minerva 0.2.0

//! The positional-read laws (arc 11 phase three, S200): the order thread's
//! reads against `order()` and the independent oracle, over the same
//! enriched histories the walk law runs, on both maintenance paths (the
//! rebuild the pure merges take and the incremental inserts, flips, and
//! spine descents the in-place fold and the weave path take).

extern crate alloc;

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

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

use super::super::super::d;
use super::super::{Record, Seq, arb_ops_with_paste, reference_order, run};
use super::walk::enrich_with_sided_edits;

/// Every positional law against one settled store: length, forward
/// selection, offsets (visible, tombstone, and refused), and the two
/// reverse walks, each checked against `order()` (the contract form) and
/// the slot-level walk.
fn assert_positional_laws(store: &Rhapsody) -> Result<(), TestCaseError> {
    store.check_order_thread();
    let order = store.order();

    // Length: the root aggregate is order()'s length, never visible_len's
    // (a dangling visible element counts there but holds no place).
    prop_assert_eq!(store.order_len(), order.len());
    prop_assert!(store.visible_len() >= store.order_len());

    // Forward selection: order_at is exactly the indexed read, and out of
    // range is a verdict.
    for (offset, &dot) in order.iter().enumerate() {
        prop_assert_eq!(store.order_at(offset), Some(dot));
        prop_assert_eq!(store.offset_of(dot), Some(offset));
    }
    prop_assert_eq!(store.order_at(order.len()), None);
    prop_assert_eq!(store.order_at(usize::MAX), None);

    // Refusals: every unplaced or unwoven dot has no offset and no reverse
    // resume, mirroring is_reachable (the tombstone-offset law itself runs
    // against the independent oracle in the property body, where the slot
    // sequence is derivable).
    for dot in unplaced_dots(store) {
        prop_assert_eq!(store.offset_of(dot), None);
        prop_assert!(store.order_walk_rev_before(dot).is_none());
    }
    prop_assert_eq!(store.offset_of(d(u32::MAX, u64::MAX)), None);
    // The non-dot counter zero is unrepresentable, so the offset read has
    // no zero arm left to refuse (ruling R-91).
    prop_assert!(Dot::from_parts(1, 0).is_err());

    // The reverse walks: the whole document backward, and the reversed
    // prefix at every placed slot (visible or tombstone), sized exactly.
    let rev: Vec<Dot> = store.order_walk_rev().collect();
    let mut expected = order.clone();
    expected.reverse();
    prop_assert_eq!(&rev, &expected);
    prop_assert_eq!(store.order_walk_rev().len(), order.len());
    for dot in store.woven().dots() {
        let placed = store.is_reachable(dot);
        let walk = store.order_walk_rev_before(dot);
        prop_assert_eq!(placed, walk.is_some());
        if let Some(walk) = walk {
            let boundary = store.offset_of(dot).expect("a placed dot has an offset");
            let mut prefix: Vec<Dot> = order[..boundary].to_vec();
            prefix.reverse();
            let got: Vec<Dot> = walk.collect();
            prop_assert_eq!(got, prefix, "reversed prefix at {:?}", dot);
        }
    }
    Ok(())
}

proptest! {
    /// S200 law: the positional reads agree with `order()` at every offset
    /// and every placed slot, on every maintenance path. After any history
    /// enriched with sided edits and tombstones, the laws hold on the
    /// converged fold (thread built by the pure merge's rebuild), on a
    /// replica reached through the in-place fold (including incremental
    /// repair regions and dynamic endpoint replacement), and on a bare
    /// store woven element by element in walk order (anchors always first,
    /// so every insert runs the incremental position rules: bucket heads,
    /// non-head region descents, and the Before arms, with no rebuild to
    /// hide behind).
    #[test]
    fn prop_positional_reads_agree_with_the_order(
        ops in arb_ops_with_paste(),
        edits in prop::collection::vec((0usize..16, any::<bool>()), 0..6),
    ) {
        let (live, mut record) = run(&ops);
        let seq = enrich_with_sided_edits(&live, &mut record, &edits);
        assert_positional_laws(seq.store())?;

        // The tombstone-offset law, against the independent oracle: the
        // slot sequence is the reference walk with nothing expelled, and
        // every placed slot's offset is the count of visible elements
        // strictly before it, tombstones included.
        let slots = reference_order(&Record {
            woven: record.woven.clone(),
            expelled: BTreeSet::new(),
        });
        let mut visible_before = 0usize;
        for &dot in &slots {
            prop_assert_eq!(
                seq.store().offset_of(dot),
                Some(visible_before),
                "slot offsets agree with the oracle at {:?}",
                dot
            );
            if seq.store().is_visible(dot) {
                visible_before += 1;
            }
        }

        // The in-place fold path, seeded from a POPULATED replica so both
        // settle arms run: a live replica folding the converged state sees
        // genuine expelled residuals (its visible dots the fold
        // supersedes), the arm a from-empty fold can never reach (its
        // visible set is empty, so `expelled` is always empty there; the
        // S200 gate review's coverage finding), beside admitted flips,
        // parks, and repairs.
        let mut incremental = live.first().cloned().unwrap_or_default();
        incremental.merge_from(&seq);
        assert_positional_laws(incremental.store())?;
        prop_assert_eq!(incremental.store().order_len(), seq.store().order_len());
        prop_assert_eq!(incremental.store().order(), seq.store().order());

        // And the from-empty fold (maximal parks and repairs) keeps its
        // own arm.
        let mut fresh = Seq::new();
        fresh.merge_from(&seq);
        assert_positional_laws(fresh.store())?;
        prop_assert_eq!(fresh.store().order_len(), seq.store().order_len());

        // The pure-weave path in walk order (anchors always precede their
        // children, so every insert runs the incremental position rules:
        // bucket heads, non-head region descents, and the Before arms,
        // with no rebuild to hide behind). Everything woven this way is
        // visible, so the thread must read back the full slot sequence.
        let mut bare = Rhapsody::new();
        for &dot in &slots {
            let locus = seq
                .store()
                .locus(dot)
                .expect("a walked slot has a locus");
            prop_assert!(bare.weave(dot, locus));
        }
        bare.check_order_thread();
        prop_assert_eq!(bare.order_len(), slots.len());
        for (offset, &dot) in slots.iter().enumerate() {
            prop_assert_eq!(bare.order_at(offset), Some(dot));
            prop_assert_eq!(bare.offset_of(dot), Some(offset));
        }
        assert_positional_laws(&bare)?;

        // Condense keeps every surviving offset honest: excise what an
        // omniscient claim retires and re-check the laws whole.
        let mut condensed = seq.store().clone();
        let mut retired = crate::metis::DotSet::new();
        for &dot in &record.expelled {
            let _ = retired.insert(dot);
        }
        let _ = condensed.condense(&crate::metis::Retired::trust(retired));
        assert_positional_laws(&condensed)?;
        prop_assert_eq!(condensed.order(), seq.store().order());
    }
}

/// The unplaced dots, read off the placement diagnostic for the refusal
/// arm.
fn unplaced_dots(store: &Rhapsody) -> Vec<Dot> {
    store
        .woven()
        .dots()
        .filter(|&dot| !store.is_reachable(dot))
        .collect()
}