minerva 0.2.0

//! The replay's foundations, in executable form: the two counterexamples
//! the 2026-07-10 research intakes verified in this crate's exact
//! semantics (S212), and the probe-decoding gadget at the core of the
//! replay-summary bound (S279, ruling R-61, the tenth foundations note:
//! `docs/metis-replay-summary-bound.adoc`). Together they document WHY
//! the recension's convergence foundation is replay determinism and
//! nothing else: the replay outcome is not an optimum any algebra could
//! recompute, it is not composable from independently replayed
//! sub-records, and no exact summary bounded in the live-element count
//! can make it composable, because a counterpart record can read one
//! anchor-choice bit per move of an encoded record back out of the
//! merged visible order, so exact summaries need at least one bit
//! per move. (The intake notes live in `docs/lit-review/`, local and
//! untracked; the theorem's tracked home is the foundations note.)

extern crate alloc;

use alloc::vec::Vec;

use proptest::prelude::*;

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

use super::{Moves, Text, clock, d, move_to};

/// Three origin siblings `a`, `b`, `c`, born in that rank order.
fn three_siblings() -> (Text, Dot, Dot, Dot) {
    let mut text: Text = Composer::new(1);
    let clk = clock(1);
    let mut born = [None; 3];
    for slot in &mut born {
        let rank = clk.now(0u16);
        let (dot, _) = text.compose(|dot| {
            let mut delta = Rhapsody::new();
            assert!(delta.weave(
                dot,
                Locus {
                    anchor: Anchor::Origin,
                    rank,
                }
            ));
            (delta, DotSet::new())
        });
        *slot = Some(dot);
    }
    let [a, b, c] = born.map(|dot| dot.expect("three siblings born"));
    (text, a, b, c)
}

/// The three-move counterexample (verified by hand in the composable-replay
/// intake, RQ1): the replay is an order-dependent FIXED POINT, not a
/// maximum-weight branching. Moves in ascending rank order `m1: b after a`,
/// `m2: c after b`, `m3: a after c`: the replay applies `m1` and `m2` and
/// refuses `m3` as a cycle-former, even though the feasible subset
/// `{m2, m3}` carries the strictly larger rank weight (proven executable
/// here: a record holding only those two applies both). So no
/// Edmonds/Tarjan optimum characterizes the outcome, no summary can
/// recompute it, and undo must be deterministic replay from the record,
/// never an algebraic inverse.
#[test]
fn test_the_replay_is_a_fixed_point_not_an_optimum() {
    let (text, a, b, c) = three_siblings();
    let clk = clock(4);
    let m1_to = Locus {
        anchor: Anchor::After(a.into()),
        rank: clk.now(0u16),
    };
    let m2_to = Locus {
        anchor: Anchor::After(b.into()),
        rank: clk.now(0u16),
    };
    let m3_to = Locus {
        anchor: Anchor::After(c.into()),
        rank: clk.now(0u16),
    };

    // The full record: all three moves.
    let mut moves: Moves = Composer::new(4);
    let _ = move_to(&mut moves, b.into(), m1_to);
    let _ = move_to(&mut moves, c.into(), m2_to);
    let (m3, _) = move_to(&mut moves, a.into(), m3_to);

    let recension = text.state().store().recension(moves.state().store());
    assert_eq!(
        recension.refused(),
        [m3],
        "the heaviest move is refused as a cycle-former"
    );
    assert_eq!(recension.order(), [a, b, c], "the applied chain a > b > c");

    // The heavier feasible subset {m2, m3}: a record holding only those
    // two applies BOTH, so the full replay's outcome is not the
    // maximum-weight feasible subset. The fixed point is the design, and
    // replay determinism is its only convergence foundation.
    let mut heavier: Moves = Composer::new(5);
    let _ = move_to(&mut heavier, c.into(), m2_to);
    let _ = move_to(&mut heavier, a.into(), m3_to);
    let alternative = text.state().store().recension(heavier.state().store());
    assert!(
        alternative.refused().is_empty(),
        "the subset the replay forgoes is feasible on its own"
    );
    assert_eq!(alternative.order(), [b, c, a]);
}

