vest/regular/
clone.rs

1use super::bytes::Bytes;
2use super::bytes_n::BytesN;
3use super::tag::Tag;
4use super::tail::Tail;
5use super::uints::{U16, U32, U64, U8};
6use vstd::prelude::*;
7
8verus! {
9
10macro_rules! impl_reflexive_clone {
11    ($($ty:ty),*) => {
12        ::builtin_macros::verus! {
13            $(
14                impl Clone for $ty {
15                    fn clone(&self) -> (out: Self)
16                        ensures
17                            out == *self,
18                    {
19                        Self
20                    }
21                }
22            )*
23        }
24    };
25}
26
27impl_reflexive_clone!(U8, U16, U32, U64, Tail);
28
29macro_rules! impl_clone_for_int_tags {
30    ($($combinator:ty),*) => {
31        ::builtin_macros::verus! {
32            $(
33                impl Clone for $combinator {
34                    fn clone(&self) -> (out: Self)
35                        ensures
36                            out == *self,
37                    {
38                        Tag::new(self.0.inner.clone(), self.0.predicate.0)
39                    }
40                }
41            )*
42        }
43    };
44}
45
46impl_clone_for_int_tags!(Tag<U8, u8>, Tag<U16, u16>, Tag<U32, u32>, Tag<U64, u64>);
47
48// impl<T: FromToBytes + Copy> Clone for Tag<Int<T>, T> {
49//     fn clone(&self) -> (out: Self)
50//         ensures
51//             out == *self,
52//     {
53//         Tag::new(self.0.inner.clone(), self.0.predicate.0)
54//     }
55// }
56//
57impl<'a> Clone for Tag<Bytes, &'a [u8]> {
58    fn clone(&self) -> (out: Self)
59        ensures
60            out == *self,
61    {
62        Tag::new(self.0.inner.clone(), self.0.predicate.0)
63    }
64}
65
66impl<'a, const N: usize> Clone for Tag<BytesN<N>, &'a [u8]> {
67    fn clone(&self) -> (out: Self)
68        ensures
69            out == *self,
70    {
71        Tag::new(self.0.inner.clone(), self.0.predicate.0)
72    }
73}
74
75impl Clone for Bytes {
76    fn clone(&self) -> (out: Self)
77        ensures
78            out == *self,
79    {
80        Bytes(self.0)
81    }
82}
83
84impl<const N: usize> Clone for BytesN<N> {
85    fn clone(&self) -> (out: Self)
86        ensures
87            out == *self,
88    {
89        BytesN
90    }
91}
92
93} // verus!
vest/regular/clone.rs

vest/regular/
clone.rs
