//! 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 hardware-measured energy. 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 is measured, not estimated**, whenever the host has
//!    a hardware counter ([`sandbox_meter::PowerMeter`]); the meter
//!    attestation inside the JouleContract receipt is a sealed sandbox JCR-1
//!    envelope — one standard's receipt is the other's evidence.
//! 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, PowerMeter};
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 cargo
/// subprocesses (the real compute). The harness's `run()` helper feeds this
/// for every `cargo` invocation; git and rustfmt are negligible overhead and
/// run unmetered.
struct MeterAcc {
    meter: PowerMeter,
    /// Σ machine-wide SoC-CPU energy over the metered windows (the upper bound).
    soc_uj: u64,
    /// Σ energy attributed to this run's process trees (ModelBased apportion).
    attr_uj: u64,
    /// True once at least one window rested on real per-process accounting.
    attributed: bool,
}

#[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),
}

/// 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>,
    /// Measured joules for this obligation's proof attempts.
    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 measured joules across all proof attempts (`ModelBased`, 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 attributed to this run's process trees (`ModelBased`
    /// apportionment of a real SoC measurement), microjoules — the receipt's
    /// figure, and the honest per-workload cost.
    pub attributed_uj: u64,
    /// Machine-wide SoC-CPU energy over the metered windows, microjoules —
    /// the upper bound, for context.
    pub soc_cpu_uj: u64,
    /// True when the figure rests on real per-process accounting.
    pub attributed: bool,
    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
    /// energy ATTRIBUTED to this run's process trees, not the machine-wide
    /// total. `soc_cpu_uj` carries the machine-wide upper bound.
    pub fn total_uj(&self) -> u64 {
        self.attributed_uj
    }

    /// The headline metric nobody else publishes: microjoules per verified,
    /// shipped fix. `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.
    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>,
}

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));
        }
        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(),
                soc_uj: 0,
                attr_uj: 0,
                attributed: false,
            }),
        })
    }

    /// 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 mut acc = self.meter.borrow_mut();
            let MeterAcc { meter, soc_uj, attr_uj, attributed } = &mut *acc;
            let (ok, text, a) = run_attributed(meter, program, args, &self.workspace)
                .map_err(|e| HarnessError::Spawn(format!("{program}: {e}")))?;
            *soc_uj = soc_uj.saturating_add(a.soc_cpu_uj);
            *attr_uj = attr_uj.saturating_add(a.attributed_uj);
            *attributed |= a.attributed;
            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))
    }

    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 attribution accumulator; cargo calls feed it.
        {
            let mut acc = self.meter.borrow_mut();
            acc.soc_uj = 0;
            acc.attr_uj = 0;
        }
        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 {
            gates.push(GateOutcome {
                gate: "formal-proof".into(),
                passed: f.all_proved,
                detail: format!(
                    "{} proved, {} refuted, {} unproved ({:.3} J, real z3)",
                    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())]);
            let _ = self.run("git", &["checkout", "-b", &name]);
            // -u: stage only tracked modifications — the harness owns the
            // tracked diff; untracked artifacts (target/) are not its fix.
            let _ = self.run("git", &["add", "-u", "--", "."]);
            let _ = self.run(
                "git",
                &["commit", "-m", &format!("joule-fix: {} lint findings remediated, all gates green", findings_before.saturating_sub(findings_after))],
            );
            // 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: read the per-process attribution accumulated across the
        // run's cargo subprocesses. The receipt carries the ATTRIBUTED figure
        // (ModelBased — an apportionment of a real SoC measurement), not the
        // machine-wide total; the SoC total rides along as honest context.
        let (soc_cpu_uj, attributed_uj, attributed) = {
            let acc = self.meter.borrow();
            (acc.soc_uj, acc.attr_uj, acc.attributed && acc.meter.is_hardware())
        };
        let wall = wall_start.elapsed();
        let meter_source = if attributed {
            "attributed(ModelBased over IOReport HwShunt)".to_string()
        } else {
            "estimator".to_string()
        };

        // The sandbox meter receipt records the attributed figure as a
        // ModelBased CPU reading; the JouleContract receipt anchors to it.
        let device = sandbox_meter::DeviceEnergy {
            class: sandbox_schema::DeviceClass::Cpu,
            measured_uj: None,
            estimated_uj: attributed_uj,
            provenance: sandbox_meter::Provenance::ModelBased,
        };
        let meter_receipt = sandbox_meter::Receipt::build(
            sandbox_schema::ContentId::of_bytes(prior_rev.as_bytes()),
            sandbox_schema::Tier::S0,
            vec![device],
            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,
            attributed_uj,
            attributed,
            &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,
            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.
    fn l3_pass(&self) -> Result<bool, HarnessError> {
        use std::io::Write;
        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 mut child = Command::new("sh")
            .args(["-c", cmd])
            .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}")))?;
        if let Some(stdin) = child.stdin.as_mut() {
            let _ = stdin.write_all(prompt.as_bytes());
        }
        let out = child
            .wait_with_output()
            .map_err(|e| HarnessError::Spawn(format!("L3 cmd: {e}")))?;
        let reply = String::from_utf8_lossy(&out.stdout).into_owned();

        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)
    }

    /// 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,
        attributed_uj: u64,
        attributed: bool,
        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();

        // The figure is an apportionment of a real SoC measurement: ModelBased,
        // never Metered (a process is not a shunt). A ModelBased receipt is
        // anchored to the sealed sandbox meter receipt that carries the
        // measurement the apportionment rests on; without hardware it is
        // honestly Unaccounted.
        let provenance = if attributed {
            EnergyClass::ModelBased
        } else {
            EnergyClass::Unaccounted
        };
        let energy_anchor =
            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: attributed_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();
        sh(&dir, "git init -q && git add -A && git -c user.email=t@t -c user.name=t commit -qm init");
        dir
    }

    #[test]
    fn verified_fix_end_to_end_ships_with_receipt() {
        let dir = scratch_crate("ship");
        let mut h = Harness::new(&dir).unwrap();
        h.skill_store = dir.join("skills.json");
        let report = h.run_once().unwrap();

        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));
        assert!(report.branch.is_some());
        assert!(report.total_uj() > 0);
        assert!(report.uj_per_verified_fix().is_some());

        // 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);
    }

    #[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"));

        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();
    }

    #[test]
    fn a_proven_formal_obligation_lets_the_fix_ship() {
        if !proof_solvers::z3_available() {
            return; // no solver: the formal gate can't run — covered below
        }
        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();

        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, "real z3 burned measured 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());

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

    #[test]
    fn a_refuted_formal_obligation_reverts_the_fix() {
        if !proof_solvers::z3_available() {
            return;
        }
        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();

        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");

        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"
            );
        }
    }
}