creusot_std/std/collections/
hash_map.rs

1use crate::{
2    logic::FMap,
3    prelude::*,
4    std::iter::{FromIteratorSpec, IteratorSpec},
5};
6#[cfg(feature = "nightly")]
7use std::alloc::Allocator;
8use std::{
9    collections::hash_map::*,
10    default::Default,
11    hash::{BuildHasher, Hash},
12};
13
14#[cfg(feature = "nightly")]
15impl<K: DeepModel, V, S, A: Allocator> View for HashMap<K, V, S, A> {
16    type ViewTy = FMap<K::DeepModelTy, V>;
17
18    #[logic(opaque)]
19    fn view(self) -> Self::ViewTy {
20        dead
21    }
22}
23
24extern_spec! {
25    impl<K: DeepModel, V, S, A: Allocator> HashMap<K, V, S, A> {
26        #[ensures(self@ == result@)]
27        fn iter(&self) -> Iter<'_, K, V>;
28
29        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) == (^self)@.contains(k))]
30        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) == result@.contains(k))]
31        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) ==> (*self)@[k] == *result@[k] && (^self)@[k] == ^result@[k])]
32        fn iter_mut(&mut self) -> IterMut<'_, K, V>;
33    }
34
35    impl<K: DeepModel, V, S, A: Allocator> IntoIterator for HashMap<K, V, S, A> {
36        #[ensures(self@ == result@)]
37        fn into_iter(self) -> IntoIter<K, V, A>;
38    }
39
40    impl<'a, K: DeepModel, V, S, A: Allocator> IntoIterator for &'a HashMap<K, V, S, A> {
41        #[ensures(self@ == result@)]
42        fn into_iter(self) -> Iter<'a, K, V>;
43    }
44
45    impl<'a, K: DeepModel, V, S, A: Allocator> IntoIterator for &'a mut HashMap<K, V, S, A> {
46        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) == (^self)@.contains(k))]
47        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) == result@.contains(k))]
48        #[ensures(forall<k: K::DeepModelTy> (*self)@.contains(k) ==> (*self)@[k] == *result@[k] && (^self)@[k] == ^result@[k])]
49        fn into_iter(self) -> IterMut<'a, K, V>;
50    }
51}
52
53#[cfg(feature = "nightly")]
54impl<K: DeepModel, V, A: Allocator> View for IntoIter<K, V, A> {
55    type ViewTy = FMap<K::DeepModelTy, V>;
56
57    #[logic(opaque)]
58    fn view(self) -> Self::ViewTy {
59        dead
60    }
61}
62
63#[cfg(feature = "nightly")]
64impl<K: DeepModel, V, A: Allocator> IteratorSpec for IntoIter<K, V, A> {
65    #[logic(open, prophetic, inline)]
66    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
67        // self@ equals the union of visited (viewed as a fmap) and o@
68        pearlite! {
69            self@.len() == visited.len() + o@.len()
70            && (forall<k: K, v: V> visited.contains((k, v))
71                ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
72            && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
73                ==> self@.get(k) == Some(v) && !exists<k2: K, v2: V> k2.deep_model() == k && visited.contains((k2, v2)))
74            && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
75                ==> (exists<k1: K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
76            && (forall<i1, i2>
77                0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
78                && visited[i1].0.deep_model() == visited[i2].0.deep_model()
79                ==> i1 == i2)
80        }
81    }
82
83    #[logic(open, prophetic)]
84    fn completed(&mut self) -> bool {
85        pearlite! { resolve(self) && self@.is_empty() }
86    }
87
88    #[logic(open, law)]
89    #[ensures(self.produces(Seq::empty(), self))]
90    fn produces_refl(self) {}
91
92    #[logic(open, law)]
93    #[requires(a.produces(ab, b))]
94    #[requires(b.produces(bc, c))]
95    #[ensures(a.produces(ab.concat(bc), c))]
96    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
97        proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
98    }
99}
100
101impl<'a, K: DeepModel, V> View for Iter<'a, K, V> {
102    type ViewTy = FMap<K::DeepModelTy, V>;
103
104    #[logic(opaque)]
105    fn view(self) -> Self::ViewTy {
106        dead
107    }
108}
109
110impl<'a, K: DeepModel, V> IteratorSpec for Iter<'a, K, V> {
111    #[logic(open, prophetic, inline)]
112    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
113        // `self@` equals the union of `visited` (viewed as a finite map) and `o@`
114        pearlite! {
115            self@.len() == visited.len() + o@.len()
116            && (forall<k: &K, v: &V> visited.contains((k, v))
117                ==> self@.get(k.deep_model()) == Some(*v) && o@.get(k.deep_model()) == None)
118            && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
119                ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &V> k2.deep_model() == k && visited.contains((k2, v2)))
120            && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
121                ==> (exists<k2: &K> k2.deep_model() == k && visited.contains((k2, &v))) || o@.get(k) == Some(v))
122            && (forall<i1, i2>
123                0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
124                && visited[i1].0.deep_model() == visited[i2].0.deep_model()
125                ==> i1 == i2)
126        }
127    }
128
129    #[logic(open, prophetic)]
130    fn completed(&mut self) -> bool {
131        pearlite! { resolve(self) && self@.is_empty() }
132    }
133
134    #[logic(open, law)]
135    #[ensures(self.produces(Seq::empty(), self))]
136    fn produces_refl(self) {}
137
138    #[logic(open, law)]
139    #[requires(a.produces(ab, b))]
140    #[requires(b.produces(bc, c))]
141    #[ensures(a.produces(ab.concat(bc), c))]
142    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
143        proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
144    }
145}
146
147impl<'a, K: DeepModel, V> View for IterMut<'a, K, V> {
148    type ViewTy = FMap<K::DeepModelTy, &'a mut V>;
149
150    #[logic(opaque)]
151    fn view(self) -> Self::ViewTy {
152        dead
153    }
154}
155
156impl<'a, K: DeepModel, V> IteratorSpec for IterMut<'a, K, V> {
157    #[logic(open, prophetic, inline)]
158    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
159        // self@ equals the union of visited (viewed as a fmap) and o@
160        pearlite! {
161            self@.len() == visited.len() + o@.len()
162            && (forall<k: K, v: &mut V> visited.contains((&k, v))
163                ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
164            && (forall<k: K::DeepModelTy, v: &mut V> o@.get(k) == Some(v)
165                ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &mut V> k2.deep_model() == k && visited.contains((k2, v2)))
166            && (forall<k: K::DeepModelTy, v: &mut V> self@.get(k) == Some(v)
167                ==> (exists<k1: &K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
168            && (forall<i1, i2>
169                0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
170                && visited[i1].0.deep_model() == visited[i2].0.deep_model()
171                ==> i1 == i2)
172        }
173    }
174
175    #[logic(open, prophetic)]
176    fn completed(&mut self) -> bool {
177        pearlite! { resolve(self) && self@.is_empty() }
178    }
179
180    #[logic(open, law)]
181    #[ensures(self.produces(Seq::empty(), self))]
182    fn produces_refl(self) {}
183
184    #[logic(open, law)]
185    #[requires(a.produces(ab, b))]
186    #[requires(b.produces(bc, c))]
187    #[ensures(a.produces(ab.concat(bc), c))]
188    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
189        proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
190    }
191}
192
193impl<K: Eq + Hash + DeepModel, V, S: Default + BuildHasher> FromIteratorSpec<(K, V)>
194    for HashMap<K, V, S>
195{
196    #[logic(open)]
197    fn from_iter_post(prod: Seq<(K, V)>, res: Self) -> bool {
198        pearlite! { forall<k: K::DeepModelTy, v: V> (res@.get(k) == Some(v))
199        == (exists<i, k1: K> 0 <= i && i < prod.len() && k1.deep_model() == k && prod[i] == (k1, v)
200            && forall<j> i < j && j < prod.len() ==> prod[j].0.deep_model() != k) }
201    }
202}
203
204#[cfg(not(feature = "nightly"))]
205mod impls {
206    use crate::{logic::FMap, prelude::*};
207    use std::collections::hash_map::{HashMap, IntoIter};
208
209    impl<K: DeepModel, V, S> View for HashMap<K, V, S> {
210        type ViewTy = FMap<K::DeepModelTy, V>;
211    }
212    impl<K: DeepModel, V> View for IntoIter<K, V> {
213        type ViewTy = FMap<K::DeepModelTy, V>;
214    }
215    impl<K: DeepModel, V> IteratorSpec for IntoIter<K, V> {}
216}
creusot_std/std/collections/hash_map.rs

creusot_std/std/collections/
hash_map.rs
