3589be01f3
The formal tier's input is hand-authored, and its serde forms are easy to guess
wrong (PascalCase enums, a stringified ContentAddress, JR-N rigor). Removes that
friction without touching the upstream schema serde:
- formal.example.json — a working, copy-pasteable template (the netting
postcondition), with the gotchas spelled out in an ignored _comment key.
- the FormalSpec doc and the parse-error message now name the exact forms and
point at the template.
- a test deserializes the shipped template and checks its indices, so it can
never drift from the schema.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
1537 lines
65 KiB
Rust
1537 lines
65 KiB
Rust
//! 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"
|
|
);
|
|
}
|
|
}
|
|
}
|