neberu 0.0.0

// ============================================================
// TRACE — THE ALGEBRA OF REWRITING
// ============================================================
//
// A trace is a walk through rewriting space: Wlk<TraceGen>.
// Two steps commute iff their spans don't overlap.
// This IS the confluence condition stated as a predicate.
//
// The canonical TraceWalk is unique iff the expression governance
// is confluent. Confluence failure = two canonical walks with
// different terminals.
//
// KOT (Kase Optimality Theorem):
//   Minimal:    canonical walk length = walk length
//   Complete:   no rule fires on terminal
//   Consistent: no confluence failure at source
//
// SELF-HOSTING BOUNDARY:
// TraceWalk is constructible now.
// Governable in .neb requires parametric open relations (Session 004).
// The span arithmetic condition dissolves when .neb can express ordering.

use crate::expr::Expr;
use crate::governance::Governance;
use crate::word::Word;

// ── TraceGen ─────────────────────────────────────────────────────────────────

/// A single rewrite step: self-contained, self-verifying.
/// Carries rule index, position, and the matched word (evidence).
#[derive(Clone, PartialEq, Eq, Hash)]
pub struct TraceGen {
    pub rule_idx: usize,
    pub start: usize,
    pub matched: Word, // self-verifiable: matched == gov.relations[rule_idx].source
}

impl TraceGen {
    pub fn new(rule_idx: usize, start: usize, matched: Word) -> TraceGen {
        TraceGen {
            rule_idx,
            start,
            matched,
        }
    }

    pub fn end(&self) -> usize {
        self.start + self.matched.grade()
    }

    /// Verify this step is consistent with the governance that produced it.
    pub fn verify(&self, gov: &Governance) -> bool {
        gov.relations()
            .get(self.rule_idx)
            .map(|r| r.source == self.matched)
            .unwrap_or(false)
    }
}

impl PartialOrd for TraceGen {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}
impl Ord for TraceGen {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        self.rule_idx
            .cmp(&other.rule_idx)
            .then(self.start.cmp(&other.start))
    }
}

impl std::fmt::Debug for TraceGen {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "r{}@{}[{}]", self.rule_idx, self.start, self.matched)
    }
}

// ── TraceWalk ────────────────────────────────────────────────────────────────

/// A trace walk: sequence of rewrite steps with partial commutativity.
#[derive(Clone, PartialEq, Eq)]
pub struct TraceWalk {
    steps: Vec<TraceGen>,
}

impl TraceWalk {
    pub fn empty() -> TraceWalk {
        TraceWalk { steps: vec![] }
    }
    pub fn singleton(s: TraceGen) -> TraceWalk {
        TraceWalk { steps: vec![s] }
    }
    pub fn from_steps(steps: Vec<TraceGen>) -> TraceWalk {
        TraceWalk { steps }
    }
    pub fn steps(&self) -> &[TraceGen] {
        &self.steps
    }
    pub fn len(&self) -> usize {
        self.steps.len()
    }
    pub fn is_empty(&self) -> bool {
        self.steps.is_empty()
    }

    /// Canonicalize under step-commutativity (bubble sort).
    pub fn canonicalize(&self) -> TraceWalk {
        let mut steps = self.steps.clone();
        let mut changed = true;
        while changed {
            changed = false;
            for i in 0..steps.len().saturating_sub(1) {
                if steps[i] > steps[i + 1] && steps_commute(&steps[i], &steps[i + 1]) {
                    steps.swap(i, i + 1);
                    changed = true;
                }
            }
        }
        TraceWalk { steps }
    }
}

/// Two steps commute iff their spans don't overlap.
/// Non-overlapping positions = independent rewrites = order doesn't matter.
/// Overlapping positions = interacting rewrites = order may matter.
/// This predicate IS the confluence condition.
///
/// SELF-HOSTING BOUNDARY: expressed in Rust here.
/// Session 004 target: express as .neb parametric open relation.
pub fn steps_commute(a: &TraceGen, b: &TraceGen) -> bool {
    a.end() <= b.start || b.end() <= a.start
}

// ── Build TraceWalk from Governance Trace ─────────────────────────────────────

/// Build a TraceWalk from the governance-level Trace struct.
pub fn walk_from_trace(trace: &crate::governance::Trace, gov: &Governance) -> TraceWalk {
    let steps = trace
        .steps
        .iter()
        .filter_map(|step| {
            step.fired.map(|(ri, pos)| {
                let matched = gov
                    .relations()
                    .get(ri)
                    .map(|r| r.source.clone())
                    .unwrap_or_else(Word::scalar);
                TraceGen::new(ri, pos, matched)
            })
        })
        .collect();
    TraceWalk { steps }
}

