provable_contracts/lint/

mod.rs

//! Contract quality gate: validate + audit + score in one pass.
//!
//! Runs three sequential gates across all contracts in a directory:
//! 1. **validate** — schema completeness (SCHEMA-001..013, PROVABILITY-001)
//! 2. **audit** — traceability chain (paper→equation→obligation→test→proof)
//! 3. **score** — 5-dimension quality score vs threshold
//!
//! Extended with SARIF output, rule catalog, config file, and findings.
//! Spec: `docs/specifications/sub/lint.md`

pub mod cache;
pub mod capability_cells_gate;
mod composition_gate;
pub mod config;
pub mod consistency_gate;
pub mod diff;
pub mod duplicate_stems;
pub mod evidence_gate;
pub mod finding;
mod gates;
pub use gates::collect_yaml_files;
pub mod bindings_gate;
mod gates_extended;
pub mod ratchet_gates;
pub mod refinement_gate;
pub mod refines_gate;
pub mod relations_gate;
pub mod rules;
pub mod sarif;
pub mod shapes_gate;
pub mod sigma_gate;
pub mod sigma_symbols;
mod strict_test_binding;
pub mod subsumption;
pub mod tbox_gate;
pub mod trend;
pub mod valid_under_gate;

use std::collections::{HashMap, HashSet};
use std::path::Path;
use std::time::Instant;

use serde::Serialize;

use self::finding::LintFinding;
use self::gates::{
    load_binding, load_contracts, run_audit_gate, run_score_gate, run_validate_gate,
};
use self::gates_extended::{
    check_stale_suppressions, run_enforce_gate, run_enforcement_level_gate,
    run_reverse_coverage_gate, run_verify_gate,
};
use self::rules::RuleSeverity;
use crate::ontology::arming::{meet_armed, ArmedGates};
use crate::ontology::verdict::Verdict;

/// Result of a single gate execution.
#[derive(Debug, Clone, Serialize)]
pub struct GateResult {
    pub name: String,
    pub passed: bool,
    pub skipped: bool,
    /// ONT-001 §3.4: this gate's element of the one verdict lattice (`Verdict::from_gate(passed, skipped)`).
    pub verdict: Verdict,
    pub duration_ms: u64,
    pub detail: GateDetail,
    /// Structured payload for gates invented AFTER `GateDetail` was frozen.
    ///
    /// See [`GateExtra`] for why this second channel exists. Adding a field to a
    /// struct is invisible to a `match` on `GateDetail`, which is the property
    /// the 0.3.1 compatibility corpus depends on; adding a *variant* is not.
    /// Serialised only when present, so existing JSON output is unchanged.
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub extra: Option<GateExtra>,
}

/// Gate-specific detail payload.
///
/// # This enum is FROZEN at the eight variants published in `provable-contracts`
/// 0.3.1 — do not add a ninth
///
/// `GateDetail` is public, is not `#[non_exhaustive]`, and 0.3.1 shipped 28 example
/// programs that `match` it exhaustively. Those programs are vendored verbatim under
/// `crates/facades/provable-contracts/compat/0.3.1/`, sha256-verified against their
/// published checksums by `scripts/check_facade_compat.sh` (row R6), and compiled in
/// the `ci` job that the required `gate` check depends on. A ninth variant is
/// `error[E0004]` in that corpus, and the corpus cannot be edited to accommodate it —
/// being uneditable is the whole point of a compatibility contract. Marking the enum
/// `#[non_exhaustive]` does not help either: it makes the *existing* exhaustive
/// matches non-exhaustive, which is the same compile error for the same reason.
///
/// So the vocabulary is closed. A gate added after 0.3.1 picks the truest of these
/// eight for `detail` and carries its own shape in [`GateResult::extra`], which is a
/// type 0.3.1 never names and is therefore free to grow.
#[derive(Debug, Clone, Serialize)]
#[serde(tag = "type")]
pub enum GateDetail {
    #[serde(rename = "validate")]
    Validate {
        contracts: usize,
        errors: usize,
        warnings: usize,
        error_messages: Vec<String>,
    },
    #[serde(rename = "audit")]
    Audit {
        contracts: usize,
        findings: usize,
        finding_messages: Vec<String>,
    },
    #[serde(rename = "score")]
    Score {
        contracts: usize,
        min_score: f64,
        mean_score: f64,
        threshold: f64,
        below_threshold: Vec<String>,
    },
    #[serde(rename = "verify")]
    Verify {
        total_refs: usize,
        existing: usize,
        missing: usize,
    },
    #[serde(rename = "enforce")]
    Enforce {
        equations_total: usize,
        equations_with_pre: usize,
        equations_with_post: usize,
        equations_with_lean: usize,
    },
    #[serde(rename = "reverse_coverage")]
    ReverseCoverage {
        total_pub_fns: usize,
        bound_fns: usize,
        unbound_fns: usize,
        coverage_pct: f64,
        threshold_pct: f64,
    },
    #[serde(rename = "composition")]
    Composition {
        edges_checked: usize,
        edges_satisfied: usize,
        edges_broken: usize,
    },
    #[serde(rename = "skipped")]
    Skipped { reason: String },
}

/// The `shapes` gate's positive controls and ONT-4c5's cell report — one boxed, flattened block of
/// [`GateExtra::Shapes`].
#[derive(Debug, Clone, Serialize)]
pub struct ShapesControls {
    /// The extractor positive controls: `gguf` (corrupt magic refused), `apr-model` (lying header refused).
    pub pc_extract: std::collections::BTreeMap<String, String>,
    /// ONT-4c5: per-shape positive controls (`capability-cells` → `fired`); the gate never reaches `Ran` with
    /// one that is not.
    pub pc_shapes: std::collections::BTreeMap<String, String>,
    /// ONT-4c5: the capability-cell domain D and its NotRun cells at the current release — absent unless a
    /// contract declares the `capability-cells` shape.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub capability_cells: Option<capability_cells_gate::CapabilityCellsReport>,
}

