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