verdict_parser/common/
eq.rs

1use super::*;
2use crate::asn1::*;
3/// Define and implement a temporary Eq replacement "PolyfillEq" for some types
4use vstd::prelude::*;
5
6verus! {
7
8/// A temporary replacement Clone
9pub trait PolyfillEq: View + Sized {
10    fn polyfill_eq(&self, other: &Self) -> (res: bool)
11        ensures
12            res <==> (self@ == other@);
13}
14
15macro_rules! impl_trivial_polyfill_eq {
16    ($($t:ty)*) => {
17        $(
18            ::builtin_macros::verus! {
19                impl PolyfillEq for $t {
20                    #[inline(always)]
21                    fn polyfill_eq(&self, other: &Self) -> bool {
22                        self == other
23                    }
24                }
25            }
26        )*
27    };
28}
29
30impl_trivial_polyfill_eq! {
31    bool
32    u8 u16 u32 u64 u128
33    i8 i16 i32 i64 i128
34    usize
35}
36
37macro_rules! impl_polyfill_eq_for_slice_vec {
38    ($($t:ty)*) => {
39        $(
40            ::builtin_macros::verus! {
41                impl PolyfillEq for &[$t] {
42                    fn polyfill_eq(&self, other: &Self) -> bool {
43                        if self.len() != other.len() {
44                            return false;
45                        }
46
47                        let len = self.len();
48                        for i in 0..len
49                            invariant
50                                len == self@.len(),
51                                self@.len() == other@.len(),
52                                forall |j| !(0 <= j < i) || self@[j] == other@[j],
53                        {
54                            if self[i] != other[i] {
55                                return false;
56                            }
57                        }
58
59                        assert(::builtin::ext_equal(self@, other@));
60
61                        true
62                    }
63                }
64
65                impl PolyfillEq for Vec<$t> {
66                    fn polyfill_eq(&self, other: &Self) -> bool {
67                        self.as_slice().polyfill_eq(&other.as_slice())
68                    }
69                }
70            }
71        )*
72    };
73}
74
75impl_polyfill_eq_for_slice_vec! {
76    bool
77    u8 u16 u32 u64 u128
78    i8 i16 i32 i64 i128
79    usize
80}
81
82impl<T: PolyfillEq> PolyfillEq for VecDeep<T> {
83    fn polyfill_eq(&self, other: &Self) -> (res: bool)
84    {
85        if self.len() != other.len() {
86            return false;
87        }
88
89        let len = self.len();
90        for i in 0..len
91            invariant
92                len == self@.len(),
93                self@.len() == other@.len(),
94                forall |j| 0 <= j < i ==> self@[j] == other@[j],
95        {
96            if !self.get(i).polyfill_eq(&other.get(i)) {
97                return false;
98            }
99        }
100
101        assert(self@ =~= other@);
102
103        true
104    }
105}
106
107impl<U: PolyfillEq, V: PolyfillEq> PolyfillEq for Either<U, V> {
108    #[inline(always)]
109    fn polyfill_eq(&self, other: &Self) -> (res: bool) {
110        match (self, other) {
111            (Either::Left(a), Either::Left(b)) => a.polyfill_eq(b),
112            (Either::Right(a), Either::Right(b)) => a.polyfill_eq(b),
113            _ => false,
114        }
115    }
116}
117
118impl PolyfillEq for NullValue {
119    #[inline(always)]
120    fn polyfill_eq(&self, _other: &Self) -> (res: bool) {
121        true
122    }
123}
124
125impl PolyfillEq for EndValue {
126    #[inline(always)]
127    fn polyfill_eq(&self, _other: &Self) -> (res: bool) {
128        true
129    }
130}
131
132}
verdict_parser/common/eq.rs

verdict_parser/common/
eq.rs
