creusot_std/std/collections/
hash_set.rs

1use crate::{
2    logic::FSet,
3    prelude::*,
4    std::iter::{FromIteratorSpec, 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#[cfg(feature = "nightly")]
58impl<T: DeepModel, A: Allocator> View for IntoIter<T, A> {
59    type ViewTy = FSet<T::DeepModelTy>;
60
61    #[logic(opaque)]
62    fn view(self) -> Self::ViewTy {
63        dead
64    }
65}
66
67#[logic(open)]
68pub fn set_produces<T: DeepModel, I: View<ViewTy = FSet<T::DeepModelTy>>>(
69    start: I,
70    visited: Seq<T>,
71    end: I,
72) -> bool {
73    pearlite! { start@.len() == visited.len() + end@.len()
74        && (forall<x: T::DeepModelTy> start@.contains(x) ==> (exists<x1: T> x1.deep_model() == x && visited.contains(x1)) || end@.contains(x))
75        && (forall<x: T> visited.contains(x) ==> start@.contains(x.deep_model()) && !end@.contains(x.deep_model()))
76        && (forall<x: T::DeepModelTy> end@.contains(x) ==> start@.contains(x) && !exists<x1: T> x1.deep_model() == x && visited.contains(x1))
77        && (forall<i, j>
78            0 <= i && i < visited.len() && 0 <= j && j < visited.len()
79            && visited[i].deep_model() == visited[j].deep_model()
80            ==> i == j)
81    }
82}
83
84#[logic(open)]
85#[requires(set_produces(a, ab, b))]
86#[requires(set_produces(b, bc, c))]
87#[ensures(set_produces(a, ab.concat(bc), c))]
88pub fn set_produces_trans<T: DeepModel, I: View<ViewTy = FSet<T::DeepModelTy>>>(
89    a: I,
90    ab: Seq<T>,
91    b: I,
92    bc: Seq<T>,
93    c: I,
94) {
95    Seq::<T>::concat_contains();
96    proof_assert! { forall<i, x: T> ab.len() <= i && ab.concat(bc).get(i) == Some(x) ==> bc.contains(x) };
97    proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] };
98}
99
100impl<T: DeepModel> IteratorSpec for IntoIter<T> {
101    #[logic(open, prophetic)]
102    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
103        set_produces(self, visited, o)
104    }
105
106    #[logic(open, prophetic)]
107    fn completed(&mut self) -> bool {
108        pearlite! { (self@).is_empty() }
109    }
110
111    #[logic(open, law)]
112    #[ensures(self.produces(Seq::empty(), self))]
113    fn produces_refl(self) {}
114
115    #[logic(open, law)]
116    #[requires(a.produces(ab, b))]
117    #[requires(b.produces(bc, c))]
118    #[ensures(a.produces(ab.concat(bc), c))]
119    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
120        set_produces_trans(a, ab, b, bc, c);
121    }
122}
123
124impl<'a, T: DeepModel> View for Iter<'a, T> {
125    type ViewTy = FSet<T::DeepModelTy>;
126
127    #[logic(opaque)]
128    fn view(self) -> Self::ViewTy {
129        dead
130    }
131}
132
133impl<'a, T: DeepModel> IteratorSpec for Iter<'a, T> {
134    #[logic(open, prophetic)]
135    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
136        set_produces(self, visited, o)
137    }
138
139    #[logic(open, prophetic)]
140    fn completed(&mut self) -> bool {
141        pearlite! { (self@).is_empty() }
142    }
143
144    #[logic(open, law)]
145    #[ensures(self.produces(Seq::empty(), self))]
146    fn produces_refl(self) {}
147
148    #[logic(open, law)]
149    #[requires(a.produces(ab, b))]
150    #[requires(b.produces(bc, c))]
151    #[ensures(a.produces(ab.concat(bc), c))]
152    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
153        set_produces_trans(a, ab, b, bc, c);
154    }
155}
156
157impl<T: Eq + Hash + DeepModel, S: Default + BuildHasher> FromIteratorSpec<T> for HashSet<T, S> {
158    #[logic(open)]
159    fn from_iter_post(prod: Seq<T>, res: Self) -> bool {
160        pearlite! { forall<x: T::DeepModelTy> res@.contains(x) == exists<x1: T> x1.deep_model() == x && prod.contains(x1) }
161    }
162}
163
164#[cfg(feature = "nightly")]
165impl<'a, T: DeepModel, S, A: Allocator> View for Intersection<'a, T, S, A> {
166    type ViewTy = FSet<T::DeepModelTy>;
167
168    #[logic(opaque)]
169    fn view(self) -> Self::ViewTy {
170        dead
171    }
172}
173
174#[cfg(feature = "nightly")]
175impl<'a, T: DeepModel, S, A: Allocator> View for Difference<'a, T, S, A> {
176    type ViewTy = FSet<T::DeepModelTy>;
177
178    #[logic(opaque)]
179    fn view(self) -> Self::ViewTy {
180        dead
181    }
182}
183
184impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> IteratorSpec for Intersection<'a, T, S> {
185    #[logic(open, prophetic)]
186    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
187        set_produces(self, visited, o)
188    }
189
190    #[logic(open, prophetic)]
191    fn completed(&mut self) -> bool {
192        pearlite! { resolve(self) && (self@).is_empty() }
193    }
194
195    #[logic(open, law)]
196    #[ensures(self.produces(Seq::empty(), self))]
197    fn produces_refl(self) {}
198
199    #[logic(open, law)]
200    #[requires(a.produces(ab, b))]
201    #[requires(b.produces(bc, c))]
202    #[ensures(a.produces(ab.concat(bc), c))]
203    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
204        set_produces_trans(a, ab, b, bc, c);
205    }
206}
207
208impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> IteratorSpec for Difference<'a, T, S> {
209    #[logic(open, prophetic)]
210    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
211        set_produces(self, visited, o)
212    }
213
214    #[logic(open, prophetic)]
215    fn completed(&mut self) -> bool {
216        pearlite! { resolve(self) && (self@).is_empty() }
217    }
218
219    #[logic(open, law)]
220    #[ensures(self.produces(Seq::empty(), self))]
221    fn produces_refl(self) {}
222
223    #[logic(open, law)]
224    #[requires(a.produces(ab, b))]
225    #[requires(b.produces(bc, c))]
226    #[ensures(a.produces(ab.concat(bc), c))]
227    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
228        set_produces_trans(a, ab, b, bc, c);
229    }
230}
231
232#[cfg(not(feature = "nightly"))]
233mod impls {
234    use crate::{logic::FSet, prelude::*};
235    use std::collections::hash_set::{Difference, HashSet, Intersection, IntoIter};
236
237    impl<K: DeepModel, S> View for HashSet<K, S> {
238        type ViewTy = FSet<K::DeepModelTy>;
239    }
240    impl<K: DeepModel> View for IntoIter<K> {
241        type ViewTy = FSet<K::DeepModelTy>;
242    }
243    impl<'a, T: DeepModel, S> View for Intersection<'a, T, S> {
244        type ViewTy = FSet<T::DeepModelTy>;
245    }
246    impl<'a, T: DeepModel, S> View for Difference<'a, T, S> {
247        type ViewTy = FSet<T::DeepModelTy>;
248    }
249}
creusot_std/std/collections/hash_set.rs

creusot_std/std/collections/
hash_set.rs
