Snap encoding of array assignments

[Pointerbender]

This issue is a spin-off from #819, which revealed that currently Prusti is unable to verify programs like:

#[ensures(result <= 3)]
fn foo() -> usize {
    let mut a = [1, 2, 3];
    let mut i = 0;
    while i < 3 {
        body_invariant!(i < 3);
        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
        body_invariant!(a[i] <= i + 1);
        let tmp = a[i] + 1;
        a[i] = tmp;
        i += 1;
    }
    a[1]
}

but Prusti can verify this program okay:

#[ensures(result <= 3)]
fn bar() -> usize {
    let mut a = [1, 2, 3];
    let mut i= 0;
    while i < 3 {
        body_invariant!(i < 3);
        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
        body_invariant!(a[i] <= i + 1);
        let tmp = a[i] + 1;
        set(&mut a, i, tmp);
        i += 1;
    }
    a[1]
}

#[requires(0 <= i && i < 3)]
#[ensures(forall(|j: usize| (0 <= j && j < 3 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
#[ensures(a[old(i)] == old(v))]
fn set(a: &mut [usize; 3], i: usize, v: usize) {
    a[i] = v;
}

The underlying issue seems to be related to the snapshot encoding of a.

Some ideas that were suggested in #819 are:

1. Wait for #796 which addresses snap encoding of Rust assertions. Then we can add (debug_)assert! statements at the end of the loop which will invoke snap$__$TY$__Snap$Array$10$i32$. This one is currently blocked by the refactoring.
2. We could update the quantifier triggers for array/slice assignment to also trigger on { read$Snap$Array$10$i32$__$TY$__(X, i) }, currently those only trigger on { lookup_pure__$TY$__Array$10$i32$i32$(X, i). This would be nice for the end-user experience, because less Rust assertions would be needed. However, this may decrease overall performance because of the extra trigger and larger Viper programs when snap encoding is not needed for the verification.
3. Find another way to preserve information about the array assignment between loop iterations. Johannes also suggested this option in his master thesis in section "6.1 Future Work".

I started looking into option 2 and discovered that adding just the trigger is not sufficient to make the program verify. The Viper program for foo generates the following Viper statements for the array assignment:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

With a bit of manual hacking in the Viper program, I can make the Viper program for foo verify if I replace the above 2 statements with:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_LET_4), i) }
      0 <= i && i < 3 && !(i == _LET_5)
        ==> read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_LET_4), i)
        == old[l8](read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), i))
    )
))
inhale read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), old[l8](_33)) == __t27.val_int

Would it be desirable to implement array assignments in this snap encoded form everywhere? I believe that these are fully backwards-compatible with the non-snapshot version, due to:

1. The trigger { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) } makes sure that the quantifier is triggered in all the places were it is triggered now.
2. The Viper functions snap$__$TY$__Snap$Array$3$usize$ and lookup_pure__$TY$__Array$3$usize$usize$ both require the same access predicates, namely requires acc(Array$3$usize(self), read$()).
3. The second inhale statement and the post-condition of snap$__$TY$__Snap$Array$3$usize$ ensures that the knowledge about the array values is propagated to both the Snap and non-Snap domains:

function snap$__$TY$__Snap$Array$10$i32$(self: Ref): Snap$Array$10$i32
  requires acc(Array$10$i32(self), read$())
  ensures (forall i: Int ::
         { read$Snap$Array$10$i32$__$TY$__(result, i) }
         { lookup_pure__$TY$__Array$10$i32$i32$(self, i) }
         0 <= i && i < 10 ==>
                  read$Snap$Array$10$i32$__$TY$__(result, i)
                  == lookup_pure__$TY$__Array$10$i32$i32$(self, i))
{
  cons$Snap$Array$10$i32$__$TY$__(seq_collect$Array$10$i32$__$TY$__(self, 0))
}

