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 https://github.com/viperproject/carbon/issues/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...?
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.