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_i64_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
277impl<'a, Key, Value> View for Keys<'a, Key, Value> {
278    type V = (int, Seq<Key>);
279
280    uninterp spec fn view(self: &Keys<'a, Key, Value>) -> (int, Seq<Key>);
281}
282
283pub assume_specification<'a, Key, Value>[ Keys::<'a, Key, Value>::next ](
284    keys: &mut Keys<'a, Key, Value>,
285) -> (r: Option<&'a Key>)
286    ensures
287        ({
288            let (old_index, old_seq) = old(keys)@;
289            match r {
290                None => {
291                    &&& keys@ == old(keys)@
292                    &&& old_index >= old_seq.len()
293                },
294                Some(k) => {
295                    let (new_index, new_seq) = keys@;
296                    &&& 0 <= old_index < old_seq.len()
297                    &&& new_seq == old_seq
298                    &&& new_index == old_index + 1
299                    &&& k == old_seq[old_index]
300                },
301            }
302        }),
303;
304
305pub struct KeysGhostIterator<'a, Key, Value> {
306    pub pos: int,
307    pub keys: Seq<Key>,
308    pub phantom: Option<&'a Value>,
309}
310
311impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Keys<'a, Key, Value> {
312    type GhostIter = KeysGhostIterator<'a, Key, Value>;
313
314    open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value> {
315        KeysGhostIterator { pos: self@.0, keys: self@.1, phantom: None }
316    }
317}
318
319impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for KeysGhostIterator<
320    'a,
321    Key,
322    Value,
323> {
324    type ExecIter = Keys<'a, Key, Value>;
325
326    type Item = Key;
327
328    type Decrease = int;
329
330    open spec fn exec_invariant(&self, exec_iter: &Keys<'a, Key, Value>) -> bool {
331        &&& self.pos == exec_iter@.0
332        &&& self.keys == exec_iter@.1
333    }
334
335    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
336        init matches Some(init) ==> {
337            &&& init.pos == 0
338            &&& init.keys == self.keys
339            &&& 0 <= self.pos <= self.keys.len()
340        }
341    }
342
343    open spec fn ghost_ensures(&self) -> bool {
344        self.pos == self.keys.len()
345    }
346
347    open spec fn ghost_decrease(&self) -> Option<int> {
348        Some(self.keys.len() - self.pos)
349    }
350
351    open spec fn ghost_peek_next(&self) -> Option<Key> {
352        if 0 <= self.pos < self.keys.len() {
353            Some(self.keys[self.pos])
354        } else {
355            None
356        }
357    }
358
359    open spec fn ghost_advance(&self, _exec_iter: &Keys<'a, Key, Value>) -> KeysGhostIterator<
360        'a,
361        Key,
362        Value,
363    > {
364        Self { pos: self.pos + 1, ..*self }
365    }
366}
367
368impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value> {
369    type V = Seq<Key>;
370
371    open spec fn view(&self) -> Seq<Key> {
372        self.keys.take(self.pos)
373    }
374}
375
376/// Specifications for the behavior of
377/// [`std::collections::hash_map::Values`](https://doc.rust-lang.org/std/collections/hash_map/struct.Values.html).
378#[verifier::external_type_specification]
379#[verifier::external_body]
380#[verifier::accept_recursive_types(Key)]
381#[verifier::accept_recursive_types(Value)]
382pub struct ExValues<'a, Key: 'a, Value: 'a>(Values<'a, Key, Value>);
383
384impl<'a, Key: 'a, Value: 'a> View for Values<'a, Key, Value> {
385    type V = (int, Seq<Value>);
386
387    uninterp spec fn view(self: &Values<'a, Key, Value>) -> (int, Seq<Value>);
388}
389
390pub assume_specification<'a, Key, Value>[ Values::<'a, Key, Value>::next ](
391    values: &mut Values<'a, Key, Value>,
392) -> (r: Option<&'a Value>)
393    ensures
394        ({
395            let (old_index, old_seq) = old(values)@;
396            match r {
397                None => {
398                    &&& values@ == old(values)@
399                    &&& old_index >= old_seq.len()
400                },
401                Some(v) => {
402                    let (new_index, new_seq) = values@;
403                    &&& 0 <= old_index < old_seq.len()
404                    &&& new_seq == old_seq
405                    &&& new_index == old_index + 1
406                    &&& v == old_seq[old_index]
407                },
408            }
409        }),
410;
411
412pub struct ValuesGhostIterator<'a, Key, Value> {
413    pub pos: int,
414    pub values: Seq<Value>,
415    pub phantom: Option<&'a Key>,
416}
417
418impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Values<'a, Key, Value> {
419    type GhostIter = ValuesGhostIterator<'a, Key, Value>;
420
421    open spec fn ghost_iter(&self) -> ValuesGhostIterator<'a, Key, Value> {
422        ValuesGhostIterator { pos: self@.0, values: self@.1, phantom: None }
423    }
424}
425
426impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for ValuesGhostIterator<
427    'a,
428    Key,
429    Value,
430> {
431    type ExecIter = Values<'a, Key, Value>;
432
433    type Item = Value;
434
435    type Decrease = int;
436
437    open spec fn exec_invariant(&self, exec_iter: &Values<'a, Key, Value>) -> bool {
438        &&& self.pos == exec_iter@.0
439        &&& self.values == exec_iter@.1
440    }
441
442    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
443        init matches Some(init) ==> {
444            &&& init.pos == 0
445            &&& init.values == self.values
446            &&& 0 <= self.pos <= self.values.len()
447        }
448    }
449
450    open spec fn ghost_ensures(&self) -> bool {
451        self.pos == self.values.len()
452    }
453
454    open spec fn ghost_decrease(&self) -> Option<int> {
455        Some(self.values.len() - self.pos)
456    }
457
458    open spec fn ghost_peek_next(&self) -> Option<Value> {
459        if 0 <= self.pos < self.values.len() {
460            Some(self.values[self.pos])
461        } else {
462            None
463        }
464    }
465
466    open spec fn ghost_advance(&self, _exec_iter: &Values<'a, Key, Value>) -> ValuesGhostIterator<
467        'a,
468        Key,
469        Value,
470    > {
471        Self { pos: self.pos + 1, ..*self }
472    }
473}
474
475impl<'a, Key, Value> View for ValuesGhostIterator<'a, Key, Value> {
476    type V = Seq<Value>;
477
478    open spec fn view(&self) -> Seq<Value> {
479        self.values.take(self.pos)
480    }
481}
482
483// The `iter` method of a `HashMap` returns an iterator of type `hash_map::Iter`,
484// so we specify that type here.
485#[verifier::external_type_specification]
486#[verifier::external_body]
487#[verifier::accept_recursive_types(Key)]
488#[verifier::accept_recursive_types(Value)]
489pub struct ExMapIter<'a, Key: 'a, Value: 'a>(hash_map::Iter<'a, Key, Value>);
490
491impl<'a, Key: 'a, Value: 'a> View for hash_map::Iter<'a, Key, Value> {
492    type V = (int, Seq<(Key, Value)>);
493
494    uninterp spec fn view(self: &hash_map::Iter<'a, Key, Value>) -> (int, Seq<(Key, Value)>);
495}
496
497pub assume_specification<'a, Key, Value>[ hash_map::Iter::<'a, Key, Value>::next ](
498    iter: &mut hash_map::Iter<'a, Key, Value>,
499) -> (r: Option<(&'a Key, &'a Value)>)
500    ensures
501        ({
502            let (old_index, old_seq) = old(iter)@;
503            match r {
504                None => {
505                    &&& iter@ == old(iter)@
506                    &&& old_index >= old_seq.len()
507                },
508                Some((k, v)) => {
509                    let (new_index, new_seq) = iter@;
510                    let (old_k, old_v) = old_seq[old_index];
511                    &&& 0 <= old_index < old_seq.len()
512                    &&& new_seq == old_seq
513                    &&& new_index == old_index + 1
514                    &&& k == old_k
515                    &&& v == old_v
516                    &&& old_seq.to_set().contains((*k, *v))
517                },
518            }
519        }),
520;
521
522pub struct MapIterGhostIterator<'a, Key, Value> {
523    pub pos: int,
524    pub kv_pairs: Seq<(Key, Value)>,
525    pub _marker: PhantomData<&'a Key>,
526}
527
528impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for hash_map::Iter<
529    'a,
530    Key,
531    Value,
532> {
533    type GhostIter = MapIterGhostIterator<'a, Key, Value>;
534
535    open spec fn ghost_iter(&self) -> MapIterGhostIterator<'a, Key, Value> {
536        MapIterGhostIterator { pos: self@.0, kv_pairs: self@.1, _marker: PhantomData }
537    }
538}
539
540impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for MapIterGhostIterator<
541    'a,
542    Key,
543    Value,
544> {
545    type ExecIter = hash_map::Iter<'a, Key, Value>;
546
547    type Item = (Key, Value);
548
549    type Decrease = int;
550
551    open spec fn exec_invariant(&self, exec_iter: &hash_map::Iter<'a, Key, Value>) -> bool {
552        &&& self.pos == exec_iter@.0
553        &&& self.kv_pairs == exec_iter@.1
554    }
555
556    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
557        init matches Some(init) ==> {
558            &&& init.pos == 0
559            &&& init.kv_pairs == self.kv_pairs
560            &&& 0 <= self.pos <= self.kv_pairs.len()
561        }
562    }
563
564    open spec fn ghost_ensures(&self) -> bool {
565        self.pos == self.kv_pairs.len()
566    }
567
568    open spec fn ghost_decrease(&self) -> Option<int> {
569        Some(self.kv_pairs.len() - self.pos)
570    }
571
572    open spec fn ghost_peek_next(&self) -> Option<(Key, Value)> {
573        if 0 <= self.pos < self.kv_pairs.len() {
574            Some(self.kv_pairs[self.pos])
575        } else {
576            None
577        }
578    }
579
580    open spec fn ghost_advance(
581        &self,
582        _exec_iter: &hash_map::Iter<'a, Key, Value>,
583    ) -> MapIterGhostIterator<'a, Key, Value> {
584        Self { pos: self.pos + 1, ..*self }
585    }
586}
587
588impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value> {
589    type V = Seq<(Key, Value)>;
590
591    open spec fn view(&self) -> Seq<(Key, Value)> {
592        self.kv_pairs.take(self.pos)
593    }
594}
595
596// To allow reasoning about the ghost iterator when the executable
597// function `iter()` is invoked in a `for` loop header (e.g., in
598// `for x in it: v.iter() { ... }`), we need to specify the behavior of
599// the iterator in spec mode. To do that, we add
600// `#[verifier::when_used_as_spec(spec_iter)]` to the specification for
601// the executable `iter` method and define that spec function here.
602pub uninterp spec fn spec_hash_map_iter<'a, Key, Value, S>(m: &'a HashMap<Key, Value, S>) -> (r:
603    hash_map::Iter<'a, Key, Value>);
604
605pub broadcast proof fn axiom_spec_hash_map_iter<'a, Key, Value, S>(m: &'a HashMap<Key, Value, S>)
606    ensures
607        ({
608            let (pos, v) = #[trigger] spec_hash_map_iter(m)@;
609            &&& pos == 0int
610            &&& forall|i: int| 0 <= i < v.len() ==> #[trigger] m@[v[i].0] == v[i].1
611        }),
612{
613    admit();
614}
615
616#[verifier::when_used_as_spec(spec_hash_map_iter)]
617pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::iter ](
618    m: &'a HashMap<Key, Value, S>,
619) -> (iter: hash_map::Iter<'a, Key, Value>)
620    ensures
621        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
622            let (index, s) = iter@;
623            &&& index == 0
624            &&& s.to_set() == m@.kv_pairs()
625            &&& s.no_duplicates()
626        },
627;
628
629/// Specifications for the behavior of [`std::collections::HashMap`](https://doc.rust-lang.org/std/collections/struct.HashMap.html).
630///
631/// We model a `HashMap` as having a view of type `Map<Key, Value>`, which reflects the current state of the map.
632///
633/// These specifications are only meaningful if `obeys_key_model::<Key>()` and `builds_valid_hashers::<S>()` hold.
634/// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
635/// for information on use with primitive types and other types,
636/// and see [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
637/// for information on use with Rust's default implementation and custom implementations.
638///
639/// Axioms about the behavior of HashMap are present in the broadcast group `vstd::std_specs::hash::group_hash_axioms`.
640#[verifier::external_type_specification]
641#[verifier::external_body]
642#[verifier::accept_recursive_types(Key)]
643#[verifier::accept_recursive_types(Value)]
644#[verifier::reject_recursive_types(S)]
645pub struct ExHashMap<Key, Value, S>(HashMap<Key, Value, S>);
646
647pub trait HashMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
648    spec fn spec_index(&self, k: Key) -> Value
649        recommends
650            self@.contains_key(k),
651    ;
652}
653
654impl<Key, Value, S> HashMapAdditionalSpecFns<Key, Value> for HashMap<Key, Value, S> {
655    #[verifier::inline]
656    open spec fn spec_index(&self, k: Key) -> Value {
657        self@.index(k)
658    }
659}
660
661/// The actual definition of `HashMap::deep_view`.
662///
663/// This is a separate function since it introduces a lot of quantifiers and revealing an opaque trait
664/// method is not supported. In most cases, it's easier to use one of the lemmas below instead
665/// of revealing this function directly.
666#[verifier::opaque]
667pub open spec fn hash_map_deep_view_impl<Key: DeepView, Value: DeepView, S>(
668    m: HashMap<Key, Value, S>,
669) -> Map<Key::V, Value::V> {
670    Map::new(
671        |k: Key::V|
672            exists|orig_k: Key| #[trigger] m@.contains_key(orig_k) && k == orig_k.deep_view(),
673        |dk: Key::V|
674            {
675                let k = choose|k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
676                m@[k].deep_view()
677            },
678    )
679}
680
681pub broadcast proof fn lemma_hashmap_deepview_dom<K: DeepView, V: DeepView>(m: HashMap<K, V>)
682    ensures
683        #[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),
684{
685    reveal(hash_map_deep_view_impl);
686    broadcast use group_hash_axioms;
687    broadcast use crate::vstd::group_vstd_default;
688
689    assert(m.deep_view().dom() =~= m@.dom().map(|k: K| k.deep_view()));
690}
691
692pub broadcast proof fn lemma_hashmap_deepview_properties<K: DeepView, V: DeepView>(m: HashMap<K, V>)
693    requires
694        crate::relations::injective(|k: K| k.deep_view()),
695    ensures
696        #![trigger m.deep_view()]
697        // all elements in m.view() are present in m.deep_view()
698        forall|k: K| #[trigger]
699            m@.contains_key(k) ==> m.deep_view().contains_key(k.deep_view())
700                && m.deep_view()[k.deep_view()] == m@[k].deep_view(),
701        // all elements in m.deep_view() are present in m.view()
702        forall|dk: <K as DeepView>::V| #[trigger]
703            m.deep_view().contains_key(dk) ==> exists|k: K|
704                k.deep_view() == dk && #[trigger] m@.contains_key(k),
705{
706    reveal(hash_map_deep_view_impl);
707    broadcast use group_hash_axioms;
708    broadcast use crate::vstd::group_vstd_default;
709
710    assert(m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()));
711    assert forall|k: K| #[trigger] m@.contains_key(k) implies m.deep_view().contains_key(
712        k.deep_view(),
713    ) && m.deep_view()[k.deep_view()] == m@[k].deep_view() by {
714        assert forall|k1: K, k2: K| #[trigger]
715            k1.deep_view() == #[trigger] k2.deep_view() implies k1 == k2 by {
716            let ghost k_deepview = |k: K| k.deep_view();
717            assert(crate::relations::injective(k_deepview));
718            assert(k_deepview(k1) == k_deepview(k2));
719        }
720    }
721}
722
723pub broadcast proof fn lemma_hashmap_deepview_values<K: DeepView, V: DeepView>(m: HashMap<K, V>)
724    requires
725        crate::relations::injective(|k: K| k.deep_view()),
726    ensures
727        #[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),
728{
729    reveal(hash_map_deep_view_impl);
730    broadcast use group_hash_axioms;
731    broadcast use lemma_hashmap_deepview_properties;
732    broadcast use crate::vstd::group_vstd_default;
733
734    let lhs = m.deep_view().values();
735    let rhs = m@.values().map(|v: V| v.deep_view());
736    assert forall|v: V::V| #[trigger] lhs.contains(v) implies rhs.contains(v) by {
737        let dk = choose|dk: K::V| #[trigger]
738            m.deep_view().contains_key(dk) && m.deep_view()[dk] == v;
739        let k = choose|k: K| #[trigger] m@.contains_key(k) && k.deep_view() == dk;
740        let ov = choose|ov: V| #[trigger] m@.contains_key(k) && m@[k] == ov && ov.deep_view() == v;
741        assert(v == ov.deep_view());
742        assert(m@.values().contains(ov));
743    }
744}
745
746/// Borrowing a key works the same way on deep_view as on view,
747/// if deep_view is injective; see `axiom_contains_deref_key`.
748pub broadcast proof fn axiom_hashmap_deepview_borrow<
749    K: DeepView + Borrow<Q>,
750    V: DeepView,
751    Q: View<V = <K as DeepView>::V> + Hash + Eq + ?Sized,
752>(m: HashMap<K, V>, k: &Q)
753    requires
754        obeys_key_model::<K>(),
755        crate::relations::injective(|k: K| k.deep_view()),
756    ensures
757        #[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),
758{
759    admit();
760}
761
762/// A `Map` constructed from a `HashMap` is always finite.
763pub broadcast proof fn axiom_hashmap_view_finite_dom<K, V>(m: HashMap<K, V>)
764    ensures
765        #[trigger] m@.dom().finite(),
766{
767    admit();
768}
769
770pub uninterp spec fn spec_hash_map_len<Key, Value, S>(m: &HashMap<Key, Value, S>) -> usize;
771
772pub broadcast proof fn axiom_spec_hash_map_len<Key, Value, S>(m: &HashMap<Key, Value, S>)
773    ensures
774        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_map_len(m)
775            == m@.len(),
776{
777    admit();
778}
779
780#[verifier::when_used_as_spec(spec_hash_map_len)]
781pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::len ](
782    m: &HashMap<Key, Value, S>,
783) -> (len: usize)
784    ensures
785        len == spec_hash_map_len(m),
786;
787
788pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::is_empty ](
789    m: &HashMap<Key, Value, S>,
790) -> (res: bool)
791    ensures
792        res == m@.is_empty(),
793;
794
795pub assume_specification<K: Clone, V: Clone, S: Clone>[ <HashMap::<K, V, S> as Clone>::clone ](
796    this: &HashMap<K, V, S>,
797) -> (other: HashMap<K, V, S>)
798    ensures
799        other@ == this@,
800;
801
802pub assume_specification<Key, Value>[ HashMap::<Key, Value>::new ]() -> (m: HashMap<
803    Key,
804    Value,
805    RandomState,
806>)
807    ensures
808        m@ == Map::<Key, Value>::empty(),
809;
810
811pub assume_specification<K, V, S: core::default::Default>[ <HashMap<
812    K,
813    V,
814    S,
815> as core::default::Default>::default ]() -> (m: HashMap<K, V, S>)
816    ensures
817        m@ == Map::<K, V>::empty(),
818;
819
820pub assume_specification<Key, Value>[ HashMap::<Key, Value>::with_capacity ](capacity: usize) -> (m:
821    HashMap<Key, Value, RandomState>)
822    ensures
823        m@ == Map::<Key, Value>::empty(),
824;
825
826pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<
827    Key,
828    Value,
829    S,
830>::reserve ](m: &mut HashMap<Key, Value, S>, additional: usize)
831    ensures
832        m@ == old(m)@,
833;
834
835pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<Key, Value, S>::insert ](
836    m: &mut HashMap<Key, Value, S>,
837    k: Key,
838    v: Value,
839) -> (result: Option<Value>)
840    ensures
841        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
842            &&& m@ == old(m)@.insert(k, v)
843            &&& match result {
844                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
845                None => !old(m)@.contains_key(k),
846            }
847        },
848;
849
850// The specification for `contains_key` has a parameter `key: &Q`
851// where you'd expect to find `key: &Key`. This allows for the case
852// that `Key` can be borrowed as something other than `&Key`. For
853// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
854// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
855// respectively.
856// To deal with this, we have a specification function that opaquely
857// specifies what it means for a map to contain a borrowed key of type
858// `&Q`. And the postcondition of `contains_key` just says that its
859// result matches the output of that specification function. But this
860// isn't very helpful by itself, since there's no body to that
861// specification function. So we have special-case axioms that say
862// what this means in two important circumstances: (1) `Key = Q` and
863// (2) `Key = Box<Q>`.
864pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
865    m: Map<Key, Value>,
866    k: &Q,
867) -> bool;
868
869pub broadcast proof fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
870    ensures
871        #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
872{
873    admit();
874}
875
876pub broadcast proof fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
877    ensures
878        #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
879            Box::new(*k),
880        ),
881{
882    admit();
883}
884
885pub assume_specification<
886    Key: Borrow<Q> + Hash + Eq,
887    Value,
888    S: BuildHasher,
889    Q: Hash + Eq + ?Sized,
890>[ HashMap::<Key, Value, S>::contains_key::<Q> ](m: &HashMap<Key, Value, S>, k: &Q) -> (result:
891    bool)
892    ensures
893        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result == contains_borrowed_key(
894            m@,
895            k,
896        ),
897;
898
899// The specification for `get` has a parameter `key: &Q` where you'd
900// expect to find `key: &Key`. This allows for the case that `Key` can
901// be borrowed as something other than `&Key`. For instance,
902// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
903// as `&str`, so in those cases `Q` would be `u32` and `str`
904// respectively.
905// To deal with this, we have a specification function that opaquely
906// specifies what it means for a map to map a borrowed key of type
907// `&Q` to a certain value. And the postcondition of `get` says that
908// its result matches the output of that specification function. (It
909// also says that its result corresponds to the output of
910// `contains_borrowed_key`, discussed above.) But this isn't very
911// helpful by itself, since there's no body to that specification
912// function. So we have special-case axioms that say what this means
913// in two important circumstances: (1) `Key = Q` and (2) `Key =
914// Box<Q>`.
915pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
916    m: Map<Key, Value>,
917    k: &Q,
918    v: Value,
919) -> bool;
920
921pub broadcast proof fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
922    ensures
923        #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
924            && m[*k] == v,
925{
926    admit();
927}
928
929pub broadcast proof fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
930    ensures
931        #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
932            let k = Box::new(*q);
933            &&& m.contains_key(k)
934            &&& m[k] == v
935        },
936{
937    admit();
938}
939
940pub assume_specification<
941    'a,
942    Key: Borrow<Q> + Hash + Eq,
943    Value,
944    S: BuildHasher,
945    Q: Hash + Eq + ?Sized,
946>[ HashMap::<Key, Value, S>::get::<Q> ](m: &'a HashMap<Key, Value, S>, k: &Q) -> (result: Option<
947    &'a Value,
948>)
949    ensures
950        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
951            Some(v) => maps_borrowed_key_to_value(m@, k, *v),
952            None => !contains_borrowed_key(m@, k),
953        },
954;
955
956// The specification for `remove` has a parameter `key: &Q` where
957// you'd expect to find `key: &Key`. This allows for the case that
958// `Key` can be borrowed as something other than `&Key`. For instance,
959// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
960// as `&str`, so in those cases `Q` would be `u32` and `str`
961// respectively. To deal with this, we have a specification function
962// that opaquely specifies what it means for two maps to be related by
963// a remove of a certain `&Q`. And the postcondition of `remove` says
964// that `old(self)@` and `self@` satisfy that relationship. (It also
965// says that its result corresponds to the output of
966// `contains_borrowed_key` and `maps_borrowed_key_to_value`, discussed
967// above.) But this isn't very helpful by itself, since there's no
968// body to that specification function. So we have special-case axioms
969// that say what this means in two important circumstances: (1) `Key =
970// Q` and (2) `Key = Box<Q>`.
971pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
972    old_m: Map<Key, Value>,
973    new_m: Map<Key, Value>,
974    k: &Q,
975) -> bool;
976
977pub broadcast proof fn axiom_deref_key_removed<Q, Value>(
978    old_m: Map<Q, Value>,
979    new_m: Map<Q, Value>,
980    k: &Q,
981)
982    ensures
983        #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
984            *k,
985        ),
986{
987    admit();
988}
989
990pub broadcast proof fn axiom_box_key_removed<Q, Value>(
991    old_m: Map<Box<Q>, Value>,
992    new_m: Map<Box<Q>, Value>,
993    q: &Q,
994)
995    ensures
996        #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
997            == old_m.remove(Box::new(*q)),
998{
999    admit();
1000}
1001
1002pub assume_specification<
1003    Key: Borrow<Q> + Hash + Eq,
1004    Value,
1005    S: BuildHasher,
1006    Q: Hash + Eq + ?Sized,
1007>[ HashMap::<Key, Value, S>::remove::<Q> ](m: &mut HashMap<Key, Value, S>, k: &Q) -> (result:
1008    Option<Value>)
1009    ensures
1010        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1011            &&& borrowed_key_removed(old(m)@, m@, k)
1012            &&& match result {
1013                Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
1014                None => !contains_borrowed_key(old(m)@, k),
1015            }
1016        },
1017;
1018
1019pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::clear ](
1020    m: &mut HashMap<Key, Value, S>,
1021)
1022    ensures
1023        m@ == Map::<Key, Value>::empty(),
1024;
1025
1026pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::keys ](
1027    m: &'a HashMap<Key, Value, S>,
1028) -> (keys: Keys<'a, Key, Value>)
1029    ensures
1030        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1031            let (index, s) = keys@;
1032            &&& index == 0
1033            &&& s.to_set() == m@.dom()
1034            &&& s.no_duplicates()
1035        },
1036;
1037
1038pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::values ](
1039    m: &'a HashMap<Key, Value, S>,
1040) -> (values: Values<'a, Key, Value>)
1041    ensures
1042        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1043            let (index, s) = values@;
1044            &&& index == 0
1045            &&& s.to_set() == m@.values()
1046        },
1047;
1048
1049pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
1050    ensures
1051        #[trigger] (decreases_to!(m => m@)),
1052{
1053    admit();
1054}
1055
1056// The `iter` method of a `HashSet` returns an iterator of type `hash_set::Iter`,
1057// so we specify that type here.
1058#[verifier::external_type_specification]
1059#[verifier::external_body]
1060#[verifier::accept_recursive_types(Key)]
1061pub struct ExSetIter<'a, Key: 'a>(hash_set::Iter<'a, Key>);
1062
1063impl<'a, Key: 'a> View for hash_set::Iter<'a, Key> {
1064    type V = (int, Seq<Key>);
1065
1066    uninterp spec fn view(self: &hash_set::Iter<'a, Key>) -> (int, Seq<Key>);
1067}
1068
1069pub assume_specification<'a, Key>[ hash_set::Iter::<'a, Key>::next ](
1070    elements: &mut hash_set::Iter<'a, Key>,
1071) -> (r: Option<&'a Key>)
1072    ensures
1073        ({
1074            let (old_index, old_seq) = old(elements)@;
1075            match r {
1076                None => {
1077                    &&& elements@ == old(elements)@
1078                    &&& old_index >= old_seq.len()
1079                },
1080                Some(element) => {
1081                    let (new_index, new_seq) = elements@;
1082                    &&& 0 <= old_index < old_seq.len()
1083                    &&& new_seq == old_seq
1084                    &&& new_index == old_index + 1
1085                    &&& element == old_seq[old_index]
1086                },
1087            }
1088        }),
1089;
1090
1091pub struct SetIterGhostIterator<'a, Key> {
1092    pub pos: int,
1093    pub elements: Seq<Key>,
1094    pub phantom: Option<&'a Key>,
1095}
1096
1097impl<'a, Key> super::super::pervasive::ForLoopGhostIteratorNew for hash_set::Iter<'a, Key> {
1098    type GhostIter = SetIterGhostIterator<'a, Key>;
1099
1100    open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key> {
1101        SetIterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
1102    }
1103}
1104
1105impl<'a, Key: 'a> super::super::pervasive::ForLoopGhostIterator for SetIterGhostIterator<'a, Key> {
1106    type ExecIter = hash_set::Iter<'a, Key>;
1107
1108    type Item = Key;
1109
1110    type Decrease = int;
1111
1112    open spec fn exec_invariant(&self, exec_iter: &hash_set::Iter<'a, Key>) -> bool {
1113        &&& self.pos == exec_iter@.0
1114        &&& self.elements == exec_iter@.1
1115    }
1116
1117    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
1118        init matches Some(init) ==> {
1119            &&& init.pos == 0
1120            &&& init.elements == self.elements
1121            &&& 0 <= self.pos <= self.elements.len()
1122        }
1123    }
1124
1125    open spec fn ghost_ensures(&self) -> bool {
1126        self.pos == self.elements.len()
1127    }
1128
1129    open spec fn ghost_decrease(&self) -> Option<int> {
1130        Some(self.elements.len() - self.pos)
1131    }
1132
1133    open spec fn ghost_peek_next(&self) -> Option<Key> {
1134        if 0 <= self.pos < self.elements.len() {
1135            Some(self.elements[self.pos])
1136        } else {
1137            None
1138        }
1139    }
1140
1141    open spec fn ghost_advance(&self, _exec_iter: &hash_set::Iter<'a, Key>) -> SetIterGhostIterator<
1142        'a,
1143        Key,
1144    > {
1145        Self { pos: self.pos + 1, ..*self }
1146    }
1147}
1148
1149impl<'a, Key> View for SetIterGhostIterator<'a, Key> {
1150    type V = Seq<Key>;
1151
1152    open spec fn view(&self) -> Seq<Key> {
1153        self.elements.take(self.pos)
1154    }
1155}
1156
1157/// Specifications for the behavior of [`std::collections::HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html).
1158///
1159/// We model a `HashSet` as having a view of type `Set<Key>`, which reflects the current state of the set.
1160///
1161/// These specifications are only meaningful if `obeys_key_model::<Key>()` and `builds_valid_hashers::<S>()` hold.
1162/// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
1163/// for information on use with primitive types and custom types,
1164/// and see [`builds_valid_hashers()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.builds_valid_hashers.html)
1165/// for information on use with Rust's default implementation and custom implementations.
1166///
1167/// Axioms about the behavior of HashSet are present in the broadcast group `vstd::std_specs::hash::group_hash_axioms`.
1168#[verifier::external_type_specification]
1169#[verifier::external_body]
1170#[verifier::accept_recursive_types(Key)]
1171#[verifier::reject_recursive_types(S)]
1172pub struct ExHashSet<Key, S>(HashSet<Key, S>);
1173
1174pub uninterp spec fn spec_hash_set_len<Key, S>(m: &HashSet<Key, S>) -> usize;
1175
1176pub broadcast proof fn axiom_spec_hash_set_len<Key, S>(m: &HashSet<Key, S>)
1177    ensures
1178        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_set_len(m)
1179            == m@.len(),
1180{
1181    admit();
1182}
1183
1184#[verifier::when_used_as_spec(spec_hash_set_len)]
1185pub assume_specification<Key, S>[ HashSet::<Key, S>::len ](m: &HashSet<Key, S>) -> (len: usize)
1186    ensures
1187        len == spec_hash_set_len(m),
1188;
1189
1190pub assume_specification<Key, S>[ HashSet::<Key, S>::is_empty ](m: &HashSet<Key, S>) -> (res: bool)
1191    ensures
1192        res == m@.is_empty(),
1193;
1194
1195pub assume_specification<Key>[ HashSet::<Key>::new ]() -> (m: HashSet<Key, RandomState>)
1196    ensures
1197        m@ == Set::<Key>::empty(),
1198;
1199
1200pub assume_specification<T, S: core::default::Default>[ <HashSet<
1201    T,
1202    S,
1203> as core::default::Default>::default ]() -> (m: HashSet<T, S>)
1204    ensures
1205        m@ == Set::<T>::empty(),
1206;
1207
1208pub assume_specification<Key>[ HashSet::<Key>::with_capacity ](capacity: usize) -> (m: HashSet<
1209    Key,
1210    RandomState,
1211>)
1212    ensures
1213        m@ == Set::<Key>::empty(),
1214;
1215
1216pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::reserve ](
1217    m: &mut HashSet<Key, S>,
1218    additional: usize,
1219)
1220    ensures
1221        m@ == old(m)@,
1222;
1223
1224pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::insert ](
1225    m: &mut HashSet<Key, S>,
1226    k: Key,
1227) -> (result: bool)
1228    ensures
1229        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1230            &&& m@ == old(m)@.insert(k)
1231            &&& result == !old(m)@.contains(k)
1232        },
1233;
1234
1235// The specification for `contains` has a parameter `key: &Q`
1236// where you'd expect to find `key: &Key`. This allows for the case
1237// that `Key` can be borrowed as something other than `&Key`. For
1238// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
1239// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
1240// respectively.
1241// To deal with this, we have a specification function that opaquely
1242// specifies what it means for a set to contain a borrowed key of type
1243// `&Q`. And the postcondition of `contains` just says that its
1244// result matches the output of that specification function. But this
1245// isn't very helpful by itself, since there's no body to that
1246// specification function. So we have special-case axioms that say
1247// what this means in two important circumstances: (1) `Key = Q` and
1248// (2) `Key = Box<Q>`.
1249pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
1250
1251pub broadcast proof fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
1252    ensures
1253        #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
1254{
1255    admit();
1256}
1257
1258pub broadcast proof fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
1259    ensures
1260        #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
1261{
1262    admit();
1263}
1264
1265pub assume_specification<
1266    Key: Borrow<Q> + Hash + Eq,
1267    S: BuildHasher,
1268    Q: Hash + Eq + ?Sized,
1269>[ HashSet::<Key, S>::contains ](m: &HashSet<Key, S>, k: &Q) -> (result: bool)
1270    ensures
1271        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result
1272            == set_contains_borrowed_key(m@, k),
1273;
1274
1275// The specification for `get` has a parameter `key: &Q` where you'd
1276// expect to find `key: &Key`. This allows for the case that `Key` can
1277// be borrowed as something other than `&Key`. For instance,
1278// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1279// as `&str`, so in those cases `Q` would be `u32` and `str`
1280// respectively.
1281// To deal with this, we have a specification function that opaquely
1282// specifies what it means for a returned reference to point to an
1283// element of a HashSet. And the postcondition of `get` says that
1284// its result matches the output of that specification function. (It
1285// also says that its result corresponds to the output of
1286// `contains_borrowed_key`, discussed above.) But this isn't very
1287// helpful by itself, since there's no body to that specification
1288// function. So we have special-case axioms that say what this means
1289// in two important circumstances: (1) `Key = Q` and (2) `Key =
1290// Box<Q>`.
1291pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
1292
1293pub broadcast proof fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
1294    ensures
1295        #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
1296{
1297    admit();
1298}
1299
1300pub broadcast proof fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
1301    ensures
1302        #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
1303            *q,
1304        ) == v),
1305{
1306    admit();
1307}
1308
1309pub assume_specification<
1310    'a,
1311    Key: Borrow<Q> + Hash + Eq,
1312    S: BuildHasher,
1313    Q: Hash + Eq + ?Sized,
1314>[ HashSet::<Key, S>::get::<Q> ](m: &'a HashSet<Key, S>, k: &Q) -> (result: Option<&'a Key>)
1315    ensures
1316        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
1317            Some(v) => sets_borrowed_key_to_key(m@, k, v),
1318            None => !set_contains_borrowed_key(m@, k),
1319        },
1320;
1321
1322// The specification for `remove` has a parameter `key: &Q` where
1323// you'd expect to find `key: &Key`. This allows for the case that
1324// `Key` can be borrowed as something other than `&Key`. For instance,
1325// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1326// as `&str`, so in those cases `Q` would be `u32` and `str`
1327// respectively. To deal with this, we have a specification function
1328// that opaquely specifies what it means for two sets to be related by
1329// a remove of a certain `&Q`. And the postcondition of `remove` says
1330// that `old(self)@` and `self@` satisfy that relationship. (It also
1331// says that its result corresponds to the output of
1332// `set_contains_borrowed_key`, discussed above.) But this isn't very
1333// helpful by itself, since there's no body to that specification
1334// function. So we have special-case axioms that say what this means
1335// in two important circumstances: (1) `Key = Q` and (2) `Key = Box<Q>`.
1336pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
1337    old_m: Set<Key>,
1338    new_m: Set<Key>,
1339    k: &Q,
1340) -> bool;
1341
1342pub broadcast proof fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
1343    ensures
1344        #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
1345            *k,
1346        ),
1347{
1348    admit();
1349}
1350
1351pub broadcast proof fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
1352    ensures
1353        #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
1354            == old_m.remove(Box::new(*q)),
1355{
1356    admit();
1357}
1358
1359pub assume_specification<
1360    Key: Borrow<Q> + Hash + Eq,
1361    S: BuildHasher,
1362    Q: Hash + Eq + ?Sized,
1363>[ HashSet::<Key, S>::remove::<Q> ](m: &mut HashSet<Key, S>, k: &Q) -> (result: bool)
1364    ensures
1365        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1366            &&& sets_differ_by_borrowed_key(old(m)@, m@, k)
1367            &&& result == set_contains_borrowed_key(old(m)@, k)
1368        },
1369;
1370
1371pub assume_specification<Key, S>[ HashSet::<Key, S>::clear ](m: &mut HashSet<Key, S>)
1372    ensures
1373        m@ == Set::<Key>::empty(),
1374;
1375
1376pub assume_specification<'a, Key, S>[ HashSet::<Key, S>::iter ](m: &'a HashSet<Key, S>) -> (r:
1377    hash_set::Iter<'a, Key>)
1378    ensures
1379        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1380            let (index, s) = r@;
1381            &&& index == 0
1382            &&& s.to_set() == m@
1383            &&& s.no_duplicates()
1384        },
1385;
1386
1387pub broadcast proof fn axiom_hashset_decreases<Key, S>(m: HashSet<Key, S>)
1388    ensures
1389        #[trigger] (decreases_to!(m => m@)),
1390{
1391    admit();
1392}
1393
1394pub broadcast group group_hash_axioms {
1395    axiom_box_key_removed,
1396    axiom_contains_deref_key,
1397    axiom_contains_box,
1398    axiom_deref_key_removed,
1399    axiom_maps_deref_key_to_value,
1400    axiom_maps_box_key_to_value,
1401    axiom_hashmap_deepview_borrow,
1402    axiom_hashmap_view_finite_dom,
1403    axiom_bool_obeys_hash_table_key_model,
1404    axiom_u8_obeys_hash_table_key_model,
1405    axiom_u16_obeys_hash_table_key_model,
1406    axiom_u32_obeys_hash_table_key_model,
1407    axiom_u64_obeys_hash_table_key_model,
1408    axiom_u128_obeys_hash_table_key_model,
1409    axiom_usize_obeys_hash_table_key_model,
1410    axiom_i8_obeys_hash_table_key_model,
1411    axiom_i16_obeys_hash_table_key_model,
1412    axiom_i32_obeys_hash_table_key_model,
1413    axiom_i64_obeys_hash_table_key_model,
1414    axiom_i128_obeys_hash_table_key_model,
1415    axiom_isize_obeys_hash_table_key_model,
1416    axiom_box_bool_obeys_hash_table_key_model,
1417    axiom_box_integer_type_obeys_hash_table_key_model,
1418    axiom_random_state_builds_valid_hashers,
1419    axiom_spec_hash_map_len,
1420    axiom_set_box_key_removed,
1421    axiom_set_contains_deref_key,
1422    axiom_set_contains_box,
1423    axiom_set_deref_key_removed,
1424    axiom_set_deref_key_to_value,
1425    axiom_set_box_key_to_value,
1426    axiom_spec_hash_set_len,
1427    axiom_spec_hash_map_iter,
1428    axiom_hashmap_decreases,
1429    axiom_hashset_decreases,
1430}
1431
1432} // verus!
vstd/std_specs/hash.rs

vstd/std_specs/
hash.rs
