verus nondeterminism

[tjhance]

Verus appears to exhibit nondeterminism, i.e., consecutive invocations while changing nothing can lead to different results. I can consistently get varied results if I just run the command over and over again.

Repro: verus-systems-code Checkout bea84cf8794c7c004cc352be3ba5703c62ec9d06 cd mimalloc rust-verify.sh lib.rs --verify-module segment

Verus: Commit a73ea27c5a7842309b6f42e8c0f6b49e89f8499c build in release mode (EDIT: debug mode exhibits the same behavior)

Specifically, I either get this error:

note: verifying module segment

error: precondition not satisfied
   --> segment.rs:121:21
    |
121 | /                     segment_slice_split(
122 | |                         slice.clone(),
123 | |                         found_slice_count,
124 | |                         slice_count,
125 | |                         tld_ptr.clone(),
126 | |                         Tracked(&mut *local));
    | |_____________________________________________^
    |
   ::: page_organization.rs:86:18
    |
86  |           requires self.wf(),
    |                    --------- failed precondition

error: aborting due to previous error

or

note: verifying module segment

error: precondition not satisfied
   --> segment.rs:121:21
    |
121 | /                     segment_slice_split(
122 | |                         slice.clone(),
123 | |                         found_slice_count,
124 | |                         slice_count,
125 | |                         tld_ptr.clone(),
126 | |                         Tracked(&mut *local));
    | |_____________________________________________^
...
325 |           target_slice_count > 0,
    |           ---------------------- failed precondition

error: aborting due to previous error

In the first of the two outputs, the error is actually nonsense: the line it points to is not a precondition of the function call with the precondition failure. (Similar issue to #114)

These log files might be useful to understand what's going on: log1.zip log2.zip

---

@utaal's note: for better test coverage of this, we should add a smoke test that Verus produces identical SMTLIB inputs on repeated runs on the exact same Rust/Verus input, using the examples

• [ ] add test that Verus produces SMTLIB deterministically

[tjhance]

okay I think the reason is simple: if you look at the AIR log files, it's clear things are coming out in different orders. So I think the problem has to do with hash table iteration order somewhere. We should probably try to identify the hash table iterations relevant to AIR output and give them a consistent order.

[tjhance]

I fixed an easy one - printing tuple declarations in a fixed order (77e518bbd21e0466e226d6ccd510570751ab6be1). However there are still a few things that are getting output in random order. 'havoc' statements and type-invariant axioms both seem to appear in random order.

[tjhance]

As discussed in the meeting today, a clear action item is to replace HashMap/HashSet with IndexMap/IndexSet. This will probably make Verus deterministic for a given binary & verus source file.

• [x] replace HashMap/HashSet with IndexMap/IndexSet.

[achreto]

I've seen that there are assertion failures with patterns like this:

if P() {
   assert(P()); 
}

White space changes and/or re-running it seems to make it vanish (i.e., assertion passes). So it's not stable.

An example is here

[utaal]

• [x] replace HashMap/HashSet with IndexMap/IndexSet.

This was done in https://github.com/verus-lang/verus/commit/b05f6d30c10c8c798defede02da2f3a4ec563a34

[utaal]

[Verus all-hands]

We may want to do the check for determinism for the examples, which are bigger and more likely to show the nondeterminism.