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

vstd/std_specs/
hash.rs