/// The triangle counterexample (the math-correspondences intake): the
/// replay of a merged record is NOT a function of independently replayed
/// sub-records. Moves ranked `m12 < m13 < m23` over origin siblings:
/// stream A `{m12, m23}` applies both; stream B `{m13}` applies; but the
/// UNION applies `{m12, m13}` and refuses `m23`, a verdict no composition
/// of the per-stream survivor sets can produce (their union is the very
/// cycle the merged replay refuses). This is the recorded formal ground
/// for single-record-per-container in stage C's subtree half: merged
/// refusals are not composable from per-container refusals.
#[test]
fn test_per_stream_replays_do_not_compose() {
    let (text, a, b, c) = three_siblings();
    let clk = clock(4);
    let m12_to = Locus {
        anchor: Anchor::After(a.into()),
        rank: clk.now(0u16),
    };
    let m13_to = Locus {
        anchor: Anchor::After(c.into()),
        rank: clk.now(0u16),
    };
    let m23_to = Locus {
        anchor: Anchor::After(b.into()),
        rank: clk.now(0u16),
    };

    // Stream A: {m12: b after a, m23: c after b}. Acyclic; both apply.
    let mut stream_a: Moves = Composer::new(4);
    let _ = move_to(&mut stream_a, b.into(), m12_to);
    let (m23_in_a, _) = move_to(&mut stream_a, c.into(), m23_to);
    let replay_a = text.state().store().recension(stream_a.state().store());
    assert!(replay_a.refused().is_empty());
    assert_eq!(replay_a.order(), [a, b, c]);
    let _ = m23_in_a;

    // Stream B: {m13: a after c}. Applies alone.
    let mut stream_b: Moves = Composer::new(5);
    let _ = move_to(&mut stream_b, a.into(), m13_to);
    let replay_b = text.state().store().recension(stream_b.state().store());
    assert!(replay_b.refused().is_empty());

    // The union record: every per-stream survivor together is the cycle
    // b -> a -> c -> b, so the merged replay must refuse one, and by the
    // fixed rank rule it refuses exactly the LAST (m23), which stream A
    // applied. No function of the two survivor sets alone can know that.
    let mut union: Moves = Composer::new(6);
    let _ = move_to(&mut union, b.into(), m12_to);
    let _ = move_to(&mut union, a.into(), m13_to);
    let (m23, _) = move_to(&mut union, c.into(), m23_to);
    let merged = text.state().store().recension(union.state().store());
    assert_eq!(
        merged.refused(),
        [m23],
        "the merged replay refuses a move both streams' replays would keep"
    );
    assert_eq!(merged.order(), [c, a, b], "the union's fixed point");
}

/// A move rank with a bare physical coordinate: the gadget controls
/// interleaving by construction, so ranks are spelled directly rather
/// than minted (every gadget rank sits far above the three birth ranks).
fn gadget_rank(physical: u64, station: u32) -> Kairos {
    Kairos::new(physical, 0u16, station, 0u16)
}

/// The summary-bound gadget's merged record: the encoded record `A_x`
/// (move `j` re-places `b` after `a` when `x[j]` is false, after `c` when
/// true, at rank `100 + 10j`) with the two-move probe `B_i` interleaved
/// (`p1: a after b` at rank `100 + 10i + 3`, `p2: c after b` at
/// `100 + 10i + 6`). Witness dots: station 4 for the record, station 5
/// for the probe, so the two streams' identities never collide.
fn encoded_record_with_probe(
    x: &[bool],
    probe_at: usize,
    (a, b, c): (Dot, Dot, Dot),
) -> Metatheses {
    let mut merged = Metatheses::new();
    for (j, &bit) in x.iter().enumerate() {
        let anchor = if bit {
            Anchor::After(c.into())
        } else {
            Anchor::After(a.into())
        };
        let witness = d(4, j as u64 + 1);
        assert!(merged.insert(
            witness,
            Metathesis {
                target: b.into(),
                to: Locus {
                    anchor,
                    rank: gadget_rank(100 + 10 * (j as u64 + 1), 4),
                },
            },
        ));
    }
    let probe_base = 100 + 10 * probe_at as u64;
    assert!(merged.insert(
        d(5, 1),
        Metathesis {
            target: a.into(),
            to: Locus {
                anchor: Anchor::After(b.into()),
                rank: gadget_rank(probe_base + 3, 5),
            },
        },
    ));
    assert!(merged.insert(
        d(5, 2),
        Metathesis {
            target: c.into(),
            to: Locus {
                anchor: Anchor::After(b.into()),
                rank: gadget_rank(probe_base + 6, 5),
            },
        },
    ));
    merged
}

