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// They compute with K's Hash/Eq, which agree with K::deep_view() by `K: ObeysDeepEq`.
11broadcast use {crate::group_vstd_default, crate::std_specs::hash::group_hash_axioms};
12
13/// Impls for shared traits
14impl<'a, K: ObeysDeepEq + 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: ObeysDeepEq + 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: ObeysDeepEq + 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
49/// `HashSet`'s `==` compares lengths and then membership,
50/// which is deep-view equality when `T` obeys deep equality.
51#[cfg(verus_keep_ghost)]
52impl<
53    T: ObeysDeepEq + std::hash::Hash + std::cmp::Eq,
54    S: std::hash::BuildHasher,
55    A: core::alloc::Allocator,
56> crate::std_specs::cmp::PartialEqSpecImpl for HashSet<T, S, A> {
57    open spec fn obeys_eq_spec() -> bool {
58        crate::std_specs::hash::builds_valid_hashers::<S>()
59    }
60
61    open spec fn eq_spec(&self, other: &Self) -> bool {
62        self.deep_view() == other.deep_view()
63    }
64}
65
66impl<K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq> ObeysDeepEq for HashSet<K> {
67    proof fn lemma_obeys_deep_eq() {
68        reveal(crate::laws_eq::obeys_deep_eq);
69    }
70}
71
72impl<
73    'a,
74    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
75> ExecSpecLen for &'a HashSet<K> {
76    #[inline(always)]
77    #[verifier::external_body]
78    fn exec_len(self) -> (res: usize)
79        ensures
80            res == self.deep_view().len(),
81    {
82        self.len()
83    }
84}
85
86/// Traits for Set methods
87/// Spec for executable version of [`Set::empty`].
88pub trait ExecSpecSetEmpty: Sized {
89    fn exec_empty() -> Self;
90}
91
92/// Spec for executable version of [`Set::contains`].
93pub trait ExecSpecSetContains<'a>: Sized + DeepView {
94    type Elem: DeepView;
95
96    fn exec_contains(self, a: Self::Elem) -> bool;
97}
98
99/// Spec for executable version of [`Set::insert`].
100pub trait ExecSpecSetInsert<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
101    type Elem: DeepView + DeepViewClone;
102
103    fn exec_insert(self, a: Self::Elem) -> Out;
104}
105
106/// Spec for executable version of [`Set::remove`].
107pub trait ExecSpecSetRemove<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
108    type Elem: DeepView + DeepViewClone;
109
110    fn exec_remove(self, a: Self::Elem) -> Out;
111}
112
113/// Spec for executable version of [`Set::intersect`].
114pub trait ExecSpecSetIntersect<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
115    fn exec_intersect(self, s2: Self) -> Out;
116}
117
118/// Spec for executable version of [`Set::union`].
119pub trait ExecSpecSetUnion<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
120    fn exec_union(self, s2: Self) -> Out;
121}
122
123/// Spec for executable version of [`Set::difference`].
124pub trait ExecSpecSetDifference<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
125    fn exec_difference(self, s2: Self) -> Out;
126}
127
128/// Impls for executable versions of Map methods
129impl<K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq> ExecSpecSetEmpty for HashSet<K> {
130    #[inline(always)]
131    fn exec_empty() -> (res: Self)
132        ensures
133            res.deep_view() =~= Set::empty(),
134    {
135        HashSet::new()
136    }
137}
138
139impl<'a, K: ObeysDeepEq + std::hash::Hash + std::cmp::Eq> ExecSpecSetContains<'a> for &'a HashSet<
140    K,
141> {
142    type Elem = K;
143
144    #[verifier::external_body]
145    #[inline(always)]
146    fn exec_contains(self, a: Self::Elem) -> (res: bool)
147        ensures
148            res == self.deep_view().contains(a.deep_view()),
149    {
150        self.contains(&a)
151    }
152}
153
154impl<'a, K> ExecSpecSetInsert<'a, HashSet<K>> for &'a HashSet<K> where
155    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
156 {
157    type Elem = K;
158
159    #[verifier::external_body]
160    #[inline(always)]
161    fn exec_insert(self, a: Self::Elem) -> (res: HashSet<K>)
162        ensures
163            res.deep_view() =~= self.deep_view().insert(a.deep_view()),
164    {
165        let mut m = self.deep_clone();
166        let _ = m.insert(a.deep_clone());
167        m
168    }
169}
170
171impl<'a, K> ExecSpecSetRemove<'a, HashSet<K>> for &'a HashSet<K> where
172    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
173 {
174    type Elem = K;
175
176    #[verifier::external_body]
177    #[inline(always)]
178    fn exec_remove(self, a: Self::Elem) -> (res: HashSet<K>)
179        ensures
180            res.deep_view() =~= self.deep_view().remove(a.deep_view()),
181    {
182        let mut m = self.deep_clone();
183        let _ = m.remove(&a);
184        m
185    }
186}
187
188impl<'a, K> ExecSpecSetIntersect<'a, HashSet<K>> for &'a HashSet<K> where
189    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
190 {
191    #[verifier::external_body]
192    #[inline(always)]
193    fn exec_intersect(self, s2: Self) -> (res: HashSet<K>)
194        ensures
195            res.deep_view() =~= self.deep_view().intersect(s2.deep_view()),
196    {
197        let mut intersect = HashSet::new();
198        for k in self.iter() {
199            if s2.contains(k) {
200                intersect.insert(k.deep_clone());
201            }
202        }
203        intersect
204    }
205}
206
207impl<'a, K> ExecSpecSetUnion<'a, HashSet<K>> for &'a HashSet<K> where
208    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
209 {
210    #[verifier::external_body]
211    #[inline(always)]
212    fn exec_union(self, s2: Self) -> (res: HashSet<K>)
213        ensures
214            res.deep_view() =~= self.deep_view().union(s2.deep_view()),
215    {
216        let mut un = self.deep_clone();
217        for k in s2.iter() {
218            un.insert(k.deep_clone());
219        }
220        un
221    }
222}
223
224impl<'a, K> ExecSpecSetDifference<'a, HashSet<K>> for &'a HashSet<K> where
225    K: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq,
226 {
227    #[verifier::external_body]
228    #[inline(always)]
229    fn exec_difference(self, s2: Self) -> (res: HashSet<K>)
230        ensures
231            res.deep_view() =~= self.deep_view().difference(s2.deep_view()),
232    {
233        let mut diff = HashSet::new();
234        for k in self.iter() {
235            if !s2.contains(k) {
236                diff.insert(k.deep_clone());
237            }
238        }
239        diff
240    }
241}
242
243} // verus!
vstd/contrib/exec_spec/set.rs

vstd/contrib/exec_spec/
set.rs
