minerva 0.2.0

//! Shipped-door proofs for the boundary-schedule oath.

extern crate alloc;

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

use crate::metis::{
    Anchor, Cut, EpochPreparation, EpochPreparationFold, EpochPreparationMiss, EpochStratum,
    Epochs, Stability, Vouched,
};

use super::{Moves, Text, d, move_delta, rank, text_delta, vector};
use crate::metis::dot::RawDot;

/// The note's Fact 2, executable: two members' watermarks lag the same
/// monotone truths through different report views and *cross*, so a
/// trailing pair advanced to either member's local meet overshoots a cut
/// declared off the other's, and the shipped base seam refuses it with
/// the exact first offender. First-order watermark-led advancement is
/// unsound in both directions; nothing about the schedule is adversarial.
#[test]
fn the_lag_lemma_crossing_is_executable_and_the_shipped_door_detects_it() {
    // Reporters 2 and 3 over station coordinates 1 and 2. The truths are
    // monotone (F_2 rises (5,9) to (8,9); F_3 rises (9,6) to (9,9));
    // each member holds its own floor fresh and the other's stale.
    let mut tracker_n = Stability::new([2, 3]);
    tracker_n
        .report_cut(2, &Cut::from_witnessed(vector(&[(1, 5), (2, 9)])))
        .unwrap();
    tracker_n
        .report_cut(3, &Cut::from_witnessed(vector(&[(1, 9), (2, 9)])))
        .unwrap();
    let mut tracker_d = Stability::new([2, 3]);
    tracker_d
        .report_cut(2, &Cut::from_witnessed(vector(&[(1, 8), (2, 9)])))
        .unwrap();
    tracker_d
        .report_cut(3, &Cut::from_witnessed(vector(&[(1, 9), (2, 6)])))
        .unwrap();

    let watermark_n = tracker_n.watermark();
    let watermark_d = tracker_d.watermark();
    assert_eq!(watermark_n, vector(&[(1, 5), (2, 9)]));
    assert_eq!(watermark_d, vector(&[(1, 8), (2, 6)]));
    assert!(
        watermark_n.concurrent(&watermark_d),
        "the two local meets cross: neither member's estimate bounds the other's"
    );

    // Member 2 declares off its own meet; member 3's trailing pair,
    // advanced to *its* meet, already reaches (2, 9) above the declared
    // (2, 6), and the base seam names exactly that dot.
    let mut epochs_d = Epochs::new([2, 3], NonZeroUsize::new(1).unwrap());
    let declaration_d = epochs_d
        .declare(d(2, 7), rank(7), &tracker_d, &Cut::bottom())
        .unwrap();
    let trailing_n = Text::from_context(tracker_n.watermark_cut().unwrap().to_have_set());
    assert_eq!(
        EpochPreparation::begin(&declaration_d, trailing_n, Moves::new()).unwrap_err(),
        EpochPreparationMiss::UnpinnedBase {
            dot: RawDot::new(2, 9)
        }
    );

    // And symmetrically: a declaration off member 3's meet is overshot
    // by a pair advanced to member 2's, at station 1 this time.
    let mut epochs_n = Epochs::new([2, 3], NonZeroUsize::new(1).unwrap());
    let declaration_n = epochs_n
        .declare(d(3, 1), rank(1), &tracker_n, &Cut::bottom())
        .unwrap();
    let trailing_d = Text::from_context(tracker_d.watermark_cut().unwrap().to_have_set());
    assert_eq!(
        EpochPreparation::begin(&declaration_n, trailing_d, Moves::new()).unwrap_err(),
        EpochPreparationMiss::UnpinnedBase {
            dot: RawDot::new(1, 8)
        }
    );
}

/// The shared two-station document: four log entries (each annotated
/// with its event dot, the log discipline the classifier rides) beside
/// the converged pairs the eager rebuild folds.
type LogEntries<S> = Vec<((u32, u64), S)>;

