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

extern crate alloc;

use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;

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

use super::super::super::d;
use super::super::{REPLICAS, Record, Seq, arb_ops, reference_order, run};

/// The reference in-order walk over ALL reachable dots, visibility ignored:
/// the independent oracle with an empty expelled set, so an order tombstone
/// keeps its slot. Positions every placed element for the suffix law; a dot
/// absent from this sequence has no place in the current order.
fn reference_walk_sequence(woven: &BTreeMap<Dot, Locus>) -> Vec<Dot> {
    reference_order(&Record {
        woven: woven.clone(),
        expelled: BTreeSet::new(),
    })
}

/// Folds the replicas into one converged pair and enriches it through the
/// documented visual-insert flow: each edit places a fresh element at a
/// caret (minting `Before` anchors wherever the caret's successor region is
/// occupied, the sided buckets the base generator never produces) and
/// optionally deletes it, leaving an order tombstone mid-walk. The record
/// tracks every enrichment, so it stays the fold's exact model. Shared with
/// the extent suite (PRD 0021), which pins the span projection over the
/// same enriched histories.
pub(super) fn enrich_with_sided_edits(
    live: &[Seq],
    record: &mut Record,
    edits: &[(usize, bool)],
) -> Seq {
    let station = u32::try_from(REPLICAS + 1).unwrap();
    let clk = Clock::with_default_config(TickCounter::new(), station).unwrap();
    let mut seq = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
    for &(caret_pick, delete_it) in edits {
        let visible = seq.store().order();
        let after = if visible.is_empty() {
            None
        } else {
            Some(visible[caret_pick % visible.len()])
        };
        let anchor = seq.store().anchor_for_visual_insert(after.map(Into::into));
        if let Some(top) = seq.store().children_of(anchor).next()
            && let Some(locus) = seq.store().locus(top)
        {
            clk.observe(locus.rank);
        }
        let dot = seq.next_dot(station);
        let locus = Locus {
            anchor,
            rank: clk.now(0u16),
        };
        let mut rhapsody = Rhapsody::new();
        assert!(rhapsody.weave(dot, locus));
        seq = seq.merge(&Dotted::from_store(rhapsody));
        let _ = record.woven.insert(dot, locus);
        if delete_it {
            let mut ctx = DotSet::new();
            let _ = ctx.insert(dot);
            seq = seq.merge(&Dotted::from_context(ctx));
            let _ = record.expelled.insert(dot);
        }
    }
    seq
}

proptest! {
    /// S183 law: the windowed walk agrees with the order suffix at EVERY
    /// placed element, and refuses every dot with no place. After any history,
    /// enriched with visual inserts (which mint `Before` anchors, the sided
    /// buckets the base generator never produces) and deletions (tombstone
    /// resume points), the fold satisfies, for every woven dot `d`:
    /// `order_walk_after(d)` collects to exactly the visible elements strictly
    /// after `d`'s slot in the independent reference walk when `d` is
    /// reachable, and is `None` when it is not; and the resumability boundary
    /// coincides with `is_reachable`. The lazy whole-document walk is pinned
    /// against the same oracle (`order()` is its collect, so both reads are
    /// covered, over sided buckets here where the C8 law's generator has
    /// none).
    #[test]
    fn prop_order_walk_after_agrees_with_order_suffix(
        ops in arb_ops(),
        edits in prop::collection::vec((0usize..16, any::<bool>()), 0..6),
    ) {
        let (live, mut record) = run(&ops);
        let seq = enrich_with_sided_edits(&live, &mut record, &edits);
        let store = seq.store();

        // The whole-document walk against the independent oracle (the fold
        // holds every recorded locus, so the record is its exact model).
        let lazy: Vec<Dot> = store.order_walk().collect();
        prop_assert_eq!(&lazy, &reference_order(&record));

        // The suffix law at every placed element, and refusal off it.
        let full = reference_walk_sequence(&record.woven);
        let placed: BTreeSet<Dot> = full.iter().copied().collect();
        for &dot in record.woven.keys() {
            let walk = store.order_walk_after(dot);
            prop_assert_eq!(
                store.is_reachable(dot),
                placed.contains(&dot),
                "reachability and the oracle disagree at {:?}", dot
            );
            if placed.contains(&dot) {
                let pos = full.iter().position(|&d| d == dot).unwrap();
                let expected: Vec<Dot> = full[pos + 1..]
                    .iter()
                    .copied()
                    .filter(|&dot| store.is_visible(dot))
                    .collect();
                let Some(iter) = walk else {
                    prop_assert!(false, "a placed element was refused: {:?}", dot);
                    unreachable!()
                };
                let got: Vec<Dot> = iter.collect();
                prop_assert_eq!(got, expected, "suffix mismatch at {:?}", dot);
            } else {
                prop_assert!(walk.is_none(), "an unreachable dot resumed: {:?}", dot);
            }
        }

        // A dot never woven has no place: the fresh-station read refuses.
        // The non-dot counter zero no longer reaches this door --- the
        // identity type carries the law (ruling R-91).
        let fresh_station = u32::try_from(REPLICAS + 2).unwrap();
        prop_assert!(store.order_walk_after(d(fresh_station, u64::MAX)).is_none());
        prop_assert!(Dot::from_parts(fresh_station, 0).is_err());

        // The maintenance law: a replica reached through the in-place fold
        // (S182's `merge_from`, whose `record_locus` maintains the placement
        // set incrementally, in dot order, parking and repairing as anchors
        // land) gives the same placement verdict as the rebuild path at every
        // dot. `Eq` excludes the derived coordinates, so this read-level check
        // is what pins them.
        let mut incremental = Seq::new();
        incremental.merge_from(&seq);
        for &dot in record.woven.keys() {
            prop_assert_eq!(
                incremental.store().is_reachable(dot),
                store.is_reachable(dot),
                "placement maintenance diverged from the rebuild at {:?}", dot
            );
        }
    }
}