provable_contracts/

proof_status.rs

//! Proof status report — cross-contract proof level assessment.
//!
//! Computes a hierarchical proof level (L1–L5) for each contract and
//! aggregates them into kernel equivalence classes that mirror the
//! `KernelOp` classification from apr-model-qa-playbook.
//!
//! Output is consumed by `pv proof-status` (text/JSON) and by the
//! playbook's `ProofBonus` MQS integration.

use std::collections::BTreeMap;
use std::fmt;

use serde::{Deserialize, Serialize};

use crate::binding::{BindingRegistry, ImplStatus};
use crate::discharge::summary::{self, Discharged, L4Source};
use crate::schema::Contract;

// ── Proof level hierarchy ─────────────────────────────────────────

/// Hierarchical proof assurance level.
///
/// Each level subsumes the ones below it:
/// - **L1** — Contract YAML exists with equations
/// - **L2** — Property tested (falsification tests cover obligations)
/// - **L3** — Kani bounded-model-checked
/// - **L4** — Lean 4 theorem proved
/// - **L5** — L4 + all bindings verified as implemented
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub enum ProofLevel {
    /// Contract YAML exists with equations
    L1,
    /// Property tested via falsification tests
    L2,
    /// Kani bounded-model-checked
    L3,
    /// Lean 4 theorem proved
    L4,
    /// Lean proved and all bindings verified
    L5,
}

impl fmt::Display for ProofLevel {
    /// Format the proof level as its string label (L1 through L5)
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let s = match self {
            Self::L1 => "L1",
            Self::L2 => "L2",
            Self::L3 => "L3",
            Self::L4 => "L4",
            Self::L5 => "L5",
        };
        write!(f, "{s}")
    }
}

// ── Per-contract status ───────────────────────────────────────────

/// Proof status for a single contract.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ContractProofStatus {
    /// Contract file stem (e.g. "softmax-kernel-v1")
    pub stem: String,
    /// Computed hierarchical proof level
    pub proof_level: ProofLevel,
    /// Number of proof obligations in the contract
    pub obligations: u32,
    /// Obligations declared `applies_to: not_applicable` (PMAT-3091). Counted
    /// APART: never passed, discharged or proved, and never removed from
    /// `obligations` for the level computation, so they cannot raise a level.
    #[serde(default)]
    pub not_applicable: u32,
    /// Number of falsification tests defined
    pub falsification_tests: u32,
    /// Number of Kani bounded-model-checking harnesses
    pub kani_harnesses: u32,
    /// Number of obligations proved in Lean 4
    pub lean_proved: u32,
    /// Obligations grounded by a sorry-free in-tree Lean theorem the equation names (ONT-2a)
    pub lean_grounded: u32,
    /// The contract claims a Lean proof its tree does not ground: printed `self-declared`, excluded from L4
    pub l4_self_declared: bool,
    /// Number of bindings with `implemented` status
    pub bindings_implemented: u32,
    /// Total number of equation bindings
    pub bindings_total: u32,
}

// ── Kernel class summary ──────────────────────────────────────────

/// Summary of proof status for a kernel equivalence class.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct KernelClassSummary {
    /// Kernel class identifier (A through E)
    pub label: String,
    /// Human-readable description of the kernel combination
    pub description: String,
    /// Contract stems belonging to this class
    pub contract_stems: Vec<String>,
    /// Lowest proof level among class members
    pub min_proof_level: ProofLevel,
    /// Whether all class members have full binding coverage
    pub all_bound: bool,
}

// ── Full report ───────────────────────────────────────────────────

/// Top-level proof status report, serializable to JSON.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofStatusReport {
    /// Report schema version for forward compatibility
    pub schema_version: String,
    /// Unix epoch timestamp when the report was generated
    pub timestamp: String,
    /// Per-contract proof status entries
    pub contracts: Vec<ContractProofStatus>,
    /// Kernel equivalence class summaries
    pub kernel_classes: Vec<KernelClassSummary>,
    /// ONT-2a andon: a self-declared L4 is excluded from the L4 total in this build
    pub l4_self_declared_excluded: bool,
    /// EV-8b: `discharge` when L4 credit came from `discharge-summary.json`, `self-declared` when no summary was found
    /// and the tree's own `.lean` text was scanned instead
    #[serde(default)]
    pub l4_source: L4Source,
    /// Why the summary granted nothing (`stale discharge: …`, `red discharge: …`); `None` when it granted or was absent
    #[serde(default)]
    pub l4_withheld: Option<String>,
    /// Aggregate totals across all contracts
    pub totals: ProofStatusTotals,
}

