minerva 0.2.0

//! Algebraic counterexamples for cut and epoch classification.

extern crate alloc;

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

use crate::kairos::Kairos;
use crate::metis::tests::support::dot as d;
use crate::metis::{Anchor, Dot, DotSet, Dotted, Locus, Metatheses, Metathesis, Rhapsody};

use super::super::Note;
use super::super::replica::{Decline, Replica};
use crate::metis::dot::RawDot;

type Text = Dotted<Rhapsody>;
type Moves = Dotted<Metatheses>;
fn rank(physical: u64) -> Kairos {
    Kairos::new(physical, 0, 1, 0u16)
}

fn weave(text: &mut Text, dot: Dot, anchor: Anchor, physical: u64) {
    let mut delta = Rhapsody::new();
    assert!(delta.weave(
        dot,
        Locus {
            anchor,
            rank: rank(physical),
        }
    ));
    text.merge_from(&Dotted::from_store(delta));
}

/// An undotted retraction cannot be classified against an epoch boundary.
///
/// The stability witness ranges over dots. A pure-context retract carries
/// no dot, so "is this removal part of the sealed stratum or of the
/// window?" has no witnessed answer: one replica that folds it below the
/// cut and one that holds it as window traffic both rebuild *valid* strata
/// for the same cut, and the two frozen maps disagree about every later
/// identity of that station. This is the divergence the fleet's
/// dotted-delete duty (a born-dead marker dot beside the superseded
/// target) makes unrepresentable: markers give the witness jurisdiction
/// over removals.
#[test]
fn an_undotted_retraction_cannot_be_classified_at_the_boundary() {
    let mut sealed = Text::new();
    weave(&mut sealed, d(1, 1), Anchor::Origin, 3);
    weave(&mut sealed, d(1, 2), Anchor::Origin, 2);
    weave(&mut sealed, d(1, 3), Anchor::Origin, 1);

    // An in-flight undotted retract of (1, 2): its context names only
    // already-covered dots, so both classifications rebuild lawful strata.
    let mut retract = DotSet::new();
    let _ = retract.insert(d(1, 2));
    let retract = Dotted::<Rhapsody>::from_context(retract);

    let stratum_without = sealed.clone();
    let mut stratum_with = sealed;
    stratum_with.merge_from(&retract);

    let moves = Metatheses::new();
    let map_without = stratum_without
        .store()
        .refound(&moves)
        .expect("a complete stratum folds")
        .map()
        .clone();
    let map_with = stratum_with
        .store()
        .refound(&moves)
        .expect("a complete stratum folds")
        .map()
        .clone();

    // The two replicas froze different identity maps: the second live
    // element lands at different new dots, and the swept element exists in
    // one world only. Every later translation of station 1 now disagrees.
    assert_eq!(map_without.translate(d(1, 3)), Some(d(1, 3)));
    assert_eq!(map_with.translate(d(1, 3)), Some(d(1, 2)));
    assert_eq!(map_without.translate(d(1, 2)), Some(d(1, 2)));
    assert_eq!(
        map_with.translate(d(1, 2)),
        None,
        "the replica that folded the retract swept the identity"
    );
}