/// Out-of-band structured detail for gates that post-date the frozen [`GateDetail`]
/// vocabulary.
///
/// This type did not exist in `provable-contracts` 0.3.1, so no 0.3.1 program names
/// it and none can `match` it. That is what makes it extensible where `GateDetail` is
/// not, and it is `#[non_exhaustive]` from birth so the *next* post-0.3.1 gate does
/// not have to repeat this exercise.
// `Shapes` is 304 bytes against a 88-byte second-largest, and adding `declines` to it is what
// crossed the threshold — `origin/main` at 237fbc32f lints clean, this branch does not, so the
// finding is this PR's and not inherited.
//
// ALLOWED RATHER THAN BOXED, deliberately. `large_enum_variant` is a cost heuristic about copying
// and stack size: a `GateExtra` is built ONCE PER GATE RUN, moved a handful of times, and then
// serialised. There is no hot path here for 216 bytes to matter on, so the lint is measuring a cost
// this type does not pay.
//
// The alternatives are worse. Boxing one field (clippy suggests `pc_extract`) reclaims 16 bytes and
// does not clear the ratio, so it would be churn that silences nothing. Boxing the whole payload —
// `Shapes(Box<ShapesExtra>)` — turns a struct variant into a newtype variant, which CHANGES THE
// SERDE REPRESENTATION of a `#[serde(tag = "type")]` enum that downstream consumers parse; the SLK
// gate reads this JSON. Breaking a wire format to satisfy a stack-size heuristic is the wrong trade.
//
// If `GateExtra` ever ends up in a loop or a large collection, this allow is the thing to revisit.
#[allow(clippy::large_enum_variant)]
#[derive(Debug, Clone, Serialize)]
// One value per `pv lint` run, built once and serialised: the Shapes variant's size is not a hot-path cost.
#[serde(tag = "type")]
#[non_exhaustive]
pub enum GateExtra {
    /// PV-DUP-001: contract stems claimed by several files with divergent content.
    #[serde(rename = "duplicate_stems")]
    DuplicateStems {
        /// Total ambiguous stems found in the tree.
        divergent: usize,
        /// How many of those are recorded in the ratchet baseline.
        baselined: usize,
        /// Ambiguous stems NOT in the baseline — these fail the gate.
        unbaselined: Vec<String>,
        /// Baseline entries that no longer diverge — these fail the gate too.
        stale: Vec<String>,
        /// Every ambiguous stem, with its variant count and paths, for the report.
        divergent_stems: Vec<String>,
    },
    /// ONT-2b: what Σ declares and what the corpus was checked against.
    #[serde(rename = "sigma")]
    Sigma {
        /// `entity_types` Σ declares.
        entity_types: usize,
        /// `roles` Σ declares.
        roles: usize,
        /// `symbols` Σ declares.
        symbols: usize,
        /// Contract files read (never counting `ontology.yaml` itself).
        contracts_checked: usize,
        /// Findings: undeclared entity types, undeclared roles, undeclared glyphs.
        violations: usize,
        /// `formal:` expressions read.
        formal_total: usize,
        /// Of those, how many carry NO symbol Σ declares — the `formal_prose` debt, shrink-only.
        formal_prose: usize,
    },
    /// ONT-4: the corpus's typed relations, checked against Σ's roles.
    #[serde(rename = "relations")]
    Relations {
        /// Typed edges after symmetric closure.
        relations_n: usize,
        /// Contracts carrying a `relations:` block.
        contracts_with_relations: usize,
        /// `role=count` per role used.
        roles_used: Vec<String>,
        /// Cycles through acyclic roles, as `role: a -> b -> a`.
        cycles: Vec<String>,
        /// `metadata.depends_on` edges, read and counted, never rewritten (R-5).
        legacy_depends_on: usize,
        /// Of those, how many name no contract — ratcheted shrink-only in the baseline.
        legacy_unresolved_depends_on: usize,
        /// Findings.
        violations: usize,
    },
    /// ONT-8: one evidence block — PROV-O names, one L-enum, every entity type.
    #[serde(rename = "evidence")]
    Evidence {
        /// Contract files read.
        contracts_checked: usize,
        /// Of those, how many carry an `evidence` block.
        contracts_with_evidence: usize,
        /// Distinct `entity.type` among the contracts carrying evidence — counted, never branched on (R-17).
        entity_types_checked: usize,
        /// Those types, sorted.
        entity_types: Vec<String>,
        /// `enum`: levels are parsed through `ProofLevel`, never matched against a list kept in the gate.
        levels_source: String,
        /// `level=count` over the evidence blocks that passed every rule.
        by_level: Vec<String>,
        /// The census `git_sha` a `[V]` claim binds to; `None` (the 2026-09-16 ruling) binds it to the repository.
        census_git_sha: Option<String>,
        /// `[V]` shas git could not look for — non-zero makes the verdict `Unknown{ToolAbsent}`, never `Pass`.
        unresolved_git_shas: usize,
        /// Findings.
        violations: usize,
    },
    /// ONT-7: kernel-kind contracts carry a world index (`metadata.valid_under.world`, a key of Σ's `worlds`).
    #[serde(rename = "valid_under")]
    ValidUnder {
        /// The worlds Σ declares — the index a `valid_under.world` must resolve into.
        worlds: Vec<String>,
        /// Contract files read.
        contracts_checked: usize,
        /// Of those, kernel-kind and not a registry — the class the row obliges.
        kernel_contracts: usize,
        /// Contracts (any kind) carrying `metadata.valid_under`.
        contracts_with_valid_under: usize,
        /// Kernel-kind contracts carrying none — the debt, shrink-only against the baseline.
        contracts_without_valid_under: usize,
        /// The top-level `contracts_without_valid_under` in `lint-baseline.json`; `None` = not recorded.
        baseline: Option<usize>,
        /// `world=count` over the contracts whose `valid_under` passed every rule.
        by_world: Vec<String>,
        /// Findings.
        violations: usize,
    },
    /// PVL-001 EV-11: Lean theorem modules named by a book page — the `unpaired_theorem_modules` ratchet.
    #[serde(rename = "theorem_pairing")]
    TheoremPairing {
        /// The Lean base the modules were read under.
        lean_base: String,
        /// `.md` pages read under the book roots.
        book_pages: usize,
        /// `.lean` files under `<base>/ProvableContracts/Theorems/`.
        theorem_modules: usize,
        /// Of those, named in full by at least one book page.
        paired: usize,
        /// The debt, shrink-only against the baseline.
        unpaired_theorem_modules: usize,
        /// The top-level `unpaired_theorem_modules` in `lint-baseline.json`; `None` = not recorded (reported only).
        baseline: Option<usize>,
        /// The unpaired modules, dotted, in byte order.
        unpaired: Vec<String>,
        /// Findings.
        violations: usize,
    },
    /// PVL-001 EV-11: kernel-kind contracts with an empty `metadata.depends_on` — the ratchet.
    #[serde(rename = "depends_on_present")]
    DependsOnPresent {
        /// Contract files parsed.
        contracts_checked: usize,
        /// Of those, kernel-kind and not a registry.
        kernel_contracts: usize,
        /// Kernel-kind contracts whose `metadata.depends_on` is empty — the debt, shrink-only.
        contracts_without_depends_on: usize,
        /// The top-level `contracts_without_depends_on` in `lint-baseline.json`; `None` = not recorded (reported only).
        baseline: Option<usize>,
        /// Findings.
        violations: usize,
    },
    /// PVL-001 EV-8a (#4202): `status: proved` claims no green `discharge-summary.json` derives — the ratchet.
    #[serde(rename = "proved_is_derived")]
    ProvedIsDerived {
        /// The summary read (beside the Lean base); `None` = no Lean base.
        summary: Option<String>,
        /// Why it derived nothing when it could not be read; `None` = it was read.
        summary_error: Option<String>,
        /// Every Lean step ran and passed. Only a green summary derives a claim.
        summary_green: bool,
        /// Contract files parsed.
        contracts_checked: usize,
        /// `proof_obligations[].lean.status: proved` claims.
        proved_claims: usize,
        /// Of those, not derived — the debt, shrink-only against the baseline, and it must reach 0.
        underived_proved_claims: usize,
        /// The top-level `underived_proved_claims` in `lint-baseline.json`; `None` = not recorded (reported only).
        baseline: Option<usize>,
        /// The underived claims, as `contract: theorem`, in contract order.
        underived: Vec<String>,
        /// Findings.
        violations: usize,
    },
    /// PVL-001 EV-7a (#4200): `<lean>/Challenge/` against its regeneration (`pv challenge check`).
    #[serde(rename = "challenge_fresh")]
    ChallengeFresh {
        /// The Lean dir judged.
        lean_dir: String,
        /// Challenge files the contracts render.
        files: usize,
        /// Extra, missing or differing files, one line each.
        stale: Vec<String>,
        /// Bound roots whose statement could not be lifted, as `contract: fqn: why`.
        unrestated: Vec<String>,
    },
    /// ONT-4b: the shapes gate — every `shape:` block over the extracted graph, with the plant.
    #[serde(rename = "shapes")]
    Shapes {
        /// `shape:` blocks read.
        shapes_n: usize,
        /// Distinct focus nodes across the shapes (the plant excluded).
        focus_nodes_n: usize,
        /// `fired` — the plant drew a violation; the gate never reaches `Ran` otherwise.
        pc_shape: String,
        /// How many violations the plant drew.
        plant_violations: usize,
        /// Corpus violations (the plant excluded).
        violations: usize,
        /// Corpus warnings.
        warnings: usize,
        /// `shape=focus-count` per shape.
        by_shape: Vec<String>,
        /// Triples in the extracted graph.
        triples: usize,
        /// ONT-4c1 (§3.9 per-shape arming): shapes that feed the verdict, in corpus order.
        armed_shapes: Vec<String>,
        /// Shapes computed and reported but not armed — their violations are in `unarmed_violations`.
        not_armed_shapes: Vec<String>,
        /// #3610: shapes that graded ZERO focus nodes, named — the reach the gate did not have.
        ///
        /// A separate list from `not_armed_shapes` on purpose. "Not armed by policy" and "armed and
        /// measured nothing" are different facts, and folding the second into the first would file a
        /// vacuity as a deliberate choice — which is how the defect hid in the first place.
        ///
        /// **This carries EVERY shape that graded zero, armed or unarmed**, and it is the only list
        /// any of them appears in: a vacuity is in neither `armed_shapes` (the tool's claim about
        /// what it MEASURED) nor `not_armed_shapes` (a policy choice it never made).
        ///
        /// The two differ in what they do to the verdict, not in whether they are listed here. An
        /// ARMED vacuity drives the verdict to `Unknown(NoFocus)` and the run declines — unless an
        /// armed shape that DID grade something found a violation, in which case the verdict is
        /// `Fail` (a measured violation outranks a vacuity, #3622). An UNARMED one leaves the
        /// verdict alone, because it never fed it. Both are named, because a reader
        /// needs to know the gate looked at nothing for them either way.
        ///
        /// An earlier draft of this comment said an armed vacuity "does not reach here at all",
        /// which was false — nothing returns early at the verdict, and both kinds reach this field.
        /// A quorum lane caught the sentence; the code beside it had the matching bug.
        declines: Vec<String>,
        /// Violations from unarmed shapes (named in the findings as warnings; never in the meet).
        unarmed_violations: usize,
        /// Focus nodes each extractor produced: `pv-contract`, `gguf`, `apr-model`.
        by_entity_type: std::collections::BTreeMap<String, usize>,
        /// The positive controls (`pc_extract`, `pc_shapes`) and ONT-4c5's `capability_cells`, boxed and
        /// FLATTENED: the JSON keys stay top-level where the §5 probes read them, and the variant stays under
        /// clippy's large-enum-variant bound (it sat exactly at it before ONT-4c5).
        #[serde(flatten)]
        controls: Box<ShapesControls>,
        /// Ladder receipt files read under `evidence/dogfood/models/`.
        receipts: usize,
        /// Receipt rows whose `sha256` equals a rung's.
        witnesses: usize,
        /// Receipt rows whose `sha256` differs from the rung's.
        hex_mismatches: usize,
        /// Receipt rows without a `sha256` (never a witness).
        unmeasured_rows: usize,
        /// ONT-4b2: vendored W3C SHACL-Core cases that passed this run, and how many are vendored.
        w3c_cases_passed: usize,
        w3c_cases_n: usize,
        /// The ONT-4b2 extractor counters and ONT-4d's inheritance, FLATTENED into this object: the JSON keys
        /// (`symbols_resolved`, …, `inherited_shapes_applied`) are unchanged. They are boxed only so the variant
        /// stays under clippy's `large_enum_variant` once ONT-4d's two fields joined it.
        #[serde(flatten)]
        counters: Box<ShapesCounters>,
        /// aprender#3715: what `extract:release-evidence` derived — absent unless a release subject was given.
        #[serde(skip_serializing_if = "Option::is_none")]
        release: Option<Box<crate::ontology::extract::release_evidence::ReleaseStats>>,
        /// ONT-4c (v4.14): the README claim commands a merge-path workflow runs — the MEASURED set F-33 compares.
        readme: MeasuredSet,
        /// ONT-4c (v4.14): the same for `CLAUDE.md` (`extract:llm-context`).
        claude_md: MeasuredSet,
        /// ONT-4c (v4.14): whether the measured-set ratchets (F-33 and F-34) were checked this run.
        ratchets: Ratchets,
    },
    /// ONT-5: the typed relations are jointly satisfiable, by a witness pv-sat wrote and this run re-checked.
    #[serde(rename = "ont_consistency")]
    Consistency {
        /// Clauses a typed relation produced (`depends_on`/`refines` implications, `contradicts` conflicts).
        checkable_n: usize,
        /// Contracts asserted in force (every id no contract supersedes).
        units: usize,
        /// Typed edges through a role the encoding does not name.
        unencoded_edges: usize,
        /// `fired` — the checker refused the corrupt-core fixture this run.
        pc_checker: String,
        /// The contracts of a checked unsat core; empty when the witness is a model.
        core: Vec<String>,
        /// Findings.
        violations: usize,
        /// The witness this run checked.
        witness: consistency_gate::WitnessReport,
    },
    /// ONT-4e (R-20): every `A refines B` is Liskov, by a witness pv-sat wrote and this run re-checked.
    #[serde(rename = "refines")]
    Refines(Box<refines_gate::RefinesCounters>),
    /// ONT-3a: every implemented/partial binding resolves to workspace code, or the allowlist names it.
    #[serde(rename = "bindings")]
    Bindings(Box<bindings_gate::BindingsCounters>),
    /// ONT-3b: every `model_of` resolves, and the unrefined-module count holds its shrink-only baseline.
    #[serde(rename = "refinement")]
    Refinement(Box<refinement_gate::RefinementCounters>),
}

