minerva 0.2.0

//! The production re-foundation fold (PRD 0024 stage one).
//!
//! The S215 harness (`epoch_refound/`) pins the boundary semantics on a
//! bounded toy; this suite pins the production fold itself against the
//! recension it bakes: the effective live order survives translation
//! exactly, the new store is born coalesced and floor-perfect, tombstones
//! and swept testimonies do not cross, the map's two halves obey the
//! closed form, and an unsealed stratum is refused rather than guessed at.

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::vec::Vec;

use proptest::prelude::*;

use crate::kairos::{Clock, Kairos, TickCounter};
use crate::metis::{Anchor, Dot, DotSet, Dotted, Locus, Metatheses, Metathesis, Rhapsody};

use super::strong_list::OrderLedger;
use crate::metis::dot::RawDot;

type Seq = Dotted<Rhapsody>;

/// A dot literal, for the pins that spell an identity by hand.
fn d(station: u32, counter: u64) -> Dot {
    Dot::from_parts(station, counter).expect("a test literal names a real dot")
}

fn clock(station: u32) -> Clock<TickCounter> {
    Clock::with_default_config(TickCounter::new(), station).unwrap()
}

/// A one-element rhapsody delta: `dot` woven at `locus`, a covered pair.
fn woven(dot: Dot, locus: Locus) -> Seq {
    let mut rhapsody = Rhapsody::new();
    assert!(rhapsody.weave(dot, locus));
    Dotted::from_store(rhapsody)
}

fn insert(replica: &mut Seq, clk: &Clock<TickCounter>, station: u32, anchor: Anchor) -> Dot {
    let dot = replica.next_dot(station);
    let locus = Locus {
        anchor,
        rank: clk.now(0u16),
    };
    *replica = replica.merge(&woven(dot, locus));
    dot
}

fn delete(replica: &mut Seq, dot: Dot) {
    let mut ctx = DotSet::new();
    assert!(ctx.insert(dot));
    *replica = replica.merge(&Dotted::from_context(ctx));
}

/// The fold laws every refound output owes its input, asserted in one
/// place: order preservation through the map, the per-station compaction
/// image, coalescence-grade recording state, and the tombstone refusal.
fn assert_fold_laws(text: &Rhapsody, moves: &Metatheses) {
    let recension = text.recension(moves);
    let refounded = text.refound(moves).expect("a sealed stratum folds");
    let (store, map) = (refounded.store(), refounded.map());

    // Order preservation: the new order is exactly the effective live
    // order translated, element by element (the walk is visible-only by
    // the `OrderWalk` contract).
    let effective_live: Vec<Dot> = recension.order();
    let translated: Vec<Dot> = effective_live
        .iter()
        .map(|&dot| map.translate(dot).expect("a live dot crosses"))
        .collect();
    assert_eq!(store.order(), translated);
    assert_eq!(map.live_len(), effective_live.len());

    // The compaction image: station `s`'s survivors are exactly
    // `(s, 1..=n_s)`, so the recording have-set is floor-perfect.
    let mut per_station: alloc::collections::BTreeMap<u32, u64> =
        alloc::collections::BTreeMap::new();
    for dot in &effective_live {
        *per_station.entry(dot.station()).or_insert(0) += 1;
    }
    let image: BTreeSet<Dot> = translated.iter().copied().collect();
    assert_eq!(image.len(), translated.len(), "the map is injective");
    for (&station, &count) in &per_station {
        for counter in 1..=count {
            assert!(image.contains(&d(station, counter)));
        }
    }
    assert_eq!(store.woven().hole_count(), 0);
    assert_eq!(store.woven().exceptions_len(), 0);

    // Nothing invisible crossed: every woven dot of the new store is
    // visible, and every old tombstone is refused by the map.
    for dot in store.order() {
        assert!(store.is_visible(dot));
    }
    for dot in text.woven().dots() {
        if !recension.is_visible(dot) {
            assert_eq!(map.translate(dot), None);
        }
    }

    // The affine half: one past each station's ceiling lands one past its
    // compacted range, and consecutive window dots stay consecutive.
    for (&station, &count) in &per_station {
        let ceiling = text.woven().high_water_of(station);
        assert_eq!(
            map.translate(d(station, ceiling + 1)),
            Some(d(station, count + 1))
        );
        assert_eq!(
            map.translate(d(station, ceiling + 2)),
            Some(d(station, count + 2))
        );
    }

    // Determinism: the fold is a pure function of the stratum.
    let twin = text.refound(moves).expect("a sealed stratum folds");
    assert_eq!(twin.store(), store);
    assert_eq!(twin.map(), map);
}

