List of all items

Structs

• arithmetic::overflow::CheckedU128
• arithmetic::overflow::CheckedU16
• arithmetic::overflow::CheckedU32
• arithmetic::overflow::CheckedU64
• arithmetic::overflow::CheckedU8
• arithmetic::overflow::CheckedUsize
• 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
• hash_map::HashMapWithView
• hash_map::StringHashMap
• hash_set::HashSetWithView
• hash_set::StringHashSet
• invariant::AtomicInvariant
• invariant::LocalInvariant
• map::Map
• multiset::Multiset
• pcm::Resource
• pcm::frac::FracGhost
• pcm::frac::GhostVar
• pcm::frac::GhostVarAuth
• prelude::FnSpec
• prelude::Ghost
• prelude::NoCopy
• prelude::SpecChain
• prelude::Tracked
• prelude::int
• prelude::nat
• proph::Prophecy
• raw_ptr::Dealloc
• raw_ptr::DeallocData
• raw_ptr::DynMetadata
• raw_ptr::IsExposed
• raw_ptr::PointsTo
• raw_ptr::PointsToData
• raw_ptr::PointsToRaw
• raw_ptr::Provenance
• raw_ptr::PtrData
• raw_ptr::SharedReference
• 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
• shared::Dupe::Instance
• shared::Dupe::State
• shared::Shared
• simple_pptr::PPtr
• simple_pptr::PointsTo
• std_specs::VstdSpecsForRustStdLib
• std_specs::alloc::ExGlobal
• std_specs::atomic::ExOrdering
• std_specs::control_flow::ExControlFlow
• std_specs::control_flow::ExInfallible
• std_specs::core::ExDuration
• std_specs::core::ExManuallyDrop
• std_specs::core::ExOption
• std_specs::core::ExPhantomData
• std_specs::core::ExResult
• std_specs::hash::ExDefaultHasher
• std_specs::hash::ExHashMap
• std_specs::hash::ExHashSet
• std_specs::hash::ExIter
• std_specs::hash::ExKeys
• std_specs::hash::ExRandomState
• std_specs::hash::IterGhostIterator
• std_specs::hash::KeysGhostIterator
• std_specs::range::ExRange
• std_specs::range::RangeGhostIterator
• std_specs::vec::ExVec
• std_specs::vecdeque::ExIter
• std_specs::vecdeque::ExVecDeque
• std_specs::vecdeque::IterGhostIterator
• storage_protocol::StorageResource
• string::ExString
• thread::IsThread
• thread::JoinHandle
• thread::ThreadId
• tokens::InstanceId
• tokens::MapToken
• tokens::MultisetToken
• tokens::SetToken

Enums

• raw_ptr::MemContents
• raw_ptr::Metadata
• rwlock::RwLockToks::Config
• rwlock::RwLockToks::Step
• shared::Dupe::Config
• shared::Dupe::Step

Traits

• array::ArrayAdditionalExecFns
• array::ArrayAdditionalSpecFns
• atomic_ghost::AtomicInvariantPredicate
• compute::RangeAll
• invariant::InvariantPredicate
• pcm::PCM
• pervasive::FnWithRequiresEnsures
• pervasive::ForLoopGhostIterator
• pervasive::ForLoopGhostIteratorNew
• pervasive::VecAdditionalExecFns
• prelude::Boolean
• prelude::Integer
• prelude::SpecAdd
• prelude::SpecBitAnd
• prelude::SpecBitOr
• prelude::SpecBitXor
• prelude::SpecEuclideanDiv
• prelude::SpecEuclideanMod
• prelude::SpecMul
• prelude::SpecNeg
• prelude::SpecOrd
• prelude::SpecShl
• prelude::SpecShr
• prelude::SpecSub
• prelude::Structural
• rwlock::RwLockPredicate
• slice::ExSliceIndex
• slice::SliceAdditionalExecFns
• slice::SliceAdditionalSpecFns
• std_specs::clone::ExClone
• std_specs::core::ExAllocator
• std_specs::core::ExBorrow
• std_specs::core::ExDebug
• std_specs::core::ExEq
• std_specs::core::ExFreeze
• std_specs::core::ExFrom
• std_specs::core::ExHash
• std_specs::core::ExIndex
• std_specs::core::ExIndexMut
• std_specs::core::ExInteger
• std_specs::core::ExInto
• std_specs::core::ExIntoIterator
• std_specs::core::ExIterStep
• std_specs::core::ExIterator
• std_specs::core::ExOrd
• std_specs::core::ExPartialEq
• std_specs::core::ExPartialOrd
• std_specs::core::ExPtrPointee
• std_specs::core::ExSpecOrd
• std_specs::core::ExStructural
• std_specs::core::IndexSetTrustedSpec
• std_specs::hash::DefaultHasherAdditionalSpecFns
• std_specs::hash::ExBuildHasher
• std_specs::hash::ExHasher
• std_specs::hash::HashMapAdditionalSpecFns
• std_specs::hash::IterAdditionalSpecFns
• std_specs::hash::KeysAdditionalSpecFns
• std_specs::option::OptionAdditionalFns
• std_specs::range::StepSpec
• std_specs::result::ResultAdditionalSpecFns
• std_specs::vec::VecAdditionalSpecFns
• std_specs::vecdeque::IterAdditionalSpecFns
• std_specs::vecdeque::VecDequeAdditionalSpecFns
• storage_protocol::Protocol
• string::StrSliceExecFns
• string::StringExecFns
• string::StringExecFnsIsAscii
• 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_maps_equal
• assert_multisets_equal
• assert_multisets_equal_internal
• assert_seqs_equal
• assert_sets_equal
• atomic_ghost::atomic_with_ghost
• atomic_with_ghost
• calc
• calc_macro::calc
• cell::pcell_opt
• cell::pcell_points
• invariant::open_atomic_invariant
• invariant::open_atomic_invariant_in_proof
• invariant::open_local_invariant
• invariant::open_local_invariant_in_proof
• 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_local_invariant
• open_local_invariant_in_proof
• open_local_invariant_in_proof_internal
• open_local_invariant_internal
• pcell_opt
• pcell_points
• 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::struct_with_invariants
• prelude::struct_with_invariants_vstd
• 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_keep_ghost
• prelude::verus_proof_expr
• prelude::verus_proof_macro_explicit_exprs
• prelude::verus_proof_macro_exprs
• prelude::with_triggers
• seq
• seq::seq
• seq_lib::assert_seqs_equal
• set
• set::set
• set_lib::assert_sets_equal
• vpanic

