creusot_contracts/std/collections/
hash_set.rs

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

creusot_contracts/std/collections/
hash_set.rs
