1

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...?

bobismijnnaam
  • 1,361
  • 2
  • 10
  • 20

1 Answers1

1

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.

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
  • Ok, so to work around this I can use: `assert perm(g.f) > 0/1 ? acc(g.f, i * wildcard) : acc(g.f, i * 0/1)`, or use permission typed parameters. Thanks. – bobismijnnaam Apr 08 '21 at 15:33