Module vstd::std_specs::hash

Structs

• ExDefaultHasher
• ExHashMap
• ExHashSet
• ExIter
• ExKeys
• ExRandomState
• IterGhostIterator
• KeysGhostIterator

Traits

• DefaultHasherAdditionalSpecFns
• ExBuildHasher
• ExHasher
• HashMapAdditionalSpecFns
• IterAdditionalSpecFns
• KeysAdditionalSpecFns

Functions

• _verus_external_fn_specification_57_DefaultHasher_32__58__58__32_new^⚠
• _verus_external_fn_specification_58_DefaultHasher_32__58__58__32_write^⚠
• _verus_external_fn_specification_59_DefaultHasher_32__58__58__32_finish^⚠
• _verus_external_fn_specification_60_Keys_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next^⚠
• _verus_external_fn_specification_61_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_len^⚠
• _verus_external_fn_specification_62_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_new^⚠
• _verus_external_fn_specification_63_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_with__capacity^⚠
• _verus_external_fn_specification_64_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_44__32__62__32__58__58__32_reserve^⚠
• _verus_external_fn_specification_65_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_insert^⚠
• _verus_external_fn_specification_66_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_contains__key_32__58__58__32__60__32_Q_32__62_^⚠
• _verus_external_fn_specification_67_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_^⚠
• _verus_external_fn_specification_68_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_^⚠
• _verus_external_fn_specification_69_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_clear^⚠
• _verus_external_fn_specification_70_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_keys^⚠
• _verus_external_fn_specification_71_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next^⚠
• _verus_external_fn_specification_72_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_len^⚠
• _verus_external_fn_specification_73_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new^⚠
• _verus_external_fn_specification_74_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity^⚠
• _verus_external_fn_specification_75_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve^⚠
• _verus_external_fn_specification_76_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_insert^⚠
• _verus_external_fn_specification_77_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains^⚠
• _verus_external_fn_specification_78_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_^⚠
• _verus_external_fn_specification_79_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_^⚠
• _verus_external_fn_specification_80_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_clear^⚠
• _verus_external_fn_specification_81_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_iter^⚠
• axiom_bool_obeys_hash_table_key_model
• axiom_box_bool_obeys_hash_table_key_model
• axiom_box_integer_type_obeys_hash_table_key_model
• axiom_box_key_removed
• axiom_contains_box
• axiom_contains_deref_key
• axiom_deref_key_removed
• axiom_i8_obeys_hash_table_key_model
• axiom_i16_obeys_hash_table_key_model
• axiom_i32_obeys_hash_table_key_model
• axiom_i128_obeys_hash_table_key_model
• axiom_i164_obeys_hash_table_key_model
• axiom_isize_obeys_hash_table_key_model
• axiom_maps_box_key_to_value
• axiom_maps_deref_key_to_value
• axiom_random_state_builds_valid_hashers
• axiom_set_box_key_removed
• axiom_set_box_key_to_value
• axiom_set_contains_box
• axiom_set_contains_deref_key
• axiom_set_deref_key_removed
• axiom_set_deref_key_to_value
• axiom_spec_hash_map_len
• axiom_spec_hash_set_len
• axiom_u8_obeys_hash_table_key_model
• axiom_u16_obeys_hash_table_key_model
• axiom_u32_obeys_hash_table_key_model
• axiom_u64_obeys_hash_table_key_model
• axiom_u128_obeys_hash_table_key_model
• axiom_usize_obeys_hash_table_key_model
• borrowed_key_removed
• builds_valid_hashers
• contains_borrowed_key
• group_hash_axioms
• maps_borrowed_key_to_value
• obeys_key_model
• set_contains_borrowed_key
• sets_borrowed_key_to_key
• sets_differ_by_borrowed_key
• spec_hash_map_len
• spec_hash_set_len