vstd/std_specs/
hash.rs

1//! This code adds specifications for the standard-library types
2//! `std::collections::HashMap` and `std::collections::HashSet`.
3//!
4//! Most of the specification only applies if you use `HashMap<Key,
5//! Value>` or `HashSet<Key>`. If you use some custom build hasher,
6//! e.g., with`HashMap<Key, Value, CustomBuildHasher>`, the
7//! specification won't specify much.
8//!
9//! Likewise, the specification is only meaningful when the `Key`
10//! obeys our hash table model, i.e., (1) `Key::hash` is
11//! deterministic, (2) any two `Key`s are identical if and only if the
12//! executable `==` operator considers them equal, and (3)
13//! `Key::clone` produces a result equal to its input. We have an
14//! axiom that all primitive types and `Box`es thereof obey this
15//! model. But if you want to use some other key type `MyKey`, you
16//! need to explicitly state your assumption that it does so with
17//! `assume(vstd::std_specs::hash::obeys_key_model::<MyKey>());`. In
18//! the future, we plan to devise a way for you to prove that it does
19//! so, so that you don't have to make such an assumption.
20//!
21//! By default, the Verus standard library brings useful axioms
22//! about the behavior of `HashMap` and `HashSet` into the ambient
23//! reasoning context by broadcasting the group
24//! `vstd::std_specs::hash::group_hash_axioms`.
25use super::super::prelude::*;
26use super::iter::IteratorSpec;
27
28use core::alloc::Allocator;
29use core::borrow::Borrow;
30use core::hash::{BuildHasher, Hash, Hasher};
31use core::marker::PhantomData;
32use core::option::Option;
33use core::option::Option::None;
34use std::collections::hash_map;
35use std::collections::hash_map::{
36    DefaultHasher, Entry, Keys, OccupiedEntry, RandomState, VacantEntry, Values,
37};
38use std::collections::hash_set;
39use std::collections::{HashMap, HashSet};
40
41verus! {
42
43/// Specifications for the behavior of
44/// [`std::collections::hash_map::DefaultHasher`](https://doc.rust-lang.org/std/collections/hash_map/struct.DefaultHasher.html).
45///
46/// We model a `DefaultHasher` as having a view (i.e., an abstract
47/// state) of type `Seq<Seq<u8>>`. This reflects the sequence of write
48/// operations performed so far, where each write is modeled as having
49/// written a sequence of bytes. There's also a specification for
50/// how a view will be transformed by `finish` into a `u64`.
51#[verifier::external_type_specification]
52#[verifier::external_body]
53pub struct ExDefaultHasher(DefaultHasher);
54
55impl View for DefaultHasher {
56    type V = Seq<Seq<u8>>;
57
58    #[verifier::external_body]
59    uninterp spec fn view(&self) -> Seq<Seq<u8>>;
60}
61
62pub trait DefaultHasherAdditionalSpecFns {
63    spec fn spec_finish(s: Seq<Seq<u8>>) -> u64;
64}
65
66impl DefaultHasherAdditionalSpecFns for DefaultHasher {
67    #[verifier::external_body]
68    uninterp spec fn spec_finish(s: Seq<Seq<u8>>) -> u64;
69}
70
71// This is the specification of behavior for `DefaultHasher::new()`.
72pub assume_specification[ DefaultHasher::new ]() -> (result: DefaultHasher)
73    ensures
74        result@ == Seq::<Seq<u8>>::empty(),
75;
76
77// This is the specification of behavior for `DefaultHasher::write(&[u8])`.
78pub assume_specification[ DefaultHasher::write ](state: &mut DefaultHasher, bytes: &[u8])
79    ensures
80        final(state)@ == old(state)@.push(bytes@),
81;
82
83// This is the specification of behavior for `DefaultHasher::finish()`.
84pub assume_specification[ DefaultHasher::finish ](state: &DefaultHasher) -> (result: u64)
85    ensures
86        result == DefaultHasher::spec_finish(state@),
87;
88
89/// Specifies whether a type `Key` conforms to our requirements to be
90/// a key in our hash table (and hash set) model.
91///
92/// The three requirements are (1) the hash function is deterministic,
93/// (2) any two keys of type `Key` are identical if and only if they
94/// are considered equal by the executable `==` operator, and (3) the
95/// executable `Key::clone` function produces a result identical to
96/// its input. Requirement (1) isn't satisfied by having `Key`
97/// implement `Hash`, since this trait doesn't mandate determinism.
98///
99/// The standard library has axioms that all primitive types and `Box`es
100/// thereof obey this model. If you want to use some other key
101/// type `MyKey`, you need to explicitly state your assumption that it
102/// does so with
103/// `assume(vstd::std_specs::hash::obeys_key_model::<MyKey>())`.
104/// In the future, we plan to devise a way for you to prove that it
105/// does so, so that you don't have to make such an assumption.
106#[verifier::external_body]
107pub uninterp spec fn obeys_key_model<Key: ?Sized>() -> bool;
108
109// These axioms state that any primitive type, or `Box` thereof,
110// obeys the requirements to be a key in a hash table that
111// conforms to our hash-table model.
112// (Declare each separately to enable pruning of unused primitive types.)
113pub broadcast proof fn axiom_bool_obeys_hash_table_key_model()
114    ensures
115        #[trigger] obeys_key_model::<bool>(),
116{
117    admit();
118}
119
120pub broadcast proof fn axiom_u8_obeys_hash_table_key_model()
121    ensures
122        #[trigger] obeys_key_model::<u8>(),
123{
124    admit();
125}
126
127pub broadcast proof fn axiom_u16_obeys_hash_table_key_model()
128    ensures
129        #[trigger] obeys_key_model::<u16>(),
130{
131    admit();
132}
133
134pub broadcast proof fn axiom_u32_obeys_hash_table_key_model()
135    ensures
136        #[trigger] obeys_key_model::<u32>(),
137{
138    admit();
139}
140
141pub broadcast proof fn axiom_u64_obeys_hash_table_key_model()
142    ensures
143        #[trigger] obeys_key_model::<u64>(),
144{
145    admit();
146}
147
148pub broadcast proof fn axiom_u128_obeys_hash_table_key_model()
149    ensures
150        #[trigger] obeys_key_model::<u128>(),
151{
152    admit();
153}
154
155pub broadcast proof fn axiom_usize_obeys_hash_table_key_model()
156    ensures
157        #[trigger] obeys_key_model::<usize>(),
158{
159    admit();
160}
161
162pub broadcast proof fn axiom_i8_obeys_hash_table_key_model()
163    ensures
164        #[trigger] obeys_key_model::<i8>(),
165{
166    admit();
167}
168
169pub broadcast proof fn axiom_i16_obeys_hash_table_key_model()
170    ensures
171        #[trigger] obeys_key_model::<i16>(),
172{
173    admit();
174}
175
176pub broadcast proof fn axiom_i32_obeys_hash_table_key_model()
177    ensures
178        #[trigger] obeys_key_model::<i32>(),
179{
180    admit();
181}
182
183pub broadcast proof fn axiom_i64_obeys_hash_table_key_model()
184    ensures
185        #[trigger] obeys_key_model::<i64>(),
186{
187    admit();
188}
189
190pub broadcast proof fn axiom_i128_obeys_hash_table_key_model()
191    ensures
192        #[trigger] obeys_key_model::<i128>(),
193{
194    admit();
195}
196
197pub broadcast proof fn axiom_isize_obeys_hash_table_key_model()
198    ensures
199        #[trigger] obeys_key_model::<isize>(),
200{
201    admit();
202}
203
204pub broadcast proof fn axiom_box_bool_obeys_hash_table_key_model()
205    ensures
206        #[trigger] obeys_key_model::<Box<bool>>(),
207{
208    admit();
209}
210
211pub broadcast proof fn axiom_box_integer_type_obeys_hash_table_key_model<Key: Integer + ?Sized>()
212    requires
213        obeys_key_model::<Key>(),
214    ensures
215        #[trigger] obeys_key_model::<Box<Key>>(),
216{
217    admit();
218}
219
220#[verifier::external_trait_specification]
221pub trait ExHasher {
222    type ExternalTraitSpecificationFor: Hasher;
223}
224
225// Our model for the external trait `BuildHasher` is that for any two
226// `Hasher`s it builds, if they're both given the same write sequence
227// then their states will match and they'll produce the same digest
228// when invoked with `finish()`.
229//
230// We don't expect that all types implementing the `BuildHasher` trait
231// will conform to our model, just the types T for which
232// `builds_valid_hashers::<T>()` holds.
233#[verifier::external_trait_specification]
234pub trait ExBuildHasher {
235    type ExternalTraitSpecificationFor: BuildHasher;
236
237    type Hasher: Hasher;
238}
239
240/// Specifies whether a type conforms to our requirements to be a hash builder
241/// in our hash table (and hash set) model.
242///
243/// Our model requires that for any two `Hasher`s that the `BuildHasher` builds,
244/// if they're both given the same write sequence
245/// then their states will match and they'll produce the same digest
246/// when invoked with `finish()`.
247///
248/// The standard library has an axiom that `RandomState`, the default `BuildHasher`
249/// used by `HashMap` and `HashSet`, implements this model.
250/// If you want to use some other hash builder type `MyHashBuilder`,
251/// you need to explicitly state your assumption that it does so with
252/// `assume(vstd::std_specs::hash::builds_valid_hashers::<MyHashBuilder>())`.
253#[verifier::external_body]
254pub uninterp spec fn builds_valid_hashers<T: ?Sized>() -> bool;
255
256/// Specifications for the behavior of
257/// [`std::hash::RandomState`](https://doc.rust-lang.org/std/hash/struct.RandomState.html).
258///
259/// `RandomState` is the default `BuildHasher` used by Rust's `HashMap` and `HashSet` implementations.
260/// We have an axiom that `RandomState` satisfies [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
261/// and thereby conforms to our model of how `BuildHasher` behaves.
262#[verifier::external_type_specification]
263#[verifier::external_body]
264pub struct ExRandomState(RandomState);
265
266pub broadcast proof fn axiom_random_state_builds_valid_hashers()
267    ensures
268        #[trigger] builds_valid_hashers::<RandomState>(),
269{
270    admit();
271}
272
273/// Specifications for the behavior of
274/// [`std::collections::hash_map::Keys`](https://doc.rust-lang.org/std/collections/hash_map/struct.Keys.html).
275#[verifier::external_type_specification]
276#[verifier::external_body]
277#[verifier::accept_recursive_types(Key)]
278#[verifier::accept_recursive_types(Value)]
279pub struct ExKeys<'a, Key: 'a, Value: 'a>(Keys<'a, Key, Value>);
280
281// To allow reasoning about the "contents" of the Keys iterator, without using
282// a prophecy, we need a function that gives us the underlying sequence of the original keys.
283pub uninterp spec fn into_iter_keys<'a, Key, Value>(i: Keys<'a, Key, Value>) -> Seq<Key>;
284
285impl<'a, K, V> super::iter::IteratorSpecImpl for Keys<'a, K, V> {
286    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
287        true
288    }
289
290    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
291
292    uninterp spec fn will_return_none(&self) -> bool;
293
294    uninterp spec fn decrease(&self) -> Option<nat>;
295
296    open spec fn peek(&self, index: int) -> Option<Self::Item> {
297        if 0 <= index < into_iter_keys(*self).len() {
298            Some(&into_iter_keys(*self)[index])
299        } else {
300            None
301        }
302    }
303}
304
305/// Specifications for the behavior of
306/// [`std::collections::hash_map::Values`](https://doc.rust-lang.org/std/collections/hash_map/struct.Values.html).
307#[verifier::external_type_specification]
308#[verifier::external_body]
309#[verifier::accept_recursive_types(Key)]
310#[verifier::accept_recursive_types(Value)]
311pub struct ExValues<'a, Key: 'a, Value: 'a>(Values<'a, Key, Value>);
312
313// To allow reasoning about the "contents" of the Values iterator, without using
314// a prophecy, we need a function that gives us the underlying sequence of the original values.
315pub uninterp spec fn into_iter_values<'a, Key, Value>(i: Values<'a, Key, Value>) -> Seq<Value>;
316
317impl<'a, K, V> super::iter::IteratorSpecImpl for Values<'a, K, V> {
318    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
319        true
320    }
321
322    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
323
324    uninterp spec fn will_return_none(&self) -> bool;
325
326    uninterp spec fn decrease(&self) -> Option<nat>;
327
328    open spec fn peek(&self, index: int) -> Option<Self::Item> {
329        if 0 <= index < into_iter_values(*self).len() {
330            Some(&into_iter_values(*self)[index])
331        } else {
332            None
333        }
334    }
335}
336
337// The `iter` method of a `HashMap` returns an iterator of type `hash_map::Iter`,
338// so we specify that type here.
339#[verifier::external_type_specification]
340#[verifier::external_body]
341#[verifier::accept_recursive_types(Key)]
342#[verifier::accept_recursive_types(Value)]
343pub struct ExMapIter<'a, Key: 'a, Value: 'a>(hash_map::Iter<'a, Key, Value>);
344
345// To allow reasoning about the "contents" of the Iter iterator, without using
346// a prophecy, we need a function that gives us the underlying sequence of the original map.
347pub uninterp spec fn into_iter<'a, Key, Value>(i: hash_map::Iter<'a, Key, Value>) -> Seq<
348    (Key, Value),
349>;
350
351impl<'a, K, V> super::iter::IteratorSpecImpl for hash_map::Iter<'a, K, V> {
352    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
353        true
354    }
355
356    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
357
358    uninterp spec fn will_return_none(&self) -> bool;
359
360    uninterp spec fn decrease(&self) -> Option<nat>;
361
362    open spec fn peek(&self, index: int) -> Option<Self::Item> {
363        if 0 <= index < into_iter(*self).len() {
364            let (k, v) = into_iter(*self)[index];
365            Some((&k, &v))
366        } else {
367            None
368        }
369    }
370}
371
372pub assume_specification<'a, Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::iter ](
373    m: &'a HashMap<Key, Value, S, A>,
374) -> (iter: hash_map::Iter<'a, Key, Value>)
375    ensures
376        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
377            &&& IteratorSpec::remaining(&iter).len() == m@.dom().len()
378            &&& forall|i: int|
379                #![trigger m@.contains_key(*IteratorSpec::remaining(&iter)[i].0)]
380                #![trigger m@[*IteratorSpec::remaining(&iter)[i].0]]
381                0 <= i < IteratorSpec::remaining(&iter).len() ==> m@.contains_key(
382                    *IteratorSpec::remaining(&iter)[i].0,
383                ) && m@[*IteratorSpec::remaining(&iter)[i].0] == *IteratorSpec::remaining(
384                    &iter,
385                )[i].1
386            &&& forall|k: Key| #[trigger]
387                m@.contains_key(k) ==> IteratorSpec::remaining(&iter).contains((&k, &m@[k]))
388            &&& IteratorSpec::remaining(&iter).unref().to_set() == m@.kv_pairs()
389            &&& iter.remaining().no_duplicates()
390            &&& into_iter(iter) == IteratorSpec::remaining(&iter).unref()
391            &&& IteratorSpec::decrease(&iter) is Some
392        },
393;
394
395/// Specifications for the behavior of [`std::collections::HashMap`](https://doc.rust-lang.org/std/collections/struct.HashMap.html).
396///
397/// We model a `HashMap` as having a view of type `Map<Key, Value>`, which reflects the current state of the map.
398///
399/// These specifications are only meaningful if `obeys_key_model::<Key>()` and `builds_valid_hashers::<S>()` hold.
400/// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
401/// for information on use with primitive types and other types,
402/// and see [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
403/// for information on use with Rust's default implementation and custom implementations.
404///
405/// Axioms about the behavior of HashMap are present in the broadcast group `vstd::std_specs::hash::group_hash_axioms`.
406#[verifier::external_type_specification]
407#[verifier::external_body]
408#[verifier::accept_recursive_types(Key)]
409#[verifier::accept_recursive_types(Value)]
410#[verifier::reject_recursive_types(S)]
411#[verifier::reject_recursive_types(A)]
412pub struct ExHashMap<Key, Value, S, A: Allocator>(HashMap<Key, Value, S, A>);
413
414pub trait HashMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
415    spec fn spec_index(&self, k: Key) -> Value
416        recommends
417            self@.contains_key(k),
418    ;
419}
420
421impl<Key, Value, S, A: Allocator> HashMapAdditionalSpecFns<Key, Value> for HashMap<
422    Key,
423    Value,
424    S,
425    A,
426> {
427    #[verifier::inline]
428    open spec fn spec_index(&self, k: Key) -> Value {
429        self@.index(k)
430    }
431}
432
433/// The actual definition of `HashMap::deep_view`.
434///
435/// This is a separate function since it introduces a lot of quantifiers and revealing an opaque trait
436/// method is not supported. In most cases, it's easier to use one of the lemmas below instead
437/// of revealing this function directly.
438#[verifier::opaque]
439pub open spec fn hash_map_deep_view_impl<
440    Key: DeepView,
441    Value: DeepView,
442    S,
443    A: core::alloc::Allocator,
444>(m: HashMap<Key, Value, S, A>) -> Map<Key::V, Value::V> {
445    Map::new(
446        m@.dom().map(|k: Key| k.deep_view()),
447        |dk: Key::V|
448            {
449                let k = choose|k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
450                m@[k].deep_view()
451            },
452    )
453}
454
455pub broadcast proof fn lemma_hashmap_deepview_dom<K: DeepView, V: DeepView>(m: HashMap<K, V>)
456    ensures
457        #[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),
458{
459    reveal(hash_map_deep_view_impl);
460    broadcast use group_hash_axioms;
461    broadcast use crate::vstd::group_vstd_default;
462
463    assert(m.deep_view().dom() =~= m@.dom().map(|k: K| k.deep_view()));
464}
465
466pub broadcast proof fn lemma_hashmap_deepview_properties<K: DeepView, V: DeepView>(m: HashMap<K, V>)
467    requires
468        crate::relations::injective(|k: K| k.deep_view()),
469    ensures
470        #![trigger m.deep_view()]
471        // all elements in m.view() are present in m.deep_view()
472        forall|k: K| #[trigger]
473            m@.contains_key(k) ==> m.deep_view().contains_key(k.deep_view())
474                && m.deep_view()[k.deep_view()] == m@[k].deep_view(),
475        // all elements in m.deep_view() are present in m.view()
476        forall|dk: <K as DeepView>::V| #[trigger]
477            m.deep_view().contains_key(dk) ==> exists|k: K|
478                k.deep_view() == dk && #[trigger] m@.contains_key(k),
479{
480    reveal(hash_map_deep_view_impl);
481    broadcast use group_hash_axioms;
482    broadcast use crate::vstd::group_vstd_default;
483
484    lemma_hashmap_deepview_dom(m);
485    assert(m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()));
486    assert forall|k: K| #[trigger] m@.contains_key(k) implies m.deep_view().contains_key(
487        k.deep_view(),
488    ) && m.deep_view()[k.deep_view()] == m@[k].deep_view() by {
489        assert(m@.dom().contains(k));
490        assert(m@.dom().map(|k: K| k.deep_view()).contains(k.deep_view()));
491        assert(m.deep_view().dom().contains(k.deep_view()));
492        let k2 = choose|k2: K| m@.contains_key(k2) && #[trigger] k2.deep_view() == k.deep_view();
493        assert forall|k1: K, k2: K| #[trigger]
494            k1.deep_view() == #[trigger] k2.deep_view() implies k1 == k2 by {
495            let ghost k_deepview = |k: K| k.deep_view();
496            assert(crate::relations::injective(k_deepview));
497            assert(k_deepview(k1) == k_deepview(k2));
498        }
499        assert(k2 == k);
500    }
501    assert forall|dk: K::V| #[trigger] m.deep_view().contains_key(dk) implies exists|k: K|
502        k.deep_view() == dk && #[trigger] m@.contains_key(k) by {
503        assert(m.deep_view().dom().contains(dk));
504        assert(m@.dom().map(|k: K| k.deep_view()).contains(dk));
505        let k = choose|k: K| #[trigger] m@.dom().contains(k) && k.deep_view() == dk;
506        assert(m@.contains_key(k));
507    }
508}
509
510pub broadcast proof fn lemma_hashmap_deepview_values<K: DeepView, V: DeepView>(m: HashMap<K, V>)
511    requires
512        crate::relations::injective(|k: K| k.deep_view()),
513    ensures
514        #[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),
515{
516    reveal(hash_map_deep_view_impl);
517    broadcast use group_hash_axioms;
518    broadcast use lemma_hashmap_deepview_properties;
519    broadcast use crate::vstd::group_vstd_default;
520
521    let lhs = m.deep_view().values();
522    let rhs = m@.values().map(|v: V| v.deep_view());
523    assert forall|v: V::V| #[trigger] lhs.contains(v) implies rhs.contains(v) by {
524        let dk = choose|dk: K::V| #[trigger]
525            m.deep_view().contains_key(dk) && m.deep_view()[dk] == v;
526        let k = choose|k: K| #[trigger] m@.contains_key(k) && k.deep_view() == dk;
527        let ov = choose|ov: V| #[trigger] m@.contains_key(k) && m@[k] == ov && ov.deep_view() == v;
528        assert(v == ov.deep_view());
529        assert(m@.values().contains(ov));
530    }
531}
532
533/// Borrowing a key works the same way on deep_view as on view,
534/// if deep_view is injective; see `axiom_contains_deref_key`.
535pub broadcast proof fn axiom_hashmap_deepview_borrow<
536    K: DeepView + Borrow<Q>,
537    V: DeepView,
538    Q: View<V = <K as DeepView>::V> + Hash + Eq + ?Sized,
539>(m: HashMap<K, V>, k: &Q)
540    requires
541        obeys_key_model::<K>(),
542        crate::relations::injective(|k: K| k.deep_view()),
543    ensures
544        #[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),
545{
546    admit();
547}
548
549pub uninterp spec fn spec_hash_map_len<Key, Value, S, A: Allocator>(
550    m: &HashMap<Key, Value, S, A>,
551) -> usize;
552
553pub broadcast proof fn axiom_spec_hash_map_len<Key, Value, S, A: Allocator>(
554    m: &HashMap<Key, Value, S, A>,
555)
556    ensures
557        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_map_len(m)
558            == m@.len(),
559{
560    admit();
561}
562
563#[verifier::when_used_as_spec(spec_hash_map_len)]
564pub assume_specification<Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::len ](
565    m: &HashMap<Key, Value, S, A>,
566) -> (len: usize)
567    ensures
568        len == spec_hash_map_len(m),
569;
570
571pub assume_specification<Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::capacity ](
572    m: &HashMap<Key, Value, S, A>,
573) -> (cap: usize)
574    ensures
575        cap >= spec_hash_map_len(m),
576;
577
578pub assume_specification<Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::is_empty ](
579    m: &HashMap<Key, Value, S, A>,
580) -> (res: bool)
581    ensures
582        res == m@.is_empty(),
583;
584
585pub assume_specification<K: Clone, V: Clone, S: Clone, A: Allocator + Clone>[ <HashMap::<
586    K,
587    V,
588    S,
589    A,
590> as Clone>::clone ](this: &HashMap<K, V, S, A>) -> (other: HashMap<K, V, S, A>)
591    ensures
592        other@.dom() == this@.dom(),
593        forall|key|
594            #![trigger other@.dom().contains(key)]
595            other@.dom().contains(key) ==> cloned(this@[key], #[trigger] other@[key]),
596;
597
598pub assume_specification<Key, Value>[ HashMap::<Key, Value>::new ]() -> (m: HashMap<
599    Key,
600    Value,
601    RandomState,
602>)
603    ensures
604        m@ == Map::<Key, Value>::empty(),
605;
606
607pub assume_specification<K, V, S: core::default::Default>[ <HashMap<
608    K,
609    V,
610    S,
611> as core::default::Default>::default ]() -> (m: HashMap<K, V, S>)
612    ensures
613        m@ == Map::<K, V>::empty(),
614;
615
616pub assume_specification<Key, Value>[ HashMap::<Key, Value>::with_capacity ](capacity: usize) -> (m:
617    HashMap<Key, Value, RandomState>)
618    ensures
619        m@ == Map::<Key, Value>::empty(),
620;
621
622pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::with_hasher ](
623    hash_builder: S,
624) -> (m: HashMap<Key, Value, S>)
625    ensures
626        m@ == Map::<Key, Value>::empty(),
627;
628
629pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher, A: Allocator>[ HashMap::<
630    Key,
631    Value,
632    S,
633    A,
634>::reserve ](m: &mut HashMap<Key, Value, S, A>, additional: usize)
635    ensures
636        final(m)@ == old(m)@,
637;
638
639pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher, A: Allocator>[ HashMap::<
640    Key,
641    Value,
642    S,
643    A,
644>::insert ](m: &mut HashMap<Key, Value, S, A>, k: Key, v: Value) -> (result: Option<Value>)
645    ensures
646        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
647            &&& final(m)@ == old(m)@.insert(k, v)
648            &&& match result {
649                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
650                None => !old(m)@.contains_key(k),
651            }
652        },
653;
654
655// The specification for `contains_key` has a parameter `key: &Q`
656// where you'd expect to find `key: &Key`. This allows for the case
657// that `Key` can be borrowed as something other than `&Key`. For
658// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
659// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
660// respectively.
661// To deal with this, we have a specification function that opaquely
662// specifies what it means for a map to contain a borrowed key of type
663// `&Q`. And the postcondition of `contains_key` just says that its
664// result matches the output of that specification function. But this
665// isn't very helpful by itself, since there's no body to that
666// specification function. So we have special-case axioms that say
667// what this means in two important circumstances: (1) `Key = Q` and
668// (2) `Key = Box<Q>`.
669pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
670    m: Map<Key, Value>,
671    k: &Q,
672) -> bool;
673
674pub broadcast proof fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
675    ensures
676        #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
677{
678    admit();
679}
680
681pub broadcast proof fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
682    ensures
683        #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
684            Box::new(*k),
685        ),
686{
687    admit();
688}
689
690pub assume_specification<
691    Key: Borrow<Q> + Hash + Eq,
692    Value,
693    S: BuildHasher,
694    A: Allocator,
695    Q: Hash + Eq + ?Sized,
696>[ HashMap::<Key, Value, S, A>::contains_key::<Q> ](
697    m: &HashMap<Key, Value, S, A>,
698    k: &Q,
699) -> (result: bool)
700    ensures
701        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result == contains_borrowed_key(
702            m@,
703            k,
704        ),
705;
706
707// The specification for `get` has a parameter `key: &Q` where you'd
708// expect to find `key: &Key`. This allows for the case that `Key` can
709// be borrowed as something other than `&Key`. For instance,
710// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
711// as `&str`, so in those cases `Q` would be `u32` and `str`
712// respectively.
713// To deal with this, we have a specification function that opaquely
714// specifies what it means for a map to map a borrowed key of type
715// `&Q` to a certain value. And the postcondition of `get` says that
716// its result matches the output of that specification function. (It
717// also says that its result corresponds to the output of
718// `contains_borrowed_key`, discussed above.) But this isn't very
719// helpful by itself, since there's no body to that specification
720// function. So we have special-case axioms that say what this means
721// in two important circumstances: (1) `Key = Q` and (2) `Key =
722// Box<Q>`.
723pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
724    m: Map<Key, Value>,
725    k: &Q,
726    v: Value,
727) -> bool;
728
729pub broadcast proof fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
730    ensures
731        #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
732            && m[*k] == v,
733{
734    admit();
735}
736
737pub broadcast proof fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
738    ensures
739        #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
740            let k = Box::new(*q);
741            &&& m.contains_key(k)
742            &&& m[k] == v
743        },
744{
745    admit();
746}
747
748pub assume_specification<
749    'a,
750    Key: Borrow<Q> + Hash + Eq,
751    Value,
752    S: BuildHasher,
753    A: Allocator,
754    Q: Hash + Eq + ?Sized,
755>[ HashMap::<Key, Value, S, A>::get::<Q> ](m: &'a HashMap<Key, Value, S, A>, k: &Q) -> (result:
756    Option<&'a Value>)
757    ensures
758        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
759            Some(v) => maps_borrowed_key_to_value(m@, k, *v),
760            None => !contains_borrowed_key(m@, k),
761        },
762;
763
764// The specification for `remove` has a parameter `key: &Q` where
765// you'd expect to find `key: &Key`. This allows for the case that
766// `Key` can be borrowed as something other than `&Key`. For instance,
767// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
768// as `&str`, so in those cases `Q` would be `u32` and `str`
769// respectively. To deal with this, we have a specification function
770// that opaquely specifies what it means for two maps to be related by
771// a remove of a certain `&Q`. And the postcondition of `remove` says
772// that `old(self)@` and `self@` satisfy that relationship. (It also
773// says that its result corresponds to the output of
774// `contains_borrowed_key` and `maps_borrowed_key_to_value`, discussed
775// above.) But this isn't very helpful by itself, since there's no
776// body to that specification function. So we have special-case axioms
777// that say what this means in two important circumstances: (1) `Key =
778// Q` and (2) `Key = Box<Q>`.
779pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
780    old_m: Map<Key, Value>,
781    new_m: Map<Key, Value>,
782    k: &Q,
783) -> bool;
784
785pub broadcast proof fn axiom_deref_key_removed<Q, Value>(
786    old_m: Map<Q, Value>,
787    new_m: Map<Q, Value>,
788    k: &Q,
789)
790    ensures
791        #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
792            *k,
793        ),
794{
795    admit();
796}
797
798pub broadcast proof fn axiom_box_key_removed<Q, Value>(
799    old_m: Map<Box<Q>, Value>,
800    new_m: Map<Box<Q>, Value>,
801    q: &Q,
802)
803    ensures
804        #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
805            == old_m.remove(Box::new(*q)),
806{
807    admit();
808}
809
810pub assume_specification<
811    Key: Borrow<Q> + Hash + Eq,
812    Value,
813    S: BuildHasher,
814    A: Allocator,
815    Q: Hash + Eq + ?Sized,
816>[ HashMap::<Key, Value, S, A>::remove::<Q> ](m: &mut HashMap<Key, Value, S, A>, k: &Q) -> (result:
817    Option<Value>)
818    ensures
819        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
820            &&& borrowed_key_removed(old(m)@, final(m)@, k)
821            &&& match result {
822                Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
823                None => !contains_borrowed_key(old(m)@, k),
824            }
825        },
826;
827
828pub assume_specification<Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::clear ](
829    m: &mut HashMap<Key, Value, S, A>,
830)
831    ensures
832        final(m)@ == Map::<Key, Value>::empty(),
833;
834
835pub assume_specification<'a, Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::keys ](
836    m: &'a HashMap<Key, Value, S, A>,
837) -> (keys: Keys<'a, Key, Value>)
838    ensures
839        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
840            &&& IteratorSpec::remaining(&keys).unref().to_set() == m@.dom()
841            &&& IteratorSpec::remaining(&keys).no_duplicates()
842            &&& IteratorSpec::remaining(&keys).len() == m@.dom().len()
843            &&& into_iter_keys(keys) == IteratorSpec::remaining(&keys).unref()
844            &&& IteratorSpec::decrease(&keys) is Some
845        },
846;
847
848pub assume_specification<'a, Key, Value, S, A: Allocator>[ HashMap::<Key, Value, S, A>::values ](
849    m: &'a HashMap<Key, Value, S, A>,
850) -> (values: Values<'a, Key, Value>)
851    ensures
852        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
853            &&& IteratorSpec::remaining(&values).unref().to_set() == m@.values()
854            &&& IteratorSpec::remaining(&values).len() == m@.dom().len()
855            &&& into_iter_values(values) == IteratorSpec::remaining(&values).unref()
856            &&& IteratorSpec::decrease(&values) is Some
857        },
858;
859
860pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
861    ensures
862        #[trigger] (decreases_to!(m => m@)),
863{
864    admit();
865}
866
867// The `iter` method of a `HashSet` returns an iterator of type `hash_set::Iter`,
868// so we specify that type here.
869#[verifier::external_type_specification]
870#[verifier::external_body]
871#[verifier::accept_recursive_types(Key)]
872pub struct ExSetIter<'a, Key: 'a>(hash_set::Iter<'a, Key>);
873
874// To allow reasoning about the "contents" of the HashSet iterator, without using
875// a prophecy, we need a function that gives us the underlying sequence of the original keys.
876pub uninterp spec fn into_iter_hash_keys<'a, Key>(i: hash_set::Iter::<'a, Key>) -> Seq<Key>;
877
878impl<'a, K> super::iter::IteratorSpecImpl for hash_set::Iter::<'a, K> {
879    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
880        true
881    }
882
883    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
884
885    uninterp spec fn will_return_none(&self) -> bool;
886
887    uninterp spec fn decrease(&self) -> Option<nat>;
888
889    open spec fn peek(&self, index: int) -> Option<Self::Item> {
890        if 0 <= index < into_iter_hash_keys(*self).len() {
891            Some(&into_iter_hash_keys(*self)[index])
892        } else {
893            None
894        }
895    }
896}
897
898/// Specifications for the behavior of [`std::collections::HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html).
899///
900/// We model a `HashSet` as having a view of type `Set<Key>`, which reflects the current state of the set.
901///
902/// These specifications are only meaningful if `obeys_key_model::<Key>()` and `builds_valid_hashers::<S>()` hold.
903/// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
904/// for information on use with primitive types and custom types,
905/// and see [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
906/// for information on use with Rust's default implementation and custom implementations.
907///
908/// Axioms about the behavior of HashSet are present in the broadcast group `vstd::std_specs::hash::group_hash_axioms`.
909#[verifier::external_type_specification]
910#[verifier::external_body]
911#[verifier::accept_recursive_types(Key)]
912#[verifier::reject_recursive_types(S)]
913#[verifier::reject_recursive_types(A)]
914pub struct ExHashSet<Key, S, A: Allocator>(HashSet<Key, S, A>);
915
916pub uninterp spec fn spec_hash_set_len<Key, S, A: Allocator>(m: &HashSet<Key, S, A>) -> usize;
917
918pub broadcast proof fn axiom_spec_hash_set_len<Key, S, A: Allocator>(m: &HashSet<Key, S, A>)
919    ensures
920        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_set_len(m)
921            == m@.len(),
922{
923    admit();
924}
925
926#[verifier::when_used_as_spec(spec_hash_set_len)]
927pub assume_specification<Key, S, A: Allocator>[ HashSet::<Key, S, A>::len ](
928    m: &HashSet<Key, S, A>,
929) -> (len: usize)
930    ensures
931        len == spec_hash_set_len(m),
932;
933
934pub assume_specification<Key, S, A: Allocator>[ HashSet::<Key, S, A>::is_empty ](
935    m: &HashSet<Key, S, A>,
936) -> (res: bool)
937    ensures
938        res == m@.is_empty(),
939;
940
941pub assume_specification<Key>[ HashSet::<Key>::new ]() -> (m: HashSet<Key, RandomState>)
942    ensures
943        m@ == Set::<Key>::empty(),
944;
945
946pub assume_specification<T, S: core::default::Default>[ <HashSet<
947    T,
948    S,
949> as core::default::Default>::default ]() -> (m: HashSet<T, S>)
950    ensures
951        m@ == Set::<T>::empty(),
952;
953
954pub assume_specification<Key>[ HashSet::<Key>::with_capacity ](capacity: usize) -> (m: HashSet<
955    Key,
956    RandomState,
957>)
958    ensures
959        m@ == Set::<Key>::empty(),
960;
961
962pub assume_specification<Key, S>[ HashSet::<Key, S>::with_hasher ](hash_builder: S) -> (m: HashSet<
963    Key,
964    S,
965>)
966    ensures
967        m@ == Set::<Key>::empty(),
968;
969
970pub assume_specification<Key, S>[ HashSet::<Key, S>::with_capacity_and_hasher ](
971    capacity: usize,
972    hash_builder: S,
973) -> (m: HashSet<Key, S>)
974    ensures
975        m@ == Set::<Key>::empty(),
976;
977
978pub assume_specification<Key: Eq + Hash, S: BuildHasher, A: Allocator>[ HashSet::<
979    Key,
980    S,
981    A,
982>::reserve ](m: &mut HashSet<Key, S, A>, additional: usize)
983    ensures
984        final(m)@ == old(m)@,
985;
986
987pub assume_specification<Key: Eq + Hash, S: BuildHasher, A: Allocator>[ HashSet::<
988    Key,
989    S,
990    A,
991>::insert ](m: &mut HashSet<Key, S, A>, k: Key) -> (result: bool)
992    ensures
993        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
994            &&& final(m)@ == old(m)@.insert(k)
995            &&& result == !old(m)@.contains(k)
996        },
997;
998
999// The specification for `contains` has a parameter `key: &Q`
1000// where you'd expect to find `key: &Key`. This allows for the case
1001// that `Key` can be borrowed as something other than `&Key`. For
1002// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
1003// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
1004// respectively.
1005// To deal with this, we have a specification function that opaquely
1006// specifies what it means for a set to contain a borrowed key of type
1007// `&Q`. And the postcondition of `contains` just says that its
1008// result matches the output of that specification function. But this
1009// isn't very helpful by itself, since there's no body to that
1010// specification function. So we have special-case axioms that say
1011// what this means in two important circumstances: (1) `Key = Q` and
1012// (2) `Key = Box<Q>`.
1013pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
1014
1015pub broadcast proof fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
1016    ensures
1017        #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
1018{
1019    admit();
1020}
1021
1022pub broadcast proof fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
1023    ensures
1024        #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
1025{
1026    admit();
1027}
1028
1029pub assume_specification<
1030    Key: Borrow<Q> + Hash + Eq,
1031    S: BuildHasher,
1032    A: Allocator,
1033    Q: Hash + Eq + ?Sized,
1034>[ HashSet::<Key, S, A>::contains ](m: &HashSet<Key, S, A>, k: &Q) -> (result: bool)
1035    ensures
1036        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result
1037            == set_contains_borrowed_key(m@, k),
1038;
1039
1040// The specification for `get` has a parameter `key: &Q` where you'd
1041// expect to find `key: &Key`. This allows for the case that `Key` can
1042// be borrowed as something other than `&Key`. For instance,
1043// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1044// as `&str`, so in those cases `Q` would be `u32` and `str`
1045// respectively.
1046// To deal with this, we have a specification function that opaquely
1047// specifies what it means for a returned reference to point to an
1048// element of a HashSet. And the postcondition of `get` says that
1049// its result matches the output of that specification function. (It
1050// also says that its result corresponds to the output of
1051// `contains_borrowed_key`, discussed above.) But this isn't very
1052// helpful by itself, since there's no body to that specification
1053// function. So we have special-case axioms that say what this means
1054// in two important circumstances: (1) `Key = Q` and (2) `Key =
1055// Box<Q>`.
1056pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
1057
1058pub broadcast proof fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
1059    ensures
1060        #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
1061{
1062    admit();
1063}
1064
1065pub broadcast proof fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
1066    ensures
1067        #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
1068            *q,
1069        ) == v),
1070{
1071    admit();
1072}
1073
1074pub assume_specification<
1075    'a,
1076    Key: Borrow<Q> + Hash + Eq,
1077    S: BuildHasher,
1078    A: Allocator,
1079    Q: Hash + Eq + ?Sized,
1080>[ HashSet::<Key, S, A>::get::<Q> ](m: &'a HashSet<Key, S, A>, k: &Q) -> (result: Option<&'a Key>)
1081    ensures
1082        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
1083            Some(v) => sets_borrowed_key_to_key(m@, k, v),
1084            None => !set_contains_borrowed_key(m@, k),
1085        },
1086;
1087
1088// The specification for `remove` has a parameter `key: &Q` where
1089// you'd expect to find `key: &Key`. This allows for the case that
1090// `Key` can be borrowed as something other than `&Key`. For instance,
1091// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1092// as `&str`, so in those cases `Q` would be `u32` and `str`
1093// respectively. To deal with this, we have a specification function
1094// that opaquely specifies what it means for two sets to be related by
1095// a remove of a certain `&Q`. And the postcondition of `remove` says
1096// that `old(self)@` and `self@` satisfy that relationship. (It also
1097// says that its result corresponds to the output of
1098// `set_contains_borrowed_key`, discussed above.) But this isn't very
1099// helpful by itself, since there's no body to that specification
1100// function. So we have special-case axioms that say what this means
1101// in two important circumstances: (1) `Key = Q` and (2) `Key = Box<Q>`.
1102pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
1103    old_m: Set<Key>,
1104    new_m: Set<Key>,
1105    k: &Q,
1106) -> bool;
1107
1108pub broadcast proof fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
1109    ensures
1110        #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
1111            *k,
1112        ),
1113{
1114    admit();
1115}
1116
1117pub broadcast proof fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
1118    ensures
1119        #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
1120            == old_m.remove(Box::new(*q)),
1121{
1122    admit();
1123}
1124
1125pub assume_specification<
1126    Key: Borrow<Q> + Hash + Eq,
1127    S: BuildHasher,
1128    A: Allocator,
1129    Q: Hash + Eq + ?Sized,
1130>[ HashSet::<Key, S, A>::remove::<Q> ](m: &mut HashSet<Key, S, A>, k: &Q) -> (result: bool)
1131    ensures
1132        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1133            &&& sets_differ_by_borrowed_key(old(m)@, final(m)@, k)
1134            &&& result == set_contains_borrowed_key(old(m)@, k)
1135        },
1136;
1137
1138pub assume_specification<Key, S, A: Allocator>[ HashSet::<Key, S, A>::clear ](
1139    m: &mut HashSet<Key, S, A>,
1140)
1141    ensures
1142        final(m)@ == Set::<Key>::empty(),
1143;
1144
1145pub assume_specification<'a, Key, S, A: Allocator>[ HashSet::<Key, S, A>::iter ](
1146    m: &'a HashSet<Key, S, A>,
1147) -> (hash_keys: hash_set::Iter<'a, Key>)
1148    ensures
1149        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1150            &&& IteratorSpec::remaining(&hash_keys).unref().to_set() == m@
1151            &&& IteratorSpec::remaining(&hash_keys).no_duplicates()
1152            &&& IteratorSpec::remaining(&hash_keys).len() == m@.len()
1153            &&& into_iter_hash_keys(hash_keys) == IteratorSpec::remaining(&hash_keys).unref()
1154            &&& IteratorSpec::decrease(&hash_keys) is Some
1155        },
1156;
1157
1158pub broadcast proof fn axiom_hashset_decreases<Key, S, A: Allocator>(m: HashSet<Key, S, A>)
1159    ensures
1160        #[trigger] (decreases_to!(m => m@)),
1161{
1162    admit();
1163}
1164
1165//////// Entry API
1166// Specs for OccupiedEntry, VacantEntry, and the Entry enum
1167// OccupiedEntry and VacantEntry are both opaque;
1168// Entry is just an enum wrapper around the other 2, so we leave it transparent.
1169#[verifier::reject_recursive_types_in_ground_variants(K)]
1170#[verifier::reject_recursive_types_in_ground_variants(V)]
1171#[verifier::reject_recursive_types(A)]
1172#[verifier::external_body]
1173#[verifier::external_type_specification]
1174pub struct ExOccupiedEntry<'a, K: 'a, V: 'a, A: Allocator>(OccupiedEntry<'a, K, V, A>);
1175
1176#[verifier::reject_recursive_types_in_ground_variants(K)]
1177#[verifier::accept_recursive_types(V)]
1178#[verifier::reject_recursive_types(A)]
1179#[verifier::external_body]
1180#[verifier::external_type_specification]
1181pub struct ExVacantEntry<'a, K: 'a, V: 'a, A: Allocator>(VacantEntry<'a, K, V, A>);
1182
1183#[verifier::external_type_specification]
1184#[verifier::reject_recursive_types(A)]
1185pub struct ExEntry<'a, K: 'a, V: 'a, A: Allocator>(Entry<'a, K, V, A>);
1186
1187/// Specification for an [`OccupiedEntry`].
1188/// Contains the current key and value in the entry,
1189/// and prophesies the final value after this instantiation of the entry API is complete.
1190/// The final value is optional, since the user might choose to remove the entry.
1191pub trait OccupiedEntrySpecFns<K, V, A>: Sized {
1192    spec fn spec_key(self) -> K;
1193
1194    spec fn value(self) -> V;
1195
1196    #[verifier::prophetic]
1197    spec fn final_value(self) -> Option<V>;
1198}
1199
1200impl<'a, K, V, A: Allocator> OccupiedEntrySpecFns<K, V, A> for OccupiedEntry<'a, K, V, A> {
1201    uninterp spec fn spec_key(self) -> K;
1202
1203    uninterp spec fn value(self) -> V;
1204
1205    #[verifier::prophetic]
1206    uninterp spec fn final_value(self) -> Option<V>;
1207}
1208
1209/// Specification for a [`VacantEntry`].
1210/// Contains the current key for the entry,
1211/// and prophesies the final value after this instantiation of the entry API is complete.
1212/// The final value is optional, since the user may or may not choose to insert a value.
1213pub trait VacantEntrySpecFns<K, V, A>: Sized {
1214    spec fn spec_key(self) -> K;
1215
1216    #[verifier::prophetic]
1217    spec fn final_value(self) -> Option<V>;
1218}
1219
1220impl<'a, K, V, A: Allocator> VacantEntrySpecFns<K, V, A> for VacantEntry<'a, K, V, A> {
1221    uninterp spec fn spec_key(self) -> K;
1222
1223    #[verifier::prophetic]
1224    uninterp spec fn final_value(self) -> Option<V>;
1225}
1226
1227/// Specification for an [`Entry`].
1228/// Contains the current key for the entry,
1229/// and prophesies the final value after this instantiation of the entry API is complete.
1230pub trait EntrySpecFns<K, V, A>: Sized {
1231    spec fn spec_key(self) -> K;
1232
1233    spec fn value(self) -> Option<V>;
1234
1235    #[verifier::prophetic]
1236    spec fn final_value(self) -> Option<V>;
1237}
1238
1239impl<'a, K, V, A: Allocator> EntrySpecFns<K, V, A> for Entry<'a, K, V, A> {
1240    open spec fn spec_key(self) -> K {
1241        match self {
1242            Entry::Occupied(occupied_entry) => occupied_entry.spec_key(),
1243            Entry::Vacant(vacant_entry) => vacant_entry.spec_key(),
1244        }
1245    }
1246
1247    open spec fn value(self) -> Option<V> {
1248        match self {
1249            Entry::Occupied(occupied_entry) => Some(occupied_entry.value()),
1250            Entry::Vacant(vacant_entry) => None,
1251        }
1252    }
1253
1254    #[verifier::prophetic]
1255    open spec fn final_value(self) -> Option<V> {
1256        match self {
1257            Entry::Occupied(occupied_entry) => occupied_entry.final_value(),
1258            Entry::Vacant(vacant_entry) => vacant_entry.final_value(),
1259        }
1260    }
1261}
1262
1263pub broadcast axiom fn axiom_has_resolved_occupied_entry<K, V, A: Allocator>(
1264    entry: OccupiedEntry<K, V, A>,
1265)
1266    ensures
1267        #[trigger] has_resolved(entry) ==> entry.final_value() == Some(entry.value()),
1268;
1269
1270pub broadcast axiom fn axiom_has_resolved_vacant_entry<K, V, A: Allocator>(
1271    entry: VacantEntry<K, V, A>,
1272)
1273    ensures
1274        #[trigger] has_resolved(entry) ==> entry.final_value() == None::<V>,
1275;
1276
1277pub broadcast proof fn axiom_has_resolved_entry<K, V, A: Allocator>(entry: Entry<K, V, A>)
1278    ensures
1279        #[trigger] has_resolved(entry) ==> entry.final_value() == entry.value(),
1280{
1281    broadcast use axiom_has_resolved_occupied_entry;
1282    broadcast use axiom_has_resolved_vacant_entry;
1283
1284}
1285
1286pub assume_specification<'a, Key: Hash + Eq, Value, S: BuildHasher, A: Allocator>[ HashMap::<
1287    Key,
1288    Value,
1289    S,
1290    A,
1291>::entry ](m: &'a mut HashMap<Key, Value, S, A>, key: Key) -> (entry: Entry<'a, Key, Value, A>)
1292    ensures
1293        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> (entry.key() == key
1294            && entry.value() == old(m)@.get(key) && final(m)@ == (match entry.final_value() {
1295            Some(value) => old(m)@.insert(key, value),
1296            None => old(m)@.remove(key),
1297        })),
1298;
1299
1300//// Entry
1301#[verifier::allow_in_spec]
1302pub assume_specification<'a, 'b, K, V, A: Allocator>[ Entry::key ](
1303    entry: &'b Entry::<'a, K, V, A>,
1304) -> (key: &'b K)
1305    returns
1306        &entry.spec_key(),
1307;
1308
1309pub assume_specification<'a, K, V, A: Allocator>[ Entry::or_insert ](
1310    entry: Entry::<'a, K, V, A>,
1311    default: V,
1312) -> (value: &'a mut V)
1313    ensures
1314        *value == (match entry.value() {
1315            Some(v) => v,
1316            None => default,
1317        }),
1318        entry.final_value() == Some(*final(value)),
1319;
1320
1321pub assume_specification<'a, K, V, A: Allocator>[ Entry::insert_entry ](
1322    entry: Entry::<'a, K, V, A>,
1323    value: V,
1324) -> (occ_entry: OccupiedEntry<'a, K, V, A>)
1325    ensures
1326        occ_entry.key() == entry.key(),
1327        occ_entry.value() == value,
1328        entry.final_value() == occ_entry.final_value(),
1329;
1330
1331//// OccupiedEntry
1332// This module works around a bug with `allow_in_spec` that creates duplicate spec fn names
1333mod m_occ {
1334    use super::*;
1335
1336    #[verifier::allow_in_spec]
1337    pub assume_specification<'a, 'b, K, V, A: Allocator>[ OccupiedEntry::key ](
1338        entry: &'b OccupiedEntry::<'a, K, V, A>,
1339    ) -> (key: &'b K)
1340        returns
1341            &entry.spec_key(),
1342    ;
1343
1344}
1345
1346pub assume_specification<'a, K, V, A: Allocator>[ OccupiedEntry::remove_entry ](
1347    entry: OccupiedEntry::<'a, K, V, A>,
1348) -> (kv: (K, V))
1349    ensures
1350        entry.final_value() == None,
1351    returns
1352        (*entry.key(), entry.value()),
1353;
1354
1355pub assume_specification<'a, 'b, K, V, A: Allocator>[ OccupiedEntry::get ](
1356    entry: &'b OccupiedEntry::<'a, K, V, A>,
1357) -> (value: &'b V)
1358    ensures
1359        *value == entry.value(),
1360;
1361
1362pub assume_specification<'a, 'b, K, V, A: Allocator>[ OccupiedEntry::get_mut ](
1363    entry: &'b mut OccupiedEntry::<'a, K, V, A>,
1364) -> (value: &'b mut V)
1365    ensures
1366        *value == old(entry).value(),
1367        final(entry).key() == old(entry).key(),
1368        final(entry).value() == *final(value),
1369        final(entry).final_value() == old(entry).final_value(),
1370;
1371
1372pub assume_specification<'a, K, V, A: Allocator>[ OccupiedEntry::into_mut ](
1373    entry: OccupiedEntry::<'a, K, V, A>,
1374) -> (value: &mut V)
1375    ensures
1376        *value == entry.value(),
1377        entry.final_value() == Some(*final(value)),
1378;
1379
1380pub assume_specification<'a, K, V, A: Allocator>[ OccupiedEntry::insert ](
1381    entry: &mut OccupiedEntry::<'a, K, V, A>,
1382    value: V,
1383) -> (old_value: V)
1384    ensures
1385        old_value == old(entry).value(),
1386        final(entry).key() == old(entry).key(),
1387        final(entry).value() == value,
1388        final(entry).final_value() == old(entry).final_value(),
1389;
1390
1391pub assume_specification<'a, K, V, A: Allocator>[ OccupiedEntry::remove ](
1392    entry: OccupiedEntry::<'a, K, V, A>,
1393) -> (value: V)
1394    ensures
1395        value == entry.value(),
1396        entry.final_value() == None,
1397;
1398
1399//// VacantEntry
1400// This module works around a bug with `allow_in_spec` that creates duplicate spec fn names
1401mod m_vac {
1402    use super::*;
1403
1404    #[verifier::allow_in_spec]
1405    pub assume_specification<'a, 'b, K: 'a, V: 'a, A: Allocator>[ VacantEntry::key ](
1406        entry: &'b VacantEntry::<'a, K, V, A>,
1407    ) -> (key: &'b K)
1408        returns
1409            &entry.spec_key(),
1410    ;
1411
1412}
1413
1414pub assume_specification<'a, K: 'a, V: 'a, A: Allocator>[ VacantEntry::into_key ](
1415    entry: VacantEntry::<'a, K, V, A>,
1416) -> (key: K)
1417    ensures
1418        key == entry.key(),
1419        entry.final_value() == None,
1420;
1421
1422pub assume_specification<'a, K: 'a, V: 'a, A: Allocator>[ VacantEntry::insert ](
1423    entry: VacantEntry::<'a, K, V, A>,
1424    value: V,
1425) -> (value_ref: &mut V)
1426    ensures
1427        *value_ref == value,
1428        entry.final_value() == Some(*final(value_ref)),
1429;
1430
1431pub assume_specification<'a, K: 'a, V: 'a, A: Allocator>[ VacantEntry::insert_entry ](
1432    entry: VacantEntry::<'a, K, V, A>,
1433    value: V,
1434) -> (occ_entry: OccupiedEntry::<'a, K, V, A>)
1435    ensures
1436        occ_entry.key() == entry.key(),
1437        occ_entry.value() == value,
1438        entry.final_value() == occ_entry.final_value(),
1439;
1440
1441pub broadcast group group_hash_axioms {
1442    axiom_box_key_removed,
1443    axiom_contains_deref_key,
1444    axiom_contains_box,
1445    axiom_deref_key_removed,
1446    axiom_maps_deref_key_to_value,
1447    axiom_maps_box_key_to_value,
1448    axiom_hashmap_deepview_borrow,
1449    axiom_bool_obeys_hash_table_key_model,
1450    axiom_u8_obeys_hash_table_key_model,
1451    axiom_u16_obeys_hash_table_key_model,
1452    axiom_u32_obeys_hash_table_key_model,
1453    axiom_u64_obeys_hash_table_key_model,
1454    axiom_u128_obeys_hash_table_key_model,
1455    axiom_usize_obeys_hash_table_key_model,
1456    axiom_i8_obeys_hash_table_key_model,
1457    axiom_i16_obeys_hash_table_key_model,
1458    axiom_i32_obeys_hash_table_key_model,
1459    axiom_i64_obeys_hash_table_key_model,
1460    axiom_i128_obeys_hash_table_key_model,
1461    axiom_isize_obeys_hash_table_key_model,
1462    axiom_box_bool_obeys_hash_table_key_model,
1463    axiom_box_integer_type_obeys_hash_table_key_model,
1464    axiom_random_state_builds_valid_hashers,
1465    axiom_spec_hash_map_len,
1466    axiom_set_box_key_removed,
1467    axiom_set_contains_deref_key,
1468    axiom_set_contains_box,
1469    axiom_set_deref_key_removed,
1470    axiom_set_deref_key_to_value,
1471    axiom_set_box_key_to_value,
1472    axiom_spec_hash_set_len,
1473    axiom_hashmap_decreases,
1474    axiom_hashset_decreases,
1475    axiom_has_resolved_occupied_entry,
1476    axiom_has_resolved_vacant_entry,
1477    axiom_has_resolved_entry,
1478}
1479
1480} // verus!
vstd/std_specs/hash.rs

vstd/std_specs/
hash.rs