/// Aggregate totals across all contracts.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofStatusTotals {
    /// Total number of contracts analyzed
    pub contracts: u32,
    /// Sum of proof obligations across all contracts
    pub obligations: u32,
    /// Sum of `applies_to: not_applicable` obligations (PMAT-3091), a subset of
    /// `obligations` and never a subset of anything proved.
    #[serde(default)]
    pub not_applicable: u32,
    /// Sum of falsification tests across all contracts
    pub falsification_tests: u32,
    /// Sum of Kani harnesses across all contracts
    pub kani_harnesses: u32,
    /// Sum of Lean-proved obligations across all contracts
    pub lean_proved: u32,
    /// Sum of GROUNDED Lean-proved obligations across all contracts (ONT-2a)
    pub lean_grounded: u32,
    /// Contracts whose L4 claim is self-declared, and therefore excluded from L4 (ONT-2a)
    pub l4_self_declared: u32,
    /// Sum of implemented bindings across all contracts
    pub bindings_implemented: u32,
    /// Sum of total bindings across all contracts
    pub bindings_total: u32,
}

// ── Kernel class → contract stem mapping ──────────────────────────

/// Static mapping from kernel equivalence class to contract stems.
///
/// Mirrors the `KernelOp` classification from `apr-model-qa-playbook`:
/// - **A** — GQA + `RMSNorm` + `SiLU` + `SwiGLU` + `RoPE` (Llama/Mistral)
/// - **B** — MHA + `LayerNorm` + GELU + `AbsPos` (GPT-2/BERT)
/// - **C** — MHA + `LayerNorm` + GELU + `ALiBi` (BLOOM/MPT)
/// - **D** — `LayerNorm` + GELU + `SiLU` + GQA (Gemma)
/// - **E** — `RMSNorm` + `SwiGLU` + GQA (Qwen)
fn kernel_class_map() -> Vec<(&'static str, &'static str, &'static [&'static str])> {
    vec![
        (
            "A",
            "GQA+RMSNorm+SiLU+SwiGLU+RoPE",
            &[
                "rmsnorm-kernel-v1",
                "silu-kernel-v1",
                "swiglu-kernel-v1",
                "rope-kernel-v1",
                "gqa-kernel-v1",
                "softmax-kernel-v1",
                "matmul-kernel-v1",
            ],
        ),
        (
            "B",
            "MHA+LayerNorm+GELU+AbsPos",
            &[
                "layernorm-kernel-v1",
                "gelu-kernel-v1",
                "attention-kernel-v1",
                "softmax-kernel-v1",
                "matmul-kernel-v1",
                "absolute-position-v1",
            ],
        ),
        (
            "C",
            "MHA+LayerNorm+GELU+ALiBi",
            &[
                "layernorm-kernel-v1",
                "gelu-kernel-v1",
                "attention-kernel-v1",
                "softmax-kernel-v1",
                "alibi-kernel-v1",
                "matmul-kernel-v1",
            ],
        ),
        (
            "D",
            "LayerNorm+GELU+SiLU+GQA",
            &[
                "layernorm-kernel-v1",
                "gelu-kernel-v1",
                "silu-kernel-v1",
                "gqa-kernel-v1",
                "softmax-kernel-v1",
                "matmul-kernel-v1",
            ],
        ),
        (
            "E",
            "RMSNorm+SwiGLU+GQA",
            &[
                "rmsnorm-kernel-v1",
                "swiglu-kernel-v1",
                "gqa-kernel-v1",
                "softmax-kernel-v1",
                "matmul-kernel-v1",
            ],
        ),
    ]
}

// ── Core computation ──────────────────────────────────────────────

/// Returns `true` when EVERY proof obligation is discharged in Lean.
///
/// Strict per-obligation semantics — no fuzzy over-promotion. A contract is
/// Lean-proved (L4) only when the number of Lean-proved obligations plus the
/// explicitly not-applicable ones covers ALL proof obligations, and at least
/// one obligation is genuinely proved. The obligation total is
/// `proof_obligations.len()` — the SAME total used for L2/L3 — so a
/// `verification_summary` cannot manufacture L4 by understating the total.
///
/// Proof counts come from the contract's `verification_summary` when it makes a
/// positive claim (`l4_lean_proved > 0`); otherwise from a scan of the in-tree
/// sorry-free `.lean` theorems. Because the scan can only credit obligations it
/// resolves, partial coverage (the old "≥1 resolving ref → L4" over-promotion)
/// now correctly reports L3 instead of a full L4. Contracts with legitimately
/// N/A obligations (e.g. softmax-kernel-v1 = 5 proved + 4 N/A of 9) MUST declare
/// that in `verification_summary` — the scan path grants no N/A credit.
///
/// The grounding count is passed IN rather than scanned here.
///
/// The scan reads the Lean tree from paths relative to the process CWD, so inside a unit test it resolves
/// nothing and every fixture is ungrounded by construction — a suite in which the andon could withdraw
/// ALL credit for ever and no test would notice. Taking the count as a parameter is what keeps both sides
/// covered: `grounded == 0` is the andon, `grounded + not_applicable >= total` is the credit it still
/// grants. Production callers use the wrapper and get the scan.
#[must_use]
pub fn is_lean_proved_with_grounding(contract: &Contract, grounded: u32) -> bool {
    let total = contract.proof_obligations.len() as u32;
    if total == 0 {
        return false;
    }
    // ONT-001 ONT-2a (andon): a `verification_summary` is the contract talking about ITSELF. PVL EV-8b: the
    // grounding is a theorem an equation names that a green, fresh, challenge-closed `discharge-summary.json`
    // lists; with no summary beside the Lean base, a sorry-free theorem `lean_theorem_names()` resolves. L4 is therefore
    // granted on the GROUNDED count alone; a claim with nothing under it is reported `self-declared` by
    // `is_l4_self_declared`, excluded from the L4 total, and never counted quietly. The `not_applicable`
    // credit still comes from the summary: it is a claim about APPLICABILITY, not about a proof, and it
    // is ONT-8's evidence block that will give it its own provenance.
    let not_applicable = contract
        .verification_summary
        .as_ref()
        .map_or(0, |vs| vs.l4_not_applicable);
    grounded > 0 && grounded + not_applicable >= total
}

