vstd/std_specs/
hash.rs

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

vstd/std_specs/
hash.rs
