Module prelude 

This module re-exports the most commonly used items from Vest.

use vest_lib::prelude::*; would include the Verus prelude, Vest’s executable, specification and proof traits, as well as its format combinators.

In addition, some basic length and bytes-view broadcast lemmas are enabled automatically when vest_lib is imported.

Re-exports

pub use crate::core::exec::ByteLen;

pub use crate::core::exec::InputBuf;

pub use crate::core::exec::InputSlice;

pub use crate::core::exec::OutputBuf;

pub use crate::core::exec::OutputSlice;

pub use crate::core::exec::PResult;

pub use crate::core::exec::ParseError;

pub use crate::core::exec::ParseErrorKind;

pub use crate::core::exec::Parser;

pub use crate::core::exec::PreSerializeError;

pub use crate::core::exec::Prepare;

pub use crate::core::exec::Serializer;

pub use crate::core::exec::SerializerExt;

pub use crate::combinators::star::spec::lemma_star_static_byte_len;

pub use crate::combinators::*;

pub use crate::core::proof::*;

pub use crate::core::spec::*;

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

imap

Create a map using syntax like imap![key1 => val1, key2 => val, ...].

iset

map

Create a map using syntax like map![key1 => val1, key2 => val, ...].

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.

seq

Creates a Seq containing the given elements.

set

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

IMap

IMap<K, V> is an abstract map type for specifications.

ISet

ISet<A> is a set type for specifications.

Map

Map<K, V> is an abstract map type for specifications. To use a “map” in compiled code, use an exec type like HashMap that has a Map<K, V> as its specification type.

NoCopy

ProofFnConfirm

Seq

Seq<A> is a sequence type for specifications. To use a “sequence” in compiled code, use an exec type like vec::Vec that has Seq<A> as its specification type.

Set

Set<A> is a finite set type for specifications.

SpecChain

Tracked

int

nat

real

Constants

PROOF_FN

PROOF_FN_COPY

PROOF_FN_MUT

PROOF_FN_ONCE

PROOF_FN_SEND

PROOF_FN_SYNC

Traits

ArrayAdditionalExecFns

ArrayAdditionalSpecFns

Boolean

Chainable

CountToken

Interface for VerusSync tokens created for a field marked with the count strategy.

Decimal

DeepView

ElementToken

Interface for VerusSync tokens created for a field marked with the set, persistent_set or multiset strategies.

FnWithRequiresEnsures

IeeeFloat

IeeeFloatCast

Integer

KeyValueToken

Interface for VerusSync tokens created for a field marked with the map or persistent_map strategies.

MaybeUninitAdditionalSpecFns

MonotonicCountToken

Interface for VerusSync tokens created for a field marked with the persistent_count strategy.

OptionAdditionalFns

ProofFn

ProofFnMut

ProofFnOnce

ProofFnReqEns

ProofFnReqEnsDef

ResultAdditionalSpecFns

SimpleToken

Interface for VerusSync tokens created for a field marked with the bool or persistent_bool strategy.

SliceAdditionalSpecFns

SpecAdd

SpecBitAnd

SpecBitOr

SpecBitXor

SpecEq

SpecEuclideanMod

SpecEuclideanOrRealDiv

SpecMul

SpecNeg

SpecOrd

SpecShl

SpecShr

SpecSub

StrSliceExecFns

StringExecFns

StringExecFnsIsAscii

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.

ValueToken

Interface for VerusSync tokens created for a field marked with the variable, option or persistent_option strategies.

VecAdditionalExecFns

VecAdditionalSpecFns

View

Types used in executable code can implement View to provide a mathematical abstraction of the type. For example, Vec implements a view method that returns a Seq. For base types like bool and u8, the view V of the type is the type itself. Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.

Functions

add

admit

affirm

after_borrow

arbitrary

In spec, all types are inhabited

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_

atomic_call_loop

atomic_spec

basic_lemmas

call_ensures

call_requires

choose

choose_tuple

cloned

Predicate indicating b is “a clone” of a; i.e., b could be the result of calling a.clone() or is equal to a.

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

Needed for the THIR-based erasure (rustc_mir_build_additional_files)

exists

ext_equal

ext_equal_deep

extra_dependency

f32_to_bits

f64_to_bits

final_

forall

get_future_output_type

get_union_field

get_variant_field

ghost_exec

global_size_of

has_resolved

Directives and spec functions related to &mut references

has_resolved_unsized

imply

inline_air_stmt

inv_mask_any

inv_mask_list

inv_mask_list_compl

inv_mask_none

inv_mask_set

invariant

invariant_except_break

is_smaller_than

is_smaller_than_lexicographic

is_smaller_than_recursive_function_field

is_variant

lemma_byte_array_view

lemma_byte_slice_view

lemma_identity_vec_view

mul

mut_ref_current

mut_ref_future

mut_ref_tracked

mutable_reference_tie

no_method_body

no_unwind

no_unwind_when

old

opens_invariant_mask

parser_lemmas

proof_from_false

recommends

recommends_by

requires

returns

reveal_byteslit

reveal_hide_

reveal_hide_internal_path_

reveal_strlit

shadow_ghost_value

shr_ref_struct_wrap

signed_max

signed_min

spec_affirm

A tool to check one’s reasoning while writing complex spec functions. Not intended to be used as a mechanism for instantiating quantifiers, spec_affirm should be removed from spec functions once they are complete.

spec_cast_float

spec_cast_integer

spec_cast_real

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_decimal

spec_literal_int

spec_literal_integer

spec_literal_nat

strslice_get_char

strslice_len

strslice_new_strlit

sub

tracked_exec

tracked_exec_borrow

two_phase_mutable_reference_tie

unreached

unsigned_max

use_type_invariant

verus_erasure_get_first

with_triggers

Type Aliases

InstanceId

Unique identifier for every VerusSync instance. Every “Token” and “Instance” object has an InstanceId. These ID values must agree to perform any token operation.

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