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_spec<T: PartialEq>() -> bool {
18    &&& T::obeys_eq_spec()
19    &&& obeys_eq_spec_properties::<T>()
20}
21
22#[verifier::opaque]
23pub open spec fn obeys_concrete_eq<T: PartialEq>() -> bool {
24    &&& T::obeys_eq_spec()
25    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x == y
26}
27
28#[verifier::opaque]
29pub open spec fn obeys_view_eq<T: PartialEq + View>() -> 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_deep_eq<T: PartialEq + DeepView>() -> bool {
36    &&& T::obeys_eq_spec()
37    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x.deep_view() == y.deep_view()
38}
39
40pub broadcast proof fn axiom_structural_obeys_concrete_eq<T: PartialEq + Structural>()
41    requires
42        T::obeys_eq_spec(),
43        forall|x: T, y: T| x.eq_spec(&y) <==> x == y,
44    ensures
45        #[trigger] obeys_concrete_eq::<T>(),
46{
47    reveal(obeys_concrete_eq);
48}
49
50macro_rules! primitive_laws_eq {
51    ($n: ty, $modname:ident) => {
52        verus! {
53        mod $modname {
54            use super::*;
55
56            pub broadcast proof fn lemma_obeys_eq_spec()
57                ensures
58                    #[trigger] obeys_eq_spec::<$n>(),
59            {
60                reveal(obeys_eq_spec_properties);
61            }
62
63            pub broadcast proof fn lemma_obeys_concrete_eq()
64                ensures
65                    #[trigger] obeys_concrete_eq::<$n>(),
66            {
67                reveal(obeys_concrete_eq);
68            }
69
70            pub broadcast proof fn lemma_obeys_view_eq()
71                ensures
72                    #[trigger] obeys_view_eq::<$n>(),
73            {
74                reveal(obeys_view_eq);
75            }
76
77            pub broadcast proof fn lemma_obeys_deep_eq()
78                ensures
79                    #[trigger] obeys_deep_eq::<$n>(),
80            {
81                reveal(obeys_deep_eq);
82            }
83
84            pub broadcast group group_laws_eq {
85                lemma_obeys_eq_spec,
86                lemma_obeys_concrete_eq,
87                lemma_obeys_view_eq,
88                lemma_obeys_deep_eq,
89            }
90        }
91        }
92    }
93}
94
95primitive_laws_eq!(bool, bool_laws);
96
97primitive_laws_eq!(u8, u8_laws);
98
99primitive_laws_eq!(i8, i8_laws);
100
101primitive_laws_eq!(u16, u16_laws);
102
103primitive_laws_eq!(i16, i16_laws);
104
105primitive_laws_eq!(u32, u32_laws);
106
107primitive_laws_eq!(i32, i32_laws);
108
109primitive_laws_eq!(u64, u64_laws);
110
111primitive_laws_eq!(i64, i64_laws);
112
113primitive_laws_eq!(u128, u128_laws);
114
115primitive_laws_eq!(i128, i128_laws);
116
117primitive_laws_eq!(usize, usize_laws);
118
119primitive_laws_eq!(isize, isize_laws);
120
121pub broadcast proof fn lemma_option_obeys_eq_spec<T: PartialEq>()
122    requires
123        obeys_eq_spec::<T>(),
124    ensures
125        #[trigger] obeys_eq_spec::<Option<T>>(),
126{
127    reveal(obeys_eq_spec_properties);
128}
129
130pub broadcast proof fn lemma_option_obeys_concrete_eq<T: PartialEq>()
131    requires
132        obeys_concrete_eq::<T>(),
133    ensures
134        #[trigger] obeys_concrete_eq::<Option<T>>(),
135{
136    reveal(obeys_concrete_eq);
137}
138
139pub broadcast proof fn lemma_option_obeys_view_eq<T: PartialEq + View>()
140    requires
141        obeys_concrete_eq::<T>(),
142    ensures
143        #[trigger] obeys_view_eq::<Option<T>>(),
144{
145    reveal(obeys_concrete_eq);
146    reveal(obeys_view_eq);
147}
148
149pub broadcast proof fn lemma_option_obeys_deep_eq<T: PartialEq + DeepView>()
150    requires
151        obeys_deep_eq::<T>(),
152    ensures
153        #[trigger] obeys_deep_eq::<Option<T>>(),
154{
155    reveal(obeys_deep_eq);
156}
157
158pub broadcast group group_laws_eq {
159    axiom_structural_obeys_concrete_eq,
160    bool_laws::group_laws_eq,
161    u8_laws::group_laws_eq,
162    i8_laws::group_laws_eq,
163    u16_laws::group_laws_eq,
164    i16_laws::group_laws_eq,
165    u32_laws::group_laws_eq,
166    i32_laws::group_laws_eq,
167    u64_laws::group_laws_eq,
168    i64_laws::group_laws_eq,
169    u128_laws::group_laws_eq,
170    i128_laws::group_laws_eq,
171    usize_laws::group_laws_eq,
172    isize_laws::group_laws_eq,
173    lemma_option_obeys_eq_spec,
174    lemma_option_obeys_concrete_eq,
175    lemma_option_obeys_view_eq,
176    lemma_option_obeys_deep_eq,
177}
178
179} // verus!
vstd/laws_eq.rs

vstd/
laws_eq.rs
