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
106pub broadcast proof fn lemma_ref_obeys_cmp_spec<T: Ord>()
107    requires
108        obeys_cmp::<T>(),
109    ensures
110        #[trigger] obeys_cmp::<&T>(),
111{
112    broadcast use lemma_ref_obeys_eq_spec;
113
114    assert(obeys_eq::<&T>());
115
116    assert(obeys_cmp_partial_ord::<&T>() && obeys_cmp_ord::<&T>()) by {
117        reveal(obeys_cmp_partial_ord);
118        reveal(obeys_cmp_ord);
119    }
120
121    assert(obeys_partial_cmp_spec_properties::<&T>()) by {
122        reveal(obeys_cmp_partial_ord);
123        reveal(obeys_partial_cmp_spec_properties);
124    }
125}
126
127pub broadcast proof fn lemma_option_obeys_cmp_spec<T: Ord>()
128    requires
129        obeys_cmp::<T>(),
130    ensures
131        #[trigger] obeys_cmp::<Option<T>>(),
132{
133    broadcast use lemma_option_obeys_eq_spec;
134
135    assert(obeys_eq::<Option<T>>());
136
137    assert(obeys_cmp_partial_ord::<Option<T>>() && obeys_cmp_ord::<Option<T>>()) by {
138        reveal(obeys_cmp_partial_ord);
139        reveal(obeys_cmp_ord);
140    }
141
142    assert(obeys_partial_cmp_spec_properties::<Option<T>>()) by {
143        reveal(obeys_cmp_partial_ord);
144        reveal(obeys_partial_cmp_spec_properties);
145    }
146}
147
148pub broadcast group group_laws_cmp {
149    u8_laws::lemma_obeys_cmp_spec,
150    i8_laws::lemma_obeys_cmp_spec,
151    u16_laws::lemma_obeys_cmp_spec,
152    i16_laws::lemma_obeys_cmp_spec,
153    u32_laws::lemma_obeys_cmp_spec,
154    i32_laws::lemma_obeys_cmp_spec,
155    u64_laws::lemma_obeys_cmp_spec,
156    i64_laws::lemma_obeys_cmp_spec,
157    u128_laws::lemma_obeys_cmp_spec,
158    i128_laws::lemma_obeys_cmp_spec,
159    usize_laws::lemma_obeys_cmp_spec,
160    isize_laws::lemma_obeys_cmp_spec,
161    lemma_ref_obeys_cmp_spec,
162    lemma_option_obeys_cmp_spec,
163}
164
165} // verus!
vstd/laws_cmp.rs

vstd/
laws_cmp.rs
