//! The reference verified-fix harness.
//!
//! What every commercial remediation product gets wrong, this harness makes
//! structural: the verification pipeline is not a feature bolted beside the
//! fix — **the gates ARE the contract obligations**. A run builds a
//! JouleContract whose `pre`/`post`/`inv` clauses are the pipeline stages
//! (baseline capture, build, no-new-test-failures, lint-delta, frame
//! confinement, diff guard), discharges each one with the stage's actual
//! outcome, and seals the result with its energy, graded by how that energy
//! was obtained. Three consequences, by construction:
//!
//! 1. **A fix that fails its gate is reverted and never ships** — but the
//!    refusal still produces a receipt: an undischarged obligation on the
//!    record beats a silently dropped fix.
//! 2. **The energy figure rests on a hardware reading** whenever the host
//!    exposes a live CPU energy counter ([`sandbox_meter::PowerMeter`]), and
//!    is then anchored to a sealed sandbox JCR-1 meter envelope — one
//!    standard's receipt is the other's evidence. Where it does not, the
//!    figure is an estimate and is sealed as one (JCR-1 `Estimator`,
//!    JouleContract `Unaccounted`), never as a reading.
//! 3. **The receipt grades honestly**: receipt-local validation, JR-2 at
//!    most, generator and verifier self-declared and labeled as such. Higher
//!    rigor is a deployment's verifier-of-record work, exactly per the
//!    JouleContract two-stage rule.
//!
//! v0 remediates at the **L1 lawful tier only** — `cargo clippy --fix` and
//! `rustfmt`, deterministic codemods, zero inference — which is not a
//! limitation but the doctrine: the cheapest sufficient tier closes the
//! request. Model tiers (L3 local, L4 federation) hang off the same gate.

use joule_code_cargo::{Anchor, CodingOp, Edit};
use joule_code_schema::{ContentId, Tier};
use joulecontract_receipt::{
    validate, DischargeEntry, DischargeResult, Engagement, FrameMode, Generator, MeterBinding,
    Qualification, Receipt, TierClass, TrustRoot,
};
use joulecontract_schema::{
    Ceiling, ContentAddress, Contract, EnergyClass, GovernanceClass, ObligationKind, Profile,
    Rigor,
};
use sandbox_meter::{run_attributed, Attribution, PowerMeter, TreeError, TreeMeter, TreeReading};
use sandbox_schema::DeviceClass;
use serde::{Deserialize, Serialize};
// The formally-verified fix tier. `DischargeStatus`/`Formalization`/
// `ContractDischarge` come from the proof bridge; the bridge's own
// `DischargeEntry` is NOT imported — that name already belongs to
// `joulecontract_receipt` above (the operational receipt's entry).
use joulecontract_proof::{discharge as proof_discharge, DischargeStatus, Formalization};
use proof_cascade::{ProofCache, Router};
use proof_solvers::{Propositional, Z3Smt};
use std::cell::RefCell;
use std::collections::BTreeSet;
use std::path::PathBuf;
use std::process::Command;
use std::time::{Duration, Instant};

/// Accumulates per-process energy attribution across a run's subprocesses
/// (the real compute): every `cargo` invocation, which the harness's `run()`
/// helper feeds, and the L3 model's command, which [`Harness::run_l3`] feeds.
/// git and rustfmt are negligible overhead and run unmetered.
struct MeterAcc {
    /// `PowerMeter::detect()`, machine-wide, and deliberately not
    /// `detect_in_process()`: the metered work is `cargo` and the `rustc`
    /// processes it runs, and the L3 model's process, and this process's own
    /// energy counter covers no child process. `run_attributed`'s per-child
    /// reading does not reach cargo's work either: it covers a single-process
    /// child, and `cargo` runs its work in descendants.
    meter: PowerMeter,
    /// This run's metered windows, reset at the start of each run.
    tally: EnergyTally,
    /// This run's L3 window, when the model was consulted: how it was metered
    /// and what it added to `tally`. Reset with it.
    l3: Option<L3Energy>,
}

/// The energy of one run's metered windows — its cargo windows and its L3
/// window — and the figure and grades the receipts carry for it.
///
/// A cargo window is attributed when a hardware CPU reading that advanced
/// was apportioned to the child's process tree (`ModelBased`). Otherwise its
/// figure is not a reading of this workload. It is the meter's wall × TDP
/// estimate where the host exposes no live CPU counter (every macOS 27.0.1
/// host checked), or where the counter held; or it is a machine-wide figure
/// the meter could not apportion. The L3 window is never attributed: its
/// model's own process tree is never read whole ([`grade_l3`]). The run is
/// `ModelBased` only when every window was attributed, because a sum is only
/// as good as its weakest part.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
struct EnergyTally {
    /// Σ each window's figure as an estimate of its work: over a cargo
    /// window the machine-wide SoC-CPU figure (an upper bound: every process
    /// on the host), over the L3 window [`L3Energy::figure_uj`].
    soc_uj: u64,
    /// The part of `soc_uj` in device classes other than the CPU, per class:
    /// what the machine-wide meter read of them over an L3 window (a GPU
    /// rail, NVML's GPUs). A cargo window's figure is the CPU's alone.
    non_cpu_uj: std::collections::BTreeMap<DeviceClass, u64>,
    /// Σ figure apportioned or read for this run's process trees.
    attr_uj: u64,
    windows: u64,
    attributed_windows: u64,
    /// The probes whose readings the attributed windows apportioned, each
    /// window's own (`Attribution::source`): what the meter source names.
    read_by: BTreeSet<&'static str>,
}

impl EnergyTally {
    fn add(&mut self, a: &Attribution) {
        self.add_window(a.soc_cpu_uj, a.attributed_uj, a.attributed);
        if a.attributed {
            self.read_by.insert(a.source);
        }
    }

    /// How the figure was obtained, for [`RunReport::meter_source`]: an
    /// attribution names the probes its windows' readings came from, as the
    /// meter reported them; an estimate names the meter's hardware sources,
    /// `meter_sources` ([`PowerMeter::sources`]), or says it has none.
    fn source(&self, meter_sources: &[&str]) -> String {
        if self.attributed() {
            let read_by: Vec<&str> = self.read_by.iter().copied().collect();
            format!("attributed(ModelBased over {} HwShunt)", read_by.join("+"))
        } else if meter_sources.is_empty() {
            "estimated(Unaccounted): wall-clock × TDP, no live energy counter on this host".to_string()
        } else {
            format!(
                "estimated(Unaccounted): not every window attributed; machine-wide figure over the \
                 metered windows ({})",
                meter_sources.join("+")
            )
        }
    }

    /// The L3 window: its figure, an estimate, never attributed, with the
    /// machine-wide meter's figure for each class other than the CPU kept
    /// apart, so the sealed record names the class it was read on.
    fn add_l3(&mut self, l3: &L3Energy) {
        self.add_window(l3.figure_uj, l3.attributed_uj(), false);
        for &(class, uj) in &l3.machine_by_class {
            if class != DeviceClass::Cpu {
                let sum = self.non_cpu_uj.entry(class).or_default();
                *sum = sum.saturating_add(uj);
            }
        }
    }

    /// One window: its figure as an estimate (`estimate_uj`), its figure as
    /// a reading or apportionment of its own process tree (`attributed_uj`),
    /// and whether that one is the window's honest figure (`attributed`).
    fn add_window(&mut self, estimate_uj: u64, attributed_uj: u64, attributed: bool) {
        self.soc_uj = self.soc_uj.saturating_add(estimate_uj);
        self.attr_uj = self.attr_uj.saturating_add(attributed_uj);
        self.windows += 1;
        if attributed {
            self.attributed_windows += 1;
        }
    }

    /// True when every metered window rested on real per-process accounting
    /// of a hardware CPU reading.
    fn attributed(&self) -> bool {
        self.windows > 0 && self.attributed_windows == self.windows
    }

    /// The figure the receipts carry. When attributed, it is the apportioned
    /// reading. Otherwise it is the unapportioned total over the windows, as
    /// an estimate. An apportioned estimate is no better than an estimate,
    /// and the apportioning share is 0 whenever the machine's tick counters
    /// (which update in bursts up to ~1 s apart) missed a window, which would
    /// put 0 J on the receipt for work that ran.
    fn figure_uj(&self) -> u64 {
        if self.attributed() {
            self.attr_uj
        } else {
            self.soc_uj
        }
    }

    /// The sandbox JCR-1 meter records for the figure, one per device class,
    /// summing to it. An attribution is one `ModelBased` CPU record (every
    /// window attributed, so no L3 window and nothing off the CPU). An
    /// estimate is an `Estimator` record with no measured figure for the CPU
    /// and one for each other class the L3 window's machine-wide meter read:
    /// a GPU's energy is never sealed as the CPU's.
    fn meter_records(&self) -> Vec<sandbox_meter::DeviceEnergy> {
        let record = |class, estimated_uj, provenance| sandbox_meter::DeviceEnergy {
            class,
            measured_uj: None,
            estimated_uj,
            provenance,
        };
        if self.attributed() {
            return vec![record(DeviceClass::Cpu, self.attr_uj, sandbox_meter::Provenance::ModelBased)];
        }
        let non_cpu: u64 = self.non_cpu_uj.values().fold(0, |a, &b| a.saturating_add(b));
        let mut records =
            vec![record(DeviceClass::Cpu, self.soc_uj.saturating_sub(non_cpu), sandbox_meter::Provenance::Estimator)];
        records.extend(
            self.non_cpu_uj.iter().map(|(&class, &uj)| record(class, uj, sandbox_meter::Provenance::Estimator)),
        );
        records
    }

    /// The JouleContract energy class for the figure. It is `ModelBased`,
    /// anchored to the sealed meter receipt, for an attribution. Otherwise it
    /// is `Unaccounted`, JouleContract's grade for energy estimated where the
    /// substrate exposes no reading.
    fn energy_class(&self) -> EnergyClass {
        if self.attributed() {
            EnergyClass::ModelBased
        } else {
            EnergyClass::Unaccounted
        }
    }
}

/// The L3 model's window: how its energy was read, and what it adds to the
/// run's figure ([`RunReport::total_uj`], and so
/// [`RunReport::uj_per_verified_fix`] and both receipts).
///
/// Two meters span the window, from the moment the command is let go (see
/// [`Harness::l3_cmd`]) to the moment it has exited and been reaped: the
/// machine-wide meter, as over a cargo window, and — where this host counts
/// each process's CPU energy (macOS, its per-process counter live) — a
/// [`TreeMeter`] rooted at the command's own process, which reads the CPU
/// energy of that process and its descendants and lists every way that
/// figure was seen to fall short of their whole energy. [`grade_l3`] turns
/// the two into the window's figure, in one place.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct L3Energy {
    /// The machine-wide meter's figure over the window, every device class
    /// it reads, µJ: a hardware reading where the host has a live
    /// machine-wide counter (RAPL, NVML on Linux), its wall-clock × TDP
    /// estimate where it has none (every macOS 27.0.1 host checked). Like a
    /// cargo window's, it is the whole host's, other processes included.
    pub machine_uj: u64,
    /// The same figure per device class, as the meter read them (the CPU,
    /// and a GPU where it reads one); `machine_uj` is their sum. The run's
    /// sealed records keep the classes apart.
    pub machine_by_class: Vec<(DeviceClass, u64)>,
    /// The CPU energy of the model's own process tree over the window, µJ
    /// (the [`TreeReading`]'s nanojoules rounded up), where the host counts
    /// it. `None` off macOS, where the per-process counter is not live, and
    /// when the span gave no reading (`partial_because` says why). It covers
    /// the model's CPU only: not its GPU or Neural Engine work, not work it
    /// hands to a process outside its tree, and not the last time on a core
    /// of a thread that exits (the kernel never folds it), which a model that
    /// exits in the window always has.
    pub process_cpu_uj: Option<u64>,
    /// Why `process_cpu_uj` is not the model's whole energy over the window:
    /// each gap the tree meter saw, as it words it — a model that exits in
    /// its window always has one, so its reading is never whole — or, where
    /// it saw none, [`NOT_READ_AT_EXIT`]; or why there is no reading at all.
    /// Never empty for a reading.
    pub partial_because: Vec<String>,
    /// Whether the command ran as the shell's `exec` — a plain argv — so the
    /// model's process IS the process the tree meter is rooted at, and its
    /// own count is read. A command that is not (a pipeline, a list, quoting,
    /// a redirect) runs as the shell's script: what the shell forks and
    /// reaps is a gap, its energy in no counter.
    pub direct_child: bool,
    /// What the window adds to the run's figure (see [`grade_l3`]), µJ: an
    /// estimate, never attributed.
    pub figure_uj: u64,
}

/// Why a reading of the L3 command's process tree is partial although the
/// tree meter saw no gap in it: the model had not exited when it was read
/// (the wait for its exit failed), so the reading may stop short of its
/// work. A model read at its exit always carries the exit's own gap instead.
pub const NOT_READ_AT_EXIT: &str =
    "the model had not exited when its process tree was read, so the reading may stop short of its work";

impl L3Energy {
    /// What the window's process reading added to the run's tree figures:
    /// the reading itself, a floor, else nothing.
    fn attributed_uj(&self) -> u64 {
        self.process_cpu_uj.unwrap_or(0)
    }

    /// The window in one line, for [`RunReport::meter_source`].
    fn describe(&self) -> String {
        let j = |uj: u64| uj as f64 / 1e6;
        match self.process_cpu_uj {
            Some(read) => format!(
                "L3 model's own process tree read {:.3} J of CPU, partial ({}), so the window is an estimate: that \
                 reading plus the machine-wide {:.3} J, {:.3} J",
                j(read),
                self.partial_because.join("; "),
                j(self.machine_uj),
                j(self.figure_uj)
            ),
            None => format!(
                "L3 model metered machine-wide only, {:.3} J ({})",
                j(self.machine_uj),
                if self.partial_because.is_empty() {
                    "no per-process counter on this host".to_string()
                } else {
                    self.partial_because.join("; ")
                }
            ),
        }
    }
}

