ASSERT_TIMEOUT=0 not properly passed to Viper?

[Pointerbender]

I have an example which I believe should verify:

extern crate prusti_contracts;
use prusti_contracts::*;

pub const MAX_DEPTH: usize = usize::BITS as usize;

pub struct Path {
    current: usize,
    depth: usize,
    entries: [usize; MAX_DEPTH],
    max_counts: [usize; MAX_DEPTH],
}

impl Path {
    #[pure]
    pub fn invariant(&self) -> bool {
        self.entries.len() == MAX_DEPTH
            && self.max_counts.len() == MAX_DEPTH
            && self.entries.len() == self.max_counts.len()
            && self.current < MAX_DEPTH
            && self.depth < MAX_DEPTH
            && self.current <= self.depth
    }

    #[requires(self.invariant())]
    #[ensures(self.current == 0)]
    #[ensures(self.depth == 0)]
    #[ensures(self.entries[0] == 0)]
    #[ensures(self.invariant())]
    pub fn reset(&mut self) {
        self.current = 0;
        self.depth = 0;
        self.entries[0] = 0;
        assert!(self.entries.len() == self.max_counts.len());
        assert!(self.current < MAX_DEPTH);
        assert!(self.depth < MAX_DEPTH);
        assert!(self.current <= self.depth);
        assert!(self.entries[0] == 0);
    }
}

pub fn main() {}

Prusti fails the verification with the error message (with setting ASSERT_TIMEOUT=0 "Set to 0 to disable timeout.") after about 1 minute and 25 seconds:

error: [Prusti: verification error] the asserted expression might not hold
  --> src/lib.rs:37:9
   |
37 |         assert!(self.entries[0] == 0);
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = 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
Command exited with non-zero status 101

The weird part is, if I dump the resulting program with DUMP_VIPER_PROGRAM=true and try to verify the program for target/verify/log/viper_program/lib.rs-Path::reset.vpr using Viper IDE in VS Code, it tells me Viper: Verification of lib.rs-Path::reset.vpr timed out after 100000ms the first time I run the example (i.e. during a "cold run"), but it verifies okay and without errors during a subsequent "warm run" in 98 seconds (and then okay in further subsequent runs in under 2 seconds).

I have the line assert_timeout = 0 in my Prusti.toml and I'm running the Cargo project as PRUSTI_DUMP_VIPER_PROGRAM=true PRUSTI_ASSERT_TIMEOUT=0 ASSERT_TIMEOUT=0 cargo-prusti. If I remove the last assert!() from the example, it verifies okay from the command line using cargo-prusti. Note that the identical post-condition #[ensures(self.entries[0] == 0)] is verified okay, despite the last assertion being identical. Unfortunately I was not able to make an even more minimal example. Removing any line makes it verify okay, further hinting at a timeout issue.

This gives me the suspicion that the ASSERT_TIMEOUT=0 argument is not passed to the Prusti server properly (or to the back-end). I took a quick look at the code, but did not see anything extremely suspicious there (assuming it uses the Silicon back-end by default). The only thing I could not verify, is if it is passed down properly in file prusti-common/src/verification_service.rs, as I couldn't find the manual for the CLI arguments passed to Silicon (in this case vec!["--assertTimeout".to_string(), config::assert_timeout().to_string()]) nor the code that would pass the extended arguments to the backend. There is some commented out logic in prusti-viper/src/verifier.rs, that seems like it used to handle it, but couldn't find where it is handled now in the latest version from the master branch.

Did I hit some kind of bug/out-of-date documentation/unsupported feature here by any chance? :) Thanks!

p.s. is there any way to speed up the verification of the example program? 100+ seconds seems like a lot for such a relatively simple program. Other programs of similar size often verify in matter of mere seconds (sometimes even in under a second), which is why the verification time seems a little surprising in this case. I guess it's related to the array size (64 elements on my architecture), which seems to generate a lot of statements in the Viper program.

[fpoli]

The Viper parameter is documented here: https://github.com/viperproject/silicon/blob/a8c8bce4967919b2ae652a28857a6be536c8d0f6/src/main/scala/Config.scala#L206-L210

It's then converted to Z3 here: https://github.com/viperproject/silicon/blob/16fd1f6412ab1b3b09d5e2acea637e47b6f4154a/src/main/scala/decider/Z3ProverStdIO.scala#L293

