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
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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191

//! The chain-ambiguity invariant's end-to-end law (S212): chains are
//! LAYOUT, never identity, so no interior edit, split, undo, spelling
//! history, or codec pass may lose or alter a single dot's identity,
//! locus, or relative order. This is the metis no-data-loss statement the
//! shell-discipline note's chain-identity section documents; the arithmetic
//! floor is the chain-law Kani harnesses (`wire/snapshot/proofs.rs`), the
//! canonicity floor is the proven decode core's split-chain refusal, and
//! this property is the sampled roof over the whole store.

extern crate alloc;

use alloc::vec::Vec;
use core::num::NonZeroU32;

use crate::kairos::{Clock, TickCounter};
use crate::metis::{Anchor, Dot, DotSet, Locus, Rhapsody};
use proptest::prelude::*;

use super::{Seq, arb_ops_with_paste, run};

/// One interior-ambiguity action against a run-bearing document: an insert
/// INSIDE an existing chain (the split shape), a span delete starting
/// inside it (the survivor-law shape), or the undo shape (retract of the
/// storm's own most recent insert).
#[derive(Clone, Debug)]
enum Storm {
    InsertInside { pick: usize },
    DeleteSpan { pick: usize, span: usize },
    UndoLastInsert,
}

fn arb_storm() -> impl Strategy<Value = Vec<Storm>> {
    let op = prop_oneof![
        3 => (0usize..64).prop_map(|pick| Storm::InsertInside { pick }),
        2 => (0usize..64, 1usize..9).prop_map(|(pick, span)| Storm::DeleteSpan { pick, span }),
        1 => Just(Storm::UndoLastInsert),
    ];
    prop::collection::vec(op, 0..14)
}

proptest! {
    /// The invariant, sampled whole: after any run-bearing history, any
    /// interior-edit storm (chain splits, span deletes, undo retracts),
    /// and a concurrent fork converged back through BOTH merge forms,
    ///
    /// * every dot ever woven still holds its EXACT original locus (a dot
    ///   names one write, and no split or re-spelling may lose or alter
    ///   it: the no-data-loss core);
    /// * the surviving original elements keep their exact relative order
    ///   (interior inserts interleave, they never permute);
    /// * the value is spelling-independent end to end: the churned store,
    ///   its v2 decode, and its snapshot decode are one value with one
    ///   hash, and both wire forms re-encode byte-identically from the
    ///   freshest spelling (canonical bytes are a function of the value,
    ///   never of the split history).
    #[test]
    fn prop_chain_identity_survives_interior_ambiguity(
        ops in arb_ops_with_paste(),
        storm in arb_storm(),
        fork_inserts in 0usize..4,
    ) {
        let (live, _) = run(&ops);
        let mut state = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let fork = state.clone();

        // The before-record: every woven dot's locus (identity) and the
        // visible order, captured before any ambiguity is introduced.
        let before: Vec<(Dot, Locus)> = state
            .store()
            .woven()
            .dots()
            .map(|dot| {
                let locus = state.store().locus(dot).expect("woven dots have loci");
                (dot, locus)
            })
            .collect();
        let before_order: Vec<Dot> = state.store().order();

        // The storm: interior edits driven through the public write flow,
        // a fresh station-9 clock minting above the incumbent bucket head
        // exactly as an editor would.
        let clock = Clock::with_default_config(TickCounter::new(), 9).unwrap();
        let mut inserted: Vec<Dot> = Vec::new();
        for action in &storm {
            match *action {
                Storm::InsertInside { pick } => {
                    let woven: Vec<Dot> = state.store().woven().dots().collect();
                    if woven.is_empty() {
                        continue;
                    }
                    let anchor = Anchor::After(woven[pick % woven.len()].into());
                    if let Some(top) = state.store().children_of(anchor).next()
                        && let Some(locus) = state.store().locus(top)
                    {
                        clock.observe(locus.rank);
                    }
                    let dot = state.next_dot(9);
                    let rank = clock.now(0u16);
                    let mut delta = Rhapsody::new();
                    let woven_fresh = delta.weave(dot, Locus { anchor, rank });
                    prop_assert!(woven_fresh);
                    state.merge_from(&Seq::from_store(delta));
                    inserted.push(dot);
                }
                Storm::DeleteSpan { pick, span } => {
                    let visible = state.store().order();
                    if visible.is_empty() {
                        continue;
                    }
                    let start = pick % visible.len();
                    let mut superseded = DotSet::new();
                    for &dot in visible.iter().skip(start).take(span) {
                        let _ = superseded.insert(dot);
                    }
                    state.merge_from(&Seq::from_context(superseded));
                }
                Storm::UndoLastInsert => {
                    if let Some(dot) = inserted.pop() {
                        let mut superseded = DotSet::new();
                        let _ = superseded.insert(dot);
                        state.merge_from(&Seq::from_context(superseded));
                    }
                }
            }
        }

        // A concurrent fork pastes its own run inside the document, then
        // converges back through BOTH merge forms (the run arm of the
        // in-place fold under interior ambiguity, against the pure form).
        let mut fork = fork;
        if fork_inserts > 0 {
            let fork_clock =
                Clock::with_default_config(TickCounter::new(), 8).unwrap();
            let len = u32::try_from(fork_inserts).expect("small");
            let reservation = fork_clock.now_run(NonZeroU32::new(len).unwrap(), 0u16);
            let first = fork.next_dot(8);
            let anchor = fork
                .store()
                .order()
                .first()
                .map_or(Anchor::Origin, |&head| Anchor::After(head.into()));
            let mut delta = Rhapsody::new();
            prop_assert!(delta.weave_run(first, anchor, reservation));
            fork.merge_from(&Seq::from_store(delta));
        }
        let pure = state.merge(&fork);
        state.merge_from(&fork);
        prop_assert_eq!(&state, &pure);
        state.store().check_order_thread();

        // 1. No data loss: every original dot keeps its exact locus.
        for &(dot, locus) in &before {
            prop_assert_eq!(
                state.store().locus(dot),
                Some(locus),
                "dot ({}, {}) lost or changed its locus under interior ambiguity",
                dot.station(),
                dot.counter()
            );
        }

        // 2. Surviving originals keep their exact relative order.
        let after_order = state.store().order();
        let originals_after: Vec<Dot> = after_order
            .iter()
            .copied()
            .filter(|dot| before.iter().any(|&(seen, _)| seen == *dot))
            .collect();
        let originals_expected: Vec<Dot> = before_order
            .iter()
            .copied()
            .filter(|&dot| state.store().is_visible(dot))
            .collect();
        prop_assert_eq!(originals_after, originals_expected);

        // 3. Spelling independence, end to end: both codecs round-trip to
        // the same value, and re-encode byte-identically from the fresh
        // spelling the decode built.
        let store = state.store();
        let v2 = store.to_bytes();
        let decoded = Rhapsody::from_bytes(&v2).expect("own encoding decodes");
        prop_assert_eq!(&decoded, store);
        prop_assert_eq!(&decoded.to_bytes(), &v2);
        let snapshot = store.to_snapshot_bytes();
        let resnapped = Rhapsody::from_snapshot_bytes(&snapshot).expect("own snapshot decodes");
        prop_assert_eq!(&resnapped, store);
        prop_assert_eq!(resnapped.to_snapshot_bytes(), snapshot);
        prop_assert_eq!(resnapped.to_bytes(), v2);
        prop_assert_eq!(decoded.order(), store.order());
    }
}