List of all items

Structs

• array_ptr::ArrayPtr
• array_ptr::PointsTo
• array_ptr::PointsToArray
• array_ptr::PointsToArrayData
• bit_mapping::BitMapping
• cast_ptr::PointsTo
• cast_ptr::ReprPtr
• external::nonnull::ExNonNull
• external::smart_ptr::ArcPointsTo
• external::smart_ptr::BoxPointsTo
• ghost_tree::Node
• ghost_tree::Tree
• ghost_tree::TreePath
• raw_ptr_extra::PointsTowithDealloc
• resource::storage::frac::FracStorage
• resource::storage::hybrid_product::HybridProduct
• state_machine::action::Action
• state_machine::state_machine::NetworkStateMachine
• state_machine::state_machine::StateMachine
• temporal_logic::defs::ActionPred
• temporal_logic::defs::Execution
• temporal_logic::defs::StatePred
• temporal_logic::defs::TempPred
• undroppable::NeverDrop

Enums

• external::smart_ptr::SmartPtrPointsTo
• resource::pcm::agree::AgreeR
• resource::pcm::count::CountR
• resource::pcm::csum::CsumR
• resource::pcm::excl::ExclR
• resource::pcm::frac::FracR
• resource::storage::frac::FracP
• state_machine::action::ActionResult

Traits

• bit_mapping::MapBackward
• bit_mapping::MapForwardTrait
• bit_mapping::MapInvertBackward
• bit_mapping::MapInvertForwardTrait
• cast_ptr::Repr
• external::deref::DerefSpec
• ghost_tree::TreeNodeValue
• ownership::Inv
• ownership::InvView
• ownership::ModelOf
• ownership::OwnerOf
• undroppable::Undroppable

Macros

• always_and_equality_n
• always_and_equality_n_internal
• always_lift_state_and_equality_n
• always_lift_state_and_equality_n_internal
• always_lift_state_weaken_n
• always_lift_state_weaken_n_internal
• bit_mapping::bm
• bit_mapping::bms
• bit_mapping::bms_as
• bit_mapping::decl_bms_const
• bm
• bms
• bms_as
• borrow_field
• combine_spec_entails_always_n
• combine_spec_entails_always_n_internal
• decl_bms_const
• entails_always_and_n
• entails_always_and_n_internal
• entails_always_lift_state_and_n
• entails_always_lift_state_and_n_internal
• entails_and_n
• entails_and_n_internal
• extern_const
• extern_const::extern_const
• implies_new_invariant_n
• implies_new_invariant_n_internal
• invariant_n
• invariant_n_internal
• leads_to_always_combine_n
• leads_to_always_combine_n_internal
• leads_to_always_combine_n_with_equality
• leads_to_always_combine_n_with_equality_internal
• leads_to_trans_n
• leads_to_trans_n_internal
• or_leads_to_combine_and_equality2
• or_leads_to_combine_n
• or_leads_to_combine_n_internal
• ptr_extra::borrow_field
• ptr_extra::update_field
• stable_and_always_n
• stable_and_always_n_internal
• stable_and_n
• stable_and_n_internal
• state_pred_and
• temp_pred_and
• temp_pred_and_internal
• temporal_logic::rules::always_and_equality_n
• temporal_logic::rules::always_and_equality_n_internal
• temporal_logic::rules::always_lift_state_and_equality_n
• temporal_logic::rules::always_lift_state_and_equality_n_internal
• temporal_logic::rules::always_lift_state_weaken_n
• temporal_logic::rules::always_lift_state_weaken_n_internal
• temporal_logic::rules::combine_spec_entails_always_n
• temporal_logic::rules::combine_spec_entails_always_n_internal
• temporal_logic::rules::entails_always_and_n
• temporal_logic::rules::entails_always_and_n_internal
• temporal_logic::rules::entails_always_lift_state_and_n
• temporal_logic::rules::entails_always_lift_state_and_n_internal
• temporal_logic::rules::entails_and_n
• temporal_logic::rules::entails_and_n_internal
• temporal_logic::rules::implies_new_invariant_n
• temporal_logic::rules::implies_new_invariant_n_internal
• temporal_logic::rules::invariant_n
• temporal_logic::rules::invariant_n_internal
• temporal_logic::rules::leads_to_always_combine_n
• temporal_logic::rules::leads_to_always_combine_n_internal
• temporal_logic::rules::leads_to_always_combine_n_with_equality
• temporal_logic::rules::leads_to_always_combine_n_with_equality_internal
• temporal_logic::rules::leads_to_trans_n
• temporal_logic::rules::leads_to_trans_n_internal
• temporal_logic::rules::or_leads_to_combine_and_equality2
• temporal_logic::rules::or_leads_to_combine_n
• temporal_logic::rules::or_leads_to_combine_n_internal
• temporal_logic::rules::stable_and_always_n
• temporal_logic::rules::stable_and_always_n_internal
• temporal_logic::rules::stable_and_n
• temporal_logic::rules::stable_and_n_internal
• temporal_logic::rules::state_pred_and
• temporal_logic::rules::temp_pred_and
• temporal_logic::rules::temp_pred_and_internal
• temporal_logic::rules::wf1_by_borrowing_inv_n
• update_field
• wf1_by_borrowing_inv_n

