vest/
utils.rs

1extern crate alloc;
2// use std::convert::Infallible;
3
4use vstd::prelude::*;
5use vstd::slice::slice_index_get;
6
7use crate::regular::uints::FromToBytes;
8
9verus! {
10
11/// Spec version of [`From`].
12pub trait SpecFrom<T>: Sized {
13    /// Spec version of [`From::ex_from`]
14    spec fn spec_from(t: T) -> Self;
15}
16
17/// Spec version of [`Into`].
18pub trait SpecInto<T>: Sized {
19    /// Spec version of [`Into::ex_into`]
20    spec fn spec_into(self) -> T;
21}
22
23impl<T, U> SpecInto<U> for T where U: SpecFrom<T> {
24    open spec fn spec_into(self) -> U {
25        U::spec_from(self)
26    }
27}
28
29impl<T> SpecFrom<T> for T {
30    open spec fn spec_from(t: T) -> T {
31        t
32    }
33}
34
35/// Vest equivalent of [`std::convert::From`].
36pub trait From<T> where T: View, Self: View + Sized, Self::V: SpecFrom<T::V> {
37    /// Vest equivalent of [`std::convert::From::from`].
38    fn ex_from(t: T) -> (res: Self)
39        ensures
40            res@ == Self::V::spec_from(t@),
41    ;
42}
43
44/// Vest equivalent of [`std::convert::Into`].
45pub trait Into<T> where T: View, Self: View + Sized, Self::V: SpecInto<T::V> {
46    /// Vest equivalent of [`std::convert::Into::into`].
47    fn ex_into(self) -> (res: T)
48        ensures
49            res@ == self@.spec_into(),
50    ;
51}
52
53impl<T, U> Into<U> for T where T: View, U: View, U: From<T>, U::V: SpecFrom<T::V> {
54    fn ex_into(self) -> U {
55        U::ex_from(self)
56    }
57}
58
59impl<T> From<T> for T where T: View, T::V: SpecFrom<T::V> {
60    fn ex_from(t: T) -> (res: T) {
61        t
62    }
63}
64
65impl<const N: usize, 'a, 'b> From<&'a [u8; N]> for &'b [u8] where 'a: 'b {
66    fn ex_from(v: &'a [u8; N]) -> &'b [u8] {
67        v.as_slice()
68    }
69}
70
71/// Spec version of [`TryFrom`].
72pub trait SpecTryFrom<T>: Sized {
73    /// The type returned in the event of a conversion error.
74    type Error;
75
76    /// Performs the conversion.
77    spec fn spec_try_from(value: T) -> Result<Self, Self::Error>;
78}
79
80/// Spec version of [`TryInto`].
81pub trait SpecTryInto<T>: Sized {
82    /// The type returned in the event of a conversion error.
83    type Error;
84
85    /// Performs the conversion.
86    spec fn spec_try_into(self) -> Result<T, Self::Error>;
87}
88
89impl<T, U> SpecTryInto<U> for T where U: SpecTryFrom<T> {
90    type Error = U::Error;
91
92    open spec fn spec_try_into(self) -> Result<U, U::Error> {
93        U::spec_try_from(self)
94    }
95}
96
97// impl<T, U> SpecTryFrom<U> for T where U: SpecInto<T> {
98//     type Error = Infallible;
99//
100//     open spec fn spec_try_from(value: U) -> Result<Self, Self::Error> {
101//         Ok(U::spec_into(value))
102//     }
103// }
104/// Vest equivalent of [`std::convert::TryFrom`].
105pub trait TryFrom<T> where T: View, Self: View + Sized, Self::V: SpecTryFrom<T::V> {
106    /// The type returned in the event of a conversion error.
107    type Error;
108
109    /// Vest equivalent of [`std::convert::TryFrom::try_from`].
110    fn ex_try_from(t: T) -> (res: Result<Self, Self::Error>)
111        ensures
112            res matches Ok(v) ==> {
113                &&& Self::V::spec_try_from(t@) is Ok
114                &&& Self::V::spec_try_from(t@) matches Ok(v_) && v@ == v_
115            },
116            res matches Err(e) ==> Self::V::spec_try_from(t@) is Err,
117    ;
118}
119
120/// Vest equivalent of [`std::convert::TryInto`].
121pub trait TryInto<T> where T: View, Self: View + Sized, Self::V: SpecTryInto<T::V> {
122    /// The type returned in the event of a conversion error.
123    type Error;
124
125    /// Vest equivalent of [`std::convert::TryInto::try_into`].
126    fn ex_try_into(self) -> (res: Result<T, Self::Error>)
127        ensures
128            res matches Ok(v) ==> {
129                &&& self@.spec_try_into() is Ok
130                &&& self@.spec_try_into() matches Ok(v_) && v@ == v_
131            },
132            res matches Err(e) ==> self@.spec_try_into() is Err,
133    ;
134}
135
136impl<T, U> TryInto<U> for T where T: View, U: View, U: TryFrom<T>, U::V: SpecTryFrom<T::V> {
137    type Error = U::Error;
138
139    fn ex_try_into(self) -> Result<U, U::Error> {
140        U::ex_try_from(self)
141    }
142}
143
144// impl<T, U> TryFrom<U> for T where T: View, U: View, U: Into<T>, U::V: SpecInto<T::V> {
145//     type Error = Infallible;
146//
147//     fn ex_try_from(value: U) -> Result<T, Infallible> {
148//         Ok(U::ex_into(value))
149//     }
150// }
151/// A helper trait for two different types that can be compared.
152pub trait Compare<Other> where Self: View, Other: View<V = Self::V> {
153    /// Compare a value of `Self` with a value of `Other`.
154    fn compare(&self, other: &Other) -> (o: bool)
155        ensures
156            o == (self@ == other@),
157    ;
158}
159
160impl<Int: FromToBytes> Compare<Int> for Int {
161    fn compare(&self, other: &Int) -> bool {
162        self.eq(other)
163    }
164}
165
166impl<'a, 'b> Compare<&'b [u8]> for &'a [u8] {
167    fn compare(&self, other: &&'b [u8]) -> bool {
168        compare_slice(self, *other)
169    }
170}
171
172/// Helper function to splice a sequence of bytes into another sequence of bytes.
173pub open spec fn seq_splice(data: Seq<u8>, pos: usize, v: Seq<u8>) -> Seq<u8>
174    recommends
175        pos + v.len() <= data.len(),
176{
177    data.subrange(0, pos as int).add(v).add(data.subrange(pos + v.len() as int, data.len() as int))
178}
179
180/// Helper function to set a range of bytes in a vector.
181pub fn set_range<'a>(data: &mut Vec<u8>, i: usize, input: &[u8])
182    requires
183        0 <= i + input@.len() <= old(data)@.len() <= usize::MAX,
184    ensures
185        data@.len() == old(data)@.len() && data@ == old(data)@.subrange(0, i as int).add(
186            input@,
187        ).add(old(data)@.subrange(i + input@.len(), data@.len() as int)),
188{
189    let mut j = 0;
190    while j < input.len()
191        invariant
192            data@.len() == old(data)@.len(),
193            forall|k| 0 <= k < i ==> data@[k] == old(data)@[k],
194            forall|k| i + input@.len() <= k < data@.len() ==> data@[k] == old(data)@[k],
195            0 <= i <= i + j <= i + input@.len() <= data@.len() <= usize::MAX,
196            forall|k| 0 <= k < j ==> data@[i + k] == input@[k],
197        decreases input.len() - j
198    {
199        data.set(i + j, *slice_index_get(input, j));
200        j = j + 1
201    }
202    assert(data@ =~= old(data)@.subrange(0, i as int).add(input@).add(
203        old(data)@.subrange(i + input@.len(), data@.len() as int),
204    ))
205}
206
207/// Helper function to compare two slices.
208pub fn compare_slice<'a, 'b>(x: &'a [u8], y: &'a [u8]) -> (res: bool)
209    ensures
210        res == (x@ == y@),
211{
212    if x.len() != y.len() {
213        assert(x@.len() != y@.len());
214        return false;
215    }
216    for i in 0..x.len()
217        invariant
218            0 <= i <= x.len(),
219            x.len() == y.len(),
220            forall|j: int| 0 <= j < i ==> x@[j] == y@[j],
221    {
222        if slice_index_get(x, i) != slice_index_get(y, i) {
223            assert(x@[i as int] != y@[i as int]);
224            return false;
225        }
226    }
227    proof {
228        assert(x@ =~= y@);
229    }
230    true
231}
232
233/// Helper trait for types that have a reflexive view.
234pub trait ViewReflex where Self: std::marker::Sized + View<V = Self> {
235    /// Reflexivity proof for the view.
236    proof fn reflex(&self)
237        ensures
238            self@ == self,
239    ;
240}
241
242/// Helper function to initialize a vector of `u8` with zeros.
243pub exec fn init_vec_u8(n: usize) -> (res: Vec<u8>)
244    ensures
245        res@.len() == n,
246{
247    let mut i: usize = 0;
248    let mut ret: Vec<u8> = Vec::new();
249    while i < n
250        invariant
251            0 <= i <= n,
252            ret@.len() == i,
253        decreases n - i
254    {
255        ret.push(0);
256        assert(ret@[i as int] == 0);
257        i = i + 1
258    }
259    ret
260}
261
262} // verus!
263macro_rules! declare_identity_view_reflex {
264    ($t:ty) => {
265        ::builtin_macros::verus! {
266            impl ViewReflex for $t {
267                proof fn reflex(&self) {}
268            }
269        }
270    };
271}
272
273declare_identity_view_reflex!(());
274
275declare_identity_view_reflex!(bool);
276
277declare_identity_view_reflex!(u8);
278
279declare_identity_view_reflex!(u16);
280
281declare_identity_view_reflex!(u32);
282
283declare_identity_view_reflex!(u64);
284
285declare_identity_view_reflex!(u128);
286
287declare_identity_view_reflex!(usize);
288
289declare_identity_view_reflex!(i8);
290
291declare_identity_view_reflex!(i16);
292
293declare_identity_view_reflex!(i32);
294
295declare_identity_view_reflex!(i64);
296
297declare_identity_view_reflex!(i128);
298
299declare_identity_view_reflex!(isize);
vest/utils.rs

vest/
utils.rs
