neberu 0.0.0

// ============================================================
// INSPECT — THE KOT REPORT
// ============================================================
//
// inspect(source, gov) → InspectReport
//
// Runs the full pipeline:
//   1. Canonicalize source under gov → terminal + trace
//   2. Build TraceWalk from trace
//   3. Measure N₁ (walk size), N₂ (KOT gov size), N₃ (total)
//   4. Compute Q₁ (KOT verdict as Trit)
//   5. Encode certificate → Expr in Magma<Trit>
//   6. Compute Q₂ (self-referential certification)
//   7. Display the three-section report

use crate::encoding::{compute_q2, q2_governance, tracewalk_to_expr};
use crate::expr::Expr;
use crate::governance::Governance;
use crate::size::{certificate_size, governance_size, tracewalk_size, CertSize, GovSize, WalkSize};
use crate::trace::{verify_kot, walk_from_trace, KotResult};
use crate::trit::{Trit, N, P, Z};

// ── Report structure ──────────────────────────────────────────────────────────

pub struct InspectReport {
    pub source: Expr,
    pub terminal: Expr,
    pub trace_steps: usize,
    pub converged: bool,
    pub n1: WalkSize,
    pub n2: GovSize,
    pub cert: CertSize,
    pub q1: Trit,
    pub q1_result: KotResult,
    pub cert_expr: Expr, // the walk encoded as Expr in Magma<Trit>
    pub q2: Trit,
    pub gov_name: String,
    pub gov_size: GovSize, // the expression governance (not KOT gov)
}

// ── Main inspect function ─────────────────────────────────────────────────────

pub fn inspect(source: &Expr, gov: &Governance, gov_name: &str) -> InspectReport {
    // Step 1: Canonicalize
    let (terminal, trace) = gov.canonicalize_traced(source);

    // Step 2: Build TraceWalk
    let walk = walk_from_trace(&trace, gov);

    // Step 3: Measure N₁
    let n1 = tracewalk_size(&walk);

    // Step 4: Build KOT governance and measure N₂
    let kot_gov = q2_governance(); // The KOT governance (checks [P,P,P])
    let n2 = governance_size(&kot_gov);

    // Step 5: Total certificate size N₃
    let cert = certificate_size(&walk, &kot_gov);

    // Step 6: Q₁
    let q1_result = verify_kot(&walk, source, gov);
    let q1 = q1_result.as_trit();

    // Step 7: Encode certificate
    let cert_expr = tracewalk_to_expr(&walk);

    // Step 8: Q₂
    let q2 = compute_q2(&q1_result);

    // Step 9: Measure the expression governance itself
    let gov_size = governance_size(gov);

    InspectReport {
        source: source.clone(),
        terminal,
        trace_steps: trace.num_steps(),
        converged: trace.converged,
        n1,
        n2,
        cert,
        q1,
        q1_result,
        cert_expr,
        q2,
        gov_name: gov_name.to_string(),
        gov_size,
    }
}

// ── Display ───────────────────────────────────────────────────────────────────

const W: usize = 56;