/// The L3 window's figure: the one place it is decided. It is always an
/// estimate of the window, never attributed.
///
/// - **A reading** — never whole. The model is read at its exit, and an
///   exiting process's record lacks its last time on a core (the kernel
///   never folds it), so the reading is a lower bound on the model's own CPU
///   energy; its GPU time is unknown, and work it hands outside its tree is
///   in no reading of it. The figure is the reading plus the machine-wide
///   meter's figure over the same window — never less than was read, and
///   nothing the model drew outside its CPU left out — the rule mesh's
///   in-process meter bills a partial span by. The machine-wide figure
///   covers the model's CPU too, so this errs high, by at most the reading.
/// - **No reading** — no per-process counter (Linux, a counter that is not
///   live) or the span's [`TreeError`]: the machine-wide figure, exactly as
///   a cargo window's (it is the whole host's).
fn grade_l3(
    reading: Option<&Result<TreeReading, TreeError>>,
    machine_by_class: Vec<(DeviceClass, u64)>,
    direct_child: bool,
) -> L3Energy {
    let machine_uj = machine_by_class.iter().fold(0u64, |a, &(_, uj)| a.saturating_add(uj));
    match reading {
        Some(Ok(r)) => {
            let read = r.cpu_nj.div_ceil(1_000);
            let mut because: Vec<String> = r.gaps.iter().map(ToString::to_string).collect();
            if because.is_empty() {
                because.push(NOT_READ_AT_EXIT.to_string());
            }
            L3Energy {
                machine_uj,
                machine_by_class,
                process_cpu_uj: Some(read),
                partial_because: because,
                direct_child,
                figure_uj: read.saturating_add(machine_uj),
            }
        }
        Some(Err(e)) => L3Energy {
            machine_uj,
            machine_by_class,
            process_cpu_uj: None,
            partial_because: vec![format!("no reading of the model's process tree: {e}")],
            direct_child,
            figure_uj: machine_uj,
        },
        None => L3Energy {
            machine_uj,
            machine_by_class,
            process_cpu_uj: None,
            partial_because: Vec::new(),
            direct_child,
            figure_uj: machine_uj,
        },
    }
}

/// The shell script an L3 command runs as, and whether it makes the model
/// the direct child.
///
/// The script first waits on a gate — one line on its stdin, which
/// [`Harness::run_l3`] writes once the tree meter has read the waiting
/// shell — so the window opens before the model starts and the shell's own
/// start-up stays outside it. Then, for a plain argv (letters, digits,
/// spaces and `/._-:,+@` only: no quoting, expansion, assignment, redirect
/// or list), the shell `exec`s it, so the model is the same process the
/// meter is rooted at. Anything else runs as the rest of the script, as
/// `sh -c` would have run it: what it forks and reaps is in no counter.
fn l3_script(cmd: &str) -> (String, bool) {
    let cmd = cmd.trim();
    let plain = !cmd.is_empty() && cmd.chars().all(|c| c.is_ascii_alphanumeric() || " /._-:,+@".contains(c));
    let body = if plain { format!("exec {cmd}") } else { cmd.to_string() };
    (format!("IFS= read -r joule_fix_gate || exit 1\n{body}\n"), plain)
}

/// Wait for child `pid` to exit WITHOUT reaping it (`waitid` with
/// `WNOWAIT`), so its count stays readable for the tree meter's stop walk.
/// The caller reaps it afterwards. `false` if the wait failed.
#[cfg(target_os = "macos")]
fn wait_exited_unreaped(pid: u32) -> bool {
    loop {
        // SAFETY: an all-zero `siginfo_t` is a valid out-parameter.
        let mut info: libc::siginfo_t = unsafe { std::mem::zeroed() };
        // SAFETY: `info` is writable for the call; `pid` is this process's child.
        let rc = unsafe { libc::waitid(libc::P_PID, pid as libc::id_t, &mut info, libc::WEXITED | libc::WNOWAIT) };
        if rc == 0 {
            return true;
        }
        if std::io::Error::last_os_error().raw_os_error() != Some(libc::EINTR) {
            return false;
        }
    }
}

/// No tree meter exists off macOS, so there is nothing to read before the reap.
#[cfg(not(target_os = "macos"))]
fn wait_exited_unreaped(_pid: u32) -> bool {
    false
}

#[derive(Debug, thiserror::Error)]
pub enum HarnessError {
    #[error("not a git work tree: {0} (the harness needs revert-ability before it will touch anything)")]
    NotGit(PathBuf),
    #[error("workspace has uncommitted changes; commit or stash first (the harness must own the diff)")]
    Dirty,
    #[error("command failed to launch: {0}")]
    Spawn(String),
    #[error("contract error: {0}")]
    Contract(String),
    /// Every gate passed but the fix could not be committed, so nothing
    /// shipped. The message says where the verified change was left.
    #[error("the fix passed every gate but could not be committed: {0}")]
    Ship(String),
}

/// One pipeline stage's outcome — the discharge evidence for one obligation.
#[derive(Clone, Debug, Serialize)]
pub struct GateOutcome {
    pub gate: String,
    pub passed: bool,
    pub detail: String,
}

/// The formal-tier input, read from `<workspace>/.joule-fix/formal.json` when
/// present: a domain [`Contract`] and the [`Formalization`]s that encode the
/// obligations the fix must honor. Absent file ⇒ no formal gate (the harness
/// runs exactly as before). The formalizations are an explicit, grounded input
/// — the harness never invents one (autoformalization is an upstream concern).
///
/// `formal.example.json` (next to this crate's `Cargo.toml`) is a working,
/// copy-pasteable template. The serde forms that trip up a hand-written file:
/// `rigor_target` is `"JR-1".."JR-4"`; `ceiling.enb_ref` is a **string**
/// `"sha2-256:<64-hex>"` (not an object); `kind` is one of
/// `Trivial|Arithmetic|Decidable|General|Hard`; `grounding` is one of
/// `Ungrounded|HumanReviewed|CrossChecked` — all PascalCase. `obligation`
/// indexes the contract's obligations in declaration order (pre, then post,
/// then inv, then frame).
#[derive(Debug, Deserialize)]
struct FormalSpec {
    contract: Contract,
    formalizations: Vec<Formalization>,
}

/// One formalized obligation's proof outcome, for the report and evidence file.
#[derive(Clone, Debug, Serialize)]
pub struct FormalEntry {
    /// The obligation text as the domain contract declares it.
    pub obligation: String,
    /// `proved` | `refuted` | `unproved`.
    pub verdict: String,
    /// The tier that closed it (when proved).
    pub closed_by: Option<String>,
    /// The counter-model witness (when refuted by a decision procedure).
    pub counter_model: Option<String>,
    /// Joules for this obligation's proof attempts, as the proof cascade
    /// accounted them (`Estimator`, in-process: wall time × proof-solvers'
    /// default power, which no host calibrated).
    pub uj: u64,
}

/// The formal-tier verdict for a run: did every supplied formalization prove?
#[derive(Clone, Debug, Serialize)]
pub struct FormalOutcome {
    pub proved: usize,
    pub refuted: usize,
    pub unproved: usize,
    /// Total joules across all proof attempts (`Estimator`, in-process —
    /// distinct from the cargo-attributed gate energy).
    pub proof_uj: u64,
    /// True iff at least one formalization was supplied and **every** one
    /// proved. This is the gate: any refutation or unproven goal fails it, and
    /// the fix reverts like any other failed gate.
    pub all_proved: bool,
    pub entries: Vec<FormalEntry>,
}

/// The result of one harness run.
#[derive(Debug)]
pub struct RunReport {
    /// Findings before the fix (clippy warning count).
    pub findings_before: usize,
    /// Findings after (counted only when a fix was applied).
    pub findings_after: Option<usize>,
    pub changed_files: Vec<String>,
    pub gates: Vec<GateOutcome>,
    /// All gates green and a non-empty fix was applied.
    pub shipped: bool,
    /// The branch carrying the fix, when shipped.
    pub branch: Option<String>,
    /// Energy apportioned to, or read for, this run's process trees,
    /// microjoules: each cargo window's apportionment, and the L3 model's
    /// own process-tree reading where there is one ([`L3Energy`]). When
    /// `attributed`, it is a `ModelBased` figure resting on real readings:
    /// the receipts' figure, and the honest per-workload cost. Otherwise it is
    /// at best an estimate or a floor, and is context only.
    pub attributed_uj: u64,
    /// Each metered window's figure as an estimate, summed, microjoules:
    /// over a cargo window the machine-wide SoC-CPU figure (an upper bound,
    /// every process on the host), over the L3 window
    /// [`L3Energy::figure_uj`]. When not `attributed`, this is the receipts'
    /// figure, as an estimate.
    pub soc_cpu_uj: u64,
    /// True when every metered window rested on real per-process accounting
    /// of a hardware CPU reading. False means the receipts carry an estimate.
    pub attributed: bool,
    /// The L3 model's window, when the model was consulted: its machine-wide
    /// figure, its own process tree's reading and why that is partial, and
    /// what it added to this run's figure. Its energy is in `soc_cpu_uj`,
    /// `attributed_uj` and the receipts.
    pub l3: Option<L3Energy>,
    pub wall: Duration,
    pub meter_source: String,
    pub contract: Contract,
    pub receipt: Receipt,
    /// The DSSE envelope (in-toto Statement, JouleContract predicate).
    pub envelope_json: String,
    /// The sealed sandbox JCR-1 meter envelope backing the meter binding.
    pub meter_envelope: Vec<u8>,
    /// The receipt-local verdict claim string.
    pub local_claim: String,
    /// The formal-tier outcome, when a `.joule-fix/formal.json` was present and
    /// the fix carried formalizations. `None` ⇒ no formal gate ran (the default,
    /// behaving exactly as before). A failed formal gate appears in `gates` and
    /// blocks shipping like any other.
    pub formal: Option<FormalOutcome>,
}

impl RunReport {
    /// Microjoules for the whole verified run (measure → fix → gate), the
    /// figure the receipts carry: every cargo window and the L3 model's
    /// window. When `attributed`, it is the energy ATTRIBUTED to this run's
    /// process trees, not the machine-wide total. Otherwise it is each
    /// window's estimate summed ([`soc_cpu_uj`](Self::soc_cpu_uj)), which is
    /// then an estimate and is sealed as one (`Estimator`, `Unaccounted`).
    /// It is never an apportioned zero for work that ran.
    pub fn total_uj(&self) -> u64 {
        if self.attributed {
            self.attributed_uj
        } else {
            self.soc_cpu_uj
        }
    }

    /// The headline metric nobody else publishes: microjoules per verified,
    /// shipped fix. It is attributed when `attributed` and an estimate
    /// otherwise. `None` when nothing shipped (energy was still spent and is
    /// still on the receipt — refusals aren't free, and saying so is the
    /// point).
    pub fn uj_per_verified_fix(&self) -> Option<u64> {
        if !self.shipped {
            return None;
        }
        let fixed = self
            .findings_after
            .map(|after| self.findings_before.saturating_sub(after))
            .unwrap_or(0);
        if fixed == 0 {
            None
        } else {
            Some(self.total_uj() / fixed as u64)
        }
    }
}

/// One induced remediation skill: a deterministic line transform keyed by
/// the lint's message text, compiled from a fix that SHIPPED through the
/// full gate at a stochastic tier. Recurrences of the same pattern never
/// consult a model again — the skill is the L1 form of an L3 lesson.
#[derive(Clone, Debug, Serialize, serde::Deserialize)]
pub struct Skill {
    /// The normalized lint message (everything after `warning:`/`error:`).
    pub message_key: String,
    /// The exact offending line (as it appeared, trimmed).
    pub old_line: String,
    /// Its replacement (trimmed; original indentation is preserved on apply).
    pub new_line: String,
    /// How many times the skill has closed a recurrence.
    pub hits: u64,
}

/// The skill store: a JSON file of induced rules. Plain data, no model,
/// no registry service — a skill you can read is a skill you can audit.
#[derive(Default, Serialize, serde::Deserialize)]
pub struct SkillStore {
    pub skills: Vec<Skill>,
}

impl SkillStore {
    pub fn load(path: &std::path::Path) -> SkillStore {
        std::fs::read_to_string(path)
            .ok()
            .and_then(|s| serde_json::from_str(&s).ok())
            .unwrap_or_default()
    }

    pub fn save(&self, path: &std::path::Path) {
        if let Some(dir) = path.parent() {
            let _ = std::fs::create_dir_all(dir);
        }
        if let Ok(json) = serde_json::to_string_pretty(self) {
            let _ = std::fs::write(path, json);
        }
    }
}

/// The lint message with its location stripped: the class key.
fn message_key(finding: &str) -> Option<String> {
    let tail = finding
        .split_once(": warning: ")
        .or_else(|| finding.split_once(": error: "))?
        .1;
    Some(tail.trim().to_string())
}

