vstd/
laws_eq.rs

1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4use super::prelude::*;
5use super::std_specs::cmp::PartialEqSpec;
6use super::view::*;
7
8verus! {
9
10#[verifier::opaque]
11pub open spec fn obeys_eq_spec_properties<T: PartialEq>() -> bool {
12    &&& forall|x: T, y: T| #[trigger] x.eq_spec(&y) <==> y.eq_spec(&x)
13    &&& forall|x: T, y: T, z: T|
14        x.eq_spec(&y) && #[trigger] y.eq_spec(&z) ==> #[trigger] x.eq_spec(&z)
15}
16
17pub open spec fn obeys_eq<T: PartialEq>() -> bool {
18    &&& T::obeys_eq_spec()
19    &&& obeys_eq_spec_properties::<T>()
20}
21
22#[deprecated(note = "`laws_eq::obeys_eq_spec` has been renamed to `laws_eq::obeys_eq`")]
23#[verifier::inline]
24pub open spec fn obeys_eq_spec<T: PartialEq>() -> bool {
25    obeys_eq::<T>()
26}
27
28#[verifier::opaque]
29pub open spec fn obeys_concrete_eq<T: PartialEq>() -> bool {
30    &&& T::obeys_eq_spec()
31    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x == y
32}
33
34#[verifier::opaque]
35pub open spec fn obeys_view_eq<T: PartialEq + View>() -> bool {
36    &&& T::obeys_eq_spec()
37    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x@ == y@
38}
39
40#[verifier::opaque]
41pub open spec fn obeys_deep_eq<T: PartialEq + DeepView>() -> bool {
42    &&& T::obeys_eq_spec()
43    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x.deep_view() == y.deep_view()
44}
45
46pub broadcast proof fn axiom_structural_obeys_concrete_eq<T: PartialEq + Structural>()
47    requires
48        T::obeys_eq_spec(),
49        forall|x: T, y: T| x.eq_spec(&y) <==> x == y,
50    ensures
51        #[trigger] obeys_concrete_eq::<T>(),
52{
53    reveal(obeys_concrete_eq);
54}
55
56macro_rules! primitive_laws_eq {
57    ($n: ty, $modname:ident) => {
58        verus! {
59        mod $modname {
60            use super::*;
61
62            pub broadcast proof fn lemma_obeys_eq_spec()
63                ensures
64                    #[trigger] obeys_eq::<$n>(),
65            {
66                reveal(obeys_eq_spec_properties);
67            }
68
69            pub broadcast proof fn lemma_obeys_concrete_eq()
70                ensures
71                    #[trigger] obeys_concrete_eq::<$n>(),
72            {
73                reveal(obeys_concrete_eq);
74            }
75
76            pub broadcast proof fn lemma_obeys_view_eq()
77                ensures
78                    #[trigger] obeys_view_eq::<$n>(),
79            {
80                reveal(obeys_view_eq);
81            }
82
83            pub broadcast proof fn lemma_obeys_deep_eq()
84                ensures
85                    #[trigger] obeys_deep_eq::<$n>(),
86            {
87                reveal(obeys_deep_eq);
88            }
89
90            pub broadcast group group_laws_eq {
91                lemma_obeys_eq_spec,
92                lemma_obeys_concrete_eq,
93                lemma_obeys_view_eq,
94                lemma_obeys_deep_eq,
95            }
96        }
97        }
98    }
99}
100
101primitive_laws_eq!(bool, bool_laws);
102
103primitive_laws_eq!(u8, u8_laws);
104
105primitive_laws_eq!(i8, i8_laws);
106
107primitive_laws_eq!(u16, u16_laws);
108
109primitive_laws_eq!(i16, i16_laws);
110
111primitive_laws_eq!(u32, u32_laws);
112
113primitive_laws_eq!(i32, i32_laws);
114
115primitive_laws_eq!(u64, u64_laws);
116
117primitive_laws_eq!(i64, i64_laws);
118
119primitive_laws_eq!(u128, u128_laws);
120
121primitive_laws_eq!(i128, i128_laws);
122
123primitive_laws_eq!(usize, usize_laws);
124
125primitive_laws_eq!(isize, isize_laws);
126
127/* references */
128
129pub broadcast proof fn lemma_ref_obeys_eq_spec<T: PartialEq>()
130    requires
131        obeys_eq::<T>(),
132    ensures
133        #[trigger] obeys_eq::<&T>(),
134{
135    reveal(obeys_eq_spec_properties);
136}
137
138pub broadcast proof fn lemma_ref_obeys_concrete_eq<T: PartialEq>()
139    requires
140        obeys_concrete_eq::<T>(),
141    ensures
142        #[trigger] obeys_concrete_eq::<&T>(),
143{
144    reveal(obeys_concrete_eq);
145}
146
147pub broadcast proof fn lemma_ref_obeys_view_eq<T: PartialEq + View>()
148    requires
149        obeys_view_eq::<T>(),
150    ensures
151        #[trigger] obeys_view_eq::<&T>(),
152{
153    reveal(obeys_view_eq);
154}
155
156pub broadcast proof fn lemma_ref_obeys_deep_eq<T: PartialEq + DeepView>()
157    requires
158        obeys_deep_eq::<T>(),
159    ensures
160        #[trigger] obeys_deep_eq::<&T>(),
161{
162    reveal(obeys_deep_eq);
163}
164
165/* Option */
166
167pub broadcast proof fn lemma_option_obeys_eq_spec<T: PartialEq>()
168    requires
169        obeys_eq::<T>(),
170    ensures
171        #[trigger] obeys_eq::<Option<T>>(),
172{
173    reveal(obeys_eq_spec_properties);
174}
175
176pub broadcast proof fn lemma_option_obeys_concrete_eq<T: PartialEq>()
177    requires
178        obeys_concrete_eq::<T>(),
179    ensures
180        #[trigger] obeys_concrete_eq::<Option<T>>(),
181{
182    reveal(obeys_concrete_eq);
183}
184
185pub broadcast proof fn lemma_option_obeys_view_eq<T: PartialEq + View>()
186    requires
187        obeys_concrete_eq::<T>(),
188    ensures
189        #[trigger] obeys_view_eq::<Option<T>>(),
190{
191    reveal(obeys_concrete_eq);
192    reveal(obeys_view_eq);
193}
194
195pub broadcast proof fn lemma_option_obeys_deep_eq<T: PartialEq + DeepView>()
196    requires
197        obeys_deep_eq::<T>(),
198    ensures
199        #[trigger] obeys_deep_eq::<Option<T>>(),
200{
201    reveal(obeys_deep_eq);
202}
203
204pub broadcast group group_laws_eq {
205    axiom_structural_obeys_concrete_eq,
206    bool_laws::group_laws_eq,
207    u8_laws::group_laws_eq,
208    i8_laws::group_laws_eq,
209    u16_laws::group_laws_eq,
210    i16_laws::group_laws_eq,
211    u32_laws::group_laws_eq,
212    i32_laws::group_laws_eq,
213    u64_laws::group_laws_eq,
214    i64_laws::group_laws_eq,
215    u128_laws::group_laws_eq,
216    i128_laws::group_laws_eq,
217    usize_laws::group_laws_eq,
218    isize_laws::group_laws_eq,
219    lemma_ref_obeys_eq_spec,
220    lemma_ref_obeys_concrete_eq,
221    lemma_ref_obeys_view_eq,
222    lemma_ref_obeys_deep_eq,
223    lemma_option_obeys_eq_spec,
224    lemma_option_obeys_concrete_eq,
225    lemma_option_obeys_view_eq,
226    lemma_option_obeys_deep_eq,
227}
228
229} // verus!
vstd/laws_eq.rs

vstd/
laws_eq.rs
