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. If the key is not present in the map, the map is unmodified.
114 ///
115 /// See Rust's [`HashMap::remove()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.remove) for implementation details.
116 #[verifier::external_body]
117 pub fn remove(&mut self, k: &Key)
118 ensures
119 self@ == old(self)@.remove(k@),
120 {
121 self.m.remove(k);
122 }
123
124 /// Returns true if the map contains the given key.
125 ///
126 /// See Rust's [`HashMap::contains_key()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.contains_key) for implementation details.
127 #[verifier::external_body]
128 pub fn contains_key(&self, k: &Key) -> (result: bool)
129 ensures
130 result == self@.contains_key(k@),
131 {
132 self.m.contains_key(k)
133 }
134
135 /// 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`.
136 ///
137 /// See Rust's [`HashMap::get()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.get) for implementation details.
138 #[verifier::external_body]
139 pub fn get<'a>(&'a self, k: &Key) -> (result: Option<&'a Value>)
140 ensures
141 match result {
142 Some(v) => self@.contains_key(k@) && *v == self@[k@],
143 None => !self@.contains_key(k@),
144 },
145 {
146 self.m.get(k)
147 }
148
149 /// Clears all key-value pairs in the map. Retains the allocated memory for reuse.
150 ///
151 /// See Rust's [`HashMap::clear()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.clear) for implementation details.
152 #[verifier::external_body]
153 pub fn clear(&mut self)
154 ensures
155 self@ == Map::<<Key as View>::V, Value>::empty(),
156 {
157 self.m.clear()
158 }
159
160 /// 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.
161 #[verifier::external_body]
162 pub fn union_prefer_right(&mut self, other: Self)
163 ensures
164 self@ == old(self)@.union_prefer_right(other@),
165 {
166 self.m.extend(other.m)
167 }
168}
169
170pub broadcast axiom fn axiom_hash_map_with_view_spec_len<Key, Value>(
171 m: &HashMapWithView<Key, Value>,
172) where Key: View + Eq + Hash
173 ensures
174 #[trigger] m.spec_len() == m@.len(),
175;
176
177/// `StringHashMap` is a trusted wrapper around `std::collections::HashMap<String, Value>` with `View` implemented for the type `vstd::map::Map<Seq<char>, Value>`.
178///
179/// This type was created for ease of use with `String` as it uses `&str` instead of `&String` for methods that require shared references.
180/// 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.
181///
182/// See the Rust documentation for [`HashMap`](https://doc.rust-lang.org/std/collections/struct.HashMap.html)
183/// for details about its implementation.
184///
185/// If you are using `std::collections::HashMap` directly, see [`ExHashMap`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/hash/struct.ExHashMap.html)
186/// for information on the Verus specifications for this type.
187#[verifier::ext_equal]
188#[verifier::reject_recursive_types(Value)]
189pub struct StringHashMap<Value> {
190 m: HashMap<String, Value>,
191}
192
193impl<Value> View for StringHashMap<Value> {
194 type V = Map<Seq<char>, Value>;
195
196 uninterp spec fn view(&self) -> Self::V;
197}
198
199impl<Value> StringHashMap<Value> {
200 /// Creates an empty `StringHashMap` with a capacity of 0.
201 ///
202 /// See Rust's [`HashMap::new()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.new) for implementation details.
203 #[verifier::external_body]
204 pub fn new() -> (result: Self)
205 ensures
206 result@ == Map::<Seq<char>, Value>::empty(),
207 {
208 Self { m: HashMap::new() }
209 }
210
211 /// Creates an empty `StringHashMap` with at least capacity for the specified number of elements.
212 ///
213 /// See Rust's [`HashMap::with_capacity()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.with_capacity) for implementation details.
214 #[verifier::external_body]
215 pub fn with_capacity(capacity: usize) -> (result: Self)
216 ensures
217 result@ == Map::<Seq<char>, Value>::empty(),
218 {
219 Self { m: HashMap::with_capacity(capacity) }
220 }
221
222 /// Reserves capacity for at least `additional` number of elements in the map.
223 ///
224 /// See Rust's [`HashMap::reserve()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.reserve) for implementation details.
225 #[verifier::external_body]
226 pub fn reserve(&mut self, additional: usize)
227 ensures
228 self@ == old(self)@,
229 {
230 self.m.reserve(additional);
231 }
232
233 /// Returns true if the map is empty.
234 #[verifier::external_body]
235 pub fn is_empty(&self) -> (result: bool)
236 ensures
237 result == self@.is_empty(),
238 {
239 self.m.is_empty()
240 }
241
242 /// Returns the number of elements in the map.
243 pub uninterp spec fn spec_len(&self) -> usize;
244
245 /// Returns the number of elements in the map.
246 #[verifier::external_body]
247 #[verifier::when_used_as_spec(spec_len)]
248 pub fn len(&self) -> (result: usize)
249 ensures
250 result == self@.len(),
251 {
252 self.m.len()
253 }
254
255 /// Inserts the given key and value in the map.
256 ///
257 /// See Rust's [`HashMap::insert()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.insert) for implementation details.
258 #[verifier::external_body]
259 pub fn insert(&mut self, k: String, v: Value)
260 ensures
261 self@ == old(self)@.insert(k@, v),
262 {
263 self.m.insert(k, v);
264 }
265
266 /// Removes the given key from the map. If the key is not present in the map, the map is unmodified.
267 ///
268 /// See Rust's [`HashMap::remove()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.remove) for implementation details.
269 #[verifier::external_body]
270 pub fn remove(&mut self, k: &str)
271 ensures
272 self@ == old(self)@.remove(k@),
273 {
274 self.m.remove(k);
275 }
276
277 /// Returns true if the map contains the given key.
278 ///
279 /// See Rust's [`HashMap::contains_key()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.contains_key) for implementation details.
280 #[verifier::external_body]
281 pub fn contains_key(&self, k: &str) -> (result: bool)
282 ensures
283 result == self@.contains_key(k@),
284 {
285 self.m.contains_key(k)
286 }
287
288 /// 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`.
289 ///
290 /// See Rust's [`HashMap::get()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.get) for implementation details.
291 #[verifier::external_body]
292 pub fn get<'a>(&'a self, k: &str) -> (result: Option<&'a Value>)
293 ensures
294 match result {
295 Some(v) => self@.contains_key(k@) && *v == self@[k@],
296 None => !self@.contains_key(k@),
297 },
298 {
299 self.m.get(k)
300 }
301
302 /// Clears all key-value pairs in the map. Retains the allocated memory for reuse.
303 ///
304 /// See Rust's [`HashMap::clear()`](https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.clear) for implementation details.
305 #[verifier::external_body]
306 pub fn clear(&mut self)
307 ensures
308 self@ == Map::<Seq<char>, Value>::empty(),
309 {
310 self.m.clear()
311 }
312
313 /// 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.
314 #[verifier::external_body]
315 pub fn union_prefer_right(&mut self, other: Self)
316 ensures
317 self@ == old(self)@.union_prefer_right(other@),
318 {
319 self.m.extend(other.m)
320 }
321}
322
323pub broadcast axiom fn axiom_string_hash_map_spec_len<Value>(m: &StringHashMap<Value>)
324 ensures
325 #[trigger] m.spec_len() == m@.len(),
326;
327
328pub broadcast group group_hash_map_axioms {
329 axiom_hash_map_with_view_spec_len,
330 axiom_string_hash_map_spec_len,
331}
332
333} // verus!