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

vstd/contrib/exec_spec/
mod.rs
