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
.