#[test]
fn test_refound_bakes_the_recension_and_sweeps_the_skeleton() {
    let mut replica: Seq = Dotted::new();
    let one = clock(1);
    let two = clock(2);
    let a = insert(&mut replica, &one, 1, Anchor::Origin);
    let b = insert(&mut replica, &one, 1, Anchor::After(a.into()));
    let c = insert(&mut replica, &one, 1, Anchor::After(b.into()));
    let tail = insert(&mut replica, &two, 2, Anchor::After(c.into()));
    delete(&mut replica, b);

    let mut moves = Metatheses::new();
    // Applied: `c` moves directly after `a`.
    assert!(moves.insert(
        d(9, 1),
        Metathesis {
            target: c.into(),
            to: Locus {
                anchor: Anchor::After(a.into()),
                rank: one.now(0u16),
            },
        },
    ));
    // Refused cycle-former: `a` after `c` once `c` hangs off `a`.
    assert!(moves.insert(
        d(9, 2),
        Metathesis {
            target: a.into(),
            to: Locus {
                anchor: Anchor::After(c.into()),
                rank: one.now(0u16),
            },
        },
    ));

    let text = replica.store();
    let recension = text.recension(&moves);
    assert_eq!(recension.refused(), [d(9, 2)]);

    assert_fold_laws(text, &moves);

    // The hard pins: the tombstone does not cross, and the moved element's
    // new position is its baked one (after `a`, before the old successor).
    let refounded = text.refound(&moves).expect("sealed");
    let map = refounded.map();
    assert_eq!(map.translate(b), None);
    let new_a = map.translate(a).expect("live");
    let new_c = map.translate(c).expect("live");
    let new_tail = map.translate(tail).expect("live");
    assert_eq!(refounded.store().order(), [new_a, new_c, new_tail]);
    // Station 1 has ceiling 3 (three mints); its window dot (1, 7) shifts
    // affinely past the two survivors: 2 + (7 - 3) = 6.
    assert_eq!(map.translate(d(1, 7)), Some(d(1, 6)));
}

#[test]
fn test_refound_is_born_coalesced() {
    // One long single-station chain plus a second station's tail: the
    // re-mint must spell the chain inline (explicit locus entries stay at
    // the segment heads), the same economy the snapshot codec factors.
    let mut replica: Seq = Dotted::new();
    let one = clock(1);
    let two = clock(2);
    let mut anchor = Anchor::Origin;
    for _ in 0..6 {
        let dot = insert(&mut replica, &one, 1, anchor);
        anchor = Anchor::After(dot.into());
    }
    for _ in 0..3 {
        let dot = insert(&mut replica, &two, 2, anchor);
        anchor = Anchor::After(dot.into());
    }

    let refounded = replica.store().refound(&Metatheses::new()).expect("sealed");
    assert_eq!(refounded.store().order().len(), 9);
    assert_eq!(
        refounded.store().skeleton_explicit_entries(),
        2,
        "one explicit entry per station segment head"
    );
}

#[test]
fn test_refound_heads_spell_the_fixed_public_rule() {
    // The charter's re-mint rule is public and fixed: a station segment's
    // head anchors after the walk predecessor (Origin at the front) and
    // carries the deterministic per-station base rank, never a rank derived
    // from another station's chain. This is the head-grade spelling the
    // proven consecutiveness contract licenses the fold to skip checking
    // inline, so it is pinned here at the boundary instead.
    let mut replica: Seq = Dotted::new();
    let one = clock(1);
    let two = clock(2);
    let a = insert(&mut replica, &one, 1, Anchor::Origin);
    let b = insert(&mut replica, &one, 1, Anchor::After(a.into()));
    let _c = insert(&mut replica, &two, 2, Anchor::After(b.into()));

    let refounded = replica.store().refound(&Metatheses::new()).expect("sealed");
    let store = refounded.store();

    let head_one = store.locus(d(1, 1)).expect("station 1's head crossed");
    assert_eq!(head_one.anchor, Anchor::Origin);
    assert_eq!(head_one.rank, Kairos::new(0, 0, 1, 0u16));

    let head_two = store.locus(d(2, 1)).expect("station 2's head crossed");
    assert_eq!(
        head_two.anchor,
        Anchor::After(RawDot {
            station: 1,
            counter: 2
        })
    );
    assert_eq!(head_two.rank, Kairos::new(0, 0, 2, 0u16));
}

