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

creusot_std/std/collections/
hash_map.rs
