minerva 0.2.0

extern crate alloc;

use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;

use crate::metis::{Dot, DotMap, DotSet, Dotted};
use proptest::prelude::*;

/// The document shape: caller keys over bare presence dots (observed-remove).
type Doc = Dotted<DotMap<u8, DotSet>>;

/// The oracle a tape leaves behind, and the fleet it ran over: the live
/// replicas, every minted dot with its key, and the superseded dots.
type Outcome = (Vec<Doc>, BTreeMap<Dot, u8>, BTreeSet<Dot>);

/// The replica fleet size; station ids are `0..=2`.
const REPLICAS: usize = 3;
/// The key domain, kept small so removals and concurrent writes actually collide.
const KEYS: u8 = 3;
/// The per-run op cap: mirrors the fuzz target's slice.
const MAX_OPS: usize = 400;

proptest! {
    /// The always-on twin of the `causal_convergence` fuzz target: a
    /// proptest-generated byte tape, interpreted by the same op-tape logic (the
    /// two copies are kept structurally parallel on purpose, the fuzz target
    /// being the high-volume twin), asserting the same five convergence laws.
    /// This guards the laws under the normal `cargo test` gate at proptest
    /// volume; the fuzz target drives them far deeper.
    #[test]
    fn prop_op_tape_interpreter_matches_the_suite(
        tape in prop::collection::vec(any::<u8>(), 0..512),
    ) {
        let (live, minted, expelled) = interpret(&tape);

        // Law 1: fold-order invariance.
        let forward = live.iter().fold(Doc::new(), |acc, doc| acc.merge(doc));
        let backward = live.iter().rev().fold(Doc::new(), |acc, doc| acc.merge(doc));
        prop_assert_eq!(&forward, &backward);

        // Law 2: the oracle. The fold's store is exactly the never-expelled
        // minted dots under their keys; its context is exactly the minted dots.
        let mut survivors: DotMap<u8, DotSet> = DotMap::new();
        for (&dot, &key) in &minted {
            if expelled.contains(&dot) {
                continue;
            }
            let mut held: DotSet = survivors.get(&key).cloned().unwrap_or_default();
            prop_assert!(held.insert(dot));
            let _ = survivors.insert(key, held);
        }
        prop_assert_eq!(forward.store(), &survivors);
        let mut seen = DotSet::new();
        for &dot in minted.keys() {
            let _ = seen.insert(dot);
        }
        prop_assert_eq!(forward.context(), &seen);

        // Law 3: absorption. The fold merged with each replica is the fold.
        for doc in &live {
            prop_assert_eq!(&forward.merge(doc), &forward);
        }

        // Law 4: the delta theorem, per ordered replica pair.
        for a in &live {
            for b in &live {
                let via_delta = b.merge(&a.delta_for(b.context()));
                let via_full = b.merge(a);
                prop_assert_eq!(via_delta, via_full);
            }
        }

        // Law 5: coveredness. Each replica rebuilt from its own parts is Ok.
        for doc in &live {
            let rebuilt = Dotted::try_new(doc.store().clone(), doc.context().clone());
            prop_assert!(rebuilt.is_ok());
        }
    }
}

/// Interprets a byte tape as ops over a fresh three-replica fleet, returning the
/// replicas and the oracle (minted dots with their key, superseded dots).
///
/// The test-side twin of the fuzz target's `fuzz_target!` body; kept structurally
/// parallel. Bytes are consumed two at a time as `(opcode, argument)`, capped at
/// [`MAX_OPS`]. `opcode % 5` selects the op; the argument's bits select operands.
fn interpret(tape: &[u8]) -> Outcome {
    let mut live: Vec<Doc> = (0..REPLICAS).map(|_| Dotted::new()).collect();
    let mut minted: BTreeMap<Dot, u8> = BTreeMap::new();
    let mut expelled: BTreeSet<Dot> = BTreeSet::new();

    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);
        let key = (argument / 3) % KEYS;
        match opcode % 5 {
            0 => {
                // Add: mint a fresh dot under `key`, merge the singleton delta.
                let station = u32::try_from(replica).unwrap_or(u32::MAX);
                let fresh = live[replica].next_dot(station);
                let mut held = DotSet::new();
                assert!(held.insert(fresh), "a fresh dot is always new");
                let delta = Dotted::from_store(DotMap::singleton(key, held));
                live[replica] = live[replica].merge(&delta);
                let _ = minted.insert(fresh, key);
            }
            1 => {
                // RemoveObserved: supersede the dots held under `key`.
                let observed = live[replica].store().get(&key).cloned().unwrap_or_default();
                for dot in observed.dots() {
                    let _ = expelled.insert(dot);
                }
                let delta: Doc = Dotted::from_context(observed);
                live[replica] = live[replica].merge(&delta);
            }
            2 => {
                // GossipFull: merge the other replica's full state.
                let learned = live[replica].merge(&live[other]);
                live[replica] = learned;
            }
            3 => {
                // GossipDelta: merge exactly what the other replica owes this one.
                let delta = live[other].delta_for(live[replica].context());
                live[replica] = live[replica].merge(&delta);
            }
            _ => {
                // ContextRoundTrip: the have-set wire laws under a semantic state.
                let context = live[replica].context();
                let bytes = context.to_bytes();
                let decoded = DotSet::from_bytes(&bytes).expect("own context frame decodes");
                assert_eq!(
                    decoded.to_bytes(),
                    bytes,
                    "an accepted context frame must re-encode identically"
                );
                assert_eq!(
                    &decoded, context,
                    "the round trip must preserve the context"
                );
            }
        }
    }

    (live, minted, expelled)
}