fn generation_log() -> (LogEntries<Text>, LogEntries<Moves>, Text, Moves) {
    let text_entries = vec![
        ((1, 1), text_delta(d(1, 1), Anchor::Origin, rank(3))),
        (
            (1, 2),
            text_delta(
                d(1, 2),
                Anchor::After(RawDot {
                    station: 1,
                    counter: 1,
                }),
                rank(5),
            ),
        ),
        (
            (2, 1),
            text_delta(
                d(2, 1),
                Anchor::After(RawDot {
                    station: 1,
                    counter: 1,
                }),
                rank(4),
            ),
        ),
    ];
    let move_entries = vec![((2, 2), move_delta(d(2, 2), (1, 2), rank(9)))];
    let mut text = Text::new();
    for (_, delta) in &text_entries {
        text.merge_from(delta);
    }
    let mut moves = Moves::new();
    for (_, delta) in &move_entries {
        moves.merge_from(delta);
    }
    (text_entries, move_entries, text, moves)
}

/// The oath shape end to end, against the shipped doors: advertisements
/// bound both rivals of a contested window from below, so the trailing
/// base advanced to the oath meet (snapshotted at the candidates'
/// delivery, the note's snapshot rule) seeds one staging per candidate,
/// the winner's staging finishes as the eager rebuild's exact stratum,
/// and the loser's surfaces the typed miss whose cure the schedule
/// already owns.
#[test]
fn a_trailing_base_at_the_oath_meet_serves_every_candidate_of_a_contested_window() {
    let (text_entries, move_entries, text, moves) = generation_log();
    let coverage = text.context().merge(moves.context());
    let boundary = Cut::floor_of(&coverage);
    assert_eq!(boundary.as_vector(), &vector(&[(1, 2), (2, 2)]));

    // Each member advertised an earlier value of its own monotone
    // watermark (emission counters 1; both later declaration dots are
    // minted at counter 3, so the per-emitter fence holds). The oath
    // meet is the trailing frontier: no future declaration by either
    // member may re-found below its own advertisement, so the meet sits
    // below every cut either can still declare.
    let advertised_one = vector(&[(1, 1), (2, 1)]);
    let advertised_two = vector(&[(1, 2), (2, 1)]);
    let oath_meet = advertised_one.meet(&advertised_two);
    assert_eq!(oath_meet, vector(&[(1, 1), (2, 1)]));

    // The trailing base: exactly the log entries the oath meet covers,
    // folded before any declaration exists.
    let mut trailing_text = Text::new();
    let mut trailing_moves = Moves::new();
    for (dot, delta) in &text_entries {
        if dot.1 <= oath_meet.get(dot.0) {
            trailing_text.merge_from(delta);
        }
    }
    for (dot, delta) in &move_entries {
        if dot.1 <= oath_meet.get(dot.0) {
            trailing_moves.merge_from(delta);
        }
    }

    // Two rivals declare at the same witnessed boundary (ranks 1 and 9;
    // the fixed public rule picks station 2). The oath bound holds for
    // both cuts, which is the whole point: the base is committed before
    // anyone knows which rival wins, and it must serve either.
    let mut stability = Stability::new([1, 2]);
    stability.report_cut(1, &boundary).unwrap();
    stability.report_cut(2, &boundary).unwrap();
    let mut epochs = Epochs::new([1, 2], NonZeroUsize::new(1).unwrap());
    let losing = epochs
        .declare(d(1, 3), rank(1), &stability, &Cut::bottom())
        .unwrap();
    let mut rival = Epochs::new([1, 2], NonZeroUsize::new(1).unwrap());
    let winning = rival
        .declare(d(2, 3), rank(9), &stability, &Cut::bottom())
        .unwrap();
    epochs
        .deliver(winning.clone(), &stability, &Cut::bottom())
        .unwrap();
    assert!(&oath_meet <= losing.cut().as_vector());
    assert!(&oath_meet <= winning.cut().as_vector());

    // One staging per candidate, both seeded from the frozen base; the
    // whole log absorbs into each (already-folded entries join
    // idempotently, above-cut entries would classify window-side).
    let mut stage_losing =
        EpochPreparation::begin(&losing, trailing_text.clone(), trailing_moves.clone())
            .expect("the oath meet sits below the losing candidate's cut");
    let mut stage_winning = EpochPreparation::begin(&winning, trailing_text, trailing_moves)
        .expect("the oath meet sits below the winning candidate's cut");
    for (dot, delta) in &text_entries {
        assert_eq!(
            stage_losing.absorb_text(&[(*dot).into()], delta),
            EpochPreparationFold::Staged
        );
        assert_eq!(
            stage_winning.absorb_text(&[(*dot).into()], delta),
            EpochPreparationFold::Staged
        );
    }
    for (dot, delta) in &move_entries {
        assert_eq!(
            stage_losing.absorb_moves(&[(*dot).into()], delta),
            EpochPreparationFold::Staged
        );
        assert_eq!(
            stage_winning.absorb_moves(&[(*dot).into()], delta),
            EpochPreparationFold::Staged
        );
    }

    // The rounds fix the rank-9 rival; the winner's staging is the
    // rebuild's exact stratum, the loser's is the typed miss.
    let mut delivered = boundary.as_vector().clone();
    delivered.observe(1, 3);
    delivered.observe(2, 3);
    let delivered = Cut::from_witnessed(delivered);
    stability.report_cut(1, &delivered).unwrap();
    stability.report_cut(2, &delivered).unwrap();
    epochs
        .confirm(losing.address(), &Vouched::trust(1, delivered.clone()))
        .unwrap();
    epochs
        .confirm(losing.address(), &Vouched::trust(2, delivered.clone()))
        .unwrap();
    let adopted = epochs
        .adopt(1, delivered.as_vector().get(1), &stability)
        .unwrap();
    assert_eq!(adopted.address(), winning.address());

    let staged = stage_winning
        .finish(&adopted)
        .expect("the staged winner is the adopted winner");
    let control = EpochStratum::new(&adopted, text, moves).unwrap();
    assert_eq!(staged.pristine(), control.pristine());
    assert_eq!(
        stage_losing.finish(&adopted).unwrap_err(),
        EpochPreparationMiss::DifferentWinner {
            staged: losing.address(),
            adopted: adopted.address(),
        }
    );
}