/// Returns `true` when the contract CLAIMS a Lean proof its own tree does not ground.
///
/// The claim is the summary's `l4_lean_proved` plus its `l4_not_applicable` covering every obligation —
/// exactly the test that granted L4 before ONT-2a. The grounding is [`count_lean_theorems_for_contract`].
/// A contract that would have been L4 by its own summary and is not L4 by grounding is SELF-DECLARED: the
/// report prints the word beside it, the L4 total excludes it, and ONT-3b is where the credit is earned.
#[must_use]
pub fn is_l4_self_declared(contract: &Contract) -> bool {
    is_l4_self_declared_with_grounding(contract, count_lean_theorems_for_contract(contract))
}

/// [`is_l4_self_declared`] with the grounding count passed in, for the same reason.
#[must_use]
pub fn is_l4_self_declared_with_grounding(contract: &Contract, grounded: u32) -> bool {
    let total = contract.proof_obligations.len() as u32;
    if total == 0 {
        return false;
    }
    let Some(vs) = contract.verification_summary.as_ref() else {
        return false;
    };
    let claim_covers = vs.l4_lean_proved > 0 && vs.l4_lean_proved + vs.l4_not_applicable >= total;
    claim_covers && !is_lean_proved_with_grounding(contract, grounded)
}

/// Obligations declared `applies_to: not_applicable` (PMAT-3091).
///
/// This is a count for the report only. The level computation deliberately
/// does NOT subtract it from the obligation total: tests, kani harnesses and
/// Lean theorems are counted per contract, not linked per obligation, so there
/// is no numerator to remove an N/A obligation from, and removing it from the
/// denominator alone would let a declaration lower the bar for L2/L3/L4. An
/// N/A obligation therefore leaves the level exactly where an undeclared one
/// would. It is also not `verification_summary.l4_not_applicable`: it grants
/// no Lean credit.
#[must_use]
#[allow(clippy::cast_possible_truncation)]
pub fn count_not_applicable(contract: &Contract) -> u32 {
    contract
        .proof_obligations
        .iter()
        .filter(|ob| ob.is_not_applicable())
        .count() as u32
}

/// Returns `true` when all bindings are implemented.
fn is_fully_bound(binding_status: Option<(u32, u32)>) -> bool {
    binding_status.is_some_and(|(implemented, total)| total > 0 && implemented == total)
}

/// Compute the proof level for a single contract.
///
/// Derivation rules (highest matching level wins):
/// - **L5**: every obligation Lean-proved AND all bindings implemented
/// - **L4**: every obligation Lean-proved — strict per-obligation coverage,
///   `proved + not_applicable >= proof_obligations.len()` with `proved > 0`
///   (partial coverage is NOT L4; see [`is_lean_proved`])
/// - **L3**: has Kani harnesses AND falsification tests cover obligations
/// - **L2**: falsification tests count >= obligations count
/// - **L1**: contract exists with equations
#[allow(clippy::cast_possible_truncation)]
pub fn compute_proof_level(contract: &Contract, binding_status: Option<(u32, u32)>) -> ProofLevel {
    compute_proof_level_with_grounding(
        contract,
        binding_status,
        count_lean_theorems_for_contract(contract),
    )
}

/// [`compute_proof_level`] with the grounding count passed in (ONT-2a).
#[allow(clippy::cast_possible_truncation)]
#[must_use]
pub fn compute_proof_level_with_grounding(
    contract: &Contract,
    binding_status: Option<(u32, u32)>,
    grounded: u32,
) -> ProofLevel {
    let total_obligations = contract.proof_obligations.len() as u32;
    let ft_count = contract.falsification_tests.len() as u32;
    let kani_count = contract.kani_harnesses.len() as u32;

    // Check L4/L5: Lean proved
    if is_lean_proved_with_grounding(contract, grounded) {
        return if is_fully_bound(binding_status) {
            ProofLevel::L5
        } else {
            ProofLevel::L4
        };
    }

    // Check L3: Kani + falsification
    let has_tests = ft_count >= total_obligations && total_obligations > 0;
    if kani_count > 0 && has_tests {
        return ProofLevel::L3;
    }

    // Check L2: falsification tests cover obligations
    if has_tests {
        return ProofLevel::L2;
    }

    // L1: contract exists with equations
    ProofLevel::L1
}

