vest_lib 0.0.4

VestLib: A library of formally verified parser and serializer combinators
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

use super::bytes::{Fixed, Tail, Variable};
use super::uints::{U16Le, U32Le, U64Le, U8};
use vstd::prelude::*;

verus! {

macro_rules! impl_reflexive_clone {
    ($($ty:ty),*) => {
        ::vstd::prelude::verus! {
            $(
                impl Clone for $ty {
                    fn clone(&self) -> (out: Self)
                        ensures
                            out == *self,
                    {
                        Self
                    }
                }
            )*
        }
    };
}

impl_reflexive_clone!(U8, U16Le, U32Le, U64Le, Tail);

impl Clone for Variable {
    fn clone(&self) -> (out: Self)
        ensures
            out == *self,
    {
        Variable(self.0)
    }
}

impl<const N: usize> Clone for Fixed<N> {
    fn clone(&self) -> (out: Self)
        ensures
            out == *self,
    {
        Fixed
    }
}

} // verus!