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

vstd/contrib/exec_spec/
multiset.rs
