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_spec<T: Ord>() -> bool {
48    &&& obeys_eq_spec::<T>()
49    &&& obeys_cmp_partial_ord::<T>()
50    &&& obeys_cmp_ord::<T>()
51    &&& obeys_partial_cmp_spec_properties::<T>()
52}
53
54macro_rules! num_laws_cmp {
55    ($n: ty, $modname:ident) => {
56        verus! {
57        mod $modname {
58            use super::*;
59
60            pub broadcast proof fn lemma_obeys_cmp_spec()
61                ensures
62                    #[trigger] obeys_cmp_spec::<$n>(),
63            {
64                broadcast use group_laws_eq;
65                reveal(obeys_eq_spec_properties);
66                reveal(obeys_partial_cmp_spec_properties);
67                reveal(obeys_cmp_partial_ord);
68                reveal(obeys_cmp_ord);
69                assert(obeys_eq_spec::<$n>());
70            }
71        }
72        }
73    }
74}
75
76num_laws_cmp!(u8, u8_laws);
77
78num_laws_cmp!(i8, i8_laws);
79
80num_laws_cmp!(u16, u16_laws);
81
82num_laws_cmp!(i16, i16_laws);
83
84num_laws_cmp!(u32, u32_laws);
85
86num_laws_cmp!(i32, i32_laws);
87
88num_laws_cmp!(u64, u64_laws);
89
90num_laws_cmp!(i64, i64_laws);
91
92num_laws_cmp!(u128, u128_laws);
93
94num_laws_cmp!(i128, i128_laws);
95
96num_laws_cmp!(usize, usize_laws);
97
98num_laws_cmp!(isize, isize_laws);
99
100pub broadcast proof fn lemma_option_obeys_cmp_spec<T: Ord>()
101    requires
102        obeys_cmp_spec::<T>(),
103    ensures
104        #[trigger] obeys_cmp_spec::<Option<T>>(),
105{
106    broadcast use lemma_option_obeys_eq_spec;
107
108    assert(obeys_eq_spec::<Option<T>>());
109
110    assert(obeys_cmp_partial_ord::<Option<T>>() && obeys_cmp_ord::<Option<T>>()) by {
111        reveal(obeys_cmp_partial_ord);
112        reveal(obeys_cmp_ord);
113    }
114
115    assert(obeys_partial_cmp_spec_properties::<Option<T>>()) by {
116        reveal(obeys_cmp_partial_ord);
117        reveal(obeys_partial_cmp_spec_properties);
118    }
119}
120
121pub broadcast group group_laws_cmp {
122    u8_laws::lemma_obeys_cmp_spec,
123    i8_laws::lemma_obeys_cmp_spec,
124    u16_laws::lemma_obeys_cmp_spec,
125    i16_laws::lemma_obeys_cmp_spec,
126    u32_laws::lemma_obeys_cmp_spec,
127    i32_laws::lemma_obeys_cmp_spec,
128    u64_laws::lemma_obeys_cmp_spec,
129    i64_laws::lemma_obeys_cmp_spec,
130    u128_laws::lemma_obeys_cmp_spec,
131    i128_laws::lemma_obeys_cmp_spec,
132    usize_laws::lemma_obeys_cmp_spec,
133    isize_laws::lemma_obeys_cmp_spec,
134    lemma_option_obeys_cmp_spec,
135}
136
137} // verus!
vstd/laws_cmp.rs

vstd/
laws_cmp.rs
