minerva 0.2.0

//! The strong-list oracle (S288, ruling R-70): the order core of the Attiya
//! et al. strong list specification as an independent, implementation-blind
//! checker over *observed executions*.
//!
//! The standing rhapsody suites check implementation agreement (the
//! maintained walk against an independent re-derivation of the same
//! semantics) and convergence (one order at every replica after gossip).
//! Neither checks the *specification*: that one global total order exists
//! which every list state ever observed, at any replica and any time, reads
//! as a subsequence of. That is the strong list specification's load-bearing
//! clause (Attiya, Burckhardt, Gotsman, Morrison, Yang, Zawirski,
//! "Specification and Complexity of Collaborative Text Editing", PODC 2016),
//! the clause that separates it from the weak specification, whose anomalies
//! are only visible *across* states.
//!
//! The oracle is deliberately blind to the implementation: it sees no
//! anchors, no ranks, no skeleton, no tombstones, only sequences of element
//! identities (dots). An [`OrderLedger`] accumulates every observed visible
//! order; each state contributes its consecutive pairs as constraints (the
//! consecutive pairs of a sequence generate its whole order by transitivity,
//! and the transitive closure of an acyclic union stays acyclic, so
//! consecutive pairs are exactly enough). The [`OrderLedger::verdict`] then
//! either produces a witness total order (a topological order of the
//! constraint graph, which every observed state embeds into as a
//! subsequence) or refuses with a [`Contradiction`]: a cycle of elements,
//! each step naming the first observation that contributed it, so a
//! violation carries its evidence in the house style.
//!
//! Scope, stated exactly:
//!
//! * The oracle covers the specification's *order* half over the
//!   insert/delete surface (weaves, retracts, condense, gossip). Set
//!   faithfulness (that a state shows exactly the visible elements) is
//!   owned by the standing convergence and reference suites; movement
//!   (PRD 0022) is deliberately outside, because a metathesis lawfully
//!   reorders an existing identity and no single execution-wide order can
//!   or should embed states straddling one. Across an epoch boundary the
//!   oracle composes by renaming (the cross-seal arm in `tests/refound.rs`).
//! * Strong-list is *not* non-interleaving: an execution whose runs
//!   interleave block-wise can still satisfy the specification, so the
//!   `FugueMax` corner recorded as PRD 0018 R6 stays a residual this oracle
//!   deliberately does not judge (the exhibit in `examples.rs` pins that
//!   scoping executable).

extern crate alloc;

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

mod examples;

use super::support::dot;
use crate::metis::Dot;

/// The refusal evidence: a directed cycle of constraints no total order can
/// satisfy, each step tagged with the observation that first contributed it.
#[derive(Clone, Debug, PartialEq, Eq)]
pub(super) struct Contradiction {
    /// The cycle in edge direction: `cycle[j]` is constrained before
    /// `cycle[j + 1]`, and the last element before the first.
    pub(super) cycle: Vec<Dot>,
    /// Per step, the index of the first observation that recorded the
    /// constraint (`witnesses[j]` grounds the `cycle[j]` step; the last
    /// entry grounds the wrap-around step).
    pub(super) witnesses: Vec<usize>,
}

/// The execution-order ledger: every element ever observed, and every
/// adjacent-pair constraint any observed state has asserted.
#[derive(Clone, Debug, Default)]
pub(super) struct OrderLedger {
    /// Every element that has appeared in an observation.
    nodes: BTreeSet<Dot>,
    /// Directed constraints `u` before `v`, tagged with the first
    /// observation that contributed them.
    edges: BTreeMap<(Dot, Dot), usize>,
    /// How many states have been observed.
    observations: usize,
}

impl OrderLedger {
    /// An empty ledger.
    pub(super) const fn new() -> Self {
        Self {
            nodes: BTreeSet::new(),
            edges: BTreeMap::new(),
            observations: 0,
        }
    }

    /// Records one observed visible order and returns its observation index.
    ///
    /// Every element enters the node set; every adjacent pair enters the
    /// constraint set (first observation wins the tag, later duplicates
    /// change nothing).
    pub(super) fn observe(&mut self, state: &[Dot]) -> usize {
        let index = self.observations;
        for &dot in state {
            let _ = self.nodes.insert(dot);
        }
        for pair in state.windows(2) {
            let _ = self.edges.entry((pair[0], pair[1])).or_insert(index);
        }
        self.observations += 1;
        index
    }

    /// How many states this ledger has observed.
    pub(super) const fn observations(&self) -> usize {
        self.observations
    }

