minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

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

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

proptest! {
    /// C7: a visual insert round-trips through `order()` for arbitrary weave
    /// schedules. After any history, pick a caret at each visible position (and
    /// the document start), weave a fresh element at
    /// `anchor_for_visual_insert(after)` with a rank ABOVE `children_of(after)`,
    /// and the new element reads at exactly that slot: immediately after `after`
    /// (or first, when `after` is `None`).
    #[test]
    fn prop_visual_insert_round_trips_through_order(
        ops in arb_ops(), caret_pick in 0usize..16,
    ) {
        let (live, _) = run(&ops);
        // Insert at the last replica (station REPLICAS), a fresh station so its
        // dots are novel and its clock is its own.
        let station = u32::try_from(REPLICAS + 1).unwrap();
        let clk = Clock::with_default_config(TickCounter::new(), station).unwrap();
        let mut seq = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));

        let visible_before = seq.store().order();
        // The caret sits after `after` (None = document start).
        let after = if visible_before.is_empty() {
            None
        } else {
            Some(visible_before[caret_pick % visible_before.len()])
        };
        let anchor = seq.store().anchor_for_visual_insert(after.map(Into::into));
        // Mint a rank above the anchor's current children (the visual-insert
        // rule's rank half): observe the highest-ranked current child, then mint.
        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 locus = Locus { anchor, rank };
        let mut rhapsody = Rhapsody::new();
        prop_assert!(rhapsody.weave(dot, locus));
        seq = seq.merge(&Dotted::from_store(rhapsody));

        // The new element reads at exactly the intended slot.
        let after_order = seq.store().order();
        let idx = after_order.iter().position(|&d| d == dot).unwrap();
        match after {
            None => prop_assert_eq!(idx, 0, "document-start insert reads first"),
            Some(a) => {
                let a_idx = after_order.iter().position(|&d| d == a).unwrap();
                prop_assert_eq!(idx, a_idx + 1, "the insert reads immediately after the caret element");
            }
        }
    }
}