Invariant fails but assert before loop verifies

Question

In the following program, the last invariant of the loop fails to verify. But if I put it as an assert before the while loop, the condition verifies. If I add that the field ia does not change, it also verifies. Why is this needed? Shouldn't this be implied by the read permissions? I can imagine that old interacts in a weird way with the loop pre-state/havocking of the state, but that doesn't explain to me why it fails. Could it be a bug?

domain VCTArray[CT] {
  function loc(a: VCTArray[CT], i: Int): CT
  
  function alen(a: VCTArray[CT]): Int
}

//  a field 
field ia: VCTArray[Ref]

//  a field 
field item: Int

method negatefirst(diz: Ref)
requires diz != null
requires acc(diz.ia, 1/2)
requires alen(diz.ia) > 0 ==> acc(loc(diz.ia, 0).item, write)
{
  // Verifies just fine
  assert alen(diz.ia) > 0 ==> (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item))
  while (false)
    invariant acc(diz.ia, 1/4) 
    // invariant diz.ia == old(diz.ia) // Adding this invariant allows the program to verify
    invariant alen(diz.ia) > 0 ==> acc(loc(diz.ia, 0).item, write)
    // Error: insufficient permission to acces loc(diz.ia, 0).item
    invariant alen(diz.ia) > 0 ==> (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item)) 
  { 
    
  }
}

My silicon version:

$ ./silicon.sh --help
Silicon 1.1-SNAPSHOT (d45da1d7+)

Answer 1

The behaviour you observed is a known difference between Silicon and Carbon, which can indeed be confusing.

Here is what's happening in Silicon: Loop bodies are essentially verified in isolation, i.e. modularly: the invariant is inhaled in an empty state, followed by the loop guard; then the body is verified. When inhaling your last invariant, its left-hand side alen(diz.ia) > 0 is assumed (on one path) and its right-hand side old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item) is (attempted to be) inhaled. Now, recall that the ongoing verification happens in isolation, in a new state: therefore, diz.ia in the current state might not reference the same object as diz.ia in the old state. If so, then alen(diz.ia) > 0 (current state) does not imply old(alen(diz.ia) > 0), and field old(loc(diz.ia, 0).item) might thus not be accessible. Consequently, assuming that the reference did not change between these two states — i.e. invariant diz.ia == old(diz.ia) — makes the program verify.

That's the purist's way of verifying a loop body; in practice, the isolation is not as strict: both verifiers frame knowledge about local variables into the loop, for variables that (syntactically) aren't assigned to in the loop body. Here's an example:

method test() {
  var i: Int := 0
  var j: Int := 0
  
  while (true)
  {
    assert i == 0 // Verified
    assert j == 0 // Rejected
    j := j
  }
}

Carbon goes a step further and also frames knowledge about fields into the loop body, for fields for which the surrounding verification scope (e.g. the method body containing the loop) retains some permissions:

field f: Int

method test(r: Ref, p: Perm) {
  inhale none < p
  inhale acc(r.f, p) && r.f == 0
  
  while (true)
    invariant acc(r.f, p/2) // Verified in Carbon, rejected by Silicon
  {
    assert r.f == 0
  }
}

The above verifies in Carbon as-is, but no longer, if you change the invariant's permissions to p (or havoc the field's value by exhale acc(r.f, p); inhale acc(r.f, p) right before the loop).

Bottom line: the Viper team should decide on the "right" semantics, and make sure both verifiers adhere to it.