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

vstd/std_specs/
hash.rs
