List of all items

Structs

• arithmetic::overflow::CheckedU128
• arithmetic::overflow::CheckedU16
• arithmetic::overflow::CheckedU32
• arithmetic::overflow::CheckedU64
• arithmetic::overflow::CheckedU8
• arithmetic::overflow::CheckedUsize
• atomic::AtomicUpdate
• atomic::Commit
• atomic::PAtomicBool
• atomic::PAtomicI16
• atomic::PAtomicI32
• atomic::PAtomicI64
• atomic::PAtomicI8
• atomic::PAtomicIsize
• atomic::PAtomicPtr
• atomic::PAtomicU16
• atomic::PAtomicU32
• atomic::PAtomicU64
• atomic::PAtomicU8
• atomic::PAtomicUsize
• atomic::PermissionBool
• atomic::PermissionDataBool
• atomic::PermissionDataI16
• atomic::PermissionDataI32
• atomic::PermissionDataI64
• atomic::PermissionDataI8
• atomic::PermissionDataIsize
• atomic::PermissionDataPtr
• atomic::PermissionDataU16
• atomic::PermissionDataU32
• atomic::PermissionDataU64
• atomic::PermissionDataU8
• atomic::PermissionDataUsize
• atomic::PermissionI16
• atomic::PermissionI32
• atomic::PermissionI64
• atomic::PermissionI8
• atomic::PermissionIsize
• atomic::PermissionPtr
• atomic::PermissionU16
• atomic::PermissionU32
• atomic::PermissionU64
• atomic::PermissionU8
• atomic::PermissionUsize
• atomic_ghost::AtomicBool
• atomic_ghost::AtomicI16
• atomic_ghost::AtomicI32
• atomic_ghost::AtomicI64
• atomic_ghost::AtomicI8
• atomic_ghost::AtomicIsize
• atomic_ghost::AtomicPredBool
• atomic_ghost::AtomicPredI16
• atomic_ghost::AtomicPredI32
• atomic_ghost::AtomicPredI64
• atomic_ghost::AtomicPredI8
• atomic_ghost::AtomicPredIsize
• atomic_ghost::AtomicPredPtr
• atomic_ghost::AtomicPredU16
• atomic_ghost::AtomicPredU32
• atomic_ghost::AtomicPredU64
• atomic_ghost::AtomicPredU8
• atomic_ghost::AtomicPredUsize
• atomic_ghost::AtomicPtr
• atomic_ghost::AtomicU16
• atomic_ghost::AtomicU32
• atomic_ghost::AtomicU64
• atomic_ghost::AtomicU8
• atomic_ghost::AtomicUsize
• cell::CellId
• cell::InvCell
• cell::PCell
• cell::PointsTo
• cell::PointsToData
• cell::invcell::InvCell
• cell::pcell::PCell
• cell::pcell::PointsTo
• cell::pcell_maybe_uninit::PCell
• cell::pcell_maybe_uninit::PointsTo
• contrib::exec_spec::ExecMultiset
• endian::EndianNat
• function::ExFnProof
• hash_map::HashMapWithView
• hash_map::StringHashMap
• hash_set::HashSetWithView
• hash_set::StringHashSet
• imap::IMap
• invariant::AtomicInvariant
• invariant::LocalInvariant
• invariant::OpenInvariantCredit
• iset::ISet
• map::Map
• multiset::Multiset
• prelude::FnProof
• prelude::FnSpec
• prelude::Ghost
• prelude::NoCopy
• prelude::ProofFnConfirm
• prelude::SpecChain
• prelude::Tracked
• prelude::int
• prelude::nat
• prelude::real
• proph::Prophecy
• proph::ProphecyGhost
• proph::ProphecySeq
• raw_ptr::Dealloc
• raw_ptr::DeallocData
• raw_ptr::FakeMetadata
• raw_ptr::IsExposed
• raw_ptr::PointsTo
• raw_ptr::PointsToData
• raw_ptr::PointsToRaw
• raw_ptr::Provenance
• raw_ptr::SharedReference
• resource::Loc
• resource::algebra::Resource
• resource::auth::AuthRA
• resource::frac::FracGhost
• resource::frac_opt::Empty
• resource::frac_opt::Frac
• resource::ghost_var::GhostVar
• resource::ghost_var::GhostVarAuth
• resource::imap::GhostIMapAuth
• resource::imap::GhostIPointsTo
• resource::imap::GhostISubmap
• resource::imap::GhostPersistentIPointsTo
• resource::imap::GhostPersistentISubmap
• resource::iset::GhostISetAuth
• resource::iset::GhostISingleton
• resource::iset::GhostISubset
• resource::iset::GhostPersistentISingleton
• resource::iset::GhostPersistentISubset
• resource::map::GhostMapAuth
• resource::map::GhostPersistentPointsTo
• resource::map::GhostPersistentSubmap
• resource::map::GhostPointsTo
• resource::map::GhostSubmap
• resource::pcm::Resource
• resource::product::ProductRA
• resource::seq::GhostSeqAuth
• resource::seq::GhostSubseq
• resource::set::GhostPersistentSingleton
• resource::set::GhostPersistentSubset
• resource::set::GhostSetAuth
• resource::set::GhostSingleton
• resource::set::GhostSubset
• resource::storage_protocol::StorageResource
• rwlock::InvariantPredicate_auto_RwLock_exc
• rwlock::InvariantPredicate_auto_RwLock_rc
• rwlock::ReadHandle
• rwlock::RwLock
• rwlock::RwLockToks::Instance
• rwlock::RwLockToks::State
• rwlock::RwLockToks::flag_exc
• rwlock::RwLockToks::flag_rc
• rwlock::RwLockToks::pending_reader
• rwlock::RwLockToks::pending_writer
• rwlock::RwLockToks::reader
• rwlock::RwLockToks::writer
• rwlock::WriteHandle
• seq::Seq
• set::Set
• simple_pptr::PPtr
• simple_pptr::PointsTo
• string::ExChars
• string::ExString
• thread::IsThread
• thread::JoinHandle
• thread::ThreadId
• tokens::IMapToken
• tokens::ISetToken
• tokens::MapToken
• tokens::MultisetToken
• tokens::SetToken