/// Counters a `shapes` run reports, flattened into [`GateExtra::Shapes`]'s JSON.
#[derive(Debug, Clone, Default, Serialize)]
pub struct ShapesCounters {
    /// ONT-4b2: bound Rust symbols the `syn` walk resolved / could not resolve.
    pub symbols_resolved: usize,
    pub symbols_unresolved: usize,
    /// ONT-4b2: Lean theorems extracted, and contract `lean_theorem:` references naming none of them.
    pub lean_statements: usize,
    pub lean_refs_unresolved: usize,
    /// ONT-4d (R-19): applications of a shape to instances of a strict sub-concept of its target, summed over shapes. Such a
    /// node may ALSO be typed the target directly (`pv_contract` asserts `ont:Contract` on every contract), so
    /// this counts the hierarchy being applied, not reach that exists only through it. The fixture
    /// `subsumption-inherit` is where inheritance is the ONLY path.
    pub inherited_shapes_applied: usize,
    /// `<shape> <- <sub-concept>=<n>` for each shape inherited down the hierarchy, sorted.
    pub inherited_by_shape: Vec<String>,
}

/// ONT-4c: one measured claim set, sorted.
#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)]
pub struct MeasuredSet {
    pub verified_commands: Vec<String>,
}

/// ONT-4c: `measured_sets` is `checked` only when F-34 ran against a comparand (the CLI resolves it from git);
/// outside a work tree it is `not-checked`, which a probe must read as RED, never as a pass.
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
pub struct Ratchets {
    pub measured_sets: String,
}

impl Default for Ratchets {
    fn default() -> Self {
        Self {
            measured_sets: "not-checked".into(),
        }
    }
}

