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