/// The replay-summary bound's core step, executable (S279): a counterpart
/// record can DECODE the anchor choice of any chosen move of an encoded
/// record out of the merged visible order, over a fixed
/// three-element skeleton. Move `i` of the encoded
/// record `A_x` re-places one target between two anchors; the two-move
/// probe `B_i` lands just after it in rank and freezes the shape, so the
/// final order is `[a, b, c]` exactly when `x[i]` is false and
/// `[c, b, a]` exactly when true, whatever the other moves say. Decoding
/// every bit of every 3-bit record through its three probes is the
/// exhaustive small case; the property below generalizes the lengths.
///
/// This is why no live-bounded exact summary exists (the theorem in
/// the foundations note): if the merged visible order were
/// computable from a summary of `A_x` plus the counterpart, the
/// summary would determine every probe's outcome, hence every encoded
/// bit; a record of `n` moves needs `n` bits of summary, over three
/// live elements. Exact replay composes across a rank prefix (the
/// sealed-cut state) or across provably disjoint components, never
/// across arbitrary interleaving.
#[test]
fn test_the_probe_decodes_the_record_through_the_merged_replay() {
    let (text, a, b, c) = three_siblings();
    for encoded in 0u8..8 {
        let x: Vec<bool> = (0..3).map(|j| encoded & (1 << j) != 0).collect();
        let mut decoded = Vec::new();
        for i in 1..=3 {
            let merged = encoded_record_with_probe(&x, i, (a, b, c));
            let replay = text.state().store().recension(&merged);
            assert!(replay.pending().is_empty());
            let order = replay.order();
            decoded.push(if order == [a, b, c] {
                false
            } else {
                assert_eq!(
                    order,
                    [c, b, a],
                    "the two probe outcomes are the two chains"
                );
                true
            });
        }
        assert_eq!(
            decoded, x,
            "every bit of the record survives to the outcome"
        );
    }
}

proptest! {
    /// The gadget's law at arbitrary record lengths: for every encoded
    /// record and every probe position, the merged replay's order decodes
    /// exactly the probed move, and the refusal set is exactly the losing
    /// probe half plus the record's later moves on the closed side (the
    /// shape freeze the proof's invariance step claims).
    #[test]
    fn prop_the_probe_decodes_any_position_of_any_record(
        x in prop::collection::vec(any::<bool>(), 1..24),
        pick in any::<prop::sample::Index>(),
    ) {
        let (text, a, b, c) = three_siblings();
        let i = pick.index(x.len()) + 1;
        let merged = encoded_record_with_probe(&x, i, (a, b, c));
        let replay = text.state().store().recension(&merged);
        prop_assert!(replay.pending().is_empty());

        let bit = x[i - 1];
        let expected_order = if bit { [c, b, a] } else { [a, b, c] };
        prop_assert_eq!(replay.order(), expected_order);

        // The refusals, in rank order: the probe half that hit the cycle,
        // then every later record move re-placing `b` toward the side the
        // freeze closed.
        let losing_probe = if bit { d(5, 2) } else { d(5, 1) };
        let mut expected_refusals = alloc::vec![losing_probe];
        for (j, &later) in x.iter().enumerate().skip(i) {
            if later != bit {
                expected_refusals.push(d(4, j as u64 + 1));
            }
        }
        prop_assert_eq!(replay.refused(), expected_refusals.as_slice());
    }
}