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
60/// Whether the type's cmp spec matches structural equality, i.e.,
61/// whether `v1.cmp(&v2) is Equal <==> v1 == v2`.
62pub open spec fn obeys_cmp_concrete_eq<T: Ord>() -> bool {
63    forall|v1: T, v2: T| v1.cmp_spec(&v2) is Equal <==> v1 == v2
64}
65
66/// Whether the type's cmp spec matches deep-view equality, i.e.,
67/// whether `v1.cmp(&v2) is Equal <==> v1.deep_view() == v2.deep_view()`.
68pub open spec fn obeys_cmp_deep_eq<T: Ord + DeepView>() -> bool {
69    forall|v1: T, v2: T| v1.cmp_spec(&v2) is Equal <==> v1.deep_view() == v2.deep_view()
70}
71
72macro_rules! num_laws_cmp {
73    ($n: ty, $modname:ident) => {
74        verus! {
75        mod $modname {
76            use super::*;
77
78            pub broadcast proof fn lemma_obeys_cmp_spec()
79                ensures
80                    #[trigger] obeys_cmp::<$n>(),
81            {
82                broadcast use group_laws_eq;
83                reveal(obeys_eq_spec_properties);
84                reveal(obeys_partial_cmp_spec_properties);
85                reveal(obeys_cmp_partial_ord);
86                reveal(obeys_cmp_ord);
87                assert(obeys_eq::<$n>());
88            }
89        }
90        }
91    }
92}
93
94num_laws_cmp!(u8, u8_laws);
95
96num_laws_cmp!(i8, i8_laws);
97
98num_laws_cmp!(u16, u16_laws);
99
100num_laws_cmp!(i16, i16_laws);
101
102num_laws_cmp!(u32, u32_laws);
103
104num_laws_cmp!(i32, i32_laws);
105
106num_laws_cmp!(u64, u64_laws);
107
108num_laws_cmp!(i64, i64_laws);
109
110num_laws_cmp!(u128, u128_laws);
111
112num_laws_cmp!(i128, i128_laws);
113
114num_laws_cmp!(usize, usize_laws);
115
116num_laws_cmp!(isize, isize_laws);
117
118macro_rules! tuple_cmp_impl {
119    ($modname:ident, $($T:ident )+) => {
120        verus! {
121        mod $modname {
122            use super::*;
123
124            pub broadcast proof fn lemma_obeys_cmp_spec<$($T,)+>()
125                where
126                    $($T: Ord + PartialEq,)+
127                requires
128                    $(obeys_cmp::<$T>(),)+
129                ensures
130                    #[trigger] obeys_cmp::<($($T,)+)>(),
131            {
132                broadcast use group_laws_eq;
133                reveal(obeys_eq_spec_properties);
134                reveal(obeys_partial_cmp_spec_properties);
135                reveal(obeys_cmp_partial_ord);
136                reveal(obeys_cmp_ord);
137                assert(obeys_cmp::<($($T,)+)>());
138            }
139        }
140        }
141    }
142}
143
144tuple_cmp_impl!(tuple_1_laws, T);
145
146tuple_cmp_impl!(tuple_2_laws, U T);
147
148proof fn lemma_isomorphic_obeys_cmp<T: PartialEq + Ord, U: PartialEq + Ord>(f: spec_fn(U) -> T)
149    requires
150        obeys_cmp::<T>(),
151        obeys_eq::<U>(),
152        U::obeys_partial_cmp_spec(),
153        U::obeys_cmp_spec(),
154        forall|x: U, y: U| x.eq_spec(&y) == f(x).eq_spec(&f(y)),
155        forall|x: U, y: U| x.partial_cmp_spec(&y) == f(x).partial_cmp_spec(&f(y)),
156        forall|x: U, y: U| x.cmp_spec(&y) == f(x).cmp_spec(&f(y)),
157    ensures
158        obeys_cmp::<U>(),
159{
160    reveal(obeys_eq_spec_properties);
161    reveal(obeys_partial_cmp_spec_properties);
162    reveal(obeys_cmp_partial_ord);
163    reveal(obeys_cmp_ord);
164}
165
166proof fn lemma_obeys_cmp_obeys_traits<T: Ord>()
167    requires
168        obeys_cmp::<T>(),
169    ensures
170        T::obeys_eq_spec(),
171        T::obeys_partial_cmp_spec(),
172        T::obeys_cmp_spec(),
173{
174    reveal(obeys_cmp_partial_ord);
175    reveal(obeys_cmp_ord);
176}
177
178macro_rules! tuple_cmp_induct_impl {
179    ($modname:ident, $inductmod:ident, 0 $U:ident, $($idx:tt $T:ident, )+) => {
180        verus! {
181        mod $modname {
182            use super::*;
183
184            pub broadcast proof fn lemma_obeys_cmp_spec<$U, $($T,)+>()
185                where
186                    $U: Ord + PartialEq,
187                    $($T: Ord + PartialEq,)+
188                requires
189                    obeys_cmp::<$U>(),
190                    $(obeys_cmp::<$T>(),)+
191                ensures
192                    #[trigger] obeys_cmp::<($U, $($T,)+)>(),
193            {
194                broadcast use super::tuple_2_laws::lemma_obeys_cmp_spec;
195                broadcast use super::$inductmod::lemma_obeys_cmp_spec;
196                broadcast use group_laws_eq;
197                lemma_obeys_cmp_obeys_traits::<$U>();
198                $(lemma_obeys_cmp_obeys_traits::<$T>();)+
199                lemma_isomorphic_obeys_cmp(|x: ($U, $($T,)+)| (x.0, ($(x.$idx,)+)));
200                assert(obeys_cmp::<($U, $($T,)+)>());
201            }
202        }
203        }
204    };
205}
206
207tuple_cmp_induct_impl!(tuple_3_laws, tuple_2_laws, 0 V, 1 U, 2 T,);
208
209tuple_cmp_induct_impl!(tuple_4_laws, tuple_3_laws, 0 X, 1 W, 2 V, 3 U, );
210
211tuple_cmp_induct_impl!(tuple_5_laws, tuple_4_laws, 0 X, 1 W, 2 V, 3 U, 4 T, );
212
213tuple_cmp_induct_impl!(tuple_6_laws, tuple_5_laws, 0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
214
215tuple_cmp_induct_impl!(tuple_7_laws, tuple_6_laws, 0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
216
217tuple_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, );
218
219tuple_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, );
220
221tuple_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, );
222
223tuple_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, );
224
225tuple_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, );
226
227pub broadcast proof fn lemma_ref_obeys_cmp_spec<T: Ord>()
228    requires
229        obeys_cmp::<T>(),
230    ensures
231        #[trigger] obeys_cmp::<&T>(),
232{
233    broadcast use lemma_ref_obeys_eq_spec;
234
235    assert(obeys_eq::<&T>());
236
237    assert(obeys_cmp_partial_ord::<&T>() && obeys_cmp_ord::<&T>()) by {
238        reveal(obeys_cmp_partial_ord);
239        reveal(obeys_cmp_ord);
240    }
241
242    assert(obeys_partial_cmp_spec_properties::<&T>()) by {
243        reveal(obeys_cmp_partial_ord);
244        reveal(obeys_partial_cmp_spec_properties);
245    }
246}
247
248pub broadcast proof fn lemma_option_obeys_cmp_spec<T: Ord>()
249    requires
250        obeys_cmp::<T>(),
251    ensures
252        #[trigger] obeys_cmp::<Option<T>>(),
253{
254    broadcast use lemma_option_obeys_eq_spec;
255
256    assert(obeys_eq::<Option<T>>());
257
258    assert(obeys_cmp_partial_ord::<Option<T>>() && obeys_cmp_ord::<Option<T>>()) by {
259        reveal(obeys_cmp_partial_ord);
260        reveal(obeys_cmp_ord);
261    }
262
263    assert(obeys_partial_cmp_spec_properties::<Option<T>>()) by {
264        reveal(obeys_cmp_partial_ord);
265        reveal(obeys_partial_cmp_spec_properties);
266    }
267}
268
269pub broadcast group group_laws_cmp {
270    u8_laws::lemma_obeys_cmp_spec,
271    i8_laws::lemma_obeys_cmp_spec,
272    u16_laws::lemma_obeys_cmp_spec,
273    i16_laws::lemma_obeys_cmp_spec,
274    u32_laws::lemma_obeys_cmp_spec,
275    i32_laws::lemma_obeys_cmp_spec,
276    u64_laws::lemma_obeys_cmp_spec,
277    i64_laws::lemma_obeys_cmp_spec,
278    u128_laws::lemma_obeys_cmp_spec,
279    i128_laws::lemma_obeys_cmp_spec,
280    usize_laws::lemma_obeys_cmp_spec,
281    isize_laws::lemma_obeys_cmp_spec,
282    lemma_ref_obeys_cmp_spec,
283    lemma_option_obeys_cmp_spec,
284    tuple_1_laws::lemma_obeys_cmp_spec,
285    tuple_2_laws::lemma_obeys_cmp_spec,
286    tuple_3_laws::lemma_obeys_cmp_spec,
287    tuple_4_laws::lemma_obeys_cmp_spec,
288    tuple_5_laws::lemma_obeys_cmp_spec,
289    tuple_6_laws::lemma_obeys_cmp_spec,
290    tuple_7_laws::lemma_obeys_cmp_spec,
291    tuple_8_laws::lemma_obeys_cmp_spec,
292    tuple_9_laws::lemma_obeys_cmp_spec,
293    tuple_10_laws::lemma_obeys_cmp_spec,
294    tuple_11_laws::lemma_obeys_cmp_spec,
295    tuple_12_laws::lemma_obeys_cmp_spec,
296}
297
298} // verus!
vstd/laws_cmp.rs

vstd/
laws_cmp.rs