/// Directories scanned (relative to CWD) for sorry-free Lean theorem files,
/// in priority order. The IN-TREE staging tree is FIRST — it is the
/// post-APR-MONO source of truth and a superset of the external sibling, so
/// L4/L5 proof levels are reproducible on a fresh clone / CI without a
/// co-located `../provable-contracts` checkout. The bare `lean` and the
/// external sibling are kept as fallbacks for dev machines that still use them.
pub(crate) const LEAN_THEOREM_BASES: &[&str] = &[
    "crates/aprender-contracts-staging/lean",
    "lean",
    "../provable-contracts/lean",
];

/// Register the three naming forms a single label contributes: namespaced, bare, and lowercased.
fn insert_name_forms(names: &mut std::collections::HashSet<String>, label: &str) {
    names.insert(format!("Theorems.{label}"));
    names.insert(label.to_string());
    names.insert(label.to_lowercase());
}

/// `relu_nonneg` → `ReluNonneg`.
pub(crate) fn camel_case(snake: &str) -> String {
    snake
        .split('_')
        .map(|s| {
            let mut c = s.chars();
            match c.next() {
                None => String::new(),
                Some(f) => f.to_uppercase().chain(c).collect(),
            }
        })
        .collect()
}

/// `ReluNonneg` → `Relu`: the leading word of a CamelCase name.
pub(crate) fn first_camel_word(camel: &str) -> String {
    camel
        .chars()
        .enumerate()
        .take_while(|(i, c)| *i == 0 || !c.is_uppercase())
        .map(|(_, c)| c)
        .collect()
}

/// Register every `theorem <name>` a file declares, in the forms a contract may cite it by.
fn insert_theorem_names_from_content(names: &mut std::collections::HashSet<String>, content: &str) {
    for line in content.lines() {
        let Some(pos) = line.find("theorem ") else {
            continue;
        };
        let tname: String = line[pos + 8..]
            .chars()
            .take_while(|c| c.is_alphanumeric() || *c == '_')
            .collect();
        if tname.is_empty() {
            continue;
        }
        let camel = camel_case(&tname);
        names.insert(format!("Theorems.{camel}"));
        names.insert(camel.clone());
        let first_word = first_camel_word(&camel);
        if first_word.len() >= 3 {
            names.insert(format!("Theorems.{first_word}"));
            names.insert(first_word);
        }
    }
}

/// Lean identifier continuation: `sorry_free` and `x.sorry'` are not the `sorry` token.
fn is_lean_ident_byte(c: u8) -> bool {
    c.is_ascii_alphanumeric() || c == b'_' || c == b'\''
}

/// Whether Lean source admits a proof hole: the token `sorry` outside `--` line comments and
/// (nested) `/- -/` block comments (#4351).
///
/// A doc comment that SAYS "compiles sorry-free" admits nothing, and a byte-level `contains("sorry")`
/// denied such files every theorem they prove. The scan still fails CLOSED everywhere else:
/// - a `sorry` inside a string literal counts — a string is code, not commentary;
/// - string and char literals are skipped only so a `"--"` or `'"'` cannot open a fake comment
///   that would hide a real `sorry` after it;
/// - a file that ends inside a comment or string counts — it does not compile, so it proves nothing.
pub(crate) fn lean_has_sorry(content: &str) -> bool {
    let b = content.as_bytes();
    let mut i = 0;
    let mut depth = 0usize;
    while i < b.len() {
        if depth > 0 {
            (i, depth) = step_block_comment(b, i, depth);
            continue;
        }
        match scan_code_at(b, i) {
            LeanScan::Next(j) => i = j,
            LeanScan::OpenBlock(j) => {
                depth = 1;
                i = j;
            }
            LeanScan::Sorry => return true,
            LeanScan::EndsInLineComment => return false,
        }
    }
    depth > 0
}

/// One step of [`lean_has_sorry`] outside a block comment.
enum LeanScan {
    /// Resume scanning at this byte.
    Next(usize),
    /// A `/-` opened a block comment; resume at this byte, inside it.
    OpenBlock(usize),
    /// A `sorry` token was found (or a literal ran off the end of the file).
    Sorry,
    /// A `--` comment runs to EOF: nothing after it can admit a hole.
    EndsInLineComment,
}

/// `sorry` as a whole Lean token at byte `i`.
fn sorry_token_at(b: &[u8], i: usize) -> bool {
    b[i..].starts_with(b"sorry")
        && (i == 0 || !is_lean_ident_byte(b[i - 1]))
        && b.get(i + 5).is_none_or(|&c| !is_lean_ident_byte(c))
}

