connections 0.1.0

Galois connections as first-class values: lawful numeric casts, Q-format / IEEE / time ladders
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

//! Kani harnesses for 1-byte little-endian byte encodings.

use crate::conn::{ConnL, ConnR};
use crate::core::{L2, LE};
use crate::prop::conn as conn_laws;

macro_rules! prove_iso_le {
    ($mod_name:ident, $CONN:path, $T:ty) => {
        mod $mod_name {
            use super::*;

            #[kani::proof]
            fn galois_l() {
                let a: $T = kani::any();
                let b = LE(kani::any::<[u8; 1]>());
                assert!(conn_laws::galois_l(&$CONN.view_l(), a, b));
            }

            #[kani::proof]
            fn galois_r() {
                let a: $T = kani::any();
                let b = LE(kani::any::<[u8; 1]>());
                assert!(conn_laws::galois_r(&$CONN.view_r(), a, b));
            }

            #[kani::proof]
            fn iso_roundtrip_l() {
                let a: $T = kani::any();
                assert!(conn_laws::iso_roundtrip_l(&$CONN.view_l(), a));
            }

            #[kani::proof]
            fn roundtrip_ceil() {
                let b = LE(kani::any::<[u8; 1]>());
                assert!(conn_laws::roundtrip_ceil(&$CONN.view_l(), b));
            }

            #[kani::proof]
            fn floor_le_ceil() {
                let a: $T = kani::any();
                assert!(conn_laws::floor_le_ceil(&$CONN, a));
            }

            #[kani::proof]
            fn order_preserving() {
                let a: $T = kani::any();
                let b: $T = kani::any();
                assert!(a.cmp(&b) == $CONN.ceil(a).cmp(&$CONN.ceil(b)));
            }
        }
    };
}

macro_rules! prove_iso_l2 {
    ($mod_name:ident, $CONN:path, $T:ty) => {
        mod $mod_name {
            use super::*;

            #[kani::proof]
            fn galois_l() {
                let a: $T = kani::any();
                let b = L2(kani::any::<[u8; 1]>());
                assert!(conn_laws::galois_l(&$CONN.view_l(), a, b));
            }

            #[kani::proof]
            fn galois_r() {
                let a: $T = kani::any();
                let b = L2(kani::any::<[u8; 1]>());
                assert!(conn_laws::galois_r(&$CONN.view_r(), a, b));
            }

            #[kani::proof]
            fn iso_roundtrip_l() {
                let a: $T = kani::any();
                assert!(conn_laws::iso_roundtrip_l(&$CONN.view_l(), a));
            }

            #[kani::proof]
            fn roundtrip_ceil() {
                let b = L2(kani::any::<[u8; 1]>());
                assert!(conn_laws::roundtrip_ceil(&$CONN.view_l(), b));
            }

            #[kani::proof]
            fn floor_le_ceil() {
                let a: $T = kani::any();
                assert!(conn_laws::floor_le_ceil(&$CONN, a));
            }

            #[kani::proof]
            fn order_preserving() {
                let a: $T = kani::any();
                let b: $T = kani::any();
                assert!(a.cmp(&b) == $CONN.ceil(a).cmp(&$CONN.ceil(b)));
            }
        }
    };
}

prove_iso_le!(u008_le, crate::core::u008::U008LE01, u8);
prove_iso_l2!(i008_le, crate::core::i008::I008LE01, i8);

mod bool_le {
    use super::*;

    fn any_bool() -> bool {
        let n: u8 = kani::any();
        n != 0
    }

    #[kani::proof]
    fn host_roundtrip_l() {
        let a = any_bool();
        assert!(conn_laws::iso_roundtrip_l(&crate::core::bool::BOOLLE01, a));
    }

    #[kani::proof]
    fn order_preserving() {
        let a = any_bool();
        let b = any_bool();
        assert!(
            a.cmp(&b)
                == crate::core::bool::BOOLLE01
                    .ceil(a)
                    .cmp(&crate::core::bool::BOOLLE01.ceil(b))
        );
    }
}