/// Replay a TraceWalk from a source expression.
pub fn replay(walk: &TraceWalk, source: &Expr, gov: &Governance) -> Expr {
    let mut current = source.clone();
    for step in &walk.steps {
        current = gov.apply_at(&current, step.rule_idx, step.start);
    }
    current
}

// ── Confluence ────────────────────────────────────────────────────────────────

/// A confluence witness: two walks from the same source reaching different terminals.
pub struct ConfluenceWitness {
    pub source: Expr,
    pub walk_a: TraceWalk,
    pub walk_b: TraceWalk,
    pub terminal_a: Expr,
    pub terminal_b: Expr,
}

impl ConfluenceWitness {
    pub fn is_real(&self) -> bool {
        self.terminal_a != self.terminal_b
    }
}

impl std::fmt::Display for ConfluenceWitness {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        writeln!(f, "confluence failure:")?;
        writeln!(f, "  source:  {}", self.source)?;
        writeln!(f, "  path A → {}", self.terminal_a)?;
        writeln!(f, "  path B → {}", self.terminal_b)?;
        write!(f, "  your governance is not confluent at this expression.")
    }
}

/// Find confluence witnesses for `source` under `gov`.
/// Critical pair analysis: overlapping applicable rules may produce different results.
/// Confluent governance (all standard Clifford algebras) returns empty vec.
pub fn explore_confluence(gov: &Governance, source: &Expr) -> Vec<ConfluenceWitness> {
    let mut witnesses = Vec::new();
    for (word, coeff) in source.terms() {
        let single = Expr::term(*coeff, word.clone());
        let applicable = gov.applicable(word);
        for i in 0..applicable.len() {
            for j in (i + 1)..applicable.len() {
                let (ri, pi) = applicable[i];
                let (rj, pj) = applicable[j];
                let end_i = pi + gov.relations()[ri].source.grade();
                let end_j = pj + gov.relations()[rj].source.grade();
                // Only critical pairs: overlapping spans.
                if end_i <= pj || end_j <= pi {
                    continue;
                }

                let after_i = gov.apply_at(&single, ri, pi);
                let after_j = gov.apply_at(&single, rj, pj);
                let term_a = gov.canonicalize(&after_i);
                let term_b = gov.canonicalize(&after_j);

                if term_a != term_b {
                    let step_i = TraceGen::new(ri, pi, gov.relations()[ri].source.clone());
                    let step_j = TraceGen::new(rj, pj, gov.relations()[rj].source.clone());
                    witnesses.push(ConfluenceWitness {
                        source: single.clone(),
                        walk_a: TraceWalk::singleton(step_i),
                        walk_b: TraceWalk::singleton(step_j),
                        terminal_a: term_a,
                        terminal_b: term_b,
                    });
                }
            }
        }
    }
    witnesses
}

// ── KOT Walk Verification ─────────────────────────────────────────────────────

/// KOT verification result: Minimality + Completeness + Consistency.
/// The theorem as structure, not heuristic.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct KotResult {
    pub minimal: bool,
    pub complete: bool,
    pub consistent: bool,
    pub witnesses: Vec<String>,
}

impl KotResult {
    pub fn passed(&self) -> bool {
        self.minimal && self.complete && self.consistent
    }

    /// As a Trit: P = optimal, N = not optimal.
    /// This is the MS-α encoding: the KOT certifies itself as a Trit.
    pub fn as_trit(&self) -> crate::trit::Trit {
        if self.passed() {
            crate::trit::P
        } else {
            crate::trit::N
        }
    }
}

impl std::fmt::Display for KotResult {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        if self.passed() {
            write!(f, "KOT: {} (minimal, complete, consistent)", self.as_trit())
        } else {
            write!(f, "KOT: {} ", self.as_trit())?;
            if !self.minimal {
                write!(f, "[not minimal] ")?;
            }
            if !self.complete {
                write!(f, "[not complete] ")?;
            }
            if !self.consistent {
                write!(f, "[not consistent] ")?;
            }
            for w in &self.witnesses {
                write!(f, "\n  {w}")?;
            }
            Ok(())
        }
    }
}

