verdict_parser/common/
clone.rs

1use super::*;
2/// Define and implement a temporary Clone replacement "PolyfillClone" for some types
3use vstd::prelude::*;
4
5verus! {
6
7/// A temporary replacement Clone
8pub trait PolyfillClone: View + Sized {
9    fn clone(&self) -> (res: Self)
10        ensures
11            res@ == self@;
12}
13
14impl PolyfillClone for bool {
15    #[inline(always)]
16    fn clone(&self) -> Self {
17        *self
18    }
19}
20
21impl<'a> PolyfillClone for &'a str {
22    #[inline(always)]
23    fn clone(&self) -> Self {
24        *self
25    }
26}
27
28impl<'a, T> PolyfillClone for &'a [T] {
29    #[inline(always)]
30    fn clone(&self) -> Self {
31        *self
32    }
33}
34
35impl PolyfillClone for usize {
36    #[inline(always)]
37    fn clone(&self) -> Self {
38        *self
39    }
40}
41
42impl PolyfillClone for u8 {
43    #[inline(always)]
44    fn clone(&self) -> Self {
45        *self
46    }
47}
48
49impl PolyfillClone for u16 {
50    #[inline(always)]
51    fn clone(&self) -> Self {
52        *self
53    }
54}
55
56// Can't do this due to https://github.com/verus-lang/verus/issues/1108
57// impl PolyfillClone for () {
58//     fn clone(&self) -> Self {
59//         ()
60//     }
61// }
62
63impl<T: Copy> PolyfillClone for Vec<T> {
64    /// We trust the builtin Vec::clone implementation
65    #[verifier::external_body]
66    #[inline(always)]
67    fn clone(&self) -> Self {
68        Clone::clone(self)
69    }
70}
71
72impl<T1: PolyfillClone, T2: PolyfillClone> PolyfillClone for (T1, T2) {
73    #[inline(always)]
74    fn clone(&self) -> Self {
75        (self.0.clone(), self.1.clone())
76    }
77}
78
79impl<T1: PolyfillClone, T2: PolyfillClone> PolyfillClone for Either<T1, T2> {
80    #[inline(always)]
81    fn clone(&self) -> Self {
82        match self {
83            Either::Left(v) => Either::Left(v.clone()),
84            Either::Right(v) => Either::Right(v.clone()),
85        }
86    }
87}
88
89}
verdict_parser/common/clone.rs

verdict_parser/common/
clone.rs
