vstd/contrib/exec_spec/
mod.rs

1//! This module provides runtime utilities for the compiled
2//! executable code of [`verus_builtin_macros::exec_spec_verified`]
3//! and [`verus_builtin_macros::exec_spec_unverified`].
4#![cfg(all(feature = "alloc", feature = "std"))]
5
6use crate::multiset::*;
7use crate::prelude::*;
8use std::collections::HashMap;
9use std::collections::HashSet;
10pub use verus_builtin_macros::exec_spec_unverified;
11pub use verus_builtin_macros::exec_spec_verified;
12
13mod map;
14pub use map::*;
15mod multiset;
16pub use multiset::*;
17mod option;
18pub use option::*;
19mod seq;
20pub use seq::*;
21mod set;
22pub use set::*;
23mod string;
24pub use string::*;
25
26verus! {
27
28/// [`ToRef`] and [`ToOwned`] are almost the same trait
29/// but separated to avoid type inference ambiguities.
30pub trait ToRef<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
31    fn get_ref(self) -> (res: T)
32        ensures
33            res.deep_view() == self.deep_view(),
34    ;
35}
36
37pub trait ToOwned<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
38    fn get_owned(self) -> (res: T)
39        ensures
40            res.deep_view() == self.deep_view(),
41    ;
42}
43
44/// Cloned objects have the same deep view
45pub trait DeepViewClone: Sized + DeepView {
46    fn deep_clone(&self) -> (res: Self)
47        ensures
48            res.deep_view() == self.deep_view(),
49    ;
50}
51
52/// Any spec types used in [`exec_spec_verified`] or [`exec_spec_unverified`] macros
53/// must implement this trait to indicate
54/// the corresponding exec type (owned and borrowed versions).
55pub trait ExecSpecType where
56    for <'a>&'a Self::ExecOwnedType: ToRef<Self::ExecRefType<'a>>,
57    for <'a>Self::ExecRefType<'a>: ToOwned<Self::ExecOwnedType>,
58 {
59    /// Owned version of the exec type.
60    type ExecOwnedType: DeepView<V = Self>;
61
62    /// Reference version of the exec type.
63    type ExecRefType<'a>: DeepView<V = Self>;
64}
65
66/// Spec for the executable version of equality.
67pub trait ExecSpecEq<'a>: DeepView + Sized {
68    type Other: DeepView<V = Self::V>;
69
70    fn exec_eq(this: Self, other: Self::Other) -> (res: bool)
71        ensures
72            res == (this.deep_view() =~~= other.deep_view()),
73    ;
74}
75
76/// Spec for executable version of [`Seq`] and [`str`] indexing.
77pub trait ExecSpecIndex<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
78    type Elem: DeepView;
79
80    fn exec_index(self, index: usize) -> Self::Elem
81        requires
82            0 <= index < self.deep_view().len(),
83    ;
84}
85
86/// Spec for executable version of `len`.
87pub trait ExecSpecLen {
88    fn exec_len(self) -> usize;
89}
90
91/// A macro to implement various traits for primitive arithmetic types.
92macro_rules! impl_primitives {
93    ($(,)?) => {};
94    ($t:ty $(,$rest:ty)* $(,)?) => {
95        verus! {
96            impl ExecSpecType for $t {
97                type ExecOwnedType = $t;
98                type ExecRefType<'a> = $t;
99            }
100
101            impl<'a> ToRef<$t> for &'a $t {
102                #[inline(always)]
103                fn get_ref(self) -> $t {
104                    *self
105                }
106            }
107
108            impl ToOwned<$t> for $t {
109                #[inline(always)]
110                fn get_owned(self) -> $t {
111                    self
112                }
113            }
114
115            impl DeepViewClone for $t {
116                #[inline(always)]
117                fn deep_clone(&self) -> Self {
118                    *self
119                }
120            }
121
122            impl<'a> ExecSpecEq<'a> for $t {
123                type Other = $t;
124
125                #[inline(always)]
126                fn exec_eq(this: Self, other: Self::Other) -> bool {
127                    this == other
128                }
129            }
130
131            // For cases like comparing Seq<u32> and Seq<u32>
132            impl<'a> ExecSpecEq<'a> for &'a $t {
133                type Other = &'a $t;
134
135                #[inline(always)]
136                fn exec_eq(this: Self, other: Self::Other) -> bool {
137                    this == other
138                }
139            }
140        }
141
142        impl_primitives!($($rest),*);
143    };
144}
145
146impl_primitives! {
147    u8, u16, u32, u64, u128, usize,
148    i8, i16, i32, i64, i128, isize,
149    bool, char,
150}
151// impl on tuples up to size 4, to match the impls of View in vstd
152
153
154macro_rules! impl_exec_spec_tuple {
155    ([$(
156        ($T:ident, $n:tt)
157    ),*])=> {
158        verus! {
159
160            impl<'a, $($T: Sized + DeepView),*> ToRef<&'a ($($T,)*)> for &'a ($($T,)*) {
161                #[inline(always)]
162                fn get_ref(self) -> &'a ($($T,)*) {
163                    self
164                }
165            }
166
167            impl<'a, $($T: DeepView + DeepViewClone),*> ToOwned<($($T,)*)> for &'a ($($T,)*) {
168                #[inline(always)]
169                fn get_owned(self) -> ($($T,)*) {
170                    self.deep_clone()
171                }
172            }
173
174            impl<$($T: DeepViewClone),*> DeepViewClone for ($($T,)*) {
175                #[inline(always)]
176                #[allow(non_snake_case)]
177                fn deep_clone(&self) -> Self {
178                    ($(self.$n.deep_clone(),)*)
179                }
180            }
181
182            impl<'a, $($T: DeepView),*> ExecSpecEq<'a> for &'a ($($T,)*)
183            where
184                $( &'a $T: ExecSpecEq<'a, Other = &'a $T>, )*
185            {
186                type Other = &'a ($($T,)*);
187
188                #[inline(always)]
189                #[allow(non_snake_case)]
190                fn exec_eq(this: Self, other: Self::Other) -> bool {
191                    $( <&$T>::exec_eq(&this.$n, &other.$n) )&&*
192                }
193            }
194
195        }
196    };
197}
198
199impl_exec_spec_tuple!([(T0, 0)]);
200
201impl_exec_spec_tuple!([(T0, 0), (T1, 1)]);
202
203impl_exec_spec_tuple!([(T0, 0), (T1, 1), (T2, 2)]);
204
205impl_exec_spec_tuple!([(T0, 0), (T1, 1), (T2, 2), (T3, 3)]);
206
207} // verus!
vstd/contrib/exec_spec/mod.rs

vstd/contrib/exec_spec/
mod.rs