/// A witnessed watermark can still refuse the stratum: the cut is a
/// per-station floor, not a causal closure, so a below-cut delete of an
/// above-cut target puts above-cut context into every rebuilt stratum.
/// The refusal is deterministic (every replica rebuilds the same delta
/// set), and the declarer's dry-run turns it from a stuck window into a
/// declined declaration; gossip then raises the watermark past the gap.
#[test]
fn a_witnessed_cut_can_still_refuse_the_stratum() {
    const ROSTER: [u32; 3] = [1, 2, 3];
    let depth = NonZeroUsize::new(2).expect("positive");
    let mut one = Replica::new(1, &ROSTER, depth);
    let mut two = Replica::new(2, &ROSTER, depth);
    let mut three = Replica::new(3, &ROSTER, depth);

    // Station 1 weaves twice; station 2 sees both and deletes the second
    // (a dotted delete whose context names the target); station 3 never
    // sees the second weave, so its floor holds the fleet's watermark
    // below the deleted target while the delete marker itself settles.
    let mut outbox_one = Vec::new();
    let _ = one.insert_visible(0, &mut outbox_one);
    let _ = one.insert_visible(0, &mut outbox_one);
    let mut weaves = outbox_one
        .iter()
        .filter(|note| matches!(note, Note::Old { .. }))
        .cloned();
    let first_weave = weaves.next().expect("first weave note");
    let second_weave = weaves.next().expect("second weave note");

    let mut relay = Vec::new();
    two.handle(&first_weave, &mut relay);
    two.handle(&second_weave, &mut relay);
    let mut outbox_two = Vec::new();
    let deleted = two.delete_visible(0, &mut outbox_two);
    assert_eq!(deleted, Some(d(1, 2)), "station 2 deletes the second weave");

    // Station 3 sees the first weave and the delete, never the second
    // weave; station 1 sees the delete. Every report flows to everyone.
    let mut deliveries: Vec<Note> = Vec::new();
    deliveries.push(first_weave);
    deliveries.extend(
        outbox_one
            .iter()
            .filter(|note| matches!(note, Note::Report { .. }))
            .cloned(),
    );
    deliveries.extend(relay);
    deliveries.extend(outbox_two);
    let mut round = deliveries;
    while !round.is_empty() {
        let mut next = Vec::new();
        for note in &round {
            // The second weave stays undelivered; everything else floods.
            for replica in [&mut one, &mut two, &mut three] {
                let mut out = Vec::new();
                replica.handle(note, &mut out);
                next.extend(out);
            }
        }
        round = next;
    }

    // The watermark now covers the delete marker (2, 1) but not its target
    // (1, 2): a witnessed, gap-free, yet not causally self-supporting cut.
    // The dry-run declines with exactly the offending dot; nothing opened.
    assert_eq!(
        one.try_declare(&mut Vec::new()),
        Err(Decline::NotSelfSupporting { dot: d(1, 2) }),
        "the rebuilt stratum would carry above-cut context"
    );
    assert_eq!(one.epochs().candidates().count(), 0, "no window opened");

    // Delivering the outrun weave raises the watermark; the same declarer
    // now proceeds.
    let mut flood = vec![second_weave];
    while let Some(note) = flood.pop() {
        for replica in [&mut one, &mut two, &mut three] {
            let mut out = Vec::new();
            replica.handle(&note, &mut out);
            flood.extend(out);
        }
    }
    assert!(
        one.try_declare(&mut Vec::new()).is_ok(),
        "the risen watermark is self-supporting"
    );
}

/// The have-set counts event dots, never context spillover.
///
/// A delete delta's context names its superseded target, so a receiver
/// that never delivered the target's weave still *sees* its dot ride past
/// in a context. Folding context dots into the delivered have-set would
/// raise that receiver's floor over the missing weave and forge a fleet
/// watermark covering an element one replica cannot rebuild: its stratum
/// skeleton would lack the tombstone a later element anchors through,
/// while every other replica's stratum carries it, the frozen maps
/// diverge, and the missing-weave replica's own fold refuses what the
/// declarer's dry-run licensed. The envelope therefore names its event
/// dots and the replica counts exactly those. This pin drives the forging
/// schedule and asserts the watermark honestly refuses to rise until the
/// weave itself lands everywhere, after which the fleet crosses the
/// boundary and converges.
#[test]
fn the_have_set_counts_events_never_context_spillover() {
    const ROSTER: [u32; 3] = [1, 2, 3];
    let depth = NonZeroUsize::new(2).expect("positive");
    let mut one = Replica::new(1, &ROSTER, depth);
    let mut two = Replica::new(2, &ROSTER, depth);
    let mut three = Replica::new(3, &ROSTER, depth);

    // Station 1 weaves three elements; the third anchors through the
    // second, so a replica without the second weave must park the third.
    let mut outbox_one = Vec::new();
    let _ = one.insert_visible(0, &mut outbox_one);
    let _ = one.insert_visible(0, &mut outbox_one);
    let _ = one.insert_visible(1, &mut outbox_one);
    let mut weaves = outbox_one
        .iter()
        .filter(|note| matches!(note, Note::Old { .. }))
        .cloned();
    let first_weave = weaves.next().expect("first weave note");
    let second_weave = weaves.next().expect("second weave note");
    let third_weave = weaves.next().expect("third weave note");

    // Station 2 sees the whole document and deletes the second element:
    // the marker's context names (1, 2).
    let mut relay = Vec::new();
    two.handle(&first_weave, &mut relay);
    two.handle(&second_weave, &mut relay);
    two.handle(&third_weave, &mut relay);
    let mut outbox_two = Vec::new();
    let deleted = two.delete_visible(0, &mut outbox_two);
    assert_eq!(deleted, Some(d(1, 2)), "station 2 deletes the second weave");

    // Station 3 sees everything except the second weave; every report and
    // the delete flood to everyone.
    let mut round: Vec<Note> = Vec::new();
    round.push(first_weave);
    round.push(third_weave);
    round.extend(
        outbox_one
            .iter()
            .filter(|note| matches!(note, Note::Report { .. }))
            .cloned(),
    );
    round.extend(relay);
    round.extend(outbox_two);
    while !round.is_empty() {
        let mut next = Vec::new();
        for note in &round {
            for replica in [&mut one, &mut two, &mut three] {
                let mut out = Vec::new();
                replica.handle(note, &mut out);
                next.extend(out);
            }
        }
        round = next;
    }

    // Station 3's have-set saw (1, 2) only as context; counting it would
    // put the fleet watermark at {1: 3, 2: 1} and license the declaration.
    // The honest floor holds at {1: 1}, so the dry-run declines on the
    // delete's above-cut reference, exactly as the discipline demands.
    assert_eq!(
        one.try_declare(&mut Vec::new()),
        Err(Decline::NotSelfSupporting { dot: d(1, 2) }),
        "a context-only sighting must not raise the watermark"
    );

    // The weave lands everywhere; the watermark rises honestly and the
    // fleet crosses the boundary whole.
    let mut flood = vec![second_weave];
    while let Some(note) = flood.pop() {
        for replica in [&mut one, &mut two, &mut three] {
            let mut out = Vec::new();
            replica.handle(&note, &mut out);
            flood.extend(out);
        }
    }
    let mut declare_out = Vec::new();
    let _ = one
        .try_declare(&mut declare_out)
        .expect("the risen watermark is self-supporting");
    let mut round = declare_out;
    while !round.is_empty() {
        let mut next = Vec::new();
        for note in &round {
            for replica in [&mut one, &mut two, &mut three] {
                let mut out = Vec::new();
                replica.handle(note, &mut out);
                next.extend(out);
            }
        }
        round = next;
    }
    for replica in [&one, &two, &three] {
        assert_eq!(
            replica.generation(),
            2,
            "replica {} sealed the boundary",
            replica.id()
        );
    }
    assert_eq!(one.seals, two.seals);
    assert_eq!(one.seals, three.seals);
    assert_eq!(one.text(), two.text());
    assert_eq!(one.text(), three.text());
    assert_eq!(one.effective_order(), two.effective_order());
    assert_eq!(one.effective_order(), three.effective_order());
}

