Resources can be used on left of implication in assumes

Impure expressions are typically not allowed on the LHS of an implication, except in an assume :

field val: Int

method foo(r: Ref) 
    requires acc(r.val) ==> true
    ensures acc(r.val) ==> true
{
    assume acc(r.val) ==> true
    assert acc(r.val) ==> true 

    inhale acc(r.val) ==> true
    exhale acc(r.val) ==> true
}

In the above example, all uses of acc(r.val) are not allowed except for assume acc(r.val) ==> true. Isn't this a bit inconsistent, especially if you cannot assert something you have assumed?

Start by reproducing the issue's example and compare how requires, ensures, assume, assert, inhale, and exhale handle acc(r.val) on the left of implication. Determine the intended consistency rule for these constructs, then verify that the resulting behavior is covered by the relevant existing verification tests or language checks.