/// Overall lint report.
#[derive(Debug, Clone, Serialize)]
pub struct LintReport {
    pub passed: bool,
    pub gates: Vec<GateResult>,
    pub total_duration_ms: u64,
    #[serde(skip_serializing_if = "Vec::is_empty")]
    pub findings: Vec<LintFinding>,
    #[serde(skip)]
    pub cache_stats: cache::CacheStats,
    /// Per-contract processing times: `(contract_stem, duration_ms)`.
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub contract_timings: Vec<(String, u64)>,
    /// ONT-001 §3.9: the meet over the armed gates — what the exit code reports. `passed` is the legacy
    /// every-gate-passed-or-skipped flag and is kept unchanged for existing readers.
    pub verdict: Verdict,
    /// Each armed gate, in armed order, with the verdict it contributed (`Unknown(NotRun)` if it did not run).
    pub armed_gates: Vec<ArmedGateVerdict>,
    /// Gates that ran but are not armed: printed as `Unknown(NotArmed)` and excluded from the meet.
    pub not_armed: Vec<String>,
    /// The `armed_gates` monotone check, as the CLI measured it; `None` when nothing checked it.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub armed_monotone: Option<String>,
    /// ONT-4c1: the `armed_shapes` monotone check, as the CLI measured it.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub armed_shapes_monotone: Option<String>,
}

/// One armed gate's contribution to [`LintReport::verdict`].
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
pub struct ArmedGateVerdict {
    pub name: String,
    pub verdict: Verdict,
}

impl LintReport {
    /// Recompute the meet over `armed`. Gates that ran but are not armed are listed in `not_armed`.
    pub fn arm(&mut self, armed: &ArmedGates) {
        let results: Vec<(String, Verdict)> = self
            .gates
            .iter()
            .map(|g| (g.name.clone(), g.verdict))
            .collect();
        let meet = meet_armed(&results, armed);
        self.verdict = meet.verdict;
        self.armed_gates = meet
            .armed
            .into_iter()
            .map(|(name, verdict)| ArmedGateVerdict { name, verdict })
            .collect();
        self.not_armed = meet.not_armed;
    }
}

/// Configuration for `pv lint`.
pub struct LintConfig<'a> {
    pub contract_dir: &'a Path,
    pub binding_path: Option<&'a Path>,
    pub min_score: f64,
    pub severity_filter: Option<RuleSeverity>,
    pub severity_overrides: HashMap<String, RuleSeverity>,
    pub suppressed_findings: Vec<String>,
    pub suppressed_rules: Vec<String>,
    pub suppressed_files: Vec<String>,
    pub strict: bool,
    pub no_cache: bool,
    pub cache_stats: bool,
    /// Optional crate directory for reverse coverage gate (Gate 7).
    pub crate_dir: Option<&'a Path>,
    /// Minimum enforcement level for Gate 6 (from `--min-level`).
    pub min_level: Option<crate::schema::EnforcementLevel>,
    /// Enable Gate 9 (strict test-binding, PV-VER-002). Issue #1510.
    pub strict_test_binding: bool,
    /// Run only gate 1 (validate, the precondition) and the strict test-binding gate; gates 2-22 do not
    /// run and nothing is cached (aprender#4974). Every armed gate that did not run meets as `NotRun`,
    /// so the report can never read as a full-lint pass. Requires `strict_test_binding`.
    pub strict_test_binding_only: bool,
}

impl<'a> LintConfig<'a> {
    /// Create a basic config (backward compatible).
    pub fn new(contract_dir: &'a Path, binding_path: Option<&'a Path>, min_score: f64) -> Self {
        Self {
            contract_dir,
            binding_path,
            min_score,
            severity_filter: None,
            severity_overrides: HashMap::new(),
            suppressed_findings: Vec::new(),
            suppressed_rules: Vec::new(),
            suppressed_files: Vec::new(),
            strict: false,
            no_cache: false,
            cache_stats: false,
            crate_dir: None,
            min_level: None,
            strict_test_binding: false,
            strict_test_binding_only: false,
        }
    }
}

/// Run one gate and record it, or record it as skipped when gate 1 (validate) failed.
///
/// Every gate after validate repeats the same `if validation_passed { run } else
/// { skipped_gate(name, "validation failed") }` shape; this is that shape, once.
fn push_gate<F>(
    gates: &mut Vec<GateResult>,
    all_findings: &mut Vec<LintFinding>,
    run: F,
    name: &str,
    validation_passed: bool,
) where
    F: FnOnce() -> (GateResult, Vec<LintFinding>),
{
    let (result, mut findings) = if validation_passed {
        run()
    } else {
        (skipped_gate(name, "validation failed"), Vec::new())
    };
    gates.push(result);
    all_findings.append(&mut findings);
}

/// Per-contract timing: measure how long each contract's findings take to process,
/// sorted by duration descending.
fn per_contract_timings(
    contracts: &[(String, crate::schema::Contract)],
    binding: Option<&crate::binding::BindingRegistry>,
) -> Vec<(String, u64)> {
    let mut contract_timings: Vec<(String, u64)> = Vec::with_capacity(contracts.len());
    for (stem, contract) in contracts {
        let ct_start = Instant::now();
        // Validate
        let _ = crate::schema::validate_contract(contract);
        // Audit
        let _ = crate::audit::audit_contract(contract);
        // Score
        let _ = crate::scoring::score_contract(contract, binding, stem);
        let ct_ms = u64::try_from(ct_start.elapsed().as_micros() / 1000).unwrap_or(0);
        contract_timings.push((format!("{stem}.yaml"), ct_ms));
    }
    // Sort by duration descending
    contract_timings.sort_by_key(|b| std::cmp::Reverse(b.1));
    contract_timings
}

/// Cache: store findings per-contract for future runs.
fn store_findings_in_cache(
    root: &std::path::Path,
    config: &LintConfig,
    contracts: &[(String, crate::schema::Contract)],
    all_findings: &[LintFinding],
    stats: &mut cache::CacheStats,
) {
    let rule_cfg = format!("{:?}{:?}", config.severity_overrides, config.strict);
    for (stem, _) in contracts {
        stats.total += 1;
        let yaml_path = config.contract_dir.join(format!("{stem}.yaml"));
        let yaml_content = std::fs::read_to_string(&yaml_path).unwrap_or_default();
        let hash = cache::content_hash(&yaml_content, &rule_cfg);
        if cache::cache_get(root, &hash).is_some() {
            stats.hits += 1;
        } else {
            stats.misses += 1;
            let contract_findings: Vec<_> = all_findings
                .iter()
                .filter(|f| f.contract_stem.as_deref() == Some(stem.as_str()))
                .cloned()
                .collect();
            let _ = cache::cache_put(root, &hash, &contract_findings);
        }
    }
}

