Use snapshot encoding for Rust assertions

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

#[requires(forall(|i: usize| (0 <= i && i < 16) ==> (array[i] > 100) ))]
pub fn assert_example(array: &[usize; 16]) {
    assert!(array[0] > 100);
}

fn main() {}

fails verification with the error:

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

error: could not compile `prusti-example` due to previous error

Digging a bit deeper, I noticed this is because the precondition is inhaled using snapshot encoding:

inhale (forall _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101: Int ::
  0 <= _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
  && _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 <= 18446744073709551615
    ==> 0 <= _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
        && _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 < 16
             ==> _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 < 16
                  && read$Snap$Array$16$usize$__$TY$__Snap$Array$16$usize$$int$$$int$(
                    snap$__$TY$__Array$16$usize$Snap$Array$16$usize(_1.val_ref),
                    _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
                  ) > 100
)

Note that because this is a user specified precondition, there are no explicit triggers defined and Viper is tasked with inferring the correct triggers. Then the assert!() is checked in the body as:

  __t5 := builtin$havoc_int()
  inhale __t5 >= 0 && 18446744073709551615 >= __t5
  assert acc(Array$16$usize(_1.val_ref), read$())
  inhale __t5 >= 0 && 18446744073709551615 >= __t5
  inhale lookup_pure__$TY$__Array$16$usize$$int$$$int$(_1.val_ref, _6) == __t5
  _5 := builtin$havoc_int()
  _5 := __t5
  label l0
  // [mir] _4 = Gt(move _5, const 100_usize)
  
  _4 := builtin$havoc_ref()
  inhale acc(_4.val_bool, write)
  _4.val_bool := _5 > 100

Here it uses a lookup_pure, but this will not trigger the quantifier from the precondition, hence the verification fails. I see two possible ways to address this problem:

First, we can use snapshot encoding for the Rust assertion, so that the implicit trigger expressions are triggered and the quantifier from the precondition is instantiated. We achieve this by using inhale read$Snap$Array$16$usize$__$TY$__Snap$Array$16$usize$$int$$$int$(snap$__$TY$__Array$16$usize$Snap$Array$16$usize(_1.val_ref), _6) == __t5 instead of inhale lookup_pure__$TY$__Array$16$usize$$int$$$int$(_1.val_ref, _6) == __t5.

The other option is to somehow add explicit triggers to the precondition so that the quantifier is instantiated whenever a lookup_pure is called, together with an extra clause in the quantifier body:

inhale (forall _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101: Int ::
  { lookup_pure__$TY$__Array$16$usize$$int$$$int$(_1.val_ref, _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101) }
  { read$Snap$Array$16$usize$__$TY$__Snap$Array$16$usize$$int$$$int$(
                    snap$__$TY$__Array$16$usize$Snap$Array$16$usize(_1.val_ref),
                    _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
                  ) }
  0 <= _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
  && _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 <= 18446744073709551615
    ==> 0 <= _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
        && _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 < 16
             ==> _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101 < 16
                  && read$Snap$Array$16$usize$__$TY$__Snap$Array$16$usize$$int$$$int$(
                    snap$__$TY$__Array$16$usize$Snap$Array$16$usize(_1.val_ref),
                    _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
                  ) > 100
                  && lookup_pure__$TY$__Array$16$usize$$int$$$int$(
                          _1.val_ref,
                          _2_quant_2c47419d7b5c4fa681d9a6f889ecb294_101
                  ) > 100
)

My gut feeling says it's probably easier to implement snapshot encoding for all Rust assertions than to modify end-user specifications on-the-fly, but I'm not sure if that would have any other implications elsewhere.