/// Inside `depth` nested `/- -/` comments: returns the next byte and the new depth.
fn step_block_comment(b: &[u8], i: usize, depth: usize) -> (usize, usize) {
    if b[i..].starts_with(b"/-") {
        (i + 2, depth + 1)
    } else if b[i..].starts_with(b"-/") {
        (i + 2, depth - 1)
    } else {
        (i + 1, depth)
    }
}

/// Classify the lexeme starting at byte `i` of code (not inside any comment).
fn scan_code_at(b: &[u8], i: usize) -> LeanScan {
    let prev_ident = i > 0 && is_lean_ident_byte(b[i - 1]);
    if b[i..].starts_with(b"--") {
        return match b[i..].iter().position(|&c| c == b'\n') {
            Some(p) => LeanScan::Next(i + p + 1),
            None => LeanScan::EndsInLineComment,
        };
    }
    if b[i..].starts_with(b"/-") {
        return LeanScan::OpenBlock(i + 2);
    }
    if b[i] == b'r' && !prev_ident && matches!(b.get(i + 1), Some(b'"' | b'#')) {
        return scan_raw_string(b, i);
    }
    if b[i] == b'"' {
        return scan_string(b, i);
    }
    if b[i] == b'\'' && !prev_ident {
        return LeanScan::Next(skip_char_literal(b, i));
    }
    if sorry_token_at(b, i) {
        LeanScan::Sorry
    } else {
        LeanScan::Next(i + 1)
    }
}

/// A literal's body `[from, to)` counts a `sorry` in it; else resume at `resume`.
fn scan_literal_body(b: &[u8], from: usize, to: usize, resume: usize) -> LeanScan {
    if (from..to).any(|k| sorry_token_at(b, k)) {
        LeanScan::Sorry
    } else {
        LeanScan::Next(resume)
    }
}

/// r"…" / r#"…"#: no escapes, closed by `"` plus the same number of `#`.
fn scan_raw_string(b: &[u8], i: usize) -> LeanScan {
    let hashes = b[i + 1..].iter().take_while(|&&c| c == b'#').count();
    let open = i + 1 + hashes;
    if b.get(open) != Some(&b'"') {
        return LeanScan::Next(i + 1);
    }
    let mut close = vec![b'"'];
    close.extend(std::iter::repeat_n(b'#', hashes));
    let Some(p) = b[open + 1..]
        .windows(close.len())
        .position(|w| w == close.as_slice())
    else {
        return LeanScan::Sorry;
    };
    let end = open + 1 + p;
    scan_literal_body(b, open + 1, end, end + close.len())
}

/// "…" with `\` escapes; an unterminated string does not compile, so it counts.
fn scan_string(b: &[u8], i: usize) -> LeanScan {
    let mut j = i + 1;
    loop {
        match b.get(j) {
            None => return LeanScan::Sorry,
            Some(b'\\') => j += 2,
            Some(b'"') => break,
            Some(_) => j += 1,
        }
    }
    scan_literal_body(b, i + 1, j, j + 1)
}

/// A char literal is at most an escape plus one UTF-8 scalar; anything else is not one.
fn skip_char_literal(b: &[u8], i: usize) -> usize {
    let from = if b.get(i + 1) == Some(&b'\\') {
        i + 3
    } else {
        i + 2
    };
    match b
        .get(from..b.len().min(i + 7))
        .and_then(|s| s.iter().position(|&c| c == b'\''))
    {
        Some(p) => from + p + 1,
        None => i + 1,
    }
}

/// Register the names contributed by one domain directory's sorry-free `.lean` files.
///
/// A file that admits a `sorry` ([`lean_has_sorry`]) contributes NOTHING: an admitted proof grounds no
/// claim, which is the whole reason this scan is the grounding ONT-2a trusts over a contract's own
/// summary. Each file also registers `Theorems.<Domain>.<Stem>`, the `domain.file` form a contract's
/// `lean_theorem:` cites (e.g. `Theorems.GgufExportSymmetry.Roundtrip`, #4351).
fn insert_domain_theorems(names: &mut std::collections::HashSet<String>, domain: &std::path::Path) {
    let domain_name = domain
        .file_name()
        .unwrap_or_default()
        .to_string_lossy()
        .to_string();
    let Ok(files) = std::fs::read_dir(domain) else {
        return;
    };
    for file in files.flatten() {
        let path = file.path();
        if path.extension().is_none_or(|e| e != "lean") {
            continue;
        }
        let Ok(content) = std::fs::read_to_string(&path) else {
            continue;
        };
        if lean_has_sorry(&content) {
            continue;
        }
        let stem = path
            .file_stem()
            .unwrap_or_default()
            .to_string_lossy()
            .to_string();
        names.insert(format!("Theorems.{domain_name}.{stem}"));
        insert_name_forms(names, &domain_name);
        insert_name_forms(names, &stem);
        insert_theorem_names_from_content(names, &content);
    }
}

