vest_lib/
utils.rs

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

vest_lib/
utils.rs
