Failing (trivial) assertion in presence of a quantifier over a slice

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

pub fn main() {}

#[requires(forall(|i: usize|
    (0 <= i && i < slice.len()) ==> (slice[i] == i),
    triggers=[(slice[i],)]
))]
pub fn test(slice: &mut [usize]) {
    if slice.len() == 3 {
        debug_assert!(slice[0] == 0);
        debug_assert!(slice[1] == 1);
        debug_assert!(slice[2] == 2);
    }
}

Fails verification with the error:

error: [Prusti: verification error] the asserted expression might not hold
  --> src/lib.rs:30:9
   |
30 |         debug_assert!(slice[2] == 2);
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the macro `$crate::assert` (in Nightly builds, run with -Z macro-backtrace for more info)

The weird part is that the first 2 assertions are verified okay, but then Prusti misses out on the third assertion (which should hold).

[Pointerbender]

A small addendum, it seems this is because the assertions do not (always?) seem to trigger the quantifier.

The quantifier being (at the Viper level):

  inhale (let _LET_0 == (_1.val_ref) in (
    forall _0_quant_0: Int ::
    { read$Snap$Slice$usize$__$TY$__(snap$__$TY$__Snap$Slice$usize$(_1.val_ref), _0_quant_0) }
    0 <= _0_quant_0 && _0_quant_0 <= 18446744073709551615
      ==> !(0 <= _0_quant_0) || (
        !(_0_quant_0 < len$Snap$Slice$usize$__$TY$__(snap$__$TY$__Snap$Slice$usize$(_LET_0)))
        || _0_quant_0 < len$Snap$Slice$usize$__$TY$__(snap$__$TY$__Snap$Slice$usize$(_LET_0))
        && read$Snap$Slice$usize$__$TY$__(snap$__$TY$__Snap$Slice$usize$(_LET_0), _0_quant_0) == _0_quant_0
      )
  ))

while the array accesses in the Viper method are expressed as:

inhale lookup_pure__$TY$__Slice$usize$usize$(_1.val_ref, _11) == __t26
inhale lookup_pure__$TY$__Slice$usize$usize$(_1.val_ref, _21) == __t30
inhale lookup_pure__$TY$__Slice$usize$usize$(_1.val_ref, _31) == __t34

In order to verify the original example, it needs to properly trigger the quantifier at least once, so that this Viper function is called at least once, after which Silicon knows to connect lookup_pure with read$Snap:

function snap$__$TY$__Snap$Slice$usize$(self: Ref): Snap$Slice$usize
  requires acc(Slice$usize(self), read$())
  ensures [(forall i: Int :: { read$Snap$Slice$usize$__$TY$__(result, i) } { lookup_pure__$TY$__Slice$usize$usize$(self, i) } 0 <= i && i < Slice$len__$TY$__usize$(self) ==> read$Snap$Slice$usize$__$TY$__(result, i) == lookup_pure__$TY$__Slice$usize$usize$(self, i)), true]
  ensures [Slice$len__$TY$__usize$(self) == len$Snap$Slice$usize$__$TY$__(result), true]
{
  cons$Snap$Slice$usize$__$TY$__(seq_collect$Slice$usize$__$TY$__(self, 0))
}

An example of a program that does verify:

use prusti_contracts::*;

fn main() {}

#[requires(forall(|i: usize|
    (0 <= i && i < slice.len()) ==> (slice[i] == i),
    triggers=[(slice[i],)]
))]
#[requires(slice[0] == slice[0])] // dummy statement
pub fn test(slice: &mut [usize]) {
    if slice.len() == 3 {
        debug_assert!(slice[0] == 0);
        debug_assert!(slice[1] == 1);
        debug_assert!(slice[2] == 2);
    }
}

Although it is still interesting why it can verify the first 2 assertions in the original example but not the 3rd, I would expect all three assertions to fail due to the quantifier not triggering :D Also, for the working example there is no pre-condition that describes the length of slice. Should #[requires(slice[0] == slice[0])] result in a possible out-of-bounds error in this case, because the slice could be an empty slice?

Existing Github issues related to this one are #796 and #877.