/// Every theorem name one base directory contributes; empty when the base is absent.
fn scan_theorem_base(base: &str) -> std::collections::HashSet<String> {
    let mut names = std::collections::HashSet::new();
    let search_dir = std::path::Path::new(base).join("ProvableContracts/Theorems");
    if !search_dir.exists() {
        return names;
    }
    let Ok(domains) = std::fs::read_dir(&search_dir) else {
        return names;
    };
    for domain_entry in domains.flatten() {
        let path = domain_entry.path();
        if path.is_dir() {
            insert_domain_theorems(&mut names, &path);
        }
    }
    names
}

/// Build a set of all sorry-free Lean theorem names from the Theorems/ directory.
/// Scans once, caches the result in a thread-local for repeated calls.
fn lean_theorem_names() -> &'static std::collections::HashSet<String> {
    use std::sync::OnceLock;
    static CACHE: OnceLock<std::collections::HashSet<String>> = OnceLock::new();
    CACHE.get_or_init(|| {
        for base in LEAN_THEOREM_BASES {
            let names = scan_theorem_base(base);
            if !names.is_empty() {
                return names;
            }
        }
        std::collections::HashSet::new()
    })
}

/// The L4 grounding this process reads once: the discharge summary beside the first Lean base that has one, or the
/// ONT-2a scan when none does.
struct Grounding {
    source: L4Source,
    discharged: Discharged,
}

fn grounding() -> &'static Grounding {
    use std::sync::OnceLock;
    static CACHE: OnceLock<Grounding> = OnceLock::new();
    CACHE.get_or_init(|| {
        let bases: Vec<&std::path::Path> = LEAN_THEOREM_BASES
            .iter()
            .map(std::path::Path::new)
            .collect();
        grounding_from(&bases, summary::current_tree_sha)
    })
}

/// `grounding()` without the cache, over explicit bases and a tree-sha source, so a test can drive the whole
/// discharge → refinement path. The first base with a summary wins.
fn grounding_from(
    bases: &[&std::path::Path],
    tree_sha: impl Fn(&std::path::Path) -> Option<String>,
) -> Grounding {
    for &dir in bases {
        let path = summary::summary_path(dir);
        if !dir.is_dir() || !path.is_file() {
            continue;
        }
        let mut discharged = match summary::load(&path) {
            Ok(s) => summary::discharged(&s, tree_sha(dir).as_deref()),
            Err(why) => Discharged {
                withheld: Some(why),
                ..Discharged::default()
            },
        };
        refine(dir, &mut discharged);
        return Grounding {
            source: L4Source::Discharge,
            discharged,
        };
    }
    Grounding {
        source: L4Source::SelfDeclared,
        discharged: Discharged::default(),
    }
}

/// ONT-3b (#4073): a discharged theorem stays L4 only when an `extraction`/`simulation` model whose `model_of`
/// resolves covers its module. The workspace walk runs only when the discharge grants something.
fn refine(lean_dir: &std::path::Path, discharged: &mut Discharged) {
    use crate::discharge::refinement;
    if discharged.theorems.is_empty() {
        return;
    }
    let l4 = match refinement::load(lean_dir) {
        Ok(rec) => {
            let modules = discharged.module_of.values().cloned().collect();
            let root = workspace_root(lean_dir);
            refinement::l4_modules(&refinement::judge(
                &rec.models,
                &modules,
                refinement::workspace_resolver(&root),
            ))
        }
        Err(_) => std::collections::BTreeSet::new(),
    };
    discharged.require_refinement(&l4);
}

/// The nearest ancestor of `dir` whose Cargo.toml has a `[workspace]` table, else `.`.
fn workspace_root(dir: &std::path::Path) -> std::path::PathBuf {
    let abs = std::fs::canonicalize(dir).unwrap_or_else(|_| dir.to_path_buf());
    abs.ancestors()
        .find(|a| {
            std::fs::read_to_string(a.join("Cargo.toml"))
                .is_ok_and(|t| t.lines().any(|l| l.trim() == "[workspace]"))
        })
        .map_or_else(
            || std::path::PathBuf::from("."),
            std::path::Path::to_path_buf,
        )
}

/// The discharge summary's grant as this process read it: empty when there is no summary, or it is withheld.
#[must_use]
pub fn discharge_grounding() -> &'static Discharged {
    &grounding().discharged
}

/// EV-8b: the equations whose `lean_theorem` the discharge summary grants. A theorem the YAML names and the summary
/// does not list earns nothing, however the YAML describes it.
#[must_use]
pub fn count_discharged_for_contract(contract: &Contract, discharged: &Discharged) -> u32 {
    let n = contract
        .equations
        .values()
        .filter_map(|eq| eq.lean_theorem.as_deref())
        .filter(|t| discharged.grants(t))
        .count();
    u32::try_from(n).unwrap_or(u32::MAX)
}

