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