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
• function::ExFnProof
• hash_map::HashMapWithView
• hash_map::StringHashMap
• hash_set::HashSetWithView
• hash_set::StringHashSet
• invariant::AtomicInvariant
• invariant::LocalInvariant
• map::Map
• multiset::Multiset
• pcm::Resource
• prelude::DummyCapture
• prelude::FnProof
• prelude::FnSpec
• prelude::Ghost
• prelude::NoCopy
• prelude::ProofFnConfirm
• prelude::SpecChain
• prelude::Tracked
• prelude::int
• prelude::nat
• proph::Prophecy
• raw_ptr::Dealloc
• raw_ptr::DeallocData
• 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::borrow::ExCow
• std_specs::control_flow::ExControlFlow
• std_specs::control_flow::ExInfallible
• std_specs::core::ExAssertParamIsClone
• std_specs::core::ExDuration
• std_specs::core::ExManuallyDrop
• std_specs::core::ExOption
• std_specs::core::ExOrdering
• std_specs::core::ExPhantomData
• std_specs::core::ExResult
• std_specs::hash::ExDefaultHasher
• std_specs::hash::ExHashMap
• std_specs::hash::ExHashSet
• std_specs::hash::ExKeys
• std_specs::hash::ExMapIter
• std_specs::hash::ExRandomState
• std_specs::hash::ExSetIter
• std_specs::hash::ExValues
• std_specs::hash::KeysGhostIterator
• std_specs::hash::MapIterGhostIterator
• std_specs::hash::SetIterGhostIterator
• std_specs::hash::ValuesGhostIterator
• std_specs::range::ExRange
• std_specs::range::RangeGhostIterator
• std_specs::slice::ExIter
• std_specs::slice::IterGhostIterator
• std_specs::vec::ExIntoIter
• std_specs::vec::ExVec
• std_specs::vec::IntoIterGhostIterator
• std_specs::vecdeque::ExIter
• std_specs::vecdeque::ExVecDeque
• std_specs::vecdeque::IterGhostIterator
• storage_protocol::StorageResource
• string::CharsGhostIterator
• string::ExChars
• string::ExString
• thread::IsThread
• thread::JoinHandle
• thread::ThreadId
• tokens::InstanceId
• tokens::MapToken
• tokens::MultisetToken
• tokens::SetToken
• tokens::frac::Empty
• tokens::frac::Frac
• tokens::frac::FracGhost
• tokens::frac::GhostVar
• tokens::frac::GhostVarAuth
• tokens::map::GhostMapAuth
• tokens::map::GhostSubmap
• tokens::seq::GhostSeqAuth
• tokens::seq::GhostSubseq

Enums

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

Traits