/// The fence is necessary: deliver one post-declaration advertisement
/// ahead of its declaration (no transport law grants that order, the
/// S282 second review finding) and the oath meet overshoots the
/// declared cut. The violation is exactly detectable before any fold
/// is trusted: the held advertisement's own-station stamp has reached
/// the declaration's dot count, and the shipped base seam concurs
/// after the fact with the same first offender the stamp fence names
/// in advance.
#[test]
fn a_reordered_advertisement_overshoots_and_the_counter_fence_names_it() {
    // Station 2's honest emission order: advertise (own-station stamp
    // 1), declare (dot count 3, minted above every earlier stamp),
    // advertise again (stamp 4, above the declared cut, lawful once
    // the declaration is out). Station 1 advertised high and stays
    // silent.
    let advertised_early = vector(&[(1, 1), (2, 1)]);
    let advertised_late = vector(&[(1, 4), (2, 4)]);
    let late_counter: u64 = 4;
    let advertised_other = vector(&[(1, 9), (2, 9)]);

    let mut stability = Stability::new([1, 2]);
    let declared = Cut::from_witnessed(vector(&[(1, 2), (2, 2)]));
    stability.report_cut(1, &declared).unwrap();
    stability.report_cut(2, &declared).unwrap();
    let mut epochs = Epochs::new([1, 2], NonZeroUsize::new(1).unwrap());
    let declaration = epochs
        .declare(d(2, 3), rank(3), &stability, &Cut::bottom())
        .unwrap();

    // In emission order the oath meet is bounded by the early
    // advertisement and stays below the cut.
    let fenced_meet = advertised_early.meet(&advertised_other);
    assert!(&fenced_meet <= declaration.cut().as_vector());

    // Reordered, the late advertisement folds first and the meet rises
    // strictly past the cut: a trailing pair advanced to it is unusable
    // for this boundary, and the base seam says so with the first
    // offender.
    let broken_meet = advertised_early
        .merge(&advertised_late)
        .meet(&advertised_other);
    assert!(declaration.cut().as_vector().happens_before(&broken_meet));
    let trailing = Text::from_context(Cut::from_witnessed(broken_meet).to_have_set());
    assert_eq!(
        EpochPreparation::begin(&declaration, trailing, Moves::new()).unwrap_err(),
        EpochPreparationMiss::UnpinnedBase {
            dot: RawDot::new(1, 4)
        }
    );

    // The counter fence detects the broken schedule *before* the fold:
    // an advertisement at or past the declaration's own emission
    // counter cannot have preceded it at the emitter.
    assert!(late_counter >= declaration.dot().counter());
}