Attribute Macros

• prelude::is_variant
• prelude::is_variant_no_deprecation_warning
• prelude::verus_enum_synthesize
• prelude::verus_spec
• prelude::verus_verify

Derive Macros

• prelude::Structural

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::div_mod::is_mod_equivalent
• arithmetic::div_mod::lemma_add_mod_noop
• arithmetic::div_mod::lemma_add_mod_noop_right
• arithmetic::div_mod::lemma_basic_div
• arithmetic::div_mod::lemma_basic_div_specific_divisor
• arithmetic::div_mod::lemma_breakdown
• arithmetic::div_mod::lemma_div_basics
• arithmetic::div_mod::lemma_div_basics_1
• arithmetic::div_mod::lemma_div_basics_2
• arithmetic::div_mod::lemma_div_basics_3
• arithmetic::div_mod::lemma_div_basics_4
• arithmetic::div_mod::lemma_div_basics_5
• arithmetic::div_mod::lemma_div_by_multiple
• arithmetic::div_mod::lemma_div_by_multiple_is_strongly_ordered
• arithmetic::div_mod::lemma_div_by_self
• arithmetic::div_mod::lemma_div_decreases
• arithmetic::div_mod::lemma_div_denominator
• arithmetic::div_mod::lemma_div_is_div_recursive
• arithmetic::div_mod::lemma_div_is_ordered
• arithmetic::div_mod::lemma_div_is_ordered_by_denominator
• arithmetic::div_mod::lemma_div_is_strictly_smaller
• arithmetic::div_mod::lemma_div_minus_one
• arithmetic::div_mod::lemma_div_multiples_vanish
• arithmetic::div_mod::lemma_div_multiples_vanish_fancy
• arithmetic::div_mod::lemma_div_multiples_vanish_quotient
• arithmetic::div_mod::lemma_div_non_zero
• arithmetic::div_mod::lemma_div_nonincreasing
• arithmetic::div_mod::lemma_div_of0
• arithmetic::div_mod::lemma_div_plus_one
• arithmetic::div_mod::lemma_div_pos_is_pos
• arithmetic::div_mod::lemma_dividing_sums
• arithmetic::div_mod::lemma_fundamental_div_mod
• arithmetic::div_mod::lemma_fundamental_div_mod_converse
• arithmetic::div_mod::lemma_fundamental_div_mod_converse_div
• arithmetic::div_mod::lemma_fundamental_div_mod_converse_mod
• arithmetic::div_mod::lemma_hoist_over_denominator
• arithmetic::div_mod::lemma_indistinguishable_quotients
• arithmetic::div_mod::lemma_mod_add_multiples_vanish
• arithmetic::div_mod::lemma_mod_adds
• arithmetic::div_mod::lemma_mod_bound
• arithmetic::div_mod::lemma_mod_breakdown
• arithmetic::div_mod::lemma_mod_decreases
• arithmetic::div_mod::lemma_mod_division_less_than_divisor
• arithmetic::div_mod::lemma_mod_equivalence
• arithmetic::div_mod::lemma_mod_is_mod_recursive
• arithmetic::div_mod::lemma_mod_is_zero
• arithmetic::div_mod::lemma_mod_mod
• arithmetic::div_mod::lemma_mod_mul_equivalent
• arithmetic::div_mod::lemma_mod_multiples_basic
• arithmetic::div_mod::lemma_mod_multiples_vanish
• arithmetic::div_mod::lemma_mod_neg_neg
• arithmetic::div_mod::lemma_mod_ordering
• arithmetic::div_mod::lemma_mod_pos_bound
• arithmetic::div_mod::lemma_mod_self_0
• arithmetic::div_mod::lemma_mod_sub_multiples_vanish
• arithmetic::div_mod::lemma_mod_subtraction
• arithmetic::div_mod::lemma_mod_twice
• arithmetic::div_mod::lemma_mul_hoist_inequality
• arithmetic::div_mod::lemma_mul_mod_noop
• arithmetic::div_mod::lemma_mul_mod_noop_general
• arithmetic::div_mod::lemma_mul_mod_noop_left
• arithmetic::div_mod::lemma_mul_mod_noop_right
• arithmetic::div_mod::lemma_multiply_divide_le
• arithmetic::div_mod::lemma_multiply_divide_lt
• arithmetic::div_mod::lemma_part_bound1
• arithmetic::div_mod::lemma_part_bound2
• arithmetic::div_mod::lemma_remainder
• arithmetic::div_mod::lemma_remainder_lower
• arithmetic::div_mod::lemma_remainder_upper
• arithmetic::div_mod::lemma_round_down
• arithmetic::div_mod::lemma_small_div_converse
• arithmetic::div_mod::lemma_small_mod
• arithmetic::div_mod::lemma_sub_mod_noop
• arithmetic::div_mod::lemma_sub_mod_noop_right
• arithmetic::div_mod::lemma_truncate_middle
• arithmetic::logarithm::lemma_log0
• arithmetic::logarithm::lemma_log_is_ordered
• arithmetic::logarithm::lemma_log_nonnegative
• arithmetic::logarithm::lemma_log_pow
• arithmetic::logarithm::lemma_log_s
• arithmetic::logarithm::log
• 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::mul::lemma_mul_basics
• arithmetic::mul::lemma_mul_basics_1
• arithmetic::mul::lemma_mul_basics_2
• arithmetic::mul::lemma_mul_basics_3
• arithmetic::mul::lemma_mul_basics_4
• arithmetic::mul::lemma_mul_by_zero_is_zero
• arithmetic::mul::lemma_mul_cancels_negatives
• arithmetic::mul::lemma_mul_equality_converse
• arithmetic::mul::lemma_mul_increases
• arithmetic::mul::lemma_mul_inequality
• arithmetic::mul::lemma_mul_inequality_converse
• arithmetic::mul::lemma_mul_is_associative
• arithmetic::mul::lemma_mul_is_commutative
• arithmetic::mul::lemma_mul_is_distributive_add
• arithmetic::mul::lemma_mul_is_distributive_add_other_way
• arithmetic::mul::lemma_mul_is_distributive_sub
• arithmetic::mul::lemma_mul_is_distributive_sub_other_way
• arithmetic::mul::lemma_mul_is_mul_pos
• arithmetic::mul::lemma_mul_is_mul_recursive
• arithmetic::mul::lemma_mul_left_inequality
• arithmetic::mul::lemma_mul_nonnegative
• arithmetic::mul::lemma_mul_nonzero
• arithmetic::mul::lemma_mul_ordering
• arithmetic::mul::lemma_mul_strict_inequality
• arithmetic::mul::lemma_mul_strict_inequality_converse
• arithmetic::mul::lemma_mul_strict_upper_bound
• arithmetic::mul::lemma_mul_strictly_increases
• arithmetic::mul::lemma_mul_strictly_positive
• arithmetic::mul::lemma_mul_unary_negation
• arithmetic::mul::lemma_mul_upper_bound
• arithmetic::power2::lemma2_to64
• arithmetic::power2::lemma2_to64_rest
• arithmetic::power2::lemma_pow2
• arithmetic::power2::lemma_pow2_adds
• arithmetic::power2::lemma_pow2_pos
• arithmetic::power2::lemma_pow2_strictly_increases
• arithmetic::power2::lemma_pow2_unfold
• arithmetic::power2::pow2
• arithmetic::power::group_pow_properties
• arithmetic::power::lemma0_pow
• arithmetic::power::lemma1_pow
• arithmetic::power::lemma_pow0
• arithmetic::power::lemma_pow1
• arithmetic::power::lemma_pow_adds
• arithmetic::power::lemma_pow_distributes
• arithmetic::power::lemma_pow_division_inequality
• arithmetic::power::lemma_pow_increases
• arithmetic::power::lemma_pow_increases_converse
• arithmetic::power::lemma_pow_mod
• arithmetic::power::lemma_pow_mod_noop
• arithmetic::power::lemma_pow_multiplies
• arithmetic::power::lemma_pow_positive
• arithmetic::power::lemma_pow_strictly_increases
• arithmetic::power::lemma_pow_strictly_increases_converse
• arithmetic::power::lemma_pow_sub_add_cancel
• arithmetic::power::lemma_pow_subtracts
• arithmetic::power::lemma_pull_out_pows
• arithmetic::power::lemma_square_is_pow2
• arithmetic::power::pow
• array::_verus_external_fn_specification_0__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice
• array::array_index_get
• array::array_len_matches_n
• array::array_view
• array::axiom_spec_array_as_slice
• array::axiom_spec_array_fill_for_copy_type
• array::group_array_axioms
• array::lemma_array_index
• array::spec_array_as_slice
• array::spec_array_fill_for_copy_type
• atomic::wrapping_add_i16
• atomic::wrapping_add_i32
• atomic::wrapping_add_i64
• atomic::wrapping_add_i8
• atomic::wrapping_add_isize
• atomic::wrapping_add_u16
• atomic::wrapping_add_u32
• atomic::wrapping_add_u64
• atomic::wrapping_add_u8
• atomic::wrapping_add_usize
• atomic::wrapping_sub_i16
• atomic::wrapping_sub_i32
• atomic::wrapping_sub_i64
• atomic::wrapping_sub_i8
• atomic::wrapping_sub_isize
• atomic::wrapping_sub_u16
• atomic::wrapping_sub_u32
• atomic::wrapping_sub_u64
• atomic::wrapping_sub_u8
• atomic::wrapping_sub_usize
• bits::lemma_low_bits_mask_div2
• bits::lemma_low_bits_mask_is_odd
• bits::lemma_low_bits_mask_unfold
• bits::lemma_low_bits_mask_values
• bits::lemma_u16_low_bits_mask_is_mod
• bits::lemma_u16_pow2_no_overflow
• bits::lemma_u16_shl_is_mul
• bits::lemma_u16_shr_is_div
• bits::lemma_u32_low_bits_mask_is_mod
• bits::lemma_u32_pow2_no_overflow
• bits::lemma_u32_shl_is_mul
• bits::lemma_u32_shr_is_div
• bits::lemma_u64_low_bits_mask_is_mod
• bits::lemma_u64_pow2_no_overflow
• bits::lemma_u64_shl_is_mul
• bits::lemma_u64_shr_is_div
• bits::lemma_u8_low_bits_mask_is_mod
• bits::lemma_u8_pow2_no_overflow
• bits::lemma_u8_shl_is_mul
• bits::lemma_u8_shr_is_div
• bits::low_bits_mask
• bytes::lemma_auto_spec_u128_to_from_le_bytes
• bytes::lemma_auto_spec_u16_to_from_le_bytes
• bytes::lemma_auto_spec_u32_to_from_le_bytes
• bytes::lemma_auto_spec_u64_to_from_le_bytes
• bytes::spec_u128_from_le_bytes
• bytes::spec_u128_to_le_bytes
• bytes::spec_u16_from_le_bytes
• bytes::spec_u16_to_le_bytes
• bytes::spec_u32_from_le_bytes
• bytes::spec_u32_to_le_bytes
• bytes::spec_u64_from_le_bytes
• bytes::spec_u64_to_le_bytes
• 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
• compute::all_spec_ensures
• compute::range_all_spec_rec
• group_vstd_default
• hash_map::axiom_hash_map_with_view_spec_len
• hash_map::axiom_string_hash_map_spec_len
• hash_map::group_hash_map_axioms
• hash_set::axiom_hash_set_with_view_spec_len
• hash_set::axiom_string_hash_set_spec_len
• hash_set::group_hash_set_axioms
• invariant::create_open_invariant_credit
• layout::_verus_external_fn_specification_1_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_
• layout::_verus_external_fn_specification_2_core_32__58__58__32_mem_32__58__58__32_align__of_32__58__58__32__60__32_V_32__62_
• layout::align_of
• layout::align_of_as_usize
• layout::group_layout_axioms
• layout::is_power_2
• layout::is_sized
• layout::layout_for_type_is_valid
• layout::layout_of_primitives
• layout::layout_of_references_and_pointers
• layout::layout_of_references_and_pointers_for_sized_types
• layout::layout_of_unit_tuple
• layout::size_of
• layout::size_of_as_usize
• layout::valid_layout
• map::axiom_map_empty
• map::axiom_map_ext_equal
• map::axiom_map_ext_equal_deep
• map::axiom_map_index_decreases_finite
• map::axiom_map_index_decreases_infinite
• map::axiom_map_insert_different
• map::axiom_map_insert_domain
• map::axiom_map_insert_same
• map::axiom_map_remove_different
• map::axiom_map_remove_domain
• map::group_map_axioms
• map_lib::group_map_properties
• map_lib::group_map_union
• map_lib::lemma_disjoint_union_size
• map_lib::lemma_map_new_domain
• map_lib::lemma_map_new_values
• map_lib::lemma_map_properties
• map_lib::lemma_submap_of_trans
• map_lib::lemma_union_dom
• map_lib::lemma_union_insert_left
• map_lib::lemma_union_insert_right
• map_lib::lemma_union_remove_left
• map_lib::lemma_union_remove_right
• map_lib::lemma_values_finite
• math::abs
• math::add
• math::clip
• math::div
• math::max
• math::max3
• math::min
• math::sub
• modes::tracked_static_ref
• modes::tracked_swap
• multiset::axiom_choose_count
• multiset::axiom_count_le_len
• multiset::axiom_filter_count
• multiset::axiom_len_add
• multiset::axiom_len_empty
• multiset::axiom_len_singleton
• multiset::axiom_len_sub
• multiset::axiom_multiset_add
• multiset::axiom_multiset_always_finite
• multiset::axiom_multiset_contained
• multiset::axiom_multiset_empty
• multiset::axiom_multiset_ext_equal
• multiset::axiom_multiset_ext_equal_deep
• multiset::axiom_multiset_new_not_contained
• multiset::axiom_multiset_singleton
• multiset::axiom_multiset_singleton_different
• multiset::axiom_multiset_sub
• multiset::group_multiset_axioms
• multiset::group_multiset_properties
• multiset::lemma_difference_bottoms_out
• multiset::lemma_difference_count
• multiset::lemma_insert_containment
• multiset::lemma_insert_increases_count_by_1
• multiset::lemma_insert_len
• multiset::lemma_insert_non_decreasing
• multiset::lemma_insert_other_elements_unchanged
• multiset::lemma_intersection_count
• multiset::lemma_left_pseudo_idempotence
• multiset::lemma_multiset_empty_len
• multiset::lemma_multiset_properties
• multiset::lemma_right_pseudo_idempotence
• multiset::lemma_update_different
• multiset::lemma_update_same
• pcm::conjunct_shared
• pcm::frame_preserving_update
• pcm::frame_preserving_update_nondeterministic
• pcm::incl
• pcm::set_op
• pcm_lib::combine_values
• pcm_lib::copy_duplicable_part
• pcm_lib::duplicate
• pcm_lib::extract
• pcm_lib::incorporate
• pcm_lib::lemma_pcm_properties
• pcm_lib::redistribute
• pcm_lib::split_mut
• pcm_lib::update_and_redistribute
• pcm_lib::update_mut
• pcm_lib::validate_3
• pcm_lib::validate_4
• pcm_lib::validate_5
• pcm_lib::validate_multiple
• pervasive::affirm
• pervasive::allow_panic
• pervasive::arbitrary
• pervasive::assert
• pervasive::assume
• pervasive::cloned
• pervasive::print_u64
• pervasive::proof_from_false
• pervasive::runtime_assert
• pervasive::spec_affirm
• pervasive::strictly_cloned
• pervasive::trigger
• pervasive::unreached
• prelude::add
• prelude::admit
• prelude::arch_word_bits
• prelude::array_index
• prelude::assert_
• prelude::assert_bit_vector
• prelude::assert_bitvector_by
• prelude::assert_by
• prelude::assert_by_compute
• prelude::assert_by_compute_only
• prelude::assert_forall_by
• prelude::assert_nonlinear_by
• prelude::assume_
• prelude::call_ensures
• prelude::call_requires
• prelude::choose
• prelude::choose_tuple
• prelude::closure_to_fn_spec
• prelude::decreases
• prelude::decreases_by
• prelude::decreases_when
• prelude::ensures
• prelude::equal
• prelude::exists
• prelude::ext_equal
• prelude::ext_equal_deep
• prelude::extra_dependency
• prelude::forall
• prelude::get_union_field
• prelude::get_variant_field
• prelude::ghost_exec
• prelude::global_size_of
• prelude::imply
• prelude::infer_spec_for_loop_iter
• prelude::inline_air_stmt
• prelude::invariant
• prelude::invariant_except_break
• prelude::is_smaller_than
• prelude::is_smaller_than_lexicographic
• prelude::is_smaller_than_recursive_function_field
• prelude::is_variant
• prelude::mul
• prelude::no_method_body
• prelude::no_unwind
• prelude::no_unwind_when
• prelude::old
• prelude::opens_invariants
• prelude::opens_invariants_any
• prelude::opens_invariants_except
• prelude::opens_invariants_none
• prelude::opens_invariants_set
• prelude::recommends
• prelude::recommends_by
• prelude::requires
• prelude::returns
• prelude::reveal_hide_
• prelude::reveal_hide_internal_path_
• prelude::reveal_strlit
• prelude::signed_max
• prelude::signed_min
• prelude::spec_cast_integer
• prelude::spec_chained_cmp
• prelude::spec_chained_eq
• prelude::spec_chained_ge
• prelude::spec_chained_gt
• prelude::spec_chained_le
• prelude::spec_chained_lt
• prelude::spec_chained_value
• prelude::spec_eq
• prelude::spec_literal_int
• prelude::spec_literal_integer
• prelude::spec_literal_nat
• prelude::strslice_get_char
• prelude::strslice_is_ascii
• prelude::strslice_len
• prelude::sub
• prelude::tracked_exec
• prelude::tracked_exec_borrow
• prelude::unsigned_max
• prelude::use_type_invariant
• prelude::with_triggers
• raw_ptr::_verus_external_fn_specification_3_core_32__58__58__32_ptr_32__58__58__32_null
• raw_ptr::_verus_external_fn_specification_4_core_32__58__58__32_ptr_32__58__58__32_null__mut
• raw_ptr::allocate
• raw_ptr::axiom_ptr_mut_from_data
• raw_ptr::cast_array_ptr_to_slice_ptr
• raw_ptr::cast_ptr_to_thin_ptr
• raw_ptr::cast_ptr_to_usize
• raw_ptr::deallocate
• raw_ptr::expose_provenance
• raw_ptr::group_raw_ptr_axioms
• raw_ptr::ptr_from_data
• raw_ptr::ptr_mut_from_data
• raw_ptr::ptr_mut_read
• raw_ptr::ptr_mut_write
• raw_ptr::ptr_null
• raw_ptr::ptr_null_mut
• raw_ptr::ptr_ref
• raw_ptr::ptr_ref2
• raw_ptr::ptrs_mut_eq
• raw_ptr::spec_cast_array_ptr_to_slice_ptr
• raw_ptr::spec_cast_ptr_to_thin_ptr
• raw_ptr::spec_cast_ptr_to_usize
• raw_ptr::with_exposed_provenance
• relations::antisymmetric
• relations::associative
• relations::asymmetric
• relations::commutative
• relations::connected
• relations::equivalence_relation
• relations::injective
• relations::irreflexive
• relations::is_greatest
• relations::is_least
• relations::is_maximal
• relations::is_minimal
• relations::lemma_new_first_element_still_sorted_by
• relations::partial_ordering
• relations::pre_ordering
• relations::reflexive
• relations::sorted_by
• relations::strict_total_ordering
• relations::strongly_connected
• relations::symmetric
• relations::total_ordering
• relations::transitive
• rwlock::RwLockToks::show::acquire_exc_end
• rwlock::RwLockToks::show::acquire_exc_start
• rwlock::RwLockToks::show::acquire_read_abandon
• rwlock::RwLockToks::show::acquire_read_end
• rwlock::RwLockToks::show::acquire_read_start
• rwlock::RwLockToks::show::initialize_full
• rwlock::RwLockToks::show::release_exc
• rwlock::RwLockToks::show::release_shared
• rwlock::RwLockToks::take_step::acquire_exc_end
• rwlock::RwLockToks::take_step::acquire_exc_start
• rwlock::RwLockToks::take_step::acquire_read_abandon
• rwlock::RwLockToks::take_step::acquire_read_end
• rwlock::RwLockToks::take_step::acquire_read_start
• rwlock::RwLockToks::take_step::initialize_full
• rwlock::RwLockToks::take_step::release_exc
• rwlock::RwLockToks::take_step::release_shared
• seq::axiom_seq_add_index1
• seq::axiom_seq_add_index2
• seq::axiom_seq_add_len
• seq::axiom_seq_empty
• seq::axiom_seq_ext_equal
• seq::axiom_seq_ext_equal_deep
• seq::axiom_seq_index_decreases
• seq::axiom_seq_len_decreases
• seq::axiom_seq_new_index
• seq::axiom_seq_new_len
• seq::axiom_seq_push_index_different
• seq::axiom_seq_push_index_same
• seq::axiom_seq_push_len
• seq::axiom_seq_subrange_decreases
• seq::axiom_seq_subrange_index
• seq::axiom_seq_subrange_len
• seq::axiom_seq_update_different
• seq::axiom_seq_update_len
• seq::axiom_seq_update_same
• seq::group_seq_axioms
• seq_lib::commutative_foldr
• seq_lib::group_filter_ensures
• seq_lib::group_seq_lib_default
• seq_lib::group_seq_properties
• seq_lib::group_to_multiset_ensures
• seq_lib::lemma_append_last
• seq_lib::lemma_concat_associative
• seq_lib::lemma_flatten_alt_concat
• seq_lib::lemma_flatten_concat
• seq_lib::lemma_fold_right_permutation
• seq_lib::lemma_max_of_concat
• seq_lib::lemma_min_of_concat
• seq_lib::lemma_multiset_commutative
• seq_lib::lemma_no_dup_in_concat
• seq_lib::lemma_seq_append_take_skip
• seq_lib::lemma_seq_concat_contains_all_elements
• seq_lib::lemma_seq_contains
• seq_lib::lemma_seq_contains_after_push
• seq_lib::lemma_seq_empty_contains_nothing
• seq_lib::lemma_seq_empty_equality
• seq_lib::lemma_seq_properties
• seq_lib::lemma_seq_skip_build_commut
• seq_lib::lemma_seq_skip_contains
• seq_lib::lemma_seq_skip_index
• seq_lib::lemma_seq_skip_index2
• seq_lib::lemma_seq_skip_len
• seq_lib::lemma_seq_skip_nothing
• seq_lib::lemma_seq_skip_of_skip
• seq_lib::lemma_seq_skip_update_commut1
• seq_lib::lemma_seq_skip_update_commut2
• seq_lib::lemma_seq_subrange_elements
• seq_lib::lemma_seq_take_contains
• seq_lib::lemma_seq_take_index
• seq_lib::lemma_seq_take_len
• seq_lib::lemma_seq_take_nothing
• seq_lib::lemma_seq_take_update_commut1
• seq_lib::lemma_seq_take_update_commut2
• seq_lib::lemma_seq_union_to_multiset_commutative
• seq_lib::lemma_sorted_unique
• seq_lib::seq_to_set_is_finite
• seq_lib::subrange_of_matching_take
• seq_lib::to_multiset_build
• seq_lib::to_multiset_contains
• seq_lib::to_multiset_len
• seq_lib::to_multiset_remove
• set::axiom_mk_map_domain
• set::axiom_mk_map_index
• set::axiom_set_choose_finite
• set::axiom_set_choose_len
• set::axiom_set_complement
• set::axiom_set_contains_len
• set::axiom_set_difference
• set::axiom_set_difference_finite
• set::axiom_set_empty
• set::axiom_set_empty_finite
• set::axiom_set_empty_len
• set::axiom_set_ext_equal
• set::axiom_set_ext_equal_deep
• set::axiom_set_insert_different
• set::axiom_set_insert_finite
• set::axiom_set_insert_len
• set::axiom_set_insert_same
• set::axiom_set_intersect
• set::axiom_set_intersect_finite
• set::axiom_set_new
• set::axiom_set_remove_different
• set::axiom_set_remove_finite
• set::axiom_set_remove_insert
• set::axiom_set_remove_len
• set::axiom_set_remove_same
• set::axiom_set_union
• set::axiom_set_union_finite
• set::fold::is_fun_commutative
• set::fold::lemma_finite_set_induct
• set::fold::lemma_fold_empty
• set::fold::lemma_fold_insert
• set::group_set_axioms
• set_lib::axiom_is_empty
• set_lib::axiom_is_empty_len0
• set_lib::group_set_lib_default
• set_lib::group_set_properties
• set_lib::lemma_int_range
• set_lib::lemma_len_difference
• set_lib::lemma_len_intersect
• set_lib::lemma_len_subset
• set_lib::lemma_len_union
• set_lib::lemma_len_union_ind
• set_lib::lemma_map_size
• set_lib::lemma_set_difference2
• set_lib::lemma_set_difference_len
• set_lib::lemma_set_disjoint
• set_lib::lemma_set_disjoint_lens
• set_lib::lemma_set_empty_equivalency_len
• set_lib::lemma_set_insert_finite_iff
• set_lib::lemma_set_intersect_again1
• set_lib::lemma_set_intersect_again2
• set_lib::lemma_set_intersect_union_lens
• set_lib::lemma_set_properties
• set_lib::lemma_set_remove_finite_iff
• set_lib::lemma_set_subset_finite
• set_lib::lemma_set_union_again1
• set_lib::lemma_set_union_again2
• set_lib::lemma_set_union_finite_iff
• set_lib::lemma_set_union_finite_implies_sets_finite
• set_lib::lemma_subset_equality
• set_lib::set_int_range
• shared::Dupe::show::initialize_one
• shared::Dupe::take_step::initialize_one
• slice::_verus_external_fn_specification_5__60__32__91_T_93__32__62__32__58__58__32_len
• slice::_verus_external_fn_specification_6__60__32__91_T_93__32__62__32__58__58__32_get_32__58__58__32__60__32_I_32__62_
• slice::axiom_slice_get_usize
• slice::axiom_spec_len
• slice::group_slice_axioms
• slice::slice_index_get
• slice::slice_subrange
• slice::slice_to_vec
• slice::spec_slice_get
• slice::spec_slice_len
• std_specs::bits::_verus_external_fn_specification_13_u8_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_14_u8_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_15_u8_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_16_u8_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_17_u16_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_18_u16_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_19_u16_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_20_u16_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_21_u32_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_22_u32_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_23_u32_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_24_u32_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_25_u64_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_26_u64_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_27_u64_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_28_u64_32__58__58__32_leading__ones
• std_specs::bits::axiom_u16_leading_ones
• std_specs::bits::axiom_u16_leading_zeros
• std_specs::bits::axiom_u16_trailing_ones
• std_specs::bits::axiom_u16_trailing_zeros
• std_specs::bits::axiom_u32_leading_ones
• std_specs::bits::axiom_u32_leading_zeros
• std_specs::bits::axiom_u32_trailing_ones
• std_specs::bits::axiom_u32_trailing_zeros
• std_specs::bits::axiom_u64_leading_ones
• std_specs::bits::axiom_u64_leading_zeros
• std_specs::bits::axiom_u64_trailing_ones
• std_specs::bits::axiom_u64_trailing_zeros
• std_specs::bits::axiom_u8_leading_ones
• std_specs::bits::axiom_u8_leading_zeros
• std_specs::bits::axiom_u8_trailing_ones
• std_specs::bits::axiom_u8_trailing_zeros
• std_specs::bits::group_bits_axioms
• std_specs::bits::u16_leading_ones
• std_specs::bits::u16_leading_zeros
• std_specs::bits::u16_trailing_ones
• std_specs::bits::u16_trailing_zeros
• std_specs::bits::u32_leading_ones
• std_specs::bits::u32_leading_zeros
• std_specs::bits::u32_trailing_ones
• std_specs::bits::u32_trailing_zeros
• std_specs::bits::u64_leading_ones
• std_specs::bits::u64_leading_zeros
• std_specs::bits::u64_trailing_ones
• std_specs::bits::u64_trailing_zeros
• std_specs::bits::u8_leading_ones
• std_specs::bits::u8_leading_zeros
• std_specs::bits::u8_trailing_ones
• std_specs::bits::u8_trailing_zeros
• std_specs::clone::_verus_external_fn_specification_29__60__32_bool_32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_30__60__32_char_32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_31__60__32__38__32__39_b_32_T_32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_32__60__32_Tracked_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_33__60__32_Ghost_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::control_flow::_verus_external_fn_specification_34_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_branch
• std_specs::control_flow::_verus_external_fn_specification_35_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_branch
• std_specs::control_flow::_verus_external_fn_specification_36_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_from__residual
• std_specs::control_flow::_verus_external_fn_specification_37_Result_32__58__58__32__60__32_T_44__32_F_32__62__32__58__58__32_from__residual
• std_specs::control_flow::group_control_flow_axioms
• std_specs::control_flow::spec_from
• std_specs::control_flow::spec_from_blanket_identity
• std_specs::core::_verus_external_fn_specification_38_T_32__58__58__32_into
• std_specs::core::_verus_external_fn_specification_39_core_32__58__58__32_mem_32__58__58__32_swap_32__58__58__32__60__32_T_32__62_
• std_specs::core::_verus_external_fn_specification_40_I_32__58__58__32_into__iter
• std_specs::core::_verus_external_fn_specification_41_core_32__58__58__32_intrinsics_32__58__58__32_likely
• std_specs::core::_verus_external_fn_specification_42_core_32__58__58__32_intrinsics_32__58__58__32_unlikely
• std_specs::core::_verus_external_fn_specification_43_bool_32__58__58__32_then
• std_specs::core::_verus_external_fn_specification_44_core_32__58__58__32_hint_32__58__58__32_unreachable__unchecked
• std_specs::core::_verus_external_fn_specification_45__60__32_u16_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_46__60__32_u32_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_47__60__32_u64_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_48__60__32_usize_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_49__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_50__60__32_u32_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u16_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_51__60__32_u64_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u16_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_52__60__32_usize_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u16_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_53__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u16_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_54__60__32_u64_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u32_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_55__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u32_32__62__32__62__32__58__58__32_from
• std_specs::core::_verus_external_fn_specification_56__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u64_32__62__32__62__32__58__58__32_from
• std_specs::core::index_set
• std_specs::core::iter_into_iter_spec
• std_specs::hash::_verus_external_fn_specification_57_DefaultHasher_32__58__58__32_new
• std_specs::hash::_verus_external_fn_specification_58_DefaultHasher_32__58__58__32_write
• std_specs::hash::_verus_external_fn_specification_59_DefaultHasher_32__58__58__32_finish
• std_specs::hash::_verus_external_fn_specification_60_Keys_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next
• std_specs::hash::_verus_external_fn_specification_61_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_len
• std_specs::hash::_verus_external_fn_specification_62_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_new
• std_specs::hash::_verus_external_fn_specification_63_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_with__capacity
• std_specs::hash::_verus_external_fn_specification_64_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_44__32__62__32__58__58__32_reserve
• std_specs::hash::_verus_external_fn_specification_65_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_insert
• std_specs::hash::_verus_external_fn_specification_66_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_contains__key_32__58__58__32__60__32_Q_32__62_
• std_specs::hash::_verus_external_fn_specification_67_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_
• std_specs::hash::_verus_external_fn_specification_68_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_
• std_specs::hash::_verus_external_fn_specification_69_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_clear
• std_specs::hash::_verus_external_fn_specification_70_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_keys
• std_specs::hash::_verus_external_fn_specification_71_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next
• std_specs::hash::_verus_external_fn_specification_72_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_len
• std_specs::hash::_verus_external_fn_specification_73_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new
• std_specs::hash::_verus_external_fn_specification_74_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity
• std_specs::hash::_verus_external_fn_specification_75_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve
• std_specs::hash::_verus_external_fn_specification_76_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_insert
• std_specs::hash::_verus_external_fn_specification_77_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains
• std_specs::hash::_verus_external_fn_specification_78_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_
• std_specs::hash::_verus_external_fn_specification_79_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_
• std_specs::hash::_verus_external_fn_specification_80_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_clear
• std_specs::hash::_verus_external_fn_specification_81_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_iter
• std_specs::hash::axiom_bool_obeys_hash_table_key_model
• std_specs::hash::axiom_box_bool_obeys_hash_table_key_model
• std_specs::hash::axiom_box_integer_type_obeys_hash_table_key_model
• std_specs::hash::axiom_box_key_removed
• std_specs::hash::axiom_contains_box
• std_specs::hash::axiom_contains_deref_key
• std_specs::hash::axiom_deref_key_removed
• std_specs::hash::axiom_i128_obeys_hash_table_key_model
• std_specs::hash::axiom_i164_obeys_hash_table_key_model
• std_specs::hash::axiom_i16_obeys_hash_table_key_model
• std_specs::hash::axiom_i32_obeys_hash_table_key_model
• std_specs::hash::axiom_i8_obeys_hash_table_key_model
• std_specs::hash::axiom_isize_obeys_hash_table_key_model
• std_specs::hash::axiom_maps_box_key_to_value
• std_specs::hash::axiom_maps_deref_key_to_value
• std_specs::hash::axiom_random_state_builds_valid_hashers
• std_specs::hash::axiom_set_box_key_removed
• std_specs::hash::axiom_set_box_key_to_value
• std_specs::hash::axiom_set_contains_box
• std_specs::hash::axiom_set_contains_deref_key
• std_specs::hash::axiom_set_deref_key_removed
• std_specs::hash::axiom_set_deref_key_to_value
• std_specs::hash::axiom_spec_hash_map_len
• std_specs::hash::axiom_spec_hash_set_len
• std_specs::hash::axiom_u128_obeys_hash_table_key_model
• std_specs::hash::axiom_u16_obeys_hash_table_key_model
• std_specs::hash::axiom_u32_obeys_hash_table_key_model
• std_specs::hash::axiom_u64_obeys_hash_table_key_model
• std_specs::hash::axiom_u8_obeys_hash_table_key_model
• std_specs::hash::axiom_usize_obeys_hash_table_key_model
• std_specs::hash::borrowed_key_removed
• std_specs::hash::builds_valid_hashers
• std_specs::hash::contains_borrowed_key
• std_specs::hash::group_hash_axioms
• std_specs::hash::maps_borrowed_key_to_value
• std_specs::hash::obeys_key_model
• std_specs::hash::set_contains_borrowed_key
• std_specs::hash::sets_borrowed_key_to_key
• std_specs::hash::sets_differ_by_borrowed_key
• std_specs::hash::spec_hash_map_len
• std_specs::hash::spec_hash_set_len
• std_specs::num::_verus_external_fn_specification_208_u32_32__58__58__32_checked__rem
• std_specs::num::_verus_external_fn_specification_209_u32_32__58__58__32_checked__rem__euclid
• std_specs::num::_verus_external_fn_specification_210_i32_32__58__58__32_checked__div
• std_specs::num::_verus_external_fn_specification_211_i32_32__58__58__32_checked__div__euclid
• std_specs::num::_verus_external_fn_specification_212_i32_32__58__58__32_checked__rem
• std_specs::num::_verus_external_fn_specification_213_i32_32__58__58__32_checked__rem__euclid
• std_specs::option::_verus_external_fn_specification_214_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_is__some
• std_specs::option::_verus_external_fn_specification_215_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_is__none
• std_specs::option::_verus_external_fn_specification_216_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_as__ref
• std_specs::option::_verus_external_fn_specification_217_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_unwrap
• std_specs::option::_verus_external_fn_specification_218_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_unwrap__or
• std_specs::option::_verus_external_fn_specification_219_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_take
• std_specs::option::_verus_external_fn_specification_220_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_map
• std_specs::option::_verus_external_fn_specification_221__60__32_Option_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::option::_verus_external_fn_specification_222_Option_32__58__58__32_ok__or
• std_specs::option::is_none
• std_specs::option::is_some
• std_specs::option::spec_ok_or
• std_specs::option::spec_unwrap
• std_specs::option::spec_unwrap_or
• std_specs::range::_verus_external_fn_specification_223_Range_32__58__58__32__60__32_A_32__62__32__58__58__32_next
• std_specs::range::axiom_spec_range_next_i128
• std_specs::range::axiom_spec_range_next_i16
• std_specs::range::axiom_spec_range_next_i32
• std_specs::range::axiom_spec_range_next_i64
• std_specs::range::axiom_spec_range_next_i8
• std_specs::range::axiom_spec_range_next_isize
• std_specs::range::axiom_spec_range_next_u128
• std_specs::range::axiom_spec_range_next_u16
• std_specs::range::axiom_spec_range_next_u32
• std_specs::range::axiom_spec_range_next_u64
• std_specs::range::axiom_spec_range_next_u8
• std_specs::range::axiom_spec_range_next_usize
• std_specs::range::group_range_axioms
• std_specs::range::spec_range_next
• std_specs::result::_verus_external_fn_specification_224_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_is__ok
• std_specs::result::_verus_external_fn_specification_225_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_is__err
• std_specs::result::_verus_external_fn_specification_226_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_as__ref
• std_specs::result::_verus_external_fn_specification_227_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_unwrap
• std_specs::result::_verus_external_fn_specification_228_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_unwrap__err
• std_specs::result::_verus_external_fn_specification_229_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_map
• std_specs::result::_verus_external_fn_specification_230_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_map__err
• std_specs::result::_verus_external_fn_specification_231_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_ok
• std_specs::result::_verus_external_fn_specification_232_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_err
• std_specs::result::err
• std_specs::result::is_err
• std_specs::result::is_ok
• std_specs::result::ok
• std_specs::result::spec_unwrap
• std_specs::result::spec_unwrap_err
• std_specs::smart_ptrs::_verus_external_fn_specification_268__60__32__91_T_93__32__62__32__58__58__32_into__vec
• std_specs::smart_ptrs::_verus_external_fn_specification_269_Box_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_270_Rc_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_271_Arc_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_272__60__32_Box_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::smart_ptrs::_verus_external_fn_specification_273_Rc_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_try__unwrap
• std_specs::smart_ptrs::_verus_external_fn_specification_274_Rc_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_into__inner
• std_specs::vec::_verus_external_fn_specification_233_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_len
• std_specs::vec::_verus_external_fn_specification_234_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::vec::_verus_external_fn_specification_235_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
• std_specs::vec::_verus_external_fn_specification_236_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve
• std_specs::vec::_verus_external_fn_specification_237_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push
• std_specs::vec::_verus_external_fn_specification_238_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop
• std_specs::vec::_verus_external_fn_specification_239_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_append
• std_specs::vec::_verus_external_fn_specification_240_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_extend__from__slice
• std_specs::vec::_verus_external_fn_specification_241_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_insert
• std_specs::vec::_verus_external_fn_specification_242_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_remove
• std_specs::vec::_verus_external_fn_specification_243_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_clear
• std_specs::vec::_verus_external_fn_specification_244_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_as__slice
• std_specs::vec::_verus_external_fn_specification_245_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_split__off
• std_specs::vec::_verus_external_fn_specification_246__60__32_Vec_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::vec::_verus_external_fn_specification_247_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate
• std_specs::vec::_verus_external_fn_specification_248_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize
• std_specs::vec::axiom_spec_len
• std_specs::vec::axiom_vec_index_decreases
• std_specs::vec::group_vec_axioms
• std_specs::vec::spec_vec_len
• std_specs::vec::vec_clone_deep_view_proof
• std_specs::vec::vec_clone_trigger
• std_specs::vec::vec_index
• std_specs::vecdeque::_verus_external_fn_specification_249_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_index
• std_specs::vecdeque::_verus_external_fn_specification_250_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_len
• std_specs::vecdeque::_verus_external_fn_specification_251_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::vecdeque::_verus_external_fn_specification_252_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
• std_specs::vecdeque::_verus_external_fn_specification_253_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve
• std_specs::vecdeque::_verus_external_fn_specification_254_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push__back
• std_specs::vecdeque::_verus_external_fn_specification_255_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push__front
• std_specs::vecdeque::_verus_external_fn_specification_256_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop__back
• std_specs::vecdeque::_verus_external_fn_specification_257_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop__front
• std_specs::vecdeque::_verus_external_fn_specification_258_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_append
• std_specs::vecdeque::_verus_external_fn_specification_259_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_insert
• std_specs::vecdeque::_verus_external_fn_specification_260_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_remove
• std_specs::vecdeque::_verus_external_fn_specification_261_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_clear
• std_specs::vecdeque::_verus_external_fn_specification_262_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_split__off
• std_specs::vecdeque::_verus_external_fn_specification_263__60__32_VecDeque_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::vecdeque::_verus_external_fn_specification_264_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate
• std_specs::vecdeque::_verus_external_fn_specification_265_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize
• std_specs::vecdeque::_verus_external_fn_specification_266_Iter_32__58__58__32__60__32__39_a_44__32_T_32__62__32__58__58__32_next
• std_specs::vecdeque::_verus_external_fn_specification_267_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_iter
• std_specs::vecdeque::axiom_spec_iter
• std_specs::vecdeque::axiom_spec_len
• std_specs::vecdeque::axiom_vec_dequeue_index_decreases
• std_specs::vecdeque::group_vec_dequeue_axioms
• std_specs::vecdeque::spec_iter
• std_specs::vecdeque::spec_vec_dequeue_len
• std_specs::vecdeque::vec_dequeue_clone_trigger
• storage_protocol::deposits
• storage_protocol::exchanges
• storage_protocol::exchanges_nondeterministic
• storage_protocol::guards
• storage_protocol::incl
• storage_protocol::set_op
• storage_protocol::updates
• storage_protocol::withdraws
• string::_verus_external_fn_specification_10_String_32__58__58__32_as__str
• string::_verus_external_fn_specification_11__60__32_String_32_as_32_Clone_32__62__32__58__58__32_clone
• string::_verus_external_fn_specification_12__60__32_String_32_as_32_PartialEq_32__62__32__58__58__32_eq
• string::_verus_external_fn_specification_7_str_32__58__58__32_is__ascii
• string::_verus_external_fn_specification_8_str_32__58__58__32_to__string
• string::_verus_external_fn_specification_9_String_32__58__58__32_is__ascii
• string::axiom_str_literal_get_char
• string::axiom_str_literal_is_ascii
• string::axiom_str_literal_len
• string::group_string_axioms
• string::new_strlit_spec
• string::str_slice_is_ascii
• string::string_is_ascii
• thread::ghost_thread_id
• thread::spawn
• thread::thread_id
• tokens::bool_value_eq_option_token
• tokens::bool_value_le_option_token
• tokens::option_value_eq_option_token
• tokens::option_value_le_option_token

Type Aliases

• atomic::AtomicCellId
• pcm::Loc
• 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