#[test]
fn test_refound_refuses_an_unsealed_stratum() {
    // A dangling anchor parks its element: no witnessed cut could have
    // produced this state, so the fold refuses with the dot as evidence.
    let mut replica: Seq = Dotted::new();
    let one = clock(1);
    let a = insert(&mut replica, &one, 1, Anchor::Origin);
    let parked = replica.next_dot(1);
    let orphan = Locus {
        anchor: Anchor::After(RawDot {
            station: 1,
            counter: 40,
        }),
        rank: one.now(0u16),
    };
    replica = replica.merge(&woven(parked, orphan));

    let err = replica
        .store()
        .refound(&Metatheses::new())
        .expect_err("an unplaced dot refuses");
    assert_eq!(err.dot, parked);

    // The sealed twin without the orphan folds.
    let mut sealed: Seq = Dotted::new();
    let sealed_a = insert(&mut sealed, &clock(1), 1, Anchor::Origin);
    assert_eq!(sealed_a, a);
    assert!(sealed.store().refound(&Metatheses::new()).is_ok());
}

#[test]
fn test_refound_of_the_empty_store_is_empty_and_affine_is_identity() {
    let refounded = Rhapsody::new().refound(&Metatheses::new()).expect("sealed");
    assert!(refounded.store().order().is_empty());
    assert_eq!(refounded.map().live_len(), 0);
    // A never-woven station's window dots translate identically.
    assert_eq!(refounded.map().translate(d(3, 5)), Some(d(3, 5)));
}

/// Advances a clock past every visible rank of `store` (the receive rule),
/// so the next mint is strictly maximal and post-seal weaves land exactly
/// where they anchor.
fn observe_ranks(clk: &Clock<TickCounter>, store: &Rhapsody) {
    for dot in store.order() {
        if let Some(locus) = store.locus(dot) {
            clk.observe(locus.rank);
        }
    }
}

#[test]
fn test_the_strong_list_order_survives_the_boundary() {
    // The S288 cross-seal arm, insert/delete lane: every order observed
    // across a divergent two-replica execution enters the strong-list
    // ledger, whose verdict proves the final converged order is total on
    // survivors and consistent with every earlier state. That totality is
    // what licenses the boundary hand-off: the next generation's ledger is
    // seeded with the final order renamed through the frozen map (a total
    // order carries every survivor constraint, so nothing is lost at the
    // rename), and post-seal editing must stay consistent with it. This is
    // the specification-grade form of the consignment's opening-read pin.
    let mut ledger = OrderLedger::new();
    let c1 = clock(1);
    let c2 = clock(2);

    let mut base: Seq = Dotted::new();
    let a = insert(&mut base, &c1, 1, Anchor::Origin);
    let b = insert(&mut base, &c1, 1, Anchor::After(a.into()));
    let _ = ledger.observe(&base.store().order());

    // Two divergent replicas over the shared prefix: an append on one, a
    // prepend and a delete on the other.
    let mut left = base.clone();
    let mut right = base.clone();
    let _c = insert(&mut left, &c1, 1, Anchor::After(b.into()));
    let _ = ledger.observe(&left.store().order());
    let d = insert(&mut right, &c2, 2, Anchor::Before(a.into()));
    let _ = ledger.observe(&right.store().order());
    delete(&mut right, b);
    let _ = ledger.observe(&right.store().order());

    let merged = left.merge(&right);
    assert_eq!(merged.store().order(), right.merge(&left).store().order());
    let final_order = merged.store().order();
    let _ = ledger.observe(&final_order);
    let _ = ledger
        .verdict()
        .expect("the pre-seal execution admits one order");
    assert_eq!(final_order.first(), Some(&d));

    // The boundary: refound, then rename the final order through the map.
    let refounded = merged.store().refound(&Metatheses::new()).expect("sealed");
    let (store, map) = refounded.into_parts();
    let renamed: Vec<Dot> = final_order
        .iter()
        .map(|&dot| map.translate(dot).expect("a live dot crosses"))
        .collect();
    assert_eq!(
        store.order(),
        renamed,
        "the opening read is the renamed order"
    );

    // The next generation: seed with the renamed order, keep editing.
    let mut next = OrderLedger::new();
    let _ = next.observe(&renamed);
    let mut reborn: Seq = Dotted::from_store(store);
    let n1 = clock(1);
    observe_ranks(&n1, reborn.store());
    let head = renamed[0];
    let e = insert(&mut reborn, &n1, 1, Anchor::Before(head.into()));
    let _ = next.observe(&reborn.store().order());
    delete(&mut reborn, renamed[1]);
    let _ = next.observe(&reborn.store().order());
    let witness = next
        .verdict()
        .expect("the boundary must not reorder survivors");
    assert_eq!(reborn.store().order().first(), Some(&e));
    assert_eq!(witness.len(), renamed.len() + 1);
}

