Module prelude

Source

Re-exports§

pub use super::map::map;
pub use super::map::Map;
pub use super::seq::seq;
pub use super::seq::Seq;
pub use super::set::set;
pub use super::set::Set;
pub use super::pervasive::affirm;
pub use super::pervasive::arbitrary;
pub use super::pervasive::cloned;
pub use super::pervasive::proof_from_false;
pub use super::pervasive::spec_affirm;
pub use super::pervasive::unreached;
pub use super::array::ArrayAdditionalExecFns;
pub use super::array::ArrayAdditionalSpecFns;
pub use super::pervasive::FnWithRequiresEnsures;
pub use super::slice::SliceAdditionalSpecFns;
pub use super::std_specs::option::OptionAdditionalFns;
pub use super::std_specs::result::ResultAdditionalSpecFns;
pub use super::std_specs::vec::VecAdditionalSpecFns;
pub use super::pervasive::VecAdditionalExecFns;
pub use super::string::StrSliceExecFns;
pub use super::string::StringExecFns;
pub use super::string::StringExecFnsIsAscii;
pub use super::tokens::CountToken;
pub use super::tokens::ElementToken;
pub use super::tokens::KeyValueToken;
pub use super::tokens::MonotonicCountToken;
pub use super::tokens::SimpleToken;
pub use super::tokens::ValueToken;
pub use super::tokens::InstanceId;
pub use super::view::*;

Macros§

atomic_with_ghost_helper
calc_proc_macro
decreases_to
decreases_to!(b => a) means that height(a) < height(b), so that b can decrease to a in decreases clauses. decreases_to!(b1, …, bn => a1, …, am) can compare lexicographically ordered values, which can be useful when making assertions about decreases clauses. Notes:
decreases_to_internal
fndecl
proof
Add a verus proof block.
proof_decl
proof_decl add extra stmts that are used only for verification. For example, declare a ghost/tracked variable. To avoid confusion, let stmts without ghost/tracked is not supported. Non-local stmts inside proof_decl! are treated similar to those in proof!
proof_with
proof_with add ghost input/output to the next function call. In stable rust, we cannot add attribute-based macro to expr/statement. Using proof_with! to tell #[verus_spec] to add ghost input/output. Using proof_with outside of #[verus_spec] does not have any side effects.
struct_with_invariants
verus
verus_erase_ghost
verus_exec_expr
verus_exec_expr_erase_ghost
verus_exec_expr_keep_ghost
verus_exec_inv_macro_exprs
verus_exec_macro_exprs
verus_ghost_inv_macro_exprs
verus_impl
Like verus!, but for use inside a (non-trait) impl
verus_keep_ghost
verus_proof_expr
verus_proof_macro_explicit_exprs
verus_proof_macro_explicit_exprs!(f!(tts)) applies verus syntax to transform tts into tts', then returns f!(tts'), only applying the transform to any of the exprs within it that are explicitly prefixed with @@, leaving the rest as-is. Contrast this to [verus_proof_macro_exprs] which is likely what you want to try first to see if it satisfies your needs.
verus_proof_macro_exprs
verus_proof_macro_exprs!(f!(exprs)) applies verus syntax to transform exprs into exprs’, then returns f!(exprs’), where exprs is a sequence of expressions separated by “,”, “;”, and/or “=>”.
verus_trait_impl
Like verus!, but for use inside a trait impl
with_triggers

Structs§

DummyCapture
FnProof
FnProof is the type of proof closures; the syntax proof_fn is used to wrap FnProof
FnSpec
Ghost
NoCopy
ProofFnConfirm
SpecChain
Tracked
int
nat

Constants§

PROOF_FN
PROOF_FN_COPY
PROOF_FN_MUT
PROOF_FN_ONCE
PROOF_FN_SEND
PROOF_FN_SYNC

Traits§

Boolean
Integer
ProofFn
ProofFnMut
ProofFnOnce
ProofFnReqEns
ProofFnReqEnsDef
SpecAdd
SpecBitAnd
SpecBitOr
SpecBitXor
SpecEuclideanDiv
SpecEuclideanMod
SpecMul
SpecNeg
SpecOrd
SpecShl
SpecShr
SpecSub
Structural
derive(Structural) means that exec-mode == and ghost == always yield the same result. derive(Structural) is only allowed when all the fields of a type are also Structural. derive(StructuralEq) means derive(Structural) and also implement PartialEqSpec, setting eq_spec to == and obeys_eq_spec to true.

Functions§

add
admit
arch_word_bits
array_index
assert_
assert_bit_vector
assert_bitvector_by
assert_by
assert_by_compute
assert_by_compute_only
assert_forall_by
assert_nonlinear_by
assume_
call_ensures
call_requires
choose
choose_tuple
closure_to_fn_spec
constrain_type
decreases
decreases_by
decreases_when
default_ensures
Mark an ensures clause in a trait as applying just to the default implementation, not the trait declaration in general
dummy_capture_consume
dummy_capture_new
ensures
equal
erased_ghost_value
exists
ext_equal
ext_equal_deep
extra_dependency
f32_to_bits
f64_to_bits
forall
get_union_field
get_variant_field
ghost_exec
global_size_of
has_resolved
imply
infer_spec_for_loop_iter
inline_air_stmt
invariant
invariant_except_break
is_smaller_than
is_smaller_than_lexicographic
is_smaller_than_recursive_function_field
is_variant
mul
mut_ref_current
mut_ref_future
no_method_body
no_unwind
no_unwind_when
old
opens_invariants
opens_invariants_any
opens_invariants_except
opens_invariants_none
opens_invariants_set
recommends
recommends_by
requires
resolve
returns
reveal_hide_
reveal_hide_internal_path_
reveal_strlit
signed_max
signed_min
spec_cast_integer
spec_chained_cmp
spec_chained_eq
spec_chained_ge
spec_chained_gt
spec_chained_le
spec_chained_lt
spec_chained_value
spec_eq
spec_literal_int
spec_literal_integer
spec_literal_nat
strslice_get_char
strslice_is_ascii
strslice_len
sub
tracked_exec
tracked_exec_borrow
unsigned_max
use_type_invariant
with_triggers

Attribute Macros§

is_variant
Add is_<VARIANT> and get_<VARIANT> functions to an enum
is_variant_no_deprecation_warning
Add is_<VARIANT> and get_<VARIANT> functions to an enum
verus_enum_synthesize
verus_spec
verus_verify

Derive Macros§

Structural
StructuralEq