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

//! Kani harnesses for [`crate::uhlc::NDURU064`] and
//! [`crate::uhlc::HLIDLX16`], both iso Conns. HLIDLX16 proves the
//! all-zero puncture is represented by `None`, while every non-zero
//! byte string round-trips through `Some(ID)`.

use crate::conn::{ConnL, ConnR};
use crate::core::LX;
use crate::prop::conn as conn_laws;
use crate::uhlc::{HLIDLX16, NDURU064};
use core::num::NonZeroU128;
use uhlc::{ID, NTP64};

fn arb_opt_id_symbolic() -> Option<ID> {
    NonZeroU128::new(kani::any()).map(ID::from)
}

mod ndur_u064 {
    use super::*;

    #[kani::proof]
    fn galois_l() {
        let t = NTP64(kani::any());
        let n: u64 = kani::any();
        assert!(conn_laws::galois_l(&NDURU064.view_l(), t, n));
    }

    #[kani::proof]
    fn galois_r() {
        let t = NTP64(kani::any());
        let n: u64 = kani::any();
        assert!(conn_laws::galois_r(&NDURU064.view_r(), t, n));
    }

    #[kani::proof]
    fn iso_roundtrip_l() {
        let t = NTP64(kani::any());
        assert!(conn_laws::iso_roundtrip_l(&NDURU064.view_l(), t));
    }

    #[kani::proof]
    fn floor_le_ceil() {
        let t = NTP64(kani::any());
        assert!(conn_laws::floor_le_ceil(&NDURU064, t));
    }
}

mod hlid_lx16 {
    use super::*;

    #[kani::proof]
    fn galois_l() {
        let a = arb_opt_id_symbolic();
        let bytes: [u8; 16] = kani::any();
        assert!(conn_laws::galois_l(&HLIDLX16.view_l(), a, LX(bytes)));
    }

    #[kani::proof]
    fn galois_r() {
        let a = arb_opt_id_symbolic();
        let bytes: [u8; 16] = kani::any();
        assert!(conn_laws::galois_r(&HLIDLX16.view_r(), a, LX(bytes)));
    }

    #[kani::proof]
    fn iso_roundtrip_l() {
        let a = arb_opt_id_symbolic();
        assert!(conn_laws::iso_roundtrip_l(&HLIDLX16.view_l(), a));
    }

    #[kani::proof]
    fn roundtrip_ceil() {
        let bytes: [u8; 16] = kani::any();
        assert!(conn_laws::roundtrip_ceil(&HLIDLX16.view_l(), LX(bytes)));
    }

    #[kani::proof]
    fn floor_le_ceil() {
        let a = arb_opt_id_symbolic();
        assert!(conn_laws::floor_le_ceil(&HLIDLX16, a));
    }
}