Enums

• atomic::UpdateControlFlow
• endian::Endian
• raw_ptr::MemContents
• resource::agree::AgreementRA
• resource::exclusive::ExclusiveRA
• resource::frac::FractionRA
• resource::sum::SumRA
• rwlock::RwLockToks::Config
• rwlock::RwLockToks::Step

Traits

• array::ArrayAdditionalExecFns
• array::ArrayAdditionalSpecFns
• atomic::UpdatePredicate
• atomic::UpdateTry
• atomic_ghost::AtomicInvariantPredicate
• compute::RangeAll
• contrib::exec_spec::DeepViewClone
• contrib::exec_spec::ExecSpecEq
• contrib::exec_spec::ExecSpecIndex
• contrib::exec_spec::ExecSpecLen
• contrib::exec_spec::ExecSpecMapDom
• contrib::exec_spec::ExecSpecMapEmpty
• contrib::exec_spec::ExecSpecMapGet
• contrib::exec_spec::ExecSpecMapIndex
• contrib::exec_spec::ExecSpecMapInsert
• contrib::exec_spec::ExecSpecMapRemove
• contrib::exec_spec::ExecSpecMultisetAdd
• contrib::exec_spec::ExecSpecMultisetCount
• contrib::exec_spec::ExecSpecMultisetEmpty
• contrib::exec_spec::ExecSpecMultisetSingleton
• contrib::exec_spec::ExecSpecMultisetSub
• contrib::exec_spec::ExecSpecOptionUnwrap
• contrib::exec_spec::ExecSpecSeqAdd
• contrib::exec_spec::ExecSpecSeqContains
• contrib::exec_spec::ExecSpecSeqDropFirst
• contrib::exec_spec::ExecSpecSeqDropLast
• contrib::exec_spec::ExecSpecSeqEmpty
• contrib::exec_spec::ExecSpecSeqFirst
• contrib::exec_spec::ExecSpecSeqIndexOf
• contrib::exec_spec::ExecSpecSeqIndexOfFirst
• contrib::exec_spec::ExecSpecSeqIndexOfLast
• contrib::exec_spec::ExecSpecSeqIsPrefixOf
• contrib::exec_spec::ExecSpecSeqIsSuffixOf
• contrib::exec_spec::ExecSpecSeqLast
• contrib::exec_spec::ExecSpecSeqPush
• contrib::exec_spec::ExecSpecSeqSkip
• contrib::exec_spec::ExecSpecSeqSubrange
• contrib::exec_spec::ExecSpecSeqTake
• contrib::exec_spec::ExecSpecSeqToMultiset
• contrib::exec_spec::ExecSpecSeqUpdate
• contrib::exec_spec::ExecSpecSetContains
• contrib::exec_spec::ExecSpecSetDifference
• contrib::exec_spec::ExecSpecSetEmpty
• contrib::exec_spec::ExecSpecSetInsert
• contrib::exec_spec::ExecSpecSetIntersect
• contrib::exec_spec::ExecSpecSetRemove
• contrib::exec_spec::ExecSpecSetUnion
• contrib::exec_spec::ExecSpecType
• contrib::exec_spec::ToOwned
• contrib::exec_spec::ToRef
• endian::Base
• endian::BasePow2
• endian::CompatibleSmallerBaseFor
• float::ExIeeeFloatCast
• float::FloatBitsProperties
• function::ExProofFn
• function::ExProofFnMut
• function::ExProofFnOnce
• function::ExProofFnReqEns
• function::ExProofFnReqEnsAssoc
• function::ExProofFnSpecification
• future::ExFuture
• future::FutureAdditionalSpecFns
• invariant::InvariantPredicate
• logatom::MutLinearizer
• logatom::MutOperation
• logatom::ReadLinearizer
• logatom::ReadOperation
• pervasive::ForLoopGhostIterator
• pervasive::ForLoopGhostIteratorNew
• pervasive::VecAdditionalExecFns
• predicate::Predicate
• prelude::Boolean
• prelude::Chainable
• prelude::Decimal
• prelude::IeeeFloat
• prelude::IeeeFloatCast
• prelude::Integer
• prelude::ProofFn
• prelude::ProofFnMut
• prelude::ProofFnOnce
• prelude::ProofFnReqEns
• prelude::ProofFnReqEnsDef
• prelude::SpecAdd
• prelude::SpecBitAnd
• prelude::SpecBitOr
• prelude::SpecBitXor
• prelude::SpecEq
• prelude::SpecEuclideanMod
• prelude::SpecEuclideanOrRealDiv
• prelude::SpecMul
• prelude::SpecNeg
• prelude::SpecOrd
• prelude::SpecShl
• prelude::SpecShr
• prelude::SpecSub
• prelude::Structural
• resource::algebra::ResourceAlgebra
• resource::pcm::PCM
• resource::storage_protocol::Protocol
• rwlock::RwLockPredicate
• set_lib::FiniteFull
• set_lib::FiniteRange
• slice::ExSliceIndex
• slice::SliceAdditionalExecFns
• slice::SliceAdditionalSpecFns
• slice::SliceIndexSpec
• slice::SliceIndexSpecImpl
• string::StrSliceExecFns
• string::StringExecFns
• string::StringExecFnsIsAscii
• string::StringSliceAdditionalSpecFns
• tokens::CountToken
• tokens::ElementToken
• tokens::KeyValueToken
• tokens::MonotonicCountToken
• tokens::SimpleToken
• tokens::UniqueElementToken
• tokens::UniqueKeyValueToken
• tokens::UniqueSimpleToken
• tokens::UniqueValueToken
• tokens::ValueToken
• view::DeepView
• view::View