I believe I had read somewhere (can't remember where I saw this) that Vytautas already suggested before to consider using snapshot encoding for assertions, but there was no official Github issue for it yet.

[vakaras]

Yes, you are correct: my current plan is to use snapshots for all assertions.

[Pointerbender]

Are there any plans to support unsafe {} and raw pointers in Prusti in the (far) future? I could think of one hypothetical scenario that may not play nice with using only snapshot encoding (i.e. without the heap permissions) for assertions in that case:

pub fn example(value: *mut usize) -> usize {
    let ptr = unsafe { &mut *value };
    assert!(unsafe { *value } != 1); // undefined behavior
    *ptr = 1; 
    *ptr
}

fn main() {
    let mut value = 0;
    example(core::ptr::addr_of_mut!(value));
}

Here Prusti will not be able to detect the UB if it also doesn't assert the heap permissions to *value somehow. I guess this would have to be asserted outside of the snapshot encoding / Viper expression. Miri currently detects this UB okay (click Tools > Miri on the Playground). As long as unsafe {} is not supported yet by Prusti such a corner case should never show up in sound safe Rust, though, I think.

[vakaras]

Are there any plans to support unsafe {} and raw pointers in Prusti in the (far) future?

Yes, we plan to support some part of unsafe Rust in (hopefully) not so distant future.

I could think of one hypothetical scenario that may not play nice with using only snapshot encoding (i.e. without the heap permissions) for assertions in that case:

pub fn example(value: *mut usize) -> usize {
    let ptr = unsafe { &mut *value };
    assert!(unsafe { *value } != 1); // undefined behavior
    *ptr = 1; 
    *ptr
}

fn main() {
    let mut value = 0;
    example(core::ptr::addr_of_mut!(value));
}

Here Prusti will not be able to detect the UB if it also doesn't assert the heap permissions to *value somehow. I guess this would have to be asserted outside of the snapshot encoding / Viper expression. Miri currently detects this UB okay (click Tools > Miri on the Playground). As long as unsafe {} is not supported yet by Prusti such a corner case should never show up in sound safe Rust, though, I think.

For your example, permissions, unfortunately, will not help because the permission to access *value and *ptr belongs to the activation record (stack frame) and, therefore, you can access them through both places. Actually, this is probably the smallest example that shows the difference between RustBelt and Stacked Borrows: you can verify this example in RustBelt, but Stacked Borrows rejects it. There have been attempts to unify RustBelt and Stacked Borrows, but it seems that they raised more questions than answered.

[Pointerbender]

There have been attempts to unify RustBelt and Stacked Borrows, but it seems that they raised more questions than answered.

Thanks for the link to that thesis! I think this is the most intuitive explanation of RustBelt and concurrent separation logic that I've seen so far :)

Yes, we plan to support some part of unsafe Rust in (hopefully) not so distant future. For your example, permissions, unfortunately, will not help because the permission to access *value and *ptr belongs to the activation record (stack frame) and, therefore, you can access them through both places.

I'm already curious to see how the first support for unsafe Rust (perhaps even some interior mutability?) will look like! Judging by that master thesis you linked, I suspect we won't see a full fledged Stacked Borrows implementation for the first version :smile: (or maybe not ever if you go an entirely different route than SB)

[Pointerbender]

For your example, permissions, unfortunately, will not help because the permission to access *value and *ptr belongs to the activation record (stack frame) and, therefore, you can access them through both places. Actually, this is probably the smallest example that shows the difference between RustBelt and Stacked Borrows: you can verify this example in RustBelt, but Stacked Borrows rejects it.

I had a random thought about this one today: in Prusti's case, would it be possible to introduce an "implicit frame" whenever a raw pointer (*const T/*mut T) is dereferenced, in order to catch the undefined behavior under Stacked Borrows rules from that example? Or would this cause problems for other situations?

[vakaras]

What do you mean by an implicit frame? The fact that permissions are assigned to stack frames comes from the underlying Viper infrastructure.

[Pointerbender]

Hmm, I tried to see if I could illustrate this with a Viper example, but so far I came up empty handed and now have more questions than before, haha. I think I'll need to ponder on this one a bit more and possibly come back to it later, otherwise I'll risk derailing the entire conversation into many other interesting topics :D