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
89
90
91
92
93
94
95
96

//! Kani proof harnesses for the chain law (S212, under ruling R-9 as
//! written: heap-free scalar arithmetic over fixed-width values, the
//! packed-stamp proof class; no collection is constructed on any path).
//!
//! These close the chain-ambiguity loop the run program opened. The S197
//! harness proves the codec's `rank_successor` IS the clock fold's frozen
//! -reading send step; the S211 harnesses prove a reservation's members ARE
//! iterated sends. What remained assumed rather than proven was the metis
//! half: that the *inline step spelling* is lossless (a stored step
//! materializes the original locus byte for byte), and that a committed
//! send succession always *chains* under the codec's own predicate (so a
//! run coalesces by arithmetic, never by luck). Together with the sampled
//! twins in the snapshot suite and the identity plane's dual-form property,
//! these are the proof floor of the invariant that chain factoring is
//! layout, never identity: no spelling decision can lose or alter a locus.

use super::super::super::placement::{Anchor, Locus};
use super::{apply_chain_step, chain_step, flatten, pure};
use crate::kairos::Kairos;
use crate::metis::dot::RawDot;

/// A symbolic anchor: origin, after, or before an arbitrary dot.
fn any_anchor() -> Anchor {
    let tag: u8 = kani::any();
    kani::assume(tag < 3);
    match tag {
        0 => Anchor::Origin,
        1 => Anchor::After(RawDot {
            station: kani::any(),
            counter: kani::any(),
        }),
        _ => Anchor::Before(RawDot {
            station: kani::any(),
            counter: kani::any(),
        }),
    }
}

/// A fully symbolic locus.
fn any_locus() -> Locus {
    Locus {
        anchor: any_anchor(),
        rank: Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>()),
    }
}

/// The lossless-spelling law, the no-data-loss core of the inline step:
/// whenever the chain law admits a step between two consecutive-dot loci,
/// applying that step to the predecessor reconstructs the follower EXACTLY
/// (every field: anchor, physical, logical, kairotic, minting station).
/// This is the arithmetic fact the identity plane's stepped slots stand on:
/// a slot that stores `s` instead of a column entry has lost nothing,
/// whatever later splits re-materialize. It also machine-checks the
/// documented safety of `apply_chain_step`'s unchecked physical addition
/// over the step's whole admissible range.
#[kani::proof]
fn chain_step_spelling_is_lossless() {
    let prev_dot: (u32, u64) = (kani::any(), kani::any());
    let prev = any_locus();
    kani::assume(prev_dot.1 < u64::MAX);
    let next_dot = (prev_dot.0, prev_dot.1 + 1);
    let next = any_locus();
    if let Some(step) = chain_step(prev_dot, &prev, next_dot, &next) {
        assert_eq!(
            apply_chain_step(prev_dot, &prev, step),
            next,
            "an admitted step must reconstruct the original locus exactly"
        );
    }
}

/// The mint-to-wire closure: the send-step successor of ANY committed rank
/// always chains under the codec's own predicate, and its spelling is the
/// zero step. With S197 (`rank_successor` is the fold's send step) and
/// S211 (a reservation's members are iterated sends), this proves every
/// reservation member past the head is anchored, ranked, and spelled as
/// one chain interior: coalescing by construction, in the codec's own
/// vocabulary, for the full symbolic space of committed ranks.
#[kani::proof]
fn a_committed_send_succession_always_chains() {
    let prev_dot: (u32, u64) = (kani::any(), kani::any());
    kani::assume(prev_dot.1 < u64::MAX);
    let next_dot = (prev_dot.0, prev_dot.1 + 1);
    let prev = any_locus();
    let next = apply_chain_step(prev_dot, &prev, 0);

    assert!(
        pure::chainable(&flatten(prev_dot, &prev), &flatten(next_dot, &next)),
        "the successor locus must satisfy the codec chain predicate"
    );
    assert_eq!(
        chain_step(prev_dot, &prev, next_dot, &next),
        Some(0),
        "the successor locus must spell as the inline zero step"
    );
}