vstd/contrib/exec_spec/
multiset.rs

1//! This module contains [`Multiset`]-specific method implementations.
2use crate::contrib::exec_spec::*;
3use crate::prelude::*;
4use std::collections::HashMap;
5
6verus! {
7
8// Note: all of the exec translations are currently unverified.
9// Some will require axiomatization because their corresponding specs are uninterp.
10// They compute with T's Hash/Eq, which agree with T::deep_view() by `T: ObeysDeepEq`.
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/// `Multiset<T>` is compiled to `ExecMultiset<T>`.
18#[derive(Eq, Debug)]
19pub struct ExecMultiset<T: std::hash::Hash + std::cmp::Eq> {
20    pub m: HashMap<T, usize>,
21}
22
23/// Compares multiplicities, where an absent element has multiplicity 0 (as in the deep view).
24impl<T: std::hash::Hash + std::cmp::Eq> PartialEq for ExecMultiset<T> {
25    #[verifier::external_body]
26    fn eq(&self, other: &Self) -> bool {
27        let count = |m: &HashMap<T, usize>, k: &T| m.get(k).copied().unwrap_or(0);
28        self.m.iter().all(|(k, v)| count(&other.m, k) == *v) && other.m.iter().all(
29            |(k, v)| count(&self.m, k) == *v,
30        )
31    }
32}
33
34#[cfg(verus_keep_ghost)]
35impl<
36    T: ObeysDeepEq + std::hash::Hash + std::cmp::Eq,
37> crate::std_specs::cmp::PartialEqSpecImpl for ExecMultiset<T> {
38    open spec fn obeys_eq_spec() -> bool {
39        true
40    }
41
42    open spec fn eq_spec(&self, other: &Self) -> bool {
43        self.deep_view() == other.deep_view()
44    }
45}
46
47impl<T: ObeysDeepEq + std::hash::Hash + std::cmp::Eq> ObeysDeepEq for ExecMultiset<T> {
48    proof fn lemma_obeys_deep_eq() {
49        reveal(crate::laws_eq::obeys_deep_eq);
50    }
51}
52
53/// Implementations for shared traits
54/*
55trouble implementing this - complains about lifetime of T
56impl<T: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecType for Multiset<T> {
57    type ExecOwnedType = ExecMultiset<T>;
58
59    type ExecRefType<'a> = &'a ExecMultiset<T>;
60}*/
61impl<T: DeepView + std::hash::Hash + std::cmp::Eq> DeepView for ExecMultiset<T> {
62    type V = Multiset<<T as DeepView>::V>;
63
64    open spec fn deep_view(&self) -> Self::V {
65        Multiset::from_map(self.m.deep_view().map_values(|v| v as nat))
66    }
67}
68
69impl<'a, T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq> ToRef<
70    &'a ExecMultiset<T>,
71> for &'a ExecMultiset<T> {
72    #[inline(always)]
73    fn get_ref(self) -> &'a ExecMultiset<T> {
74        &self
75    }
76}
77
78impl<'a, T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq> ToOwned<
79    ExecMultiset<T>,
80> for &'a ExecMultiset<T> {
81    #[verifier::external_body]
82    #[inline(always)]
83    fn get_owned(self) -> ExecMultiset<T> {
84        let mut new_map = HashMap::new();
85        for (k, v) in self.m.iter() {
86            new_map.insert(k.deep_clone(), v.deep_clone());
87        }
88        ExecMultiset { m: new_map }
89    }
90}
91
92impl<
93    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
94> DeepViewClone for ExecMultiset<T> {
95    #[verifier::external_body]
96    #[inline(always)]
97    fn deep_clone(&self) -> Self {
98        let mut new_map = HashMap::new();
99        for (k, v) in self.m.iter() {
100            new_map.insert(k.deep_clone(), v.deep_clone());
101        }
102        ExecMultiset { m: new_map }
103    }
104}
105
106impl<
107    'a,
108    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
109> ExecSpecLen for &'a ExecMultiset<T> {
110    #[inline(always)]
111    #[verifier::external_body]
112    fn exec_len(self) -> (res: usize)
113        ensures
114            res == self.deep_view().len(),
115    {
116        let mut len = 0;
117        for (_, v) in self.m.iter() {
118            len = len + v;
119        }
120        len
121    }
122}
123
124//
125// Trait definitions for methods
126//
127/// Spec for executable version of [`Multiset::count`].
128pub trait ExecSpecMultisetCount: Sized + DeepView {
129    type Elem;
130
131    fn exec_count(self, value: Self::Elem) -> usize;
132}
133
134/// Spec for executable version of [`Multiset::empty`].
135pub trait ExecSpecMultisetEmpty: Sized {
136    fn exec_empty() -> Self;
137}
138
139/// Spec for executable version of [`Multiset::singleton`].
140pub trait ExecSpecMultisetSingleton: Sized {
141    type Elem;
142
143    fn exec_singleton(v: Self::Elem) -> Self;
144}
145
146/// Spec for executable version of [`Multiset::add`].
147pub trait ExecSpecMultisetAdd<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
148    fn exec_add(self, m2: Self) -> Out;
149}
150
151/// Spec for executable version of [`Multiset::sub`].
152pub trait ExecSpecMultisetSub<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
153    fn exec_sub(self, m2: Self) -> Out;
154}
155
156//
157// Implementations for ExecMultiset
158//
159impl<
160    'a,
161    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
162> ExecSpecMultisetCount for &'a ExecMultiset<T> {
163    type Elem = T;
164
165    #[inline(always)]
166    #[verifier::external_body]
167    fn exec_count(self, value: Self::Elem) -> (res: usize)
168        ensures
169            res == self.deep_view().count(value.deep_view()),
170    {
171        match self.m.get(&value) {
172            Some(v) => v.deep_clone(),
173            None => 0,
174        }
175    }
176}
177
178impl<T: ObeysDeepEq + std::hash::Hash + std::cmp::Eq> ExecSpecMultisetEmpty for ExecMultiset<T> {
179    #[verifier::external_body]
180    #[inline(always)]
181    fn exec_empty() -> (res: Self)
182        ensures
183            res.deep_view() =~= Multiset::empty(),
184    {
185        ExecMultiset { m: HashMap::new() }
186    }
187}
188
189impl<
190    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
191> ExecSpecMultisetSingleton for ExecMultiset<T> {
192    type Elem = T;
193
194    #[verifier::external_body]
195    #[inline(always)]
196    fn exec_singleton(v: Self::Elem) -> (res: Self)
197        ensures
198            res.deep_view() =~= Multiset::singleton(v.deep_view()),
199    {
200        let mut m = HashMap::new();
201        m.insert(v.deep_clone(), 1);
202        ExecMultiset { m }
203    }
204}
205
206impl<'a, T> ExecSpecMultisetAdd<'a, ExecMultiset<T>> for &'a ExecMultiset<T> where
207    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
208 {
209    #[verifier::external_body]
210    #[inline(always)]
211    fn exec_add(self, m2: Self) -> (res: ExecMultiset<T>)
212        ensures
213            res.deep_view() =~= self.deep_view().add(m2.deep_view()),
214    {
215        let mut add = self.deep_clone();
216        for (k, v) in m2.m.iter() {
217            if !add.m.contains_key(k) {
218                add.m.insert(k.deep_clone(), v.deep_clone());
219            } else {
220                let new_count = add.m.get(k).unwrap() + v;
221                add.m.insert(k.deep_clone(), new_count);
222            }
223        }
224        add
225    }
226}
227
228impl<'a, T> ExecSpecMultisetSub<'a, ExecMultiset<T>> for &'a ExecMultiset<T> where
229    T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
230 {
231    #[verifier::external_body]
232    #[inline(always)]
233    fn exec_sub(self, m2: Self) -> (res: ExecMultiset<T>)
234        ensures
235            res.deep_view() =~= self.deep_view().sub(m2.deep_view()),
236    {
237        let mut sub = HashMap::new();
238        for (k, v) in self.m.iter() {
239            if m2.m.contains_key(k) {
240                let v2 = m2.m.get(k).unwrap();
241                if v2 < v {
242                    sub.insert(k.deep_clone(), v.deep_clone() - v2);
243                }
244            } else {
245                sub.insert(k.deep_clone(), v.deep_clone());
246            }
247        }
248        ExecMultiset { m: sub }
249    }
250}
251
252} // verus!
vstd/contrib/exec_spec/multiset.rs

vstd/contrib/exec_spec/
multiset.rs
