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

vstd/contrib/exec_spec/
map.rs
