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
127macro_rules! tuple_eq_impl {
128 ($modname:ident, $($T:ident )+) => {
129 verus! {
130 mod $modname {
131 use super::*;
132
133 pub broadcast proof fn lemma_obeys_eq_spec<$($T,)+>()
134 where
135 $($T: PartialEq,)+
136 requires
137 $(obeys_eq::<$T>(),)+
138 ensures
139 #[trigger] obeys_eq::<($($T,)+)>(),
140 {
141 reveal(obeys_eq_spec_properties);
142 }
143
144 pub broadcast proof fn lemma_obeys_concrete_eq<$($T,)+>()
145 where
146 $($T: PartialEq,)+
147 requires
148 $(obeys_concrete_eq::<$T>(),)+
149 ensures
150 #[trigger] obeys_concrete_eq::<($($T,)+)>(),
151 {
152 reveal(obeys_concrete_eq);
153 }
154
155 pub broadcast proof fn lemma_obeys_view_eq<$($T,)+>()
156 where
157 $($T: PartialEq + View,)+
158 requires
159 $(obeys_view_eq::<$T>(),)+
160 ensures
161 #[trigger] obeys_view_eq::<($($T,)+)>(),
162 {
163 reveal(obeys_view_eq);
164 }
165
166 pub broadcast proof fn lemma_obeys_deep_eq<$($T,)+>()
167 where
168 $($T: PartialEq + DeepView,)+
169 requires
170 $(obeys_deep_eq::<$T>(),)+
171 ensures
172 #[trigger] obeys_deep_eq::<($($T,)+)>(),
173 {
174 reveal(obeys_deep_eq);
175 }
176
177 pub broadcast group group_laws_eq {
178 lemma_obeys_eq_spec,
179 lemma_obeys_concrete_eq,
180 lemma_obeys_view_eq,
181 lemma_obeys_deep_eq,
182 }
183 }
184 }
185 }
186}
187
188tuple_eq_impl!(tuple_1_laws, T);
189
190tuple_eq_impl!(tuple_2_laws, U T);
191
192proof fn lemma_isomorphic_obeys_eq<T: PartialEq, U: PartialEq>(f: spec_fn(U) -> T)
193 requires
194 obeys_eq::<T>(),
195 U::obeys_eq_spec(),
196 forall|x: U, y: U| x.eq_spec(&y) == f(x).eq_spec(&f(y)),
197 ensures
198 obeys_eq::<U>(),
199{
200 reveal(obeys_eq_spec_properties);
201}
202
203macro_rules! tuple_eq_induct_impl {
204 ($modname:ident, $inductmod:ident, 0 $U:ident, $($idx:tt $T:ident, )+) => {
205 verus! {
206 mod $modname {
207 use super::*;
208
209 pub broadcast proof fn lemma_obeys_eq_spec<$U, $($T,)+>()
210 where
211 $U: PartialEq,
212 $($T: PartialEq,)+
213 requires
214 obeys_eq::<$U>(),
215 $(obeys_eq::<$T>(),)+
216 ensures
217 #[trigger] obeys_eq::<($U, $($T,)+)>(),
218 {
219 broadcast use tuple_2_laws::lemma_obeys_eq_spec;
220 broadcast use $inductmod::lemma_obeys_eq_spec;
221 lemma_isomorphic_obeys_eq(|x: ($U, $($T,)+)| (x.0, ($(x.$idx,)+)));
222 reveal(obeys_eq_spec_properties);
223 }
224
225 pub broadcast proof fn lemma_obeys_concrete_eq<$U, $($T,)+>()
226 where
227 $U: PartialEq,
228 $($T: PartialEq,)+
229 requires
230 obeys_concrete_eq::<$U>(),
231 $(obeys_concrete_eq::<$T>(),)+
232 ensures
233 #[trigger] obeys_concrete_eq::<($U, $($T,)+)>(),
234 {
235 reveal(obeys_concrete_eq);
236 }
237
238 pub broadcast proof fn lemma_obeys_view_eq<$U, $($T,)+>()
239 where
240 $U: PartialEq + View,
241 $($T: PartialEq + View,)+
242 requires
243 obeys_view_eq::<$U>(),
244 $(obeys_view_eq::<$T>(),)+
245 ensures
246 #[trigger] obeys_view_eq::<($U, $($T,)+)>(),
247 {
248 broadcast use tuple_2_laws::group_laws_eq;
249 broadcast use $inductmod::group_laws_eq;
250 reveal(obeys_view_eq);
251 }
252
253 pub broadcast proof fn lemma_obeys_deep_eq<$U, $($T,)+>()
254 where
255 $U: PartialEq + DeepView,
256 $($T: PartialEq + DeepView,)+
257 requires
258 obeys_deep_eq::<$U>(),
259 $(obeys_deep_eq::<$T>(),)+
260 ensures
261 #[trigger] obeys_deep_eq::<($U, $($T,)+)>(),
262 {
263 broadcast use tuple_2_laws::group_laws_eq;
264 broadcast use $inductmod::group_laws_eq;
265 reveal(obeys_deep_eq);
266 }
267
268 pub broadcast group group_laws_eq {
269 lemma_obeys_eq_spec,
270 lemma_obeys_concrete_eq,
271 lemma_obeys_view_eq,
272 lemma_obeys_deep_eq,
273 }
274 }
275 }
276 };
277}
278
279tuple_eq_induct_impl!(tuple_3_laws, tuple_2_laws, 0 V, 1 U, 2 T,);
280
281tuple_eq_induct_impl!(tuple_4_laws, tuple_3_laws, 0 X, 1 W, 2 V, 3 U, );
282
283tuple_eq_induct_impl!(tuple_5_laws, tuple_4_laws, 0 X, 1 W, 2 V, 3 U, 4 T, );
284
285tuple_eq_induct_impl!(tuple_6_laws, tuple_5_laws, 0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
286
287tuple_eq_induct_impl!(tuple_7_laws, tuple_6_laws, 0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
288
289tuple_eq_induct_impl!(tuple_8_laws, tuple_7_laws, 0 A, 1 Z, 2 Y, 3 X, 4 W, 5 V, 6 U, 7 T, );
290
291tuple_eq_induct_impl!(tuple_9_laws, tuple_8_laws, 0 B, 1 A, 2 Z, 3 Y, 4 X, 5 W, 6 V, 7 U, 8 T, );
292
293tuple_eq_induct_impl!(tuple_10_laws, tuple_9_laws, 0 C, 1 B, 2 A, 3 Z, 4 Y, 5 X, 6 W, 7 V, 8 U, 9 T, );
294
295tuple_eq_induct_impl!(tuple_11_laws, tuple_10_laws, 0 D, 1 C, 2 B, 3 A, 4 Z, 5 Y, 6 X, 7 W, 8 V, 9 U, 10 T, );
296
297tuple_eq_induct_impl!(tuple_12_laws, tuple_11_laws, 0 E, 1 D, 2 C, 3 B, 4 A, 5 Z, 6 Y, 7 X, 8 W, 9 V, 10 U, 11 T, );
298
299pub broadcast proof fn lemma_ref_obeys_eq_spec<T: PartialEq>()
302 requires
303 obeys_eq::<T>(),
304 ensures
305 #[trigger] obeys_eq::<&T>(),
306{
307 reveal(obeys_eq_spec_properties);
308}
309
310pub broadcast proof fn lemma_ref_obeys_concrete_eq<T: PartialEq>()
311 requires
312 obeys_concrete_eq::<T>(),
313 ensures
314 #[trigger] obeys_concrete_eq::<&T>(),
315{
316 reveal(obeys_concrete_eq);
317}
318
319pub broadcast proof fn lemma_ref_obeys_view_eq<T: PartialEq + View>()
320 requires
321 obeys_view_eq::<T>(),
322 ensures
323 #[trigger] obeys_view_eq::<&T>(),
324{
325 reveal(obeys_view_eq);
326}
327
328pub broadcast proof fn lemma_ref_obeys_deep_eq<T: PartialEq + DeepView>()
329 requires
330 obeys_deep_eq::<T>(),
331 ensures
332 #[trigger] obeys_deep_eq::<&T>(),
333{
334 reveal(obeys_deep_eq);
335}
336
337pub broadcast proof fn lemma_option_obeys_eq_spec<T: PartialEq>()
340 requires
341 obeys_eq::<T>(),
342 ensures
343 #[trigger] obeys_eq::<Option<T>>(),
344{
345 reveal(obeys_eq_spec_properties);
346}
347
348pub broadcast proof fn lemma_option_obeys_concrete_eq<T: PartialEq>()
349 requires
350 obeys_concrete_eq::<T>(),
351 ensures
352 #[trigger] obeys_concrete_eq::<Option<T>>(),
353{
354 reveal(obeys_concrete_eq);
355}
356
357pub broadcast proof fn lemma_option_obeys_view_eq<T: PartialEq + View>()
358 requires
359 obeys_concrete_eq::<T>(),
360 ensures
361 #[trigger] obeys_view_eq::<Option<T>>(),
362{
363 reveal(obeys_concrete_eq);
364 reveal(obeys_view_eq);
365}
366
367pub broadcast proof fn lemma_option_obeys_deep_eq<T: PartialEq + DeepView>()
368 requires
369 obeys_deep_eq::<T>(),
370 ensures
371 #[trigger] obeys_deep_eq::<Option<T>>(),
372{
373 reveal(obeys_deep_eq);
374}
375
376pub broadcast group group_laws_eq {
377 axiom_structural_obeys_concrete_eq,
378 bool_laws::group_laws_eq,
379 u8_laws::group_laws_eq,
380 i8_laws::group_laws_eq,
381 u16_laws::group_laws_eq,
382 i16_laws::group_laws_eq,
383 u32_laws::group_laws_eq,
384 i32_laws::group_laws_eq,
385 u64_laws::group_laws_eq,
386 i64_laws::group_laws_eq,
387 u128_laws::group_laws_eq,
388 i128_laws::group_laws_eq,
389 usize_laws::group_laws_eq,
390 isize_laws::group_laws_eq,
391 tuple_1_laws::group_laws_eq,
392 tuple_2_laws::group_laws_eq,
393 tuple_3_laws::group_laws_eq,
394 tuple_4_laws::group_laws_eq,
395 tuple_5_laws::group_laws_eq,
396 tuple_6_laws::group_laws_eq,
397 tuple_7_laws::group_laws_eq,
398 tuple_8_laws::group_laws_eq,
399 tuple_9_laws::group_laws_eq,
400 tuple_10_laws::group_laws_eq,
401 tuple_11_laws::group_laws_eq,
402 tuple_12_laws::group_laws_eq,
403 lemma_ref_obeys_eq_spec,
404 lemma_ref_obeys_concrete_eq,
405 lemma_ref_obeys_view_eq,
406 lemma_ref_obeys_deep_eq,
407 lemma_option_obeys_eq_spec,
408 lemma_option_obeys_concrete_eq,
409 lemma_option_obeys_view_eq,
410 lemma_option_obeys_deep_eq,
411}
412
413}