Macros

• assert_by_contradiction
• assert_imaps_equal
• assert_isets_equal
• assert_maps_equal
• assert_multisets_equal
• assert_multisets_equal_internal
• assert_seqs_equal
• assert_sets_equal
• atomic::open_atomic_update
• atomic::open_atomic_update_in_proof
• atomic::peek_atomic_update
• atomic::peek_atomic_update_in_proof
• atomic::try_open_atomic_update
• atomic::try_open_atomic_update_in_proof
• atomic_ghost::atomic_with_ghost
• atomic_with_ghost
• calc
• calc_macro::calc
• cell::pcell_points
• contrib::exec_spec::exec_spec_unverified
• contrib::exec_spec::exec_spec_verified
• contrib::set_build
• contrib::set_build_debug
• imap
• imap::assert_imaps_equal
• imap::imap
• invariant::open_atomic_invariant
• invariant::open_atomic_invariant_in_proof
• invariant::open_local_invariant
• invariant::open_local_invariant_in_proof
• iset
• iset::iset
• iset_lib::assert_isets_equal
• map
• map::assert_maps_equal
• map::map
• multiset::assert_multisets_equal
• open_atomic_invariant
• open_atomic_invariant_in_proof
• open_atomic_invariant_in_proof_internal
• open_atomic_invariant_internal
• open_atomic_update
• open_atomic_update_in_proof
• open_local_invariant
• open_local_invariant_in_proof
• open_local_invariant_in_proof_internal
• open_local_invariant_internal
• pcell_points
• peek_atomic_update
• peek_atomic_update_in_proof
• pervasive::struct_with_invariants
• prelude::atomic_with_ghost_helper
• prelude::calc_proc_macro
• prelude::decreases_to
• prelude::decreases_to_internal
• prelude::fndecl
• prelude::proof
• prelude::proof_decl
• prelude::proof_with
• prelude::struct_with_invariants
• prelude::verus
• prelude::verus_erase_ghost
• prelude::verus_exec_expr
• prelude::verus_exec_expr_erase_ghost
• prelude::verus_exec_expr_keep_ghost
• prelude::verus_exec_inv_macro_exprs
• prelude::verus_exec_macro_exprs
• prelude::verus_ghost_inv_macro_exprs
• prelude::verus_impl
• prelude::verus_keep_ghost
• prelude::verus_proof_expr
• prelude::verus_proof_macro_explicit_exprs
• prelude::verus_proof_macro_exprs
• prelude::verus_trait_impl
• prelude::with_triggers
• seq
• seq::seq
• seq_lib::assert_seqs_equal
• set
• set::set
• set_lib::assert_sets_equal
• try_open_atomic_update
• try_open_atomic_update_in_proof
• try_open_atomic_update_internal
• vpanic

