minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

use alloc::vec::Vec;

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

use super::super::{REPLICAS, Seq};

proptest! {
    /// S127: two replicas each build a backward run by repeated insert-before at
    /// a shared boundary (the document start, or after a shared visible element),
    /// and after merging in any fold order each replica's run reads as a
    /// contiguous block. This is the interleaving the single-sided left anchor
    /// suffered (concurrent prepends merging as "xayb"), cured by the Fugue side.
    #[test]
    fn prop_backward_runs_stay_contiguous(
        len1 in 2usize..=6, len2 in 2usize..=6, shared_boundary in any::<bool>(),
    ) {
        // A shared prefix element the two runs prepend before (or the document
        // start when `shared_boundary` is false). Both replicas start from it so
        // the boundary is genuinely shared.
        let station_seed = u32::try_from(REPLICAS + 1).unwrap();
        let seed_clk =
            Clock::with_default_config(TickCounter::new(), station_seed).unwrap();
        let mut base = Seq::new();
        let after = if shared_boundary {
            let dot = base.next_dot(station_seed);
            let locus = Locus { anchor: Anchor::Origin, rank: seed_clk.now(0u16) };
            let mut w = Rhapsody::new();
            prop_assert!(w.weave(dot, locus));
            base = base.merge(&Dotted::from_store(w));
            Some(dot)
        } else {
            None
        };

        // Two replicas, each holding the shared base, build a backward run: each
        // element inserts BEFORE the run's current head (or the boundary), so the
        // run reads in insert order right after the boundary.
        let build_run = |station: u32, len: usize| -> (Seq, Vec<Dot>) {
            let clk = Clock::with_default_config(TickCounter::new(), station).unwrap();
            let mut seq = base.clone();
            let mut run: Vec<Dot> = Vec::new();
            for _ in 0..len {
                let anchor = seq.store().anchor_for_visual_insert(after.map(Into::into));
                if let Some(top) = seq.store().children_of(anchor).next()
                    && let Some(locus) = seq.store().locus(top)
                {
                    clk.observe(locus.rank);
                }
                let dot = seq.next_dot(station);
                let rank = clk.now(0u16);
                let mut w = Rhapsody::new();
                let _ = w.weave(dot, Locus { anchor, rank });
                seq = seq.merge(&Dotted::from_store(w));
                // Insert-before builds the run head-first, so each new element
                // reads at the FRONT of the run: prepend to the running vector.
                run.insert(0, dot);
            }
            (seq, run)
        };
        let (r1, run1) = build_run(1, len1);
        let (r2, run2) = build_run(2, len2);

        // Merge both ways: fold-order independent, and each run contiguous.
        let forward = r1.merge(&r2);
        let backward = r2.merge(&r1);
        prop_assert_eq!(forward.store().order(), backward.store().order());
        let order = forward.store().order();

        let contiguous = |run: &[Dot]| -> bool {
            order.windows(run.len()).any(|w| w == run)
        };
        prop_assert!(contiguous(&run1), "run 1 interleaved: {:?} in {:?}", run1, order);
        prop_assert!(contiguous(&run2), "run 2 interleaved: {:?} in {:?}", run2, order);
    }
}