/// The grounding count for a contract: from the discharge summary when one exists, else the ONT-2a scan.
fn count_lean_theorems_for_contract(contract: &Contract) -> u32 {
    let g = grounding();
    match g.source {
        L4Source::Discharge => count_discharged_for_contract(contract, &g.discharged),
        L4Source::SelfDeclared => count_scanned_theorems_for_contract(contract),
    }
}

/// Count Lean theorems for a contract by matching `lean_theorem` refs against
/// sorry-free `.lean` files in the Theorems/ directory.
fn count_scanned_theorems_for_contract(contract: &Contract) -> u32 {
    let theorems = lean_theorem_names();
    let mut count = 0u32;
    for eq in contract.equations.values() {
        if let Some(ref theorem_ref) = eq.lean_theorem {
            let name = theorem_ref.trim().trim_matches('"');
            // Try exact match, then without prefix, then lowercase
            if theorems.contains(name)
                || theorems.contains(name.strip_prefix("Theorems.").unwrap_or(name))
                || theorems.contains(&name.to_lowercase())
            {
                count += 1;
            }
        }
    }
    count
}

/// Build a complete proof status report.
///
/// `contracts` is a list of `(stem, &Contract)` pairs.
/// `binding` is an optional binding registry for binding coverage.
/// `include_classes` controls whether kernel class summaries are generated.
#[allow(clippy::cast_possible_truncation)]
pub fn proof_status_report(
    contracts: &[(String, &Contract)],
    binding: Option<&BindingRegistry>,
    include_classes: bool,
) -> ProofStatusReport {
    let mut statuses = Vec::new();
    let mut totals = ProofStatusTotals {
        contracts: contracts.len() as u32,
        obligations: 0,
        not_applicable: 0,
        falsification_tests: 0,
        kani_harnesses: 0,
        lean_proved: 0,
        lean_grounded: 0,
        l4_self_declared: 0,
        bindings_implemented: 0,
        bindings_total: 0,
    };

    for (stem, contract) in contracts {
        let contract_file = format!("{stem}.yaml");

        let obligations = contract.proof_obligations.len() as u32;
        let not_applicable = count_not_applicable(contract);
        let ft_count = contract.falsification_tests.len() as u32;
        let kani_count = contract.kani_harnesses.len() as u32;
        // The CLAIM (what the contract says about itself) and the GROUNDING (what the tree shows) are two
        // numbers since ONT-2a; before it, the first stood in for the second whenever it was non-zero.
        let lean_proved = contract
            .verification_summary
            .as_ref()
            .map_or(0, |vs| vs.l4_lean_proved);
        let lean_grounded = count_lean_theorems_for_contract(contract);
        let lean_proved = if lean_proved == 0 {
            lean_grounded
        } else {
            lean_proved
        };
        let l4_self_declared = is_l4_self_declared_with_grounding(contract, lean_grounded);

        // Count bindings for this contract
        let (b_impl, b_total) = if let Some(reg) = binding {
            count_bindings(&contract_file, contract, reg)
        } else {
            (0, contract.equations.len() as u32)
        };

        let binding_status = if binding.is_some() {
            Some((b_impl, b_total))
        } else {
            None
        };

        let proof_level =
            compute_proof_level_with_grounding(contract, binding_status, lean_grounded);

        totals.obligations += obligations;
        totals.not_applicable += not_applicable;
        totals.falsification_tests += ft_count;
        totals.kani_harnesses += kani_count;
        totals.lean_proved += lean_proved;
        totals.lean_grounded += lean_grounded;
        totals.l4_self_declared += u32::from(l4_self_declared);
        totals.bindings_implemented += b_impl;
        totals.bindings_total += b_total;

        statuses.push(ContractProofStatus {
            stem: stem.clone(),
            proof_level,
            obligations,
            not_applicable,
            falsification_tests: ft_count,
            kani_harnesses: kani_count,
            lean_proved,
            lean_grounded,
            l4_self_declared,
            bindings_implemented: b_impl,
            bindings_total: b_total,
        });
    }

    // Build kernel class summaries
    let kernel_classes = if include_classes {
        build_kernel_classes(&statuses)
    } else {
        Vec::new()
    };

    let timestamp = current_timestamp();

    ProofStatusReport {
        schema_version: "1.0.0".to_string(),
        l4_self_declared_excluded: true,
        l4_source: grounding().source,
        l4_withheld: grounding().discharged.withheld.clone(),
        timestamp,
        contracts: statuses,
        kernel_classes,
        totals,
    }
}

