vstd/contrib/exec_spec/
set.rs

1//! This module contains [`Set`]-specific method implementations.
2use crate::contrib::exec_spec::*;
3use crate::prelude::*;
4use std::collections::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 HashSet<K>::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 {crate::group_vstd_default, crate::std_specs::hash::group_hash_axioms};
12
13/// Impls for shared traits
14impl<'a, K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ToRef<
15    &'a HashSet<K>,
16> for &'a HashSet<K> {
17    #[inline(always)]
18    fn get_ref(self) -> &'a HashSet<K> {
19        &self
20    }
21}
22
23impl<'a, K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ToOwned<
24    HashSet<K>,
25> for &'a HashSet<K> {
26    #[verifier::external_body]
27    #[inline(always)]
28    fn get_owned(self) -> HashSet<K> {
29        let mut new_set = HashSet::new();
30        for k in self.iter() {
31            new_set.insert(k.deep_clone());
32        }
33        new_set
34    }
35}
36
37impl<K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> DeepViewClone for HashSet<K> {
38    #[verifier::external_body]
39    #[inline(always)]
40    fn deep_clone(&self) -> Self {
41        let mut new_set = HashSet::new();
42        for k in self.iter() {
43            new_set.insert(k.deep_clone());
44        }
45        new_set
46    }
47}
48
49impl<'a, K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecEq<
50    'a,
51> for &'a HashSet<K> where &'a K: ExecSpecEq<'a, Other = &'a K> {
52    type Other = &'a HashSet<K>;
53
54    #[verifier::external_body]
55    #[inline(always)]
56    fn exec_eq(this: Self, other: Self::Other) -> bool {
57        if this.len() != other.len() {
58            return false;
59        }
60        for k in this.iter() {
61            if !other.contains(k) {
62                return false;
63            }
64        }
65        true
66    }
67}
68
69impl<'a, K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecLen for &'a HashSet<
70    K,
71> {
72    #[inline(always)]
73    #[verifier::external_body]
74    fn exec_len(self) -> (res: usize)
75        ensures
76            res == self.deep_view().len(),
77    {
78        self.len()
79    }
80}
81
82/// Traits for Set methods
83/// Spec for executable version of [`Set::empty`].
84pub trait ExecSpecSetEmpty: Sized {
85    fn exec_empty() -> Self;
86}
87
88/// Spec for executable version of [`Set::contains`].
89pub trait ExecSpecSetContains<'a>: Sized + DeepView {
90    type Elem: DeepView;
91
92    fn exec_contains(self, a: Self::Elem) -> bool;
93}
94
95/// Spec for executable version of [`Set::insert`].
96pub trait ExecSpecSetInsert<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
97    type Elem: DeepView + DeepViewClone;
98
99    fn exec_insert(self, a: Self::Elem) -> Out;
100}
101
102/// Spec for executable version of [`Set::remove`].
103pub trait ExecSpecSetRemove<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
104    type Elem: DeepView + DeepViewClone;
105
106    fn exec_remove(self, a: Self::Elem) -> Out;
107}
108
109/// Spec for executable version of [`Set::intersect`].
110pub trait ExecSpecSetIntersect<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
111    fn exec_intersect(self, s2: Self) -> Out;
112}
113
114/// Spec for executable version of [`Set::union`].
115pub trait ExecSpecSetUnion<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
116    fn exec_union(self, s2: Self) -> Out;
117}
118
119/// Spec for executable version of [`Set::difference`].
120pub trait ExecSpecSetDifference<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
121    fn exec_difference(self, s2: Self) -> Out;
122}
123
124/// Impls for executable versions of Map methods
125impl<K: DeepView + std::hash::Hash + std::cmp::Eq> ExecSpecSetEmpty for HashSet<K> {
126    #[inline(always)]
127    fn exec_empty() -> (res: Self)
128        ensures
129            res.deep_view() =~= Set::empty(),
130    {
131        HashSet::new()
132    }
133}
134
135impl<'a, K: DeepView + std::hash::Hash + std::cmp::Eq> ExecSpecSetContains<'a> for &'a HashSet<K> {
136    type Elem = K;
137
138    #[verifier::external_body]
139    #[inline(always)]
140    fn exec_contains(self, a: Self::Elem) -> (res: bool)
141        ensures
142            res == self.deep_view().contains(a.deep_view()),
143    {
144        self.contains(&a)
145    }
146}
147
148impl<'a, K> ExecSpecSetInsert<'a, HashSet<K>> for &'a HashSet<K> where
149    K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq,
150 {
151    type Elem = K;
152
153    #[verifier::external_body]
154    #[inline(always)]
155    fn exec_insert(self, a: Self::Elem) -> (res: HashSet<K>)
156        ensures
157            res.deep_view() =~= self.deep_view().insert(a.deep_view()),
158    {
159        let mut m = self.deep_clone();
160        let _ = m.insert(a.deep_clone());
161        m
162    }
163}
164
165impl<'a, K> ExecSpecSetRemove<'a, HashSet<K>> for &'a HashSet<K> where
166    K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq,
167 {
168    type Elem = K;
169
170    #[verifier::external_body]
171    #[inline(always)]
172    fn exec_remove(self, a: Self::Elem) -> (res: HashSet<K>)
173        ensures
174            res.deep_view() =~= self.deep_view().remove(a.deep_view()),
175    {
176        let mut m = self.deep_clone();
177        let _ = m.remove(&a);
178        m
179    }
180}
181
182impl<'a, K> ExecSpecSetIntersect<'a, HashSet<K>> for &'a HashSet<K> where
183    K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq,
184 {
185    #[verifier::external_body]
186    #[inline(always)]
187    fn exec_intersect(self, s2: Self) -> (res: HashSet<K>)
188        ensures
189            res.deep_view() =~= self.deep_view().intersect(s2.deep_view()),
190    {
191        let mut intersect = HashSet::new();
192        for k in self.iter() {
193            if s2.contains(k) {
194                intersect.insert(k.deep_clone());
195            }
196        }
197        intersect
198    }
199}
200
201impl<'a, K> ExecSpecSetUnion<'a, HashSet<K>> for &'a HashSet<K> where
202    K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq,
203 {
204    #[verifier::external_body]
205    #[inline(always)]
206    fn exec_union(self, s2: Self) -> (res: HashSet<K>)
207        ensures
208            res.deep_view() =~= self.deep_view().union(s2.deep_view()),
209    {
210        let mut un = self.deep_clone();
211        for k in s2.iter() {
212            un.insert(k.deep_clone());
213        }
214        un
215    }
216}
217
218impl<'a, K> ExecSpecSetDifference<'a, HashSet<K>> for &'a HashSet<K> where
219    K: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq,
220 {
221    #[verifier::external_body]
222    #[inline(always)]
223    fn exec_difference(self, s2: Self) -> (res: HashSet<K>)
224        ensures
225            res.deep_view() =~= self.deep_view().difference(s2.deep_view()),
226    {
227        let mut diff = HashSet::new();
228        for k in self.iter() {
229            if !s2.contains(k) {
230                diff.insert(k.deep_clone());
231            }
232        }
233        diff
234    }
235}
236
237} // verus!
vstd/contrib/exec_spec/set.rs

vstd/contrib/exec_spec/
set.rs
