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<Key, Value>[ HashMap::<Key, Value>::with_capacity ](capacity: usize) -> (m:
836    HashMap<Key, Value, RandomState>)
837    ensures
838        m@ == Map::<Key, Value>::empty(),
839;
840
841pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<
842    Key,
843    Value,
844    S,
845>::reserve ](m: &mut HashMap<Key, Value, S>, additional: usize)
846    ensures
847        m@ == old(m)@,
848;
849
850pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<Key, Value, S>::insert ](
851    m: &mut HashMap<Key, Value, S>,
852    k: Key,
853    v: Value,
854) -> (result: Option<Value>)
855    ensures
856        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
857            &&& m@ == old(m)@.insert(k, v)
858            &&& match result {
859                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
860                None => !old(m)@.contains_key(k),
861            }
862        },
863;
864
865// The specification for `contains_key` has a parameter `key: &Q`
866// where you'd expect to find `key: &Key`. This allows for the case
867// that `Key` can be borrowed as something other than `&Key`. For
868// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
869// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
870// respectively.
871// To deal with this, we have a specification function that opaquely
872// specifies what it means for a map to contain a borrowed key of type
873// `&Q`. And the postcondition of `contains_key` just says that its
874// result matches the output of that specification function. But this
875// isn't very helpful by itself, since there's no body to that
876// specification function. So we have special-case axioms that say
877// what this means in two important circumstances: (1) `Key = Q` and
878// (2) `Key = Box<Q>`.
879pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
880    m: Map<Key, Value>,
881    k: &Q,
882) -> bool;
883
884pub broadcast proof fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
885    ensures
886        #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
887{
888    admit();
889}
890
891pub broadcast proof fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
892    ensures
893        #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
894            Box::new(*k),
895        ),
896{
897    admit();
898}
899
900pub assume_specification<
901    Key: Borrow<Q> + Hash + Eq,
902    Value,
903    S: BuildHasher,
904    Q: Hash + Eq + ?Sized,
905>[ HashMap::<Key, Value, S>::contains_key::<Q> ](m: &HashMap<Key, Value, S>, k: &Q) -> (result:
906    bool)
907    ensures
908        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result == contains_borrowed_key(
909            m@,
910            k,
911        ),
912;
913
914// The specification for `get` has a parameter `key: &Q` where you'd
915// expect to find `key: &Key`. This allows for the case that `Key` can
916// be borrowed as something other than `&Key`. For instance,
917// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
918// as `&str`, so in those cases `Q` would be `u32` and `str`
919// respectively.
920// To deal with this, we have a specification function that opaquely
921// specifies what it means for a map to map a borrowed key of type
922// `&Q` to a certain value. And the postcondition of `get` says that
923// its result matches the output of that specification function. (It
924// also says that its result corresponds to the output of
925// `contains_borrowed_key`, discussed above.) But this isn't very
926// helpful by itself, since there's no body to that specification
927// function. So we have special-case axioms that say what this means
928// in two important circumstances: (1) `Key = Q` and (2) `Key =
929// Box<Q>`.
930pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
931    m: Map<Key, Value>,
932    k: &Q,
933    v: Value,
934) -> bool;
935
936pub broadcast proof fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
937    ensures
938        #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
939            && m[*k] == v,
940{
941    admit();
942}
943
944pub broadcast proof fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
945    ensures
946        #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
947            let k = Box::new(*q);
948            &&& m.contains_key(k)
949            &&& m[k] == v
950        },
951{
952    admit();
953}
954
955pub assume_specification<
956    'a,
957    Key: Borrow<Q> + Hash + Eq,
958    Value,
959    S: BuildHasher,
960    Q: Hash + Eq + ?Sized,
961>[ HashMap::<Key, Value, S>::get::<Q> ](m: &'a HashMap<Key, Value, S>, k: &Q) -> (result: Option<
962    &'a Value,
963>)
964    ensures
965        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
966            Some(v) => maps_borrowed_key_to_value(m@, k, *v),
967            None => !contains_borrowed_key(m@, k),
968        },
969;
970
971// The specification for `remove` has a parameter `key: &Q` where
972// you'd expect to find `key: &Key`. This allows for the case that
973// `Key` can be borrowed as something other than `&Key`. For instance,
974// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
975// as `&str`, so in those cases `Q` would be `u32` and `str`
976// respectively. To deal with this, we have a specification function
977// that opaquely specifies what it means for two maps to be related by
978// a remove of a certain `&Q`. And the postcondition of `remove` says
979// that `old(self)@` and `self@` satisfy that relationship. (It also
980// says that its result corresponds to the output of
981// `contains_borrowed_key` and `maps_borrowed_key_to_value`, discussed
982// above.) But this isn't very helpful by itself, since there's no
983// body to that specification function. So we have special-case axioms
984// that say what this means in two important circumstances: (1) `Key =
985// Q` and (2) `Key = Box<Q>`.
986pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
987    old_m: Map<Key, Value>,
988    new_m: Map<Key, Value>,
989    k: &Q,
990) -> bool;
991
992pub broadcast proof fn axiom_deref_key_removed<Q, Value>(
993    old_m: Map<Q, Value>,
994    new_m: Map<Q, Value>,
995    k: &Q,
996)
997    ensures
998        #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
999            *k,
1000        ),
1001{
1002    admit();
1003}
1004
1005pub broadcast proof fn axiom_box_key_removed<Q, Value>(
1006    old_m: Map<Box<Q>, Value>,
1007    new_m: Map<Box<Q>, Value>,
1008    q: &Q,
1009)
1010    ensures
1011        #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
1012            == old_m.remove(Box::new(*q)),
1013{
1014    admit();
1015}
1016
1017pub assume_specification<
1018    Key: Borrow<Q> + Hash + Eq,
1019    Value,
1020    S: BuildHasher,
1021    Q: Hash + Eq + ?Sized,
1022>[ HashMap::<Key, Value, S>::remove::<Q> ](m: &mut HashMap<Key, Value, S>, k: &Q) -> (result:
1023    Option<Value>)
1024    ensures
1025        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1026            &&& borrowed_key_removed(old(m)@, m@, k)
1027            &&& match result {
1028                Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
1029                None => !contains_borrowed_key(old(m)@, k),
1030            }
1031        },
1032;
1033
1034pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::clear ](
1035    m: &mut HashMap<Key, Value, S>,
1036)
1037    ensures
1038        m@ == Map::<Key, Value>::empty(),
1039;
1040
1041pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::keys ](
1042    m: &'a HashMap<Key, Value, S>,
1043) -> (keys: Keys<'a, Key, Value>)
1044    ensures
1045        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1046            let (index, s) = keys@;
1047            &&& index == 0
1048            &&& s.to_set() == m@.dom()
1049            &&& s.no_duplicates()
1050        },
1051;
1052
1053pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::values ](
1054    m: &'a HashMap<Key, Value, S>,
1055) -> (values: Values<'a, Key, Value>)
1056    ensures
1057        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1058            let (index, s) = values@;
1059            &&& index == 0
1060            &&& s.to_set() == m@.values()
1061        },
1062;
1063
1064pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
1065    ensures
1066        #[trigger] (decreases_to!(m => m@)),
1067{
1068    admit();
1069}
1070
1071// The `iter` method of a `HashSet` returns an iterator of type `hash_set::Iter`,
1072// so we specify that type here.
1073#[verifier::external_type_specification]
1074#[verifier::external_body]
1075#[verifier::accept_recursive_types(Key)]
1076pub struct ExSetIter<'a, Key: 'a>(hash_set::Iter<'a, Key>);
1077
1078pub trait SetIterAdditionalSpecFns<'a, Key: 'a> {
1079    spec fn view(self: &Self) -> (int, Seq<Key>);
1080}
1081
1082impl<'a, Key: 'a> SetIterAdditionalSpecFns<'a, Key> for hash_set::Iter<'a, Key> {
1083    uninterp spec fn view(self: &hash_set::Iter<'a, Key>) -> (int, Seq<Key>);
1084}
1085
1086pub assume_specification<'a, Key>[ hash_set::Iter::<'a, Key>::next ](
1087    elements: &mut hash_set::Iter<'a, Key>,
1088) -> (r: Option<&'a Key>)
1089    ensures
1090        ({
1091            let (old_index, old_seq) = old(elements)@;
1092            match r {
1093                None => {
1094                    &&& elements@ == old(elements)@
1095                    &&& old_index >= old_seq.len()
1096                },
1097                Some(element) => {
1098                    let (new_index, new_seq) = elements@;
1099                    &&& 0 <= old_index < old_seq.len()
1100                    &&& new_seq == old_seq
1101                    &&& new_index == old_index + 1
1102                    &&& element == old_seq[old_index]
1103                },
1104            }
1105        }),
1106;
1107
1108pub struct SetIterGhostIterator<'a, Key> {
1109    pub pos: int,
1110    pub elements: Seq<Key>,
1111    pub phantom: Option<&'a Key>,
1112}
1113
1114impl<'a, Key> super::super::pervasive::ForLoopGhostIteratorNew for hash_set::Iter<'a, Key> {
1115    type GhostIter = SetIterGhostIterator<'a, Key>;
1116
1117    open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key> {
1118        SetIterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
1119    }
1120}
1121
1122impl<'a, Key: 'a> super::super::pervasive::ForLoopGhostIterator for SetIterGhostIterator<'a, Key> {
1123    type ExecIter = hash_set::Iter<'a, Key>;
1124
1125    type Item = Key;
1126
1127    type Decrease = int;
1128
1129    open spec fn exec_invariant(&self, exec_iter: &hash_set::Iter<'a, Key>) -> bool {
1130        &&& self.pos == exec_iter@.0
1131        &&& self.elements == exec_iter@.1
1132    }
1133
1134    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
1135        init matches Some(init) ==> {
1136            &&& init.pos == 0
1137            &&& init.elements == self.elements
1138            &&& 0 <= self.pos <= self.elements.len()
1139        }
1140    }
1141
1142    open spec fn ghost_ensures(&self) -> bool {
1143        self.pos == self.elements.len()
1144    }
1145
1146    open spec fn ghost_decrease(&self) -> Option<int> {
1147        Some(self.elements.len() - self.pos)
1148    }
1149
1150    open spec fn ghost_peek_next(&self) -> Option<Key> {
1151        if 0 <= self.pos < self.elements.len() {
1152            Some(self.elements[self.pos])
1153        } else {
1154            None
1155        }
1156    }
1157
1158    open spec fn ghost_advance(&self, _exec_iter: &hash_set::Iter<'a, Key>) -> SetIterGhostIterator<
1159        'a,
1160        Key,
1161    > {
1162        Self { pos: self.pos + 1, ..*self }
1163    }
1164}
1165
1166impl<'a, Key> View for SetIterGhostIterator<'a, Key> {
1167    type V = Seq<Key>;
1168
1169    open spec fn view(&self) -> Seq<Key> {
1170        self.elements.take(self.pos)
1171    }
1172}
1173
1174/// Specifications for the behavior of [`std::collections::HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html).
1175///
1176/// We model a `HashSet` as having a view of type `Set<Key>`, which reflects the current state of the set.
1177///
1178/// These specifications are only meaningful if `obeys_key_model::<Key>()` and `builds_valid_hashers::<S>()` hold.
1179/// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
1180/// for information on use with primitive types and custom types,
1181/// and see [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
1182/// for information on use with Rust's default implementation and custom implementations.
1183///
1184/// Axioms about the behavior of HashSet are present in the broadcast group `vstd::std_specs::hash::group_hash_axioms`.
1185#[verifier::external_type_specification]
1186#[verifier::external_body]
1187#[verifier::accept_recursive_types(Key)]
1188#[verifier::reject_recursive_types(S)]
1189pub struct ExHashSet<Key, S>(HashSet<Key, S>);
1190
1191impl<Key, S> View for HashSet<Key, S> {
1192    type V = Set<Key>;
1193
1194    uninterp spec fn view(&self) -> Set<Key>;
1195}
1196
1197pub uninterp spec fn spec_hash_set_len<Key, S>(m: &HashSet<Key, S>) -> usize;
1198
1199pub broadcast proof fn axiom_spec_hash_set_len<Key, S>(m: &HashSet<Key, S>)
1200    ensures
1201        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_set_len(m)
1202            == m@.len(),
1203{
1204    admit();
1205}
1206
1207#[verifier::when_used_as_spec(spec_hash_set_len)]
1208pub assume_specification<Key, S>[ HashSet::<Key, S>::len ](m: &HashSet<Key, S>) -> (len: usize)
1209    ensures
1210        len == spec_hash_set_len(m),
1211;
1212
1213pub assume_specification<Key, S>[ HashSet::<Key, S>::is_empty ](m: &HashSet<Key, S>) -> (res: bool)
1214    ensures
1215        res == m@.is_empty(),
1216;
1217
1218pub assume_specification<Key>[ HashSet::<Key>::new ]() -> (m: HashSet<Key, RandomState>)
1219    ensures
1220        m@ == Set::<Key>::empty(),
1221;
1222
1223pub assume_specification<Key>[ HashSet::<Key>::with_capacity ](capacity: usize) -> (m: HashSet<
1224    Key,
1225    RandomState,
1226>)
1227    ensures
1228        m@ == Set::<Key>::empty(),
1229;
1230
1231pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::reserve ](
1232    m: &mut HashSet<Key, S>,
1233    additional: usize,
1234)
1235    ensures
1236        m@ == old(m)@,
1237;
1238
1239pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::insert ](
1240    m: &mut HashSet<Key, S>,
1241    k: Key,
1242) -> (result: bool)
1243    ensures
1244        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1245            &&& m@ == old(m)@.insert(k)
1246            &&& result == !old(m)@.contains(k)
1247        },
1248;
1249
1250// The specification for `contains` has a parameter `key: &Q`
1251// where you'd expect to find `key: &Key`. This allows for the case
1252// that `Key` can be borrowed as something other than `&Key`. For
1253// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
1254// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
1255// respectively.
1256// To deal with this, we have a specification function that opaquely
1257// specifies what it means for a set to contain a borrowed key of type
1258// `&Q`. And the postcondition of `contains` just says that its
1259// result matches the output of that specification function. But this
1260// isn't very helpful by itself, since there's no body to that
1261// specification function. So we have special-case axioms that say
1262// what this means in two important circumstances: (1) `Key = Q` and
1263// (2) `Key = Box<Q>`.
1264pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
1265
1266pub broadcast proof fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
1267    ensures
1268        #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
1269{
1270    admit();
1271}
1272
1273pub broadcast proof fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
1274    ensures
1275        #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
1276{
1277    admit();
1278}
1279
1280pub assume_specification<
1281    Key: Borrow<Q> + Hash + Eq,
1282    S: BuildHasher,
1283    Q: Hash + Eq + ?Sized,
1284>[ HashSet::<Key, S>::contains ](m: &HashSet<Key, S>, k: &Q) -> (result: bool)
1285    ensures
1286        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result
1287            == set_contains_borrowed_key(m@, k),
1288;
1289
1290// The specification for `get` has a parameter `key: &Q` where you'd
1291// expect to find `key: &Key`. This allows for the case that `Key` can
1292// be borrowed as something other than `&Key`. For instance,
1293// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1294// as `&str`, so in those cases `Q` would be `u32` and `str`
1295// respectively.
1296// To deal with this, we have a specification function that opaquely
1297// specifies what it means for a returned reference to point to an
1298// element of a HashSet. And the postcondition of `get` says that
1299// its result matches the output of that specification function. (It
1300// also says that its result corresponds to the output of
1301// `contains_borrowed_key`, discussed above.) But this isn't very
1302// helpful by itself, since there's no body to that specification
1303// function. So we have special-case axioms that say what this means
1304// in two important circumstances: (1) `Key = Q` and (2) `Key =
1305// Box<Q>`.
1306pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
1307
1308pub broadcast proof fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
1309    ensures
1310        #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
1311{
1312    admit();
1313}
1314
1315pub broadcast proof fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
1316    ensures
1317        #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
1318            *q,
1319        ) == v),
1320{
1321    admit();
1322}
1323
1324pub assume_specification<
1325    'a,
1326    Key: Borrow<Q> + Hash + Eq,
1327    S: BuildHasher,
1328    Q: Hash + Eq + ?Sized,
1329>[ HashSet::<Key, S>::get::<Q> ](m: &'a HashSet<Key, S>, k: &Q) -> (result: Option<&'a Key>)
1330    ensures
1331        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
1332            Some(v) => sets_borrowed_key_to_key(m@, k, v),
1333            None => !set_contains_borrowed_key(m@, k),
1334        },
1335;
1336
1337// The specification for `remove` has a parameter `key: &Q` where
1338// you'd expect to find `key: &Key`. This allows for the case that
1339// `Key` can be borrowed as something other than `&Key`. For instance,
1340// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1341// as `&str`, so in those cases `Q` would be `u32` and `str`
1342// respectively. To deal with this, we have a specification function
1343// that opaquely specifies what it means for two sets to be related by
1344// a remove of a certain `&Q`. And the postcondition of `remove` says
1345// that `old(self)@` and `self@` satisfy that relationship. (It also
1346// says that its result corresponds to the output of
1347// `set_contains_borrowed_key`, discussed above.) But this isn't very
1348// helpful by itself, since there's no body to that specification
1349// function. So we have special-case axioms that say what this means
1350// in two important circumstances: (1) `Key = Q` and (2) `Key = Box<Q>`.
1351pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
1352    old_m: Set<Key>,
1353    new_m: Set<Key>,
1354    k: &Q,
1355) -> bool;
1356
1357pub broadcast proof fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
1358    ensures
1359        #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
1360            *k,
1361        ),
1362{
1363    admit();
1364}
1365
1366pub broadcast proof fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
1367    ensures
1368        #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
1369            == old_m.remove(Box::new(*q)),
1370{
1371    admit();
1372}
1373
1374pub assume_specification<
1375    Key: Borrow<Q> + Hash + Eq,
1376    S: BuildHasher,
1377    Q: Hash + Eq + ?Sized,
1378>[ HashSet::<Key, S>::remove::<Q> ](m: &mut HashSet<Key, S>, k: &Q) -> (result: bool)
1379    ensures
1380        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1381            &&& sets_differ_by_borrowed_key(old(m)@, m@, k)
1382            &&& result == set_contains_borrowed_key(old(m)@, k)
1383        },
1384;
1385
1386pub assume_specification<Key, S>[ HashSet::<Key, S>::clear ](m: &mut HashSet<Key, S>)
1387    ensures
1388        m@ == Set::<Key>::empty(),
1389;
1390
1391pub assume_specification<'a, Key, S>[ HashSet::<Key, S>::iter ](m: &'a HashSet<Key, S>) -> (r:
1392    hash_set::Iter<'a, Key>)
1393    ensures
1394        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1395            let (index, s) = r@;
1396            &&& index == 0
1397            &&& s.to_set() == m@
1398            &&& s.no_duplicates()
1399        },
1400;
1401
1402pub broadcast proof fn axiom_hashset_decreases<Key, S>(m: HashSet<Key, S>)
1403    ensures
1404        #[trigger] (decreases_to!(m => m@)),
1405{
1406    admit();
1407}
1408
1409pub broadcast group group_hash_axioms {
1410    axiom_box_key_removed,
1411    axiom_contains_deref_key,
1412    axiom_contains_box,
1413    axiom_deref_key_removed,
1414    axiom_maps_deref_key_to_value,
1415    axiom_maps_box_key_to_value,
1416    axiom_hashmap_deepview_borrow,
1417    axiom_hashmap_view_finite_dom,
1418    axiom_bool_obeys_hash_table_key_model,
1419    axiom_u8_obeys_hash_table_key_model,
1420    axiom_u16_obeys_hash_table_key_model,
1421    axiom_u32_obeys_hash_table_key_model,
1422    axiom_u64_obeys_hash_table_key_model,
1423    axiom_u128_obeys_hash_table_key_model,
1424    axiom_usize_obeys_hash_table_key_model,
1425    axiom_i8_obeys_hash_table_key_model,
1426    axiom_i16_obeys_hash_table_key_model,
1427    axiom_i32_obeys_hash_table_key_model,
1428    axiom_i164_obeys_hash_table_key_model,
1429    axiom_i128_obeys_hash_table_key_model,
1430    axiom_isize_obeys_hash_table_key_model,
1431    axiom_box_bool_obeys_hash_table_key_model,
1432    axiom_box_integer_type_obeys_hash_table_key_model,
1433    axiom_random_state_builds_valid_hashers,
1434    axiom_spec_hash_map_len,
1435    axiom_set_box_key_removed,
1436    axiom_set_contains_deref_key,
1437    axiom_set_contains_box,
1438    axiom_set_deref_key_removed,
1439    axiom_set_deref_key_to_value,
1440    axiom_set_box_key_to_value,
1441    axiom_spec_hash_set_len,
1442    axiom_spec_hash_map_iter,
1443    axiom_hashmap_decreases,
1444    axiom_hashset_decreases,
1445}
1446
1447} // verus!
vstd/std_specs/hash.rs

vstd/std_specs/
hash.rs
