minerva 0.2.0

//! The snapshot-frame suite (PRD 0023): the run-compressed sibling codec's
//! round trips, its agreement with the canonical v2 frame, its compression
//! accounting, the chain law's clock-fold agreement (the sampled twin of
//! the Kani harness), and the shaped canonical-form refusals.

extern crate alloc;

use alloc::vec::Vec;

use crate::kairos::Kairos;
use crate::metis::{Anchor, Dot, Locus, Rhapsody};
use proptest::prelude::*;

use super::d;

mod refusals;

/// One simulated editing step for the honest-typing generator: a station
/// either continues typing where it left off (extending a chain) or seeks
/// somewhere else first (breaking one).
#[derive(Clone, Debug)]
struct Stroke {
    /// Which of the three stations types.
    station_pick: usize,
    /// Whether the station seeks (anchors at the origin) before typing.
    seek: bool,
    /// Whether the stroke hangs on the BEFORE side after a seek.
    before_side: bool,
    /// The clock's physical advance for this stroke; zero freezes the
    /// reading, exercising the logical successor path.
    tick: u64,
}

/// A honest-typing history: per-station consecutive dots, anchors chained
/// AFTER the previous stroke unless the stroke seeks, ranks minted by a
/// simulated Hybrid Logical Clock per station (frozen readings take the
/// logical successor, advances reset it), so the built rhapsodies factor
/// into genuine chain runs with genuine breaks.
fn arb_strokes() -> impl Strategy<Value = Vec<Stroke>> {
    prop::collection::vec(
        (
            0usize..3,
            prop::bool::weighted(0.15),
            any::<bool>(),
            0u64..5000,
        )
            .prop_map(|(station_pick, seek, before_side, tick)| Stroke {
                station_pick,
                seek,
                before_side,
                tick,
            }),
        0..96,
    )
}

/// Builds a rhapsody from a stroke tape, simulating one clock per station
/// (the fold's send arm: a frozen reading bumps the logical, an advance
/// resets it).
fn build_typed(strokes: &[Stroke]) -> Rhapsody {
    let mut rhapsody = Rhapsody::new();
    // Per station: next dot index, last woven dot, clock (physical, logical).
    let mut next_index = [1u64; 3];
    let mut last_dot: [Option<Dot>; 3] = [None; 3];
    let mut clocks = [(0u64, 0u16); 3];
    for stroke in strokes {
        let pick = stroke.station_pick % 3;
        let station = u32::try_from(pick).expect("small pick") + 1;
        let dot = d(station, next_index[pick]);
        next_index[pick] += 1;
        let anchor = match (stroke.seek, last_dot[pick]) {
            (false, Some(previous)) => Anchor::After(previous.into()),
            (true, Some(previous)) if stroke.before_side => Anchor::Before(previous.into()),
            _ => Anchor::Origin,
        };
        let (physical, logical) = clocks[pick];
        let minted = if stroke.tick == 0 {
            // The fold's frozen-reading arm: bump, roll at the sentinel.
            let bumped = logical.saturating_add(1);
            if bumped == u16::MAX {
                (physical.saturating_add(1), 0)
            } else {
                (physical, bumped)
            }
        } else {
            (physical.saturating_add(stroke.tick), 0)
        };
        clocks[pick] = minted;
        let rank = Kairos::new(minted.0, minted.1, station, 0u16);
        assert!(rhapsody.weave(dot, Locus { anchor, rank }));
        last_dot[pick] = Some(dot);
    }
    rhapsody
}