/// An undotted retirement of a *placement-relevant* testimony cannot be
/// classified at an epoch boundary.
///
/// The named consumer's live condense retract is a pure-context supersede
/// of the testimony dots (no marker is minted, and the returned delta is
/// discarded). For an orphaned testimony (its target already excised) that
/// shape happens to be boundary-neutral: an invisible target is swept
/// wholesale by the re-foundation whether or not the retraction folded.
/// But the same undotted shape applied to a testimony whose target is
/// visible at the cut (the recorded future undo path, retracting live
/// testimonies) rebuilds two different strata from identical witnesses:
/// the retraction adds no dot, so both worlds carry the same context and
/// the same cut, yet the surviving move bakes different walk orders and
/// the frozen identity maps disagree on every later dot of the station.
#[test]
fn an_undotted_testimony_retirement_cannot_be_classified_at_the_boundary() {
    let mut sealed = Text::new();
    weave(&mut sealed, d(1, 1), Anchor::Origin, 2);
    weave(&mut sealed, d(1, 2), Anchor::Origin, 1);

    // The testimony moves (1, 1) after (1, 2); both elements stay visible.
    let testimony = Dotted::from_store(Metatheses::singleton(
        d(2, 1),
        Metathesis {
            target: RawDot::new(1, 1),
            to: Locus {
                anchor: Anchor::After(RawDot {
                    station: 1,
                    counter: 2,
                }),
                rank: rank(3),
            },
        },
    ));
    let mut moves_without = Moves::new();
    moves_without.merge_from(&testimony);

    // The in-flight undotted retract: context only, no marker.
    let mut retract = DotSet::new();
    let _ = retract.insert(d(2, 1));
    let retract = Dotted::<Metatheses>::from_context(retract);
    let mut moves_with = moves_without.clone();
    moves_with.merge_from(&retract);

    // The witness cannot tell the two worlds apart: same context, so the
    // same watermark licenses both strata.
    assert_eq!(moves_without.context(), moves_with.context());

    let baked_moved = sealed
        .store()
        .refound(moves_without.store())
        .expect("a complete stratum folds");
    let baked_unmoved = sealed
        .store()
        .refound(moves_with.store())
        .expect("a complete stratum folds");

    // The replica that held the testimony bakes the moved walk; the one
    // that folded the retract bakes the birth walk. The compacted store
    // spells the same numerals either way; the divergence is the frozen
    // map, which now disagrees about every station-1 identity forever: the
    // same old dot denotes different re-founded elements in the two
    // worlds, and every cross-boundary read (duplicate recognition, seal
    // annexes, external references) reads through that map.
    assert_eq!(baked_moved.map().translate(d(1, 1)), Some(d(1, 2)));
    assert_eq!(baked_unmoved.map().translate(d(1, 1)), Some(d(1, 1)));
    assert_eq!(baked_moved.map().translate(d(1, 2)), Some(d(1, 1)));
    assert_eq!(baked_unmoved.map().translate(d(1, 2)), Some(d(1, 2)));
}