/// Gates 2-9: audit, score, verify, enforce, enforcement-level, reverse-coverage, duplicate-stems, composition.
/// Each is skipped (not run) when `validation_passed` is false, per `push_gate`'s contract.
fn run_gates_2_to_9(
    config: &LintConfig,
    contracts: &[(String, crate::schema::Contract)],
    binding: Option<&crate::binding::BindingRegistry>,
    validation_passed: bool,
    gates: &mut Vec<GateResult>,
    all_findings: &mut Vec<LintFinding>,
) {
    // Gate 2: audit (skip if validation failed)
    push_gate(
        gates,
        all_findings,
        || run_audit_gate(contracts),
        "audit",
        validation_passed,
    );

    // Gate 3: score (skip if validation failed)
    push_gate(
        gates,
        all_findings,
        || run_score_gate(contracts, binding, config.min_score),
        "score",
        validation_passed,
    );

    // Gate 4: verify (source code fulfillment)
    push_gate(
        gates,
        all_findings,
        || {
            let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
            run_verify_gate(contracts, project_root)
        },
        "verify",
        validation_passed,
    );

    // Gate 5: enforce (equations must have preconditions/postconditions)
    push_gate(
        gates,
        all_findings,
        || run_enforce_gate(contracts),
        "enforce",
        validation_passed,
    );

    // Gate 6: enforcement level (Section 17, Gap 1 + Gap 5 level lock)
    push_gate(
        gates,
        all_findings,
        || {
            let min_level = config
                .min_level
                .unwrap_or(crate::schema::EnforcementLevel::Standard);
            run_enforcement_level_gate(contracts, min_level)
        },
        "enforcement-level",
        validation_passed,
    );

    // Gate 7: reverse coverage (optional — skip if no binding or crate dir)
    push_gate(
        gates,
        all_findings,
        || match (config.binding_path, config.crate_dir) {
            (Some(bp), Some(cd)) => run_reverse_coverage_gate(bp, cd),
            _ => (
                skipped_gate("reverse-coverage", "no --binding or --crate-dir provided"),
                Vec::new(),
            ),
        },
        "reverse-coverage",
        validation_passed,
    );

    // Gate 8: duplicate stems (PV-DUP-001). Must run BEFORE composition — it tells
    // the composition gate which stems are unresolvable, which is the difference
    // between a defined verdict and one decided by `read_dir` order.
    let duplicates = duplicate_stems::scan_duplicate_stems(config.contract_dir);
    let ambiguous = duplicate_stems::ambiguous_stems(&duplicates);
    push_gate(
        gates,
        all_findings,
        || {
            let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
            let baseline = duplicate_stems::read_baseline(project_root);
            duplicate_stems::run_duplicate_stem_gate(&duplicates, &baseline)
        },
        "duplicate-stems",
        validation_passed,
    );

    // Gate 9: composition (assumes/guarantees chain verification)
    push_gate(
        gates,
        all_findings,
        || composition_gate::run_composition_gate(contracts, &ambiguous),
        "composition",
        validation_passed,
    );
}

/// Gates 10-22: the ONT-* ontology gates. Same R-8 shape throughout — each is computed on every run and armed
/// per repo, never skipped by `validation_passed` the way gates 2-9 are.
fn run_ontology_gates_10_to_22(
    contract_dir: &Path,
    validation_passed: bool,
    gates: &mut Vec<GateResult>,
    all_findings: &mut Vec<LintFinding>,
) {
    // Gate 10: sigma (ONT-2b). R-8: a new gate is COMPUTED everywhere and armed per repo — so it runs here as
    // well as under `--gate sigma`, or `armed_gates` could name a gate no run ever computes.
    let (sigma_gate_result, mut sigma_findings) = sigma_result(contract_dir, validation_passed);
    gates.push(sigma_gate_result);
    all_findings.append(&mut sigma_findings);

    // Gate 11: relations (ONT-4). Same R-8 shape as sigma: computed in every run, armed per repo.
    let (relations_gate_result, mut relations_findings) =
        relations_result(contract_dir, validation_passed);
    gates.push(relations_gate_result);
    all_findings.append(&mut relations_findings);

    // Gate 12: shapes (ONT-4b). Same R-8 shape: computed in every run, armed per repo.
    let (shapes_gate_result, mut shapes_findings) = shapes_result(contract_dir, validation_passed);
    gates.push(shapes_gate_result);
    all_findings.append(&mut shapes_findings);

    // Gate 13: valid-under (ONT-7). Same R-8 shape: computed in every run, armed per repo.
    let (valid_under_gate_result, mut valid_under_findings) =
        valid_under_result(contract_dir, validation_passed);
    gates.push(valid_under_gate_result);
    all_findings.append(&mut valid_under_findings);

    // Gates 14, 15, 16: theorem-pairing, depends-on-present (PVL-001 EV-11), proved-is-derived (EV-8a). Same R-8
    // shape: computed in every run, armed per repo.
    for (name, run) in RATCHET_GATES {
        let (result, mut findings) = ratchet_result(contract_dir, validation_passed, name, run);
        gates.push(result);
        all_findings.append(&mut findings);
    }

    // Gate 17: challenge-fresh (PVL-001 EV-7a). Same R-8 shape: computed wherever a Lean theorem base exists,
    // armed per repo (only through `make ont-ratchet`).
    gates.push(challenge_result(contract_dir));

    // Gate 18 (numbered by agreement: ONT-7 13, EV-11 14-16, EV-7a 17): ont-consistency (ONT-5). Same R-8 shape:
    // computed in every run, armed per repo.
    let (consistency_gate_result, mut consistency_findings) =
        consistency_result(contract_dir, validation_passed);
    gates.push(consistency_gate_result);
    all_findings.append(&mut consistency_findings);

    // Gate 19: refines (ONT-4e, R-20). Same R-8 shape: computed in every run, armed per repo.
    let (refines_gate_result, mut refines_findings) =
        refines_result(contract_dir, validation_passed);
    gates.push(refines_gate_result);
    all_findings.append(&mut refines_findings);

    // Gate 20: bindings (ONT-3a). Same R-8 shape: computed in every run, armed per repo.
    let (bindings_gate_result, mut bindings_findings) = ratchet_result(
        contract_dir,
        validation_passed,
        bindings_gate::GATE,
        bindings_gate::run_bindings_gate,
    );
    gates.push(bindings_gate_result);
    all_findings.append(&mut bindings_findings);

    // Gate 21: refinement (ONT-3b). Same R-8 shape.
    let (refinement_gate_result, mut refinement_findings) = ratchet_result(
        contract_dir,
        validation_passed,
        refinement_gate::GATE,
        refinement_gate::run_refinement_gate,
    );
    gates.push(refinement_gate_result);
    all_findings.append(&mut refinement_findings);

    // Gate 22: evidence (ONT-8). Same R-8 shape: computed in every run, armed per repo.
    let (evidence_gate_result, mut evidence_findings) =
        evidence_result(contract_dir, validation_passed);
    gates.push(evidence_gate_result);
    all_findings.append(&mut evidence_findings);
}

/// Gate 9 (again, by original numbering): strict test-binding (Issue #1510), opt-in via `--strict-test-binding`.
fn run_strict_test_binding_gate_if_enabled(
    config: &LintConfig,
    contracts: &[(String, crate::schema::Contract)],
    validation_passed: bool,
    gates: &mut Vec<GateResult>,
    all_findings: &mut Vec<LintFinding>,
) {
    if !config.strict_test_binding {
        return;
    }
    push_gate(
        gates,
        all_findings,
        || {
            let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
            strict_test_binding::run_strict_test_binding_gate(
                contracts,
                project_root,
                config.strict,
            )
        },
        "strict-test-binding",
        validation_passed,
    );
}

/// Post-gate passes: fold in the validate gate's own findings, time contracts, detect stale suppressions, mark
/// new-vs-pre-existing findings, cache them, then apply suppressions/overrides/severity filter.
#[allow(clippy::too_many_arguments)]
fn finalize_findings(
    config: &LintConfig,
    contracts: &[(String, crate::schema::Contract)],
    binding: Option<&crate::binding::BindingRegistry>,
    validation_passed: bool,
    cache_root: Option<&std::path::Path>,
    stats: &mut cache::CacheStats,
    all_findings: &mut Vec<LintFinding>,
    mut validate_findings: Vec<LintFinding>,
) -> Vec<(String, u64)> {
    all_findings.append(&mut validate_findings);

    // Per-contract timing: measure how long each contract's findings take to process
    let contract_timings = if validation_passed {
        per_contract_timings(contracts, binding)
    } else {
        Vec::new()
    };

    // Stale suppression detection (PV-SUP-001, Section 17 Gap 2)
    let mut stale_findings = check_stale_suppressions(
        all_findings,
        &config.suppressed_rules,
        &config.suppressed_findings,
    );
    all_findings.append(&mut stale_findings);

    // Issue lifecycle: mark each finding as new or pre-existing
    mark_new_findings(all_findings, config.contract_dir);

    // Cache: store findings per-contract for future runs
    if let Some(root) = cache_root {
        store_findings_in_cache(root, config, contracts, all_findings, stats);
    }

    // Apply suppressions, severity overrides, strict mode, and severity filter
    apply_suppressions(all_findings, config);
    apply_severity_overrides(all_findings, config);
    if let Some(min_sev) = config.severity_filter {
        all_findings.retain(|f| f.severity >= min_sev);
    }

    contract_timings
}

