Cannot assert wildcard permission that was in contract

[bobismijnnaam]

The following program fails to verify:

field f: Int

method m(g: Ref, i: Int)
requires acc(g.f, i * wildcard)
{
    assert acc(g.f, i * wildcard)
}

I first stumbled upon this where i was a more complex expression (specifically, an abstract function). When you turn i into a constant, it verifies. Carbon reports the error reported in viperproject/carbon#376. I might've reported the root cause of this error once before, but I wasn't sure, so I thought I'd file an issue. Is there a chance this is a bug, or is it an (expected) incompleteness?

Adding "i > 0" as a requires clause causes the example to verify, which I don't really understand. I would either expect a well-formedness error if i needed to be bigger than 0, or a pass without the "i > 0" clause...?

[mschwerhoff]

Interesting example! The observed behaviour may be surprising, but can be explained. Before we go into specifics, a bit of background: when inhaling an accessibility predicate acc(R, P), for some resource R and permission expression p, then none ≤ p is assumed. none is included because permission to R could be conditional, e.g. requires p == (b ? write : none).

In your example, this yields none ≤ i * k1, where k1 represents the first wildcard. For the latter, none < k1 < write is assumed. Observe that i == 0 is possible, in which case i * k1 would be none.

For the assert, a second wildcard k2 is introduced. Before k2 can be assumed to be "any read fraction less than what's currently being held", i.e. before none < k2 < perm(g.f) can be assumed, it must be checked that none < perm(g.f). This fails, however: perm(g.f) is none if i == 0.

Does that make sense to you? Also, would you mind asking this on StackOverflow?

[bobismijnnaam]

Okay, I see how this can happen. So the problem is:

1. perm(g.f) might be 0
2. Any wildcard is always less than what is available, but non-zero, and hence requires some permission to be available to even exist
3. This is not the case by 1), so a value for k2 cannot exist, hence error

I guess to reflect my use case I'll have to be more explicit to viper that I don't mind if the wildcard is zero (since I'm assuming you are not going to include a wildcard_or_zero type of construct. Not sure how that would work, anyway...):

method m2(g: Ref, i: Int)
requires acc(g.f, i * wildcard)
{
    assert perm(g.f) > 0/1 ? acc(g.f, i * wildcard) : acc(g.f, i * 0/1)
}

Thanks for your explanation, I think I have enough now to continue. I'll post the question on SO as well. SO post is here: https://stackoverflow.com/questions/67006707/cannot-assert-wildcard-permission-that-was-in-contract

[mschwerhoff]

I probably know too little about your use case, but I would either require 0 < i, or consider replacing wildcard by permission-typed parameters. The latter might be more appropriate if, as you write, none-permissions are actually OK. Wildcards were explicitly designed to match the intuitive requirement "some read-enabling fraction, but less than what the caller holds, so that the caller can retain a fraction itself".

[bobismijnnaam]

I'm looking into formalising/checking rewrite rules in vercors that simplify the wildcard (partially) away, and this was an edge case I was running into. So in the case of those rewrite rules going for a permission-typed parameter might not be possible, but I'll have to look into it to be sure. In any case, it's good to know about the implicit requirements of wildcard!