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

//! Kani harnesses for [`crate::uint_uint!`] (`uN → uM` widening) and
//! [`crate::int_uint!`] (`iN → uM` widening / same-width cross-sign).
//! Both are single-sided left-Galois (`pub const Conn<A, B>`) — no
//! triple, no marker struct.
//!
//! Source is a plain primitive (no `Extended<_>` wrapper); Kani's
//! `kani::any::<_>()` handles every primitive integer type natively.

use crate::prop::conn as conn_laws;

/// Five L-Galois harnesses for one `uint_uint!` or `int_uint!` Conn.
macro_rules! prove_uint_widen {
    ($mod_name:ident, $CONN:path, $A:ty, $B:ty) => {
        mod $mod_name {
            use super::*;

            #[kani::proof]
            fn galois_l() {
                let a: $A = kani::any();
                let b: $B = kani::any();
                assert!(conn_laws::galois_l(&$CONN, a, b));
            }

            // `prop::conn::monotone_l` is conditional; unconstrained
            // inputs are sound (see int_narrow.rs for full notes).
            #[kani::proof]
            fn monotone_l() {
                let a1: $A = kani::any();
                let a2: $A = kani::any();
                assert!(conn_laws::monotone_l(&$CONN, a1, a2));
            }

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

            #[kani::proof]
            fn kernel_l() {
                let b: $B = kani::any();
                assert!(conn_laws::kernel_l(&$CONN, b));
            }

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

// Per AGENTS.md `## Conn placement`, U###U### and I###U### widening
// Conns both live in their source module — tie-break rule (2). The
// harnesses below import per-source so the path matches the actual
// hosting after the Plan-26 `core/`/`fixed/` split.

use crate::core::i008 as ci008;
use crate::core::i016 as ci016;
use crate::core::i032 as ci032;
use crate::core::i064 as ci064;
use crate::core::i128 as ci128;
use crate::core::u008 as cu008;
use crate::core::u016 as cu016;
use crate::core::u032 as cu032;
use crate::core::u064 as cu064;

// ── uint_uint! widenings (source-keyed) ─────────────────────────────

prove_uint_widen!(uu_u008u016, cu008::U008U016, u8, u16);
prove_uint_widen!(uu_u008u032, cu008::U008U032, u8, u32);
prove_uint_widen!(uu_u008u064, cu008::U008U064, u8, u64);
prove_uint_widen!(uu_u008u128, cu008::U008U128, u8, u128);

prove_uint_widen!(uu_u016u032, cu016::U016U032, u16, u32);
prove_uint_widen!(uu_u016u064, cu016::U016U064, u16, u64);
prove_uint_widen!(uu_u016u128, cu016::U016U128, u16, u128);

prove_uint_widen!(uu_u032u064, cu032::U032U064, u32, u64);
prove_uint_widen!(uu_u032u128, cu032::U032U128, u32, u128);

prove_uint_widen!(uu_u064u128, cu064::U064U128, u64, u128);

// ── int_uint! widenings (source-keyed) ──────────────────────────────

prove_uint_widen!(iu_i008u008, ci008::I008U008, i8, u8);
prove_uint_widen!(iu_i008u016, ci008::I008U016, i8, u16);
prove_uint_widen!(iu_i008u032, ci008::I008U032, i8, u32);
prove_uint_widen!(iu_i008u064, ci008::I008U064, i8, u64);
prove_uint_widen!(iu_i008u128, ci008::I008U128, i8, u128);

prove_uint_widen!(iu_i016u016, ci016::I016U016, i16, u16);
prove_uint_widen!(iu_i016u032, ci016::I016U032, i16, u32);
prove_uint_widen!(iu_i016u064, ci016::I016U064, i16, u64);
prove_uint_widen!(iu_i016u128, ci016::I016U128, i16, u128);

prove_uint_widen!(iu_i032u032, ci032::I032U032, i32, u32);
prove_uint_widen!(iu_i032u064, ci032::I032U064, i32, u64);
prove_uint_widen!(iu_i032u128, ci032::I032U128, i32, u128);

prove_uint_widen!(iu_i064u064, ci064::I064U064, i64, u64);
prove_uint_widen!(iu_i064u128, ci064::I064U128, i64, u128);

prove_uint_widen!(iu_i128u128, ci128::I128U128, i128, u128);