vstd/contrib/
exec_spec.rs

1//! This module provides runtime utilities for the compiled
2//! executable code of [`builtin_macros::exec_spec`].
3#![cfg(all(feature = "alloc", feature = "std"))]
4
5use crate::prelude::*;
6pub use verus_builtin_macros::exec_spec;
7
8verus! {
9
10/// [`ToRef`] and [`ToOwned`] are almost the same trait
11/// but separated to avoid type inference ambiguities.
12pub trait ToRef<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
13    fn get_ref(self) -> (res: T)
14        ensures
15            res.deep_view() == self.deep_view(),
16    ;
17}
18
19pub trait ToOwned<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
20    fn get_owned(self) -> (res: T)
21        ensures
22            res.deep_view() == self.deep_view(),
23    ;
24}
25
26/// Cloned objects have the same deep view
27pub trait DeepViewClone: Sized + DeepView {
28    fn deep_clone(&self) -> (res: Self)
29        ensures
30            res.deep_view() == self.deep_view(),
31    ;
32}
33
34/// Any spec types used in [`exec_spec`] macro
35/// must implement this trait to indicate
36/// the corresponding exec type (owned and borrowed versions).
37pub trait ExecSpecType where
38    for <'a>&'a Self::ExecOwnedType: ToRef<Self::ExecRefType<'a>>,
39    for <'a>Self::ExecRefType<'a>: ToOwned<Self::ExecOwnedType>,
40 {
41    /// Owned version of the exec type.
42    type ExecOwnedType: DeepView<V = Self>;
43
44    /// Reference version of the exec type.
45    type ExecRefType<'a>: DeepView<V = Self>;
46}
47
48/// Spec for the executable version of equality.
49pub trait ExecSpecEq<'a>: DeepView + Sized {
50    type Other: DeepView<V = Self::V>;
51
52    fn exec_eq(this: Self, other: Self::Other) -> (res: bool)
53        ensures
54            res == (this.deep_view() =~~= other.deep_view()),
55    ;
56}
57
58/// Spec for executable version of [`Seq::len`].
59pub trait ExecSpecLen {
60    fn exec_len(&self) -> usize;
61}
62
63/// Spec for executable version of [`Seq`] indexing.
64pub trait ExecSpecIndex<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
65    type Elem: DeepView;
66
67    fn exec_index(self, index: usize) -> Self::Elem
68        requires
69            0 <= index < self.deep_view().len(),
70    ;
71}
72
73/// A macro to implement various traits for primitive arithmetic types.
74macro_rules! impl_primitives {
75    ($(,)?) => {};
76    ($t:ty $(,$rest:ty)* $(,)?) => {
77        verus! {
78            impl ExecSpecType for $t {
79                type ExecOwnedType = $t;
80                type ExecRefType<'a> = $t;
81            }
82
83            impl<'a> ToRef<$t> for &'a $t {
84                #[inline(always)]
85                fn get_ref(self) -> $t {
86                    *self
87                }
88            }
89
90            impl ToOwned<$t> for $t {
91                #[inline(always)]
92                fn get_owned(self) -> $t {
93                    self
94                }
95            }
96
97            impl DeepViewClone for $t {
98                #[inline(always)]
99                fn deep_clone(&self) -> Self {
100                    *self
101                }
102            }
103
104            impl<'a> ExecSpecEq<'a> for $t {
105                type Other = $t;
106
107                #[inline(always)]
108                fn exec_eq(this: Self, other: Self::Other) -> bool {
109                    this == other
110                }
111            }
112
113            // For cases like comparing Seq<u32> and Seq<u32>
114            impl<'a> ExecSpecEq<'a> for &'a $t {
115                type Other = &'a $t;
116
117                #[inline(always)]
118                fn exec_eq(this: Self, other: Self::Other) -> bool {
119                    this == other
120                }
121            }
122        }
123
124        impl_primitives!($($rest),*);
125    };
126}
127
128impl_primitives! {
129    u8, u16, u32, u64, u128, usize,
130    i8, i16, i32, i64, i128, isize,
131    bool, char,
132}
133
134impl<'a, T: Sized + DeepView> ToRef<&'a Option<T>> for &'a Option<T> {
135    #[inline(always)]
136    fn get_ref(self) -> &'a Option<T> {
137        self
138    }
139}
140
141impl<'a, T: DeepView + DeepViewClone> ToOwned<Option<T>> for &'a Option<T> {
142    #[inline(always)]
143    fn get_owned(self) -> Option<T> {
144        self.deep_clone()
145    }
146}
147
148impl<T: DeepViewClone> DeepViewClone for Option<T> {
149    #[inline(always)]
150    fn deep_clone(&self) -> Self {
151        match self {
152            Some(t) => Some(t.deep_clone()),
153            None => None,
154        }
155    }
156}
157
158impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Option<T> where &'a T: ExecSpecEq<'a, Other = &'a T> {
159    type Other = &'a Option<T>;
160
161    #[inline(always)]
162    fn exec_eq(this: Self, other: Self::Other) -> bool {
163        match (this, other) {
164            (Some(t1), Some(t2)) => <&'a T>::exec_eq(t1, t2),
165            (None, None) => true,
166            _ => false,
167        }
168    }
169}
170
171/// TODO: generalize to more tuple types
172impl<'a, T1: Sized + DeepView, T2: Sized + DeepView> ToRef<&'a (T1, T2)> for &'a (T1, T2) {
173    #[inline(always)]
174    fn get_ref(self) -> &'a (T1, T2) {
175        self
176    }
177}
178
179impl<'a, T1: DeepView + DeepViewClone, T2: DeepView + DeepViewClone> ToOwned<(T1, T2)> for &'a (
180    T1,
181    T2,
182) {
183    #[inline(always)]
184    fn get_owned(self) -> (T1, T2) {
185        self.deep_clone()
186    }
187}
188
189impl<T1: DeepViewClone, T2: DeepViewClone> DeepViewClone for (T1, T2) {
190    #[inline(always)]
191    fn deep_clone(&self) -> Self {
192        (self.0.deep_clone(), self.1.deep_clone())
193    }
194}
195
196impl<'a, T1: DeepView, T2: DeepView> ExecSpecEq<'a> for &'a (T1, T2) where
197    &'a T1: ExecSpecEq<'a, Other = &'a T1>,
198    &'a T2: ExecSpecEq<'a, Other = &'a T2>,
199 {
200    type Other = &'a (T1, T2);
201
202    #[inline(always)]
203    fn exec_eq(this: Self, other: Self::Other) -> bool {
204        <&T1>::exec_eq(&this.0, &other.0) && <&T2>::exec_eq(&this.1, &other.1)
205    }
206}
207
208/// We use this special alias to tell the `exec_spec` macro to
209/// compile [`Seq<char>`] to [`String`] instead of [`Vec<char>`].
210pub type SpecString = Seq<char>;
211
212impl ExecSpecType for SpecString {
213    type ExecOwnedType = String;
214
215    type ExecRefType<'a> = &'a str;
216}
217
218impl<'a> ToRef<&'a str> for &'a String {
219    #[inline(always)]
220    fn get_ref(self) -> &'a str {
221        self.as_str()
222    }
223}
224
225impl<'a> ToOwned<String> for &'a str {
226    #[verifier::external_body]
227    #[inline(always)]
228    fn get_owned(self) -> String {
229        self.to_string()
230    }
231}
232
233impl DeepViewClone for String {
234    #[inline(always)]
235    fn deep_clone(&self) -> Self {
236        self.clone()
237    }
238}
239
240impl<'a> ExecSpecEq<'a> for &'a str {
241    type Other = &'a str;
242
243    #[verifier::external_body]
244    #[inline(always)]
245    fn exec_eq(this: Self, other: Self::Other) -> bool {
246        this == other
247    }
248}
249
250/// Required for comparing, e.g., [`Vec<String>`]s.
251impl<'a> ExecSpecEq<'a> for &'a String {
252    type Other = &'a String;
253
254    #[verifier::external_body]
255    #[inline(always)]
256    fn exec_eq(this: Self, other: Self::Other) -> bool {
257        this == other
258    }
259}
260
261impl<'a> ExecSpecLen for &'a str {
262    #[inline(always)]
263    fn exec_len(&self) -> (res: usize)
264        ensures
265            res == self.deep_view().len(),
266    {
267        self.unicode_len()
268    }
269}
270
271impl<'a> ExecSpecIndex<'a> for &'a str {
272    type Elem = char;
273
274    #[inline(always)]
275    fn exec_index(self, index: usize) -> (res: Self::Elem)
276        ensures
277            res == self.deep_view()[index as int],
278    {
279        self.get_char(index)
280    }
281}
282
283/// NOTE: can't implement [`ExecSpecType`] for [`Seq<T>`]
284/// since it conflicts with [`SpecString`] (i.e., [`Seq<char>`]).
285impl<'a, T: DeepView> ToRef<&'a [T]> for &'a Vec<T> {
286    #[inline(always)]
287    fn get_ref(self) -> &'a [T] {
288        self.as_slice()
289    }
290}
291
292impl<'a, T: DeepView + DeepViewClone> ToOwned<Vec<T>> for &'a [T] {
293    /// TODO: verify this
294    #[verifier::external_body]
295    #[inline(always)]
296    fn get_owned(self) -> Vec<T> {
297        self.iter().map(|x| x.deep_clone()).collect()
298    }
299}
300
301impl<T: DeepViewClone> DeepViewClone for Vec<T> {
302    /// TODO: verify this
303    #[verifier::external_body]
304    #[inline(always)]
305    fn deep_clone(&self) -> Self {
306        self.iter().map(|x| x.deep_clone()).collect()
307    }
308}
309
310impl<'a, T: DeepView> ExecSpecEq<'a> for &'a [T] where &'a T: ExecSpecEq<'a, Other = &'a T> {
311    type Other = &'a [T];
312
313    #[verifier::external_body]
314    #[inline(always)]
315    fn exec_eq(this: Self, other: Self::Other) -> bool {
316        this.len() == other.len() && this.iter().zip(other.iter()).all(
317            |(a, b)| <&'a T>::exec_eq(a, b),
318        )
319    }
320}
321
322impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Vec<T> where &'a T: ExecSpecEq<'a, Other = &'a T> {
323    type Other = &'a Vec<T>;
324
325    #[verifier::external_body]
326    #[inline(always)]
327    fn exec_eq(this: Self, other: Self::Other) -> bool {
328        this.len() == other.len() && this.iter().zip(other.iter()).all(
329            |(a, b)| <&'a T>::exec_eq(a, b),
330        )
331    }
332}
333
334impl<'a, T: DeepView> ExecSpecLen for &'a [T] {
335    #[verifier::external_body]
336    #[inline(always)]
337    fn exec_len(&self) -> (res: usize)
338        ensures
339            res == self.deep_view().len(),
340    {
341        self.len()
342    }
343}
344
345impl<'a, T: DeepView> ExecSpecIndex<'a> for &'a [T] {
346    type Elem = &'a T;
347
348    #[verifier::external_body]
349    #[inline(always)]
350    fn exec_index(self, index: usize) -> (res: Self::Elem)
351        ensures
352            res.deep_view() == self.deep_view()[index as int],
353    {
354        self.get(index).unwrap()
355    }
356}
357
358} // verus!
vstd/contrib/exec_spec.rs

vstd/contrib/
exec_spec.rs
