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