Crate vstd

Source
Expand description

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
laws_cmp
laws_eq
layout
logatom
map
map_lib
math
modes
multiset
multiset_lib
pcm
pcm_lib
pervasive
prelude
proph
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_optDeprecated
pcell_points
seq
Creates a Seq containing the given elements.
set
vpanic
Replace panic macro with vpanic when needed. panic!{} may call panic_fmt with private rt::Argument, which could not be supported in verus.

Functions§

group_vstd_default