pub fn display(r: &InspectReport) {
    let bar = "─".repeat(W);
    let heavy = "═".repeat(W);
    let thin = "·".repeat(W);

    // ── Header ──
    println!("╔{}╗", heavy);
    println!("║{:^width$}║", " NĒBERU INSPECT ", width = W);
    println!("╠{}╣", heavy);

    // ── Section 1: Expression ──
    println!(
        "║  {:<8} {:<width$}║",
        "source:",
        format!("{}", r.source),
        width = W - 11
    );
    println!(
        "║  {:<8} {:<width$}║",
        "algebra:",
        r.gov_name,
        width = W - 11
    );
    println!("╠{}╣", bar);

    if r.trace_steps == 0 {
        println!("║  already canonical{:<width$}║", "", width = W - 20);
    } else {
        println!(
            "║  canonicalization: {} step{}{}    ║",
            r.trace_steps,
            if r.trace_steps == 1 { "" } else { "s" },
            " ".repeat(W - 22 - digit_count(r.trace_steps))
        );
        println!(
            "║  terminal: {:<width$}║",
            format!("{}", r.terminal),
            width = W - 13
        );
    }

    // ── Section 2: The Numbers ──
    println!("╠{}╣", heavy);
    println!("║{:^width$}║", " THE NUMBERS ", width = W);
    println!("╠{}╣", bar);

    // N₁: trace encoding
    println!(
        "║  N₁ — trace encoding (Magma<Trit>){:<width$}║",
        "",
        width = W - 37
    );
    println!("║    steps:        {:<width$}║", r.n1.steps, width = W - 19);
    println!(
        "║    trits:        {:<width$}║",
        format!(
            "{} t  ({} bits, {} byte{})",
            r.n1.total_trits,
            r.n1.bits,
            r.n1.bytes,
            if r.n1.bytes == 1 { "" } else { "s" }
        ),
        width = W - 19
    );

    // Show step breakdown if multiple steps
    if r.n1.steps > 1 {
        for (i, s) in r.n1.step_sizes.iter().enumerate() {
            println!(
                "║    step {:>2}:       {:<width$}║",
                i + 1,
                format!(
                    "{} trits  [r:{} s:{} sep:{} m:{}]",
                    s.total_trits, s.rule_idx_trits, s.start_trits, s.sep_trits, s.matched_trits
                ),
                width = W - 21
            );
        }
    } else if r.n1.steps == 1 {
        let s = &r.n1.step_sizes[0];
        println!(
            "║    breakdown:    {:<width$}║",
            format!(
                "rule:{} start:{} sep:{} match:{}",
                s.rule_idx_trits, s.start_trits, s.sep_trits, s.matched_trits
            ),
            width = W - 19
        );
    }

    println!("║  {:<width$}║", thin, width = W - 3);

    // N₂: KOT governance
    println!("║  N₂ — KOT governance{:<width$}║", "", width = W - 22);
    println!(
        "║    relations:    {:<width$}║",
        r.n2.num_relations,
        width = W - 19
    );
    println!(
        "║    trits:        {:<width$}║",
        format!(
            "{} t  ({} bits, {} bytes)",
            r.n2.total_trits, r.n2.bits, r.n2.bytes
        ),
        width = W - 19
    );

    println!("║  {:<width$}║", thin, width = W - 3);

    // N₂b: expression governance
    println!(
        "║  N₂b — expression governance ({})  {:<width$}║",
        r.gov_name,
        "",
        width = W.saturating_sub(35 + r.gov_name.len())
    );
    println!(
        "║    relations:    {:<width$}║",
        r.gov_size.num_relations,
        width = W - 19
    );
    println!(
        "║    trits:        {:<width$}║",
        format!(
            "{} t  ({} bits, {} bytes)",
            r.gov_size.total_trits, r.gov_size.bits, r.gov_size.bytes
        ),
        width = W - 19
    );

    println!("║  {:<width$}║", thin, width = W - 3);

    // N₃: total certificate
    println!(
        "║  N₃ — certificate total  (N₁ + N₂){:<width$}║",
        "",
        width = W - 37
    );
    println!(
        "║    trits:        {:<width$}║",
        format!(
            "{} t  ({} bits, {} bytes)",
            r.cert.n3_trits, r.cert.n3_bits, r.cert.n3_bytes
        ),
        width = W - 19
    );

    // ── Section 3: Verdict Q₁ ──
    println!("╠{}╣", heavy);
    println!("║{:^width$}║", " VERDICT ", width = W);
    println!("╠{}╣", bar);

    println!(
        "║  Q₁ = {:?}  {}  {:<width$}║",
        r.q1,
        trit_sym(r.q1),
        match r.q1 {
            P => "OPTIMAL",
            N => "NOT OPTIMAL",
            Z => "INDETERMINATE",
            _ => "INVALID",
        },
        width = W.saturating_sub(14)
    );

    println!(
        "║    minimal:    {} {:<width$}║",
        check(r.q1_result.minimal),
        "",
        width = W - 16
    );
    println!(
        "║    complete:   {} {:<width$}║",
        check(r.q1_result.complete),
        "",
        width = W - 16
    );
    println!(
        "║    consistent: {} {:<width$}║",
        check(r.q1_result.consistent),
        "",
        width = W - 16
    );

    if !r.q1_result.witnesses.is_empty() {
        println!("╠{}╣", bar);
        println!("║  confluence failure:{:<width$}║", "", width = W - 21);
        for w in &r.q1_result.witnesses {
            for line in w.lines() {
                println!("║    {:<width$}║", line, width = W - 5);
            }
        }
    }

    // ── Section 4: Self-reference Q₂ ──
    println!("╠{}╣", heavy);
    println!("║{:^width$}║", " SELF-CERTIFICATION ", width = W);
    println!("╠{}╣", bar);

    println!(
        "║  certificate encoded as Expr in Magma<Trit>:  {:<width$}║",
        "",
        width = W.saturating_sub(47)
    );
    println!(
        "║    {:<width$}║",
        format!("{}", r.cert_expr),
        width = W - 5
    );

    println!("║  {:<width$}║", thin, width = W - 3);

    println!(
        "║  Q₂ = {:?}  {}  {:<width$}║",
        r.q2,
        trit_sym(r.q2),
        match r.q2 {
            P => "certificate is correctly certified",
            N => "certificate has an error",
            Z => "indeterminate",
            _ => "invalid",
        },
        width = W.saturating_sub(14)
    );

    // Fixed point statement
    if r.q1 == P && r.q2 == P {
        println!("╠{}╣", bar);
        println!(
            "║  {:<width$}║",
            "Q₁ = Q₂ = P  —  fixed point reached",
            width = W - 3
        );
        println!(
            "║  {:<width$}║",
            "the axiom describes itself.",
            width = W - 3
        );
    }

    println!("╚{}╝", heavy);

    // Summary line
    println!(
        "\n  N₁={} t  N₂={} t  N₃={} t  |  Q₁={:?}  Q₂={:?}",
        r.cert.n1.total_trits, r.cert.n2.total_trits, r.cert.n3_trits, r.q1, r.q2
    );
}

