creusot_std/std/collections/
hash_set.rs

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

creusot_std/std/collections/
hash_set.rs
