minerva 0.2.0

extern crate alloc;

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

use crate::metis::{Composer, Rhapsody};
use proptest::prelude::*;

use super::super::strong_list::OrderLedger;
use super::d;

use self::convergence::assert_convergence;
use self::ops::{
    condense_all, gossip_delta, gossip_full, order_read, retract, weave, weave_before,
};

mod convergence;
mod ops;
mod reference;
mod wire;

use crate::metis::Dot;

/// The replica fleet size; station ids are `1..=3` (0 is not a valid station).
const REPLICAS: usize = 3;
/// The per-run op cap: mirrors the fuzz target's slice.
const MAX_OPS: usize = 400;

/// The fleet a tape leaves behind.
struct Fleet {
    /// The three replica composers over their rhapsodies.
    live: Vec<Composer<Rhapsody>>,
    /// The largest skeleton size each replica reached before any condense.
    peak_skeleton: Vec<usize>,
    /// Every dot any replica has retracted over the whole run.
    ever_removed: BTreeSet<Dot>,
    /// The strong-list oracle's ledger (S288): every visible order the run
    /// observes, whose joint verdict the tape demands at convergence.
    ledger: OrderLedger,
}

proptest! {
    /// The always-on twin of the `rhapsody_convergence` fuzz target: a
    /// proptest-generated byte tape interpreted by the same op-tape logic.
    #[test]
    fn prop_rhapsody_op_tape_interpreter_matches_the_suite(
        tape in prop::collection::vec(any::<u8>(), 0..512),
    ) {
        let _ = interpret(&tape);
    }
}

/// Interprets a byte tape as ops over a fresh three-replica fleet and
/// returns the fleet the tape leaves behind (so directed tests can pin the
/// run's bookkeeping, the ledger's observation count included).
///
/// Bytes are consumed two at a time as `(opcode, argument)`, capped at
/// [`MAX_OPS`]. `opcode % 7` selects the op; the argument's bits select
/// operands. A global monotonic tick supplies each weave's rank, so ranks are
/// distinct and totally ordered across the whole fleet.
fn interpret(tape: &[u8]) -> Fleet {
    let mut fleet = Fleet {
        live: (0..REPLICAS)
            .map(|i| Composer::new(station_of(i)))
            .collect(),
        peak_skeleton: alloc::vec![0usize; REPLICAS],
        ever_removed: BTreeSet::new(),
        ledger: OrderLedger::new(),
    };
    let mut tick: u64 = 0;
    let mut condensed = false;

    for pair in tape.chunks_exact(2).take(MAX_OPS) {
        let opcode = pair[0];
        let argument = pair[1];
        let replica = usize::from(argument % 3);
        let other = usize::from((argument / 3) % 3);

        match opcode % 7 {
            0 => weave(&mut fleet, replica, argument, &mut tick),
            1 => retract(&mut fleet, replica, argument),
            2 => gossip_delta(&mut fleet, replica, other),
            3 => gossip_full(&mut fleet, replica, other),
            4 => {
                condense_all(&mut fleet);
                condensed = true;
            }
            5 => order_read(&mut fleet, replica),
            _ => weave_before(&mut fleet, replica, argument, &mut tick),
        }

        // Until the first condense, the skeleton only grows. After condense,
        // the recorded peak remains an upper bound within the run.
        for i in 0..REPLICAS {
            let now = fleet.live[i].state().store().skeleton_len();
            fleet.peak_skeleton[i] = fleet.peak_skeleton[i].max(now);
            if condensed {
                assert!(
                    now <= fleet.peak_skeleton[i],
                    "the skeleton never grows past its pre-condense peak within a run",
                );
            } else {
                assert_eq!(
                    fleet.peak_skeleton[i], now,
                    "before any condense the skeleton is grow-only",
                );
            }
        }
    }

    assert_convergence(&mut fleet);
    fleet
}

#[test]
fn test_a_directed_tape_drives_every_op_deterministically() {
    // One deterministic pass through every op arm: two after-weaves, two
    // front weave-befores, delta gossip to replica two, a retract there,
    // full gossip back, a condense, and an order read. The index-insertion
    // translation and the strong-list verdict run without sampling, and the
    // observation count pins the ledger's wiring (every op that changes or
    // reads a visible order must feed the oracle): four weaves, one delta
    // gossip, one retract, one full gossip, three condense adoptions, and
    // one order read make eleven; convergence adds its six snapshot
    // pairwise joins and eighteen intermediate post-merge states (the S288
    // review's two findings) plus the converged target: thirty-six.
    let fleet = interpret(&[0, 0, 0, 0, 6, 0, 6, 255, 2, 1, 1, 1, 3, 3, 4, 0, 5, 0]);
    assert_eq!(fleet.ledger.observations(), 36);
    // Station 1 wove (1,1) "A", (1,2) "B", then prepended (1,3) "C" and
    // (1,4) "D"; replica two retracted "C" after the delta gossip, and the
    // full gossip carried the removal back: both participants read D A B
    // (the third replica never gossiped; convergence merges clones).
    for replica in &fleet.live[..2] {
        assert_eq!(replica.state().store().order(), [d(1, 4), d(1, 1), d(1, 2)]);
    }
    assert!(fleet.live[2].state().store().order().is_empty());
}

/// Replica `i` writes as station `i + 1` (0 is not a valid station).
fn station_of(i: usize) -> u32 {
    u32::try_from(i + 1).unwrap_or(u32::MAX)
}