/// Run all lint gates across a contract directory.
pub fn run_lint(config: &LintConfig) -> LintReport {
    let overall_start = Instant::now();
    let mut gates = Vec::with_capacity(3);
    let mut all_findings = Vec::new();
    let mut stats = cache::CacheStats::default();

    // A scoped run's findings are a subset; caching them would store a partial answer per contract.
    let cache_root = if config.no_cache || config.strict_test_binding_only {
        None
    } else {
        Some(cache::cache_dir(config.contract_dir))
    };

    let (contracts, parse_errors) = load_contracts(config.contract_dir);
    let binding = load_binding(config.binding_path);

    // Gate 1: validate
    let (validate_result, validate_findings) = run_validate_gate(&contracts, &parse_errors);
    let validation_passed = validate_result.passed;
    gates.push(validate_result);

    if !config.strict_test_binding_only {
        run_gates_2_to_9(
            config,
            &contracts,
            binding.as_ref(),
            validation_passed,
            &mut gates,
            &mut all_findings,
        );
        run_ontology_gates_10_to_22(
            config.contract_dir,
            validation_passed,
            &mut gates,
            &mut all_findings,
        );
    }
    run_strict_test_binding_gate_if_enabled(
        config,
        &contracts,
        validation_passed,
        &mut gates,
        &mut all_findings,
    );

    let contract_timings = finalize_findings(
        config,
        &contracts,
        binding.as_ref(),
        validation_passed,
        cache_root.as_deref(),
        &mut stats,
        &mut all_findings,
        validate_findings,
    );

    let passed = gates.iter().all(|g| g.passed || g.skipped);

    let mut report = LintReport {
        passed,
        gates,
        total_duration_ms: u64::try_from(overall_start.elapsed().as_millis()).unwrap_or(u64::MAX),
        findings: all_findings,
        cache_stats: stats,
        contract_timings,
        verdict: Verdict::Unknown(crate::ontology::verdict::Reason::NotArmed),
        armed_gates: Vec::new(),
        not_armed: Vec::new(),
        armed_monotone: None,
        armed_shapes_monotone: None,
    };
    // The default set. `pv lint` re-arms from the corpus's `lint-baseline.json` (ONT-001 §3.9): a gate a flag
    // ran but the declaration does not arm is printed and excluded, like every other unarmed gate.
    report.arm(&ArmedGates::default_set());
    report
}

/// ONT-2b: what `--gate <name>` answered. Only `Ran` and `Sigma(Ran)` are verdicts about the corpus.
pub enum NamedGateOutcome {
    /// `--gate` was given a name this build does not compute alone.
    UnknownGate,
    /// The `sigma` gate, which has two non-verdict answers of its own (no Σ, malformed Σ).
    Sigma(sigma_gate::SigmaOutcome),
    /// The `relations` gate (ONT-4), with three non-verdict answers (no Σ, malformed Σ, no typed relations).
    Relations(relations_gate::RelationsOutcome),
    /// The `shapes` gate (ONT-4b), with four non-verdict answers (unsupported shape, no shapes, no focus, control failed).
    Shapes(shapes_gate::ShapesOutcome),
    /// The `ont-consistency` gate (ONT-5): no Σ, malformed Σ, nothing checkable, a control that did not fire, a stale witness.
    Consistency(consistency_gate::ConsistencyOutcome),
    /// The `refines` gate (ONT-4e): no Σ, malformed Σ, a control that did not fire, a stale witness.
    Refines(refines_gate::RefinesOutcome),
    /// The `tbox` gate (ONT-2c): advisory classification. It has no Pass answer at all (R-7).
    Tbox(tbox_gate::TboxOutcome),
    /// The `evidence` gate (ONT-8), with three non-verdict answers (no Σ, malformed Σ, no evidence block).
    Evidence(evidence_gate::EvidenceOutcome),
    /// The `valid-under` gate (ONT-7), with three non-verdict answers (no Σ, malformed Σ, no kernel contract).
    ValidUnder(valid_under_gate::ValidUnderOutcome),
    /// A PVL-001 EV-11 ratchet (`theorem-pairing`, `depends-on-present`), whose one non-verdict answer is a decline.
    Ratchet(ratchet_gates::RatchetOutcome),
    /// A gate that ran and judged the corpus.
    Ran {
        result: Box<GateResult>,
        findings: Vec<LintFinding>,
    },
}

/// Run ONE named gate and nothing else (ONT-001 §5 ONT-2b).
///
/// Only the gates that are meaningful ALONE are offered: `sigma` reads Σ and the corpus, `validate` parses the
/// corpus. The rest of `run_lint`'s gates are skipped when validation fails, so running one of them by itself would
/// report a verdict whose precondition nobody checked — `UnknownGate` is the honest answer, not a silent pass.
#[must_use]
pub fn run_named_gate(contract_dir: &Path, name: &str) -> NamedGateOutcome {
    run_named_gate_with(contract_dir, name, &shapes_gate::ShapesOptions::default())
}

/// [`run_named_gate`] with the shapes gate's `--shape` / `--release-*` options (aprender#3715).
pub fn run_named_gate_with(
    contract_dir: &Path,
    name: &str,
    shapes_opts: &shapes_gate::ShapesOptions,
) -> NamedGateOutcome {
    match name {
        "evidence" => NamedGateOutcome::Evidence(evidence_gate::run_evidence_gate(contract_dir)),
        "relations" => {
            NamedGateOutcome::Relations(relations_gate::run_relations_gate(contract_dir))
        }
        "shapes" => {
            NamedGateOutcome::Shapes(shapes_gate::run_shapes_gate_with(contract_dir, shapes_opts))
        }
        "sigma" => NamedGateOutcome::Sigma(sigma_gate::run_sigma_gate(contract_dir)),
        consistency_gate::GATE => {
            NamedGateOutcome::Consistency(consistency_gate::run_consistency_gate(contract_dir))
        }
        refines_gate::GATE => {
            NamedGateOutcome::Refines(refines_gate::run_refines_gate(contract_dir))
        }
        bindings_gate::GATE => {
            NamedGateOutcome::Ratchet(bindings_gate::run_bindings_gate(contract_dir))
        }
        refinement_gate::GATE => {
            NamedGateOutcome::Ratchet(refinement_gate::run_refinement_gate(contract_dir))
        }
        "tbox" => NamedGateOutcome::Tbox(tbox_gate::run_tbox_gate(contract_dir)),
        "valid-under" => {
            NamedGateOutcome::ValidUnder(valid_under_gate::run_valid_under_gate(contract_dir))
        }
        "theorem-pairing" => {
            NamedGateOutcome::Ratchet(ratchet_gates::run_theorem_pairing_gate(contract_dir))
        }
        "depends-on-present" => {
            NamedGateOutcome::Ratchet(ratchet_gates::run_depends_on_present_gate(contract_dir))
        }
        "proved-is-derived" => {
            NamedGateOutcome::Ratchet(ratchet_gates::run_proved_is_derived_gate(contract_dir))
        }
        "validate" => {
            let (contracts, parse_errors) = load_contracts(contract_dir);
            let (result, findings) = run_validate_gate(&contracts, &parse_errors);
            NamedGateOutcome::Ran {
                result: Box::new(result),
                findings,
            }
        }
        _ => NamedGateOutcome::UnknownGate,
    }
}

