minerva 0.2.0

Causal ordering for distributed systems
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

//! Kani proof harnesses for the packed `Kairos` stamp and its wire frame (S86).
//!
//! Compiled only under `cargo kani` (`cfg(kani)`), never in a normal build, test,
//! clippy, or rustdoc pass. Each harness is a *total* proof over the full symbolic
//! input space unless its doc comment says otherwise; the property tests sample
//! these laws, the harnesses discharge them.

use super::{KAIROS_WIRE_LEN, Kairos};

/// Every field written by `new` is read back exactly by its accessor, for all
/// field values: the pack/unpack pair is lossless across the whole space.
#[kani::proof]
fn packing_roundtrips_every_field() {
    let physical: u64 = kani::any();
    let logical: u16 = kani::any();
    let station_id: u32 = kani::any();
    let kairotic: u16 = kani::any();
    let stamp = Kairos::new(physical, logical, station_id, kairotic);
    assert_eq!(stamp.physical(), physical);
    assert_eq!(stamp.logical(), logical);
    assert_eq!(stamp.kairotic(), kairotic);
    assert_eq!(stamp.station_id(), station_id);
}

/// The crate's core invariant, total: the derived `Ord` over the packed `u128`
/// *is* the lexicographic order over `(physical, logical, kairotic, station_id)`,
/// for every pair of stamps. This is the target architecture's "single most
/// important invariant" discharged rather than sampled.
#[kani::proof]
fn order_is_field_lexicographic() {
    let (p_a, l_a, s_a, k_a): (u64, u16, u32, u16) =
        (kani::any(), kani::any(), kani::any(), kani::any());
    let (p_b, l_b, s_b, k_b): (u64, u16, u32, u16) =
        (kani::any(), kani::any(), kani::any(), kani::any());
    let a = Kairos::new(p_a, l_a, s_a, k_a);
    let b = Kairos::new(p_b, l_b, s_b, k_b);
    // The documented significance order: physical, then logical, then the
    // kairotic tag *above* station identity.
    let a_fields = (p_a, l_a, k_a, s_a);
    let b_fields = (p_b, l_b, k_b, s_b);
    assert_eq!(a.cmp(&b), a_fields.cmp(&b_fields));
}

/// PRD 0002 R6, total: decode inverts encode for every stamp.
#[kani::proof]
#[kani::unwind(20)]
fn wire_roundtrip_is_total() {
    let stamp = Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>());
    let decoded = Kairos::from_bytes(&stamp.to_bytes()).unwrap();
    assert_eq!(decoded, stamp);
}

/// PRD 0002 R2, total: byte-wise comparison of two version-1 frames equals the
/// stamp order, so encoded stamps sort causally in a byte-keyed store, for every
/// pair of stamps (not just the sampled ones).
#[kani::proof]
#[kani::unwind(20)]
fn wire_bytes_sort_causally() {
    let a = Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>());
    let b = Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>());
    assert_eq!(a.to_bytes().cmp(&b.to_bytes()), a.cmp(&b));
}

/// Decode totality and byte identity over arbitrary input (bounded only by the
/// harness buffer, which exceeds the fixed frame): `from_bytes` never panics, an
/// accepted input is exactly one canonical frame that re-encodes identically, and
/// every non-frame-length input is rejected.
#[kani::proof]
#[kani::unwind(24)]
fn wire_decode_is_total_and_byte_identical() {
    let bytes: [u8; 20] = kani::any();
    let len: usize = kani::any();
    kani::assume(len <= bytes.len());
    let input = &bytes[..len];
    match Kairos::from_bytes(input) {
        Ok(stamp) => {
            assert_eq!(len, KAIROS_WIRE_LEN);
            let reencoded = stamp.to_bytes();
            assert_eq!(reencoded.as_slice(), input);
        }
        Err(_) => {
            // Rejection is a valid outcome; the assertion is totality (no panic).
        }
    }
    if len != KAIROS_WIRE_LEN {
        assert!(Kairos::from_bytes(input).is_err());
    }
}