/// The generation hazard (the S282 review finding): a seal resets the
/// stability rounds and the compacted plane *reuses counter numerals*
/// (PRD 0024), so an advertisement surviving from an older generation
/// is no lower bound on new-generation declarations, and the counter
/// fence is generation-blind (a mature window's first advertisement
/// carries a low counter over high numerals). Only the generation
/// discipline stands in the way: the oath table resets at seal exactly
/// as `Stability` does, and a stale-generation advertisement is
/// excluded before folding, the same tag exclusion every other
/// lifecycle record already obeys.
#[test]
fn a_stale_generation_advertisement_is_excluded_before_it_can_overshoot() {
    // A mature old generation: every member's *first* advertisement of
    // that window already carried high numerals over low emission
    // counters.
    let stale_advertised = vector(&[(1, 9), (2, 9)]);
    let stale_counter: u64 = 1;

    // After the seal the reborn coordinate space counts from the
    // bottom again: the next generation's declaration is minted at
    // small counts.
    let mut stability = Stability::new([1, 2]);
    let reborn = Cut::from_witnessed(vector(&[(1, 1), (2, 1)]));
    stability.report_cut(1, &reborn).unwrap();
    stability.report_cut(2, &reborn).unwrap();
    let mut epochs = Epochs::new([1, 2], NonZeroUsize::new(1).unwrap());
    let declaration = epochs
        .declare(d(2, 2), rank(2), &stability, &Cut::bottom())
        .unwrap();

    // The counter fence passes (1 is below the declaration's own
    // emission count): it cannot see generations, so it is not the
    // exclusion here.
    assert!(stale_counter < declaration.dot().counter());

    // An oath table that survived the seal unreset holds only stale
    // slots; their meet overshoots the reborn cut, and a trailing pair
    // advanced to it is refused by the base seam with the first
    // offender. The reset plus the stale-tag exclusion are what keep
    // this schedule unreachable.
    let poisoned_meet = stale_advertised.meet(&stale_advertised);
    assert!(declaration.cut().as_vector().happens_before(&poisoned_meet));
    let trailing = Text::from_context(Cut::from_witnessed(poisoned_meet).to_have_set());
    assert_eq!(
        EpochPreparation::begin(&declaration, trailing, Moves::new()).unwrap_err(),
        EpochPreparationMiss::UnpinnedBase {
            dot: RawDot::new(1, 9)
        }
    );

    // With the discipline, the reborn table reads bottom until every
    // member re-advertises inside the new generation, and the fresh
    // family's meet sits below the reborn cut.
    let fresh_one = vector(&[(1, 1), (2, 0)]);
    let fresh_two = vector(&[(1, 0), (2, 1)]);
    let fresh_meet = fresh_one.meet(&fresh_two);
    assert!(&fresh_meet <= declaration.cut().as_vector());
    let trailing = Text::from_context(Cut::from_witnessed(fresh_meet).to_have_set());
    let staging = EpochPreparation::begin(&declaration, trailing, Moves::new());
    assert!(staging.is_ok());
}