vstd/hash_set.rs
1// altered from HashMap
2use core::marker;
3use std::borrow::Borrow;
4
5#[allow(unused_imports)]
6use super::pervasive::*;
7use super::prelude::*;
8#[allow(unused_imports)]
9use super::set::*;
10#[cfg(verus_keep_ghost)]
11use super::std_specs::hash::obeys_key_model;
12#[allow(unused_imports)]
13use core::hash::Hash;
14use std::collections::HashSet;
15
16verus! {
17
18/// `HashSetWithView` is a trusted wrapper around `std::collections::HashSet` with `View` implemented for the type `vstd::map::Set<<Key as View>::V>`.
19///
20/// See the Rust documentation for [`HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html)
21/// for details about its implementation.
22///
23/// If you are using `std::collections::HashSet` directly, see [`ExHashSet`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/struct.ExHashSet.html)
24/// for information on the Verus specifications for this type.
25#[verifier::ext_equal]
26#[verifier::reject_recursive_types(Key)]
27pub struct HashSetWithView<Key> where Key: View + Eq + Hash {
28 m: HashSet<Key>,
29}
30
31impl<Key> View for HashSetWithView<Key> where Key: View + Eq + Hash {
32 type V = Set<<Key as View>::V>;
33
34 uninterp spec fn view(&self) -> Self::V;
35}
36
37impl<Key> HashSetWithView<Key> where Key: View + Eq + Hash {
38 /// Creates an empty `HashSetWithView` with capacity 0.
39 ///
40 /// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
41 /// for information on use with primitive types and other types.
42 /// See Rust's [`HashSet::new()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.new) for implementation details.
43 #[verifier::external_body]
44 pub fn new() -> (result: Self)
45 requires
46 obeys_key_model::<Key>(),
47 forall|k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,
48 ensures
49 result@ == Set::<<Key as View>::V>::empty(),
50 {
51 Self { m: HashSet::new() }
52 }
53
54 /// Creates an empty `HashSetWithView` with at least capacity for the specified number of elements.
55 ///
56 /// See [`obeys_key_model()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html)
57 /// for information on use with primitive types and other types.
58 /// See Rust's [`HashSet::with_capacity()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.with_capacity) for implementation details.
59 #[verifier::external_body]
60 pub fn with_capacity(capacity: usize) -> (result: Self)
61 requires
62 obeys_key_model::<Key>(),
63 forall|k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,
64 ensures
65 result@ == Set::<<Key as View>::V>::empty(),
66 {
67 Self { m: HashSet::with_capacity(capacity) }
68 }
69
70 /// Reserves capacity for at least `additional` number of elements in the set.
71 ///
72 /// See Rust's [`HashSet::reserve()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.reserve) for implementation details.
73 #[verifier::external_body]
74 pub fn reserve(&mut self, additional: usize)
75 ensures
76 self@ == old(self)@,
77 {
78 self.m.reserve(additional);
79 }
80
81 /// Returns the number of elements in the set.
82 pub uninterp spec fn spec_len(&self) -> usize;
83
84 /// Returns the number of elements in the set.
85 #[verifier::external_body]
86 #[verifier::when_used_as_spec(spec_len)]
87 pub fn len(&self) -> (result: usize)
88 ensures
89 result == self@.len(),
90 {
91 self.m.len()
92 }
93
94 /// Returns true if the set is empty.
95 #[verifier::external_body]
96 pub fn is_empty(&self) -> (result: bool)
97 ensures
98 result == self@.is_empty(),
99 {
100 self.m.is_empty()
101 }
102
103 /// Inserts the given value into the set. Returns true if the value was not previously in the set, false otherwise.
104 ///
105 /// See Rust's [`HashSet::insert()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.insert) for implementation details.
106 #[verifier::external_body]
107 pub fn insert(&mut self, k: Key) -> (result: bool)
108 ensures
109 self@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
110 {
111 self.m.insert(k)
112 }
113
114 /// Removes the given value from the set. Returns true if the value was previously in the set, false otherwise.
115 ///
116 /// See Rust's [`HashSet::remove()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.remove) for implementation details.
117 #[verifier::external_body]
118 pub fn remove(&mut self, k: &Key) -> (result: bool)
119 ensures
120 self@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
121 {
122 self.m.remove(k)
123 }
124
125 /// Returns true if the set contains the given value.
126 ///
127 /// See Rust's [`HashSet::contains()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.contains) for implementation details.
128 #[verifier::external_body]
129 pub fn contains(&self, k: &Key) -> (result: bool)
130 ensures
131 result == self@.contains(k@),
132 {
133 self.m.contains(k)
134 }
135
136 /// 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`.
137 ///
138 /// See Rust's [`HashSet::get()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.get) for implementation details.
139 #[verifier::external_body]
140 pub fn get<'a>(&'a self, k: &Key) -> (result: Option<&'a Key>)
141 ensures
142 match result {
143 Some(v) => self@.contains(k@) && v == &k,
144 None => !self@.contains(k@),
145 },
146 {
147 self.m.get(k)
148 }
149
150 /// Clears all values from the set.
151 ///
152 /// See Rust's [`HashSet::clear()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.clear) for implementation details.
153 #[verifier::external_body]
154 pub fn clear(&mut self)
155 ensures
156 self@ == Set::<<Key as View>::V>::empty(),
157 {
158 self.m.clear()
159 }
160}
161
162pub broadcast axiom fn axiom_hash_set_with_view_spec_len<Key>(m: &HashSetWithView<Key>) where
163 Key: View + Eq + Hash,
164
165 ensures
166 #[trigger] m.spec_len() == m@.len(),
167;
168
169/// `StringHashSet` is a trusted wrapper around `std::collections::HashSet<String>` with `View` implemented for the type `vstd::map::Set<Seq<char>>`.
170///
171/// This type was created for ease of use with `String` as it uses `&str` instead of `&String` for methods that require shared references.
172/// Also, it assumes that [`obeys_key_model::<String>()`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/fn.obeys_key_model.html) holds.
173///
174/// See the Rust documentation for [`HashSet`](https://doc.rust-lang.org/std/collections/struct.HashSet.html)
175/// for details about its implementation.
176///
177/// If you are using `std::collections::HashSet` directly, see [`ExHashSet`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/struct.ExHashSet.html)
178/// for information on the Verus specifications for this type.
179#[verifier::ext_equal]
180pub struct StringHashSet {
181 m: HashSet<String>,
182}
183
184impl View for StringHashSet {
185 type V = Set<Seq<char>>;
186
187 uninterp spec fn view(&self) -> Self::V;
188}
189
190impl StringHashSet {
191 /// Creates an empty `StringHashSet` with capacity 0.
192 ///
193 /// See Rust's [`HashSet::new()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.new) for implementation details.
194 #[verifier::external_body]
195 pub fn new() -> (result: Self)
196 ensures
197 result@ == Set::<Seq<char>>::empty(),
198 {
199 Self { m: HashSet::new() }
200 }
201
202 /// Creates an empty `StringHashSet` with at least capacity for the specified number of elements.
203 ///
204 /// See Rust's [`HashSet::with_capacity()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.with_capacity) for implementation details.
205 #[verifier::external_body]
206 pub fn with_capacity(capacity: usize) -> (result: Self)
207 ensures
208 result@ == Set::<Seq<char>>::empty(),
209 {
210 Self { m: HashSet::with_capacity(capacity) }
211 }
212
213 /// Reserves capacity for at least `additional` number of elements in the set.
214 ///
215 /// See Rust's [`HashSet::reserve()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.reserve) for implementation details.
216 #[verifier::external_body]
217 pub fn reserve(&mut self, additional: usize)
218 ensures
219 self@ == old(self)@,
220 {
221 self.m.reserve(additional);
222 }
223
224 /// Returns true if the set is empty.
225 #[verifier::external_body]
226 pub fn is_empty(&self) -> (result: bool)
227 ensures
228 result == self@.is_empty(),
229 {
230 self.m.is_empty()
231 }
232
233 /// Returns the number of elements in the set.
234 pub uninterp spec fn spec_len(&self) -> usize;
235
236 /// Returns the number of elements in the set.
237 #[verifier::external_body]
238 #[verifier::when_used_as_spec(spec_len)]
239 pub fn len(&self) -> (result: usize)
240 ensures
241 result == self@.len(),
242 {
243 self.m.len()
244 }
245
246 /// Inserts the given value into the set. Returns true if the value was not previously in the set, false otherwise.
247 ///
248 /// See Rust's [`HashSet::insert()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.insert) for implementation details.
249 #[verifier::external_body]
250 pub fn insert(&mut self, k: String) -> (result: bool)
251 ensures
252 self@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
253 {
254 self.m.insert(k)
255 }
256
257 /// Removes the given value from the set. Returns true if the value was previously in the set, false otherwise.
258 ///
259 /// See Rust's [`HashSet::remove()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.remove) for implementation details.
260 #[verifier::external_body]
261 pub fn remove(&mut self, k: &str) -> (result: bool)
262 ensures
263 self@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
264 {
265 self.m.remove(k)
266 }
267
268 /// Returns true if the set contains the given value.
269 ///
270 /// See Rust's [`HashSet::contains()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.contains) for implementation details.
271 #[verifier::external_body]
272 pub fn contains(&self, k: &str) -> (result: bool)
273 ensures
274 result == self@.contains(k@),
275 {
276 self.m.contains(k)
277 }
278
279 /// 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`.
280 ///
281 /// See Rust's [`HashSet::get()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.get) for implementation details.
282 #[verifier::external_body]
283 pub fn get<'a>(&'a self, k: &str) -> (result: Option<&'a String>)
284 ensures
285 match result {
286 Some(v) => self@.contains(k@) && v@ == k@,
287 None => !self@.contains(k@),
288 },
289 {
290 self.m.get(k)
291 }
292
293 /// Clears all values from the set.
294 ///
295 /// See Rust's [`HashSet::clear()`](https://doc.rust-lang.org/std/collections/struct.HashSet.html#method.clear) for implementation details.
296 #[verifier::external_body]
297 pub fn clear(&mut self)
298 ensures
299 self@ == Set::<Seq<char>>::empty(),
300 {
301 self.m.clear()
302 }
303}
304
305pub broadcast axiom fn axiom_string_hash_set_spec_len(m: &StringHashSet)
306 ensures
307 #[trigger] m.spec_len() == m@.len(),
308;
309
310pub broadcast group group_hash_set_axioms {
311 axiom_hash_set_with_view_spec_len,
312 axiom_string_hash_set_spec_len,
313}
314
315} // verus!