However, I'm not sure about what performance implications this would bring with it, so I wanted to bounce this idea off everyone here before implementing it and creating a PR :)

Thanks!

[Pointerbender]

Actually, it turns out that the snap encoding is not needed after all! Instead of these 2 statements:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

this also does the trick of making foo verify:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      0 <= i && (i < 3 && !(i == _LET_5))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

(this works for foo, but not for the selection_sort.rs test case, unfortunately)

[vakaras]

Actually, it turns out that the snap encoding is not needed after all! Instead of these 2 statements:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

this also does the trick of making foo verify:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      0 <= i && (i < 3 && !(i == _LET_5))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

(this works for foo, but not for the selection_sort.rs test case, unfortunately)

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4? Since _1 is a local Viper variable, putting it inside old has no effect on it (or at least, it should). I am confused…

[Pointerbender]

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4?

Yup, that's the only change. I suspect that the exhale/inhale acc(Array$3$usize(_1), write) statements in between the label l8 and the array assignment have something to do with it. Maybe it prevents Viper from triggering the quantifier if _1 is "havoc'ed", but it somehow remembers old[l8](_1) from before the havoc'ing?

[Pointerbender]

Full relevant code section without LET:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } 0 <= i && (i < 3 && !(i == old[l8](_33))) ==> lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i)))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

[vakaras]

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4?

Yup, that's the only change. I suspect that the exhale/inhale acc(Array$3$usize(_1), write) statements in between the label l8 and the array assignment have something to do with it. Maybe it prevents Viper from triggering the quantifier if _1 is "havoc'ed", but it somehow remembers old[l8](_1) from before the havoc'ing?

_1 is not havocked because there is no assignment to it and that is why I am confused. _1 is just the address, the statements

  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)

havoc the memory stored at address _1, but the address itself stays the same. You should be able to assert that:

assert old[l8](_1) == _1

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

[vakaras]

Full relevant code section without LET:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } 0 <= i && (i < 3 && !(i == old[l8](_33))) ==> lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i)))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

Is this the original code? old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old. What happens if you replace old[l8](_1) with _1?

[Pointerbender]

Is this the original code?

No, I have some local changes to Prusti that generates that version (and verifies). The original statements (as currently generated from the master branch from Prusti) that don't verify for foo are:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (let _LET_4 == (old[l8](_33)) in (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) } 0 <= i && (i < 3 && !(i == _LET_4)) ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

What you describe regarding the syntactic rules sounds like what could be happening for the Viper program for foo.

old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old.

Only in this case foo only verifies with the old[l8](_1) :)

What happens if you replace old[l8](_1) with _1?

In the case of the Viper program for foo, verification fails (can be replicated on current master branch). I was trying to make a smaller Viper-only example to replicate this, but I was not able to make a smaller version by hand that fails.

[Pointerbender]

_1 is not havocked because there is no assignment to it and that is why I am confused.

Apologies :) For better context about what I mean by "havoc", I was going off of this comment in the code:

https://github.com/viperproject/prusti-dev/blob/00fa0d0958e9816c1482b76284974ea34690e6c4/prusti-viper/src/encoder/procedure_encoder.rs#L5215-L5224

[Pointerbender]

In case it helps, this small hand-crafted example which does not use old[l8](_1) in the trigger verifies okay:

method example()
{
  var _1: Ref
  var _33: Int
  _1 := builtin$havoc_ref()
  _33 := builtin$havoc_int()
  inhale acc(Array$3$usize(_1), write)
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 0) == 1
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 1) == 2
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 2) == 3
  _33 := 0
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == old[l8](_33)))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == 3
  assert read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), 1) == 2
}

I guess that this is in-line with what would be expected. I'm not sure why a similar approach fails for foo, though.

[vakaras]

old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old.

Only in this case foo only verifies with the old[l8](_1) :)

This is very confusing…

[vakaras]

_1 is not havocked because there is no assignment to it and that is why I am confused.