    /// The specification verdict.
    ///
    /// `Ok` carries a witness: one total order (deterministic, the
    /// least-element Kahn linearization) that extends every recorded
    /// constraint, so every observed state reads as a subsequence of it.
    /// `Err` carries a [`Contradiction`]: a constraint cycle with the
    /// observation that grounds each step.
    ///
    /// # Errors
    ///
    /// Refuses exactly when the observed states admit no single total
    /// order, the strong list specification's order clause.
    pub(super) fn verdict(&self) -> Result<Vec<Dot>, Contradiction> {
        let mut incoming: BTreeMap<Dot, usize> = self.nodes.iter().map(|&n| (n, 0)).collect();
        let mut forward: BTreeMap<Dot, BTreeSet<Dot>> = BTreeMap::new();
        for &(u, v) in self.edges.keys() {
            if forward.entry(u).or_default().insert(v) {
                *incoming.entry(v).or_default() += 1;
            }
        }

        let mut ready: BTreeSet<Dot> = incoming
            .iter()
            .filter_map(|(&n, &degree)| (degree == 0).then_some(n))
            .collect();
        let mut witness: Vec<Dot> = Vec::with_capacity(self.nodes.len());
        while let Some(&next) = ready.iter().next() {
            let _ = ready.remove(&next);
            witness.push(next);
            if let Some(successors) = forward.get(&next) {
                for &v in successors {
                    let degree = incoming.get_mut(&v).expect("every edge end is a node");
                    *degree -= 1;
                    if *degree == 0 {
                        let _ = ready.insert(v);
                    }
                }
            }
        }
        if witness.len() == self.nodes.len() {
            return Ok(witness);
        }
        Err(self.contradiction(&witness))
    }

    /// Extracts a constraint cycle from the stalled residue: every
    /// unemitted node keeps an unemitted predecessor (that is what stalled
    /// it), so walking least predecessors must revisit a node, and the
    /// revisited stretch is a cycle.
    fn contradiction(&self, emitted: &[Dot]) -> Contradiction {
        let emitted: BTreeSet<Dot> = emitted.iter().copied().collect();
        let remaining: BTreeSet<Dot> = self.nodes.difference(&emitted).copied().collect();
        let mut backward: BTreeMap<Dot, BTreeSet<Dot>> = BTreeMap::new();
        for &(u, v) in self.edges.keys() {
            if remaining.contains(&u) && remaining.contains(&v) {
                let _ = backward.entry(v).or_default().insert(u);
            }
        }

        let start = *remaining.iter().next().expect("a stall leaves a residue");
        let mut path: Vec<Dot> = alloc::vec![start];
        let mut seen_at: BTreeMap<Dot, usize> = BTreeMap::new();
        let _ = seen_at.insert(start, 0);
        loop {
            let current = *path.last().expect("the path starts nonempty");
            let predecessor = *backward
                .get(&current)
                .and_then(|preds| preds.iter().next())
                .expect("every stalled node keeps a stalled predecessor");
            if let Some(&at) = seen_at.get(&predecessor) {
                // The path records reverse edges (`path[j + 1]` constrained
                // before `path[j]`), so the forward cycle reads the
                // revisited stretch backward, entered at the revisit.
                let mut cycle: Vec<Dot> = alloc::vec![predecessor];
                cycle.extend(path[at..].iter().rev().copied());
                let _ = cycle.pop();
                let witnesses = cycle
                    .iter()
                    .enumerate()
                    .map(|(j, &u)| {
                        let v = cycle[(j + 1) % cycle.len()];
                        self.edges[&(u, v)]
                    })
                    .collect();
                return Contradiction { cycle, witnesses };
            }
            let _ = seen_at.insert(predecessor, path.len());
            path.push(predecessor);
        }
    }
}

#[test]
fn test_the_empty_ledger_and_the_single_state_pass() {
    let mut ledger = OrderLedger::new();
    assert_eq!(ledger.verdict(), Ok(Vec::new()));
    let _ = ledger.observe(&[dot(1, 1), dot(1, 2), dot(2, 1)]);
    assert_eq!(
        ledger.verdict(),
        Ok(alloc::vec![dot(1, 1), dot(1, 2), dot(2, 1)])
    );
    assert_eq!(ledger.observations(), 1);
}

#[test]
fn test_a_repeated_element_in_one_state_is_a_self_contradiction() {
    // A state can never show one identity twice; the ledger reads it as the
    // one-step cycle it is.
    let mut ledger = OrderLedger::new();
    let index = ledger.observe(&[dot(1, 1), dot(1, 1)]);
    let refusal = ledger.verdict().expect_err("a duplicate cannot be ordered");
    assert_eq!(refusal.cycle, [dot(1, 1)]);
    assert_eq!(refusal.witnesses, [index]);
}