/// Harness configuration: identities and limits a deployment binds once.
pub struct Harness {
    pub workspace: PathBuf,
    /// Maximum changed lines a single run may ship.
    pub max_diff_lines: usize,
    /// L1 tier energy ceiling, joules (cargo subprocess work is host-priced,
    /// not token-priced; default is deliberately generous and recorded).
    pub ceiling_joules: f64,
    /// Steward label for the meter seal + receipt signer derivation.
    pub steward: String,
    signing: ed25519_dalek::SigningKey,
    /// The meter subsystem's own key: the energy attestation must not be
    /// signed by the receipt signer (JouleContract §4.2 — a self-attested
    /// meter does not bind). The sandbox meter is genuinely a different
    /// component; it gets a different key.
    meter_signing: ed25519_dalek::SigningKey,
    /// The L3 stochastic fixer, as a subprocess seam: a command that reads a
    /// remediation prompt on stdin and writes SEARCH/REPLACE blocks on
    /// stdout. Any local model CLI plugs in here (a jouleclaw decode binary,
    /// a federation leg) — and whatever comes back faces the same gates as
    /// the deterministic tier, which is what makes a weak model SAFE to run.
    /// Defaults from `JOULE_FIX_L3_CMD`; `None` disables the tier.
    ///
    /// The command is metered ([`L3Energy`]) and its energy is part of the
    /// run's figure. It runs under `sh`, which waits for a gate line before
    /// it starts the command (so the meter opens on a shell at rest) and then
    /// `exec`s a plain argv — `granite-fix /path/to/snapshot` — so the model
    /// is the shell's own process and its own energy count is readable. A
    /// command that needs the shell (a pipeline, a list, quoting) runs as the
    /// shell's script instead, and what the shell forks and reaps is energy
    /// no counter holds: the reading says so. The reading is never whole —
    /// the model exits in its window, and an exiting process's record lacks
    /// its last time on a core — so the window is always an estimate
    /// ([`grade_l3`]).
    pub l3_cmd: Option<String>,
    /// Where induced skills persist. Defaults from `JOULE_FIX_SKILLS`, else
    /// `~/.joule-fix/skills.json`; the store is created on first induction.
    pub skill_store: PathBuf,
    /// Per-process energy attribution, accumulated across cargo subprocesses.
    /// `RefCell` because `run()` takes `&self` and feeds it call by call.
    meter: RefCell<MeterAcc>,
    /// Test builds only: the target directory every `cargo` run is handed
    /// (`--target-dir`), the workspace's own `target/`, so a test's scratch
    /// crate builds where it does with no `CARGO_TARGET_DIR`, whatever the
    /// test process inherited. Every scratch crate is a package named
    /// `scratch` at 0.1.0, and cargo names its artifacts without the path, so
    /// under one exported `CARGO_TARGET_DIR` the concurrent tests' crates
    /// built over each other's artifacts and fingerprints. Not in production
    /// builds: `joule-fix` hands cargo no such flag, and the user's
    /// environment, `CARGO_TARGET_DIR` included, decides where it builds.
    #[cfg(test)]
    cargo_target_dir: PathBuf,
}

impl Harness {
    pub fn new(workspace: impl Into<PathBuf>) -> Result<Harness, HarnessError> {
        let workspace = workspace.into();
        // Inside ANY git work tree counts — a workspace may be a subdirectory
        // of a monorepo. Revert-ability is the requirement, not a local .git.
        let inside = Command::new("git")
            .args(["rev-parse", "--is-inside-work-tree"])
            .current_dir(&workspace)
            .output()
            .map(|o| o.status.success())
            .unwrap_or(false);
        if !inside {
            return Err(HarnessError::NotGit(workspace));
        }
        #[cfg(test)]
        let cargo_target_dir = workspace.join("target");
        Ok(Harness {
            workspace,
            max_diff_lines: 400,
            ceiling_joules: 2_000.0,
            steward: "joule-fix.local".into(),
            signing: ed25519_dalek::SigningKey::from_bytes(&[11u8; 32]),
            meter_signing: ed25519_dalek::SigningKey::from_bytes(&[12u8; 32]),
            l3_cmd: std::env::var("JOULE_FIX_L3_CMD").ok().filter(|s| !s.trim().is_empty()),
            skill_store: std::env::var("JOULE_FIX_SKILLS")
                .map(PathBuf::from)
                .unwrap_or_else(|_| {
                    let home = std::env::var("HOME").unwrap_or_else(|_| ".".into());
                    PathBuf::from(home).join(".joule-fix/skills.json")
                }),
            meter: RefCell::new(MeterAcc {
                meter: PowerMeter::detect(),
                tally: EnergyTally::default(),
                l3: None,
            }),
            #[cfg(test)]
            cargo_target_dir,
        })
    }

    /// Use a real signing key instead of the published demo key.
    pub fn with_signing_key(mut self, key: ed25519_dalek::SigningKey) -> Self {
        self.signing = key;
        self
    }

    fn run(&self, program: &str, args: &[&str]) -> Result<(bool, String), HarnessError> {
        // The real compute is `cargo`; meter and attribute it. Other programs
        // (git, rustfmt) are negligible harness overhead and run unmetered.
        if program == "cargo" {
            let args = self.cargo_args(args);
            let mut acc = self.meter.borrow_mut();
            let MeterAcc { meter, tally, .. } = &mut *acc;
            let (ok, text, a) = run_attributed(meter, program, &args, &self.workspace)
                .map_err(|e| HarnessError::Spawn(format!("{program}: {e}")))?;
            tally.add(&a);
            return Ok((ok, text));
        }
        let out = Command::new(program)
            .args(args)
            .current_dir(&self.workspace)
            .output()
            .map_err(|e| HarnessError::Spawn(format!("{program}: {e}")))?;
        let mut text = String::from_utf8_lossy(&out.stdout).into_owned();
        text.push_str(&String::from_utf8_lossy(&out.stderr));
        Ok((out.status.success(), text))
    }

