creusot_contracts/std/collections/
hash_map.rs

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

creusot_contracts/std/collections/
hash_map.rs