proptest! {
    /// Encode-decode identity over honest-typing histories: the snapshot
    /// frame round-trips the value, and the decoded store equals the v2
    /// frame's decoding of the same value (the two codecs speak one value
    /// space).
    #[test]
    fn prop_snapshot_round_trips_and_agrees_with_v2(strokes in arb_strokes()) {
        let rhapsody = build_typed(&strokes);
        let by_snapshot = Rhapsody::from_snapshot_bytes(&rhapsody.to_snapshot_bytes());
        prop_assert_eq!(by_snapshot, Ok(rhapsody.clone()));
        let by_v2 = Rhapsody::from_bytes(&rhapsody.to_bytes()).expect("v2 round-trips");
        prop_assert_eq!(by_v2, rhapsody);
    }

    /// Decode-encode identity: every accepted snapshot frame re-encodes to
    /// exactly its own bytes, and the prefix decode consumes the whole
    /// frame (the canonical bijection).
    #[test]
    fn prop_snapshot_decode_then_encode_is_identity(strokes in arb_strokes()) {
        let bytes = build_typed(&strokes).to_snapshot_bytes();
        let (decoded, tail) = Rhapsody::from_snapshot_prefix(&bytes).expect("own frame decodes");
        prop_assert!(tail.is_empty());
        prop_assert_eq!(decoded.to_snapshot_bytes(), bytes);
    }

    /// The arbitrary-history generator of the v2 suite (adversarial ranks,
    /// dangling anchors, both sides): the snapshot codec must round-trip
    /// every legal value, chains or none.
    #[test]
    fn prop_snapshot_round_trips_adversarial_histories(
        weaves in super::properties::arb_weaves(),
    ) {
        let rhapsody = super::properties::build(&weaves);
        let bytes = rhapsody.to_snapshot_bytes();
        prop_assert_eq!(rhapsody.snapshot_encoded_len(), bytes.len());
        prop_assert_eq!(Rhapsody::from_snapshot_bytes(&bytes), Ok(rhapsody));
    }

    /// Compression accounting: the snapshot frame never exceeds the v2
    /// frame by more than the four extra header bytes (the second count),
    /// and the more the history chains the more it saves; the deterministic
    /// floor is pinned by example below.
    #[test]
    fn prop_snapshot_never_pays_more_than_the_header(strokes in arb_strokes()) {
        let rhapsody = build_typed(&strokes);
        let snapshot = rhapsody.to_snapshot_bytes();
        prop_assert_eq!(rhapsody.snapshot_encoded_len(), snapshot.len());
        prop_assert!(snapshot.len() <= rhapsody.to_bytes().len() + 4);
    }

    /// The sampled twin of the `snapshot_rank_step_matches_the_clock_fold`
    /// Kani harness, driven through the public clock: minting at a frozen
    /// reading commits exactly the codec's step-zero successor, so the
    /// chain law speaks the clock's own rule (ruling R-25; the proof covers
    /// every pair, this twin keeps the always-on gate).
    #[test]
    fn prop_rank_successor_is_the_clock_frozen_mint(physical in 0u64..1_000_000, mints in 1usize..24) {
        use crate::kairos::{Clock, ClockConfig, VirtualTimeSource};
        let source = VirtualTimeSource::new(physical);
        let clock = Clock::new(source, 7, ClockConfig::default())
            .expect("virtual clock builds");
        let mut last = clock.now(0u16);
        for _ in 0..mints {
            let next = clock.now(0u16);
            let expected = crate::metis::rank_successor(last.physical(), last.logical());
            prop_assert_eq!((next.physical(), next.logical()), expected);
            last = next;
        }
    }
}

/// The logical-rollover arm of the successor rule, deterministically: at
/// the sentinel's edge the frozen mint rolls into the next physical unit,
/// and the codec successor agrees (the arm the sampled twin cannot reach
/// by volume alone).
#[test]
fn test_rank_successor_rolls_over_at_the_sentinel() {
    assert_eq!(
        crate::metis::rank_successor(41, u16::MAX - 2),
        (41, u16::MAX - 1)
    );
    assert_eq!(crate::metis::rank_successor(41, u16::MAX - 1), (42, 0));
    assert_eq!(crate::metis::rank_successor(41, u16::MAX), (42, 0));
    assert_eq!(
        crate::metis::rank_successor(u64::MAX, u16::MAX),
        (u64::MAX, 0)
    );
}

/// The headline number, deterministic: one station typing a 64-element
/// burst (the S192 honest-traffic coalescing unit) costs one 46-byte row
/// plus 63 six-byte steps plus the suffix, against 64 v2 records; the
/// per-locus cost drops from 42 bytes toward 6.7.
#[test]
fn test_a_burst_compresses_toward_the_step_width() {
    let strokes: Vec<Stroke> = (0..64)
        .map(|k| Stroke {
            station_pick: 0,
            seek: false,
            before_side: false,
            tick: if k % 4 == 0 { 0 } else { 50_000_000 },
        })
        .collect();
    let rhapsody = build_typed(&strokes);
    let snapshot = rhapsody.to_snapshot_bytes();
    let v2 = rhapsody.to_bytes();
    // v2: header 5 + one origin record (30) + 63 after records (42 each) +
    // the 21-byte visible suffix (one gap-free station). Snapshot: header 9
    // + one row (46) + 63 six-byte steps + no free loci + the same suffix.
    assert_eq!(v2.len(), 5 + 30 + 63 * 42 + 21);
    assert_eq!(snapshot.len(), 9 + 46 + 63 * 6 + 21);
    // The compression the late-joiner bootstrap buys on this shape.
    assert!(snapshot.len() * 5 < v2.len());
}

