Macro exec_spec_verified 

exec_spec_verified!() { /* proc-macro */ }

Automatically compiles spec items to exec items, with proofs of functional correctness.

This macro takes a list of spec items, and generates a corresponding list of exec items:

• For every struct/enum A, we generate ExecA, which implements DeepView<V = A>
• For every spec function spec fn f(T) -> U, we generate

  fn exec_f(a: exec(T)) -> (r: exec(U))
  ensures r.deep_view() == f(a.deep_view()) { ... }

  where exec(T) maps a subset of supported spec types to exec types, including Seq (translated to Vec) and Option.

Below is a non-exhaustive list of supported spec expressions. Items marked with a * utilize unverified translations from spec to exec code internally.

• Basic arithmetic operations
• Logical operators (&&, ||, &&&, |||, not, ==>)
• If, match and “matches”
• Field expressions
• Bounded quantifiers of the form forall |i: <type>| <lower> <op> i <op> <upper> ==> <expr> and exists |i: <type>| <lower> <op> i <op> <upper> && <expr>, where:
  • <op> is either <= or <
  • <type> is a Rust primitive integer (i<N>, isize, u<N>, usize)
• SpecString (an alias to Seq<char> to syntactically indicate that we want String/&str), equality*, indexing, len, string literals
• Option<T> with these functions:
  • equality, unwrap
• Seq<T> (compiled to Vec<T> or &[T] depending on the context), seq! literals, and these Seq functions:
  • equality*, len, indexing, subrange*, add*, push*, update*, empty, to_multiset*, drop_first*, drop_last*, take*, skip*, first, last, is_suffix_of*, is_prefix_of*, contains*, index_of*, index_of_first*, index_of_last*
• Map<K, V> (compiled to HashMap<K, V>), and these Map functions:
  • equality*, len*, indexing*, empty, dom*, insert*, remove*, get*
  • Note: indexing is only supported on Map<K, V> where K is a primitive type (e.g. usize); for other types K, use get instead.
• Set<T> (compiled to HashSet<T>), and these Set functions:
  • equality*, len*, empty, contains*, insert*, remove*, union*, intersect*, difference*
• Multiset<T> (compiled to ExecMultiset<T>, a type implemented in vstd::contrib::exec_spec whose internal representation is a HashMap), and these Multiset functions:
  • equality*, len*, count*, empty*, singleton*, add*, sub*
• User-defined structs and enums. These types should be defined within the macro using spec-compatible types for the fields (e.g. Seq). Such types are then compiled to their Exec- versions, which use the exec versions of each field’s type (e.g. Vec/slice).
• Primitive integer/boolean types (i<N>, isize, u<N>, usize, char, etc.). Note that int and nat cannot be used in exec_spec_verified!.