/// Verify KOT over a TraceWalk.
/// Original expr needed once to seed replay. Walk is self-sufficient after that.
pub fn verify_kot(walk: &TraceWalk, source: &Expr, gov: &Governance) -> KotResult {
    let canonical = walk.canonicalize();
    let minimal = canonical.len() == walk.len();
    let terminal = replay(&canonical, source, gov);
    let complete = terminal.terms().all(|(w, _)| gov.applicable(w).is_empty());
    let failures = explore_confluence(gov, source);
    let consistent = failures.is_empty();
    let witnesses = failures.iter().map(|w| format!("{w}")).collect();

    KotResult {
        minimal,
        complete,
        consistent,
        witnesses,
    }
}

// ── Tests ─────────────────────────────────────────────────────────────────────

#[cfg(test)]
mod tests {
    use super::*;
    use crate::gen::Gen;
    use crate::governance::{Governance, Relation};
    use crate::rat::Rat;

    fn ei(i: u32) -> Gen {
        Gen::imaginary(i)
    }

    #[test]
    fn tracegen_end() {
        let s = TraceGen::new(0, 3, Word::from_gens(&[ei(0), ei(1)]));
        assert_eq!(s.end(), 5);
    }

    #[test]
    fn tracegen_verify() {
        let gov = Governance::cl(1, 0, 0);
        let matched = Word::from_gens(&[ei(0), ei(0)]);
        let s = TraceGen::new(0, 0, matched);
        assert!(s.verify(&gov));
    }

    #[test]
    fn steps_commute_non_overlapping() {
        let a = TraceGen::new(0, 0, Word::from_gens(&[ei(0), ei(1)])); // [0,2)
        let b = TraceGen::new(1, 3, Word::from_gens(&[ei(0), ei(1)])); // [3,5)
        assert!(steps_commute(&a, &b));
    }

    #[test]
    fn steps_do_not_commute_overlapping() {
        let a = TraceGen::new(0, 0, Word::from_gens(&[ei(0), ei(1)])); // [0,2)
        let b = TraceGen::new(1, 1, Word::from_gens(&[ei(0), ei(1)])); // [1,3)
        assert!(!steps_commute(&a, &b));
    }

    #[test]
    fn confluence_clifford_confluent() {
        let gov = Governance::cl(2, 0, 0);
        let e2e1 = Expr::term(Rat::one(), Word::from_gens(&[ei(1), ei(0)]));
        let witnesses = explore_confluence(&gov, &e2e1);
        assert!(witnesses.is_empty(), "Cl(2,0,0) must be confluent");
    }

    #[test]
    fn confluence_contradictory_rules_witness() {
        let gov = Governance::free()
            .with_relation(Relation::new(
                Word::from_gens(&[ei(0), ei(0)]),
                Expr::int(-1),
            ))
            .with_relation(Relation::new(
                Word::from_gens(&[ei(0), ei(0)]),
                Expr::int(1),
            ));
        let e1e1 = Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)]));
        let witnesses = explore_confluence(&gov, &e1e1);
        assert!(
            !witnesses.is_empty(),
            "contradictory rules must produce witness"
        );
        assert!(witnesses[0].is_real());
    }

    #[test]
    fn kot_cl100_square_passes() {
        let gov = Governance::cl(1, 0, 0);
        let source = Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)]));
        let (_, trace) = gov.canonicalize_traced(&source);
        let walk = walk_from_trace(&trace, &gov);
        let result = verify_kot(&walk, &source, &gov);
        assert!(result.passed(), "Cl(1,0,0) square: {result}");
        assert_eq!(
            result.as_trit(),
            crate::trit::P,
            "KOT result must be P (optimal)"
        );
    }

    #[test]
    fn kot_contradictory_fails_consistency() {
        let gov = Governance::free()
            .with_relation(Relation::new(
                Word::from_gens(&[ei(0), ei(0)]),
                Expr::int(-1),
            ))
            .with_relation(Relation::new(
                Word::from_gens(&[ei(0), ei(0)]),
                Expr::int(1),
            ));
        let source = Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)]));
        let result = verify_kot(&TraceWalk::empty(), &source, &gov);
        assert!(!result.consistent);
        assert_eq!(result.as_trit(), crate::trit::N);
    }

    #[test]
    fn kot_result_as_trit() {
        // MS-α: KOT result IS a Trit.
        // The system encodes its own optimality verdict as the axiom's primitive type.
        let gov = Governance::cl(1, 0, 0);
        let source = Expr::gen(ei(0));
        let result = verify_kot(&TraceWalk::empty(), &source, &gov);
        let t = result.as_trit();
        assert!(t.is_valid());
        assert_eq!(t, crate::trit::P); // a generator with no rules = trivially optimal
    }
}