Functions

• arithmetic::lemma_nat_align_down_sound
• arithmetic::lemma_nat_align_up_sound
• arithmetic::nat_align_down
• arithmetic::nat_align_up
• array_ptr::axiom_mem_contents_unwrap_init_correctness
• array_ptr::axiom_mem_contents_unwrap_uninit_correctness
• array_ptr::axiom_mem_contents_wrap_correctness
• array_ptr::is_mem_contents_all_init
• array_ptr::is_mem_contents_all_uninit
• array_ptr::layout_for_array_is_valid
• array_ptr::mem_contents_unwrap
• array_ptr::mem_contents_wrap
• array_ptr::ptr_mut_fill
• array_ptr::ptr_mut_read_all
• array_ptr::ptr_mut_read_at
• array_ptr::ptr_mut_write_at
• array_ptr::ptr_ref
• array_ptr::ptr_ref_at
• auxiliary::arbitrary_cell_pointsto
• external::_verus_external_fn_specification_8_core_32__58__58__32_hint_32__58__58__32_spin__loop
• external::deref::arc_deref_spec
• external::deref::box_deref_spec
• external::deref::group_deref_spec
• external::deref::rc_deref_spec
• external::deref::ref_deref_spec
• external::ilog2::_verus_external_fn_specification_0_u8_32__58__58__32_ilog2
• external::ilog2::_verus_external_fn_specification_1_u16_32__58__58__32_ilog2
• external::ilog2::_verus_external_fn_specification_2_u32_32__58__58__32_ilog2
• external::ilog2::_verus_external_fn_specification_3_usize_32__58__58__32_ilog2
• external::ilog2::_verus_external_fn_specification_4_u64_32__58__58__32_ilog2
• external::ilog2::lemma2_to64_hi32
• external::ilog2::lemma_log2_to64
• external::ilog2::lemma_pow2_increases
• external::ilog2::lemma_pow2_is_pow2
• external::ilog2::lemma_pow2_is_pow2_to64
• external::ilog2::lemma_pow2_log2
• external::ilog2::lemma_u16_ilog2_ordered
• external::ilog2::lemma_u16_ilog2_to16
• external::ilog2::lemma_u16_is_pow2_is_ilog2_pow2
• external::ilog2::lemma_u16_log2_bounds
• external::ilog2::lemma_u16_pow2_ilog2
• external::ilog2::lemma_u16_pow2_ilog2_x
• external::ilog2::lemma_u32_ilog2_ordered
• external::ilog2::lemma_u32_ilog2_to32
• external::ilog2::lemma_u32_is_pow2_is_ilog2_pow2
• external::ilog2::lemma_u32_log2_bounds
• external::ilog2::lemma_u32_pow2_ilog2
• external::ilog2::lemma_u32_pow2_ilog2_x
• external::ilog2::lemma_u64_ilog2_ordered
• external::ilog2::lemma_u64_ilog2_to64
• external::ilog2::lemma_u64_is_pow2_is_ilog2_pow2
• external::ilog2::lemma_u64_log2_bounds
• external::ilog2::lemma_u64_pow2_ilog2
• external::ilog2::lemma_u64_pow2_ilog2_x
• external::ilog2::lemma_u8_ilog2_ordered
• external::ilog2::lemma_u8_ilog2_to8
• external::ilog2::lemma_u8_is_pow2_is_ilog2_pow2
• external::ilog2::lemma_u8_log2_bounds
• external::ilog2::lemma_u8_pow2_ilog2
• external::ilog2::lemma_u8_pow2_ilog2_x
• external::ilog2::lemma_usize_ilog2_ordered
• external::ilog2::lemma_usize_ilog2_to32
• external::ilog2::lemma_usize_is_pow2_is_ilog2_pow2
• external::ilog2::lemma_usize_log2_bounds
• external::ilog2::lemma_usize_pow2_ilog2
• external::ilog2::lemma_usize_pow2_ilog2_x
• external::ilog2::lemma_usize_pow2_shl_is_pow2
• external::ilog2::lemma_usize_shl_is_mul
• external::ilog2::u16_ilog2_spec
• external::ilog2::u32_ilog2_spec
• external::ilog2::u64_ilog2_spec
• external::ilog2::u8_ilog2_spec
• external::ilog2::usize_ilog2_spec
• external::manually_drop::manually_drop_deref_spec
• external::manually_drop::manually_drop_new_spec
• external::manually_drop::manually_drop_unwrap
• external::nonnull::_verus_external_fn_specification_5_NonNull_32__58__58__32_new__unchecked
• external::nonnull::_verus_external_fn_specification_6_NonNull_32__58__58__32_as__ptr
• external::nonnull::_verus_external_fn_specification_7_NonNull_32__58__58__32_dangling
• external::nonnull::axiom_nonull_from_ptr_mut_eq
• external::nonnull::axiom_nonull_is_nonnull
• external::nonnull::axiom_ptr_mut_from_nonull_eq
• external::nonnull::group_nonnull
• external::nonnull::nonnull_dangling_spec
• external::nonnull::nonnull_from_ptr_mut
• external::nonnull::ptr_mut_from_nonull
• external::smart_ptr::arc_from_raw
• external::smart_ptr::arc_into_raw
• external::smart_ptr::arc_pointer_spec
• external::smart_ptr::box_from_raw
• external::smart_ptr::box_into_raw
• external::smart_ptr::box_pointer_spec
• function_properties::bijective_on
• function_properties::construct_inverse
• function_properties::construct_left_inverse
• function_properties::inverse_on
• function_properties::left_inverse_on
• function_properties::lemma_bijective_cardinality
• function_properties::lemma_bijective_subset_still_bijective
• function_properties::lemma_construct_inverse_sound
• function_properties::lemma_construct_left_inverse_sound
• function_properties::lemma_injective_implies_injective_on
• function_properties::lemma_injective_map_cardinality
• function_properties::lemma_inverse_of_bijection_is_bijective
• function_properties::lemma_left_inverse_of_bijection_is_bijective
• function_properties::lemma_right_inverse_of_bijection_is_bijective
• function_properties::lemma_two_sided_inverse_implies_bijective
• function_properties::right_inverse_on
• ghost_tree::group_ghost_tree
• ghost_tree::path_between
• ghost_tree::path_between_properties
• map_extra::forall_map
• map_extra::forall_map_values
• map_extra::group_forall_map_lemmas
• map_extra::group_map_remove_keys_lemmas
• map_extra::group_value_filter_lemmas
• map_extra::lemma_forall_map_entry
• map_extra::lemma_forall_map_insert
• map_extra::lemma_forall_map_remove
• map_extra::lemma_forall_map_values_entry
• map_extra::lemma_forall_map_values_insert
• map_extra::lemma_forall_map_values_remove
• map_extra::lemma_insert_value_filter_different_len_contains
• map_extra::lemma_insert_value_filter_different_len_not_contains
• map_extra::lemma_insert_value_filter_false
• map_extra::lemma_insert_value_filter_same_len
• map_extra::lemma_insert_value_filter_true
• map_extra::lemma_map_insert_len
• map_extra::lemma_map_remove_keys_finite
• map_extra::lemma_map_remove_len
• map_extra::lemma_project_first_key_finite
• map_extra::lemma_project_first_key_sound
• map_extra::lemma_project_first_key_value_filter_empty
• map_extra::lemma_project_first_key_value_filter_non_empty
• map_extra::lemma_remove_value_filter_false
• map_extra::lemma_remove_value_filter_true
• map_extra::lemma_value_filter_all_false
• map_extra::lemma_value_filter_all_true
• map_extra::lemma_value_filter_choose
• map_extra::lemma_value_filter_contains
• map_extra::lemma_value_filter_contains_key
• map_extra::lemma_value_filter_finite
• map_extra::project_first_key
• map_extra::project_second_key
• map_extra::value_filter
• map_extra::value_filter_choose
• raw_ptr_extra::lemma_two_align_of_equal
• raw_ptr_extra::lemma_two_size_of_equal
• seq_extra::forall_seq
• seq_extra::group_forall_seq_lemmas
• seq_extra::group_seq_extra_lemmas
• seq_extra::lemma_drop_last_contains_different
• seq_extra::lemma_forall_seq_drop_last
• seq_extra::lemma_forall_seq_index
• seq_extra::lemma_forall_seq_push
• seq_extra::lemma_prefix_of_common_sequence
• seq_extra::lemma_push_contains_different
• seq_extra::lemma_push_contains_same
• seq_extra::lemma_seq_add_head_back
• seq_extra::lemma_seq_all_add
• seq_extra::lemma_seq_all_drop_last
• seq_extra::lemma_seq_all_index
• seq_extra::lemma_seq_all_push
• seq_extra::lemma_seq_drop_pushed_head
• seq_extra::lemma_seq_push_head
• seq_extra::lemma_seq_push_head_take_head
• seq_extra::lemma_seq_to_set_map_contains
• seq_extra::seq_tracked_add
• seq_extra::seq_tracked_empty
• seq_extra::seq_tracked_map_values
• seq_extra::seq_tracked_new
• seq_extra::seq_tracked_subrange
• seq_extra::seq_tracked_update
• set_extra::is_partition
• set_extra::lemma_empty_bad_set_implies_forall
• set_extra::lemma_filter_all_false
• set_extra::lemma_filter_len_unchanged_implies_equal
• set_extra::lemma_flatten_cardinality_under_disjointness
• set_extra::lemma_flatten_cardinality_under_disjointness_same_length
• set_extra::lemma_full_good_set_implies_forall
• set_extra::lemma_insert_filter_false
• set_extra::lemma_insert_filter_true
• set_extra::lemma_nat_range_finite
• set_extra::lemma_remove_filter_true
• set_extra::lemma_set_prop_mutual_exclusion
• set_extra::lemma_set_separation
• set_extra::pairwise_disjoint
• set_extra::set_prop_mutual_exclusion
• std_extra::_verus_external_fn_specification_9__60__32__91_T_93__32__62__32__58__58__32_as__ptr
• std_extra::as_ptr_spec
• temporal_logic::defs::always
• temporal_logic::defs::enabled
• temporal_logic::defs::eventually
• temporal_logic::defs::false_pred
• temporal_logic::defs::later
• temporal_logic::defs::lift_action
• temporal_logic::defs::lift_state
• temporal_logic::defs::lift_state_exists
• temporal_logic::defs::lift_state_forall
• temporal_logic::defs::lift_state_prime
• temporal_logic::defs::not
• temporal_logic::defs::stable
• temporal_logic::defs::tla_exists
• temporal_logic::defs::tla_forall
• temporal_logic::defs::true_pred
• temporal_logic::defs::valid
• temporal_logic::defs::weak_fairness
• temporal_logic::rules::always_and_equality
• temporal_logic::rules::always_double_equality
• temporal_logic::rules::always_implies_forall_intro
• temporal_logic::rules::always_implies_preserved_by_always
• temporal_logic::rules::always_implies_to_leads_to
• temporal_logic::rules::always_lift_state_and_equality
• temporal_logic::rules::always_lift_state_weaken
• temporal_logic::rules::always_p_is_stable
• temporal_logic::rules::always_to_always_later
• temporal_logic::rules::always_weaken
• temporal_logic::rules::eliminate_always
• temporal_logic::rules::entails_always_lift_state_and
• temporal_logic::rules::entails_always_lift_state_and_elim
• temporal_logic::rules::entails_and_different_temp
• temporal_logic::rules::entails_and_equality
• temporal_logic::rules::entails_and_temp
• temporal_logic::rules::entails_and_temp_reverse
• temporal_logic::rules::entails_implies_leads_to
• temporal_logic::rules::entails_implies_temp_reverse
• temporal_logic::rules::entails_not_temp_reverse
• temporal_logic::rules::entails_or_temp
• temporal_logic::rules::entails_preserved_by_always
• temporal_logic::rules::entails_tla_exists_by_witness
• temporal_logic::rules::entails_trans
• temporal_logic::rules::entails_trans_by_simplify
• temporal_logic::rules::group_tla_rules
• temporal_logic::rules::implies_new_invariant
• temporal_logic::rules::implies_tla_exists_by_witness
• temporal_logic::rules::implies_tla_exists_intro
• temporal_logic::rules::init_invariant
• temporal_logic::rules::leads_to_always_combine
• temporal_logic::rules::leads_to_always_enhance
• temporal_logic::rules::leads_to_always_tla_forall
• temporal_logic::rules::leads_to_apply
• temporal_logic::rules::leads_to_by_borrowing_inv
• temporal_logic::rules::leads_to_framed_by_or
• temporal_logic::rules::leads_to_rank_step_one
• temporal_logic::rules::leads_to_rank_step_one_usize
• temporal_logic::rules::leads_to_self_temp
• temporal_logic::rules::leads_to_shortcut_temp
• temporal_logic::rules::leads_to_stable
• temporal_logic::rules::leads_to_tla_exists_by_witness
• temporal_logic::rules::leads_to_tla_exists_intro
• temporal_logic::rules::leads_to_trans
• temporal_logic::rules::leads_to_weaken
• temporal_logic::rules::lift_state_and_equality
• temporal_logic::rules::lift_state_exists_absorb_equality
• temporal_logic::rules::lift_state_exists_equality
• temporal_logic::rules::lift_state_exists_leads_to_case_analysis
• temporal_logic::rules::lift_state_exists_leads_to_intro
• temporal_logic::rules::lift_state_forall_absorb_equality
• temporal_logic::rules::lift_state_implies_equality
• temporal_logic::rules::lift_state_not_equality
• temporal_logic::rules::lift_state_or_equality
• temporal_logic::rules::or_leads_to_case_analysis
• temporal_logic::rules::or_leads_to_combine
• temporal_logic::rules::p_leads_to_q_is_stable
• temporal_logic::rules::pack_conditions_to_spec
• temporal_logic::rules::spec_entails_always_tla_forall
• temporal_logic::rules::spec_entails_tla_forall
• temporal_logic::rules::stable_and_temp
• temporal_logic::rules::state_exists_intro
• temporal_logic::rules::state_pred_and_apply_equality
• temporal_logic::rules::state_pred_implies_apply_equality
• temporal_logic::rules::state_pred_not_apply_equality
• temporal_logic::rules::state_pred_or_apply_equality
• temporal_logic::rules::strengthen_leads_to_with_until
• temporal_logic::rules::strengthen_next
• temporal_logic::rules::temp_pred_equality
• temporal_logic::rules::tla_exists_leads_to_intro
• temporal_logic::rules::tla_forall_a_p_leads_to_q_a_is_stable
• temporal_logic::rules::tla_forall_always_equality
• temporal_logic::rules::tla_forall_always_equality_variant
• temporal_logic::rules::tla_forall_apply
• temporal_logic::rules::transform_leads_to_with_until
• temporal_logic::rules::unpack_conditions_from_spec
• temporal_logic::rules::use_always_tla_forall
• temporal_logic::rules::use_tla_forall
• temporal_logic::rules::vacuous_leads_to
• temporal_logic::rules::wf1
• temporal_logic::rules::wf1_by_borrowing_inv
• temporal_logic::rules::wf1_variant_temp