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

vstd/std_specs/
hash.rs
