Expand description
The “extra standard library” for Verus. Contains various utilities and general datatypes for proofs useful in Asterinas verification, as well as extending Verus standard library(vstd) with additional functionality.
Modules§
- arithmetic
- array_
ptr - auxiliary
- bit_
mapping - cast_
ptr - extern_
const - external
- Specifications for functions from Rust standard library but not specified in
vstd. - function_
properties - Properties of pure mathematical spec functions (
spec_fn). - ghost_
tree - map_
extra - Extra properties of
vstd::map::Map. - ownership
- prelude
- ptr_
extra - raw_
ptr_ extra - resource
- Resource algebras based on PCM and storage-protocol inspired by Iris and Leaf.
- seq_
extra - Extra properties of
vstd::seq::Seq. - set_
extra - Extra properties of
vstd::set::Set. - state_
machine - TLA-style state machines.
- std_
extra - temporal_
logic - TLA temporal logic definitions and proof rules.
- undroppable
Macros§
- always_
and_ equality_ n - always_
and_ equality_ n_ internal - always_
lift_ state_ and_ equality_ n - always_
lift_ state_ and_ equality_ n_ internal - always_
lift_ state_ weaken_ n - always_
lift_ state_ weaken_ n_ internal - bm
- bms
- bms_as
- borrow_
field - combine_
spec_ entails_ always_ n - combine_
spec_ entails_ always_ n_ internal - decl_
bms_ const - entails_
always_ and_ n - entails_
always_ and_ n_ internal - entails_
always_ lift_ state_ and_ n - entails_
always_ lift_ state_ and_ n_ internal - entails_
and_ n - entails_
and_ n_ internal - extern_
const - ! This module provides a macro to define a constant that can be used when ! crossing crates.
- implies_
new_ invariant_ n - implies_
new_ invariant_ n_ internal - invariant_
n - invariant_
n_ internal - leads_
to_ always_ combine_ n - leads_
to_ always_ combine_ n_ internal - leads_
to_ always_ combine_ n_ with_ equality - leads_
to_ always_ combine_ n_ with_ equality_ internal - leads_
to_ trans_ n - leads_
to_ trans_ n_ internal - or_
leads_ to_ combine_ and_ equality2 - or_
leads_ to_ combine_ n - or_
leads_ to_ combine_ n_ internal - stable_
and_ always_ n - stable_
and_ always_ n_ internal - stable_
and_ n - stable_
and_ n_ internal - state_
pred_ and - temp_
pred_ and - temp_
pred_ and_ internal - update_
field - wf1_
by_ borrowing_ inv_ n