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