Crate vstd

The “standard library” for Verus. Contains various utilities and datatypes for proofs, as well as runtime functionality with specifications. For an introduction to Verus, see the tutorial.

Modules

• arithmetic
• array
• atomic
• atomic_ghost
  Provides sequentially-consistent atomic memory locations with associated ghost state. See the atomic_with_ghost! documentation for more information.
• bits
  Properties of bitwise operators.
• bytes
  Conversions to/from bytes
• calc_macro
  The calc macro provides support for reasoning about a structured proof calculation.
• cell
• compute
• function
• hash_map
• hash_set
• invariant
• layout
• map
• map_lib
• math
• modes
• multiset
• multiset_lib
• pcm
• pcm_lib
• pervasive
• prelude
• proph
• ptrDeprecated
• raw_ptr
  Tools and reasoning principles for raw pointers. The tools here are meant to address “real Rust pointers, including all their subtleties on the Rust Abstract Machine, to the largest extent that is reasonable.”
• relations
  Provides specifications for spec closures as relations.
• rwlock
• seq
• seq_lib
• set
• set_lib
• shared
• simple_pptr
• slice
• std_specs
• storage_protocol
• string
• thread
• tokens
• view

Macros

• assert_by_contradiction
  Allows you to prove a boolean predicate by assuming its negation and proving a contradiction.
• assert_maps_equal
  Prove two maps map1 and map2 are equal by proving that their values are equal at each key.
• assert_multisets_equal
• assert_multisets_equal_internal
• assert_seqs_equal
  Prove two sequences s1 and s2 are equal by proving that their elements are equal at each index.
• assert_sets_equal
  Prove two sets equal by extensionality. Usage is:
• atomic_with_ghost
  Performs a given atomic operation on a given atomic while providing access to its ghost state.
• calc
  The calc! macro supports structured proofs through calculations.
• map
  Create a map using syntax like map![key1 => val1, key2 => val, ...].
• open_atomic_invariant
  Macro used to temporarily “open” an AtomicInvariant object, obtaining the stored value within.
• open_atomic_invariant_in_proof
• open_atomic_invariant_in_proof_internal
• open_atomic_invariant_internal
• open_local_invariant
  Macro used to temporarily “open” a LocalInvariant object, obtaining the stored value within.
• open_local_invariant_in_proof
• open_local_invariant_in_proof_internal
• open_local_invariant_internal
• pcell_opt
• seq
  Creates a Seq containing the given elements.
• set

Functions

• group_vstd_default