Derive the body invariant from the loop condition

[suhr]

Currently, the following fails to check:

fn index_all<T>(slice: &[T]) {
    let mut i = 0;
    while i < slice_len(slice) {
        let el = index_slice(slice, i);
        i += 1;
    }
}

Though adding body_invariant!(i < slice_len(slice)) into the loop body fixes the issue, Prusti could derive the invariant from the loop condition.

[jmc-figueira]

I can confirm this has happened to me as well, in the following example:

    #[requires(n > 0)]
    #[ensures(result.len() == n)]
    #[ensures(forall(|i: usize| (i < result.len()) ==> result.lookup(i) == elem))]
    pub fn from_elem(elem: u64/*T*/, n: usize) -> Self {
        let mut i = 0usize;
        let mut result = VecWrapper::with_capacity(n);

        while i < n {
            body_invariant!(result.len() == i);
            body_invariant!(i < n);
            body_invariant!(forall(|k: usize| (i > 0 && k < result.len()) ==> result.lookup(k) == elem));
            result.push(elem);
            i += 1;
        }

        result
    }

Specifically, body_invariant!(i < n); is required for the method's postconditions to hold true.

[Aurel300]

This would be nice in the long term. I don't think we can infer the invariant given the loop condition in general, because the loop condition itself can have side effects or complex control flow (e.g. if there is a ? operator involved). Even so, pure loop conditions (+ maybe some other restrictions) should account for a large amount of Rust code.

[JonasAlaif]

This would be nice in the long term. I don't think we can infer the invariant given the loop condition in general, because the loop condition itself can have side effects or complex control flow (e.g. if there is a ? operator involved). Even so, pure loop conditions (+ maybe some other restrictions) should account for a large amount of Rust code.

I think this can actually be done without too much difficulty; rather than "inferring" the condition in the sense that we take the boolean expression g and stick it in as a body_invariant!(g) we can let Viper handle everything. My idea comes from the fact that we can successfully assert !g right after the loop, but why is that? Well we encode:

while {
  guard_invariant!(I_G); // Introduce this macro
  g // possibly non-pure
} {
  body_invariant!(I_B);
  B
}
assert!( !g );

as

var b0 = ⟦g⟧
if b0 {
  assert ⟦I_B⟧
  exhale loop_perms
  havoc loop_stack
  inhale loop_perms
  assume ⟦I_B⟧
  ⟦B⟧
  var bn = ⟦g⟧
  if bn {
    assert ⟦I_B⟧
    inhale false
  }
}
var t = ⟦!g⟧
assert t

Clearly the assert t succeeds (it could fail if g isn't pure, but in that case it correctly fails since it would also fail in Rust).

But what if we added:

...
  inhale loop_perms
  assume ⟦I_G⟧
  var bi = ⟦g⟧
  assume bi
  assume ⟦I_B⟧
...

As in, exhale/havoc/inhale represents one or more previous loop iterations, that is, the loop guard must clearly have been true just before we started the current iteration and so why not inhale that fact. And we don't care if ⟦g⟧ isn't pure since we are effectively pulling it out of the exhale/havoc/inhale part which should already have been over-approximating the effect of ⟦g⟧. The extra I_G invariant is only needed when ⟦g⟧ requires something to successfully verify (e.g. there is an array dereference in the guard) and should be checked at the appropriate places.

To go back to the original concern with body_invariant!(g), we can see that it would indeed cause issues with a non-pure g. Specifically, in the two assert ⟦g && Inv⟧ lines above; clearly ⟦g⟧ == true at both of these lines, but if we tried to assert ⟦g && Inv⟧ then we would be "executing" ⟦g⟧ twice possibly making the second "execution" (within the assert) evaluate to false.

[fpoli]

A minimal example is the following. The goal of this issue is to verify it out-of-the-box.

fn main() {
  let mut i = 0;
  while i < 10 {
    assert!(i < 99);
    i += 1;
  }
}

Interestingly, the following is already supported and could be used as default when no loop body invariant is specified.

fn main() {
  let mut i = 0;
  while { body_invariant!(true); i < 10 } {
    assert!(i < 99);
    i += 1;
  }
}

The semantics should be equivalent to the following (which, however, fails due to bug #389):

fn main() {
   let mut i = 5;
   assert!(true); // check the invariant before evaluating the first loop guard...
   while i < 10 {
       assert!(i < 99);
       i += 1;
       body_invariant!(true); // ... and check the same invariant at the end of every loop iteration.
   }
}