vstd/hash_set.rs
1// altered from HashMap
2use core::marker;
3use std::borrow::Borrow;
4
5#[cfg(verus_keep_ghost)]
6use super::laws_eq::obeys_view_eq;
7#[allow(unused_imports)]
8use super::pervasive::*;
9use super::prelude::*;
10#[allow(unused_imports)]
11use super::set::*;
12#[cfg(verus_keep_ghost)]
13use super::set_lib::assert_sets_equal;
14#[cfg(verus_keep_ghost)]
15use super::std_specs::borrow::BorrowSpec;
16#[cfg(verus_keep_ghost)]
17use super::std_specs::cmp::PartialEqSpec;
18#[cfg(verus_keep_ghost)]
19use super::std_specs::hash::{hash_set_inv, obeys_key_model};
20#[allow(unused_imports)]
21use core::hash::Hash;
22use std::collections::HashSet;
23
24verus! {
25
26broadcast use {
27 crate::set::group_set_lemmas,
28 crate::set::Set::lemma_map_contains,
29 crate::set::Set::lemma_set_map_insert_commute,
30 crate::std_specs::hash::group_hash_axioms,
31 crate::std_specs::borrow::group_borrow_axioms,
32};
33
34/// `HashSetWithView` is a verified wrapper around `std::collections::HashSet` with `View` implemented for the type `vstd::set::Set<<Key as View>::V>`.
35///
36/// Its constructors require [`obeys_view_eq`] in addition to [`obeys_key_model`].
37/// Constructors establish [`Self::well_formed`], which all other operations require and preserve.
38///
39/// See the Rust documentation for [`HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html)
40/// for details about its implementation.
41///
42/// If you are using `std::collections::HashSet` directly, see [`ExHashSet`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/struct.ExHashSet.html)
43/// for information on the Verus specifications for this type.
44#[verifier::ext_equal]
45#[verifier::reject_recursive_types(Key)]
46pub struct HashSetWithView<Key> where Key: View + Eq + Hash {
47 m: HashSet<Key>,
48}
49
50impl<Key> View for HashSetWithView<Key> where Key: View + Eq + Hash {
51 type V = Set<<Key as View>::V>;
52
53 closed spec fn view(&self) -> Self::V {
54 self.m@.map(|k: Key| k@)
55 }
56}
57
58impl<Key> HashSetWithView<Key> where Key: View + Eq + Hash {
59 pub closed spec fn well_formed(&self) -> bool {
60 &&& obeys_key_model::<Key>()
61 &&& obeys_view_eq::<Key>()
62 &&& hash_set_inv(&self.m)
63 }
64
65 proof fn lemma_view(&self)
66 requires
67 self.well_formed(),
68 ensures
69 self@.len() == self.m@.len(),
70 forall|k: Key| #[trigger] self.m@.contains(k) ==> self@.contains(k@),
71 forall|view: Key::V| #[trigger]
72 self@.contains(view) ==> exists|k: Key| #[trigger]
73 self.m@.contains(k) && k@ == view,
74 {
75 reveal(obeys_view_eq);
76 assert(self.m@.injective_on(|k: Key| k@));
77 crate::set_lib::lemma_map_size(self.m@, self@, |k: Key| k@);
78 }
79
80 /// Creates an empty `HashSetWithView`.
81 ///
82 /// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
83 /// for information on use with primitive types and other types.
84 /// See Rust's [`HashSet::new()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.new) for implementation details.
85 pub fn new() -> (result: Self)
86 requires
87 obeys_key_model::<Key>(),
88 obeys_view_eq::<Key>(),
89 ensures
90 result.well_formed(),
91 result@ == Set::<<Key as View>::V>::empty(),
92 {
93 Self { m: HashSet::new() }
94 }
95
96 /// Creates an empty `HashSetWithView` with at least capacity for the specified number of elements.
97 ///
98 /// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
99 /// for information on use with primitive types and other types.
100 /// See Rust's [`HashSet::with_capacity()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.with_capacity) for implementation details.
101 pub fn with_capacity(capacity: usize) -> (result: Self)
102 requires
103 obeys_key_model::<Key>(),
104 obeys_view_eq::<Key>(),
105 ensures
106 result.well_formed(),
107 result@ == Set::<<Key as View>::V>::empty(),
108 {
109 Self { m: HashSet::with_capacity(capacity) }
110 }
111
112 /// Reserves capacity for at least `additional` number of elements in the set.
113 ///
114 /// See Rust's [`HashSet::reserve()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.reserve) for implementation details.
115 pub fn reserve(&mut self, additional: usize)
116 requires
117 old(self).well_formed(),
118 ensures
119 final(self).well_formed(),
120 final(self)@ == old(self)@,
121 {
122 self.m.reserve(additional);
123 }
124
125 /// Returns the number of elements in the set.
126 pub open spec fn spec_len(&self) -> usize {
127 self@.len() as usize
128 }
129
130 /// Returns the number of elements in the set.
131 #[verifier::when_used_as_spec(spec_len)]
132 pub fn len(&self) -> (result: usize)
133 requires
134 self.well_formed(),
135 ensures
136 result == self@.len(),
137 {
138 proof {
139 self.lemma_view();
140 }
141 self.m.len()
142 }
143
144 /// Returns true if the set is empty.
145 pub fn is_empty(&self) -> (result: bool)
146 requires
147 self.well_formed(),
148 ensures
149 result == self@.is_empty(),
150 {
151 proof {
152 self.lemma_view();
153 }
154 self.m.is_empty()
155 }
156
157 /// Inserts the given value into the set. Returns true if the value was not previously in the set, false otherwise.
158 ///
159 /// See Rust's [`HashSet::insert()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.insert) for implementation details.
160 pub fn insert(&mut self, k: Key) -> (result: bool)
161 requires
162 old(self).well_formed(),
163 ensures
164 final(self).well_formed(),
165 final(self)@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
166 {
167 proof {
168 reveal(obeys_view_eq);
169 self.lemma_view();
170 }
171 let result = self.m.insert(k);
172 proof {
173 self.lemma_view();
174 }
175 result
176 }
177
178 /// Removes the given value from the set. Returns true if the value was previously in the set, false otherwise.
179 ///
180 /// See Rust's [`HashSet::remove()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.remove) for implementation details.
181 pub fn remove(&mut self, k: &Key) -> (result: bool)
182 requires
183 old(self).well_formed(),
184 ensures
185 final(self).well_formed(),
186 final(self)@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
187 {
188 proof {
189 reveal(obeys_view_eq);
190 self.lemma_view();
191 }
192 let ghost before = self@;
193 let ghost old_m = self.m@;
194 let result = self.m.remove(k);
195 proof {
196 self.lemma_view();
197 if result {
198 assert_sets_equal!(self@, before.remove(k@), view => {
199 if self@.contains(view) {
200 let stored = choose|stored: Key|
201 #[trigger] self.m@.contains(stored) && stored@ == view;
202 assert(view != k@);
203 }
204 if before.contains(view) && view != k@ {
205 let stored = choose|stored: Key|
206 #[trigger] old_m.contains(stored) && stored@ == view;
207 assert(self.m@.contains(stored));
208 }
209 });
210 }
211 }
212 result
213 }
214
215 /// Returns true if the set contains the given value.
216 ///
217 /// See Rust's [`HashSet::contains()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.contains) for implementation details.
218 pub fn contains(&self, k: &Key) -> (result: bool)
219 requires
220 self.well_formed(),
221 ensures
222 result == self@.contains(k@),
223 {
224 proof {
225 reveal(obeys_view_eq);
226 self.lemma_view();
227 }
228 self.m.contains(k)
229 }
230
231 /// Returns a reference to the value in the set that is equal to the given value. If the value is not present in the set, returns `None`.
232 ///
233 /// See Rust's [`HashSet::get()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.get) for implementation details.
234 pub fn get<'a>(&'a self, k: &Key) -> (result: Option<&'a Key>)
235 requires
236 self.well_formed(),
237 ensures
238 match result {
239 Some(v) => self@.contains(k@) && v@ == k@,
240 None => !self@.contains(k@),
241 },
242 {
243 proof {
244 reveal(obeys_view_eq);
245 self.lemma_view();
246 }
247 self.m.get(k)
248 }
249
250 /// Clears all values from the set.
251 ///
252 /// See Rust's [`HashSet::clear()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.clear) for implementation details.
253 pub fn clear(&mut self)
254 requires
255 old(self).well_formed(),
256 ensures
257 final(self).well_formed(),
258 final(self)@ == Set::<<Key as View>::V>::empty(),
259 {
260 self.m.clear()
261 }
262}
263
264/// `StringHashSet` is a verified wrapper around `std::collections::HashSet<String>` with `View` implemented for the type `vstd::set::Set<Seq<char>>`.
265///
266/// This type was created for ease of use with `String` as it uses `&str` instead of `&String` for methods that require shared references.
267/// Constructors establish [`Self::well_formed`], which all other operations require and preserve.
268/// Standard-library axioms provide the key models for `String` and `str`.
269///
270/// See the Rust documentation for [`HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html)
271/// for details about its implementation.
272///
273/// If you are using `std::collections::HashSet` directly, see [`ExHashSet`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/struct.ExHashSet.html)
274/// for information on the Verus specifications for this type.
275#[verifier::ext_equal]
276pub struct StringHashSet {
277 m: HashSetWithView<String>,
278}
279
280impl View for StringHashSet {
281 type V = Set<Seq<char>>;
282
283 closed spec fn view(&self) -> Self::V {
284 self.m@
285 }
286}
287
288impl StringHashSet {
289 pub closed spec fn well_formed(&self) -> bool {
290 self.m.well_formed()
291 }
292
293 /// Creates an empty `StringHashSet`.
294 ///
295 /// See Rust's [`HashSet::new()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.new) for implementation details.
296 pub fn new() -> (result: Self)
297 ensures
298 result.well_formed(),
299 result@ == Set::<Seq<char>>::empty(),
300 {
301 proof {
302 reveal(obeys_view_eq);
303 }
304 Self { m: HashSetWithView::new() }
305 }
306
307 /// Creates an empty `StringHashSet` with at least capacity for the specified number of elements.
308 ///
309 /// See Rust's [`HashSet::with_capacity()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.with_capacity) for implementation details.
310 pub fn with_capacity(capacity: usize) -> (result: Self)
311 ensures
312 result.well_formed(),
313 result@ == Set::<Seq<char>>::empty(),
314 {
315 proof {
316 reveal(obeys_view_eq);
317 }
318 Self { m: HashSetWithView::with_capacity(capacity) }
319 }
320
321 /// Reserves capacity for at least `additional` number of elements in the set.
322 ///
323 /// See Rust's [`HashSet::reserve()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.reserve) for implementation details.
324 pub fn reserve(&mut self, additional: usize)
325 requires
326 old(self).well_formed(),
327 ensures
328 final(self).well_formed(),
329 final(self)@ == old(self)@,
330 {
331 self.m.reserve(additional);
332 }
333
334 /// Returns true if the set is empty.
335 pub fn is_empty(&self) -> (result: bool)
336 requires
337 self.well_formed(),
338 ensures
339 result == self@.is_empty(),
340 {
341 self.m.is_empty()
342 }
343
344 /// Returns the number of elements in the set.
345 pub open spec fn spec_len(&self) -> usize {
346 self@.len() as usize
347 }
348
349 /// Returns the number of elements in the set.
350 #[verifier::when_used_as_spec(spec_len)]
351 pub fn len(&self) -> (result: usize)
352 requires
353 self.well_formed(),
354 ensures
355 result == self@.len(),
356 {
357 self.m.len()
358 }
359
360 /// Inserts the given value into the set. Returns true if the value was not previously in the set, false otherwise.
361 ///
362 /// See Rust's [`HashSet::insert()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.insert) for implementation details.
363 pub fn insert(&mut self, k: String) -> (result: bool)
364 requires
365 old(self).well_formed(),
366 ensures
367 final(self).well_formed(),
368 final(self)@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
369 {
370 self.m.insert(k)
371 }
372
373 /// Removes the given value from the set. Returns true if the value was previously in the set, false otherwise.
374 ///
375 /// See Rust's [`HashSet::remove()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.remove) for implementation details.
376 pub fn remove(&mut self, k: &str) -> (result: bool)
377 requires
378 old(self).well_formed(),
379 ensures
380 final(self).well_formed(),
381 final(self)@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
382 {
383 proof {
384 self.m.lemma_view();
385 }
386 let ghost before = self@;
387 let ghost old_m = self.m.m@;
388 let result = self.m.m.remove(k);
389 proof {
390 self.m.lemma_view();
391 if !result && before.contains(k@) {
392 let stored = choose|stored: String| #[trigger]
393 old_m.contains(stored) && stored@ == k@;
394 assert(k.eq_spec(<String as BorrowSpec<str>>::borrow_spec(&stored)));
395 }
396 assert_sets_equal!(self@, before.remove(k@), view => {
397 if self@.contains(view) {
398 let stored = choose|stored: String| #[trigger]
399 self.m.m@.contains(stored) && stored@ == view;
400 assert(view != k@);
401 }
402 if before.contains(view) && view != k@ {
403 let stored = choose|stored: String| #[trigger]
404 old_m.contains(stored) && stored@ == view;
405 assert(self.m.m@.contains(stored));
406 }
407 });
408 }
409 result
410 }
411
412 /// Returns true if the set contains the given value.
413 ///
414 /// See Rust's [`HashSet::contains()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.contains) for implementation details.
415 pub fn contains(&self, k: &str) -> (result: bool)
416 requires
417 self.well_formed(),
418 ensures
419 result == self@.contains(k@),
420 {
421 self.get(k).is_some()
422 }
423
424 /// Returns a reference to the value in the set that is equal to the given value. If the value is not present in the set, returns `None`.
425 ///
426 /// See Rust's [`HashSet::get()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.get) for implementation details.
427 pub fn get<'a>(&'a self, k: &str) -> (result: Option<&'a String>)
428 requires
429 self.well_formed(),
430 ensures
431 match result {
432 Some(v) => self@.contains(k@) && v@ == k@,
433 None => !self@.contains(k@),
434 },
435 {
436 proof {
437 self.m.lemma_view();
438 }
439 let result = self.m.m.get(k);
440 proof {
441 match result {
442 Some(stored) => {
443 assert(stored@ == k@);
444 },
445 None => {
446 if self@.contains(k@) {
447 let stored = choose|stored: String| #[trigger]
448 self.m.m@.contains(stored) && stored@ == k@;
449 assert(k.eq_spec(<String as BorrowSpec<str>>::borrow_spec(&stored)));
450 }
451 },
452 }
453 }
454 result
455 }
456
457 /// Clears all values from the set.
458 ///
459 /// See Rust's [`HashSet::clear()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.clear) for implementation details.
460 pub fn clear(&mut self)
461 requires
462 old(self).well_formed(),
463 ensures
464 final(self).well_formed(),
465 final(self)@ == Set::<Seq<char>>::empty(),
466 {
467 self.m.clear()
468 }
469}
470
471} // verus!