minerva 0.2.0

//! Span-projection laws (PRD 0021): [`Rhapsody::extent`] against an
//! independent positional oracle, over histories enriched with sided
//! anchors and tombstones, plus the contiguity and sided-expansion laws.

extern crate alloc;

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

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

use super::super::{Record, arb_ops, reference_order, run};
use super::walk::enrich_with_sided_edits;
use crate::metis::dot::RawDot;

/// The oracle's boundary model: every verge mapped to a scalar position
/// against the reference slot order (all reachable dots, tombstones
/// included), slots at even positions, boundaries at odd. `After(slot_i)`
/// and `Before(slot_{i+1})` collide by construction (they bound one gap),
/// and the tie resolves forward exactly when the start is the `After` end
/// of the pair, which is the scan rule said positionally.
fn reference_extent(record: &Record, start: Verge, end: Verge) -> Extent {
    let full = reference_order(&Record {
        woven: record.woven.clone(),
        expelled: BTreeSet::new(),
    });
    let slot_of: BTreeMap<Dot, usize> = full
        .iter()
        .enumerate()
        .map(|(index, &dot)| (dot, index))
        .collect();
    let position = |verge: Verge| -> Option<usize> {
        match verge {
            Verge::Origin => Some(0),
            Verge::Terminus => Some(2 * full.len() + 3),
            // A verge names a raw coordinate, so the crossing to an
            // identity may fail; a non-dot verge simply has no slot and
            // dangles, its pre-existing reading (ruling R-91).
            Verge::Before(dot) => Dot::try_from(dot)
                .ok()
                .and_then(|dot| slot_of.get(&dot))
                .map(|&i| 2 * i + 1),
            Verge::After(dot) => Dot::try_from(dot)
                .ok()
                .and_then(|dot| slot_of.get(&dot))
                .map(|&i| 2 * i + 3),
        }
    };
    let (start_pos, end_pos) = (position(start), position(end));
    let (Some(start_pos), Some(end_pos)) = (start_pos, end_pos) else {
        return Extent::Dangling {
            start: start_pos.is_none(),
            end: end_pos.is_none(),
        };
    };
    if start == end {
        return Extent::Covered(Vec::new());
    }
    let forward = start_pos < end_pos
        || (start_pos == end_pos
            && matches!(start, Verge::After(_))
            && matches!(end, Verge::Before(_)));
    if !forward {
        return Extent::Inverted;
    }
    let covered = full
        .iter()
        .enumerate()
        .filter(|&(index, dot)| {
            let slot_pos = 2 * index + 2;
            start_pos < slot_pos && slot_pos < end_pos && !record.expelled.contains(dot)
        })
        .map(|(_, &dot)| dot)
        .collect();
    Extent::Covered(covered)
}

/// Every verge the oracle and the scan should agree on for this record:
/// the fixed edges, both sides of every woven dot, and both sides of a
/// dot no replica ever minted (the dangling case).
fn all_verges(record: &Record) -> Vec<Verge> {
    let mut verges = alloc::vec![Verge::Origin, Verge::Terminus];
    for &dot in record.woven.keys() {
        verges.push(Verge::Before(dot.into()));
        verges.push(Verge::After(dot.into()));
    }
    verges.push(Verge::Before(RawDot {
        station: 9,
        counter: 1,
    }));
    verges.push(Verge::After(RawDot {
        station: 9,
        counter: 1,
    }));
    verges
}

proptest! {
    /// The projection law: after any enriched history, `extent` agrees with
    /// the independent positional oracle for EVERY pair of verges over the
    /// woven dots, the fixed edges, and a never-minted dot: covered content,
    /// covered emptiness, inversion, and dangling all match, and covered
    /// content is a contiguous interval of `order()`.
    #[test]
    fn prop_extent_agrees_with_the_positional_oracle(
        ops in arb_ops(),
        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);
        let store = seq.store();
        let order = store.order();
        let verges = all_verges(&record);
        for &start in &verges {
            for &end in &verges {
                let got = store.extent(start, end);
                prop_assert_eq!(
                    &got,
                    &reference_extent(&record, start, end),
                    "extent({:?}, {:?}) disagrees with the oracle",
                    start,
                    end,
                );
                // Covered content is a contiguous interval of the document
                // order (never a scatter): the span reads as an editor
                // highlights.
                if let Extent::Covered(covered) = &got
                    && let Some(first) = covered.first()
                {
                    let at = order.iter().position(|dot| dot == first);
                    prop_assert!(at.is_some_and(
                        |i| order[i..i + covered.len()] == covered[..],
                    ));
                }
            }
        }
    }

    /// The sided expansion law (the Peritext expand flags, structurally):
    /// for any placed visible element `d` of any enriched history, a fresh
    /// gap insert at `d`'s caret lands inside a span that starts `After(d)`
    /// and outside one that ends `After(d)`; symmetrically it lands inside
    /// a span that ends `Before(s)` at the successor and outside one that
    /// starts `Before(s)`.
    #[test]
    fn prop_edge_inserts_respect_the_sides(
        ops in arb_ops(),
        caret_pick in 0usize..16,
    ) {
        let (live, mut record) = run(&ops);
        let mut seq = enrich_with_sided_edits(&live, &mut record, &[]);
        let visible = seq.store().order();
        prop_assume!(!visible.is_empty());
        let caret = visible[caret_pick % visible.len()];

        // The documented visual insert at the caret after `d`.
        let station = 9;
        let clk = crate::kairos::Clock::with_default_config(
            crate::kairos::TickCounter::new(),
            station,
        ).unwrap();
        let anchor = seq.store().anchor_for_visual_insert(Some(caret.into()));
        if let Some(top) = seq.store().children_of(anchor).next()
            && let Some(locus) = seq.store().locus(top)
        {
            clk.observe(locus.rank);
        }
        let fresh = seq.next_dot(station);
        let locus = Locus {
            anchor,
            rank: clk.now(0u16),
        };
        let mut delta = Rhapsody::new();
        prop_assert!(delta.weave(fresh, locus));
        seq = seq.merge(&crate::metis::Dotted::from_store(delta));
        let store = seq.store();

        let inside = |extent: &Extent| matches!(
            extent, Extent::Covered(covered) if covered.contains(&fresh),
        );
        // Expanding left edge admits it; non-expanding right edge does not.
        prop_assert!(inside(&store.extent(Verge::After(caret.into()), Verge::Terminus)));
        prop_assert!(!inside(&store.extent(Verge::Origin, Verge::After(caret.into()))));
        // Against the caret's successor (when one exists): an end Before(s)
        // expands over the gap insert; a start Before(s) excludes it.
        let order = store.order();
        let caret_at = order.iter().position(|&dot| dot == caret).unwrap();
        if let Some(&successor) = order.get(caret_at + 2) {
            prop_assert!(inside(
                &store.extent(Verge::After(caret.into()), Verge::Before(successor.into()))
            ));
            prop_assert!(!inside(
                &store.extent(Verge::Before(successor.into()), Verge::Terminus)
            ));
        }
    }
}