/// Format a proof status report as human-readable text.
pub fn format_text(report: &ProofStatusReport) -> String {
    let mut out = String::new();

    out.push_str(&format!(
        "Proof Status ({} contracts)\n\n",
        report.totals.contracts
    ));

    out.push_str(&format!(
        "  {:<35} {:>5} {:>6} {:>5} {:>4} {:>4} {:>9} {:>13}\n",
        "Contract", "Level", "Obligs", "Tests", "Kani", "Lean", "Bindings", "L4 evidence"
    ));
    out.push_str(&format!("  {}\n", "─".repeat(86)));

    for c in &report.contracts {
        // ONT-2a: the andon is a COLUMN, not a footnote. A claim the tree does not ground says so on its
        // own line, beside the level it no longer reaches.
        let l4_evidence = if c.l4_self_declared {
            "self-declared"
        } else if c.lean_grounded > 0 {
            "grounded"
        } else {
            "-"
        };
        out.push_str(&format!(
            "  {:<35} {:>5} {:>6} {:>5} {:>4} {:>4} {:>4}/{:<4} {:>13}\n",
            truncate(&c.stem, 35),
            c.proof_level,
            c.obligations,
            c.falsification_tests,
            c.kani_harnesses,
            c.lean_proved,
            c.bindings_implemented,
            c.bindings_total,
            l4_evidence,
        ));
    }

    if !report.kernel_classes.is_empty() {
        out.push_str("\nKernel Classes:\n");
        for kc in &report.kernel_classes {
            let bound_str = if kc.all_bound { "all bound" } else { "gaps" };
            out.push_str(&format!(
                "  {} ({}): min={}, {} contracts, {}\n",
                kc.label,
                kc.description,
                kc.min_proof_level,
                kc.contract_stems.len(),
                bound_str,
            ));
        }
    }

    out.push_str(&format!(
        "\nTotals: {} obligations ({} N/A, never counted as proved), {} tests, {} kani, {} lean claimed ({} grounded), {}/{} bound\n\
         L4 evidence: {} contract(s) self-declared and excluded from L4 (ONT-2a andon); grounded means a \
         theorem the equation names that a green, fresh discharge-summary.json lists (EV-8b), or with no summary \
         a sorry-free in-tree Lean theorem\n",
        report.totals.obligations,
        report.totals.not_applicable,
        report.totals.falsification_tests,
        report.totals.kani_harnesses,
        report.totals.lean_proved,
        report.totals.lean_grounded,
        report.totals.bindings_implemented,
        report.totals.bindings_total,
        report.totals.l4_self_declared,
    ));
    let source = match report.l4_source {
        L4Source::Discharge => "discharge (discharge-summary.json)",
        L4Source::SelfDeclared => "self-declared (no discharge-summary.json; in-tree .lean scan)",
    };
    out.push_str(&format!("L4 source: {source}\n"));
    if let Some(why) = &report.l4_withheld {
        out.push_str(&format!("L4 withheld: {why}\n"));
    }

    out
}

// ── Internal helpers ──────────────────────────────────────────────

/// Count implemented vs total bindings for a contract in the registry
#[allow(clippy::cast_possible_truncation)]
pub(crate) fn count_bindings(
    contract_file: &str,
    contract: &Contract,
    binding: &BindingRegistry,
) -> (u32, u32) {
    let total = contract.equations.len() as u32;
    let implemented = binding
        .bindings_for(contract_file)
        .iter()
        .filter(|b| b.status == ImplStatus::Implemented)
        .count() as u32;
    (implemented, total)
}

/// Build kernel equivalence class summaries from per-contract statuses
fn build_kernel_classes(statuses: &[ContractProofStatus]) -> Vec<KernelClassSummary> {
    let status_map: BTreeMap<&str, &ContractProofStatus> =
        statuses.iter().map(|s| (s.stem.as_str(), s)).collect();

    kernel_class_map()
        .into_iter()
        .map(|(label, desc, stems)| {
            let found_stems: Vec<String> = stems
                .iter()
                .filter(|s| status_map.contains_key(**s))
                .map(|s| (*s).to_string())
                .collect();

            let min_level = found_stems
                .iter()
                .filter_map(|s| status_map.get(s.as_str()))
                .map(|c| c.proof_level)
                .min()
                .unwrap_or(ProofLevel::L1);

            let all_bound = !found_stems.is_empty()
                && found_stems.iter().all(|s| {
                    status_map.get(s.as_str()).is_some_and(|c| {
                        c.bindings_total > 0 && c.bindings_implemented == c.bindings_total
                    })
                });

            KernelClassSummary {
                label: label.to_string(),
                description: desc.to_string(),
                contract_stems: found_stems,
                min_proof_level: min_level,
                all_bound,
            }
        })
        .collect()
}

/// Truncate a string to at most `max` bytes for column alignment
fn truncate(s: &str, max: usize) -> &str {
    if s.len() > max {
        &s[..max]
    } else {
        s
    }
}

/// Generate an ISO-8601-style Unix epoch timestamp string
fn current_timestamp() -> String {
    // Use a simple ISO-8601 timestamp without external deps.
    // In production this would use chrono or time crate.
    // For now we use std::time for a Unix epoch string.
    let duration = std::time::SystemTime::now()
        .duration_since(std::time::UNIX_EPOCH)
        .unwrap_or_default();
    format!("{}Z", duration.as_secs())
}

#[cfg(test)]
#[path = "proof_status_tests.rs"]
mod tests;