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
• function
• invariant
• layout
• map
• map_lib
• math
• modes
• multiset
• pcm
• pcm_lib
• pervasive
• prelude
• ptr
• raw_ptr
• relations
  Provides specifications for spec closures as relations.
• seq
• seq_lib
• set
• set_lib
• slice
• std_specs
• storage_protocol
• string
• thread
• 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