/// A tombstoned interior does not break the chain: deletion is causal
/// invisibility, the skeleton keeps every locus, so a churned document's
/// snapshot factors exactly as the untouched one and only the visible
/// suffix differs.
#[test]
fn test_tombstones_ride_inside_runs() {
    use crate::metis::{DotSet, DotStore};
    let strokes: Vec<Stroke> = (0..8)
        .map(|_| Stroke {
            station_pick: 0,
            seek: false,
            before_side: false,
            tick: 1000,
        })
        .collect();
    let rhapsody = build_typed(&strokes);
    // A retract-shaped peer: empty store, context covering the interior
    // three, so the survivor law reads them seen-and-superseded.
    let mut removal_context = DotSet::new();
    for index in [3u64, 4, 5] {
        assert!(removal_context.insert(d(1, index)));
    }
    let self_context = rhapsody.woven().clone();
    let churned = rhapsody.causal_merge(&self_context, &Rhapsody::new(), &removal_context);
    assert_eq!(churned.skeleton_len(), 8);
    assert_eq!(churned.visible_len(), 5);
    let frame = churned.to_snapshot_bytes();
    // Still one chain run and no free loci: the identity plane and its
    // factoring are untouched by visibility.
    assert_eq!(&frame[1..5], &1u32.to_be_bytes());
    assert_eq!(&frame[5..9], &0u32.to_be_bytes());
    assert_eq!(Rhapsody::from_snapshot_bytes(&frame), Ok(churned));
}

/// The S197 gate review's counterexample, pinned: a deleted low dot under a
/// long live run makes the visible suffix dense above a hole (38 dots in a
/// 37-byte have-set frame), which a byte-length suffix budget refuses as the
/// codec's own output. Under the skeleton-cardinality budget the legal value
/// round-trips through BOTH codecs, at any length.
#[test]
fn test_a_deleted_low_dot_survives_the_suffix_budget() {
    use crate::metis::{DotSet, DotStore};
    let strokes: Vec<Stroke> = (0..40)
        .map(|_| Stroke {
            station_pick: 0,
            seek: false,
            before_side: false,
            tick: 1000,
        })
        .collect();
    let rhapsody = build_typed(&strokes);
    let mut removal_context = DotSet::new();
    assert!(removal_context.insert(d(1, 1)));
    let self_context = rhapsody.woven().clone();
    let churned = rhapsody.causal_merge(&self_context, &Rhapsody::new(), &removal_context);
    assert_eq!(churned.skeleton_len(), 40);
    assert_eq!(churned.visible_len(), 39);
    // The suffix alone is smaller than its dot count: the exact shape the
    // byte-length budget refused (the standalone have-set boundary, which
    // deliberately stands, PRD 0016).
    let suffix = {
        let mut visible = DotSet::new();
        for index in 2..=40u64 {
            assert!(visible.insert(d(1, index)));
        }
        visible.to_bytes()
    };
    assert!(DotSet::from_bytes(&suffix).is_err());
    // Both rhapsody codecs round-trip the value regardless: the skeleton
    // vouches for the set.
    assert_eq!(
        Rhapsody::from_snapshot_bytes(&churned.to_snapshot_bytes()).as_ref(),
        Ok(&churned)
    );
    assert_eq!(
        Rhapsody::from_bytes(&churned.to_bytes()).as_ref(),
        Ok(&churned)
    );
}

