vstd/contrib/exec_spec/
map.rs

1//! This module contains [`Map`]-specific method implementations.
2use crate::contrib::exec_spec::*;
3use crate::prelude::*;
4use std::collections::{HashMap, HashSet};
5
6verus! {
7
8// Note: many of the exec translations are currently unverified, even though the exec functions have specs in vstd.
9// This is because HashMap<K, V>::deep_view() is quite hard to work with.
10broadcast use {
11    crate::group_vstd_default,
12    crate::std_specs::hash::group_hash_axioms,
13    crate::std_specs::hash::lemma_hashmap_deepview_dom,
14};
15
16/// Impls for shared traits
17impl<
18    'a,
19    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
20    V: DeepView + DeepViewClone,
21> ToRef<&'a HashMap<K, V>> for &'a HashMap<K, V> {
22    #[inline(always)]
23    fn get_ref(self) -> &'a HashMap<K, V> {
24        &self
25    }
26}
27
28impl<
29    'a,
30    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
31    V: DeepView + DeepViewClone,
32> ToOwned<HashMap<K, V>> for &'a HashMap<K, V> {
33    #[verifier::external_body]
34    #[inline(always)]
35    fn get_owned(self) -> HashMap<K, V> {
36        let mut new_map = HashMap::new();
37        for (k, v) in self.iter() {
38            new_map.insert(k.deep_clone(), v.deep_clone());
39        }
40        new_map
41    }
42}
43
44impl<
45    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
46    V: DeepView + DeepViewClone,
47> DeepViewClone for HashMap<K, V> {
48    #[verifier::external_body]
49    #[inline(always)]
50    fn deep_clone(&self) -> Self {
51        let mut new_map = HashMap::new();
52        for (k, v) in self.iter() {
53            new_map.insert(k.deep_clone(), v.deep_clone());
54        }
55        new_map
56    }
57}
58
59/// `HashMap`'s `==` compares lengths and then values key by key,
60/// which is deep-view equality when both `K` and `V` obey deep equality.
61#[cfg(verus_keep_ghost)]
62impl<
63    K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq,
64    V: ObeysDeepEq,
65    S: std::hash::BuildHasher,
66    A: core::alloc::Allocator,
67> crate::std_specs::cmp::PartialEqSpecImpl for HashMap<K, V, S, A> {
68    open spec fn obeys_eq_spec() -> bool {
69        crate::std_specs::hash::builds_valid_hashers::<S>()
70    }
71
72    open spec fn eq_spec(&self, other: &Self) -> bool {
73        self.deep_view() == other.deep_view()
74    }
75}
76
77impl<K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq, V: ObeysDeepEq> ObeysDeepEq for HashMap<
78    K,
79    V,
80> {
81    proof fn lemma_obeys_deep_eq() {
82        reveal(crate::laws_eq::obeys_deep_eq);
83    }
84}
85
86impl<
87    'a,
88    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
89    V: DeepView + DeepViewClone,
90> ExecSpecLen for &'a HashMap<K, V> {
91    #[inline(always)]
92    #[verifier::external_body]
93    fn exec_len(self) -> (res: usize)
94        ensures
95            res == self.deep_view().len(),
96    {
97        self.len()
98    }
99}
100
101/// Traits for Map methods
102/// Spec for executable version of [`Map::empty`].
103pub trait ExecSpecMapEmpty: Sized {
104    fn exec_empty() -> Self;
105}
106
107// todo: this only works for primtive key types right now
108/// Spec for executable version of [`Map`] indexing.
109pub trait ExecSpecMapIndex<'a>: Sized + DeepView<
110    V = Map<<Self::Key as DeepView>::V, <Self::Value as DeepView>::V>,
111> {
112    type Key: DeepView;
113
114    type Value: DeepView;
115
116    fn exec_index(self, key: Self::Key) -> Self::Value
117        requires
118            self.deep_view().dom().contains(key.deep_view()),
119    ;
120}
121
122/// Spec for executable version of [`Map::insert`].
123pub trait ExecSpecMapInsert<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
124    type Key: DeepView + DeepViewClone;
125
126    type Value: DeepView + DeepViewClone;
127
128    fn exec_insert(self, key: Self::Key, value: Self::Value) -> Out;
129}
130
131/// Spec for executable version of [`Map::remove`].
132pub trait ExecSpecMapRemove<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
133    type Key: DeepView + DeepViewClone;
134
135    fn exec_remove(self, key: Self::Key) -> Out;
136}
137
138/// Spec for executable version of [`Map::dom`].
139pub trait ExecSpecMapDom<'a>: Sized + DeepView {
140    type Key: DeepView + DeepViewClone;
141
142    fn exec_dom(self) -> HashSet<Self::Key>;
143}
144
145/// Spec for executable version of [`Map::get`].
146pub trait ExecSpecMapGet<'a>: Sized + DeepView {
147    type Key: DeepView + DeepViewClone;
148
149    type Value: DeepView + DeepViewClone;
150
151    fn exec_get(self, k: Self::Key) -> Option<Self::Value>;
152}
153
154/// Impls for executable versions of Map methods
155impl<K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq, V: DeepView> ExecSpecMapEmpty for HashMap<
156    K,
157    V,
158> {
159    #[inline(always)]
160    fn exec_empty() -> (res: Self)
161        ensures
162            res.deep_view() =~= Map::empty(),
163    {
164        HashMap::new()
165    }
166}
167
168impl<'a, K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq, V: DeepView> ExecSpecMapIndex<
169    'a,
170> for &'a HashMap<K, V> {
171    type Key = K;
172
173    type Value = &'a V;
174
175    #[verifier::external_body]
176    #[inline(always)]
177    fn exec_index(self, index: Self::Key) -> (res: Self::Value)
178        ensures
179            res.deep_view() == self.deep_view()[index.deep_view()],
180    {
181        self.get(&index).unwrap()
182    }
183}
184
185impl<'a, K, V> ExecSpecMapInsert<'a, HashMap<K, V>> for &'a HashMap<K, V> where
186    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
187    V: DeepView + DeepViewClone,
188 {
189    type Key = K;
190
191    type Value = V;
192
193    #[verifier::external_body]
194    #[inline(always)]
195    fn exec_insert(self, key: Self::Key, value: Self::Value) -> (res: HashMap<K, V>)
196        ensures
197            res.deep_view() =~= self.deep_view().insert(key.deep_view(), value.deep_view()),
198    {
199        let mut m = self.deep_clone();
200        let _ = m.insert(key.deep_clone(), value.deep_clone());
201        m
202    }
203}
204
205impl<'a, K, V> ExecSpecMapRemove<'a, HashMap<K, V>> for &'a HashMap<K, V> where
206    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
207    V: DeepView + DeepViewClone,
208 {
209    type Key = K;
210
211    #[verifier::external_body]
212    #[inline(always)]
213    fn exec_remove(self, key: Self::Key) -> (res: HashMap<K, V>)
214        ensures
215            res.deep_view() =~= self.deep_view().remove(key.deep_view()),
216    {
217        let mut m = self.deep_clone();
218        let _ = m.remove(&key);
219        m
220    }
221}
222
223impl<'a, K, V> ExecSpecMapDom<'a> for &'a HashMap<K, V> where
224    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
225    V: DeepView + DeepViewClone,
226 {
227    type Key = K;
228
229    #[verifier::external_body]
230    #[inline(always)]
231    fn exec_dom(self) -> (res: HashSet<K>)
232        ensures
233            res.deep_view() =~= self.deep_view().dom(),
234    {
235        let mut m = HashSet::new();
236        for key in self.keys() {
237            m.insert(key.deep_clone());
238        }
239        m
240    }
241}
242
243impl<'a, K, V> ExecSpecMapGet<'a> for &'a HashMap<K, V> where
244    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
245    V: DeepView + DeepViewClone,
246 {
247    type Key = K;
248
249    type Value = V;
250
251    #[verifier::external_body]
252    #[inline(always)]
253    fn exec_get(self, k: Self::Key) -> (res: Option<Self::Value>)
254        ensures
255            match (res, self.deep_view().get(k.deep_view())) {
256                (Some(v1), Some(v2)) => v1.deep_view() == v2,
257                (None, None) => true,
258                (_, _) => false,
259            },
260    {
261        self.get(&k).map(|v| v.deep_clone())
262    }
263}
264
265} // verus!
vstd/contrib/exec_spec/map.rs

vstd/contrib/exec_spec/
map.rs