    /// The arguments a `cargo` run is given: `args`, as passed. In test
    /// builds only, `--target-dir <workspace>/target` follows the subcommand
    /// (every cargo run here has one: `clippy`, `test`, `build`), and the
    /// flag outranks an inherited `CARGO_TARGET_DIR`.
    fn cargo_args<'a>(&'a self, args: &[&'a str]) -> Vec<&'a str> {
        #[cfg(test)]
        if let Some((sub, rest)) = args.split_first() {
            let dir = self.cargo_target_dir.to_str().expect("a test workspace path is UTF-8");
            return [*sub, "--target-dir", dir].into_iter().chain(rest.iter().copied()).collect();
        }
        args.to_vec()
    }

    fn git_head(&self) -> Result<String, HarnessError> {
        let (ok, out) = self.run("git", &["rev-parse", "HEAD"])?;
        if !ok {
            return Err(HarnessError::Spawn("git rev-parse HEAD".into()));
        }
        Ok(out.trim().to_string())
    }

    fn git_clean(&self) -> Result<bool, HarnessError> {
        let (_, out) = // -uno: the harness owns the TRACKED diff; untracked build artifacts
        // (target/, .joule-fix/) are not its concern and must not wedge it.
        self.run("git", &["status", "--porcelain", "--untracked-files=no", "--", "."])?;
        Ok(out.trim().is_empty())
    }

    fn clippy_warning_count(&self) -> Result<usize, HarnessError> {
        let (_, out) = self.run(
            "cargo",
            &["clippy", "--workspace", "--message-format=short", "--quiet"],
        )?;
        // A finding is a per-location diagnostic: "<path>:<line>:<col>: warning|error".
        // Deny-by-default lints arrive as errors and are findings too (they
        // don't block `cargo build`, only clippy itself). Summary lines
        // ("error: could not compile …") carry no location and don't count.
        Ok(out
            .lines()
            .filter(|l| {
                l.contains(".rs:") && (l.contains(": warning:") || l.contains(": error:"))
            })
            .count())
    }

    fn test_failures(&self) -> Result<BTreeSet<String>, HarnessError> {
        // NOT --quiet: quiet mode suppresses the per-test result lines the
        // baseline diff is built from.
        let (_, out) = self.run("cargo", &["test", "--workspace"])?;
        Ok(out
            .lines()
            .filter_map(|l| l.strip_prefix("test ").and_then(|r| r.strip_suffix(" ... FAILED")))
            .map(str::to_string)
            .collect())
    }

    fn changed_files(&self) -> Result<Vec<String>, HarnessError> {
        let (_, out) = self.run("git", &["diff", "--name-only", "--relative", "--", "."])?;
        Ok(out.lines().map(str::to_string).filter(|s| !s.is_empty()).collect())
    }

    fn diff_lines(&self) -> Result<usize, HarnessError> {
        let (_, out) = self.run("git", &["diff", "--numstat", "--relative", "--", "."])?;
        Ok(out
            .lines()
            .filter_map(|l| {
                let mut it = l.split_whitespace();
                let add: usize = it.next()?.parse().ok()?;
                let del: usize = it.next()?.parse().ok()?;
                Some(add + del)
            })
            .sum())
    }

    /// One full verified-remediation run.
    pub fn run_once(&self) -> Result<RunReport, HarnessError> {
        if !self.git_clean()? {
            return Err(HarnessError::Dirty);
        }
        // Load+validate the formal spec FIRST — a malformed spec must fail on a
        // clean tree, before any edit the harness would then have to revert.
        let formal_spec = self.load_formal_spec()?;
        let prior_rev = self.git_head()?;
        let prior = ContentId::of_bytes(prior_rev.as_bytes());

        // Reset the per-run tally, all of it; this run's cargo calls and its
        // L3 window feed it. An earlier run's windows are not this run's
        // energy: without the reset, a second run on this Harness would seal
        // the first run's figure into its own receipts (on every host,
        // estimated or not), and an attributed earlier window could grade
        // this one.
        {
            let mut acc = self.meter.borrow_mut();
            acc.tally = EnergyTally::default();
            acc.l3 = None;
        }
        let wall_start = Instant::now();

        // ---- Stage 0: baseline (the `pre` obligation's evidence).
        let baseline_failures = self.test_failures()?;
        let findings_before = self.clippy_warning_count()?;
        let baseline_captured = true;

        let mut gates: Vec<GateOutcome> = vec![GateOutcome {
            gate: "baseline".into(),
            passed: baseline_captured,
            detail: format!(
                "{} clippy findings, {} pre-existing test failures recorded",
                findings_before,
                baseline_failures.len()
            ),
        }];

        // ---- Fix at the L1 lawful tier: deterministic codemods, no model.
        // Nothing to fix ⇒ nothing runs: a clean workspace gets a verified-
        // clean receipt, not a formatting pass dressed as remediation.
        if findings_before > 0 {
            let (_, _fix_out) = self.run(
                "cargo",
                &[
                    "clippy",
                    "--workspace",
                    "--fix",
                    "--allow-dirty",
                    "--allow-no-vcs",
                    "--quiet",
                ],
            )?;
            // Format ONLY the files the fix touched — reformatting untouched
            // files is out-of-frame noise, not remediation.
            let touched = self.changed_files()?;
            for f in touched.iter().filter(|f| f.ends_with(".rs")) {
                let _ = self.run("rustfmt", &["--edition", "2021", f]);
            }
        }

        // ---- Induced skills next: lessons already paid for at a stochastic
        // tier re-apply deterministically, before any model is consulted.
        let mut skills_applied = 0usize;
        if findings_before > 0 && self.clippy_warning_count()? > 0 {
            skills_applied = self.skill_pass()?;
        }

        // ---- Escalate to L3 only what L1 + skills left behind (cheapest
        // sufficient tier: the model is consulted last, and only when
        // configured). Snapshot finding files first — a shipped L3 fix is
        // the raw material skills are induced from.
        let mut used_l3 = false;
        // (path, message_key, offending line trimmed, old content)
        let mut l3_snapshot: Vec<(String, String, String, String)> = Vec::new();
        if self.l3_cmd.is_some() && findings_before > 0 && self.clippy_warning_count()? > 0 {
            for f in self.current_findings()? {
                let mut parts = f.split(':');
                let (Some(path), line_no, Some(key)) =
                    (parts.next(), parts.next().and_then(|n| n.parse::<usize>().ok()), message_key(&f))
                else {
                    continue;
                };
                if !path.ends_with(".rs") {
                    continue;
                }
                if let (Some(n), Ok(body)) = (line_no, std::fs::read_to_string(self.workspace.join(path))) {
                    if let Some(line) = body.lines().nth(n.saturating_sub(1)) {
                        l3_snapshot.push((path.to_string(), key, line.trim().to_string(), body));
                    }
                }
            }
            used_l3 = self.l3_pass()?;
        }
        let changed = self.changed_files()?;

        // ---- Gates (each one is an obligation's discharge evidence).
        let build_ok = changed.is_empty() || self.run("cargo", &["build", "--workspace", "--quiet"])?.0;
        gates.push(GateOutcome {
            gate: "build".into(),
            passed: build_ok,
            detail: if changed.is_empty() { "no fix applied".into() } else { "cargo build --workspace".into() },
        });

        let post_failures = if changed.is_empty() { baseline_failures.clone() } else { self.test_failures()? };
        let new_failures: Vec<&String> = post_failures.difference(&baseline_failures).collect();
        let tests_ok = new_failures.is_empty();
        gates.push(GateOutcome {
            gate: "tests-vs-baseline".into(),
            passed: tests_ok,
            detail: if tests_ok {
                "no new test failures".into()
            } else {
                format!("NEW failures: {new_failures:?}")
            },
        });

        let findings_after = self.clippy_warning_count()?;
        let lint_ok = changed.is_empty() || findings_after < findings_before;
        gates.push(GateOutcome {
            gate: "lint-delta".into(),
            passed: lint_ok,
            detail: format!("{findings_before} → {findings_after} findings"),
        });

        // Frame: the fix may touch Rust sources and manifests anywhere in the
        // workspace — and nothing else (no CI files, no secrets, no scripts).
        let frame_paths: Vec<String> = vec!["src/".into(), "crates/".into(), "Cargo.toml".into(), "Cargo.lock".into()];
        let op = CodingOp {
            alg: 0x01,
            prior: prior.clone(),
            edits: changed
                .iter()
                .map(|p| Edit {
                    path: p.clone(),
                    anchor: Anchor::ByteRange { start: 0, end: 0 },
                    replacement: Vec::new(), // identity carried by git; anchors are per-file markers here
                })
                .collect(),
            author: self.signing.verifying_key().to_bytes(),
            intent: format!(
                "remediate {findings_before} lint findings ({}{})",
                if used_l3 { "L1 lawful + L3 stochastic, gate-verified" } else { "L1 lawful tier" },
                if skills_applied > 0 {
                    format!("; {skills_applied} induced skill(s) applied — zero inference")
                } else {
                    String::new()
                }
            ),
            tier: if used_l3 { Tier::L3 } else { Tier::L1 },
        };
        let contract = self.contract(&frame_paths, findings_before);
        let frame_ok = changed.is_empty()
            || joule_code_joulecontract::frame_check(&contract, &op).is_ok();
        gates.push(GateOutcome {
            gate: "frame".into(),
            passed: frame_ok,
            detail: format!("{} files changed, footprint {:?}", changed.len(), frame_paths),
        });

        let diff = self.diff_lines()?;
        let diff_ok = diff <= self.max_diff_lines;
        gates.push(GateOutcome {
            gate: "diff-guard".into(),
            passed: diff_ok,
            detail: format!("{diff} changed lines (limit {})", self.max_diff_lines),
        });

        // ---- Formal tier (opt-in): if the run carries formalizations
        // (`.joule-fix/formal.json`), the fix's formal obligations must be
        // machine-checked by a decision procedure. A refuted or unproven goal
        // fails the gate — which reverts the fix exactly like a failed test.
        // The rung above build+test, and the one the market has not reached.
        let formal = formal_spec.as_ref().map(|s| self.discharge_formal(s));
        if let Some(f) = &formal {
            // The detail rides into a failed gate's receipt entry, so it names
            // the solver only when there was one to decide the goals.
            let solver = if proof_solvers::z3_available() {
                "real z3"
            } else {
                "no z3 on PATH: SMT goals left undecided"
            };
            gates.push(GateOutcome {
                gate: "formal-proof".into(),
                passed: f.all_proved,
                detail: format!(
                    "{} proved, {} refuted, {} unproved ({:.3} J, {solver})",
                    f.proved,
                    f.refuted,
                    f.unproved,
                    f.proof_uj as f64 / 1e6,
                ),
            });
        }

        // ---- Verdict: every gate green AND a real fix happened.
        let all_green = gates.iter().all(|g| g.passed);
        let shipped = all_green && !changed.is_empty();

        let branch = if shipped {
            let name = format!("joule-fix/{}", &prior_rev[..12.min(prior_rev.len())]);
            // Shipped means committed. Every step is checked: an unchecked
            // `checkout -b` that fails (the branch exists) would let the
            // commit land on whatever branch is current, and an unchecked
            // `commit` that fails (no git identity, a rejecting hook) would
            // report a fix as shipped while it sits uncommitted in the tree.
            let (ok, out) = self.run("git", &["checkout", "-b", &name])?;
            if !ok {
                return Err(HarnessError::Ship(format!(
                    "git checkout -b {name}: {} (the verified change is left uncommitted in the work tree)",
                    out.trim()
                )));
            }
            // -u: stage only tracked modifications — the harness owns the
            // tracked diff; untracked artifacts (target/) are not its fix.
            let (ok, out) = self.run("git", &["add", "-u", "--", "."])?;
            if !ok {
                return Err(HarnessError::Ship(format!(
                    "git add on {name}: {} (the verified change is left uncommitted on {name})",
                    out.trim()
                )));
            }
            let (ok, out) = self.run(
                "git",
                &["commit", "-m", &format!("joule-fix: {} lint findings remediated, all gates green", findings_before.saturating_sub(findings_after))],
            )?;
            if !ok {
                return Err(HarnessError::Ship(format!(
                    "git commit on {name}: {} (the verified change is left staged on {name})",
                    out.trim()
                )));
            }
            // A gate-verified stochastic fix is a lesson worth keeping:
            // compile it into a deterministic skill so the next recurrence
            // never pays the model's joules again.
            if used_l3 {
                self.induce_skills(&l3_snapshot);
            }
            Some(name)
        } else {
            // Never ship on a failed gate: revert the work tree — and VERIFY
            // the revert took. A swallowed revert failure leaves the rejected
            // diff in the user's tree, which is worse than shipping it.
            let _ = self.run("git", &["checkout", "--", "."]);
            if !self.git_clean()? {
                let _ = self.run("git", &["restore", "--source=HEAD", "--worktree", "--", "."]);
            }
            if !self.git_clean()? {
                return Err(HarnessError::Spawn(
                    "revert failed: rejected changes remain in the work tree — manual cleanup required".into(),
                ));
            }
            None
        };

        // ---- Energy: the per-window accounting accumulated across the run's
        // cargo subprocesses and its L3 model. When every window was
        // attributed, the receipts carry the ATTRIBUTED figure (ModelBased —
        // resting on real readings), not the machine-wide total. Otherwise
        // they carry an estimate and grade it as one — never a figure signed
        // as a reading.
        let (tally, meter_sources, l3) = {
            let acc = self.meter.borrow();
            (acc.tally.clone(), acc.meter.sources(), acc.l3.clone())
        };
        let (soc_cpu_uj, attributed_uj, attributed) = (tally.soc_uj, tally.attr_uj, tally.attributed());
        let wall = wall_start.elapsed();
        let base_source = tally.source(&meter_sources);
        let meter_source = match &l3 {
            Some(l3) => format!("{base_source}; {}", l3.describe()),
            None => base_source,
        };

        // The sandbox meter receipt seals the receipts' figure with its grade:
        // ModelBased for an attribution, the Estimator grade for an estimate.
        // The JouleContract receipt anchors to it only when attributed.
        let meter_receipt = sandbox_meter::Receipt::build(
            sandbox_schema::ContentId::of_bytes(prior_rev.as_bytes()),
            sandbox_schema::Tier::S0,
            tally.meter_records(),
            1,
            [3u8; 8],
        )
        .map_err(|e| HarnessError::Contract(e.to_string()))?;
        let meter_envelope = meter_receipt
            .seal(&self.steward, &self.meter_signing)
            .map_err(|e| HarnessError::Contract(e.to_string()))?;

        let receipt = self.receipt(
            &contract,
            &op,
            &tally,
            &meter_envelope,
            &gates,
            findings_before,
            findings_after,
        )?;
        let verdict =
            validate(&contract, &receipt).map_err(|e| HarnessError::Contract(e.to_string()))?;
        let envelope = joulecontract_wire::emit(&receipt, &self.signing)
            .map_err(|e| HarnessError::Contract(e.to_string()))?;

        Ok(RunReport {
            findings_before,
            findings_after: if changed.is_empty() { None } else { Some(findings_after) },
            changed_files: changed,
            gates,
            shipped,
            branch,
            attributed_uj,
            soc_cpu_uj,
            attributed,
            l3,
            wall,
            meter_source,
            contract,
            receipt,
            envelope_json: serde_json::to_string_pretty(&envelope)
                .map_err(|e| HarnessError::Contract(e.to_string()))?,
            meter_envelope,
            local_claim: verdict.claim(),
            formal,
        })
    }

    /// Load and validate `<workspace>/.joule-fix/formal.json` (the formal tier's
    /// input) **before any edit is applied**, so a malformed spec fails fast on
    /// a clean tree rather than mid-run. `None` when no formal spec is present —
    /// the default, leaving the run identical to before. Index/duplicate checks
    /// mirror the proof bridge's so the later discharge cannot fail.
    fn load_formal_spec(&self) -> Result<Option<FormalSpec>, HarnessError> {
        let path = self.workspace.join(".joule-fix/formal.json");
        let Ok(text) = std::fs::read_to_string(&path) else {
            return Ok(None);
        };
        let spec: FormalSpec = serde_json::from_str(&text).map_err(|e| {
            HarnessError::Contract(format!(
                "formal.json: {e} — see formal.example.json for the exact serde forms \
                 (rigor_target JR-1..JR-4, enb_ref a 'sha2-256:<64-hex>' string, \
                 kind/grounding PascalCase)"
            ))
        })?;
        let n = spec.contract.obligations().len();
        let mut seen = BTreeSet::new();
        for f in &spec.formalizations {
            if f.obligation >= n {
                return Err(HarnessError::Contract(format!(
                    "formal.json: formalization names obligation {} but the contract declares {n}",
                    f.obligation
                )));
            }
            if !seen.insert(f.obligation) {
                return Err(HarnessError::Contract(format!(
                    "formal.json: duplicate formalization for obligation {}",
                    f.obligation
                )));
            }
        }
        Ok(Some(spec))
    }

    /// The formally-verified fix tier: discharge the loaded formalizations
    /// through the proof cascade over a real `z3` — a **decision-procedure
    /// ladder only** (`Propositional`, then `Z3Smt`): a formal gate must never
    /// fall through to a model stand-in. Writes the full per-obligation
    /// discharge to `.joule-fix/formal-discharge.json` as re-checkable evidence.
    fn discharge_formal(&self, spec: &FormalSpec) -> FormalOutcome {
        let router = Router::new(vec![Box::new(Propositional), Box::new(Z3Smt)]);
        let mut cache = ProofCache::new();
        // Indices were validated in `load_formal_spec`, so the only `Err` here
        // would be a bug; fail the gate safely rather than ship an unproven fix.
        let Ok(dis) = proof_discharge(&spec.contract, &spec.formalizations, &router, &mut cache)
        else {
            return FormalOutcome {
                proved: 0,
                refuted: 0,
                unproved: spec.formalizations.len(),
                proof_uj: 0,
                all_proved: false,
                entries: Vec::new(),
            };
        };

        let (mut proved, mut refuted, mut unproved) = (0usize, 0usize, 0usize);
        let mut entries = Vec::new();
        for e in &dis.entries {
            // Only obligations that were actually formalized belong to THIS
            // gate; unformalized ones are the operational gates' business and
            // the bridge records them separately (demoted, never dropped).
            let (verdict, closed_by, counter_model, uj) = match &e.status {
                DischargeStatus::Proved(r) => {
                    proved += 1;
                    ("proved", r.closed_by.map(|t| format!("{t:?}")), None, r.total_uj)
                }
                DischargeStatus::Unproved(r) if r.refuted => {
                    refuted += 1;
                    ("refuted", None, r.counter_model.clone(), r.total_uj)
                }
                DischargeStatus::Unproved(r) => {
                    unproved += 1;
                    ("unproved", None, None, r.total_uj)
                }
                DischargeStatus::Unformalized => continue,
            };
            entries.push(FormalEntry {
                obligation: e.obligation.text.clone(),
                verdict: verdict.into(),
                closed_by,
                counter_model,
                uj,
            });
        }
        let supplied = proved + refuted + unproved;
        // The gate: at least one formalization, and every one proved. Any
        // refutation or unproven goal fails it (and reverts the fix).
        let all_proved = supplied > 0 && refuted == 0 && unproved == 0;
        let proof_uj = entries.iter().map(|e| e.uj).sum();

        // Evidence an auditor can re-check independently of this report.
        let evidence = self.workspace.join(".joule-fix/formal-discharge.json");
        if let Some(dir) = evidence.parent() {
            let _ = std::fs::create_dir_all(dir);
        }
        if let Ok(j) = serde_json::to_string_pretty(&dis) {
            let _ = std::fs::write(&evidence, j);
        }

        FormalOutcome { proved, refuted, unproved, proof_uj, all_proved, entries }
    }

    /// The current per-location findings (short-format diagnostic lines).
    fn current_findings(&self) -> Result<Vec<String>, HarnessError> {
        let (_, lint_out) = self.run(
            "cargo",
            &["clippy", "--workspace", "--message-format=short", "--quiet"],
        )?;
        Ok(lint_out
            .lines()
            .filter(|l| l.contains(".rs:") && (l.contains(": warning:") || l.contains(": error:")))
            .map(str::to_string)
            .collect())
    }

    /// The induced-skill tier: for each remaining finding whose message
    /// matches a stored skill, apply the line transform deterministically.
    /// Zero inference; the gates still judge the result like anyone else's.
    fn skill_pass(&self) -> Result<usize, HarnessError> {
        let mut store = SkillStore::load(&self.skill_store);
        if store.skills.is_empty() {
            return Ok(0);
        }
        let mut applied = 0usize;
        for finding in self.current_findings()? {
            let (Some(path), Some(key)) = (finding.split(':').next(), message_key(&finding)) else {
                continue;
            };
            if !path.ends_with(".rs") {
                continue;
            }
            let Some(skill) = store.skills.iter_mut().find(|s| s.message_key == key) else {
                continue;
            };
            let full = self.workspace.join(path);
            let Ok(content) = std::fs::read_to_string(&full) else { continue };
            let mut lines: Vec<String> = content.lines().map(str::to_string).collect();
            let mut hit = false;
            for line in lines.iter_mut() {
                if line.trim() == skill.old_line {
                    let indent: String = line.chars().take_while(|c| c.is_whitespace()).collect();
                    *line = format!("{indent}{}", skill.new_line);
                    hit = true;
                    break;
                }
            }
            if hit {
                let mut out = lines.join("\n");
                if content.ends_with('\n') {
                    out.push('\n');
                }
                if std::fs::write(&full, out).is_ok() {
                    skill.hits += 1;
                    applied += 1;
                }
            }
        }
        if applied > 0 {
            store.save(&self.skill_store);
        }
        Ok(applied)
    }

    /// Induce skills from a SHIPPED stochastic fix. The rule is anchored to
    /// the finding's OFFENDING LINE: when it vanished from the fixed file,
    /// its replacement is the new line sharing the longest common prefix
    /// (models reformat around the fix; the lesson is the line, not the
    /// file). Only gate-verified lessons compile; a reverted fix teaches
    /// nothing — and a badly-induced skill cannot ship damage either, since
    /// every application faces the same gates.
    fn induce_skills(&self, snapshot: &[(String, String, String, String)]) {
        let mut store = SkillStore::load(&self.skill_store);
        let mut induced = false;
        for (path, key, offending, old_content) in snapshot {
            if offending.is_empty() || store.skills.iter().any(|s| s.message_key == *key) {
                continue;
            }
            let Ok(new_content) = std::fs::read_to_string(self.workspace.join(path)) else {
                continue;
            };
            let new_trimmed: Vec<&str> =
                new_content.lines().map(str::trim).filter(|l| !l.is_empty()).collect();
            if new_trimmed.contains(&offending.as_str()) {
                continue; // the offending line survived: nothing was learned
            }
            let old_set: BTreeSet<&str> = old_content.lines().map(str::trim).collect();
            let common_prefix = |a: &str, b: &str| -> usize {
                a.bytes().zip(b.bytes()).take_while(|(x, y)| x == y).count()
            };
            let Some((best, plen)) = new_trimmed
                .iter()
                .filter(|l| !old_set.contains(**l))
                .map(|l| (*l, common_prefix(l, offending)))
                .max_by_key(|(_, p)| *p)
            else {
                continue;
            };
            // The replacement must visibly descend from the offending line.
            if plen < 6.max(offending.len() / 4) {
                continue;
            }
            store.skills.push(Skill {
                message_key: key.clone(),
                old_line: offending.clone(),
                new_line: best.to_string(),
                hits: 0,
            });
            induced = true;
        }
        if induced {
            store.save(&self.skill_store);
        }
    }

    /// One L3 consultation: prompt = the remaining findings plus the touched
    /// files' contents; reply = SEARCH/REPLACE blocks, applied verbatim.
    /// Returns true when the model changed anything. The GATES decide whether
    /// any of it survives — this function trusts nothing it applies. The
    /// model's command is metered and its energy enters the run's figure
    /// ([`run_l3`](Self::run_l3)).
    fn l3_pass(&self) -> Result<bool, HarnessError> {
        let cmd = self.l3_cmd.as_ref().expect("caller checked");

        let all = self.current_findings()?;
        let findings: Vec<&str> = all.iter().map(String::as_str).take(8).collect();
        let mut files: BTreeSet<String> = BTreeSet::new();
        for f in &findings {
            if let Some(path) = f.split(':').next() {
                if path.ends_with(".rs") && self.workspace.join(path).exists() {
                    files.insert(path.to_string());
                }
            }
        }
        let single_file = (files.len() == 1).then(|| files.iter().next().cloned().unwrap());
        let mut prompt = if let Some(f) = &single_file {
            // Whole-file replacement: the easier task for a small model, and
            // the gates plus the diff guard bound the blast radius.
            format!(
                "Fix the Rust lint findings below by correcting the file. Reply with the                  COMPLETE corrected contents of {f} in a single ```rust code fence.                  No explanation.\n\nFindings:\n"
            )
        } else {
            String::from(
                "Fix the following Rust lint findings. Reply ONLY with one or more blocks of the form:\n                 <<<<<<< SEARCH <path>\n<exact text to find>\n=======\n<replacement>\n>>>>>>> REPLACE\n\nFindings:\n",
            )
        };
        for f in &findings {
            prompt.push_str(f);
            prompt.push('\n');
        }
        for path in &files {
            if let Ok(body) = std::fs::read_to_string(self.workspace.join(path)) {
                prompt.push_str(&format!("\n--- {path} ---\n{body}"));
            }
        }

        let reply = self.run_l3(cmd, prompt.as_bytes())?;

        if self.apply_search_replace(&reply) {
            return Ok(true);
        }
        if let Some(f) = &single_file {
            return Ok(self.apply_fenced_file(&reply, f));
        }
        Ok(false)
    }

    /// Run the L3 command on `prompt` and meter it: its stdout, with the
    /// window's [`L3Energy`] added to this run's tally.
    ///
    /// The command is spawned as [`l3_script`] says, waiting on its gate.
    /// The tree meter (where this host has one) is rooted at that process and
    /// reads it at rest; the machine-wide span opens; the gate line and the
    /// prompt go to its stdin, and it runs. Its stdout is read to the end, it
    /// is waited for without being reaped, so its exited count is still
    /// readable, and the tree meter's span is stopped on it; then it is
    /// reaped and the machine-wide span closed. [`grade_l3`] grades the two.
    fn run_l3(&self, cmd: &str, prompt: &[u8]) -> Result<String, HarnessError> {
        use std::io::{Read, Write};
        let (script, direct_child) = l3_script(cmd);
        // The per-process counter's liveness probe burns about 300 ms of CPU
        // on this thread the first time: here, before anything is spawned.
        let _ = sandbox_meter::process_energy_status();
        let mut child = Command::new("sh")
            .args(["-c", &script])
            .current_dir(&self.workspace)
            .stdin(std::process::Stdio::piped())
            .stdout(std::process::Stdio::piped())
            .stderr(std::process::Stdio::null())
            .spawn()
            .map_err(|e| HarnessError::Spawn(format!("L3 cmd: {e}")))?;
        let pid = child.id();
        // `None` off macOS, where the per-process counter is not live, or
        // where the process cannot be read.
        let tree = TreeMeter::for_process(pid);
        let tree_start = tree.as_ref().map(TreeMeter::start);

        let mut acc = self.meter.borrow_mut();
        let machine = acc.meter.start();
        if let Some(mut stdin) = child.stdin.take() {
            // The gate, then the prompt; dropping stdin closes it. A command
            // that stops reading early closes the pipe, and the rest of the
            // prompt is its own business, as it always was.
            let _ = stdin.write_all(b"\n").and_then(|()| stdin.write_all(prompt));
        }
        let mut reply = Vec::new();
        if let Some(mut out) = child.stdout.take() {
            let _ = out.read_to_end(&mut reply);
        }
        let reading = match (&tree, tree_start) {
            (Some(tree), Some(start)) => {
                // Exited and not reaped: the stop walk reads its final record.
                // Should the wait fail, the walk reads whatever the process is
                // then, and its gaps say so.
                let _ = wait_exited_unreaped(pid);
                Some(tree.stop(start))
            }
            _ => None,
        };
        let status = child.wait();
        let m = machine.stop(&mut acc.meter);
        let by_class = m.devices.iter().map(|d| (d.class, d.measured_uj.unwrap_or(d.estimated_uj))).collect();
        let l3 = grade_l3(reading.as_ref(), by_class, direct_child);
        acc.tally.add_l3(&l3);
        acc.l3 = Some(l3);
        status.map_err(|e| HarnessError::Spawn(format!("L3 cmd: {e}")))?;
        Ok(String::from_utf8_lossy(&reply).into_owned())
    }

    /// Apply a whole-file reply: the first fenced code block becomes the
    /// file's new contents. Trusts nothing — the gates judge the result.
    fn apply_fenced_file(&self, reply: &str, path: &str) -> bool {
        let Some(open) = reply.find("```") else { return false };
        let after = &reply[open + 3..];
        let Some(nl) = after.find('\n') else { return false };
        let body = &after[nl + 1..];
        let Some(close) = body.find("\n```") else { return false };
        let new_content = &body[..close + 1];
        if new_content.trim().is_empty() {
            return false;
        }
        std::fs::write(self.workspace.join(path), new_content).is_ok()
    }

    /// Apply SEARCH/REPLACE blocks. Unparseable or non-matching blocks are
    /// skipped — the model gets no error channel and no second chance; the
    /// lint-delta gate will simply find its work insufficient.
    fn apply_search_replace(&self, reply: &str) -> bool {
        let mut applied = false;
        let mut rest = reply;
        while let Some(start) = rest.find("<<<<<<< SEARCH ") {
            let block = &rest[start + "<<<<<<< SEARCH ".len()..];
            let Some(nl) = block.find('\n') else { break };
            let path = block[..nl].trim().to_string();
            let body = &block[nl + 1..];
            let (Some(sep), Some(end)) = (body.find("\n=======\n"), body.find("\n>>>>>>> REPLACE")) else {
                break;
            };
            if sep < end {
                let search = &body[..sep];
                let replace = &body[sep + "\n=======\n".len()..end];
                let full = self.workspace.join(&path);
                // Path safety belongs to the frame gate, but directory
                // traversal never even gets applied.
                if !path.contains("..") && full.exists() {
                    if let Ok(content) = std::fs::read_to_string(&full) {
                        if content.contains(search) {
                            let new_content = content.replacen(search, replace, 1);
                            if std::fs::write(&full, new_content).is_ok() {
                                applied = true;
                            }
                        }
                    }
                }
            }
            rest = &body[end..];
        }
        applied
    }

    /// The run's contract: the gates, stated as obligations.
    fn contract(&self, frame: &[String], findings: usize) -> Contract {
        Contract {
            joulecontract: "0.8.0".into(),
            subject: format!("L1 lint remediation of {findings} findings in {}", self.workspace.display()),
            rigor_target: Rigor::Jr2,
            pre: vec!["baseline captured: test failures and lint findings recorded before any edit".into()],
            post: vec![
                "build succeeds after the fix".into(),
                "no test failures beyond the recorded baseline".into(),
                "lint finding count strictly decreased".into(),
            ],
            inv: vec![format!(
                "total diff within {} changed lines",
                self.max_diff_lines
            )],
            frame: frame.to_vec(),
            ceiling: Ceiling {
                enpi_joules: self.ceiling_joules,
                unit: "EOC-J".into(),
                enb_ref: ContentAddress::of_bytes(b"joule-fix L1 EnB v0: host cargo pipeline, no inference"),
                derivation: None, // honestly unanchored until an energy office signs a basis
            },
            sector_equivalence: None,
            amends: None,
        }
    }

    /// Build the receipt: one discharge entry per obligation, result taken
    /// from the matching gate's ACTUAL outcome.
    #[allow(clippy::too_many_arguments)]
    fn receipt(
        &self,
        contract: &Contract,
        op: &CodingOp,
        energy: &EnergyTally,
        meter_envelope: &[u8],
        gates: &[GateOutcome],
        before: usize,
        after: usize,
    ) -> Result<Receipt, HarnessError> {
        let gate_for = |kind: &ObligationKind, text: &str| -> &GateOutcome {
            let name = match (kind, text) {
                (ObligationKind::Pre, _) => "baseline",
                (ObligationKind::Post, t) if t.starts_with("build") => "build",
                (ObligationKind::Post, t) if t.starts_with("no test") => "tests-vs-baseline",
                (ObligationKind::Post, _) => "lint-delta",
                (ObligationKind::Inv, _) => "diff-guard",
                (ObligationKind::Frame, _) => "frame",
            };
            gates.iter().find(|g| g.gate == name).expect("gate exists")
        };

        let harness_key = ContentAddress::of_bytes(self.signing.verifying_key().as_bytes());
        let tier_addr = ContentAddress::of_bytes(b"joule-fix L1 lawful pipeline v0");
        let qualification = Qualification {
            attestation: ContentAddress::of_bytes(b"joule-fix gate suite v0: cargo build/test/clippy as deterministic verifiers"),
            signer_key: harness_key.clone(),
            valid_until: u64::MAX,
            validated_at: 0,
            root: Some(TrustRoot::ReferenceImpl),
        };

        let discharge: Vec<DischargeEntry> = contract
            .obligations()
            .into_iter()
            .map(|ob| {
                let gate = gate_for(&ob.kind, &ob.text);
                let is_frame = ob.kind == ObligationKind::Frame;
                DischargeEntry {
                    obligation: ob,
                    tier: tier_addr.clone(),
                    tier_class: TierClass::Deterministic,
                    tier_operator_keys: BTreeSet::from([harness_key.clone()]),
                    result: if gate.passed {
                        DischargeResult::Closed
                    } else {
                        DischargeResult::Undischarged {
                            reason: format!("{}: {}", gate.gate, gate.detail),
                        }
                    },
                    mode: is_frame.then_some(FrameMode::Observed),
                    qualification: Some(qualification.clone()),
                    verifier_keys: BTreeSet::from([harness_key.clone()]),
                    // Self-run harness: verifier == generator party, stated
                    // plainly. Independence computes false and the receipt
                    // grades accordingly — that's the honest local ceiling.
                    verifier_entity: None,
                    engagement: Some(Engagement {
                        selected_by: self.steward.clone(),
                        compensated_by: self.steward.clone(),
                    }),
                    recourse: None,
                    re_discharged_by: None,
                }
            })
            .collect();

        // An attributed figure is an apportionment of a real SoC reading:
        // ModelBased, never Metered (a process is not a shunt), and anchored
        // to the sealed sandbox meter receipt that carries it. Unless every
        // window was attributed, the figure is an estimate, and Unaccounted
        // (energy estimated where the substrate exposes no reading) is the
        // honest class.
        let provenance = energy.energy_class();
        let energy_anchor =
            energy.attributed().then(|| ContentAddress::of_bytes(meter_envelope));
        // No MeterBinding: that attests a Metered (direct-shunt) figure, which
        // this is not. The energy_anchor is the ModelBased evidence path.
        let meter: Option<MeterBinding> = None;

        Ok(Receipt {
            contract: contract
                .content_address()
                .map_err(|e| HarnessError::Contract(e.to_string()))?,
            transition: joule_code_joulecontract::bridge_id(&op.prior),
            generator: Generator {
                system: format!("joule-fix v0 (L1 lawful: clippy --fix + rustfmt; {before}→{after} findings)"),
                version_digest: ContentAddress::of_bytes(env!("CARGO_PKG_VERSION").as_bytes()),
                attestation: None, // self-run: honestly generator_unattested
                attestation_signer: None,
                key_set: BTreeSet::from([harness_key.clone()]),
                entity: None,
                human_principals: vec![self.steward.clone()],
                loop_governance: None,
            },
            discharge,
            execution: vec![tier_addr],
            joules_spent: energy.figure_uj() as f64 / 1e6,
            meter,
            energy_anchor,
            joules_allowed: contract.ceiling.enpi_joules,
            provenance,
            enb_ref: contract.ceiling.enb_ref.clone(),
            grid_mix: None,
            register_pin: ContentAddress::of_bytes(b"joule-fix register v0"),
            evidence: None, // local receipt: evidence:external, stated not hidden
            claimed_profile: Profile {
                rigor: Rigor::Jr1, // self-verified: independence computes false
                energy: provenance,
                governance: GovernanceClass::Declared,
            },
            receipt_signer: harness_key,
        })
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    fn sh(dir: &std::path::Path, cmd: &str) {
        let ok = Command::new("sh")
            .arg("-c")
            .arg(cmd)
            .current_dir(dir)
            .output()
            .map(|o| o.status.success())
            .unwrap_or(false);
        assert!(ok, "setup command failed: {cmd}");
    }

    /// Build a scratch git crate with deterministic, clippy-fixable findings.
    fn scratch_crate(label: &str) -> PathBuf {
        let dir = std::env::temp_dir().join(format!("joule-fix-test-{label}-{}", std::process::id()));
        let _ = std::fs::remove_dir_all(&dir);
        std::fs::create_dir_all(dir.join("src")).unwrap();
        std::fs::write(
            dir.join("Cargo.toml"),
            "[package]\nname = \"scratch\"\nversion = \"0.1.0\"\nedition = \"2021\"\n\n[workspace]\n",
        )
        .unwrap();
        std::fs::write(
            dir.join("src/main.rs"),
            r#"fn answer() -> u64 { return 42; }
fn main() { let x: u64 = answer(); println!("{}", x); }
#[test]
fn answers() { assert_eq!(answer(), 42); }
"#,
        )
        .unwrap();
        // A repo-local identity: the harness's own ship commit must work in
        // any environment, including a CI container with no global git
        // identity (where it used to fail silently and leave the tree dirty).
        sh(&dir, "git init -q && git config user.email t@t && git config user.name t && git add -A && git commit -qm init");
        dir
    }

    fn git_out(dir: &std::path::Path, args: &[&str]) -> String {
        let o = Command::new("git").args(args).current_dir(dir).output().unwrap();
        assert!(o.status.success(), "git {args:?}: {}", String::from_utf8_lossy(&o.stderr));
        String::from_utf8_lossy(&o.stdout).trim().to_string()
    }

    #[test]
    fn verified_fix_end_to_end_ships_with_receipt() {
        let dir = scratch_crate("ship");
        let before = git_out(&dir, &["rev-parse", "HEAD"]);
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        // A test's cargo runs build in the scratch crate's own `target/`:
        // `--target-dir` follows the subcommand and outranks an inherited
        // `CARGO_TARGET_DIR`, under which every scratch crate (each named
        // `scratch`) would share one target directory with the other tests'.
        let own_target = dir.join("target");
        assert_eq!(
            h.cargo_args(&["test", "--workspace"]),
            ["test", "--target-dir", own_target.to_str().unwrap(), "--workspace"]
        );
        let report = h.run_once().unwrap();
        assert!(own_target.join("debug").is_dir(), "the scratch crate did not build in its own target directory");

        assert!(report.findings_before > 0, "scratch crate has findings");
        assert!(report.shipped, "gates: {:?}", report.gates);
        assert!(report.gates.iter().all(|g| g.passed));
        assert_eq!(report.findings_after, Some(0));
        // Shipped means committed: the fix is a commit on the reported branch,
        // on top of where the run started, and nothing is left uncommitted.
        let branch = report.branch.clone().expect("a shipped fix names its branch");
        assert_eq!(git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]), branch);
        assert_eq!(git_out(&dir, &["rev-parse", "HEAD~1"]), before, "one commit on top of the start");
        assert!(git_out(&dir, &["status", "--porcelain", "--untracked-files=no"]).is_empty(), "shipped, yet the tree is dirty");
        // Work ran, so the figure is never zero — attributed or estimated.
        assert!(report.total_uj() > 0, "{} µJ ({})", report.total_uj(), report.meter_source);
        assert!(report.uj_per_verified_fix().is_some_and(|uj| uj > 0));

        // Both receipts grade the figure by how it was obtained.
        eprintln!(
            "joule-fix run: attributed={} total_uj={} soc_cpu_uj={} attributed_uj={} ({})",
            report.attributed, report.total_uj(), report.soc_cpu_uj, report.attributed_uj, report.meter_source
        );
        assert_eq!(report.receipt.joules_spent, report.total_uj() as f64 / 1e6);
        let sealed = sandbox_meter::jcr1::open(&report.meter_envelope).expect("meter envelope").payload;
        let seals = |grade: &str| sealed.windows(grade.len()).any(|w| w == grade.as_bytes());
        if report.attributed {
            assert_eq!(report.receipt.provenance, EnergyClass::ModelBased);
            assert!(seals("ModelBased") && !seals("Estimator"), "meter envelope grade");
        } else {
            assert_eq!(report.receipt.provenance, EnergyClass::Unaccounted);
            assert!(report.receipt.energy_anchor.is_none());
            assert!(
                seals("Estimator") && !seals("ModelBased"),
                "an estimate sealed in the meter envelope as ModelBased"
            );
        }
        // Where the meter cannot read CPU energy at all, nothing is attributed.
        #[cfg(all(target_os = "macos", target_arch = "aarch64"))]
        if sandbox_meter::ioreport_status() != sandbox_meter::IoReportStatus::Live {
            assert!(!report.attributed, "attributed with no live CPU rail ({:?})", sandbox_meter::ioreport_status());
        }
        #[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
        assert!(!report.attributed, "the unattributed fallback never attributes");

        // The receipt validates locally and tells the truth about itself:
        // self-verified ⇒ independence false ⇒ JR-1 ceiling, stated.
        let v = validate(&report.contract, &report.receipt).unwrap();
        assert!(v.permits(&report.receipt.claimed_profile), "claim: {}", v.claim());
        assert!(report.envelope_json.contains("in-toto"));

        let _ = std::fs::remove_dir_all(&dir);
    }