/// The gate names `--gate` computes alone, for the refusal message.
pub const NAMED_GATES: [&str; 14] = [
    bindings_gate::GATE,
    refinement_gate::GATE,
    "depends-on-present",
    "evidence",
    consistency_gate::GATE,
    "proved-is-derived",
    refines_gate::GATE,
    "relations",
    "shapes",
    "sigma",
    "tbox",
    "theorem-pairing",
    "valid-under",
    "validate",
];

/// The EV-11 ratchet gates, by name, in the order the full run computes them.
type RatchetRun = fn(&Path) -> ratchet_gates::RatchetOutcome;
const RATCHET_GATES: [(&str, RatchetRun); 3] = [
    ("theorem-pairing", ratchet_gates::run_theorem_pairing_gate),
    (
        "depends-on-present",
        ratchet_gates::run_depends_on_present_gate,
    ),
    (
        "proved-is-derived",
        ratchet_gates::run_proved_is_derived_gate,
    ),
];

/// An EV-11 ratchet as `run_lint` reports it. Its decline becomes a SKIPPED gate here, as sigma's non-verdict
/// answers do — under `--gate <name>` it is an exit of its own (2).
fn ratchet_result(
    contract_dir: &Path,
    validation_passed: bool,
    name: &str,
    run: RatchetRun,
) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate(name, "validation failed"), Vec::new());
    }
    match run(contract_dir) {
        ratchet_gates::RatchetOutcome::Ran { result, findings } => (*result, findings),
        ratchet_gates::RatchetOutcome::Declined(why) => (skipped_gate(name, &why), Vec::new()),
    }
}

/// The `sigma` gate as `run_lint` reports it. Σ's two non-verdict answers become SKIPPED gates here — under
/// `--gate sigma` they are an exit of their own (decline / error), but inside a full run "skipped" is how the
/// lattice already says "not measured".
fn sigma_result(contract_dir: &Path, validation_passed: bool) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate("sigma", "validation failed"), Vec::new());
    }
    match sigma_gate::run_sigma_gate(contract_dir) {
        sigma_gate::SigmaOutcome::Ran { result, findings } => (*result, findings),
        sigma_gate::SigmaOutcome::NoSigma => (
            skipped_gate("sigma", "no contracts/ontology.yaml"),
            Vec::new(),
        ),
        sigma_gate::SigmaOutcome::Malformed(e) => (
            skipped_gate("sigma", &format!("Σ is malformed: {e}")),
            Vec::new(),
        ),
    }
}

/// The `evidence` gate as `run_lint` reports it (ONT-8). Its three non-verdict answers become SKIPPED gates here, as
/// sigma's do — under `--gate evidence` they are exits of their own (decline / error).
fn evidence_result(contract_dir: &Path, validation_passed: bool) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate("evidence", "validation failed"), Vec::new());
    }
    match evidence_gate::run_evidence_gate(contract_dir) {
        evidence_gate::EvidenceOutcome::Ran { result, findings } => (*result, findings),
        evidence_gate::EvidenceOutcome::NoSigma => (
            skipped_gate("evidence", "no contracts/ontology.yaml"),
            Vec::new(),
        ),
        evidence_gate::EvidenceOutcome::Malformed(e) => (
            skipped_gate("evidence", &format!("Σ is malformed: {e}")),
            Vec::new(),
        ),
        evidence_gate::EvidenceOutcome::NoEvidence { contracts_checked } => (
            skipped_gate(
                "evidence",
                &format!(
                    "no evidence block in {contracts_checked} contracts — R-2: zero is a decline"
                ),
            ),
            Vec::new(),
        ),
    }
}

/// The `valid-under` gate as `run_lint` reports it (ONT-7). Its three non-verdict answers become SKIPPED gates
/// here, as sigma's do — under `--gate valid-under` they are exits of their own (decline / error).
fn valid_under_result(
    contract_dir: &Path,
    validation_passed: bool,
) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate("valid-under", "validation failed"), Vec::new());
    }
    match valid_under_gate::run_valid_under_gate(contract_dir) {
        valid_under_gate::ValidUnderOutcome::Ran { result, findings } => (*result, findings),
        valid_under_gate::ValidUnderOutcome::NoSigma => (
            skipped_gate("valid-under", "no contracts/ontology.yaml"),
            Vec::new(),
        ),
        valid_under_gate::ValidUnderOutcome::Malformed(e) => (
            skipped_gate("valid-under", &format!("Σ is malformed: {e}")),
            Vec::new(),
        ),
        valid_under_gate::ValidUnderOutcome::NoKernels { contracts_checked } => (
            skipped_gate(
                "valid-under",
                &format!("no kernel-kind contract and no valid_under in {contracts_checked} contracts — R-2: zero is a decline"),
            ),
            Vec::new(),
        ),
    }
}

/// The `relations` gate as `run_lint` reports it. Its three non-verdict answers become SKIPPED gates here, as
/// sigma's do — under `--gate relations` they are exits of their own (decline / error).
fn relations_result(
    contract_dir: &Path,
    validation_passed: bool,
) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate("relations", "validation failed"), Vec::new());
    }
    match relations_gate::run_relations_gate(contract_dir) {
        relations_gate::RelationsOutcome::Ran { result, findings } => (*result, findings),
        relations_gate::RelationsOutcome::NoSigma => (
            skipped_gate("relations", "no contracts/ontology.yaml"),
            Vec::new(),
        ),
        relations_gate::RelationsOutcome::Malformed(e) => (
            skipped_gate("relations", &format!("Σ is malformed: {e}")),
            Vec::new(),
        ),
        relations_gate::RelationsOutcome::NoRelations {
            contracts_checked,
            legacy_depends_on,
        } => (
            skipped_gate(
                "relations",
                &format!("no typed relations in {contracts_checked} contracts ({legacy_depends_on} legacy metadata.depends_on edges) — R-2: zero is a decline"),
            ),
            Vec::new(),
        ),
    }
}