/// The finding's second arm, pinned: prefix acceptance must not depend on
/// what trails the frame. The same frame decodes identically bare and under
/// an arbitrary tail, and the tail comes back exactly.
#[test]
fn test_prefix_acceptance_is_independent_of_the_tail() {
    use crate::metis::{DotSet, DotStore};
    let strokes: Vec<Stroke> = (0..40)
        .map(|_| Stroke {
            station_pick: 0,
            seek: false,
            before_side: false,
            tick: 1000,
        })
        .collect();
    let rhapsody = build_typed(&strokes);
    let mut removal_context = DotSet::new();
    assert!(removal_context.insert(d(1, 1)));
    let self_context = rhapsody.woven().clone();
    let churned = rhapsody.causal_merge(&self_context, &Rhapsody::new(), &removal_context);
    let frame = churned.to_snapshot_bytes();

    let (bare, bare_tail) = Rhapsody::from_snapshot_prefix(&frame).expect("bare frame decodes");
    assert!(bare_tail.is_empty());

    let mut framed = frame.clone();
    framed.extend_from_slice(&[0xAA; 64]);
    let (tailed, tail) = Rhapsody::from_snapshot_prefix(&framed).expect("tailed frame decodes");
    assert_eq!(tail, &[0xAA; 64]);
    assert_eq!(bare, tailed);

    // The v2 sibling holds the same law.
    let v2 = churned.to_bytes();
    let (v2_bare, _) = Rhapsody::from_prefix(&v2).expect("bare v2 decodes");
    let mut v2_framed = v2;
    v2_framed.extend_from_slice(&[0xAA; 64]);
    let (v2_tailed, v2_tail) = Rhapsody::from_prefix(&v2_framed).expect("tailed v2 decodes");
    assert_eq!(v2_tail, &[0xAA; 64]);
    assert_eq!(v2_bare, v2_tailed);
}

proptest! {
    /// Round trips survive deletion, both codecs: over honest-typing
    /// histories with a generated subset of elements retracted (the survivor
    /// law shrinking visibility under the grow-only skeleton), encode and
    /// decode are still inverse. The generator reaches dense-above-a-hole
    /// visible sets, the shape the S197 gate review proved the byte-budget
    /// suffix refused.
    #[test]
    fn prop_round_trips_survive_deletion(strokes in arb_strokes(), mask in any::<u64>()) {
        use crate::metis::{DotSet, DotStore};
        let rhapsody = build_typed(&strokes);
        let mut removal_context = DotSet::new();
        for (ordinal, dot) in rhapsody.woven().dots().enumerate() {
            if mask & (1 << (ordinal % 64)) != 0 {
                let _ = removal_context.insert(dot);
            }
        }
        let self_context = rhapsody.woven().clone();
        let churned = rhapsody.causal_merge(&self_context, &Rhapsody::new(), &removal_context);
        let by_snapshot = Rhapsody::from_snapshot_bytes(&churned.to_snapshot_bytes());
        prop_assert_eq!(by_snapshot, Ok(churned.clone()));
        let by_v2 = Rhapsody::from_bytes(&churned.to_bytes());
        prop_assert_eq!(by_v2, Ok(churned));
    }

    /// The run-coalesced plane's byte-identity differential (S199, arc 11
    /// phase two; the shell-discipline rule for codec-adjacent shells): a
    /// store churned through retraction and condense holds re-materialized
    /// explicit spellings where an ascending rebuild would step inline, and
    /// the two layouts spell identical bytes on BOTH codecs. The rebuilt
    /// twin comes through decode (`from_parts`, maximal coalescing), so the
    /// comparison is genuinely dual-form, never clone-shared.
    #[test]
    fn prop_wire_bytes_are_spelling_independent(strokes in arb_strokes(), mask in any::<u64>()) {
        use crate::metis::{DotSet, DotStore, Retired};
        let rhapsody = build_typed(&strokes);
        let mut removal_context = DotSet::new();
        for (ordinal, dot) in rhapsody.woven().dots().enumerate() {
            if mask & (1 << (ordinal % 64)) != 0 {
                let _ = removal_context.insert(dot);
            }
        }
        let self_context = rhapsody.woven().clone();
        let mut churned = rhapsody.causal_merge(&self_context, &Rhapsody::new(), &removal_context);
        // Excise what the claim reaches: the plane removals re-materialize
        // stepped followers into explicit entries, the churn under test.
        let _ = churned.condense(&Retired::trust(removal_context));
        let v2 = churned.to_bytes();
        let snapshot = churned.to_snapshot_bytes();
        let rebuilt = Rhapsody::from_bytes(&v2).expect("the canonical frame decodes");
        prop_assert_eq!(&rebuilt, &churned);
        prop_assert_eq!(rebuilt.to_bytes(), v2, "v2 bytes are layout-free");
        prop_assert_eq!(
            rebuilt.to_snapshot_bytes(),
            snapshot,
            "snapshot bytes are layout-free"
        );
    }
}