    /// A fix that passes every gate but cannot be committed did not ship.
    /// The harness used to discard `git commit`'s result and report
    /// `shipped: true` with a branch name while the fix sat uncommitted.
    /// That is what a CI container with no git identity produced.
    #[test]
    fn a_fix_whose_commit_is_rejected_is_never_reported_shipped() {
        let dir = scratch_crate("commit-rejected");
        sh(&dir, "printf '#!/bin/sh\\nexit 1\\n' > .git/hooks/pre-commit && chmod +x .git/hooks/pre-commit");
        let before = git_out(&dir, &["rev-parse", "HEAD"]);
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        match h.run_once() {
            Err(HarnessError::Ship(msg)) => assert!(msg.contains("git commit"), "{msg}"),
            other => panic!("a rejected commit must not ship: {:?}", other.map(|r| (r.shipped, r.branch))),
        }
        assert_eq!(git_out(&dir, &["rev-parse", "HEAD"]), before, "nothing was committed");
        let _ = std::fs::remove_dir_all(&dir);
    }

    /// When the fix's branch already exists, the harness must not commit the
    /// fix onto whatever branch happens to be checked out.
    #[test]
    fn a_fix_never_lands_on_the_current_branch_when_its_own_branch_exists() {
        let dir = scratch_crate("branch-exists");
        let before = git_out(&dir, &["rev-parse", "HEAD"]);
        let current = git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]);
        git_out(&dir, &["branch", &format!("joule-fix/{}", &before[..12])]);
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        match h.run_once() {
            Err(HarnessError::Ship(msg)) => assert!(msg.contains("checkout -b"), "{msg}"),
            other => panic!("an existing branch must stop the ship: {:?}", other.map(|r| (r.shipped, r.branch))),
        }
        assert_eq!(git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]), current);
        assert_eq!(git_out(&dir, &["rev-parse", "HEAD"]), before, "the fix was committed onto {current}");
        let _ = std::fs::remove_dir_all(&dir);
    }

    /// One metered cargo window, as `run_attributed` reports it.
    fn window(soc_cpu_uj: u64, attributed_uj: u64, attributed: bool) -> Attribution {
        let source = if attributed { "ioreport-energy-model" } else { "estimator" };
        window_read_by(soc_cpu_uj, attributed_uj, attributed, source)
    }

    /// [`window`], its figure read by the probe named `source`.
    fn window_read_by(soc_cpu_uj: u64, attributed_uj: u64, attributed: bool, source: &'static str) -> Attribution {
        Attribution {
            soc_cpu_uj,
            attributed_uj,
            proc_cpu_secs: 1.0,
            busy_cpu_secs: if attributed_uj > 0 { 4.0 } else { 0.0 },
            share: if attributed_uj > 0 { 0.25 } else { 0.0 },
            wall: Duration::from_secs(1),
            attributed,
            // cargo runs its work in descendants: never a per-child reading.
            child_energy_uj: None,
            source,
        }
    }

    /// An attributed run's meter source names the probes its windows were read
    /// by, as the meter reported them — never a counter it did not read.
    #[test]
    fn an_attributed_run_names_the_probes_that_read_it() {
        let mut t = EnergyTally::default();
        t.add(&window_read_by(10_000_000, 2_500_000, true, "rapl-powercap"));
        t.add(&window_read_by(30_000_000, 7_500_000, true, "rapl-powercap"));
        assert!(t.attributed());
        let source = t.source(&["rapl-powercap", "nvml-total-energy"]);
        assert_eq!(source, "attributed(ModelBased over rapl-powercap HwShunt)");
        assert!(!source.contains("IOReport"), "{source}");

        t.add(&window_read_by(10_000_000, 2_500_000, true, "composite"));
        assert_eq!(t.source(&[]), "attributed(ModelBased over composite+rapl-powercap HwShunt)");

        // An estimate names the meter's sources, not any window's.
        let mut est = EnergyTally::default();
        est.add(&window(20_000_000, 0, false));
        assert!(est.source(&["ioreport-energy-model"]).starts_with("estimated(Unaccounted)"));
        assert!(est.source(&[]).contains("no live energy counter"));
    }

    /// A run whose windows were estimated is sealed as an estimate, and never
    /// as an apportioned zero. This is every macOS 27.0.1 host checked, where
    /// the meter has no live CPU counter. main sealed 0 J `ModelBased` there,
    /// and the core fix alone still sealed the apportioned estimate
    /// `ModelBased` in the meter envelope, and 0 J whenever the tick counters
    /// missed every window.
    #[test]
    fn an_unattributed_run_is_sealed_as_an_estimate_never_an_apportioned_zero() {
        let mut t = EnergyTally::default();
        // The machine tick counters missed this window: share 0.
        t.add(&window(20_000_000, 0, false));
        t.add(&window(40_000_000, 10_000_000, false));
        assert!(!t.attributed());
        assert_eq!(t.figure_uj(), 60_000_000, "the unapportioned estimate");
        assert_eq!(t.energy_class(), EnergyClass::Unaccounted);
        let records = t.meter_records();
        assert_eq!(records.len(), 1, "cargo windows are the CPU's alone: {records:?}");
        let r = &records[0];
        assert_eq!(r.provenance, sandbox_meter::Provenance::Estimator);
        assert_eq!((r.measured_uj, r.estimated_uj), (None, 60_000_000));
        r.check_provenance().unwrap();

        // Even when every window's share was lost, the run is not free.
        let mut missed = EnergyTally::default();
        missed.add(&window(20_000_000, 0, false));
        assert_eq!(missed.figure_uj(), 20_000_000);
    }

    /// Each run on a Harness seals its own cargo windows only. The tally a
    /// run leaves behind (here with a stale window added on top, so the
    /// assertion does not depend on run 1's figure) never reaches the next
    /// run's figure, grade or receipts.
    #[test]
    fn a_second_run_seals_only_its_own_cargo_windows() {
        const STALE_UJ: u64 = 1_000_000_000_000_000; // 1 GJ: no scratch run comes near it
        let dir = scratch_crate("rerun");
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        let first = h.run_once().unwrap();
        assert!(first.shipped, "gates: {:?}", first.gates);
        {
            // Run 1's windows are still in the tally when run 1 returns.
            let acc = h.meter.borrow();
            assert!(acc.tally.windows > 0, "run 1 metered its cargo calls");
            assert_eq!(acc.tally.soc_uj, first.soc_cpu_uj);
        }
        h.meter.borrow_mut().tally.add(&window(STALE_UJ, STALE_UJ, true));

        let second = h.run_once().unwrap();
        eprintln!(
            "joule-fix rerun: first soc_cpu_uj={} second soc_cpu_uj={} attributed={} ({})",
            first.soc_cpu_uj, second.soc_cpu_uj, second.attributed, second.meter_source
        );
        assert!(second.soc_cpu_uj < STALE_UJ, "run 2 sealed an earlier run's windows: {} µJ", second.soc_cpu_uj);
        assert!(second.attributed_uj < STALE_UJ, "{}", second.attributed_uj);
        assert!(second.total_uj() > 0, "run 2's own cargo calls ran");
        assert!(second.receipt.joules_spent < STALE_UJ as f64 / 1e6);
        assert_eq!(second.receipt.joules_spent, second.total_uj() as f64 / 1e6);
        let acc = h.meter.borrow();
        assert_eq!(acc.tally.soc_uj, second.soc_cpu_uj, "the tally holds run 2's windows alone");
        assert_eq!(acc.tally.attributed(), second.attributed);
        drop(acc);
        let _ = std::fs::remove_dir_all(&dir);
    }

    /// `ModelBased` only when every window was attributed: one estimated
    /// window makes the sum an estimate. main labelled the run attributed if
    /// any window was, and never reset that between runs.
    #[test]
    fn a_run_is_attributed_only_when_every_window_was() {
        let mut all = EnergyTally::default();
        all.add(&window(10_000_000, 2_500_000, true));
        all.add(&window(30_000_000, 7_500_000, true));
        assert!(all.attributed());
        assert_eq!(all.figure_uj(), 10_000_000, "the apportioned reading");
        assert_eq!(all.energy_class(), EnergyClass::ModelBased);
        let records = all.meter_records();
        assert_eq!(records.len(), 1, "{records:?}");
        assert_eq!((records[0].class, records[0].provenance), (DeviceClass::Cpu, sandbox_meter::Provenance::ModelBased));
        records[0].check_provenance().unwrap();

        let mut mixed = all;
        mixed.add(&window(20_000_000, 0, false));
        assert!(!mixed.attributed());
        assert_eq!(mixed.figure_uj(), 60_000_000, "the unapportioned estimate");
        assert_eq!(mixed.energy_class(), EnergyClass::Unaccounted);
        assert_eq!(mixed.meter_records()[0].provenance, sandbox_meter::Provenance::Estimator);

        // Nothing metered is not an attribution either.
        assert!(!EnergyTally::default().attributed());
    }

    #[test]
    fn l3_fix_passes_the_same_gates() {
        // A finding clippy --fix can NOT auto-fix (approx_constant): L1
        // leaves it, the configured L3 subprocess fixes it, the gates verify.
        let dir = scratch_crate("l3ship");
        std::fs::write(
            dir.join("src/main.rs"),
            "fn main() { let pi = 3.14; println!(\"{}\", pi); }\n",
        )
        .unwrap();
        // The mock L3 fixer: a deterministic stand-in at the exact seam a
        // jouleclaw decode binary plugs into.
        let fixer = dir.join("mock-l3.sh");
        std::fs::write(
            &fixer,
            "#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
'<<<<<<< SEARCH src/main.rs' \
'fn main() { let pi = 3.14; println!(\"{}\", pi); }' \
'=======' \
'fn main() { let pi = std::f64::consts::PI; println!(\"{}\", pi); }' \
'>>>>>>> REPLACE'\n",
        )
        .unwrap();
        sh(&dir, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");

        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        h.l3_cmd = Some("./mock-l3.sh".into());
        let report = h.run_once().unwrap();

        assert!(report.findings_before > 0);
        assert!(report.shipped, "gates: {:?}", report.gates);
        assert_eq!(report.findings_after, Some(0));
        assert_eq!(report.receipt.discharge.len(), report.contract.obligations().len());
        // The op records the stochastic tier; the receipt still validates.
        assert!(report.local_claim.contains("JR-1"));
        let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
        assert!(src.contains("std::f64::consts::PI"));

        // The model's window was metered and is in the run's figure. The
        // mock is a shell script that forks `cat`: on a host that reads the
        // model's own process, that reaped `cat` is a gap, so the window is
        // an estimate holding the reading and the machine-wide figure.
        let l3 = report.l3.clone().expect("the L3 window was metered");
        eprintln!("l3 window: {l3:?}; run total {} µJ ({})", report.total_uj(), report.meter_source);
        assert!(l3.machine_uj > 0 && l3.figure_uj >= l3.machine_uj, "{l3:?}");
        assert!(l3.direct_child, "`./mock-l3.sh` is a plain argv");
        assert!(!report.attributed, "an L3 window is never attributed");
        assert!(report.total_uj() >= l3.figure_uj, "{} µJ total < the L3 window's {l3:?}", report.total_uj());
        assert!(report.meter_source.contains("L3 model"), "{}", report.meter_source);
        if let Some(read) = l3.process_cpu_uj {
            assert_eq!(l3.figure_uj, read + l3.machine_uj, "{l3:?}");
            assert!(l3.partial_because.iter().any(|w| w.contains("reaped")), "the forked `cat`: {l3:?}");
            assert!(l3.partial_because.iter().any(|w| w.contains("exited")), "the script exited: {l3:?}");
        }

        let _ = std::fs::remove_dir_all(&dir);
    }

    /// The L3 window's grading, pure: a reading of the model's process tree
    /// is never attributed — whatever the gaps, it is an estimate of the
    /// window, the reading plus the machine-wide figure, and it always says
    /// why it is partial; no reading is the machine-wide figure alone.
    #[test]
    fn the_l3_window_is_never_attributed_and_a_reading_is_an_estimate() {
        use sandbox_meter::TreeGap;
        let reading = |cpu_nj: u64, gaps: Vec<TreeGap>| TreeReading {
            cpu_uj: cpu_nj.div_ceil(1_000),
            cpu_nj,
            processes: 1,
            pids: vec![4242],
            wall: Duration::from_secs(2),
            gaps,
        };
        let machine = 40_000_000;
        let cpu = || vec![(DeviceClass::Cpu, machine)];

        // The shape every model that exits in its window has.
        let exited = grade_l3(Some(&Ok(reading(3_000_000_001, vec![TreeGap::Exited { pid: 4242 }]))), cpu(), true);
        assert_eq!(exited.partial_because, vec![TreeGap::Exited { pid: 4242 }.to_string()]);
        assert_eq!((exited.process_cpu_uj, exited.figure_uj), (Some(3_000_001), 3_000_001 + machine), "rounded up");

        // No gap seen: the model was not read at its exit. Still an estimate.
        let no_gap = grade_l3(Some(&Ok(reading(3_000_000_000, vec![]))), cpu(), true);
        assert_eq!(no_gap.partial_because, vec![NOT_READ_AT_EXIT.to_string()]);
        assert_eq!(no_gap.figure_uj, 3_000_000 + machine);

        let gpu = grade_l3(Some(&Ok(reading(5_000, vec![TreeGap::Exited { pid: 1 }, TreeGap::Gpu { ns: 9 }]))), cpu(), false);
        assert_eq!(gpu.partial_because.len(), 2, "{gpu:?}");
        assert_eq!(gpu.figure_uj, 5 + machine);
        assert!(!gpu.direct_child);

        let no_reading = grade_l3(Some(&Err(TreeError::RootGone { pid: 4242 })), cpu(), true);
        assert_eq!((no_reading.process_cpu_uj, no_reading.figure_uj), (None, machine));
        assert!(no_reading.partial_because[0].contains("no reading"), "{no_reading:?}");

        let no_meter = grade_l3(None, cpu(), true);
        assert_eq!((no_meter.process_cpu_uj, no_meter.figure_uj), (None, machine));
        assert!(no_meter.partial_because.is_empty());

        // In the tally: an estimate, as `run_l3` adds it.
        for l3 in [&exited, &no_gap, &no_meter] {
            let mut t = EnergyTally::default();
            t.add_l3(l3);
            assert!(!t.attributed(), "{l3:?}");
            assert_eq!(t.figure_uj(), l3.figure_uj, "{l3:?}");
            assert_eq!(t.energy_class(), EnergyClass::Unaccounted, "never a reading of a partial window");
        }
    }

    /// The L3 window's machine-wide figure is sealed one record per device
    /// class: a GPU the meter read (an Apple GPU rail, NVML on Linux) is a
    /// `Gpu` record, never folded into the CPU's. The records sum to the
    /// run's figure, and the receipt builds from them.
    #[test]
    fn the_l3_windows_device_classes_are_sealed_apart() {
        use sandbox_meter::TreeGap;
        let reading = TreeReading {
            cpu_uj: 3_000_000,
            cpu_nj: 3_000_000_000,
            processes: 1,
            pids: vec![7],
            wall: Duration::from_secs(1),
            gaps: vec![TreeGap::Exited { pid: 7 }],
        };
        let machine = vec![(DeviceClass::Cpu, 30_000_000), (DeviceClass::Gpu, 10_000_000)];
        let l3 = grade_l3(Some(&Ok(reading)), machine, true);
        assert_eq!((l3.machine_uj, l3.figure_uj), (40_000_000, 43_000_000), "{l3:?}");

        let mut t = EnergyTally::default();
        t.add(&window(20_000_000, 5_000_000, true));
        t.add_l3(&l3);
        assert_eq!(t.figure_uj(), 63_000_000);
        let records = t.meter_records();
        let by_class: Vec<(DeviceClass, Option<u64>, u64, sandbox_meter::Provenance)> =
            records.iter().map(|r| (r.class, r.measured_uj, r.estimated_uj, r.provenance)).collect();
        let est = sandbox_meter::Provenance::Estimator;
        assert_eq!(
            by_class,
            [(DeviceClass::Cpu, None, 53_000_000, est), (DeviceClass::Gpu, None, 10_000_000, est)],
            "the CPU: the cargo window, the reading and the machine's CPU; the GPU apart"
        );
        let receipt = sandbox_meter::Receipt::build(
            sandbox_schema::ContentId::of_bytes(b"prior"),
            sandbox_schema::Tier::S0,
            records,
            1,
            [3u8; 8],
        )
        .expect("one record per class");
        assert_eq!(receipt.total.estimated_uj, t.figure_uj());

        // A second L3 window adds to its class's record.
        t.add_l3(&l3);
        assert_eq!(t.meter_records()[1].estimated_uj, 20_000_000);
        assert_eq!(t.meter_records().iter().map(|r| r.estimated_uj).sum::<u64>(), t.figure_uj());
    }

    /// A plain argv is `exec`ed after the gate, so the model is the meter's
    /// root process; anything that needs the shell runs as its script.
    #[test]
    fn a_plain_l3_command_is_execed_after_the_gate_and_a_shell_command_is_not() {
        let (script, direct) = l3_script("  granite-fix /models/granite-4.0-h_snapshot  ");
        assert!(direct);
        assert_eq!(script, "IFS= read -r joule_fix_gate || exit 1\nexec granite-fix /models/granite-4.0-h_snapshot\n");
        assert!(l3_script("./mock-l3.sh").1);
        assert!(l3_script("/bin/model --threads 8 -m a.gguf").1);
        for shell in [
            "model | tee log",
            "model; true",
            "MODEL_THREADS=8 model",
            "model > out",
            "model \"a b\"",
            "model $HOME/x",
            "~/bin/model",
            "model &",
            "",
        ] {
            let (script, direct) = l3_script(shell);
            assert!(!direct, "{shell:?}");
            assert!(script.starts_with("IFS= read -r joule_fix_gate || exit 1\n"), "{script}");
            assert!(!script.contains("exec "), "{script}");
        }
    }

    /// The stand-in model's marker and report, in its working directory (the
    /// scratch workspace).
    const STAND_IN_MARKER: &str = ".l3-stand-in";
    const STAND_IN_REPORT: &str = ".l3-stand-in-report";

    /// This process's own CPU energy count, nJ: `proc_pid_rusage(getpid(),
    /// RUSAGE_INFO_V6)`'s `ri_energy_nj`, read with a bare buffer of the
    /// struct's 464 bytes at its SDK offset, 336. Written out here, sharing
    /// no code with the meter it checks.
    #[cfg(target_os = "macos")]
    fn own_energy_nj() -> u64 {
        extern "C" {
            fn proc_pid_rusage(pid: i32, flavor: i32, buffer: *mut std::ffi::c_void) -> i32;
        }
        let mut buf = [0u64; 58];
        // SAFETY: `buf` is 464 writable bytes, the size of `rusage_info_v6`.
        let rc = unsafe { proc_pid_rusage(std::process::id() as i32, 6, buf.as_mut_ptr().cast()) };
        assert_eq!(rc, 0, "proc_pid_rusage on this process");
        buf[336 / 8]
    }

    #[cfg(not(target_os = "macos"))]
    fn own_energy_nj() -> u64 {
        0
    }

    /// Not a test of its own: the stand-in L3 model, run as a subprocess by
    /// [`the_l3_models_energy_enters_the_run_total_as_its_own_count_says`]
    /// (this test binary, filtered to this test). It reads its prompt to the
    /// end, does a fixed amount of CPU work, leaves the core (which folds its
    /// count), and writes its own count and the prompt's length to its
    /// working directory. Anywhere without its marker it returns at once.
    #[test]
    #[ignore = "a subprocess stand-in, run by the L3 energy test"]
    fn l3_stand_in_model() {
        use std::io::Read;
        let Ok(iterations) = std::fs::read_to_string(STAND_IN_MARKER) else { return };
        let iterations: u64 = iterations.trim().parse().expect("the marker holds an iteration count");
        let mut prompt = Vec::new();
        std::io::stdin().read_to_end(&mut prompt).expect("the prompt");
        let mut x = 1u64;
        for i in 0..iterations {
            x = std::hint::black_box(x.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(i));
        }
        std::thread::sleep(Duration::from_millis(20));
        std::fs::write(STAND_IN_REPORT, format!("{} {} {x}", own_energy_nj(), prompt.len())).expect("the report");
    }

    /// The L3 model's energy is now in the run's figure. The model here is a
    /// stand-in that burns a fixed amount of CPU and then reports its own
    /// energy count, read from inside it before it exits: the oracle, which
    /// shares no code with the tree meter. Where this host reads the model's
    /// process (macOS, the per-process counter live) the window's reading of
    /// it agrees with that count to within the shell's start-up before the
    /// gate (in the oracle, not the window) and the stand-in's tear-down
    /// after its report (in the window, not the oracle); the window is an
    /// estimate, partial because the model exited in it; and its figure, the
    /// reading plus the machine-wide figure, is what the run's tally holds.
    /// Elsewhere it is the machine-wide figure. Two windows, accumulated.
    #[test]
    fn the_l3_models_energy_enters_the_run_total_as_its_own_count_says() {
        // About a second of one core, unoptimized; a fixed amount of work,
        // however loaded the host.
        const ITERATIONS: u64 = 150_000_000;
        let dir = scratch_crate("l3-energy");
        std::fs::write(dir.join(STAND_IN_MARKER), ITERATIONS.to_string()).unwrap();
        let exe = std::env::current_exe().expect("this test binary");
        let cmd = format!("{} tests::l3_stand_in_model --exact --ignored", exe.display());
        let h = Harness::new(&dir).unwrap();
        let prompt = vec![b'p'; 100_000];
        let reads_processes =
            cfg!(target_os = "macos") && sandbox_meter::process_energy_status() == sandbox_meter::CounterStatus::Live;

        let mut figures = 0u64;
        for window in 1..=2u64 {
            let reply = h.run_l3(&cmd, &prompt).expect("the stand-in ran");
            assert!(reply.contains("1 passed"), "the stand-in did not run: {reply}");
            let report = std::fs::read_to_string(dir.join(STAND_IN_REPORT)).expect("the stand-in's report");
            let mut fields = report.split_whitespace().map(|f| f.parse::<u64>().unwrap());
            let (oracle_nj, prompt_len) = (fields.next().unwrap(), fields.next().unwrap());
            assert_eq!(prompt_len, prompt.len() as u64, "the model read the whole prompt, and not the gate");
            let acc = h.meter.borrow();
            let l3 = acc.l3.clone().expect("the window was metered");
            eprintln!("l3 window {window}: oracle {oracle_nj} nJ (the model's own count); {l3:?}");
            figures += l3.figure_uj;
            assert_eq!(acc.tally.windows, window);
            assert_eq!(acc.tally.figure_uj(), figures, "the run's figure holds every L3 window");
            assert!(!acc.tally.attributed());
            assert!(l3.machine_uj > 0, "{l3:?}");
            if reads_processes {
                assert!(l3.direct_child, "setup: {cmd} is a plain argv");
                let read = l3.process_cpu_uj.unwrap_or_else(|| panic!("no reading of the model: {l3:?}"));
                let oracle_uj = oracle_nj / 1_000;
                let ratio = read as f64 / oracle_uj as f64;
                assert!(oracle_uj > 100_000, "setup: the stand-in's work read {oracle_uj} µJ");
                assert!((0.8..=1.25).contains(&ratio), "the window read {read} µJ of a model that counted {oracle_uj} µJ");
                assert!(l3.partial_because.iter().any(|w| w.contains("exited")), "{l3:?}");
                assert_eq!(l3.figure_uj, read + l3.machine_uj);
                // CI's macOS energy job greps for this line: the oracle ran.
                eprintln!("l3 model process: window {window} read {read} µJ of a model that counted {oracle_uj} µJ");
            } else {
                assert_eq!((l3.process_cpu_uj, l3.figure_uj), (None, l3.machine_uj), "{l3:?}");
            }
        }
        let _ = std::fs::remove_dir_all(&dir);
    }

    #[test]
    fn shipped_l3_fix_induces_a_skill_that_closes_the_recurrence_without_a_model() {
        let store = std::env::temp_dir().join(format!("joule-fix-skills-{}.json", std::process::id()));
        let _ = std::fs::remove_file(&store);

        // ---- First occurrence: the model (mock) fixes it; skill induced.
        let a = scratch_crate("skill-a");
        std::fs::write(
            a.join("src/main.rs"),
            "fn main() {\n    let pi = 3.14;\n    println!(\"{}\", pi);\n}\n",
        )
        .unwrap();
        std::fs::write(
            a.join("mock-l3.sh"),
            "#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
'```rust' \
'fn main() {' \
'    let pi = std::f64::consts::PI;' \
'    println!(\"{}\", pi);' \
'}' \
'```'\n",
        )
        .unwrap();
        sh(&a, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");
        let mut h = Harness::new(&a).unwrap();
        h.skill_store = store.clone();
        h.l3_cmd = Some("./mock-l3.sh".into());
        let first = h.run_once().unwrap();
        assert!(first.shipped, "gates: {:?}", first.gates);
        let stored = SkillStore::load(&store);
        assert_eq!(stored.skills.len(), 1, "the verified fix must induce");

        // ---- Recurrence, DIFFERENT crate, NO model configured at all: the
        // induced skill closes it deterministically.
        let b = scratch_crate("skill-b");
        std::fs::write(
            b.join("src/main.rs"),
            "fn circumference(r: f64) -> f64 {\n    let pi = 3.14;\n    2.0 * pi * r\n}\nfn main() { println!(\"{}\", circumference(1.0)); }\n",
        )
        .unwrap();
        sh(&b, "git add -A && git -c user.email=t@t -c user.name=t commit -qm pi2");
        let mut h2 = Harness::new(&b).unwrap();
        h2.skill_store = store.clone();
        h2.l3_cmd = None; // no model exists here
        let second = h2.run_once().unwrap();
        assert!(second.shipped, "gates: {:?}", second.gates);
        assert_eq!(second.findings_after, Some(0));
        assert!(!second.receipt.discharge[0].obligation.text.is_empty());
        let src = std::fs::read_to_string(b.join("src/main.rs")).unwrap();
        assert!(src.contains("std::f64::consts::PI"));
        assert!(src.contains("    let pi"), "indentation preserved");
        assert_eq!(SkillStore::load(&store).skills[0].hits, 1);

        let _ = std::fs::remove_file(&store);
        let _ = std::fs::remove_dir_all(&a);
        let _ = std::fs::remove_dir_all(&b);
    }

    #[test]
    fn l3_garbage_is_caught_by_the_gate_and_reverted() {
        // The mock model emits a build-breaking "fix": the gate must catch
        // it, revert it, and put the refusal on the record. This is the
        // weak-model-made-safe property, tested.
        let dir = scratch_crate("l3refuse");
        std::fs::write(
            dir.join("src/main.rs"),
            "fn main() { let pi = 3.14; println!(\"{}\", pi); }\n",
        )
        .unwrap();
        let fixer = dir.join("mock-l3.sh");
        std::fs::write(
            &fixer,
            "#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
'<<<<<<< SEARCH src/main.rs' \
'fn main() { let pi = 3.14; println!(\"{}\", pi); }' \
'=======' \
'fn main() { this is not rust at all }' \
'>>>>>>> REPLACE'\n",
        )
        .unwrap();
        sh(&dir, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");

        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        h.l3_cmd = Some("./mock-l3.sh".into());
        let report = h.run_once().unwrap();

        assert!(!report.shipped, "broken fix must not ship");
        let build_gate = report.gates.iter().find(|g| g.gate == "build").unwrap();
        assert!(!build_gate.passed);
        // Reverted: the original (lint and all) is back.
        let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
        assert!(src.contains("3.14"));

        let _ = std::fs::remove_dir_all(&dir);
    }

    #[test]
    fn failed_gate_reverts_and_never_ships() {
        let dir = scratch_crate("refuse");
        // A test that pins the lint: fixing `return 42;` to `42` breaks it.
        std::fs::write(
            dir.join("src/main.rs"),
            r#"fn answer() -> u64 { return 42; }
fn main() { let x: u64 = answer(); println!("{}", x); }
#[test]
fn pins_source_text() {
    // The needle is assembled at runtime so the assert's own text doesn't
    // satisfy it (include_str! includes this test too).
    let src = include_str!("main.rs");
    let needle = ["ret", "urn 42;"].concat();
    assert!(src.contains(&needle), "fix would break this test");
}
"#,
        )
        .unwrap();
        sh(&dir, "git add -A && git -c user.email=t@t -c user.name=t commit -qm pin");

        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        let report = h.run_once().unwrap();

        assert!(!report.shipped, "the pinned test must block shipping");
        assert!(report.branch.is_none());
        let tests_gate = report.gates.iter().find(|g| g.gate == "tests-vs-baseline").unwrap();
        assert!(!tests_gate.passed);
        // The work tree was reverted — the fix is gone.
        let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
        assert!(src.contains("return 42;"));
        // And the refusal is on the record: an undischarged obligation.
        assert!(report
            .receipt
            .discharge
            .iter()
            .any(|e| matches!(&e.result, DischargeResult::Undischarged { reason } if reason.contains("tests-vs-baseline"))));

        let _ = std::fs::remove_dir_all(&dir);
    }

    /// A `.joule-fix/formal.json` over a netting postcondition (pre=0, post=1,
    /// frame=2): the post is formalized as the SMT goal `net_def`; pre and frame
    /// stay natural language (demoted, never dropped). `net_def` is the `net`
    /// expression — `(- debits credits)` proves, `(+ debits credits)` refutes.
    fn write_formal_spec(dir: &std::path::Path, net_def: &str) {
        use proof_schema::{GoalKind, SpecGrounding};
        let contract = Contract {
            joulecontract: "joulecontract/0.6".into(),
            subject: "scratch netting".into(),
            rigor_target: Rigor::Jr2,
            pre: vec!["debits and credits are integers".into()],
            post: vec!["when debits == credits, the net is zero".into()],
            inv: vec![],
            frame: vec!["the ledger row".into()],
            ceiling: Ceiling {
                enpi_joules: 10.0,
                unit: "joules/settlement".into(),
                enb_ref: ContentAddress::of_bytes(b"enb"),
                derivation: None,
            },
            sector_equivalence: None,
            amends: None,
        };
        let statement = format!(
            "(declare-const debits Int)(declare-const credits Int)(declare-const net Int)\
             (assert (= net {net_def}))(assert (= debits credits))(assert (not (= net 0)))"
        );
        let f = Formalization {
            obligation: 1,
            statement,
            kind: GoalKind::Decidable,
            grounding: SpecGrounding::CrossChecked,
        };
        let spec = serde_json::json!({ "contract": contract, "formalizations": [f] });
        std::fs::create_dir_all(dir.join(".joule-fix")).unwrap();
        std::fs::write(dir.join(".joule-fix/formal.json"), spec.to_string()).unwrap();
    }

    /// Whether the formal-tier tests run against a real `z3`.
    ///
    /// They follow this repo's z3 convention (proof-solvers, joulecontract-
    /// proof, and the standards-build workflow's "Install z3" step): a suite
    /// passes with or without a solver, and asserts something either way.
    /// With `z3` the SMT rung decides the obligation and its verdict is
    /// asserted. Without it the obligation is Unproved, never a fabricated
    /// proof, and the formal gate fails closed, so the fix is reverted — that
    /// is asserted instead. Neither branch returns without asserting, and each
    /// logs which one ran.
    ///
    /// Where a solver is supposed to be installed (a CI job that installs z3,
    /// a dev box), set `JOULE_FIX_EXPECT_Z3=1`: a missing `z3` then FAILS
    /// these tests rather than quietly taking the solverless branch.
    fn z3_for_formal_test(test: &str) -> bool {
        let present = proof_solvers::z3_available();
        let expected = std::env::var("JOULE_FIX_EXPECT_Z3").as_deref() == Ok("1");
        assert!(present || !expected, "{test}: JOULE_FIX_EXPECT_Z3=1, but there is no working `z3` on PATH");
        eprintln!(
            "{test}: z3 {}",
            if present { "present, asserting its verdict" } else { "absent, asserting the formal gate fails closed" }
        );
        present
    }

    /// Without a solver nothing decides the obligation: it is Unproved (not
    /// proved, and not refuted either: there is no counter-model without a
    /// solver), the formal gate fails and says why, and the fix is reverted
    /// although every other gate passed.
    fn assert_the_formal_gate_failed_closed(dir: &std::path::Path, report: &RunReport) {
        let formal = report.formal.as_ref().expect("formal gate ran");
        assert_eq!((formal.proved, formal.refuted, formal.unproved), (0, 0, 1), "{:?}", formal.entries);
        assert!(!formal.all_proved);
        let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
        assert!(!g.passed);
        assert!(g.detail.contains("no z3 on PATH") && !g.detail.contains("real z3"), "{}", g.detail);
        assert!(
            report.gates.iter().filter(|g| g.gate != "formal-proof").all(|g| g.passed),
            "only the undecided proof blocks this fix: {:?}",
            report.gates
        );
        assert!(!report.shipped, "an undecided formal obligation must block shipping");
        let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
        assert!(src.contains("return 42;"), "the operational fix was reverted");
        assert!(dir.join(".joule-fix/formal-discharge.json").exists(), "the discharge evidence is written either way");
    }

    #[test]
    fn a_proven_formal_obligation_lets_the_fix_ship() {
        let z3 = z3_for_formal_test("a_proven_formal_obligation_lets_the_fix_ship");
        let dir = scratch_crate("formal-ok");
        write_formal_spec(&dir, "(- debits credits)"); // the correct postcondition
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        let report = h.run_once().unwrap();

        if z3 {
            let formal = report.formal.as_ref().expect("formal gate ran");
            assert!(formal.all_proved, "entries: {:?}", formal.entries);
            assert_eq!((formal.proved, formal.refuted, formal.unproved), (1, 0, 0));
            assert!(formal.proof_uj > 0, "the proof attempt was accounted joules");
            let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
            assert!(g.passed);
            assert!(report.shipped, "all gates incl. formal green: {:?}", report.gates);
            // the discharge evidence was written for an auditor
            assert!(dir.join(".joule-fix/formal-discharge.json").exists());
        } else {
            assert_the_formal_gate_failed_closed(&dir, &report);
        }

        let _ = std::fs::remove_dir_all(&dir);
    }

    #[test]
    fn a_refuted_formal_obligation_reverts_the_fix() {
        let z3 = z3_for_formal_test("a_refuted_formal_obligation_reverts_the_fix");
        let dir = scratch_crate("formal-refute");
        write_formal_spec(&dir, "(+ debits credits)"); // the BUG: z3 finds a counter-model
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        let report = h.run_once().unwrap();

        if z3 {
            let formal = report.formal.as_ref().expect("formal gate ran");
            assert_eq!(formal.refuted, 1, "z3 refuted the false postcondition");
            assert!(!formal.all_proved);
            // the witness rode through from the cascade
            assert!(formal.entries.iter().any(|e| e.verdict == "refuted"));
            let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
            assert!(!g.passed);
            // a refuted formal obligation reverts the fix exactly like a failed test
            assert!(!report.shipped, "a refuted proof must block shipping");
            let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
            assert!(src.contains("return 42;"), "the operational fix was reverted");
        } else {
            assert_the_formal_gate_failed_closed(&dir, &report);
        }

        let _ = std::fs::remove_dir_all(&dir);
    }

    #[test]
    fn the_shipped_formal_template_parses_and_validates() {
        // Guards `formal.example.json` against schema drift: the template we
        // tell users to copy must always deserialize and index validly.
        let path = concat!(env!("CARGO_MANIFEST_DIR"), "/formal.example.json");
        let text = std::fs::read_to_string(path).expect("template present");
        let spec: FormalSpec = serde_json::from_str(&text).expect("template parses");
        assert_eq!(spec.formalizations.len(), 1);
        for f in &spec.formalizations {
            assert!(
                f.obligation < spec.contract.obligations().len(),
                "template formalization indexes a real obligation"
            );
        }
    }
}