Apologies :) For better context about what I mean by "havoc", I was going off of this comment in the code:

https://github.com/viperproject/prusti-dev/blob/00fa0d0958e9816c1482b76284974ea34690e6c4/prusti-viper/src/encoder/procedure_encoder.rs#L5215-L5224

I see ☺. That comment should say that the contents of the array are havocked.

[vakaras]

I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to:

Would it be desirable to implement array assignments in this snap encoded form everywhere?

I think it would make our life easier if we everywhere used the same lookup function. @Aurel300 Do you see any reason not to do that?

[fpoli]

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

I'd also compare the change randomizing the Z3 seeds:

// Prusti.toml
extra_verifier_args = [ "--z3RandomizeSeeds" ]

[Pointerbender]

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

I'd also compare the change randomizing the Z3 seeds:

// Prusti.toml
extra_verifier_args = [ "--z3RandomizeSeeds" ]

The extra_verifier_args = [ "--z3RandomizeSeeds" ] seems to have no effect on the verification result of foo. Increasing the assert_timeout flag or adding extra_verifier_args = [ "--z3RandomizeSeeds", "--checkTimeout=100", "--z3SaturationTimeout=1000", "--qpSplitTimeout=1000" ] also does not result in longer verification times, indicating Z3 manages to exhaust the search space.The version { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) } consistently fails verification even with a different seed every time. The version with { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } consistently passes verification for foo.

It's starting to look more and more like this is an obscure corner case which confuses Viper/Z3 (and in a deterministic fashion despite random seeds, too :sweat_smile: ). There is more to it than just the choice for triggers. So far I've not been able to trigger the same circumstances without a loop. Maybe the mix of goto, the trigger syntax using old and "havoc'ing the contents of the array" would cause it to trip up? I'm not quite sure how to go about crafting a manual Viper example for this one, though.

[Pointerbender]

I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to:

Would it be desirable to implement array assignments in this snap encoded form everywhere?

I think it would make our life easier if we everywhere used the same lookup function. @Aurel300 Do you see any reason not to do that?

I was playing around with this a bit more today and it gets more confusing :) The version where array assignments are snapshot encoded suffer from the same quirk where the Viper program for foo only verifies if it uses the trigger { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(old[l8](_1)), i) }, but it fails verification when using a trigger without old i.e. { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), i) }.

The original version that Prusti gives me that doesn't verify is: lib.rs_prusti_example::foo 20220223 unmodified.vpr.txt. Here is an annotated version of the same program that does verify: lib.rs_prusti_example::foo 20220223 modified.vpr.txt. All changes and comments are within lines 409-426.

[vakaras]

This sounds more and more like a bug in the Viper backend. However, the examples are way too large to ask the backend developers to look into. Would be nice to get a repro on a 20 or so lines example.

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

[Pointerbender]

Would be nice to get a repro on a 20 or so lines example.

I'll see if I can whip up something during the weekend :)

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

In case we don't manage to reproduce a small example, would it be acceptable to use the old triggers until the refactoring lands?

[vakaras]

Would be nice to get a repro on a 20 or so lines example.

I'll see if I can whip up something during the weekend :)

Thanks!

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

In case we don't manage to reproduce a small example, would it be acceptable to use the old triggers until the refactoring lands?

If it has no regressions, I think we could.

[Pointerbender]

I'll see if I can whip up something during the weekend :)

This is the smallest version I could come up with: lib.rs_prusti_example::foo 20220228 small.vpr.txt

Surprisingly, the confusing behavior can be triggered without loops or goto statements!

[vakaras]

I'll see if I can whip up something during the weekend :)

This is the smallest version I could come up with: lib.rs_prusti_example::foo 20220228 small.vpr.txt

Surprisingly, the confusing behavior can be triggered without loops or goto statements!

Thank you very much for reducing the example. I have filed a Silicon issue: https://github.com/viperproject/silicon/issues/603