fn trit_sym(t: Trit) -> &'static str {
    match t {
        P => "✓",
        N => "✗",
        Z => "?",
        _ => "!",
    }
}

fn check(b: bool) -> &'static str {
    if b {
        "✓"
    } else {
        "✗"
    }
}

fn digit_count(n: usize) -> usize {
    if n == 0 {
        1
    } else {
        n.ilog10() as usize + 1
    }
}

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

#[cfg(test)]
mod tests {
    use super::*;
    use crate::gen::Gen;
    use crate::rat::Rat;
    use crate::word::Word;

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

    #[test]
    fn inspect_e1e1_cl100() {
        let gov = Governance::cl(1, 0, 0);
        let source = Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)]));
        let r = inspect(&source, &gov, "Cl(1,0,0)");
        assert_eq!(r.trace_steps, 1);
        assert_eq!(r.terminal, Expr::int(-1));
        assert_eq!(r.q1, P);
        assert_eq!(r.q2, P);
        assert_eq!(r.n1.total_trits, 4); // INV INV N N
        assert!(r.cert.n3_trits > 0);
    }

    #[test]
    fn inspect_already_canonical() {
        let gov = Governance::cl(2, 0, 0);
        let source = Expr::gen(ei(0)); // e1 is already canonical
        let r = inspect(&source, &gov, "Cl(2,0,0)");
        assert_eq!(r.trace_steps, 0);
        assert_eq!(r.q1, P);
        assert_eq!(r.q2, P);
        assert_eq!(r.n1.total_trits, 0); // empty walk
    }

    #[test]
    fn inspect_contradictory_governance() {
        use crate::governance::Relation;
        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 r = inspect(&source, &gov, "contradictory");
        assert_eq!(r.q1, N);
        assert_eq!(r.q2, N); // the failing certificate is also correctly identified as N
    }

    #[test]
    fn q1_and_q2_both_p_for_standard_algebras() {
        let cases = [
            (
                Governance::cl(1, 0, 0),
                Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)])),
                "Cl(1,0,0)",
            ),
            (Governance::cl(2, 0, 0), Expr::gen(ei(0)), "Cl(2,0,0)"),
        ];
        for (gov, source, name) in cases {
            let r = inspect(&source, &gov, name);
            assert_eq!(r.q1, P, "Q₁ must be P for {name}");
            assert_eq!(r.q2, P, "Q₂ must be P for {name}");
        }
    }

    #[test]
    fn display_runs_without_panic() {
        let gov = Governance::cl(1, 0, 0);
        let source = Expr::term(Rat::one(), Word::from_gens(&[ei(0), ei(0)]));
        let r = inspect(&source, &gov, "Cl(1,0,0)");
        // Just verify it doesn't panic — output goes to stdout
        display(&r);
    }

    #[test]
    fn n1_n2_n3_relationship() {
        let gov = Governance::cl(2, 0, 0);
        let source = Expr::term(Rat::one(), Word::from_gens(&[ei(1), ei(0)])); // e2*e1 needs one step
        let r = inspect(&source, &gov, "Cl(2,0,0)");
        assert_eq!(
            r.cert.n3_trits,
            r.cert.n1.total_trits + r.cert.n2.total_trits
        );
    }
}