List of all items

Structs

• 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
• prelude::FnSpec
• prelude::Ghost
• prelude::NoCopy
• prelude::SpecChain
• prelude::Tracked
• prelude::int
• prelude::nat
• proph::Prophecy
• ptr::Dealloc
• ptr::DeallocData
• ptr::DeallocRaw
• ptr::DeallocRawData
• ptr::PPtr
• ptr::PointsTo
• ptr::PointsToData
• ptr::PointsToRaw
• 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_exc_token_data
• rwlock::RwLockToks::flag_rc
• rwlock::RwLockToks::flag_rc_token_data
• rwlock::RwLockToks::pending_reader
• rwlock::RwLockToks::pending_reader_token_data
• rwlock::RwLockToks::pending_writer
• rwlock::RwLockToks::pending_writer_token_data
• rwlock::RwLockToks::reader
• rwlock::RwLockToks::reader_token_data
• rwlock::RwLockToks::writer
• rwlock::RwLockToks::writer_token_data
• rwlock::WriteHandle
• seq::Seq
• set::Set
• shared::Dupe::Instance
• shared::Dupe::State
• shared::Shared
• simple_pptr::PPtr
• simple_pptr::PointsTo
• 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::ExRandomState
• std_specs::range::ExRange
• std_specs::range::RangeGhostIterator
• std_specs::vec::ExGlobal
• std_specs::vec::ExVec
• storage_protocol::StorageResource
• string::ExString
• thread::IsThread
• thread::JoinHandle
• thread::ThreadId

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::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::ExInteger
• 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::hash::DefaultHasherAdditionalSpecFns
• std_specs::hash::ExBuildHasher
• std_specs::hash::ExHasher
• std_specs::hash::HashMapAdditionalSpecFns
• std_specs::option::OptionAdditionalFns
• std_specs::range::StepSpec
• std_specs::result::ResultAdditionalSpecFns
• std_specs::vec::VecAdditionalSpecFns
• storage_protocol::Protocol
• string::StrSliceExecFns
• string::StringExecFns
• string::StringExecFnsIsAscii
• 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
• 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
• 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::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

Attribute Macros

