creusot_std/std/collections/
hash_map.rs

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

creusot_std/std/collections/
hash_map.rs