Attribute Macros

• contrib::auto_spec
• contrib::make_spec_type
• contrib::self_view
• prelude::is_variant
• prelude::is_variant_no_deprecation_warning
• prelude::verus_enum_synthesize
• prelude::verus_spec
• prelude::verus_verify

Derive Macros

• prelude::Structural
• prelude::StructuralEq

Functions

• arithmetic::div_mod::group_div_basics
• arithmetic::div_mod::group_fundamental_div_mod_converse
• arithmetic::div_mod::group_mod_basics
• arithmetic::div_mod::group_mod_properties
• arithmetic::mul::group_mul_basics
• arithmetic::mul::group_mul_is_commutative_and_distributive
• arithmetic::mul::group_mul_is_distributive
• arithmetic::mul::group_mul_properties
• arithmetic::power::group_pow_properties
• array::array_index_get
• array::group_array_axioms
• bytes::u128_from_le_bytes
• bytes::u128_to_le_bytes
• bytes::u16_from_le_bytes
• bytes::u16_to_le_bytes
• bytes::u32_from_le_bytes
• bytes::u32_to_le_bytes
• bytes::u64_from_le_bytes
• bytes::u64_to_le_bytes
• endian::group_endian_nat_axioms
• function::group_function_axioms
• group_vstd_default
• hash_map::group_hash_map_axioms
• hash_set::group_hash_set_axioms
• imap::group_imap_lemmas
• imap_lib::group_imap_extra
• imap_lib::group_imap_properties
• imap_lib::group_imap_union
• invariant::create_open_invariant_credit
• iset::group_iset_lemmas
• iset_lib::group_iset_lib_default
• iset_lib::group_iset_properties
• layout::group_align_properties
• layout::group_layout_axioms
• layout::layout_for_type_is_valid
• layout::layout_for_val_is_valid
• map::group_map_lemmas
• map_lib::group_map_extra
• map_lib::group_map_properties
• map_lib::group_map_union
• multiset::group_multiset_axioms
• multiset::group_multiset_properties
• pervasive::print_u64
• pervasive::runtime_assert
• pervasive::unreached
• raw_ptr::allocate
• raw_ptr::cast_array_ptr_to_slice_ptr
• raw_ptr::cast_ptr_to_thin_ptr
• raw_ptr::cast_ptr_to_usize
• raw_ptr::cast_slice_ptr_to_slice_ptr
• raw_ptr::cast_slice_ptr_to_str_ptr
• raw_ptr::cast_str_ptr_to_slice_ptr
• raw_ptr::deallocate
• raw_ptr::expose_provenance
• raw_ptr::group_raw_ptr_axioms
• raw_ptr::ptr_mut_read
• raw_ptr::ptr_mut_ref
• raw_ptr::ptr_mut_write
• raw_ptr::ptr_ref
• raw_ptr::ptr_ref2
• raw_ptr::with_exposed_provenance
• seq::group_seq_axioms
• seq::group_seq_lemmas
• seq::group_seq_lemmas_expensive
• seq_lib::group_filter_ensures
• seq_lib::group_seq_lib_default
• seq_lib::group_seq_properties
• seq_lib::group_to_multiset_ensures
• set::group_set_lemmas
• set_lib::group_set_lib_default
• set_lib::group_set_properties
• slice::group_slice_axioms
• slice::slice_index_get
• slice::slice_subrange
• slice::slice_to_vec
• string::group_string_axioms
• thread::spawn
• thread::thread_id
• utf8::group_utf8_lib

Type Aliases

• atomic::AtomicCellId
• contrib::exec_spec::SpecString
• raw_ptr::Metadata
• rwlock::FieldType_RwLock_cell
• rwlock::FieldType_RwLock_exc
• rwlock::FieldType_RwLock_inst
• rwlock::FieldType_RwLock_pred
• rwlock::FieldType_RwLock_rc
• rwlock::RwLockToks::pending_reader_multiset
• rwlock::RwLockToks::reader_multiset
• tokens::InstanceId

Constants

• prelude::PROOF_FN
• prelude::PROOF_FN_COPY
• prelude::PROOF_FN_MUT
• prelude::PROOF_FN_ONCE
• prelude::PROOF_FN_SEND
• prelude::PROOF_FN_SYNC