Verifying Verus built-in types against a model

Currently, Verus has completely axiomatic types for Seq, Set, and Map: the types are #[verifier::external_body], the functions are opaque, and then there are axioms that characterize the functions. This runs the risk of introducing unsound axioms, since nothing checks that they make sense collectively.

Here we implement each of these types with an underlying model (with primitives like inductive data types and functions, or enums, structs, and spec_fns in Verus parlance). This does not introduce any additional axioms or trust, we just rely on the existing data types. It also means that we can try adding new lemmas or strengthening the existing ones by removing preconditions without fear; if we can prove the new lemma, it's definitely safe to keep. (At least for soundness - we still have to think about triggers and automation performance to avoid making users' proofs slower.)

There are some limitations around #[verifier(broadcast_forall)] that make this not work as a drop-in replacement: the lemmas can be marked broadcast_forall, but users have to call reveal to use the lemmas (rather than them being always available), and they also can't be proven alongside the axioms because then the proofs just use the axioms. These limitations should all be resolved in Verus relatively soon.

Status

Seq is fully implemented and verified.

Set is implemented but not quite verified (especially the length axioms).

Map needs to be implemented and verified. The model of Map<K, V> should be something like {has: spec_fn(K) -> Option<V>}, with m.dom() == Set::new(|k| (m.has)(k).is_Some()) and m[k] == (m.has)(k).Some_v().

Verifying

verus --crate-type=lib src/lib.rs