#[test]
fn test_a_moved_stratum_reopens_consistent() {
    // The S288 cross-seal arm, movement lane. Movement is outside the
    // strong list specification (a metathesis lawfully reorders an
    // existing identity), so the pre-seal ledger deliberately observes
    // only the *effective* order the seal bakes, never the raw states a
    // move straddled; from the boundary on, the renamed baked order is the
    // one order post-seal editing must keep.
    let mut replica: Seq = Dotted::new();
    let one = clock(1);
    let a = insert(&mut replica, &one, 1, Anchor::Origin);
    let b = insert(&mut replica, &one, 1, Anchor::After(a.into()));
    let c = insert(&mut replica, &one, 1, Anchor::After(b.into()));
    let mut moves = Metatheses::new();
    assert!(moves.insert(
        d(9, 1),
        Metathesis {
            target: c.into(),
            to: Locus {
                anchor: Anchor::After(a.into()),
                rank: one.now(0u16),
            },
        },
    ));

    let text = replica.store();
    let effective = text.recension(&moves).order();
    assert_eq!(effective, [a, c, b], "the move bakes");
    let refounded = text.refound(&moves).expect("sealed");
    let (store, map) = refounded.into_parts();
    let renamed: Vec<Dot> = effective
        .iter()
        .map(|&dot| map.translate(dot).expect("a live dot crosses"))
        .collect();

    let mut next = OrderLedger::new();
    let _ = next.observe(&renamed);
    let mut reborn: Seq = Dotted::from_store(store);
    let n1 = clock(1);
    observe_ranks(&n1, reborn.store());
    let end = *renamed.last().expect("three survivors crossed");
    let f = insert(&mut reborn, &n1, 1, Anchor::After(end.into()));
    let _ = next.observe(&reborn.store().order());
    delete(&mut reborn, renamed[1]);
    let _ = next.observe(&reborn.store().order());
    let _ = next
        .verdict()
        .expect("the moved stratum reopens order-consistent");
    assert_eq!(reborn.store().order().last(), Some(&f));
}

// The sampled fold law over generated documents: weaves at woven anchors
// (either side), deletions, and movements (applied, superseded, and
// refused cycles alike), all through the real pair and clocks.

#[derive(Clone, Copy, Debug)]
enum OpSeed {
    Weave { station: u8, anchor: u8, side: bool },
    Delete { target: u8 },
    Move { target: u8, anchor: u8, side: bool },
}

fn run_ops(seeds: &[OpSeed]) -> (Seq, Metatheses) {
    let mut replica: Seq = Dotted::new();
    let clocks = [clock(1), clock(2), clock(3)];
    let mut moves = Metatheses::new();
    let mut dots: Vec<Dot> = Vec::new();
    let mut testimony = 0u64;
    for seed in seeds {
        match *seed {
            OpSeed::Weave {
                station,
                anchor,
                side,
            } => {
                let station = u32::from(station % 3) + 1;
                let slot = usize::from(anchor) % (dots.len() + 1);
                let anchor = if slot == dots.len() {
                    Anchor::Origin
                } else if side {
                    Anchor::Before(dots[slot].into())
                } else {
                    Anchor::After(dots[slot].into())
                };
                let clk = &clocks[station as usize - 1];
                dots.push(insert(&mut replica, clk, station, anchor));
            }
            OpSeed::Delete { target } => {
                if dots.is_empty() {
                    continue;
                }
                delete(&mut replica, dots[usize::from(target) % dots.len()]);
            }
            OpSeed::Move {
                target,
                anchor,
                side,
            } => {
                if dots.is_empty() {
                    continue;
                }
                let target = dots[usize::from(target) % dots.len()];
                let slot = usize::from(anchor) % (dots.len() + 1);
                let to_anchor = if slot == dots.len() {
                    Anchor::Origin
                } else if side {
                    Anchor::Before(dots[slot].into())
                } else {
                    Anchor::After(dots[slot].into())
                };
                testimony += 1;
                assert!(moves.insert(
                    d(9, testimony),
                    Metathesis {
                        target: target.into(),
                        to: Locus {
                            anchor: to_anchor,
                            rank: clocks[0].now(0u16),
                        },
                    },
                ));
            }
        }
    }
    (replica, moves)
}

proptest! {
    #[test]
    fn prop_refound_preserves_the_effective_order(
        seeds in proptest::collection::vec(
            prop_oneof![
                (any::<u8>(), any::<u8>(), any::<bool>()).prop_map(|(station, anchor, side)| {
                    OpSeed::Weave { station, anchor, side }
                }),
                any::<u8>().prop_map(|target| OpSeed::Delete { target }),
                (any::<u8>(), any::<u8>(), any::<bool>()).prop_map(|(target, anchor, side)| {
                    OpSeed::Move { target, anchor, side }
                }),
            ],
            0..14,
        )
    ) {
        let (replica, moves) = run_ops(&seeds);
        assert_fold_laws(replica.store(), &moves);
    }
}