With PRUSTI_DUMP_DEBUG_INFO=true you should find at log/viper/*.smt2 the dump of the commands that Viper sends to Z3. I would expect to find many (set-option :timeout <your_value>) lines in there (or none, if you disabled the timeout). Try to see if there are still timeouts in the dump. If so, there might be other kinds of timeouts to disable in Viper.

Anyway, the assert timeout is not the only parameter that might influence the verification time. Prusti sends the program to Viper as a Java object, not as a string. So, it's possible that Viper generates slightly different Z3 command that turn out to take much more (or less) to run. You can check these issues regarding the Z3 seed to learn more. Silicon's z3RandomizeSeeds parameter can be used to try random seeds.

Generating lots of Viper statements might increase the verification time, yes. Some statements are much more expensive than others (fold, unfold, quantifiers) while others are very cheap (boolean local variables, domain functions). We are working on that. For the short term, adding caching might be the easiest solution (#722).

[Pointerbender]

Thank you for the pointers!

I ran the example in different configurations to see what's in the *.smt2 files. For all runs I used the following basic Prusti.toml configuration:

check_overflows = true
check_panics = true
skip_unsupported_features = true

And then varied the assertTimeout parameter in both the command line and in Prusti.toml. Below are the results. In scenarios 1 through 4 we see both the assert_timeout = 300000 (5 minutes) and assert_timeout = 0 represented in the *.smt2 files. Scenarios 1 & 3 and scenarios 2 & 4 give identical results. However, since all verifications fail in under 90 seconds, it seems likely that the verification trips over one of the other set-option :timeout statements present in the *.smt2 files. In scenario 5 it defaults to a timeout of 10000 when no timeout is specified (as defined in prusti-common/src/config.rs).

Some statements are much more expensive than others (fold, unfold, quantifiers)

In the Viper program for pub fn reset() the function m_invariant__$TY$__Snap$struct$m_Path$$bool$ looks suspicious :) Its function body is 83094 characters long (out of the 128633 bytes for the entire Viper program, about 65% of the entire program size including comments). The program has 161 inhale statements, 11 exhale statements, 4 fold statements, 3 unfold statements and 8 unfolding statements.

adding caching might be the easiest solution

This sounds promising!

Scenario 1: Command line parameter PRUSTI_ASSERT_TIMEOUT=300000

Prusti.toml config changes: None Command: PRUSTI_DUMP_DEBUG_INFO=true PRUSTI_ASSERT_TIMEOUT=300000 time cargo-prusti Running time: 1:27.69 elapsed

$ grep -ri timeout target/verify/log/viper_tmp/ | sort | uniq
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 300000)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-01.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-02.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-03.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-04.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 20)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 300000)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 40)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 500)

Scenario 2: Command line parameter PRUSTI_ASSERT_TIMEOUT=0

Prusti.toml config changes: None Command: PRUSTI_DUMP_DEBUG_INFO=true PRUSTI_ASSERT_TIMEOUT=0 time cargo-prusti Running time: 1:26.77 elapsed

$ grep -ri timeout target/verify/log/viper_tmp/ | sort | uniq
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 0)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-01.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-02.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-03.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-04.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 0)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 20)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 40)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 500)

Scenario 3: Prusti.toml parameter assert_timeout = 300000

Prusti.toml config changes: assert_timeout = 300000 Command: PRUSTI_DUMP_DEBUG_INFO=true time cargo-prusti Running time: 1:28.11 elapsed

$ grep -ri timeout target/verify/log/viper_tmp/ | sort | uniq
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 300000)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-01.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-02.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-03.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-04.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 20)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 300000)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 40)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 500)

Scenario 4: Prusti.toml parameter assert_timeout = 0

Prusti.toml config changes: assert_timeout = 0 Command: PRUSTI_DUMP_DEBUG_INFO=true time cargo-prusti Running time: 1:29.45 elapsed

$ grep -ri timeout target/verify/log/viper_tmp/ | sort | uniq
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 0)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-01.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-02.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-03.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-04.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 0)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 20)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 40)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 500)

Scenario 5: No additional parameters

Prusti.toml config changes: None Command: PRUSTI_DUMP_DEBUG_INFO=true time cargo-prusti Running time: 1:29.45 elapsed

$ grep -ri timeout target/verify/log/viper_tmp/ | sort | uniq
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 10000)
target/verify/log/viper_tmp/logfile-00.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-01.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-02.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-03.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-04.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-05.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-06.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-07.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 100)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 10000)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 20)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 40)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 50)
target/verify/log/viper_tmp/logfile-08.smt2:(set-option :timeout 500)

[Pointerbender]

Fun additional detail, when I comment out the lines related to calling .len() on an array inside pub fn invariant(), its Viper pure function body shrinks to a mere 488 characters and the entire cold verification run succeeds in around 30 seconds.

impl Path {
    #[pure]
    pub fn invariant(&self) -> bool {
            self.current < MAX_DEPTH
            && self.depth < MAX_DEPTH
            && self.current <= self.depth
    }
...
}

[fpoli]

Good catch! The encoding of Path::invariant seems to take 20 seconds (using a debug build of Prusti). This is very unusual, the encoding is very inefficient.

All pure functions are temporarily encoded as impure (as VIper methods) by Prusti, and it turns out that the impure encoding of a move of a &[usize] is very verbose:

  // [mir] _8 = move _9 as &[usize] (Pointer(Unsize))
  label l1
  _8 := builtin$havoc_ref()
  inhale acc(_8.val_ref, write)
  inhale acc(Slice$usize(_8.val_ref), read$())
  inhale Slice$len__$TY$__Slice$usize$$int$(_8.val_ref) == 64
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 0) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 0)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 1) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 1)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 2) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 2)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 3) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 3)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 4) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 4)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 5) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 5)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 6) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 6)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 7) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 7)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 8) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 8)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 9) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 9)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 10) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 10)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 11) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 11)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 12) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 12)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 13) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 13)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 14) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 14)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 15) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 15)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 16) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 16)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 17) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 17)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 18) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 18)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 19) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 19)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 20) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 20)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 21) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 21)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 22) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 22)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 23) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 23)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 24) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 24)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 25) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 25)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 26) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 26)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 27) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 27)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 28) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 28)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 29) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 29)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 30) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 30)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 31) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 31)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 32) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 32)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 33) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 33)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 34) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 34)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 35) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 35)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 36) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 36)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 37) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 37)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 38) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 38)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 39) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 39)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 40) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 40)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 41) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 41)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 42) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 42)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 43) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 43)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 44) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 44)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 45) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 45)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 46) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 46)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 47) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 47)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 48) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 48)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 49) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 49)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 50) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 50)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 51) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 51)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 52) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 52)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 53) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 53)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 54) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 54)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 55) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 55)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 56) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 56)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 57) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 57)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 58) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 58)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 59) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 59)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 60) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 60)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 61) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 61)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 62) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 62)
  inhale lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, 63) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, 63)

There are some things to improve:

1. Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix.

   forall i: Int :: 0 <= i && i < 64 ==> lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, i)
   

2. The pure encoding (Viper function) would be much more efficient in this case. We should switch to it soon.

[fpoli]

Regarding the remaining timeouts in the smt2 files, my guess is that they come from other Silicon options, like

https://github.com/viperproject/silicon/blob/a8c8bce4967919b2ae652a28857a6be536c8d0f6/src/main/scala/Config.scala#L212-L228

You should be able to set them in Prusti.toml with something like

extra_verifier_args = [ "--checkTimeout=100",  "--z3SaturationTimeout=1000" ]

[Aurel300]

1. Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix.

forall i: Int :: 0 <= i && i < 64 ==> lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, i)

We should somehow choose a bound to decide whether we should "inline" the quantification or not. My hope is that for very small slice lengths, the quantifier might be less efficient of an encoding. Additionally, we should really make sure to generate sufficient triggers on such a quantification (maybe this is actually why we are not generating quantifiers atm…). It would be very bad UX if a function verified for one slice length but not for a larger one.

[Pointerbender]

You should be able to set them in Prusti.toml

Nice! I'll give this a try. Although my guess would be that the default parameters would suffice once the encoding performance is fine-tuned :) Thanks!

[Pointerbender]

Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix.

forall i: Int :: 0 <= i && i < 64 ==> lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_8.val_ref, i)

I'd like to create a PR to fix this one :) The inefficient encoding happens here:

https://github.com/viperproject/prusti-dev/blob/fd6d4826227dff9d7a2f60c913de02410e6e6244/prusti-viper/src/encoder/procedure_encoder.rs#L5883-L5901

Additionally, we should really make sure to generate sufficient triggers on such a quantification

Does something like this seem appropriate?

  inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
  inhale (forall i: Int :: { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) } { lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i) } 0 <= i && i < 64 ==> lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i))

I've noticed in another place that no explicit triggers are used for the inhale statement. Is there a reason for that? Could it help performance if I add the triggers there too?

My hope is that for very small slice lengths, the quantifier might be less efficient of an encoding.

I did a quick test (with the above triggers included), but at first glance there is no noticeable performance difference when calling .len() on an array between multiple inhale statements or a single inhaled quantifier. If there is a difference, it's milliseconds on a 2+ second run, which I think falls within the variance when running the same test multiple times. Perhaps for more complicated examples that repeatedly trigger the quantification the performance difference would be more noticeable, but I haven't tested it that thoroughly.

[fpoli]

Does something like this seem appropriate?

inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
inhale (forall i: Int ::
   { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) }
   { lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i) }
   0 <= i && i < 64 ==>
       lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
 )

It looks good to me :+1:

[Pointerbender]

It looks good to me :+1:

Thanks!

I've noticed in another place that no explicit triggers are used for the inhale statement. Is there a reason for that? Could it help performance if I add the triggers there too? https://github.com/viperproject/prusti-dev/blob/fd6d4826227dff9d7a2f60c913de02410e6e6244/prusti-viper/src/encoder/procedure_encoder.rs#L2716-L2720

So I looked a bit deeper into this question. This generates Viper code like:

  // [mir] _9 = <[usize; 127] as std::ops::Index<std::ops::Range<usize>>>::index(move _10, move _11) -> [return: bb4, unwind: bb21]
  
  label l12
  _9 := builtin$havoc_ref()
  inhale acc(ref$Slice$usize(_9), read$())
  unfold acc(ref$Slice$usize(_9), read$())
  inhale Slice$len__$TY$__Slice$usize$$int$(_9.val_ref) == _11.f$end.val_int - _11.f$start.val_int
  inhale (forall i: Int, j: Int ::
    0 <= i && (
      i < Slice$len__$TY$__Slice$usize$$int$(_9.val_ref) && (
        j == i + _11.f$start.val_int && (
          _11.f$start.val_int <= j && j < _11.f$end.val_int
        )
      )
    ) ==>
        lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i) == lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
  )

There are no explicit triggers defined. The Viper manual says "If no triggers are specified, Viper will infer them automatically with a heuristics based on the body of the quantifier. In some unfortunate cases this automatic choice will not be good enough and can lead to either incompletenesses (necessary instantiations which are not made) or matching loops; it is recommended to always specify triggers on Viper quantifiers."

Is there any way to find out which triggers were inferred by Viper? I imagine it only has two choices for the triggers in the above forall statement (due to that "Each quantified variable must occur at least once in a trigger set."):

{
  lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i),
  lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
}

and/or the trigger:

{
  lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i),
  lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j),
  Slice$len__$TY$__Slice$usize$$int$(_9.val_ref)
}

Would it be correct to hard-code only the first trigger explicitly? Would it be "incomplete" if Viper only inferred the latter trigger?

Thanks!

[fpoli]

Is there any way to find out which triggers were inferred by Viper?

Not that I'm aware of. (But it would be a useful feature to request. Dafny has a flag to report to the user the triggers that have been inferred automatically.)

Would it be correct to hard-code only the first trigger explicitly?

Yes, I don't see any incompleteness or maching loop with that.

Would it be "incomplete" if Viper only inferred the latter trigger?

It would be the exactly same because we always generate an inhale Slice$len__$TY$__Slice$usize$$int$(_9.val_ref) == ..., which provides the extra trigger just before inhaling the quantifier:

https://github.com/viperproject/prusti-dev/blob/fd6d4826227dff9d7a2f60c913de02410e6e6244/prusti-viper/src/encoder/procedure_encoder.rs#L2680-L2682

Of the two, I would use the smaller set of triggers, such that Z3 has to check less stuff when instantiating quantifiers.

[Pointerbender]

Great, thank you! I will proceed with the smaller set for the trigger in that case:

{
  lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i),
  lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
}

Revisiting the other forall quantifier, we discussed using two disjoint sets of triggers:

inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
inhale (forall i: Int ::
   { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) }
   { lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i) }
   0 <= i && i < 64 ==>
       lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
 )

Is there some performance to be gained if we make this a single trigger set? Like so:

inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
inhale (forall i: Int ::
   {
        lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i),
        lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
   }
   0 <= i && i < 64 ==>
       lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
 )

The idea here is that by reducing the trigger area, the quantifier will be instantiated less often, leading to faster verification times where it is not triggered, because Z3 is then steered clear of the additional search space the quantifier would generate.

Of the two, I would use the smaller set of triggers, such that Z3 has to check less stuff when instantiating quantifiers.

In the mental model I've built so far around Viper/Z3/quantifiers, Z3 checks two different things:

1. Whether to instantiate the quantifier or not by looking at the triggers.
2. Expand the search space if the quantifier is triggered.

Intuitively, I would think that the second step is the most "expensive". If this is indeed the case, does that mean that it could lead to better performance on average if we use 1 trigger instead of two disjoint triggers? Or would I need to benchmark this to be sure? If this is indeed leads to better performance, then I also see some other candidates that could benefit from an additional expression in the trigger set, e.g.such as here on line 5248:

https://github.com/viperproject/prusti-dev/blob/fd6d4826227dff9d7a2f60c913de02410e6e6244/prusti-viper/src/encoder/procedure_encoder.rs#L5237-L5250

I could make the trigger set { lookup_array_i, old(lookup_array_i) } in order to steer Z3 clear of this quantifier for the case where both expressions aren't available, in the hopes of making Prusti faster in those cases.

[fpoli]

Is there some performance to be gained if we make this a single trigger set?

Your mental model is correct. A single trigger set would trigger in strictly less cases than the two sets, so the former would cause less instantiations and the search space would be smaller. However, it might be less complete, like in the following case.

Imagine that the user writes the following precondition

forall i: Int ::
    { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) }
    0 <= i && i < 64 ==> lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) > 100

then in the body we create a slice

inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
inhale (forall i: Int ::
   {
        lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i),
        lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
   }
   0 <= i && i < 64 ==>
       lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
)

and finally the user wants to assert the following postcondition

lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i) > 100

In this case both quantifiers would never be instantiated because the trigger lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) never matches an expression, thus the verifier won't be able to prove the postcondition. (In some lucky cases Z3 might still pick the trigger from the body of the first quantifier, but that's unusual, it's subject to heuristics, it's not reliable...)

Because of cases like this, we usually specify all triggers that might be useful for the user, provided that they are not redundant and that they don't cause matching loops (see slide 103 of these slides for an example of a matching loop). Finding matching loops involving many quantifiers is usually hard; the axiom-profiler is in some cases useful.

Back to the quantifier that you mentioned, I would keep the two small sets of triggers because I don't see obvious matching loops. If you find any, we should reconsider.

[fpoli]

Note that reducing quantifier instantiations might make verification of some programs slower. For example, a Rust function with a precondition forall i :: { f(i), g(i), h(i) ... } false and a hard-to-verify but correct body is trivial to verify if the quantifier gets instantiated, otherwise it might take very long.

[Pointerbender]

That makes total sense now, thank you for the clear examples! :smile:

However, it might be less complete, [...] In this case both quantifiers would never be instantiated because the trigger lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) never matches an expression, thus the verifier won't be able to prove the postcondition.

In that case I think it means that the suggested trigger for the quantification for the ranges is also incomplete:

{
  lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i),
  lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
}

Should we replace it with two inhaled quantifiers? Like so:

inhale forall i: Int :: { lookup_pure(array, i) } start <= i && i < end ==> forall j: Int :: { j in [0..slice_length) } 0 <= j && j < slice_length ==> lookup_pure(array, i) == lookup_pure(slice, j)
inhale forall j: Int :: { lookup_pure(slice, j) } 0 <= j && j < slice_length ==> forall i: Int :: { i in [start..end) } start <= i && i < end ==> lookup_pure(array, i) == lookup_pure(slice, j)

[fpoli]

Should we replace it with two inhaled quantifiers? Like so:

inhale forall i: Int :: { lookup_pure(array, i) } start <= i && i < end ==> forall j: Int :: { j in [0..slice_length) } 0 <= j && j < slice_length ==> lookup_pure(array, i) == lookup_pure(slice, j)
inhale forall j: Int :: { lookup_pure(slice, j) } 0 <= j && j < slice_length ==> forall i: Int :: { i in [start..end) } start <= i && i < end ==> lookup_pure(array, i) == lookup_pure(slice, j)

1. Something is wrong in those quantifiers. Probably a j == i + ... && condition is missing.
2. It should be possible to merge the two inhale to a single statement.
3. If i in [start..end) is just start <= i && i < end then it cannot be used as trigger. There should be a function call.
4. In the original quantifier we used two separate quantified variables on purpose to avoid a matching loop, and that forces us to mention two function calls in the triggering set. I'm not sure how to avoid that. I don't think that nesting the quantifiers helps.

[Pointerbender]

1. Something is wrong in those quantifiers. Probably a j == i + ... && condition is missing.
2. It should be possible to merge the two inhale to a single statement.
3. If i in [start..end) is just start <= i && i < end then it cannot be used as trigger. There should be a function call.
4. In the original quantifier we used two separate quantified variables on purpose to avoid a matching loop, and that forces us to mention two function calls in the triggering set. I'm not sure how to avoid that. I don't think that nesting the quantifiers helps.

Many thanks for those (late Friday!) pointers, that allowed me to play some more with it this weekend :smile:

I think I may have cracked it. I scribbled down a slightly simplified version directly in Viper to see if my proof-of-concept can withstand the next round of peer review before I implement it in Prusti :)

field val_int: Int

field val_ref: Ref

function Slice$len__$TY$__Slice$usize$$int$(self: Ref): Int
  requires acc(Slice$usize(self), read$())
  ensures result >= 0
  ensures result <= 18446744073709551615


function lookup_pure__$TY$__Array$127$usize$$int$$$int$(self: Ref, idx: Int): Int
  requires acc(Array$127$usize(self), read$())
  requires 0 <= idx
  requires idx < 127


function lookup_pure__$TY$__Slice$usize$$int$$$int$(self: Ref, idx: Int): Int
  requires acc(Slice$usize(self), read$())
  requires 0 <= idx
  requires idx < Slice$len__$TY$__Slice$usize$$int$(self)

function read$(): Perm
  ensures none < result
  ensures result < write

predicate Array$127$usize(self: Ref)

predicate Slice$usize(self: Ref) 

predicate ref$Array$127$usize(self: Ref) {
  acc(self.val_ref, write) && acc(Array$127$usize(self.val_ref), write)
}

predicate ref$Slice$usize(self: Ref) {
  acc(self.val_ref, write) && acc(Slice$usize(self.val_ref), write)
}

predicate usize(self: Ref) {
  acc(self.val_int, write) && (0 <= self.val_int && self.val_int <= 18446744073709551615)
}

method m_range() returns (_0: Ref) {
    var array: Ref;
    var start: Ref;
    var end: Ref;

    // inhale preconditions
    inhale acc(ref$Array$127$usize(array), read$());
    inhale acc(array.val_ref, read$());
    inhale acc(Array$127$usize(array.val_ref), read$());
    inhale acc(usize(start), read$());
    inhale acc(start.val_int, read$());
    inhale 0 <= start.val_int && start.val_int <= 127;
    inhale acc(usize(end), read$());
    inhale acc(end.val_int, read$());
    inhale 0 <= end.val_int && end.val_int <= 127;
    inhale start.val_int <= end.val_int;
    inhale forall j: Int :: { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) }
        0 <= j && j < 127 ==> lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) > 100
    label pre;

    // construct the new slice
    inhale acc(ref$Slice$usize(_0), write);
    inhale acc(_0.val_ref, write);
    inhale acc(Slice$usize(_0.val_ref), write);
    inhale Slice$len__$TY$__Slice$usize$$int$(_0.val_ref) == end.val_int - start.val_int;
    assert Slice$len__$TY$__Slice$usize$$int$(_0.val_ref) <= 127;

    // place the knowledge about the elements from the array into the new slice
    inhale (
        forall j: Int :: { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) }
        start.val_int <= j
        && j < end.val_int
        && j + start.val_int < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref)
        ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, j + start.val_int) == lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j)
    ) && (
        forall i: Int :: { lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) }
        0 <= i
        && i < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref)
        && i + start.val_int < 127
        ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) == lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, i + start.val_int)
    )

    // exhale postconditions
    exhale Slice$len__$TY$__Slice$usize$$int$(_0.val_ref) > 0 ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, 0) > 100

}

Here I took your counter example for when a single double trigger is not properly matched (pre: forall j: Int :: { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) } 0 <= j && j < 127 ==> lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) > 100 and post: lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, 0) > 100). To my initial surprise, the above Viper code does not create a matching loop and it verifies successfully in under a second. Thinking about it deeper, I think that's because the triggers for the quantifiers are, respectively:

{ lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) }
{ lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) }

When either of the quantifiers is instantiated, this yields the additional expressions, respectively:

lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, j + start.val_int)
lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, i + start.val_int)

Even though the evaluation of the expressions may yield j + start.val_int == i at the "value" level, at the "expression" level (i.e. before evaluation) these are not equal. Hence, instantiating either quantifier does not result in triggering the other quantifier, because the additional expression is not of a form that matches the trigger expression.

I believe the above proof-of-concept should address the last 4 feedback points. Fingers crossed I got it fully right this time :smile: Thanks!

[Pointerbender]

p.s. if we end up implementing the above solution, then we'd have to use snapshot encoding for the expressions in the quantifiers instead, otherwise programs like these won't be able to be verified by Prusti due to that the right quantifiers won't be triggered/instantiated:

#[requires(forall(|i: usize| (0 <= i && i < 16) ==> (array[i] > 100) ))]
#[ensures(result[0] > 100)]
pub fn example(array: &[usize; 16]) -> &[usize] {
    &array[4..8]
}

Using snapshot encoding for logic related to arrays/slices is also slightly relevant to #709 I believe.

[fpoli]

    inhale (
        forall j: Int :: { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) }
        start.val_int <= j
        && j < end.val_int
        && j + start.val_int < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref)
        ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, j + start.val_int) == lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j)
    ) && (
        forall i: Int :: { lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) }
        0 <= i
        && i < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref)
        && i + start.val_int < 127
        ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) == lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, i + start.val_int)
    )

I'm afraid a matching loop is there, but in your case it terminates quickly just because the instantiations (bounded in depth by some Z3 parameter: smt.qi.eager_threshold and smt.qi.lazy_threshold) happen to be lightweight enough for Z3. Consider the following example. For small k it verifies because the quantifiers are instantiated in what we call a matching loop. For high values of k the solver reaches its exploration bounds and it gives up, reporting a possible verification error. In a more complicated program, the latter might only happen after hours, if even with exploration bounds the search space is too big. That's what we aim to prevent by avoiding matching loops as much as possible. In some cases it meas that the tool is less complete, but in such cases it's usually enough for the user to manually add a dummy statement that mentions the needed triggers. It's not ideal, but it's better than having a tool that sometimes takes hours to terminate without giving an explanation and without giving to the (expert) user an escape hatch.

function foo(i: Int): Int
function bar(i: Int): Int

method test() {
	inhale forall i: Int :: { foo(i) } foo(i) == bar(i + 1);
	inhale forall j: Int :: { bar(j) } foo(j + 1) == bar(j);
	inhale foo(0) == 0;
	inhale bar(0) == 0;
	var k: Int := 50;
	assert foo(k) == bar(k); // With my Viper version it verifies when k is 50, but not when it's 51
}

[fpoli]

Btw, kudos for preparing a complete Viper example! I'm impressed :)

[fpoli]

p.s. if we end up implementing the above solution, then we'd have to use snapshot encoding for the expressions in the quantifiers instead, otherwise programs like these won't be able to be verified by Prusti due to that the right quantifiers won't be triggered/instantiated:

I think @vakaras already has some plans for that.

[Pointerbender]

I'm afraid a matching loop is there, but in your case it terminates quickly just because the instantiations (bounded in depth by some Z3 parameter: smt.qi.eager_threshold and smt.qi.lazy_threshold) happen to be lightweight enough for Z3.

Ahhh bummer :)

Btw, kudos for preparing a complete Viper example! I'm impressed :)

Thank you! Many thanks for all the examples that you keep feeding me, this helps me grasp this much faster and I'm having a lot of fun in doing so :)

Is there anything we can do to fool Z3 into reliably aborting the matching loop early? This seems to verify very fast despite the high k:

field hardstop: Bool

function foo(r: Ref, i: Int): Int
function bar(r: Ref, i: Int): Int

method test() {
    var a: Ref;
    var b: Ref;
    inhale acc(a.hardstop, write);
    inhale acc(b.hardstop, write);
    inhale a.hardstop == false && forall i: Int :: { foo(a, i) } (a.hardstop == false ==> foo(a, i) == bar(b, i + 1) && a.hardstop == true);
    inhale b.hardstop == false && forall j: Int :: { bar(b, j) } (b.hardstop == false ==> foo(a, j + 1) == bar(b, j) && b.hardstop == true);
    inhale foo(a, 0) == 0;
    inhale bar(b, 0) == 0;
    var k: Int := 1000000000000000;
    assert foo(a, k) == bar(b, k);
}

[fpoli]

Is there anything we can do to fool Z3 into reliably aborting the matching loop early? This seems to verify very fast despite the high k:

That's already done by the smt.qi.eager_threshold and smt.qi.lazy_threshold. By default they are at 50 or 100; I don't remember the exact value. Once you get the verification error (because of the threshold), I expect that further increasing k should not increase the verification time.

[fpoli]

(In your latest example assert false; verifies too.)

[Pointerbender]

This is a really fun exercise so far :) I have a another idea.

Instead of the quantifier used for slicing an array:

  inhale (forall i: Int, j: Int ::
    {
      lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i),
      lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
    }
    (
      0 <= i
      && i < Slice$len__$TY$__Slice$usize$$int$(_9.val_ref)
      && j == i + _11.f$start.val_int
      && _11.f$start.val_int <= j && j < _11.f$end.val_int
       ==>
          lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i) == 
          lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j)
    )
  )

Could there be a reason against using something like this instead?

    inhale (forall i: Int ::
      { lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) }
      (
        0 <= i
        && i < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref)
        && start.val_int + i < 127
        ==>
          lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) ==
          lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, start.val_int + i)
      )
    )

This avoids using a second variable and only triggers when the derived slice is accessed (without matching loop). The second example triggers in all the cases where the first example would, but the second one is more complete (in the sense that it would not require end-users to insert a dummy statement to trigger the quantifier, which can be a better user experience).

[Pointerbender]

p.s. to elaborate a bit further on why I chose { lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) } as the trigger and not { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) } as the only trigger:

If we were to trigger on the array lookup instead, this would not gain any additional knowledge about the array element, unless that same element was already looked up somewhere in the derived slice. Hence, if any new knowledge becomes available through the slice element, it is sufficient to only trigger the quantifier through the lookup of the slice element in order to make the knowledge transfer to the array element.

I suspect we can also apply the same reasoning to the other quantifier discussed in this Github issue (where we use a quantifier instead of N statements during the move/unsizing of a [usize; N] into a &[usize]):

inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64
inhale (forall i: Int ::
   { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) }
   { lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i) }
   0 <= i && i < 64 ==>
       lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) == lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)
 )

by removing the trigger { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) } in order to reduce the surface area of the triggers and hope to squeeze a little extra performance out of it. The idea is that triggering the quantifier through an array lookup does not yield any useful extra information (even if this in turn triggers other quantifiers), unless there exists a consumer of this extra knowledge somewhere else down the program (e.g. a post-condition or an assert/exhale). If there is such a consumer, then the quantifier will still be triggered by the slice lookup, even if the consumer of that knowledge is in itself a quantifier. For example, this verifies:

method verifies() {
    var list: Seq[Int];
    var len: Int := 16;
    inhale |list| == len;
    inhale forall i: Int :: { list[i] } 0 <= i && i < len ==> list[i] > 100;
    assert forall i: Int :: { list[i] } 0 <= i && i < len ==> list[i] > 25;
    exhale forall i: Int :: 0 <= i && i < len ==> list[i] > 25;
}

But this doesn't:

method fails() {
    var list: Seq[Int];
    var len: Int := 16;
    inhale |list| == len;
    assert forall i: Int :: { list[i] } 0 <= i && i < len ==> list[i] > 25;
    exhale forall i: Int :: { list[i] } 0 <= i && i < len ==> list[i] > 25;
}

EDIT after the post (playing devil's advocate here): I can think of one hypothetical Rust counter example where removing the { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) } trigger would require the end-user to insert a dummy statement to make this verify:

#[requires(forall(|i: usize| (0 <= i && i < 16) ==> ((array as &[usize])[i] > 100)))]
#[ensures(forall(|i: usize| (0 <= i && i < 16) ==> (array[i] > 100)))]
fn counter_example(array: &[usize; 16]) -> &[usize; 16] {
     array
}

So I guess at least it's a trade-off between supporting some (uncommon?) specifications in a user-friendly way and performance after all for the unsizing case :)

[fpoli]

playing devil's advocate here

That's the right approach :)

So I guess at least it's a trade-off between supporting some (uncommon?) specifications in a user-friendly way and performance after all for the unsizing case :)

Yes, I think so too. I expect that converting an array to a slice is far more common than converting a slice to an array. It makes sense to give the best user experience for the former case.

by removing the trigger { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) } in order to reduce the surface area of the triggers and hope to squeeze a little extra performance out of it. The idea is that triggering the quantifier through an array lookup does not yield any useful extra information (even if this in turn triggers other quantifiers), unless there exists a consumer of this extra knowledge somewhere else down the program (e.g. a post-condition or an assert/exhale). If there is such a consumer, then the quantifier will still be triggered by the slice lookup, even if the consumer of that knowledge is in itself a quantifier.

The difference should be observable in a program that calls a trusted method that converts a slice back to an array (panicking if the length is the wrong one). The postcondition of that conversion should have a quantifier similar to the convert-array-to-slice one, and for that I don't see how to choose triggers that are both complete and without matching loops. Consider the following program: the only expression that can be used to trigger the quantifiers is a2[0].

// requires forall i: Int :: { a[i] } ... ==> a[i] > 100
fn foo(a: [i32; 16]) {
    let s: &[i32] = &a;
    let a2: [i32; 16] = slice_to_array16(s);
    assert!(a2[0] > 100);
}

Like said above, it's fine for me to require the user to add assert!(s[0] > 100); in this example to trigger the quantifier instantiations of slice_to_array16. @viperproject/prusti-dev Are you of a different opinion?

[Pointerbender]

Nice example! Please allow me to try and dissect it a bit :)

The difference should be observable in a program that calls a trusted method that converts a slice back to an array (panicking if the length is the wrong one). The post-condition of that conversion should have a quantifier similar to the convert-array-to-slice one,

#[trusted]
#[ensures(forall(|i: usize| (0 <= i && i < 16) ==> (old(s[i]) == result[i] )))]
fn slice_to_array16(s: &[i32]) -> [i32; 16] {
     <[i32; 16]>::try_from(s).unwrap()
}
// requires forall i: Int :: { a[i] } ... ==> a[i] > 100
fn foo(a: [i32; 16]) {
    let s: &[i32] = &a;
    let a2: [i32; 16] = slice_to_array16(s);
    assert!(a2[0] > 100);
}

Here, the user-defined quantifier in the post-condition of slice_to_array16 has no explicit triggers defined, and Viper will try to infer them. (I recently came across some code that would suggest that these can be defined explicitly, but this is undocumented and I was not able to get it to work yet). In any case, such a trusted method would not inherit the triggers from ProcedureEncoder::encode_assign_slice() (called when unsizing an array into a slice), so I don't think this example would require a dummy statement due to the suggested changes in ProcedureEncoder::encode_assign_slice().

The postcondition of that conversion should have a quantifier similar to the convert-array-to-slice one, and for that I don't see how to choose triggers that are both complete and without matching loops.

Apologies for mixing multiple quantifiers/triggers in this thread, I think I may have caused some confusion by doing that :) Let me briefly recap both cases under discussion:

1. The first is located in ProcedureEncoder::encode_assign_slice(), which is called when a reference to an array is coerced into a reference to an (unsized) slice. Currently (on the master) branch, this still emits N statements, and so far we agreed that we can replace this by a quantifier for which the triggers will be { pure_lookup_array(array, i) } { pure_lookup_slice(slice, i) } without introducing a matching loop. In my previous post I suggested the idea to remove the { pure_lookup_array(array, i)} trigger and keep only the { pure_lookup_slice(slice, i) } trigger for better performance (together with a counter-example where this wouldn't work without additional dummy statements). I don't think this will affect any (trusted) methods with user specifications that convert a slice into an array, as long as ProcedureEncoder::encode_assign_slice() is not involved. I'd love to see more counter examples, though! So far I could only come up with one.
2. The other quantifier is located in ProcedureEncoder::encode_sequence_index_call, which is called when the Index::index() trait method is invoked. Currently it has the trigger { pure_lookup_array(array, j), pure_lookup_slice(slice, i) } using two variables in order to avoid a matching loop. In this post I'm suggesting to replace it with a different quantifier with a single variable and one trigger with just { pure_lookup_slice(slice, i) }, with the claim that it's at least as (in)complete as the { pure_lookup_array(array, j), pure_lookup_slice(slice, i) } trigger and that it will not result in a matching loop because it doesn't introduce any new terms that would re-instantiate the same quantifier, but it will cover more cases (so far I couldn't come up with any downside to this one).

[fpoli]

Thanks for the clarification! Sorry, I didn't notice that your penultimate comment was about quantifier 1 instead of 2.

Regarding the (planned) quantifier in ProcedureEncoder::encode_assign_slice, just changing the triggers from { pure_lookup_array(array, i) } { pure_lookup_slice(slice, i) } to { pure_lookup_slice(slice, i) } would be less complete in some cases, like the following program if { arrayLookup(array, i) } is removed from the line at L1. There would be less instantiations, yes, but I don't expect to gain a noticeable performance improvement. (I explain below why I think that eventual matching loops shouldn't be charged against this quantifier.)

Program

function arrayLen(self: Ref): Int
function sliceLen(self: Ref): Int
function arrayLookup(self: Ref, i: Int): Int requires 0 <= i && i < arrayLen(self)
function sliceLookup(self: Ref, i: Int): Int requires 0 <= i && i < sliceLen(self)

method test()
{
    // [rust] let array = [1, 2, 3];
    var array: Ref
    assume arrayLen(array) == 3;
    assume arrayLookup(array, 0) == 1;
    assume arrayLookup(array, 1) == 2;
    assume arrayLookup(array, 2) == 3;

    // Make the compiler coerce an array reference to slice
    // [rust] let (slice1, slice2) = array.split_at(2)
    var tmpSlice: Ref
    assume sliceLen(tmpSlice) == arrayLen(array)
    assume // Quantifier: coerce array reference to slice
        forall i: Int :: { sliceLookup(tmpSlice, i) } { arrayLookup(array, i) } // L1
            0 <= i && i < arrayLen(array) ==>
                arrayLookup(array, i) == sliceLookup(tmpSlice, i)
    var slice1: Ref
    var slice2: Ref
    slice1, slice2 := split_at(tmpSlice, 2)

    // User-written postcondition
    assert exists i: Int :: 0 <= i && i < sliceLen(slice1) && sliceLookup(slice1, i) == 1
}

// Trusted method
method split_at(slice: Ref, mid: Int) returns (slice1: Ref, slice2: Ref)
    requires sliceLen(slice) >= 0
    requires 0 <= mid && mid <= sliceLen(slice)
    ensures sliceLen(slice1) == mid
    ensures sliceLen(slice2) == sliceLen(slice) - mid
    ensures forall i: Int :: { sliceLookup(slice, i) } { sliceLookup(slice, i) }
            0 <= i && i < mid ==>
                sliceLookup(slice, i) == sliceLookup(slice1, i)
    ensures forall i: Int, j: Int :: { sliceLookup(slice, i), sliceLookup(slice, j) }
            i == mid + j && 0 <= j && j < sliceLen(slice2) ==>
                sliceLookup(slice, i) == sliceLookup(slice2, j)

Regarding the quantifier in ProcedureEncoder::encode_sequence_index_call (Q1), changing the triggers from { pure_lookup_array(array, j), pure_lookup_slice(slice, i) } to { pure_lookup_slice(slice, i) } would not be less complete, but it would cause matching loops as soon as the program contains another quantifier (Q2) with triggers on { pure_lookup_slice(slice, i) } { pure_lookup_array(array, i) } and has both pure_lookup_slice(slice, i) and pure_lookup_array(array, i) in its body.

The instantiations would be:

1. The user writes pure_lookup_slice(slice, 0).
2. pure_lookup_slice(slice, 0) triggers Q1, which generates pure_lookup_array(array, 0 + start.val_int).
3. pure_lookup_array(array, 0 + start.val_int) triggers Q2, which generates pure_lookup_slice(slice, 0 + start.val_int).
4. pure_lookup_slice(slice, 0 + start.val_int) triggers Q1, which generates pure_lookup_array(array, 0 + start.val_int + start.val_int).
5. ... Repeat until the configured maximum instantiation depth is reached.

Of course the cause of the matching loop could be attributed to Q2, not Q1, but I wouldn't agree with that. In my opinion, reasoning on pure_lookup_slice(slice, i) when a program mentions pure_lookup_array(array, i) is a common reasoning step that shouldn't be avoided because of fear of matching loops. It's Q2 that adds the + ... to i, so it's that quantifiers that should be restricted because of possible matching loops.

---

To sum up, when writing triggers I would always assume that the program contains other quantifiers that generate pure_lookup_slice(slice, i) from pure_lookup_array(array, i), vice-versa, and to (or from) any other pure function call that uses slice/array and exactly the same index i as argument. (It's not a formal description but I hope that the intuition is clear.) Then, every quantifier should have as many triggers as possible, provided that they do not create matching loops and that the triggers are not redundant.

[Pointerbender]

Thank you for the great explanation! :smile:

Regarding the (planned) quantifier in ProcedureEncoder::encode_assign_slice, just changing the triggers from { pure_lookup_array(array, i) } { pure_lookup_slice(slice, i) } to { pure_lookup_slice(slice, i) } would be less complete in some cases, like the following program if { arrayLookup(array, i) } is removed from the line at L1. There would be less instantiations, yes, but I don't expect to gain a noticeable performance improvement.

I did some bench-marking in the mean time with the changes in ProcedureEncoder::encode_assign_slice on the verification time of fn Path::reset() from the very first post in this Github issue, indeed the { pure_lookup_array(array, i) } trigger does not seem to be the root cause of the bottleneck. Let's keep this one :)

Regarding the quantifier in ProcedureEncoder::encode_sequence_index_call (Q1), changing the triggers from { pure_lookup_array(array, j), pure_lookup_slice(slice, i) } to { pure_lookup_slice(slice, i) } would not be less complete, but it would cause matching loops as soon as the program contains another quantifier (Q2) with triggers on { pure_lookup_slice(slice, i) } { pure_lookup_array(array, i) } and has both pure_lookup_slice(slice, i) and pure_lookup_array(array, i) in its body.

Ahhh, that makes sense now. I guess one special corner case is when start.val_int == 0, then we can emit pure_lookup_array(array, i) from the quantifier in ProcedureEncoder::encode_sequence_index_call instead of pure_lookup_array(array, start.val_int + i). However, I don't think it would be a good user experience if users sometimes have to add dummy statements for any slice range that doesn't start at zero, it's probably better to keep that consistent for all start values, so I won't go there :)

There is still an explosion of quantifier instantiations going on in the Viper program for fn Path::reset(), you had mentioned before:

1. Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix.
2. The pure encoding (Viper function) would be much more efficient in this case. We should switch to it soon.

Point 1 addresses the performance of the encoding, but solving point 2 would give the biggest time saving when verifying the Viper program. I have some ideas an some additional observations about point 2.

When coercing a reference to an array to a reference to a slice in a pure function in Viper using the snapshot encoding, this generates code like:

function m_invariant__$TY$__Snap$struct$m_Path$$bool$(_1: Snap$struct$m_Path): Bool
  requires true
  requires true
  ensures true
  ensures [result == mirror_simple$m_invariant__$TY$__Snap$struct$m_Path$$bool$(_1), true]
{
  (len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(
    cons$Snap$Slice$usize$__$TY$__Seq$$int$$Snap$Slice$usize(
      Seq(
        read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1), 0),
        read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1), 1),
        read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1), 2),
        read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1), 3),
        ...

The pure function body of the invariant is about 83kb long because of this :stuck_out_tongue: The code that performs this encoding lives here (again related to coercing a sized reference to an unsized reference):

https://github.com/viperproject/prusti-dev/blob/81396a073874e5997a61bf0480dbc4a22592bffb/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs#L1086-L1122

For the snap encoding, this could be solved by an additional function and axiom in the snapshot domain for the array:

domain Snap$Array$64$usize {
  function cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(array: Snap$Array$64$usize): Snap$Slice$usize

  axiom Snap$Array$64$usize$unsize {
    (forall data: Seq[Int] ::
      {
        cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(cons$Snap$Array$64$usize$__$TY$__Seq$$int$$Snap$Array$64$usize(data))
      }
      cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(cons$Snap$Array$64$usize$__$TY$__Seq$$int$$Snap$Array$64$usize(data)) == cons$Snap$Slice$usize$__$TY$__Seq$$int$$Snap$Slice$usize(data)
    )
  }
}

Then in the invariant function this can be called like:

function m_invariant__$TY$__Snap$struct$m_Path$$bool$(_1: Snap$struct$m_Path): Bool
  requires true
  requires true
  ensures true
  ensures [result == mirror_simple$m_invariant__$TY$__Snap$struct$m_Path$$bool$(_1), true]
{
  (len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(
    cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1))) != 64 ==> false)
  && (!(len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(
    cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(Snap$struct$m_Path$0$field$f$entries__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1))) != 64) ==> (
      len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(
        cast$Snap$Array$64$usize$__$TY$__Snap$Slice$usize(Snap$struct$m_Path$0$field$f$max_counts__$TY$__Snap$struct$m_Path$Snap$Array$64$usize(_1))
      ) != 64 ==> false
    )
    ...

This reduces the function body to around 2300 bytes and it avoids unnecessarily instantiating any quantifiers that trigger on { read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$ } (in this case, the invariant is just interested in the length of the array, not in the array contents).

Another opportunity I noticed for reducing the number of instantiated quantifiers is in the snapshot encoding of an array:

function snap$__$TY$__Array$64$usize$Snap$Array$64$usize(self: Ref): Snap$Array$64$usize
  requires acc(Array$64$usize(self), read$())
  ensures [(forall i: Int ::
    { read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(result, i) }
    { lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, i) }
    0 <= i && i < 64
      ==> read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(result, i) == lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, i)),
  true]
{
  cons$Snap$Array$64$usize$__$TY$__Seq$$int$$Snap$Array$64$usize(
    Seq(
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 0),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 1),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 2),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 3),
      ....
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 60),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 61),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 62),
      lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, 63)
    )
  )
}

Calling snap$__$TY$__Array$64$usize$Snap$Array$64$usize will immediately instantiate the quantifier from its post-condition 64 times (even more times for bigger array lengths!), this in turns instantiates all other quantifiers in scope, also as many times, which trigger on { read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(result, i) } or { lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, i) } (like the one from ProcedureEncoder::encode_assign_slice).

Now this one I find a bit tricky! The only way I currently see to address this one is to add a new field to the predicate Array$64$usize(self: Ref) of type Seq[Ref] (I chose Ref so that we can encode any type in the contents of the sequence). That way we could perform the snapshot encoding of an array, like: (not entirely accurate, because this would also require changes to the snapshot encoding, but to sketch the idea)

function snap$__$TY$__Array$64$usize$Snap$Array$64$usize(self: Ref): Snap$Array$64$usize
  requires acc(Array$64$usize(self), read$())
  ensures [(forall i: Int ::
    { read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(result, i) }
    { lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, i) }
    0 <= i && i < 64
      ==> read$Snap$Array$64$usize$__$TY$__Snap$Array$64$usize$$int$$$int$(result, i) == lookup_pure__$TY$__Array$64$usize$$int$$$int$(self, i)),
  true]
{
  (unfolding acc(Array$64$usize(self), read$()) in (
       (acc(seq$usize(self.val_seq), read$()) in
           cons$Snap$Array$64$usize$__$TY$__Seq$$int$$Snap$Array$64$usize(self.val_seq)
  ))
}

Which would avoid immediate unnecessary triggering almost every quantifier in the program when this function is called :)

In his thesis Johannes' mentions that we can't name fields for arrays, because these don't have fields (in 3.3.1 on page 24). Would it be possible to just "pretend" it has a single field in which it stores the sequence for easy access without triggering quantifiers? This approach would also be a deviating from another earlier design decision, namely that for Rust it's not necessary to model array permissions on the individual elements, it is sufficient to only look at the permissions for the entire array (explained in the thesis on pages 23-24). However, from the perspective of performance, there may be a reason to do this after all, provided that the additional quantifiers needed to model the permissions to the individual Ref in the Seq[Ref] won't undo the performance gained by not triggering other quantifiers.

In the bench-marking that I did, I can see a potential of at least a 9x speedup of the verification of fn Path::reset() if we can somehow stop the cascade of unnecessarily instantiated quantifiers (this speed-up does not include yet the idea to model the array contents as a field), so there is a lot of potential for improvement :)

Do you see any pitfalls with this approach to reduce the number of instantiated quantifiers? If it has the potential to work out, is this something I could work on, or is someone else already working on something similar? :) Thanks!