vstd/
laws_cmp.rs

1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4use super::laws_eq::*;
5use super::prelude::*;
6use super::std_specs::cmp::{OrdSpec, PartialEqSpec, PartialOrdSpec};
7use core::cmp::Ordering;
8
9verus! {
10
11#[verifier::opaque]
12pub open spec fn obeys_partial_cmp_spec_properties<T: PartialOrd>() -> bool {
13    &&& forall|x: T, y: T| #[trigger]
14        x.partial_cmp_spec(&y) == Some(Ordering::Equal) <==> x.eq_spec(&y)
15    &&& forall|x: T, y: T| #[trigger]
16        x.partial_cmp_spec(&y) == Some(Ordering::Less) <==> y.partial_cmp_spec(&x) == Some(
17            Ordering::Greater,
18        )
19    &&& forall|x: T, y: T, z: T|
20        x.partial_cmp_spec(&y) == Some(Ordering::Less) && #[trigger] y.partial_cmp_spec(&z) == Some(
21            Ordering::Less,
22        ) ==> #[trigger] x.partial_cmp_spec(&z) == Some(Ordering::Less)
23    &&& forall|x: T, y: T, z: T|
24        x.partial_cmp_spec(&y) == Some(Ordering::Greater) && #[trigger] y.partial_cmp_spec(&z)
25            == Some(Ordering::Greater) ==> #[trigger] x.partial_cmp_spec(&z) == Some(
26            Ordering::Greater,
27        )
28    &&& obeys_eq_spec_properties::<T>()
29}
30
31#[verifier::opaque]
32pub open spec fn obeys_cmp_partial_ord<T: PartialOrd>() -> bool {
33    &&& T::obeys_eq_spec()
34    &&& T::obeys_partial_cmp_spec()
35    &&& forall|x: T, y: T| x.eq_spec(&y) <==> x.partial_cmp_spec(&y) == Some(Ordering::Equal)
36}
37
38#[verifier::opaque]
39pub open spec fn obeys_cmp_ord<T: Ord>() -> bool {
40    &&& T::obeys_cmp_spec()
41    &&& forall|x: T, y: T|
42        #![trigger x.partial_cmp_spec(&y)]
43        #![trigger x.cmp_spec(&y)]
44        x.partial_cmp_spec(&y) == Some(x.cmp_spec(&y))
45}
46
47pub open spec fn obeys_cmp<T: Ord>() -> bool {
48    &&& obeys_eq::<T>()
49    &&& obeys_cmp_partial_ord::<T>()
50    &&& obeys_cmp_ord::<T>()
51    &&& obeys_partial_cmp_spec_properties::<T>()
52}
53
54#[deprecated(note = "`laws_cmp::obeys_cmp_spec` has been renamed to `laws_cmp::obeys_cmp`")]
55#[verifier::inline]
56pub open spec fn obeys_cmp_spec<T: Ord>() -> bool {
57    obeys_cmp::<T>()
58}
59
60macro_rules! num_laws_cmp {
61    ($n: ty, $modname:ident) => {
62        verus! {
63        mod $modname {
64            use super::*;
65
66            pub broadcast proof fn lemma_obeys_cmp_spec()
67                ensures
68                    #[trigger] obeys_cmp::<$n>(),
69            {
70                broadcast use group_laws_eq;
71                reveal(obeys_eq_spec_properties);
72                reveal(obeys_partial_cmp_spec_properties);
73                reveal(obeys_cmp_partial_ord);
74                reveal(obeys_cmp_ord);
75                assert(obeys_eq::<$n>());
76            }
77        }
78        }
79    }
80}
81
82num_laws_cmp!(u8, u8_laws);
83
84num_laws_cmp!(i8, i8_laws);
85
86num_laws_cmp!(u16, u16_laws);
87
88num_laws_cmp!(i16, i16_laws);
89
90num_laws_cmp!(u32, u32_laws);
91
92num_laws_cmp!(i32, i32_laws);
93
94num_laws_cmp!(u64, u64_laws);
95
96num_laws_cmp!(i64, i64_laws);
97
98num_laws_cmp!(u128, u128_laws);
99
100num_laws_cmp!(i128, i128_laws);
101
102num_laws_cmp!(usize, usize_laws);
103
104num_laws_cmp!(isize, isize_laws);
105
106macro_rules! tuple_cmp_impl {
107    ($modname:ident, $($T:ident )+) => {
108        verus! {
109        mod $modname {
110            use super::*;
111
112            pub broadcast proof fn lemma_obeys_cmp_spec<$($T,)+>()
113                where
114                    $($T: Ord + PartialEq,)+
115                requires
116                    $(obeys_cmp::<$T>(),)+
117                ensures
118                    #[trigger] obeys_cmp::<($($T,)+)>(),
119            {
120                broadcast use group_laws_eq;
121                reveal(obeys_eq_spec_properties);
122                reveal(obeys_partial_cmp_spec_properties);
123                reveal(obeys_cmp_partial_ord);
124                reveal(obeys_cmp_ord);
125                assert(obeys_cmp::<($($T,)+)>());
126            }
127        }
128        }
129    }
130}
131
132tuple_cmp_impl!(tuple_1_laws, T);
133
134tuple_cmp_impl!(tuple_2_laws, U T);
135
136proof fn lemma_isomorphic_obeys_cmp<T: PartialEq + Ord, U: PartialEq + Ord>(f: spec_fn(U) -> T)
137    requires
138        obeys_cmp::<T>(),
139        obeys_eq::<U>(),
140        U::obeys_partial_cmp_spec(),
141        U::obeys_cmp_spec(),
142        forall|x: U, y: U| x.eq_spec(&y) == f(x).eq_spec(&f(y)),
143        forall|x: U, y: U| x.partial_cmp_spec(&y) == f(x).partial_cmp_spec(&f(y)),
144        forall|x: U, y: U| x.cmp_spec(&y) == f(x).cmp_spec(&f(y)),
145    ensures
146        obeys_cmp::<U>(),
147{
148    reveal(obeys_eq_spec_properties);
149    reveal(obeys_partial_cmp_spec_properties);
150    reveal(obeys_cmp_partial_ord);
151    reveal(obeys_cmp_ord);
152}
153
154proof fn lemma_obeys_cmp_obeys_traits<T: Ord>()
155    requires
156        obeys_cmp::<T>(),
157    ensures
158        T::obeys_eq_spec(),
159        T::obeys_partial_cmp_spec(),
160        T::obeys_cmp_spec(),
161{
162    reveal(obeys_cmp_partial_ord);
163    reveal(obeys_cmp_ord);
164}
165
166macro_rules! tuple_cmp_induct_impl {
167    ($modname:ident, $inductmod:ident, 0 $U:ident, $($idx:tt $T:ident, )+) => {
168        verus! {
169        mod $modname {
170            use super::*;
171
172            pub broadcast proof fn lemma_obeys_cmp_spec<$U, $($T,)+>()
173                where
174                    $U: Ord + PartialEq,
175                    $($T: Ord + PartialEq,)+
176                requires
177                    obeys_cmp::<$U>(),
178                    $(obeys_cmp::<$T>(),)+
179                ensures
180                    #[trigger] obeys_cmp::<($U, $($T,)+)>(),
181            {
182                broadcast use super::tuple_2_laws::lemma_obeys_cmp_spec;
183                broadcast use super::$inductmod::lemma_obeys_cmp_spec;
184                broadcast use group_laws_eq;
185                lemma_obeys_cmp_obeys_traits::<$U>();
186                $(lemma_obeys_cmp_obeys_traits::<$T>();)+
187                lemma_isomorphic_obeys_cmp(|x: ($U, $($T,)+)| (x.0, ($(x.$idx,)+)));
188                assert(obeys_cmp::<($U, $($T,)+)>());
189            }
190        }
191        }
192    };
193}
194
195tuple_cmp_induct_impl!(tuple_3_laws, tuple_2_laws, 0 V, 1 U, 2 T,);
196
197tuple_cmp_induct_impl!(tuple_4_laws, tuple_3_laws, 0 X, 1 W, 2 V, 3 U, );
198
199tuple_cmp_induct_impl!(tuple_5_laws, tuple_4_laws, 0 X, 1 W, 2 V, 3 U, 4 T, );
200
201tuple_cmp_induct_impl!(tuple_6_laws, tuple_5_laws, 0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
202
203tuple_cmp_induct_impl!(tuple_7_laws, tuple_6_laws, 0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
204
205tuple_cmp_induct_impl!(tuple_8_laws, tuple_7_laws, 0 A, 1 Z, 2 Y, 3 X, 4 W, 5 V, 6 U, 7 T, );
206
207tuple_cmp_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, );
208
209tuple_cmp_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, );
210
211tuple_cmp_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, );
212
213tuple_cmp_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, );
214
215pub broadcast proof fn lemma_ref_obeys_cmp_spec<T: Ord>()
216    requires
217        obeys_cmp::<T>(),
218    ensures
219        #[trigger] obeys_cmp::<&T>(),
220{
221    broadcast use lemma_ref_obeys_eq_spec;
222
223    assert(obeys_eq::<&T>());
224
225    assert(obeys_cmp_partial_ord::<&T>() && obeys_cmp_ord::<&T>()) by {
226        reveal(obeys_cmp_partial_ord);
227        reveal(obeys_cmp_ord);
228    }
229
230    assert(obeys_partial_cmp_spec_properties::<&T>()) by {
231        reveal(obeys_cmp_partial_ord);
232        reveal(obeys_partial_cmp_spec_properties);
233    }
234}
235
236pub broadcast proof fn lemma_option_obeys_cmp_spec<T: Ord>()
237    requires
238        obeys_cmp::<T>(),
239    ensures
240        #[trigger] obeys_cmp::<Option<T>>(),
241{
242    broadcast use lemma_option_obeys_eq_spec;
243
244    assert(obeys_eq::<Option<T>>());
245
246    assert(obeys_cmp_partial_ord::<Option<T>>() && obeys_cmp_ord::<Option<T>>()) by {
247        reveal(obeys_cmp_partial_ord);
248        reveal(obeys_cmp_ord);
249    }
250
251    assert(obeys_partial_cmp_spec_properties::<Option<T>>()) by {
252        reveal(obeys_cmp_partial_ord);
253        reveal(obeys_partial_cmp_spec_properties);
254    }
255}
256
257pub broadcast group group_laws_cmp {
258    u8_laws::lemma_obeys_cmp_spec,
259    i8_laws::lemma_obeys_cmp_spec,
260    u16_laws::lemma_obeys_cmp_spec,
261    i16_laws::lemma_obeys_cmp_spec,
262    u32_laws::lemma_obeys_cmp_spec,
263    i32_laws::lemma_obeys_cmp_spec,
264    u64_laws::lemma_obeys_cmp_spec,
265    i64_laws::lemma_obeys_cmp_spec,
266    u128_laws::lemma_obeys_cmp_spec,
267    i128_laws::lemma_obeys_cmp_spec,
268    usize_laws::lemma_obeys_cmp_spec,
269    isize_laws::lemma_obeys_cmp_spec,
270    lemma_ref_obeys_cmp_spec,
271    lemma_option_obeys_cmp_spec,
272    tuple_1_laws::lemma_obeys_cmp_spec,
273    tuple_2_laws::lemma_obeys_cmp_spec,
274    tuple_3_laws::lemma_obeys_cmp_spec,
275    tuple_4_laws::lemma_obeys_cmp_spec,
276    tuple_5_laws::lemma_obeys_cmp_spec,
277    tuple_6_laws::lemma_obeys_cmp_spec,
278    tuple_7_laws::lemma_obeys_cmp_spec,
279    tuple_8_laws::lemma_obeys_cmp_spec,
280    tuple_9_laws::lemma_obeys_cmp_spec,
281    tuple_10_laws::lemma_obeys_cmp_spec,
282    tuple_11_laws::lemma_obeys_cmp_spec,
283    tuple_12_laws::lemma_obeys_cmp_spec,
284}
285
286} // verus!
vstd/laws_cmp.rs

vstd/
laws_cmp.rs
