1use 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#[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
67pub assume_specification[ DefaultHasher::new ]() -> (result: DefaultHasher)
69 ensures
70 result@ == Seq::<Seq<u8>>::empty(),
71;
72
73pub assume_specification[ DefaultHasher::write ](state: &mut DefaultHasher, bytes: &[u8])
75 ensures
76 state@ == old(state)@.push(bytes@),
77;
78
79pub assume_specification[ DefaultHasher::finish ](state: &DefaultHasher) -> (result: u64)
81 ensures
82 result == DefaultHasher::spec_finish(state@),
83;
84
85#[verifier::external_body]
103pub uninterp spec fn obeys_key_model<Key: ?Sized>() -> bool;
104
105pub broadcast proof fn axiom_bool_obeys_hash_table_key_model()
110 ensures
111 #[trigger] obeys_key_model::<bool>(),
112{
113 admit();
114}
115
116pub broadcast proof fn axiom_u8_obeys_hash_table_key_model()
117 ensures
118 #[trigger] obeys_key_model::<u8>(),
119{
120 admit();
121}
122
123pub broadcast proof fn axiom_u16_obeys_hash_table_key_model()
124 ensures
125 #[trigger] obeys_key_model::<u16>(),
126{
127 admit();
128}
129
130pub broadcast proof fn axiom_u32_obeys_hash_table_key_model()
131 ensures
132 #[trigger] obeys_key_model::<u32>(),
133{
134 admit();
135}
136
137pub broadcast proof fn axiom_u64_obeys_hash_table_key_model()
138 ensures
139 #[trigger] obeys_key_model::<u64>(),
140{
141 admit();
142}
143
144pub broadcast proof fn axiom_u128_obeys_hash_table_key_model()
145 ensures
146 #[trigger] obeys_key_model::<u128>(),
147{
148 admit();
149}
150
151pub broadcast proof fn axiom_usize_obeys_hash_table_key_model()
152 ensures
153 #[trigger] obeys_key_model::<usize>(),
154{
155 admit();
156}
157
158pub broadcast proof fn axiom_i8_obeys_hash_table_key_model()
159 ensures
160 #[trigger] obeys_key_model::<i8>(),
161{
162 admit();
163}
164
165pub broadcast proof fn axiom_i16_obeys_hash_table_key_model()
166 ensures
167 #[trigger] obeys_key_model::<i16>(),
168{
169 admit();
170}
171
172pub broadcast proof fn axiom_i32_obeys_hash_table_key_model()
173 ensures
174 #[trigger] obeys_key_model::<i32>(),
175{
176 admit();
177}
178
179pub broadcast proof fn axiom_i164_obeys_hash_table_key_model()
180 ensures
181 #[trigger] obeys_key_model::<i64>(),
182{
183 admit();
184}
185
186pub broadcast proof fn axiom_i128_obeys_hash_table_key_model()
187 ensures
188 #[trigger] obeys_key_model::<i128>(),
189{
190 admit();
191}
192
193pub broadcast proof fn axiom_isize_obeys_hash_table_key_model()
194 ensures
195 #[trigger] obeys_key_model::<isize>(),
196{
197 admit();
198}
199
200pub broadcast proof fn axiom_box_bool_obeys_hash_table_key_model()
201 ensures
202 #[trigger] obeys_key_model::<Box<bool>>(),
203{
204 admit();
205}
206
207pub broadcast proof fn axiom_box_integer_type_obeys_hash_table_key_model<Key: Integer + ?Sized>()
208 requires
209 obeys_key_model::<Key>(),
210 ensures
211 #[trigger] obeys_key_model::<Box<Key>>(),
212{
213 admit();
214}
215
216#[verifier::external_trait_specification]
217pub trait ExHasher {
218 type ExternalTraitSpecificationFor: Hasher;
219}
220
221#[verifier::external_trait_specification]
230pub trait ExBuildHasher {
231 type ExternalTraitSpecificationFor: BuildHasher;
232
233 type Hasher: Hasher;
234}
235
236#[verifier::external_body]
250pub uninterp spec fn builds_valid_hashers<T: ?Sized>() -> bool;
251
252#[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#[verifier::external_type_specification]
272#[verifier::external_body]
273#[verifier::accept_recursive_types(Key)]
274#[verifier::accept_recursive_types(Value)]
275pub struct ExKeys<'a, Key: 'a, Value: 'a>(Keys<'a, Key, Value>);
276
277pub trait KeysAdditionalSpecFns<'a, Key: 'a, Value: 'a> {
278 spec fn view(self: &Self) -> (int, Seq<Key>);
279}
280
281impl<'a, Key: 'a, Value: 'a> KeysAdditionalSpecFns<'a, Key, Value> for Keys<'a, Key, Value> {
282 uninterp spec fn view(self: &Keys<'a, Key, Value>) -> (int, Seq<Key>);
283}
284
285pub assume_specification<'a, Key, Value>[ Keys::<'a, Key, Value>::next ](
286 keys: &mut Keys<'a, Key, Value>,
287) -> (r: Option<&'a Key>)
288 ensures
289 ({
290 let (old_index, old_seq) = old(keys)@;
291 match r {
292 None => {
293 &&& keys@ == old(keys)@
294 &&& old_index >= old_seq.len()
295 },
296 Some(k) => {
297 let (new_index, new_seq) = keys@;
298 &&& 0 <= old_index < old_seq.len()
299 &&& new_seq == old_seq
300 &&& new_index == old_index + 1
301 &&& k == old_seq[old_index]
302 },
303 }
304 }),
305;
306
307pub struct KeysGhostIterator<'a, Key, Value> {
308 pub pos: int,
309 pub keys: Seq<Key>,
310 pub phantom: Option<&'a Value>,
311}
312
313impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Keys<'a, Key, Value> {
314 type GhostIter = KeysGhostIterator<'a, Key, Value>;
315
316 open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value> {
317 KeysGhostIterator { pos: self@.0, keys: self@.1, phantom: None }
318 }
319}
320
321impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for KeysGhostIterator<
322 'a,
323 Key,
324 Value,
325> {
326 type ExecIter = Keys<'a, Key, Value>;
327
328 type Item = Key;
329
330 type Decrease = int;
331
332 open spec fn exec_invariant(&self, exec_iter: &Keys<'a, Key, Value>) -> bool {
333 &&& self.pos == exec_iter@.0
334 &&& self.keys == exec_iter@.1
335 }
336
337 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
338 init matches Some(init) ==> {
339 &&& init.pos == 0
340 &&& init.keys == self.keys
341 &&& 0 <= self.pos <= self.keys.len()
342 }
343 }
344
345 open spec fn ghost_ensures(&self) -> bool {
346 self.pos == self.keys.len()
347 }
348
349 open spec fn ghost_decrease(&self) -> Option<int> {
350 Some(self.keys.len() - self.pos)
351 }
352
353 open spec fn ghost_peek_next(&self) -> Option<Key> {
354 if 0 <= self.pos < self.keys.len() {
355 Some(self.keys[self.pos])
356 } else {
357 None
358 }
359 }
360
361 open spec fn ghost_advance(&self, _exec_iter: &Keys<'a, Key, Value>) -> KeysGhostIterator<
362 'a,
363 Key,
364 Value,
365 > {
366 Self { pos: self.pos + 1, ..*self }
367 }
368}
369
370impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value> {
371 type V = Seq<Key>;
372
373 open spec fn view(&self) -> Seq<Key> {
374 self.keys.take(self.pos)
375 }
376}
377
378#[verifier::external_type_specification]
381#[verifier::external_body]
382#[verifier::accept_recursive_types(Key)]
383#[verifier::accept_recursive_types(Value)]
384pub struct ExValues<'a, Key: 'a, Value: 'a>(Values<'a, Key, Value>);
385
386pub trait ValuesAdditionalSpecFns<'a, Key: 'a, Value: 'a> {
387 spec fn view(self: &Self) -> (int, Seq<Value>);
388}
389
390impl<'a, Key: 'a, Value: 'a> ValuesAdditionalSpecFns<'a, Key, Value> for Values<'a, Key, Value> {
391 uninterp spec fn view(self: &Values<'a, Key, Value>) -> (int, Seq<Value>);
392}
393
394pub assume_specification<'a, Key, Value>[ Values::<'a, Key, Value>::next ](
395 values: &mut Values<'a, Key, Value>,
396) -> (r: Option<&'a Value>)
397 ensures
398 ({
399 let (old_index, old_seq) = old(values)@;
400 match r {
401 None => {
402 &&& values@ == old(values)@
403 &&& old_index >= old_seq.len()
404 },
405 Some(v) => {
406 let (new_index, new_seq) = values@;
407 &&& 0 <= old_index < old_seq.len()
408 &&& new_seq == old_seq
409 &&& new_index == old_index + 1
410 &&& v == old_seq[old_index]
411 },
412 }
413 }),
414;
415
416pub struct ValuesGhostIterator<'a, Key, Value> {
417 pub pos: int,
418 pub values: Seq<Value>,
419 pub phantom: Option<&'a Key>,
420}
421
422impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Values<'a, Key, Value> {
423 type GhostIter = ValuesGhostIterator<'a, Key, Value>;
424
425 open spec fn ghost_iter(&self) -> ValuesGhostIterator<'a, Key, Value> {
426 ValuesGhostIterator { pos: self@.0, values: self@.1, phantom: None }
427 }
428}
429
430impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for ValuesGhostIterator<
431 'a,
432 Key,
433 Value,
434> {
435 type ExecIter = Values<'a, Key, Value>;
436
437 type Item = Value;
438
439 type Decrease = int;
440
441 open spec fn exec_invariant(&self, exec_iter: &Values<'a, Key, Value>) -> bool {
442 &&& self.pos == exec_iter@.0
443 &&& self.values == exec_iter@.1
444 }
445
446 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
447 init matches Some(init) ==> {
448 &&& init.pos == 0
449 &&& init.values == self.values
450 &&& 0 <= self.pos <= self.values.len()
451 }
452 }
453
454 open spec fn ghost_ensures(&self) -> bool {
455 self.pos == self.values.len()
456 }
457
458 open spec fn ghost_decrease(&self) -> Option<int> {
459 Some(self.values.len() - self.pos)
460 }
461
462 open spec fn ghost_peek_next(&self) -> Option<Value> {
463 if 0 <= self.pos < self.values.len() {
464 Some(self.values[self.pos])
465 } else {
466 None
467 }
468 }
469
470 open spec fn ghost_advance(&self, _exec_iter: &Values<'a, Key, Value>) -> ValuesGhostIterator<
471 'a,
472 Key,
473 Value,
474 > {
475 Self { pos: self.pos + 1, ..*self }
476 }
477}
478
479impl<'a, Key, Value> View for ValuesGhostIterator<'a, Key, Value> {
480 type V = Seq<Value>;
481
482 open spec fn view(&self) -> Seq<Value> {
483 self.values.take(self.pos)
484 }
485}
486
487#[verifier::external_type_specification]
490#[verifier::external_body]
491#[verifier::accept_recursive_types(Key)]
492#[verifier::accept_recursive_types(Value)]
493pub struct ExMapIter<'a, Key: 'a, Value: 'a>(hash_map::Iter<'a, Key, Value>);
494
495pub trait MapIterAdditionalSpecFns<'a, Key: 'a, Value: 'a> {
496 spec fn view(self: &Self) -> (int, Seq<(Key, Value)>);
497}
498
499impl<'a, Key: 'a, Value: 'a> MapIterAdditionalSpecFns<'a, Key, Value> for hash_map::Iter<
500 'a,
501 Key,
502 Value,
503> {
504 uninterp spec fn view(self: &hash_map::Iter<'a, Key, Value>) -> (int, Seq<(Key, Value)>);
505}
506
507pub assume_specification<'a, Key, Value>[ hash_map::Iter::<'a, Key, Value>::next ](
508 iter: &mut hash_map::Iter<'a, Key, Value>,
509) -> (r: Option<(&'a Key, &'a Value)>)
510 ensures
511 ({
512 let (old_index, old_seq) = old(iter)@;
513 match r {
514 None => {
515 &&& iter@ == old(iter)@
516 &&& old_index >= old_seq.len()
517 },
518 Some((k, v)) => {
519 let (new_index, new_seq) = iter@;
520 let (old_k, old_v) = old_seq[old_index];
521 &&& 0 <= old_index < old_seq.len()
522 &&& new_seq == old_seq
523 &&& new_index == old_index + 1
524 &&& k == old_k
525 &&& v == old_v
526 &&& old_seq.to_set().contains((*k, *v))
527 },
528 }
529 }),
530;
531
532pub struct MapIterGhostIterator<'a, Key, Value> {
533 pub pos: int,
534 pub kv_pairs: Seq<(Key, Value)>,
535 pub _marker: PhantomData<&'a Key>,
536}
537
538impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for hash_map::Iter<
539 'a,
540 Key,
541 Value,
542> {
543 type GhostIter = MapIterGhostIterator<'a, Key, Value>;
544
545 open spec fn ghost_iter(&self) -> MapIterGhostIterator<'a, Key, Value> {
546 MapIterGhostIterator { pos: self@.0, kv_pairs: self@.1, _marker: PhantomData }
547 }
548}
549
550impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for MapIterGhostIterator<
551 'a,
552 Key,
553 Value,
554> {
555 type ExecIter = hash_map::Iter<'a, Key, Value>;
556
557 type Item = (Key, Value);
558
559 type Decrease = int;
560
561 open spec fn exec_invariant(&self, exec_iter: &hash_map::Iter<'a, Key, Value>) -> bool {
562 &&& self.pos == exec_iter@.0
563 &&& self.kv_pairs == exec_iter@.1
564 }
565
566 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
567 init matches Some(init) ==> {
568 &&& init.pos == 0
569 &&& init.kv_pairs == self.kv_pairs
570 &&& 0 <= self.pos <= self.kv_pairs.len()
571 }
572 }
573
574 open spec fn ghost_ensures(&self) -> bool {
575 self.pos == self.kv_pairs.len()
576 }
577
578 open spec fn ghost_decrease(&self) -> Option<int> {
579 Some(self.kv_pairs.len() - self.pos)
580 }
581
582 open spec fn ghost_peek_next(&self) -> Option<(Key, Value)> {
583 if 0 <= self.pos < self.kv_pairs.len() {
584 Some(self.kv_pairs[self.pos])
585 } else {
586 None
587 }
588 }
589
590 open spec fn ghost_advance(
591 &self,
592 _exec_iter: &hash_map::Iter<'a, Key, Value>,
593 ) -> MapIterGhostIterator<'a, Key, Value> {
594 Self { pos: self.pos + 1, ..*self }
595 }
596}
597
598impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value> {
599 type V = Seq<(Key, Value)>;
600
601 open spec fn view(&self) -> Seq<(Key, Value)> {
602 self.kv_pairs.take(self.pos)
603 }
604}
605
606pub uninterp spec fn spec_hash_map_iter<'a, Key, Value, S>(m: &'a HashMap<Key, Value, S>) -> (r:
613 hash_map::Iter<'a, Key, Value>);
614
615pub broadcast proof fn axiom_spec_hash_map_iter<'a, Key, Value, S>(m: &'a HashMap<Key, Value, S>)
616 ensures
617 ({
618 let (pos, v) = #[trigger] spec_hash_map_iter(m)@;
619 &&& pos == 0int
620 &&& forall|i: int| 0 <= i < v.len() ==> #[trigger] m@[v[i].0] == v[i].1
621 }),
622{
623 admit();
624}
625
626#[verifier::when_used_as_spec(spec_hash_map_iter)]
627pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::iter ](
628 m: &'a HashMap<Key, Value, S>,
629) -> (iter: hash_map::Iter<'a, Key, Value>)
630 ensures
631 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
632 let (index, s) = iter@;
633 &&& index == 0
634 &&& s.to_set() == m@.kv_pairs()
635 &&& s.no_duplicates()
636 },
637;
638
639#[verifier::external_type_specification]
651#[verifier::external_body]
652#[verifier::accept_recursive_types(Key)]
653#[verifier::accept_recursive_types(Value)]
654#[verifier::reject_recursive_types(S)]
655pub struct ExHashMap<Key, Value, S>(HashMap<Key, Value, S>);
656
657pub trait HashMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
658 spec fn spec_index(&self, k: Key) -> Value
659 recommends
660 self@.contains_key(k),
661 ;
662}
663
664impl<Key, Value, S> HashMapAdditionalSpecFns<Key, Value> for HashMap<Key, Value, S> {
665 #[verifier::inline]
666 open spec fn spec_index(&self, k: Key) -> Value {
667 self@.index(k)
668 }
669}
670
671impl<Key, Value, S> View for HashMap<Key, Value, S> {
672 type V = Map<Key, Value>;
673
674 uninterp spec fn view(&self) -> Map<Key, Value>;
675}
676
677impl<Key: DeepView, Value: DeepView, S> DeepView for HashMap<Key, Value, S> {
678 type V = Map<Key::V, Value::V>;
679
680 open spec fn deep_view(&self) -> Map<Key::V, Value::V> {
681 hash_map_deep_view_impl(*self)
682 }
683}
684
685#[verifier::opaque]
691pub open spec fn hash_map_deep_view_impl<Key: DeepView, Value: DeepView, S>(
692 m: HashMap<Key, Value, S>,
693) -> Map<Key::V, Value::V> {
694 Map::new(
695 |k: Key::V|
696 exists|orig_k: Key| #[trigger] m@.contains_key(orig_k) && k == orig_k.deep_view(),
697 |dk: Key::V|
698 {
699 let k = choose|k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
700 m@[k].deep_view()
701 },
702 )
703}
704
705pub broadcast proof fn lemma_hashmap_deepview_dom<K: DeepView, V: DeepView>(m: HashMap<K, V>)
706 ensures
707 #[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),
708{
709 reveal(hash_map_deep_view_impl);
710 broadcast use group_hash_axioms;
711 broadcast use crate::vstd::group_vstd_default;
712
713 assert(m.deep_view().dom() =~= m@.dom().map(|k: K| k.deep_view()));
714}
715
716pub broadcast proof fn lemma_hashmap_deepview_properties<K: DeepView, V: DeepView>(m: HashMap<K, V>)
717 requires
718 crate::relations::injective(|k: K| k.deep_view()),
719 ensures
720 #![trigger m.deep_view()]
721 forall|k: K| #[trigger]
723 m@.contains_key(k) ==> m.deep_view().contains_key(k.deep_view())
724 && m.deep_view()[k.deep_view()] == m@[k].deep_view(),
725 forall|dk: <K as DeepView>::V| #[trigger]
727 m.deep_view().contains_key(dk) ==> exists|k: K|
728 k.deep_view() == dk && #[trigger] m@.contains_key(k),
729{
730 reveal(hash_map_deep_view_impl);
731 broadcast use group_hash_axioms;
732 broadcast use crate::vstd::group_vstd_default;
733
734 assert(m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()));
735 assert forall|k: K| #[trigger] m@.contains_key(k) implies m.deep_view().contains_key(
736 k.deep_view(),
737 ) && m.deep_view()[k.deep_view()] == m@[k].deep_view() by {
738 assert forall|k1: K, k2: K| #[trigger]
739 k1.deep_view() == #[trigger] k2.deep_view() implies k1 == k2 by {
740 let ghost k_deepview = |k: K| k.deep_view();
741 assert(crate::relations::injective(k_deepview));
742 assert(k_deepview(k1) == k_deepview(k2));
743 }
744 }
745}
746
747pub broadcast proof fn lemma_hashmap_deepview_values<K: DeepView, V: DeepView>(m: HashMap<K, V>)
748 requires
749 crate::relations::injective(|k: K| k.deep_view()),
750 ensures
751 #[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),
752{
753 reveal(hash_map_deep_view_impl);
754 broadcast use group_hash_axioms;
755 broadcast use lemma_hashmap_deepview_properties;
756 broadcast use crate::vstd::group_vstd_default;
757
758 let lhs = m.deep_view().values();
759 let rhs = m@.values().map(|v: V| v.deep_view());
760 assert forall|v: V::V| #[trigger] lhs.contains(v) implies rhs.contains(v) by {
761 let dk = choose|dk: K::V| #[trigger]
762 m.deep_view().contains_key(dk) && m.deep_view()[dk] == v;
763 let k = choose|k: K| #[trigger] m@.contains_key(k) && k.deep_view() == dk;
764 let ov = choose|ov: V| #[trigger] m@.contains_key(k) && m@[k] == ov && ov.deep_view() == v;
765 assert(v == ov.deep_view());
766 assert(m@.values().contains(ov));
767 }
768}
769
770pub broadcast proof fn axiom_hashmap_deepview_borrow<
773 K: DeepView + Borrow<Q>,
774 V: DeepView,
775 Q: View<V = <K as DeepView>::V> + Hash + Eq + ?Sized,
776>(m: HashMap<K, V>, k: &Q)
777 requires
778 obeys_key_model::<K>(),
779 crate::relations::injective(|k: K| k.deep_view()),
780 ensures
781 #[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),
782{
783 admit();
784}
785
786pub broadcast proof fn axiom_hashmap_view_finite_dom<K, V>(m: HashMap<K, V>)
788 ensures
789 #[trigger] m@.dom().finite(),
790{
791 admit();
792}
793
794pub uninterp spec fn spec_hash_map_len<Key, Value, S>(m: &HashMap<Key, Value, S>) -> usize;
795
796pub broadcast proof fn axiom_spec_hash_map_len<Key, Value, S>(m: &HashMap<Key, Value, S>)
797 ensures
798 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_map_len(m)
799 == m@.len(),
800{
801 admit();
802}
803
804#[verifier::when_used_as_spec(spec_hash_map_len)]
805pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::len ](
806 m: &HashMap<Key, Value, S>,
807) -> (len: usize)
808 ensures
809 len == spec_hash_map_len(m),
810;
811
812pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::is_empty ](
813 m: &HashMap<Key, Value, S>,
814) -> (res: bool)
815 ensures
816 res == m@.is_empty(),
817;
818
819pub assume_specification<K: Clone, V: Clone, S: Clone>[ <HashMap::<K, V, S> as Clone>::clone ](
820 this: &HashMap<K, V, S>,
821) -> (other: HashMap<K, V, S>)
822 ensures
823 other@ == this@,
824;
825
826pub assume_specification<Key, Value>[ HashMap::<Key, Value>::new ]() -> (m: HashMap<
827 Key,
828 Value,
829 RandomState,
830>)
831 ensures
832 m@ == Map::<Key, Value>::empty(),
833;
834
835pub assume_specification<Key, Value>[ HashMap::<Key, Value>::with_capacity ](capacity: usize) -> (m:
836 HashMap<Key, Value, RandomState>)
837 ensures
838 m@ == Map::<Key, Value>::empty(),
839;
840
841pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<
842 Key,
843 Value,
844 S,
845>::reserve ](m: &mut HashMap<Key, Value, S>, additional: usize)
846 ensures
847 m@ == old(m)@,
848;
849
850pub assume_specification<Key: Eq + Hash, Value, S: BuildHasher>[ HashMap::<Key, Value, S>::insert ](
851 m: &mut HashMap<Key, Value, S>,
852 k: Key,
853 v: Value,
854) -> (result: Option<Value>)
855 ensures
856 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
857 &&& m@ == old(m)@.insert(k, v)
858 &&& match result {
859 Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
860 None => !old(m)@.contains_key(k),
861 }
862 },
863;
864
865pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
880 m: Map<Key, Value>,
881 k: &Q,
882) -> bool;
883
884pub broadcast proof fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
885 ensures
886 #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
887{
888 admit();
889}
890
891pub broadcast proof fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
892 ensures
893 #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
894 Box::new(*k),
895 ),
896{
897 admit();
898}
899
900pub assume_specification<
901 Key: Borrow<Q> + Hash + Eq,
902 Value,
903 S: BuildHasher,
904 Q: Hash + Eq + ?Sized,
905>[ HashMap::<Key, Value, S>::contains_key::<Q> ](m: &HashMap<Key, Value, S>, k: &Q) -> (result:
906 bool)
907 ensures
908 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result == contains_borrowed_key(
909 m@,
910 k,
911 ),
912;
913
914pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
931 m: Map<Key, Value>,
932 k: &Q,
933 v: Value,
934) -> bool;
935
936pub broadcast proof fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
937 ensures
938 #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
939 && m[*k] == v,
940{
941 admit();
942}
943
944pub broadcast proof fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
945 ensures
946 #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
947 let k = Box::new(*q);
948 &&& m.contains_key(k)
949 &&& m[k] == v
950 },
951{
952 admit();
953}
954
955pub assume_specification<
956 'a,
957 Key: Borrow<Q> + Hash + Eq,
958 Value,
959 S: BuildHasher,
960 Q: Hash + Eq + ?Sized,
961>[ HashMap::<Key, Value, S>::get::<Q> ](m: &'a HashMap<Key, Value, S>, k: &Q) -> (result: Option<
962 &'a Value,
963>)
964 ensures
965 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
966 Some(v) => maps_borrowed_key_to_value(m@, k, *v),
967 None => !contains_borrowed_key(m@, k),
968 },
969;
970
971pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
987 old_m: Map<Key, Value>,
988 new_m: Map<Key, Value>,
989 k: &Q,
990) -> bool;
991
992pub broadcast proof fn axiom_deref_key_removed<Q, Value>(
993 old_m: Map<Q, Value>,
994 new_m: Map<Q, Value>,
995 k: &Q,
996)
997 ensures
998 #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
999 *k,
1000 ),
1001{
1002 admit();
1003}
1004
1005pub broadcast proof fn axiom_box_key_removed<Q, Value>(
1006 old_m: Map<Box<Q>, Value>,
1007 new_m: Map<Box<Q>, Value>,
1008 q: &Q,
1009)
1010 ensures
1011 #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
1012 == old_m.remove(Box::new(*q)),
1013{
1014 admit();
1015}
1016
1017pub assume_specification<
1018 Key: Borrow<Q> + Hash + Eq,
1019 Value,
1020 S: BuildHasher,
1021 Q: Hash + Eq + ?Sized,
1022>[ HashMap::<Key, Value, S>::remove::<Q> ](m: &mut HashMap<Key, Value, S>, k: &Q) -> (result:
1023 Option<Value>)
1024 ensures
1025 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1026 &&& borrowed_key_removed(old(m)@, m@, k)
1027 &&& match result {
1028 Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
1029 None => !contains_borrowed_key(old(m)@, k),
1030 }
1031 },
1032;
1033
1034pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::clear ](
1035 m: &mut HashMap<Key, Value, S>,
1036)
1037 ensures
1038 m@ == Map::<Key, Value>::empty(),
1039;
1040
1041pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::keys ](
1042 m: &'a HashMap<Key, Value, S>,
1043) -> (keys: Keys<'a, Key, Value>)
1044 ensures
1045 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1046 let (index, s) = keys@;
1047 &&& index == 0
1048 &&& s.to_set() == m@.dom()
1049 &&& s.no_duplicates()
1050 },
1051;
1052
1053pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::values ](
1054 m: &'a HashMap<Key, Value, S>,
1055) -> (values: Values<'a, Key, Value>)
1056 ensures
1057 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1058 let (index, s) = values@;
1059 &&& index == 0
1060 &&& s.to_set() == m@.values()
1061 },
1062;
1063
1064pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
1065 ensures
1066 #[trigger] (decreases_to!(m => m@)),
1067{
1068 admit();
1069}
1070
1071#[verifier::external_type_specification]
1074#[verifier::external_body]
1075#[verifier::accept_recursive_types(Key)]
1076pub struct ExSetIter<'a, Key: 'a>(hash_set::Iter<'a, Key>);
1077
1078pub trait SetIterAdditionalSpecFns<'a, Key: 'a> {
1079 spec fn view(self: &Self) -> (int, Seq<Key>);
1080}
1081
1082impl<'a, Key: 'a> SetIterAdditionalSpecFns<'a, Key> for hash_set::Iter<'a, Key> {
1083 uninterp spec fn view(self: &hash_set::Iter<'a, Key>) -> (int, Seq<Key>);
1084}
1085
1086pub assume_specification<'a, Key>[ hash_set::Iter::<'a, Key>::next ](
1087 elements: &mut hash_set::Iter<'a, Key>,
1088) -> (r: Option<&'a Key>)
1089 ensures
1090 ({
1091 let (old_index, old_seq) = old(elements)@;
1092 match r {
1093 None => {
1094 &&& elements@ == old(elements)@
1095 &&& old_index >= old_seq.len()
1096 },
1097 Some(element) => {
1098 let (new_index, new_seq) = elements@;
1099 &&& 0 <= old_index < old_seq.len()
1100 &&& new_seq == old_seq
1101 &&& new_index == old_index + 1
1102 &&& element == old_seq[old_index]
1103 },
1104 }
1105 }),
1106;
1107
1108pub struct SetIterGhostIterator<'a, Key> {
1109 pub pos: int,
1110 pub elements: Seq<Key>,
1111 pub phantom: Option<&'a Key>,
1112}
1113
1114impl<'a, Key> super::super::pervasive::ForLoopGhostIteratorNew for hash_set::Iter<'a, Key> {
1115 type GhostIter = SetIterGhostIterator<'a, Key>;
1116
1117 open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key> {
1118 SetIterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
1119 }
1120}
1121
1122impl<'a, Key: 'a> super::super::pervasive::ForLoopGhostIterator for SetIterGhostIterator<'a, Key> {
1123 type ExecIter = hash_set::Iter<'a, Key>;
1124
1125 type Item = Key;
1126
1127 type Decrease = int;
1128
1129 open spec fn exec_invariant(&self, exec_iter: &hash_set::Iter<'a, Key>) -> bool {
1130 &&& self.pos == exec_iter@.0
1131 &&& self.elements == exec_iter@.1
1132 }
1133
1134 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
1135 init matches Some(init) ==> {
1136 &&& init.pos == 0
1137 &&& init.elements == self.elements
1138 &&& 0 <= self.pos <= self.elements.len()
1139 }
1140 }
1141
1142 open spec fn ghost_ensures(&self) -> bool {
1143 self.pos == self.elements.len()
1144 }
1145
1146 open spec fn ghost_decrease(&self) -> Option<int> {
1147 Some(self.elements.len() - self.pos)
1148 }
1149
1150 open spec fn ghost_peek_next(&self) -> Option<Key> {
1151 if 0 <= self.pos < self.elements.len() {
1152 Some(self.elements[self.pos])
1153 } else {
1154 None
1155 }
1156 }
1157
1158 open spec fn ghost_advance(&self, _exec_iter: &hash_set::Iter<'a, Key>) -> SetIterGhostIterator<
1159 'a,
1160 Key,
1161 > {
1162 Self { pos: self.pos + 1, ..*self }
1163 }
1164}
1165
1166impl<'a, Key> View for SetIterGhostIterator<'a, Key> {
1167 type V = Seq<Key>;
1168
1169 open spec fn view(&self) -> Seq<Key> {
1170 self.elements.take(self.pos)
1171 }
1172}
1173
1174#[verifier::external_type_specification]
1186#[verifier::external_body]
1187#[verifier::accept_recursive_types(Key)]
1188#[verifier::reject_recursive_types(S)]
1189pub struct ExHashSet<Key, S>(HashSet<Key, S>);
1190
1191impl<Key, S> View for HashSet<Key, S> {
1192 type V = Set<Key>;
1193
1194 uninterp spec fn view(&self) -> Set<Key>;
1195}
1196
1197pub uninterp spec fn spec_hash_set_len<Key, S>(m: &HashSet<Key, S>) -> usize;
1198
1199pub broadcast proof fn axiom_spec_hash_set_len<Key, S>(m: &HashSet<Key, S>)
1200 ensures
1201 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> #[trigger] spec_hash_set_len(m)
1202 == m@.len(),
1203{
1204 admit();
1205}
1206
1207#[verifier::when_used_as_spec(spec_hash_set_len)]
1208pub assume_specification<Key, S>[ HashSet::<Key, S>::len ](m: &HashSet<Key, S>) -> (len: usize)
1209 ensures
1210 len == spec_hash_set_len(m),
1211;
1212
1213pub assume_specification<Key, S>[ HashSet::<Key, S>::is_empty ](m: &HashSet<Key, S>) -> (res: bool)
1214 ensures
1215 res == m@.is_empty(),
1216;
1217
1218pub assume_specification<Key>[ HashSet::<Key>::new ]() -> (m: HashSet<Key, RandomState>)
1219 ensures
1220 m@ == Set::<Key>::empty(),
1221;
1222
1223pub assume_specification<Key>[ HashSet::<Key>::with_capacity ](capacity: usize) -> (m: HashSet<
1224 Key,
1225 RandomState,
1226>)
1227 ensures
1228 m@ == Set::<Key>::empty(),
1229;
1230
1231pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::reserve ](
1232 m: &mut HashSet<Key, S>,
1233 additional: usize,
1234)
1235 ensures
1236 m@ == old(m)@,
1237;
1238
1239pub assume_specification<Key: Eq + Hash, S: BuildHasher>[ HashSet::<Key, S>::insert ](
1240 m: &mut HashSet<Key, S>,
1241 k: Key,
1242) -> (result: bool)
1243 ensures
1244 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1245 &&& m@ == old(m)@.insert(k)
1246 &&& result == !old(m)@.contains(k)
1247 },
1248;
1249
1250pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
1265
1266pub broadcast proof fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
1267 ensures
1268 #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
1269{
1270 admit();
1271}
1272
1273pub broadcast proof fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
1274 ensures
1275 #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
1276{
1277 admit();
1278}
1279
1280pub assume_specification<
1281 Key: Borrow<Q> + Hash + Eq,
1282 S: BuildHasher,
1283 Q: Hash + Eq + ?Sized,
1284>[ HashSet::<Key, S>::contains ](m: &HashSet<Key, S>, k: &Q) -> (result: bool)
1285 ensures
1286 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> result
1287 == set_contains_borrowed_key(m@, k),
1288;
1289
1290pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
1307
1308pub broadcast proof fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
1309 ensures
1310 #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
1311{
1312 admit();
1313}
1314
1315pub broadcast proof fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
1316 ensures
1317 #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
1318 *q,
1319 ) == v),
1320{
1321 admit();
1322}
1323
1324pub assume_specification<
1325 'a,
1326 Key: Borrow<Q> + Hash + Eq,
1327 S: BuildHasher,
1328 Q: Hash + Eq + ?Sized,
1329>[ HashSet::<Key, S>::get::<Q> ](m: &'a HashSet<Key, S>, k: &Q) -> (result: Option<&'a Key>)
1330 ensures
1331 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> match result {
1332 Some(v) => sets_borrowed_key_to_key(m@, k, v),
1333 None => !set_contains_borrowed_key(m@, k),
1334 },
1335;
1336
1337pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
1352 old_m: Set<Key>,
1353 new_m: Set<Key>,
1354 k: &Q,
1355) -> bool;
1356
1357pub broadcast proof fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
1358 ensures
1359 #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
1360 *k,
1361 ),
1362{
1363 admit();
1364}
1365
1366pub broadcast proof fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
1367 ensures
1368 #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
1369 == old_m.remove(Box::new(*q)),
1370{
1371 admit();
1372}
1373
1374pub assume_specification<
1375 Key: Borrow<Q> + Hash + Eq,
1376 S: BuildHasher,
1377 Q: Hash + Eq + ?Sized,
1378>[ HashSet::<Key, S>::remove::<Q> ](m: &mut HashSet<Key, S>, k: &Q) -> (result: bool)
1379 ensures
1380 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1381 &&& sets_differ_by_borrowed_key(old(m)@, m@, k)
1382 &&& result == set_contains_borrowed_key(old(m)@, k)
1383 },
1384;
1385
1386pub assume_specification<Key, S>[ HashSet::<Key, S>::clear ](m: &mut HashSet<Key, S>)
1387 ensures
1388 m@ == Set::<Key>::empty(),
1389;
1390
1391pub assume_specification<'a, Key, S>[ HashSet::<Key, S>::iter ](m: &'a HashSet<Key, S>) -> (r:
1392 hash_set::Iter<'a, Key>)
1393 ensures
1394 obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
1395 let (index, s) = r@;
1396 &&& index == 0
1397 &&& s.to_set() == m@
1398 &&& s.no_duplicates()
1399 },
1400;
1401
1402pub broadcast proof fn axiom_hashset_decreases<Key, S>(m: HashSet<Key, S>)
1403 ensures
1404 #[trigger] (decreases_to!(m => m@)),
1405{
1406 admit();
1407}
1408
1409pub broadcast group group_hash_axioms {
1410 axiom_box_key_removed,
1411 axiom_contains_deref_key,
1412 axiom_contains_box,
1413 axiom_deref_key_removed,
1414 axiom_maps_deref_key_to_value,
1415 axiom_maps_box_key_to_value,
1416 axiom_hashmap_deepview_borrow,
1417 axiom_hashmap_view_finite_dom,
1418 axiom_bool_obeys_hash_table_key_model,
1419 axiom_u8_obeys_hash_table_key_model,
1420 axiom_u16_obeys_hash_table_key_model,
1421 axiom_u32_obeys_hash_table_key_model,
1422 axiom_u64_obeys_hash_table_key_model,
1423 axiom_u128_obeys_hash_table_key_model,
1424 axiom_usize_obeys_hash_table_key_model,
1425 axiom_i8_obeys_hash_table_key_model,
1426 axiom_i16_obeys_hash_table_key_model,
1427 axiom_i32_obeys_hash_table_key_model,
1428 axiom_i164_obeys_hash_table_key_model,
1429 axiom_i128_obeys_hash_table_key_model,
1430 axiom_isize_obeys_hash_table_key_model,
1431 axiom_box_bool_obeys_hash_table_key_model,
1432 axiom_box_integer_type_obeys_hash_table_key_model,
1433 axiom_random_state_builds_valid_hashers,
1434 axiom_spec_hash_map_len,
1435 axiom_set_box_key_removed,
1436 axiom_set_contains_deref_key,
1437 axiom_set_contains_box,
1438 axiom_set_deref_key_removed,
1439 axiom_set_deref_key_to_value,
1440 axiom_set_box_key_to_value,
1441 axiom_spec_hash_set_len,
1442 axiom_spec_hash_map_iter,
1443 axiom_hashmap_decreases,
1444 axiom_hashset_decreases,
1445}
1446
1447}