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
andmap2
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
ands2
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 Deprecated - 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.