• prelude::decreases
• prelude::ensures
• prelude::invariant
• prelude::invariant_except_break
• prelude::is_variant
• prelude::is_variant_no_deprecation_warning
• prelude::requires
• prelude::verus_enum_synthesize
• 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::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::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::ex_array_as_slice
• 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_implies
• compute::range_all_spec_rec
• function::fun_ext
• function::fun_ext_1
• function::fun_ext_2
• function::fun_ext_3
• function::fun_ext_4
• 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::align_of
• layout::align_of_as_usize
• layout::ex_align_of
• layout::ex_size_of
• layout::is_power_2
• layout::is_sized
• layout::layout_for_type_is_valid
• 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::lemma_disjoint_union_size
• map_lib::lemma_map_new_domain
• map_lib::lemma_map_new_values
• map_lib::lemma_map_properties
• 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::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::arbitrary
• pervasive::assert
• pervasive::assume
• pervasive::print_u64
• pervasive::proof_from_false
• pervasive::runtime_assert
• pervasive::spec_affirm
• 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::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
• ptr::group_ptr_axioms
• ptr::points_to_height_axiom
• 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::ex_ptr_null
• raw_ptr::ex_ptr_null_mut
• 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_seq_lib_default
• 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
• 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::group_set_axioms
• set_lib::axiom_is_empty
• set_lib::group_set_lib_axioms
• 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_intersect_again1
• set_lib::lemma_set_intersect_again2
• set_lib::lemma_set_intersect_union_lens
• set_lib::lemma_set_properties
• set_lib::lemma_set_union_again1
• set_lib::lemma_set_union_again2
• set_lib::lemma_subset_equality
• set_lib::set_int_range
• shared::Dupe::show::initialize_one
• shared::Dupe::take_step::initialize_one
• slice::axiom_spec_len
• slice::group_slice_axioms
• slice::slice_index_get
• slice::slice_len
• slice::slice_subrange
• slice::slice_to_vec
• slice::spec_slice_len
• 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::ex_u16_leading_ones
• std_specs::bits::ex_u16_leading_zeros
• std_specs::bits::ex_u16_trailing_ones
• std_specs::bits::ex_u16_trailing_zeros
• std_specs::bits::ex_u32_leading_ones
• std_specs::bits::ex_u32_leading_zeros
• std_specs::bits::ex_u32_trailing_ones
• std_specs::bits::ex_u32_trailing_zeros
• std_specs::bits::ex_u64_leading_ones
• std_specs::bits::ex_u64_leading_zeros
• std_specs::bits::ex_u64_trailing_ones
• std_specs::bits::ex_u64_trailing_zeros
• std_specs::bits::ex_u8_leading_ones
• std_specs::bits::ex_u8_leading_zeros
• std_specs::bits::ex_u8_trailing_ones
• std_specs::bits::ex_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::ex_bool_clone
• std_specs::clone::ex_char_clone
• std_specs::clone::ex_ghost_clone
• std_specs::clone::ex_ref_clone
• std_specs::clone::ex_tracked_clone
• std_specs::control_flow::ex_option_branch
• std_specs::control_flow::ex_option_from_residual
• std_specs::control_flow::ex_result_branch
• std_specs::control_flow::ex_result_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::ex_intrinsics_likely
• std_specs::core::ex_intrinsics_unlikely
• std_specs::core::ex_iter_into_iter
• std_specs::core::ex_swap
• std_specs::core::iter_into_iter_spec
• 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_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::borrowed_key_removed
• std_specs::hash::builds_valid_hashers
• std_specs::hash::contains_borrowed_key
• std_specs::hash::ex_default_hasher_finish
• std_specs::hash::ex_default_hasher_new
• std_specs::hash::ex_default_hasher_write
• std_specs::hash::ex_hash_contains_key
• std_specs::hash::ex_hash_map_clear
• std_specs::hash::ex_hash_map_get
• std_specs::hash::ex_hash_map_insert
• std_specs::hash::ex_hash_map_len
• std_specs::hash::ex_hash_map_new
• std_specs::hash::ex_hash_map_remove
• std_specs::hash::ex_hash_map_reserve
• std_specs::hash::ex_hash_map_with_capacity
• std_specs::hash::ex_hash_set_clear
• std_specs::hash::ex_hash_set_contains
• std_specs::hash::ex_hash_set_get
• std_specs::hash::ex_hash_set_insert
• std_specs::hash::ex_hash_set_len
• std_specs::hash::ex_hash_set_new
• std_specs::hash::ex_hash_set_remove
• std_specs::hash::ex_hash_set_reserve
• std_specs::hash::ex_hash_set_with_capacity
• 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::ex_i32_checked_div
• std_specs::num::ex_i32_checked_div_euclid
• std_specs::num::ex_i32_checked_rem
• std_specs::num::ex_i32_checked_rem_euclid
• std_specs::num::ex_u32_checked_rem
• std_specs::num::ex_u32_checked_rem_euclid
• std_specs::option::as_ref
• std_specs::option::ex_map
• std_specs::option::ex_option_clone
• std_specs::option::ex_option_is_none
• std_specs::option::ex_option_is_some
• std_specs::option::is_none
• std_specs::option::is_some
• std_specs::option::spec_unwrap
• std_specs::option::spec_unwrap_or
• std_specs::option::take
• std_specs::option::unwrap
• std_specs::option::unwrap_or
• 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::ex_range_next
• std_specs::range::group_range_axioms
• std_specs::range::spec_range_next
• std_specs::result::as_ref
• std_specs::result::err
• std_specs::result::ex_result_err
• std_specs::result::ex_result_is_err
• std_specs::result::ex_result_is_ok
• std_specs::result::ex_result_ok
• std_specs::result::is_err
• std_specs::result::is_ok
• std_specs::result::map
• std_specs::result::ok
• std_specs::result::spec_unwrap
• std_specs::result::spec_unwrap_err
• std_specs::result::unwrap
• std_specs::result::unwrap_err
• std_specs::smart_ptrs::arc_new
• std_specs::smart_ptrs::box_clone
• std_specs::smart_ptrs::box_into_vec
• std_specs::smart_ptrs::box_new
• std_specs::smart_ptrs::rc_new
• std_specs::vec::axiom_spec_len
• std_specs::vec::axiom_vec_index_decreases
• std_specs::vec::ex_vec_append
• std_specs::vec::ex_vec_as_slice
• std_specs::vec::ex_vec_clear
• std_specs::vec::ex_vec_clone
• std_specs::vec::ex_vec_insert
• std_specs::vec::ex_vec_len
• std_specs::vec::ex_vec_new
• std_specs::vec::ex_vec_pop
• std_specs::vec::ex_vec_push
• std_specs::vec::ex_vec_remove
• std_specs::vec::ex_vec_reserve
• std_specs::vec::ex_vec_split_off
• std_specs::vec::ex_vec_truncate
• std_specs::vec::ex_vec_with_capacity
• 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
• 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::axiom_str_literal_get_char
• string::axiom_str_literal_is_ascii
• string::axiom_str_literal_len
• string::ex_str_slice_is_ascii
• string::ex_str_to_string
• string::ex_string_as_str
• string::ex_string_clone
• string::ex_string_eq
• string::ex_string_is_ascii
• string::group_string_axioms
• string::new_strlit
• string::new_strlit_spec
• string::str_slice_is_ascii
• string::string_is_ascii
• thread::ghost_thread_id
• thread::spawn
• thread::thread_id

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
• string::StrSlice