/// The `shapes` gate as `run_lint` reports it. Its four non-verdict answers become SKIPPED gates here (under
/// `--gate shapes` they are exits of their own); an `Unknown{Warn}` run is reported as the gate returned it.
fn shapes_result(contract_dir: &Path, validation_passed: bool) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (skipped_gate("shapes", "validation failed"), Vec::new());
    }
    match shapes_gate::run_shapes_gate(contract_dir) {
        shapes_gate::ShapesOutcome::Ran { result, findings } => (*result, findings),
        shapes_gate::ShapesOutcome::Unsupported(e) => (skipped_gate("shapes", &format!("{e}")), Vec::new()),
        shapes_gate::ShapesOutcome::ExtractFailed(e) => (skipped_gate("shapes", &format!("{e}")), Vec::new()),
        shapes_gate::ShapesOutcome::NoShapes { contracts_checked } => (
            skipped_gate("shapes", &format!("no `shape:` block in {contracts_checked} contracts — R-2: zero is a decline")),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::NoFocus { shapes_n } => (
            skipped_gate("shapes", &format!("{shapes_n} shape(s), no focus node")),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::WrongCorpus { shapes_n, expected, found, refused } => (
            skipped_gate("shapes", &format!("extract:parity-receipt matched {found} focus node(s) and evidence/parity/EXPECTED_RECEIPTS says {expected} ({shapes_n} shape(s)){} — an extractor that saw the wrong corpus reports the same \"no violations\" as one that saw all of it", if refused.is_empty() { String::new() } else { format!("; refused: {}", refused.join("; ")) })),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::HarnessBroken { causes } => (
            skipped_gate("shapes", &format!("the CRUX harness measured itself, not apr: {}", causes.join("; "))),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::NoReceipts { shapes_n, dir } => (
            skipped_gate("shapes", &format!("{shapes_n} shape(s) resolve receipts and the tree holds none under {dir}/ — R-2: unmeasured is a decline")),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::EmptyDomain { shapes_n } => (
            skipped_gate("shapes", &format!("capability-cells: the required-cell domain D is empty ({shapes_n} shape(s)) — R-2: zero is a decline, never a pass")),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::PositiveControlFailed { shapes_n, focus_nodes_n, which } => (
            skipped_gate("shapes", &format!("positive control {which} did not fire ({shapes_n} shape(s), {focus_nodes_n} focus node(s)) — the gate cannot reject")),
            Vec::new(),
        ),
        shapes_gate::ShapesOutcome::Differential { shapes_n, focus_nodes_n, passed, n, failed } => {
            let mut g = skipped_gate(
                "shapes",
                &format!(
                    "W3C SHACL-Core differential: {passed} of {n} vendored case(s) pass; failed: {} ({shapes_n} shape(s), {focus_nodes_n} focus node(s)) — the validator disagrees with the standard, so no corpus verdict",
                    failed.join(" | ")
                ),
            );
            g.verdict = Verdict::Unknown(crate::ontology::verdict::Reason::Differential);
            (g, Vec::new())
        }
    }
}

/// The `ont-consistency` gate as `run_lint` reports it. Its declines keep their lattice reason here (a stale witness
/// is `Unknown{WitnessStale}`, not a bare skip), so the meet says what could not be checked.
fn consistency_result(
    contract_dir: &Path,
    validation_passed: bool,
) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (
            skipped_gate(consistency_gate::GATE, "validation failed"),
            Vec::new(),
        );
    }
    let outcome = consistency_gate::run_consistency_gate(contract_dir);
    if let consistency_gate::ConsistencyOutcome::Ran { result, findings } = outcome {
        return (*result, findings);
    }
    let mut g = skipped_gate(consistency_gate::GATE, &consistency_gate::why(&outcome));
    if let Some(reason) = consistency_gate::decline_reason(&outcome) {
        g.verdict = Verdict::Unknown(reason);
    }
    (g, Vec::new())
}

/// The `refines` gate as `run_lint` reports it; declines keep their lattice reason, as `ont-consistency`'s do.
fn refines_result(contract_dir: &Path, validation_passed: bool) -> (GateResult, Vec<LintFinding>) {
    if !validation_passed {
        return (
            skipped_gate(refines_gate::GATE, "validation failed"),
            Vec::new(),
        );
    }
    let outcome = refines_gate::run_refines_gate(contract_dir);
    if let refines_gate::RefinesOutcome::Ran { result, findings } = outcome {
        return (*result, findings);
    }
    let mut g = skipped_gate(refines_gate::GATE, &refines_gate::why(&outcome));
    if let Some(reason) = refines_gate::decline_reason(&outcome) {
        g.verdict = Verdict::Unknown(reason);
    }
    (g, Vec::new())
}

/// The `challenge-fresh` gate: `pv challenge check` as a gate. No Lean theorem base, a tree that does not load, or
/// zero challenges is SKIPPED (not measured), never green.
fn challenge_result(contract_dir: &Path) -> GateResult {
    const NAME: &str = "challenge-fresh";
    let start = Instant::now();
    let root = crate::ontology::extract::repo_root(contract_dir);
    let Some(lean) = crate::ontology::extract::lean::base_under(&root) else {
        return skipped_gate(NAME, "no Lean theorem base under the repo root");
    };
    let r = match crate::discharge::challenge::render(&lean, contract_dir) {
        Ok(r) => r,
        Err(e) => return skipped_gate(NAME, &format!("the Lean tree does not load: {e}")),
    };
    if r.files.is_empty() && r.unrestated.is_empty() {
        return skipped_gate(
            NAME,
            "zero challenges: no contract binds a theorem — R-2: zero is a decline",
        );
    }
    let stale = crate::discharge::challenge::diff(&lean, &r);
    let unrestated: Vec<String> = r
        .unrestated
        .iter()
        .map(|(c, fqn, why)| format!("{c}: {fqn}: {why}"))
        .collect();
    let passed = stale.is_empty() && unrestated.is_empty();
    GateResult {
        name: NAME.into(),
        passed,
        skipped: false,
        verdict: Verdict::from_gate(passed, false),
        duration_ms: u64::try_from(start.elapsed().as_millis()).unwrap_or(u64::MAX),
        // `GateDetail` is FROZEN at the 0.3.1 variants: the shape is borrowed, the payload rides in `GateExtra`.
        detail: GateDetail::Validate {
            contracts: r.files.len(),
            errors: stale.len() + unrestated.len(),
            warnings: 0,
            error_messages: stale.iter().chain(&unrestated).cloned().collect(),
        },
        extra: Some(GateExtra::ChallengeFresh {
            lean_dir: lean.display().to_string(),
            files: r.files.len(),
            stale,
            unrestated,
        }),
    }
}

fn skipped_gate(name: &str, reason: &str) -> GateResult {
    GateResult {
        name: name.into(),
        passed: false,
        skipped: true,
        verdict: Verdict::from_gate(false, true),
        duration_ms: 0,
        detail: GateDetail::Skipped {
            reason: reason.into(),
        },
        extra: None,
    }
}

fn apply_suppressions(findings: &mut [LintFinding], config: &LintConfig) {
    for f in findings.iter_mut() {
        if config.suppressed_rules.iter().any(|r| r == &f.rule_id) {
            f.suppressed = true;
            f.suppression_reason = Some("Suppressed by --suppress-rule".into());
        }
        if let Some(ref stem) = f.contract_stem {
            if config.suppressed_findings.iter().any(|s| s == stem) {
                f.suppressed = true;
                f.suppression_reason = Some("Suppressed by --suppress".into());
            }
        }
        if config.suppressed_files.iter().any(|p| f.file.contains(p)) {
            f.suppressed = true;
            f.suppression_reason = Some("Suppressed by --suppress-file".into());
        }
    }
}

/// Resolve the `.pv/` state directory relative to the contract directory's parent.
fn pv_state_dir(contract_dir: &Path) -> std::path::PathBuf {
    contract_dir.parent().unwrap_or(contract_dir).join(".pv")
}

/// Load previous fingerprints, compare with current findings, mark new ones,
/// and persist the current fingerprint set for the next run.
fn mark_new_findings(findings: &mut [LintFinding], contract_dir: &Path) {
    let state_dir = pv_state_dir(contract_dir);
    let previous_path = state_dir.join("lint-previous.json");

    // Load previous fingerprints (empty set if file missing or unreadable)
    let previous: HashSet<String> = std::fs::read_to_string(&previous_path)
        .ok()
        .and_then(|s| serde_json::from_str(&s).ok())
        .unwrap_or_default();

    // Compute current fingerprints and mark new findings
    let mut current = HashSet::new();
    for f in findings.iter_mut() {
        let fp = f.fingerprint();
        if !previous.contains(&fp) {
            f.is_new = true;
        }
        current.insert(fp);
    }

    // Persist current fingerprints for the next run
    if let Err(e) = std::fs::create_dir_all(&state_dir) {
        eprintln!("pv lint: cannot create {}: {e}", state_dir.display());
        return;
    }
    if let Ok(json) = serde_json::to_string(&current) {
        let _ = std::fs::write(&previous_path, json);
    }
}

fn apply_severity_overrides(findings: &mut [LintFinding], config: &LintConfig) {
    for f in findings.iter_mut() {
        if let Some(&sev) = config.severity_overrides.get(&f.rule_id) {
            f.severity = sev;
        }
    }
    if config.strict {
        for f in findings.iter_mut() {
            if f.severity == RuleSeverity::Warning {
                f.severity = RuleSeverity::Error;
            }
        }
    }
}

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