• array::ArrayAdditionalExecFns
• array::ArrayAdditionalSpecFns
• atomic_ghost::AtomicInvariantPredicate
• compute::RangeAll
• float::FloatBitsProperties
• function::ExProofFn
• function::ExProofFnMut
• function::ExProofFnOnce
• function::ExProofFnReqEns
• function::ExProofFnReqEnsAssoc
• function::ExProofFnSpecification
• invariant::InvariantPredicate
• logatom::MutLinearizer
• logatom::MutOperation
• logatom::ReadLinearizer
• logatom::ReadOperation
• pcm::PCM
• pervasive::FnWithRequiresEnsures
• pervasive::ForLoopGhostIterator
• pervasive::ForLoopGhostIteratorNew
• pervasive::VecAdditionalExecFns
• prelude::Boolean
• prelude::Integer
• prelude::ProofFn
• prelude::ProofFnMut
• prelude::ProofFnOnce
• prelude::ProofFnReqEns
• prelude::ProofFnReqEnsDef
• 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::cmp::ExEq
• std_specs::cmp::ExOrd
• std_specs::cmp::ExPartialEq
• std_specs::cmp::ExPartialOrd
• std_specs::cmp::OrdSpec
• std_specs::cmp::OrdSpecImpl
• std_specs::cmp::PartialEqIs
• std_specs::cmp::PartialEqSpec
• std_specs::cmp::PartialEqSpecImpl
• std_specs::cmp::PartialOrdIs
• std_specs::cmp::PartialOrdSpec
• std_specs::cmp::PartialOrdSpecImpl
• std_specs::core::ExAllocator
• std_specs::core::ExBorrow
• std_specs::core::ExDebug
• std_specs::core::ExDeref
• std_specs::core::ExDisplay
• 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::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::KeysAdditionalSpecFns
• std_specs::hash::MapIterAdditionalSpecFns
• std_specs::hash::SetIterAdditionalSpecFns
• std_specs::hash::ValuesAdditionalSpecFns
• std_specs::ops::AddSpec
• std_specs::ops::AddSpecImpl
• std_specs::ops::BitAndSpec
• std_specs::ops::BitAndSpecImpl
• std_specs::ops::BitOrSpec
• std_specs::ops::BitOrSpecImpl
• std_specs::ops::BitXorSpec
• std_specs::ops::BitXorSpecImpl
• std_specs::ops::DivSpec
• std_specs::ops::DivSpecImpl
• std_specs::ops::ExAdd
• std_specs::ops::ExBitAnd
• std_specs::ops::ExBitOr
• std_specs::ops::ExBitXor
• std_specs::ops::ExDiv
• std_specs::ops::ExMul
• std_specs::ops::ExNeg
• std_specs::ops::ExNot
• std_specs::ops::ExRem
• std_specs::ops::ExShl
• std_specs::ops::ExShr
• std_specs::ops::ExSub
• std_specs::ops::MulSpec
• std_specs::ops::MulSpecImpl
• std_specs::ops::NegSpec
• std_specs::ops::NegSpecImpl
• std_specs::ops::NotSpec
• std_specs::ops::NotSpecImpl
• std_specs::ops::RemSpec
• std_specs::ops::RemSpecImpl
• std_specs::ops::ShlSpec
• std_specs::ops::ShlSpecImpl
• std_specs::ops::ShrSpec
• std_specs::ops::ShrSpecImpl
• std_specs::ops::SubSpec
• std_specs::ops::SubSpecImpl
• std_specs::option::OptionAdditionalFns
• std_specs::range::StepSpec
• std_specs::result::ResultAdditionalSpecFns
• std_specs::vec::VecAdditionalSpecFns
• 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::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
• 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
• 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::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_subtracts
• 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_array_ext_equal
• 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_u128_shr_is_div
• bits::lemma_u16_low_bits_mask_is_mod
• bits::lemma_u16_mul_pow2_le_max_iff_max_shr
• 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_mul_pow2_le_max_iff_max_shr
• 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_mul_pow2_le_max_iff_max_shr
• 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_mul_pow2_le_max_iff_max_shr
• 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::spec_u64_to_le_bytes_open
• bytes::spec_u64_to_le_bytes_to_open
• 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
• function::group_function_axioms
• function::proof_fn_as_req_ens
• 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
• laws_cmp::group_laws_cmp
• laws_cmp::lemma_option_obeys_cmp_spec
• laws_cmp::obeys_cmp_ord
• laws_cmp::obeys_cmp_partial_ord
• laws_cmp::obeys_cmp_spec
• laws_cmp::obeys_partial_cmp_spec_properties
• laws_eq::axiom_structural_obeys_concrete_eq
• laws_eq::group_laws_eq
• laws_eq::lemma_option_obeys_concrete_eq
• laws_eq::lemma_option_obeys_deep_eq
• laws_eq::lemma_option_obeys_eq_spec
• laws_eq::lemma_option_obeys_view_eq
• laws_eq::obeys_concrete_eq
• laws_eq::obeys_deep_eq
• laws_eq::obeys_eq_spec
• laws_eq::obeys_eq_spec_properties
• laws_eq::obeys_view_eq
• 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_extra
• 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::constrain_type
• prelude::decreases
• prelude::decreases_by
• prelude::decreases_when
• prelude::default_ensures
• prelude::dummy_capture_consume
• prelude::dummy_capture_new
• prelude::ensures
• prelude::equal
• prelude::erased_ghost_value
• prelude::exists
• prelude::ext_equal
• prelude::ext_equal_deep
• prelude::extra_dependency
• prelude::f32_to_bits
• prelude::f64_to_bits
• prelude::forall
• prelude::get_union_field
• prelude::get_variant_field
• prelude::ghost_exec
• prelude::global_size_of
• prelude::has_resolved
• 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::mut_ref_current
• prelude::mut_ref_future
• 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::resolve
• 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__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq
• raw_ptr::_verus_external_fn_specification_4__60__32__42__32_const_32_T_32_as_32_PartialEq_32__60__32__42__32_const_32_T_32__62__32__62__32__58__58__32_eq
• raw_ptr::_verus_external_fn_specification_5_core_32__58__58__32_ptr_32__58__58__32_null
• raw_ptr::_verus_external_fn_specification_6_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::ptrs_mut_eq_sized
• 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_foldl
• 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_exactly_one_view
• seq_lib::lemma_filter_view_commute
• seq_lib::lemma_flatten_alt_concat
• seq_lib::lemma_flatten_concat
• seq_lib::lemma_fold_left_permutation
• 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::lemma_update_is_remove_insert
• seq_lib::seq_to_set_distributes_over_add
• 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_insert
• seq_lib::to_multiset_len
• seq_lib::to_multiset_remove
• seq_lib::to_multiset_update
• set::axiom_mk_map_domain
• set::axiom_mk_map_index
• set::axiom_set_choose_infinite
• 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_sets_eq_iff_injective_map_eq
• 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_7__60__32__91_T_93__32__62__32__58__58__32_len
• slice::_verus_external_fn_specification_8__60__32__91_T_93__32__62__32__58__58__32_get_32__58__58__32__60__32_I_32__62_
• slice::axiom_slice_ext_equal
• 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::alloc::_verus_external_fn_specification_18_alloc_32__58__58__32_boxed_32__58__58__32_box__new
• std_specs::bits::_verus_external_fn_specification_19_u8_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_20_u8_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_21_u8_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_22_u8_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_23_u16_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_24_u16_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_25_u16_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_26_u16_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_27_u32_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_28_u32_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_29_u32_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_30_u32_32__58__58__32_leading__ones
• std_specs::bits::_verus_external_fn_specification_31_u64_32__58__58__32_trailing__zeros
• std_specs::bits::_verus_external_fn_specification_32_u64_32__58__58__32_trailing__ones
• std_specs::bits::_verus_external_fn_specification_33_u64_32__58__58__32_leading__zeros
• std_specs::bits::_verus_external_fn_specification_34_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_35__60__32_bool_32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_36__60__32_char_32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::clone::_verus_external_fn_specification_37__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_38__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_39__60__32_Ghost_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::cmp::_verus_external_fn_specification_40__60__32_bool_32_as_32_PartialEq_32__60__32_bool_32__62__32__62__32__58__58__32_eq
• std_specs::cmp::_verus_external_fn_specification_41__60__32_bool_32_as_32_PartialEq_32__60__32_bool_32__62__32__62__32__58__58__32_ne
• std_specs::cmp::_verus_external_fn_specification_42__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_eq
• std_specs::cmp::_verus_external_fn_specification_43__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_ne
• std_specs::cmp::_verus_external_fn_specification_44__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_partial__cmp
• std_specs::cmp::_verus_external_fn_specification_45__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_lt
• std_specs::cmp::_verus_external_fn_specification_46__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_le
• std_specs::cmp::_verus_external_fn_specification_47__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_gt
• std_specs::cmp::_verus_external_fn_specification_48__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_ge
• std_specs::cmp::_verus_external_fn_specification_49__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_eq
• std_specs::cmp::_verus_external_fn_specification_50__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_ne
• std_specs::cmp::_verus_external_fn_specification_51__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_partial__cmp
• std_specs::cmp::_verus_external_fn_specification_52__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_lt
• std_specs::cmp::_verus_external_fn_specification_53__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_le
• std_specs::cmp::_verus_external_fn_specification_54__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_gt
• std_specs::cmp::_verus_external_fn_specification_55__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_ge
• std_specs::cmp::eq_ensures
• std_specs::cmp::ge_ensures
• std_specs::cmp::gt_ensures
• std_specs::cmp::le_ensures
• std_specs::cmp::lt_ensures
• std_specs::cmp::ne_ensures
• std_specs::cmp::partial_cmp_ensures
• std_specs::control_flow::_verus_external_fn_specification_56_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_57_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_branch
• std_specs::control_flow::_verus_external_fn_specification_58_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_from__residual
• std_specs::control_flow::_verus_external_fn_specification_59_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_60_T_32__58__58__32_into
• std_specs::core::_verus_external_fn_specification_61_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_62_I_32__58__58__32_into__iter
• std_specs::core::_verus_external_fn_specification_63_core_32__58__58__32_intrinsics_32__58__58__32_likely
• std_specs::core::_verus_external_fn_specification_64_core_32__58__58__32_intrinsics_32__58__58__32_unlikely
• std_specs::core::_verus_external_fn_specification_65_bool_32__58__58__32_then
• std_specs::core::_verus_external_fn_specification_66__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_67__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_68__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_69__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_70__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_71__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_72__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_73__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_74__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_75__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_76__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_77__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_228_DefaultHasher_32__58__58__32_new
• std_specs::hash::_verus_external_fn_specification_229_DefaultHasher_32__58__58__32_write
• std_specs::hash::_verus_external_fn_specification_230_DefaultHasher_32__58__58__32_finish
• std_specs::hash::_verus_external_fn_specification_231_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_232_Values_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_233_hash__map_32__58__58__32_Iter_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_234_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_iter
• std_specs::hash::_verus_external_fn_specification_235_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_236_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_is__empty
• std_specs::hash::_verus_external_fn_specification_237__60__32_HashMap_32__58__58__32__60__32_K_44__32_V_44__32_S_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
• std_specs::hash::_verus_external_fn_specification_238_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_239_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_240_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_241_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_242_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_243_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_244_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_245_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_246_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_247_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_values
• std_specs::hash::_verus_external_fn_specification_248_hash__set_32__58__58__32_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_249_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_250_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_is__empty
• std_specs::hash::_verus_external_fn_specification_251_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new
• std_specs::hash::_verus_external_fn_specification_252_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity
• std_specs::hash::_verus_external_fn_specification_253_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_254_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_255_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_256_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_257_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_258_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_259_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_hashmap_decreases
• std_specs::hash::axiom_hashmap_deepview_borrow
• std_specs::hash::axiom_hashmap_view_finite_dom
• std_specs::hash::axiom_hashset_decreases
• 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_iter
• 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::hash_map_deep_view_impl
• std_specs::hash::lemma_hashmap_deepview_dom
• std_specs::hash::lemma_hashmap_deepview_properties
• std_specs::hash::lemma_hashmap_deepview_values
• 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_iter
• std_specs::hash::spec_hash_map_len
• std_specs::hash::spec_hash_set_len
• std_specs::num::_verus_external_fn_specification_488_u32_32__58__58__32_checked__rem
• std_specs::num::_verus_external_fn_specification_489_u32_32__58__58__32_checked__rem__euclid
• std_specs::num::_verus_external_fn_specification_490_i32_32__58__58__32_checked__div
• std_specs::num::_verus_external_fn_specification_491_i32_32__58__58__32_checked__div__euclid
• std_specs::num::_verus_external_fn_specification_492_i32_32__58__58__32_checked__rem
• std_specs::num::_verus_external_fn_specification_493_i32_32__58__58__32_checked__rem__euclid
• std_specs::ops::_verus_external_fn_specification_100__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_101__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_102__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_103__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_104__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_105__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_106__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_107__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_108__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_109__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_110__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_111__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_112__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_113__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_114__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_115__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_116__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_117__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_118__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_119__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_120__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_121__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_122__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_123__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_124__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_125__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_126__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_127__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_128__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_129__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_130__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_131__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_132__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_133__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_134__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_135__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_136__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_137__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_138__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_139__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_140__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_141__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_142__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_143__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_144__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_145__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_146__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_147__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_148__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_149__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_150__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_151__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_152__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_153__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_154__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_155__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_156__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem
• std_specs::ops::_verus_external_fn_specification_157__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_158__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_159__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_160__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_161__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_162__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_163__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_164__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_165__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_166__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_167__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_168__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand
• std_specs::ops::_verus_external_fn_specification_169__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_170__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_171__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_172__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_173__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_174__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_175__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_176__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_177__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_178__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_179__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_180__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor
• std_specs::ops::_verus_external_fn_specification_181__60__32_bool_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_182__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_183__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_184__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_185__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_186__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_187__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_188__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_189__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_190__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_191__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_192__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_193__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor
• std_specs::ops::_verus_external_fn_specification_194__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_195__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_196__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_197__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_198__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_199__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_200__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_201__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_202__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_203__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_204__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_205__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl
• std_specs::ops::_verus_external_fn_specification_206__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_207__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_208__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_209__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_210__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_211__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_212__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_213__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_214__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_215__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_216__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_217__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr
• std_specs::ops::_verus_external_fn_specification_218__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_219__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_220__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_221__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_222__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_223__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_224__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_225__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub
• std_specs::ops::_verus_external_fn_specification_226__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul
• std_specs::ops::_verus_external_fn_specification_227__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div
• std_specs::ops::_verus_external_fn_specification_78__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_79__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_80__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_81__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_82__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_83__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg
• std_specs::ops::_verus_external_fn_specification_84__60__32_bool_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_85__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_86__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_87__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_88__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_89__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_90__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_91__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_92__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_93__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_94__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_95__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_96__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not
• std_specs::ops::_verus_external_fn_specification_97__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_98__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::_verus_external_fn_specification_99__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add
• std_specs::ops::add_ensures
• std_specs::ops::div_ensures
• std_specs::ops::mul_ensures
• std_specs::ops::neg_ensures
• std_specs::ops::sub_ensures
• std_specs::option::_verus_external_fn_specification_494_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_is__some
• std_specs::option::_verus_external_fn_specification_495_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_is__none
• std_specs::option::_verus_external_fn_specification_496_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_as__ref
• std_specs::option::_verus_external_fn_specification_497_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_unwrap
• std_specs::option::_verus_external_fn_specification_498_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_unwrap__or
• std_specs::option::_verus_external_fn_specification_499_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_expect
• std_specs::option::_verus_external_fn_specification_500_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_take
• std_specs::option::_verus_external_fn_specification_501_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_map
• std_specs::option::_verus_external_fn_specification_502__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_503__60__32_Option_32__60__32_T_32__62__32_as_32_PartialEq_32__62__32__58__58__32_eq
• std_specs::option::_verus_external_fn_specification_504__60__32_Option_32__60__32_T_32__62__32_as_32_PartialOrd_32__62__32__58__58__32_partial__cmp
• std_specs::option::_verus_external_fn_specification_505__60__32_Option_32__60__32_T_32__62__32_as_32_Ord_32__62__32__58__58__32_cmp
• std_specs::option::_verus_external_fn_specification_506_Option_32__58__58__32_ok__or
• std_specs::option::is_none
• std_specs::option::is_some
• std_specs::option::spec_expect
• std_specs::option::spec_ok_or
• std_specs::option::spec_unwrap
• std_specs::option::spec_unwrap_or
• std_specs::range::_verus_external_fn_specification_507_Range_32__58__58__32__60__32_A_32__62__32__58__58__32_next
• std_specs::range::_verus_external_fn_specification_508_Range_32__58__58__32__60__32_Idx_32__62__32__58__58__32_contains
• 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_509_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_510_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_511_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_512_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_513_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_514_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__32_expect
• std_specs::result::_verus_external_fn_specification_515_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_516_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_517_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_518_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_expect
• std_specs::result::spec_unwrap
• std_specs::result::spec_unwrap_err
• std_specs::slice::_verus_external_fn_specification_519_core_32__58__58__32_hint_32__58__58__32_unreachable__unchecked
• std_specs::slice::_verus_external_fn_specification_520_Iter_32__58__58__32__60__32__39_a_44__32_T_32__62__32__58__58__32_next
• std_specs::slice::_verus_external_fn_specification_521__60__32__91_T_93__32__62__32__58__58__32_iter
• std_specs::slice::axiom_spec_slice_iter
• std_specs::slice::group_slice_axioms
• std_specs::slice::spec_slice_iter
• std_specs::smart_ptrs::_verus_external_fn_specification_561__60__32__91_T_93__32__62__32__58__58__32_into__vec
• std_specs::smart_ptrs::_verus_external_fn_specification_562_Box_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_563_Rc_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_564_Arc_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::smart_ptrs::_verus_external_fn_specification_565__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_566_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_567_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_522_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_523_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::vec::_verus_external_fn_specification_524_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
• std_specs::vec::_verus_external_fn_specification_525_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_526_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_527_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_528_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_529_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_530_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_swap__remove
• std_specs::vec::_verus_external_fn_specification_531_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_532_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_533_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_534_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_535__60__32_Vec_32__60__32_T_44__32_A_32__62__32_as_32_core_32__58__58__32_ops_32__58__58__32_Deref_32__62__32__58__58__32_deref
• std_specs::vec::_verus_external_fn_specification_536_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_537__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_538_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_539_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize
• std_specs::vec::_verus_external_fn_specification_540_IntoIter_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_next
• std_specs::vec::_verus_external_fn_specification_541_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_into__iter
• std_specs::vec::axiom_spec_into_iter
• std_specs::vec::axiom_spec_len
• std_specs::vec::axiom_vec_index_decreases
• std_specs::vec::group_vec_axioms
• std_specs::vec::spec_into_iter
• 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_542_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_543_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_544_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_new
• std_specs::vecdeque::_verus_external_fn_specification_545_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
• std_specs::vecdeque::_verus_external_fn_specification_546_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_547_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_548_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_549_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_550_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_551_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_552_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_553_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_554_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_555_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_556__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_557_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_558_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_559_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_560_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_str_32__58__58__32_to__owned
• string::_verus_external_fn_specification_11__60__32_T_32_as_32_ToString_32__62__32__58__58__32_to__string
• string::_verus_external_fn_specification_12_String_32__58__58__32_is__ascii
• string::_verus_external_fn_specification_13_String_32__58__58__32_as__str
• string::_verus_external_fn_specification_14__60__32_String_32_as_32_Clone_32__62__32__58__58__32_clone
• string::_verus_external_fn_specification_15__60__32_String_32_as_32_PartialEq_32__62__32__58__58__32_eq
• string::_verus_external_fn_specification_16_str_32__58__58__32_chars
• string::_verus_external_fn_specification_17_Chars_32__58__58__32__60__32__39_a_32__62__32__58__58__32_next
• string::_verus_external_fn_specification_9_str_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
• string::to_string_from_display_ensures
• string::to_string_from_display_ensures_for_str
• 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
• tokens::seq::seq_to_map

Type Aliases

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

Constants

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