ccb382ba08
joule-code-remediate's meter source said "attributed(ModelBased over IOReport HwShunt)" for every attributed run, whatever counter its windows were read by. Today only the Apple Silicon attribution path can attribute, so the label happened to fit, but it was a constant, not a record: an attribution read by RAPL, or by several probes, would still have claimed IOReport. sandbox-meter's Attribution now carries the window's own Measurement::source (the probe that read it, "composite" for several, "estimator" for an estimate), so a caller names the reading by what read it. joule-code-remediate collects the sources of its attributed windows and names them; the meter source string moves into EnergyTally::source, where a test pins that an attribution read by "rapl-powercap" says so and never says IOReport. Co-Authored-By: Claude Opus 5.5 <[email protected]>
2545 lines
117 KiB
Rust
2545 lines
117 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 its energy, graded by how that energy
|
||
//! was obtained. Three consequences, by construction:
|
||
//!
|
||
//! 1. **A fix that fails its gate is reverted and never ships** — but the
|
||
//! refusal still produces a receipt: an undischarged obligation on the
|
||
//! record beats a silently dropped fix.
|
||
//! 2. **The energy figure rests on a hardware reading** whenever the host
|
||
//! exposes a live CPU energy counter ([`sandbox_meter::PowerMeter`]), and
|
||
//! is then anchored to a sealed sandbox JCR-1 meter envelope — one
|
||
//! standard's receipt is the other's evidence. Where it does not, the
|
||
//! figure is an estimate and is sealed as one (JCR-1 `Estimator`,
|
||
//! JouleContract `Unaccounted`), never as a reading.
|
||
//! 3. **The receipt grades honestly**: receipt-local validation, JR-2 at
|
||
//! most, generator and verifier self-declared and labeled as such. Higher
|
||
//! rigor is a deployment's verifier-of-record work, exactly per the
|
||
//! JouleContract two-stage rule.
|
||
//!
|
||
//! v0 remediates at the **L1 lawful tier only** — `cargo clippy --fix` and
|
||
//! `rustfmt`, deterministic codemods, zero inference — which is not a
|
||
//! limitation but the doctrine: the cheapest sufficient tier closes the
|
||
//! request. Model tiers (L3 local, L4 federation) hang off the same gate.
|
||
|
||
use joule_code_cargo::{Anchor, CodingOp, Edit};
|
||
use joule_code_schema::{ContentId, Tier};
|
||
use joulecontract_receipt::{
|
||
validate, DischargeEntry, DischargeResult, Engagement, FrameMode, Generator, MeterBinding,
|
||
Qualification, Receipt, TierClass, TrustRoot,
|
||
};
|
||
use joulecontract_schema::{
|
||
Ceiling, ContentAddress, Contract, EnergyClass, GovernanceClass, ObligationKind, Profile,
|
||
Rigor,
|
||
};
|
||
use sandbox_meter::{run_attributed, Attribution, PowerMeter, TreeError, TreeMeter, TreeReading};
|
||
use sandbox_schema::DeviceClass;
|
||
use serde::{Deserialize, Serialize};
|
||
// The formally-verified fix tier. `DischargeStatus`/`Formalization`/
|
||
// `ContractDischarge` come from the proof bridge; the bridge's own
|
||
// `DischargeEntry` is NOT imported — that name already belongs to
|
||
// `joulecontract_receipt` above (the operational receipt's entry).
|
||
use joulecontract_proof::{discharge as proof_discharge, DischargeStatus, Formalization};
|
||
use proof_cascade::{ProofCache, Router};
|
||
use proof_solvers::{Propositional, Z3Smt};
|
||
use std::cell::RefCell;
|
||
use std::collections::BTreeSet;
|
||
use std::path::PathBuf;
|
||
use std::process::Command;
|
||
use std::time::{Duration, Instant};
|
||
|
||
/// Accumulates per-process energy attribution across a run's subprocesses
|
||
/// (the real compute): every `cargo` invocation, which the harness's `run()`
|
||
/// helper feeds, and the L3 model's command, which [`Harness::run_l3`] feeds.
|
||
/// git and rustfmt are negligible overhead and run unmetered.
|
||
struct MeterAcc {
|
||
/// `PowerMeter::detect()`, machine-wide, and deliberately not
|
||
/// `detect_in_process()`: the metered work is `cargo` and the `rustc`
|
||
/// processes it runs, and the L3 model's process, and this process's own
|
||
/// energy counter covers no child process. `run_attributed`'s per-child
|
||
/// reading does not reach cargo's work either: it covers a single-process
|
||
/// child, and `cargo` runs its work in descendants.
|
||
meter: PowerMeter,
|
||
/// This run's metered windows, reset at the start of each run.
|
||
tally: EnergyTally,
|
||
/// This run's L3 window, when the model was consulted: how it was metered
|
||
/// and what it added to `tally`. Reset with it.
|
||
l3: Option<L3Energy>,
|
||
}
|
||
|
||
/// The energy of one run's metered windows — its cargo windows and its L3
|
||
/// window — and the figure and grades the receipts carry for it.
|
||
///
|
||
/// A cargo window is attributed when a hardware CPU reading that advanced
|
||
/// was apportioned to the child's process tree (`ModelBased`). Otherwise its
|
||
/// figure is not a reading of this workload. It is the meter's wall × TDP
|
||
/// estimate where the host exposes no live CPU counter (every macOS 27.0.1
|
||
/// host checked), or where the counter held; or it is a machine-wide figure
|
||
/// the meter could not apportion. The L3 window is never attributed: its
|
||
/// model's own process tree is never read whole ([`grade_l3`]). The run is
|
||
/// `ModelBased` only when every window was attributed, because a sum is only
|
||
/// as good as its weakest part.
|
||
#[derive(Clone, Debug, Default, PartialEq, Eq)]
|
||
struct EnergyTally {
|
||
/// Σ each window's figure as an estimate of its work: over a cargo
|
||
/// window the machine-wide SoC-CPU figure (an upper bound: every process
|
||
/// on the host), over the L3 window [`L3Energy::figure_uj`].
|
||
soc_uj: u64,
|
||
/// The part of `soc_uj` in device classes other than the CPU, per class:
|
||
/// what the machine-wide meter read of them over an L3 window (a GPU
|
||
/// rail, NVML's GPUs). A cargo window's figure is the CPU's alone.
|
||
non_cpu_uj: std::collections::BTreeMap<DeviceClass, u64>,
|
||
/// Σ figure apportioned or read for this run's process trees.
|
||
attr_uj: u64,
|
||
windows: u64,
|
||
attributed_windows: u64,
|
||
/// The probes whose readings the attributed windows apportioned, each
|
||
/// window's own (`Attribution::source`): what the meter source names.
|
||
read_by: BTreeSet<&'static str>,
|
||
}
|
||
|
||
impl EnergyTally {
|
||
fn add(&mut self, a: &Attribution) {
|
||
self.add_window(a.soc_cpu_uj, a.attributed_uj, a.attributed);
|
||
if a.attributed {
|
||
self.read_by.insert(a.source);
|
||
}
|
||
}
|
||
|
||
/// How the figure was obtained, for [`RunReport::meter_source`]: an
|
||
/// attribution names the probes its windows' readings came from, as the
|
||
/// meter reported them; an estimate names the meter's hardware sources,
|
||
/// `meter_sources` ([`PowerMeter::sources`]), or says it has none.
|
||
fn source(&self, meter_sources: &[&str]) -> String {
|
||
if self.attributed() {
|
||
let read_by: Vec<&str> = self.read_by.iter().copied().collect();
|
||
format!("attributed(ModelBased over {} HwShunt)", read_by.join("+"))
|
||
} else if meter_sources.is_empty() {
|
||
"estimated(Unaccounted): wall-clock × TDP, no live energy counter on this host".to_string()
|
||
} else {
|
||
format!(
|
||
"estimated(Unaccounted): not every window attributed; machine-wide figure over the \
|
||
metered windows ({})",
|
||
meter_sources.join("+")
|
||
)
|
||
}
|
||
}
|
||
|
||
/// The L3 window: its figure, an estimate, never attributed, with the
|
||
/// machine-wide meter's figure for each class other than the CPU kept
|
||
/// apart, so the sealed record names the class it was read on.
|
||
fn add_l3(&mut self, l3: &L3Energy) {
|
||
self.add_window(l3.figure_uj, l3.attributed_uj(), false);
|
||
for &(class, uj) in &l3.machine_by_class {
|
||
if class != DeviceClass::Cpu {
|
||
let sum = self.non_cpu_uj.entry(class).or_default();
|
||
*sum = sum.saturating_add(uj);
|
||
}
|
||
}
|
||
}
|
||
|
||
/// One window: its figure as an estimate (`estimate_uj`), its figure as
|
||
/// a reading or apportionment of its own process tree (`attributed_uj`),
|
||
/// and whether that one is the window's honest figure (`attributed`).
|
||
fn add_window(&mut self, estimate_uj: u64, attributed_uj: u64, attributed: bool) {
|
||
self.soc_uj = self.soc_uj.saturating_add(estimate_uj);
|
||
self.attr_uj = self.attr_uj.saturating_add(attributed_uj);
|
||
self.windows += 1;
|
||
if attributed {
|
||
self.attributed_windows += 1;
|
||
}
|
||
}
|
||
|
||
/// True when every metered window rested on real per-process accounting
|
||
/// of a hardware CPU reading.
|
||
fn attributed(&self) -> bool {
|
||
self.windows > 0 && self.attributed_windows == self.windows
|
||
}
|
||
|
||
/// The figure the receipts carry. When attributed, it is the apportioned
|
||
/// reading. Otherwise it is the unapportioned total over the windows, as
|
||
/// an estimate. An apportioned estimate is no better than an estimate,
|
||
/// and the apportioning share is 0 whenever the machine's tick counters
|
||
/// (which update in bursts up to ~1 s apart) missed a window, which would
|
||
/// put 0 J on the receipt for work that ran.
|
||
fn figure_uj(&self) -> u64 {
|
||
if self.attributed() {
|
||
self.attr_uj
|
||
} else {
|
||
self.soc_uj
|
||
}
|
||
}
|
||
|
||
/// The sandbox JCR-1 meter records for the figure, one per device class,
|
||
/// summing to it. An attribution is one `ModelBased` CPU record (every
|
||
/// window attributed, so no L3 window and nothing off the CPU). An
|
||
/// estimate is an `Estimator` record with no measured figure for the CPU
|
||
/// and one for each other class the L3 window's machine-wide meter read:
|
||
/// a GPU's energy is never sealed as the CPU's.
|
||
fn meter_records(&self) -> Vec<sandbox_meter::DeviceEnergy> {
|
||
let record = |class, estimated_uj, provenance| sandbox_meter::DeviceEnergy {
|
||
class,
|
||
measured_uj: None,
|
||
estimated_uj,
|
||
provenance,
|
||
};
|
||
if self.attributed() {
|
||
return vec![record(DeviceClass::Cpu, self.attr_uj, sandbox_meter::Provenance::ModelBased)];
|
||
}
|
||
let non_cpu: u64 = self.non_cpu_uj.values().fold(0, |a, &b| a.saturating_add(b));
|
||
let mut records =
|
||
vec![record(DeviceClass::Cpu, self.soc_uj.saturating_sub(non_cpu), sandbox_meter::Provenance::Estimator)];
|
||
records.extend(
|
||
self.non_cpu_uj.iter().map(|(&class, &uj)| record(class, uj, sandbox_meter::Provenance::Estimator)),
|
||
);
|
||
records
|
||
}
|
||
|
||
/// The JouleContract energy class for the figure. It is `ModelBased`,
|
||
/// anchored to the sealed meter receipt, for an attribution. Otherwise it
|
||
/// is `Unaccounted`, JouleContract's grade for energy estimated where the
|
||
/// substrate exposes no reading.
|
||
fn energy_class(&self) -> EnergyClass {
|
||
if self.attributed() {
|
||
EnergyClass::ModelBased
|
||
} else {
|
||
EnergyClass::Unaccounted
|
||
}
|
||
}
|
||
}
|
||
|
||
/// The L3 model's window: how its energy was read, and what it adds to the
|
||
/// run's figure ([`RunReport::total_uj`], and so
|
||
/// [`RunReport::uj_per_verified_fix`] and both receipts).
|
||
///
|
||
/// Two meters span the window, from the moment the command is let go (see
|
||
/// [`Harness::l3_cmd`]) to the moment it has exited and been reaped: the
|
||
/// machine-wide meter, as over a cargo window, and — where this host counts
|
||
/// each process's CPU energy (macOS, its per-process counter live) — a
|
||
/// [`TreeMeter`] rooted at the command's own process, which reads the CPU
|
||
/// energy of that process and its descendants and lists every way that
|
||
/// figure was seen to fall short of their whole energy. [`grade_l3`] turns
|
||
/// the two into the window's figure, in one place.
|
||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||
pub struct L3Energy {
|
||
/// The machine-wide meter's figure over the window, every device class
|
||
/// it reads, µJ: a hardware reading where the host has a live
|
||
/// machine-wide counter (RAPL, NVML on Linux), its wall-clock × TDP
|
||
/// estimate where it has none (every macOS 27.0.1 host checked). Like a
|
||
/// cargo window's, it is the whole host's, other processes included.
|
||
pub machine_uj: u64,
|
||
/// The same figure per device class, as the meter read them (the CPU,
|
||
/// and a GPU where it reads one); `machine_uj` is their sum. The run's
|
||
/// sealed records keep the classes apart.
|
||
pub machine_by_class: Vec<(DeviceClass, u64)>,
|
||
/// The CPU energy of the model's own process tree over the window, µJ
|
||
/// (the [`TreeReading`]'s nanojoules rounded up), where the host counts
|
||
/// it. `None` off macOS, where the per-process counter is not live, and
|
||
/// when the span gave no reading (`partial_because` says why). It covers
|
||
/// the model's CPU only: not its GPU or Neural Engine work, not work it
|
||
/// hands to a process outside its tree, and not the last time on a core
|
||
/// of a thread that exits (the kernel never folds it), which a model that
|
||
/// exits in the window always has.
|
||
pub process_cpu_uj: Option<u64>,
|
||
/// Why `process_cpu_uj` is not the model's whole energy over the window:
|
||
/// each gap the tree meter saw, as it words it — a model that exits in
|
||
/// its window always has one, so its reading is never whole — or, where
|
||
/// it saw none, [`NOT_READ_AT_EXIT`]; or why there is no reading at all.
|
||
/// Never empty for a reading.
|
||
pub partial_because: Vec<String>,
|
||
/// Whether the command ran as the shell's `exec` — a plain argv — so the
|
||
/// model's process IS the process the tree meter is rooted at, and its
|
||
/// own count is read. A command that is not (a pipeline, a list, quoting,
|
||
/// a redirect) runs as the shell's script: what the shell forks and
|
||
/// reaps is a gap, its energy in no counter.
|
||
pub direct_child: bool,
|
||
/// What the window adds to the run's figure (see [`grade_l3`]), µJ: an
|
||
/// estimate, never attributed.
|
||
pub figure_uj: u64,
|
||
}
|
||
|
||
/// Why a reading of the L3 command's process tree is partial although the
|
||
/// tree meter saw no gap in it: the model had not exited when it was read
|
||
/// (the wait for its exit failed), so the reading may stop short of its
|
||
/// work. A model read at its exit always carries the exit's own gap instead.
|
||
pub const NOT_READ_AT_EXIT: &str =
|
||
"the model had not exited when its process tree was read, so the reading may stop short of its work";
|
||
|
||
impl L3Energy {
|
||
/// What the window's process reading added to the run's tree figures:
|
||
/// the reading itself, a floor, else nothing.
|
||
fn attributed_uj(&self) -> u64 {
|
||
self.process_cpu_uj.unwrap_or(0)
|
||
}
|
||
|
||
/// The window in one line, for [`RunReport::meter_source`].
|
||
fn describe(&self) -> String {
|
||
let j = |uj: u64| uj as f64 / 1e6;
|
||
match self.process_cpu_uj {
|
||
Some(read) => format!(
|
||
"L3 model's own process tree read {:.3} J of CPU, partial ({}), so the window is an estimate: that \
|
||
reading plus the machine-wide {:.3} J, {:.3} J",
|
||
j(read),
|
||
self.partial_because.join("; "),
|
||
j(self.machine_uj),
|
||
j(self.figure_uj)
|
||
),
|
||
None => format!(
|
||
"L3 model metered machine-wide only, {:.3} J ({})",
|
||
j(self.machine_uj),
|
||
if self.partial_because.is_empty() {
|
||
"no per-process counter on this host".to_string()
|
||
} else {
|
||
self.partial_because.join("; ")
|
||
}
|
||
),
|
||
}
|
||
}
|
||
}
|
||
|
||
/// The L3 window's figure: the one place it is decided. It is always an
|
||
/// estimate of the window, never attributed.
|
||
///
|
||
/// - **A reading** — never whole. The model is read at its exit, and an
|
||
/// exiting process's record lacks its last time on a core (the kernel
|
||
/// never folds it), so the reading is a lower bound on the model's own CPU
|
||
/// energy; its GPU time is unknown, and work it hands outside its tree is
|
||
/// in no reading of it. The figure is the reading plus the machine-wide
|
||
/// meter's figure over the same window — never less than was read, and
|
||
/// nothing the model drew outside its CPU left out — the rule mesh's
|
||
/// in-process meter bills a partial span by. The machine-wide figure
|
||
/// covers the model's CPU too, so this errs high, by at most the reading.
|
||
/// - **No reading** — no per-process counter (Linux, a counter that is not
|
||
/// live) or the span's [`TreeError`]: the machine-wide figure, exactly as
|
||
/// a cargo window's (it is the whole host's).
|
||
fn grade_l3(
|
||
reading: Option<&Result<TreeReading, TreeError>>,
|
||
machine_by_class: Vec<(DeviceClass, u64)>,
|
||
direct_child: bool,
|
||
) -> L3Energy {
|
||
let machine_uj = machine_by_class.iter().fold(0u64, |a, &(_, uj)| a.saturating_add(uj));
|
||
match reading {
|
||
Some(Ok(r)) => {
|
||
let read = r.cpu_nj.div_ceil(1_000);
|
||
let mut because: Vec<String> = r.gaps.iter().map(ToString::to_string).collect();
|
||
if because.is_empty() {
|
||
because.push(NOT_READ_AT_EXIT.to_string());
|
||
}
|
||
L3Energy {
|
||
machine_uj,
|
||
machine_by_class,
|
||
process_cpu_uj: Some(read),
|
||
partial_because: because,
|
||
direct_child,
|
||
figure_uj: read.saturating_add(machine_uj),
|
||
}
|
||
}
|
||
Some(Err(e)) => L3Energy {
|
||
machine_uj,
|
||
machine_by_class,
|
||
process_cpu_uj: None,
|
||
partial_because: vec![format!("no reading of the model's process tree: {e}")],
|
||
direct_child,
|
||
figure_uj: machine_uj,
|
||
},
|
||
None => L3Energy {
|
||
machine_uj,
|
||
machine_by_class,
|
||
process_cpu_uj: None,
|
||
partial_because: Vec::new(),
|
||
direct_child,
|
||
figure_uj: machine_uj,
|
||
},
|
||
}
|
||
}
|
||
|
||
/// The shell script an L3 command runs as, and whether it makes the model
|
||
/// the direct child.
|
||
///
|
||
/// The script first waits on a gate — one line on its stdin, which
|
||
/// [`Harness::run_l3`] writes once the tree meter has read the waiting
|
||
/// shell — so the window opens before the model starts and the shell's own
|
||
/// start-up stays outside it. Then, for a plain argv (letters, digits,
|
||
/// spaces and `/._-:,+@` only: no quoting, expansion, assignment, redirect
|
||
/// or list), the shell `exec`s it, so the model is the same process the
|
||
/// meter is rooted at. Anything else runs as the rest of the script, as
|
||
/// `sh -c` would have run it: what it forks and reaps is in no counter.
|
||
fn l3_script(cmd: &str) -> (String, bool) {
|
||
let cmd = cmd.trim();
|
||
let plain = !cmd.is_empty() && cmd.chars().all(|c| c.is_ascii_alphanumeric() || " /._-:,+@".contains(c));
|
||
let body = if plain { format!("exec {cmd}") } else { cmd.to_string() };
|
||
(format!("IFS= read -r joule_fix_gate || exit 1\n{body}\n"), plain)
|
||
}
|
||
|
||
/// Wait for child `pid` to exit WITHOUT reaping it (`waitid` with
|
||
/// `WNOWAIT`), so its count stays readable for the tree meter's stop walk.
|
||
/// The caller reaps it afterwards. `false` if the wait failed.
|
||
#[cfg(target_os = "macos")]
|
||
fn wait_exited_unreaped(pid: u32) -> bool {
|
||
loop {
|
||
// SAFETY: an all-zero `siginfo_t` is a valid out-parameter.
|
||
let mut info: libc::siginfo_t = unsafe { std::mem::zeroed() };
|
||
// SAFETY: `info` is writable for the call; `pid` is this process's child.
|
||
let rc = unsafe { libc::waitid(libc::P_PID, pid as libc::id_t, &mut info, libc::WEXITED | libc::WNOWAIT) };
|
||
if rc == 0 {
|
||
return true;
|
||
}
|
||
if std::io::Error::last_os_error().raw_os_error() != Some(libc::EINTR) {
|
||
return false;
|
||
}
|
||
}
|
||
}
|
||
|
||
/// No tree meter exists off macOS, so there is nothing to read before the reap.
|
||
#[cfg(not(target_os = "macos"))]
|
||
fn wait_exited_unreaped(_pid: u32) -> bool {
|
||
false
|
||
}
|
||
|
||
#[derive(Debug, thiserror::Error)]
|
||
pub enum HarnessError {
|
||
#[error("not a git work tree: {0} (the harness needs revert-ability before it will touch anything)")]
|
||
NotGit(PathBuf),
|
||
#[error("workspace has uncommitted changes; commit or stash first (the harness must own the diff)")]
|
||
Dirty,
|
||
#[error("command failed to launch: {0}")]
|
||
Spawn(String),
|
||
#[error("contract error: {0}")]
|
||
Contract(String),
|
||
/// Every gate passed but the fix could not be committed, so nothing
|
||
/// shipped. The message says where the verified change was left.
|
||
#[error("the fix passed every gate but could not be committed: {0}")]
|
||
Ship(String),
|
||
}
|
||
|
||
/// One pipeline stage's outcome — the discharge evidence for one obligation.
|
||
#[derive(Clone, Debug, Serialize)]
|
||
pub struct GateOutcome {
|
||
pub gate: String,
|
||
pub passed: bool,
|
||
pub detail: String,
|
||
}
|
||
|
||
/// The formal-tier input, read from `<workspace>/.joule-fix/formal.json` when
|
||
/// present: a domain [`Contract`] and the [`Formalization`]s that encode the
|
||
/// obligations the fix must honor. Absent file ⇒ no formal gate (the harness
|
||
/// runs exactly as before). The formalizations are an explicit, grounded input
|
||
/// — the harness never invents one (autoformalization is an upstream concern).
|
||
///
|
||
/// `formal.example.json` (next to this crate's `Cargo.toml`) is a working,
|
||
/// copy-pasteable template. The serde forms that trip up a hand-written file:
|
||
/// `rigor_target` is `"JR-1".."JR-4"`; `ceiling.enb_ref` is a **string**
|
||
/// `"sha2-256:<64-hex>"` (not an object); `kind` is one of
|
||
/// `Trivial|Arithmetic|Decidable|General|Hard`; `grounding` is one of
|
||
/// `Ungrounded|HumanReviewed|CrossChecked` — all PascalCase. `obligation`
|
||
/// indexes the contract's obligations in declaration order (pre, then post,
|
||
/// then inv, then frame).
|
||
#[derive(Debug, Deserialize)]
|
||
struct FormalSpec {
|
||
contract: Contract,
|
||
formalizations: Vec<Formalization>,
|
||
}
|
||
|
||
/// One formalized obligation's proof outcome, for the report and evidence file.
|
||
#[derive(Clone, Debug, Serialize)]
|
||
pub struct FormalEntry {
|
||
/// The obligation text as the domain contract declares it.
|
||
pub obligation: String,
|
||
/// `proved` | `refuted` | `unproved`.
|
||
pub verdict: String,
|
||
/// The tier that closed it (when proved).
|
||
pub closed_by: Option<String>,
|
||
/// The counter-model witness (when refuted by a decision procedure).
|
||
pub counter_model: Option<String>,
|
||
/// Joules for this obligation's proof attempts, as the proof cascade
|
||
/// accounted them (`Estimator`, in-process: wall time × proof-solvers'
|
||
/// default power, which no host calibrated).
|
||
pub uj: u64,
|
||
}
|
||
|
||
/// The formal-tier verdict for a run: did every supplied formalization prove?
|
||
#[derive(Clone, Debug, Serialize)]
|
||
pub struct FormalOutcome {
|
||
pub proved: usize,
|
||
pub refuted: usize,
|
||
pub unproved: usize,
|
||
/// Total joules across all proof attempts (`Estimator`, in-process —
|
||
/// distinct from the cargo-attributed gate energy).
|
||
pub proof_uj: u64,
|
||
/// True iff at least one formalization was supplied and **every** one
|
||
/// proved. This is the gate: any refutation or unproven goal fails it, and
|
||
/// the fix reverts like any other failed gate.
|
||
pub all_proved: bool,
|
||
pub entries: Vec<FormalEntry>,
|
||
}
|
||
|
||
/// The result of one harness run.
|
||
#[derive(Debug)]
|
||
pub struct RunReport {
|
||
/// Findings before the fix (clippy warning count).
|
||
pub findings_before: usize,
|
||
/// Findings after (counted only when a fix was applied).
|
||
pub findings_after: Option<usize>,
|
||
pub changed_files: Vec<String>,
|
||
pub gates: Vec<GateOutcome>,
|
||
/// All gates green and a non-empty fix was applied.
|
||
pub shipped: bool,
|
||
/// The branch carrying the fix, when shipped.
|
||
pub branch: Option<String>,
|
||
/// Energy apportioned to, or read for, this run's process trees,
|
||
/// microjoules: each cargo window's apportionment, and the L3 model's
|
||
/// own process-tree reading where there is one ([`L3Energy`]). When
|
||
/// `attributed`, it is a `ModelBased` figure resting on real readings:
|
||
/// the receipts' figure, and the honest per-workload cost. Otherwise it is
|
||
/// at best an estimate or a floor, and is context only.
|
||
pub attributed_uj: u64,
|
||
/// Each metered window's figure as an estimate, summed, microjoules:
|
||
/// over a cargo window the machine-wide SoC-CPU figure (an upper bound,
|
||
/// every process on the host), over the L3 window
|
||
/// [`L3Energy::figure_uj`]. When not `attributed`, this is the receipts'
|
||
/// figure, as an estimate.
|
||
pub soc_cpu_uj: u64,
|
||
/// True when every metered window rested on real per-process accounting
|
||
/// of a hardware CPU reading. False means the receipts carry an estimate.
|
||
pub attributed: bool,
|
||
/// The L3 model's window, when the model was consulted: its machine-wide
|
||
/// figure, its own process tree's reading and why that is partial, and
|
||
/// what it added to this run's figure. Its energy is in `soc_cpu_uj`,
|
||
/// `attributed_uj` and the receipts.
|
||
pub l3: Option<L3Energy>,
|
||
pub wall: Duration,
|
||
pub meter_source: String,
|
||
pub contract: Contract,
|
||
pub receipt: Receipt,
|
||
/// The DSSE envelope (in-toto Statement, JouleContract predicate).
|
||
pub envelope_json: String,
|
||
/// The sealed sandbox JCR-1 meter envelope backing the meter binding.
|
||
pub meter_envelope: Vec<u8>,
|
||
/// The receipt-local verdict claim string.
|
||
pub local_claim: String,
|
||
/// The formal-tier outcome, when a `.joule-fix/formal.json` was present and
|
||
/// the fix carried formalizations. `None` ⇒ no formal gate ran (the default,
|
||
/// behaving exactly as before). A failed formal gate appears in `gates` and
|
||
/// blocks shipping like any other.
|
||
pub formal: Option<FormalOutcome>,
|
||
}
|
||
|
||
impl RunReport {
|
||
/// Microjoules for the whole verified run (measure → fix → gate), the
|
||
/// figure the receipts carry: every cargo window and the L3 model's
|
||
/// window. When `attributed`, it is the energy ATTRIBUTED to this run's
|
||
/// process trees, not the machine-wide total. Otherwise it is each
|
||
/// window's estimate summed ([`soc_cpu_uj`](Self::soc_cpu_uj)), which is
|
||
/// then an estimate and is sealed as one (`Estimator`, `Unaccounted`).
|
||
/// It is never an apportioned zero for work that ran.
|
||
pub fn total_uj(&self) -> u64 {
|
||
if self.attributed {
|
||
self.attributed_uj
|
||
} else {
|
||
self.soc_cpu_uj
|
||
}
|
||
}
|
||
|
||
/// The headline metric nobody else publishes: microjoules per verified,
|
||
/// shipped fix. It is attributed when `attributed` and an estimate
|
||
/// otherwise. `None` when nothing shipped (energy was still spent and is
|
||
/// still on the receipt — refusals aren't free, and saying so is the
|
||
/// point).
|
||
pub fn uj_per_verified_fix(&self) -> Option<u64> {
|
||
if !self.shipped {
|
||
return None;
|
||
}
|
||
let fixed = self
|
||
.findings_after
|
||
.map(|after| self.findings_before.saturating_sub(after))
|
||
.unwrap_or(0);
|
||
if fixed == 0 {
|
||
None
|
||
} else {
|
||
Some(self.total_uj() / fixed as u64)
|
||
}
|
||
}
|
||
}
|
||
|
||
/// One induced remediation skill: a deterministic line transform keyed by
|
||
/// the lint's message text, compiled from a fix that SHIPPED through the
|
||
/// full gate at a stochastic tier. Recurrences of the same pattern never
|
||
/// consult a model again — the skill is the L1 form of an L3 lesson.
|
||
#[derive(Clone, Debug, Serialize, serde::Deserialize)]
|
||
pub struct Skill {
|
||
/// The normalized lint message (everything after `warning:`/`error:`).
|
||
pub message_key: String,
|
||
/// The exact offending line (as it appeared, trimmed).
|
||
pub old_line: String,
|
||
/// Its replacement (trimmed; original indentation is preserved on apply).
|
||
pub new_line: String,
|
||
/// How many times the skill has closed a recurrence.
|
||
pub hits: u64,
|
||
}
|
||
|
||
/// The skill store: a JSON file of induced rules. Plain data, no model,
|
||
/// no registry service — a skill you can read is a skill you can audit.
|
||
#[derive(Default, Serialize, serde::Deserialize)]
|
||
pub struct SkillStore {
|
||
pub skills: Vec<Skill>,
|
||
}
|
||
|
||
impl SkillStore {
|
||
pub fn load(path: &std::path::Path) -> SkillStore {
|
||
std::fs::read_to_string(path)
|
||
.ok()
|
||
.and_then(|s| serde_json::from_str(&s).ok())
|
||
.unwrap_or_default()
|
||
}
|
||
|
||
pub fn save(&self, path: &std::path::Path) {
|
||
if let Some(dir) = path.parent() {
|
||
let _ = std::fs::create_dir_all(dir);
|
||
}
|
||
if let Ok(json) = serde_json::to_string_pretty(self) {
|
||
let _ = std::fs::write(path, json);
|
||
}
|
||
}
|
||
}
|
||
|
||
/// The lint message with its location stripped: the class key.
|
||
fn message_key(finding: &str) -> Option<String> {
|
||
let tail = finding
|
||
.split_once(": warning: ")
|
||
.or_else(|| finding.split_once(": error: "))?
|
||
.1;
|
||
Some(tail.trim().to_string())
|
||
}
|
||
|
||
/// Harness configuration: identities and limits a deployment binds once.
|
||
pub struct Harness {
|
||
pub workspace: PathBuf,
|
||
/// Maximum changed lines a single run may ship.
|
||
pub max_diff_lines: usize,
|
||
/// L1 tier energy ceiling, joules (cargo subprocess work is host-priced,
|
||
/// not token-priced; default is deliberately generous and recorded).
|
||
pub ceiling_joules: f64,
|
||
/// Steward label for the meter seal + receipt signer derivation.
|
||
pub steward: String,
|
||
signing: ed25519_dalek::SigningKey,
|
||
/// The meter subsystem's own key: the energy attestation must not be
|
||
/// signed by the receipt signer (JouleContract §4.2 — a self-attested
|
||
/// meter does not bind). The sandbox meter is genuinely a different
|
||
/// component; it gets a different key.
|
||
meter_signing: ed25519_dalek::SigningKey,
|
||
/// The L3 stochastic fixer, as a subprocess seam: a command that reads a
|
||
/// remediation prompt on stdin and writes SEARCH/REPLACE blocks on
|
||
/// stdout. Any local model CLI plugs in here (a jouleclaw decode binary,
|
||
/// a federation leg) — and whatever comes back faces the same gates as
|
||
/// the deterministic tier, which is what makes a weak model SAFE to run.
|
||
/// Defaults from `JOULE_FIX_L3_CMD`; `None` disables the tier.
|
||
///
|
||
/// The command is metered ([`L3Energy`]) and its energy is part of the
|
||
/// run's figure. It runs under `sh`, which waits for a gate line before
|
||
/// it starts the command (so the meter opens on a shell at rest) and then
|
||
/// `exec`s a plain argv — `granite-fix /path/to/snapshot` — so the model
|
||
/// is the shell's own process and its own energy count is readable. A
|
||
/// command that needs the shell (a pipeline, a list, quoting) runs as the
|
||
/// shell's script instead, and what the shell forks and reaps is energy
|
||
/// no counter holds: the reading says so. The reading is never whole —
|
||
/// the model exits in its window, and an exiting process's record lacks
|
||
/// its last time on a core — so the window is always an estimate
|
||
/// ([`grade_l3`]).
|
||
pub l3_cmd: Option<String>,
|
||
/// Where induced skills persist. Defaults from `JOULE_FIX_SKILLS`, else
|
||
/// `~/.joule-fix/skills.json`; the store is created on first induction.
|
||
pub skill_store: PathBuf,
|
||
/// Per-process energy attribution, accumulated across cargo subprocesses.
|
||
/// `RefCell` because `run()` takes `&self` and feeds it call by call.
|
||
meter: RefCell<MeterAcc>,
|
||
/// Test builds only: the target directory every `cargo` run is handed
|
||
/// (`--target-dir`), the workspace's own `target/`, so a test's scratch
|
||
/// crate builds where it does with no `CARGO_TARGET_DIR`, whatever the
|
||
/// test process inherited. Every scratch crate is a package named
|
||
/// `scratch` at 0.1.0, and cargo names its artifacts without the path, so
|
||
/// under one exported `CARGO_TARGET_DIR` the concurrent tests' crates
|
||
/// built over each other's artifacts and fingerprints. Not in production
|
||
/// builds: `joule-fix` hands cargo no such flag, and the user's
|
||
/// environment, `CARGO_TARGET_DIR` included, decides where it builds.
|
||
#[cfg(test)]
|
||
cargo_target_dir: PathBuf,
|
||
}
|
||
|
||
impl Harness {
|
||
pub fn new(workspace: impl Into<PathBuf>) -> Result<Harness, HarnessError> {
|
||
let workspace = workspace.into();
|
||
// Inside ANY git work tree counts — a workspace may be a subdirectory
|
||
// of a monorepo. Revert-ability is the requirement, not a local .git.
|
||
let inside = Command::new("git")
|
||
.args(["rev-parse", "--is-inside-work-tree"])
|
||
.current_dir(&workspace)
|
||
.output()
|
||
.map(|o| o.status.success())
|
||
.unwrap_or(false);
|
||
if !inside {
|
||
return Err(HarnessError::NotGit(workspace));
|
||
}
|
||
#[cfg(test)]
|
||
let cargo_target_dir = workspace.join("target");
|
||
Ok(Harness {
|
||
workspace,
|
||
max_diff_lines: 400,
|
||
ceiling_joules: 2_000.0,
|
||
steward: "joule-fix.local".into(),
|
||
signing: ed25519_dalek::SigningKey::from_bytes(&[11u8; 32]),
|
||
meter_signing: ed25519_dalek::SigningKey::from_bytes(&[12u8; 32]),
|
||
l3_cmd: std::env::var("JOULE_FIX_L3_CMD").ok().filter(|s| !s.trim().is_empty()),
|
||
skill_store: std::env::var("JOULE_FIX_SKILLS")
|
||
.map(PathBuf::from)
|
||
.unwrap_or_else(|_| {
|
||
let home = std::env::var("HOME").unwrap_or_else(|_| ".".into());
|
||
PathBuf::from(home).join(".joule-fix/skills.json")
|
||
}),
|
||
meter: RefCell::new(MeterAcc {
|
||
meter: PowerMeter::detect(),
|
||
tally: EnergyTally::default(),
|
||
l3: None,
|
||
}),
|
||
#[cfg(test)]
|
||
cargo_target_dir,
|
||
})
|
||
}
|
||
|
||
/// Use a real signing key instead of the published demo key.
|
||
pub fn with_signing_key(mut self, key: ed25519_dalek::SigningKey) -> Self {
|
||
self.signing = key;
|
||
self
|
||
}
|
||
|
||
fn run(&self, program: &str, args: &[&str]) -> Result<(bool, String), HarnessError> {
|
||
// The real compute is `cargo`; meter and attribute it. Other programs
|
||
// (git, rustfmt) are negligible harness overhead and run unmetered.
|
||
if program == "cargo" {
|
||
let args = self.cargo_args(args);
|
||
let mut acc = self.meter.borrow_mut();
|
||
let MeterAcc { meter, tally, .. } = &mut *acc;
|
||
let (ok, text, a) = run_attributed(meter, program, &args, &self.workspace)
|
||
.map_err(|e| HarnessError::Spawn(format!("{program}: {e}")))?;
|
||
tally.add(&a);
|
||
return Ok((ok, text));
|
||
}
|
||
let out = Command::new(program)
|
||
.args(args)
|
||
.current_dir(&self.workspace)
|
||
.output()
|
||
.map_err(|e| HarnessError::Spawn(format!("{program}: {e}")))?;
|
||
let mut text = String::from_utf8_lossy(&out.stdout).into_owned();
|
||
text.push_str(&String::from_utf8_lossy(&out.stderr));
|
||
Ok((out.status.success(), text))
|
||
}
|
||
|
||
/// The arguments a `cargo` run is given: `args`, as passed. In test
|
||
/// builds only, `--target-dir <workspace>/target` follows the subcommand
|
||
/// (every cargo run here has one: `clippy`, `test`, `build`), and the
|
||
/// flag outranks an inherited `CARGO_TARGET_DIR`.
|
||
fn cargo_args<'a>(&'a self, args: &[&'a str]) -> Vec<&'a str> {
|
||
#[cfg(test)]
|
||
if let Some((sub, rest)) = args.split_first() {
|
||
let dir = self.cargo_target_dir.to_str().expect("a test workspace path is UTF-8");
|
||
return [*sub, "--target-dir", dir].into_iter().chain(rest.iter().copied()).collect();
|
||
}
|
||
args.to_vec()
|
||
}
|
||
|
||
fn git_head(&self) -> Result<String, HarnessError> {
|
||
let (ok, out) = self.run("git", &["rev-parse", "HEAD"])?;
|
||
if !ok {
|
||
return Err(HarnessError::Spawn("git rev-parse HEAD".into()));
|
||
}
|
||
Ok(out.trim().to_string())
|
||
}
|
||
|
||
fn git_clean(&self) -> Result<bool, HarnessError> {
|
||
let (_, out) = // -uno: the harness owns the TRACKED diff; untracked build artifacts
|
||
// (target/, .joule-fix/) are not its concern and must not wedge it.
|
||
self.run("git", &["status", "--porcelain", "--untracked-files=no", "--", "."])?;
|
||
Ok(out.trim().is_empty())
|
||
}
|
||
|
||
fn clippy_warning_count(&self) -> Result<usize, HarnessError> {
|
||
let (_, out) = self.run(
|
||
"cargo",
|
||
&["clippy", "--workspace", "--message-format=short", "--quiet"],
|
||
)?;
|
||
// A finding is a per-location diagnostic: "<path>:<line>:<col>: warning|error".
|
||
// Deny-by-default lints arrive as errors and are findings too (they
|
||
// don't block `cargo build`, only clippy itself). Summary lines
|
||
// ("error: could not compile …") carry no location and don't count.
|
||
Ok(out
|
||
.lines()
|
||
.filter(|l| {
|
||
l.contains(".rs:") && (l.contains(": warning:") || l.contains(": error:"))
|
||
})
|
||
.count())
|
||
}
|
||
|
||
fn test_failures(&self) -> Result<BTreeSet<String>, HarnessError> {
|
||
// NOT --quiet: quiet mode suppresses the per-test result lines the
|
||
// baseline diff is built from.
|
||
let (_, out) = self.run("cargo", &["test", "--workspace"])?;
|
||
Ok(out
|
||
.lines()
|
||
.filter_map(|l| l.strip_prefix("test ").and_then(|r| r.strip_suffix(" ... FAILED")))
|
||
.map(str::to_string)
|
||
.collect())
|
||
}
|
||
|
||
fn changed_files(&self) -> Result<Vec<String>, HarnessError> {
|
||
let (_, out) = self.run("git", &["diff", "--name-only", "--relative", "--", "."])?;
|
||
Ok(out.lines().map(str::to_string).filter(|s| !s.is_empty()).collect())
|
||
}
|
||
|
||
fn diff_lines(&self) -> Result<usize, HarnessError> {
|
||
let (_, out) = self.run("git", &["diff", "--numstat", "--relative", "--", "."])?;
|
||
Ok(out
|
||
.lines()
|
||
.filter_map(|l| {
|
||
let mut it = l.split_whitespace();
|
||
let add: usize = it.next()?.parse().ok()?;
|
||
let del: usize = it.next()?.parse().ok()?;
|
||
Some(add + del)
|
||
})
|
||
.sum())
|
||
}
|
||
|
||
/// One full verified-remediation run.
|
||
pub fn run_once(&self) -> Result<RunReport, HarnessError> {
|
||
if !self.git_clean()? {
|
||
return Err(HarnessError::Dirty);
|
||
}
|
||
// Load+validate the formal spec FIRST — a malformed spec must fail on a
|
||
// clean tree, before any edit the harness would then have to revert.
|
||
let formal_spec = self.load_formal_spec()?;
|
||
let prior_rev = self.git_head()?;
|
||
let prior = ContentId::of_bytes(prior_rev.as_bytes());
|
||
|
||
// Reset the per-run tally, all of it; this run's cargo calls and its
|
||
// L3 window feed it. An earlier run's windows are not this run's
|
||
// energy: without the reset, a second run on this Harness would seal
|
||
// the first run's figure into its own receipts (on every host,
|
||
// estimated or not), and an attributed earlier window could grade
|
||
// this one.
|
||
{
|
||
let mut acc = self.meter.borrow_mut();
|
||
acc.tally = EnergyTally::default();
|
||
acc.l3 = None;
|
||
}
|
||
let wall_start = Instant::now();
|
||
|
||
// ---- Stage 0: baseline (the `pre` obligation's evidence).
|
||
let baseline_failures = self.test_failures()?;
|
||
let findings_before = self.clippy_warning_count()?;
|
||
let baseline_captured = true;
|
||
|
||
let mut gates: Vec<GateOutcome> = vec![GateOutcome {
|
||
gate: "baseline".into(),
|
||
passed: baseline_captured,
|
||
detail: format!(
|
||
"{} clippy findings, {} pre-existing test failures recorded",
|
||
findings_before,
|
||
baseline_failures.len()
|
||
),
|
||
}];
|
||
|
||
// ---- Fix at the L1 lawful tier: deterministic codemods, no model.
|
||
// Nothing to fix ⇒ nothing runs: a clean workspace gets a verified-
|
||
// clean receipt, not a formatting pass dressed as remediation.
|
||
if findings_before > 0 {
|
||
let (_, _fix_out) = self.run(
|
||
"cargo",
|
||
&[
|
||
"clippy",
|
||
"--workspace",
|
||
"--fix",
|
||
"--allow-dirty",
|
||
"--allow-no-vcs",
|
||
"--quiet",
|
||
],
|
||
)?;
|
||
// Format ONLY the files the fix touched — reformatting untouched
|
||
// files is out-of-frame noise, not remediation.
|
||
let touched = self.changed_files()?;
|
||
for f in touched.iter().filter(|f| f.ends_with(".rs")) {
|
||
let _ = self.run("rustfmt", &["--edition", "2021", f]);
|
||
}
|
||
}
|
||
|
||
// ---- Induced skills next: lessons already paid for at a stochastic
|
||
// tier re-apply deterministically, before any model is consulted.
|
||
let mut skills_applied = 0usize;
|
||
if findings_before > 0 && self.clippy_warning_count()? > 0 {
|
||
skills_applied = self.skill_pass()?;
|
||
}
|
||
|
||
// ---- Escalate to L3 only what L1 + skills left behind (cheapest
|
||
// sufficient tier: the model is consulted last, and only when
|
||
// configured). Snapshot finding files first — a shipped L3 fix is
|
||
// the raw material skills are induced from.
|
||
let mut used_l3 = false;
|
||
// (path, message_key, offending line trimmed, old content)
|
||
let mut l3_snapshot: Vec<(String, String, String, String)> = Vec::new();
|
||
if self.l3_cmd.is_some() && findings_before > 0 && self.clippy_warning_count()? > 0 {
|
||
for f in self.current_findings()? {
|
||
let mut parts = f.split(':');
|
||
let (Some(path), line_no, Some(key)) =
|
||
(parts.next(), parts.next().and_then(|n| n.parse::<usize>().ok()), message_key(&f))
|
||
else {
|
||
continue;
|
||
};
|
||
if !path.ends_with(".rs") {
|
||
continue;
|
||
}
|
||
if let (Some(n), Ok(body)) = (line_no, std::fs::read_to_string(self.workspace.join(path))) {
|
||
if let Some(line) = body.lines().nth(n.saturating_sub(1)) {
|
||
l3_snapshot.push((path.to_string(), key, line.trim().to_string(), body));
|
||
}
|
||
}
|
||
}
|
||
used_l3 = self.l3_pass()?;
|
||
}
|
||
let changed = self.changed_files()?;
|
||
|
||
// ---- Gates (each one is an obligation's discharge evidence).
|
||
let build_ok = changed.is_empty() || self.run("cargo", &["build", "--workspace", "--quiet"])?.0;
|
||
gates.push(GateOutcome {
|
||
gate: "build".into(),
|
||
passed: build_ok,
|
||
detail: if changed.is_empty() { "no fix applied".into() } else { "cargo build --workspace".into() },
|
||
});
|
||
|
||
let post_failures = if changed.is_empty() { baseline_failures.clone() } else { self.test_failures()? };
|
||
let new_failures: Vec<&String> = post_failures.difference(&baseline_failures).collect();
|
||
let tests_ok = new_failures.is_empty();
|
||
gates.push(GateOutcome {
|
||
gate: "tests-vs-baseline".into(),
|
||
passed: tests_ok,
|
||
detail: if tests_ok {
|
||
"no new test failures".into()
|
||
} else {
|
||
format!("NEW failures: {new_failures:?}")
|
||
},
|
||
});
|
||
|
||
let findings_after = self.clippy_warning_count()?;
|
||
let lint_ok = changed.is_empty() || findings_after < findings_before;
|
||
gates.push(GateOutcome {
|
||
gate: "lint-delta".into(),
|
||
passed: lint_ok,
|
||
detail: format!("{findings_before} → {findings_after} findings"),
|
||
});
|
||
|
||
// Frame: the fix may touch Rust sources and manifests anywhere in the
|
||
// workspace — and nothing else (no CI files, no secrets, no scripts).
|
||
let frame_paths: Vec<String> = vec!["src/".into(), "crates/".into(), "Cargo.toml".into(), "Cargo.lock".into()];
|
||
let op = CodingOp {
|
||
alg: 0x01,
|
||
prior: prior.clone(),
|
||
edits: changed
|
||
.iter()
|
||
.map(|p| Edit {
|
||
path: p.clone(),
|
||
anchor: Anchor::ByteRange { start: 0, end: 0 },
|
||
replacement: Vec::new(), // identity carried by git; anchors are per-file markers here
|
||
})
|
||
.collect(),
|
||
author: self.signing.verifying_key().to_bytes(),
|
||
intent: format!(
|
||
"remediate {findings_before} lint findings ({}{})",
|
||
if used_l3 { "L1 lawful + L3 stochastic, gate-verified" } else { "L1 lawful tier" },
|
||
if skills_applied > 0 {
|
||
format!("; {skills_applied} induced skill(s) applied — zero inference")
|
||
} else {
|
||
String::new()
|
||
}
|
||
),
|
||
tier: if used_l3 { Tier::L3 } else { Tier::L1 },
|
||
};
|
||
let contract = self.contract(&frame_paths, findings_before);
|
||
let frame_ok = changed.is_empty()
|
||
|| joule_code_joulecontract::frame_check(&contract, &op).is_ok();
|
||
gates.push(GateOutcome {
|
||
gate: "frame".into(),
|
||
passed: frame_ok,
|
||
detail: format!("{} files changed, footprint {:?}", changed.len(), frame_paths),
|
||
});
|
||
|
||
let diff = self.diff_lines()?;
|
||
let diff_ok = diff <= self.max_diff_lines;
|
||
gates.push(GateOutcome {
|
||
gate: "diff-guard".into(),
|
||
passed: diff_ok,
|
||
detail: format!("{diff} changed lines (limit {})", self.max_diff_lines),
|
||
});
|
||
|
||
// ---- Formal tier (opt-in): if the run carries formalizations
|
||
// (`.joule-fix/formal.json`), the fix's formal obligations must be
|
||
// machine-checked by a decision procedure. A refuted or unproven goal
|
||
// fails the gate — which reverts the fix exactly like a failed test.
|
||
// The rung above build+test, and the one the market has not reached.
|
||
let formal = formal_spec.as_ref().map(|s| self.discharge_formal(s));
|
||
if let Some(f) = &formal {
|
||
// The detail rides into a failed gate's receipt entry, so it names
|
||
// the solver only when there was one to decide the goals.
|
||
let solver = if proof_solvers::z3_available() {
|
||
"real z3"
|
||
} else {
|
||
"no z3 on PATH: SMT goals left undecided"
|
||
};
|
||
gates.push(GateOutcome {
|
||
gate: "formal-proof".into(),
|
||
passed: f.all_proved,
|
||
detail: format!(
|
||
"{} proved, {} refuted, {} unproved ({:.3} J, {solver})",
|
||
f.proved,
|
||
f.refuted,
|
||
f.unproved,
|
||
f.proof_uj as f64 / 1e6,
|
||
),
|
||
});
|
||
}
|
||
|
||
// ---- Verdict: every gate green AND a real fix happened.
|
||
let all_green = gates.iter().all(|g| g.passed);
|
||
let shipped = all_green && !changed.is_empty();
|
||
|
||
let branch = if shipped {
|
||
let name = format!("joule-fix/{}", &prior_rev[..12.min(prior_rev.len())]);
|
||
// Shipped means committed. Every step is checked: an unchecked
|
||
// `checkout -b` that fails (the branch exists) would let the
|
||
// commit land on whatever branch is current, and an unchecked
|
||
// `commit` that fails (no git identity, a rejecting hook) would
|
||
// report a fix as shipped while it sits uncommitted in the tree.
|
||
let (ok, out) = self.run("git", &["checkout", "-b", &name])?;
|
||
if !ok {
|
||
return Err(HarnessError::Ship(format!(
|
||
"git checkout -b {name}: {} (the verified change is left uncommitted in the work tree)",
|
||
out.trim()
|
||
)));
|
||
}
|
||
// -u: stage only tracked modifications — the harness owns the
|
||
// tracked diff; untracked artifacts (target/) are not its fix.
|
||
let (ok, out) = self.run("git", &["add", "-u", "--", "."])?;
|
||
if !ok {
|
||
return Err(HarnessError::Ship(format!(
|
||
"git add on {name}: {} (the verified change is left uncommitted on {name})",
|
||
out.trim()
|
||
)));
|
||
}
|
||
let (ok, out) = self.run(
|
||
"git",
|
||
&["commit", "-m", &format!("joule-fix: {} lint findings remediated, all gates green", findings_before.saturating_sub(findings_after))],
|
||
)?;
|
||
if !ok {
|
||
return Err(HarnessError::Ship(format!(
|
||
"git commit on {name}: {} (the verified change is left staged on {name})",
|
||
out.trim()
|
||
)));
|
||
}
|
||
// A gate-verified stochastic fix is a lesson worth keeping:
|
||
// compile it into a deterministic skill so the next recurrence
|
||
// never pays the model's joules again.
|
||
if used_l3 {
|
||
self.induce_skills(&l3_snapshot);
|
||
}
|
||
Some(name)
|
||
} else {
|
||
// Never ship on a failed gate: revert the work tree — and VERIFY
|
||
// the revert took. A swallowed revert failure leaves the rejected
|
||
// diff in the user's tree, which is worse than shipping it.
|
||
let _ = self.run("git", &["checkout", "--", "."]);
|
||
if !self.git_clean()? {
|
||
let _ = self.run("git", &["restore", "--source=HEAD", "--worktree", "--", "."]);
|
||
}
|
||
if !self.git_clean()? {
|
||
return Err(HarnessError::Spawn(
|
||
"revert failed: rejected changes remain in the work tree — manual cleanup required".into(),
|
||
));
|
||
}
|
||
None
|
||
};
|
||
|
||
// ---- Energy: the per-window accounting accumulated across the run's
|
||
// cargo subprocesses and its L3 model. When every window was
|
||
// attributed, the receipts carry the ATTRIBUTED figure (ModelBased —
|
||
// resting on real readings), not the machine-wide total. Otherwise
|
||
// they carry an estimate and grade it as one — never a figure signed
|
||
// as a reading.
|
||
let (tally, meter_sources, l3) = {
|
||
let acc = self.meter.borrow();
|
||
(acc.tally.clone(), acc.meter.sources(), acc.l3.clone())
|
||
};
|
||
let (soc_cpu_uj, attributed_uj, attributed) = (tally.soc_uj, tally.attr_uj, tally.attributed());
|
||
let wall = wall_start.elapsed();
|
||
let base_source = tally.source(&meter_sources);
|
||
let meter_source = match &l3 {
|
||
Some(l3) => format!("{base_source}; {}", l3.describe()),
|
||
None => base_source,
|
||
};
|
||
|
||
// The sandbox meter receipt seals the receipts' figure with its grade:
|
||
// ModelBased for an attribution, the Estimator grade for an estimate.
|
||
// The JouleContract receipt anchors to it only when attributed.
|
||
let meter_receipt = sandbox_meter::Receipt::build(
|
||
sandbox_schema::ContentId::of_bytes(prior_rev.as_bytes()),
|
||
sandbox_schema::Tier::S0,
|
||
tally.meter_records(),
|
||
1,
|
||
[3u8; 8],
|
||
)
|
||
.map_err(|e| HarnessError::Contract(e.to_string()))?;
|
||
let meter_envelope = meter_receipt
|
||
.seal(&self.steward, &self.meter_signing)
|
||
.map_err(|e| HarnessError::Contract(e.to_string()))?;
|
||
|
||
let receipt = self.receipt(
|
||
&contract,
|
||
&op,
|
||
&tally,
|
||
&meter_envelope,
|
||
&gates,
|
||
findings_before,
|
||
findings_after,
|
||
)?;
|
||
let verdict =
|
||
validate(&contract, &receipt).map_err(|e| HarnessError::Contract(e.to_string()))?;
|
||
let envelope = joulecontract_wire::emit(&receipt, &self.signing)
|
||
.map_err(|e| HarnessError::Contract(e.to_string()))?;
|
||
|
||
Ok(RunReport {
|
||
findings_before,
|
||
findings_after: if changed.is_empty() { None } else { Some(findings_after) },
|
||
changed_files: changed,
|
||
gates,
|
||
shipped,
|
||
branch,
|
||
attributed_uj,
|
||
soc_cpu_uj,
|
||
attributed,
|
||
l3,
|
||
wall,
|
||
meter_source,
|
||
contract,
|
||
receipt,
|
||
envelope_json: serde_json::to_string_pretty(&envelope)
|
||
.map_err(|e| HarnessError::Contract(e.to_string()))?,
|
||
meter_envelope,
|
||
local_claim: verdict.claim(),
|
||
formal,
|
||
})
|
||
}
|
||
|
||
/// Load and validate `<workspace>/.joule-fix/formal.json` (the formal tier's
|
||
/// input) **before any edit is applied**, so a malformed spec fails fast on
|
||
/// a clean tree rather than mid-run. `None` when no formal spec is present —
|
||
/// the default, leaving the run identical to before. Index/duplicate checks
|
||
/// mirror the proof bridge's so the later discharge cannot fail.
|
||
fn load_formal_spec(&self) -> Result<Option<FormalSpec>, HarnessError> {
|
||
let path = self.workspace.join(".joule-fix/formal.json");
|
||
let Ok(text) = std::fs::read_to_string(&path) else {
|
||
return Ok(None);
|
||
};
|
||
let spec: FormalSpec = serde_json::from_str(&text).map_err(|e| {
|
||
HarnessError::Contract(format!(
|
||
"formal.json: {e} — see formal.example.json for the exact serde forms \
|
||
(rigor_target JR-1..JR-4, enb_ref a 'sha2-256:<64-hex>' string, \
|
||
kind/grounding PascalCase)"
|
||
))
|
||
})?;
|
||
let n = spec.contract.obligations().len();
|
||
let mut seen = BTreeSet::new();
|
||
for f in &spec.formalizations {
|
||
if f.obligation >= n {
|
||
return Err(HarnessError::Contract(format!(
|
||
"formal.json: formalization names obligation {} but the contract declares {n}",
|
||
f.obligation
|
||
)));
|
||
}
|
||
if !seen.insert(f.obligation) {
|
||
return Err(HarnessError::Contract(format!(
|
||
"formal.json: duplicate formalization for obligation {}",
|
||
f.obligation
|
||
)));
|
||
}
|
||
}
|
||
Ok(Some(spec))
|
||
}
|
||
|
||
/// The formally-verified fix tier: discharge the loaded formalizations
|
||
/// through the proof cascade over a real `z3` — a **decision-procedure
|
||
/// ladder only** (`Propositional`, then `Z3Smt`): a formal gate must never
|
||
/// fall through to a model stand-in. Writes the full per-obligation
|
||
/// discharge to `.joule-fix/formal-discharge.json` as re-checkable evidence.
|
||
fn discharge_formal(&self, spec: &FormalSpec) -> FormalOutcome {
|
||
let router = Router::new(vec![Box::new(Propositional), Box::new(Z3Smt)]);
|
||
let mut cache = ProofCache::new();
|
||
// Indices were validated in `load_formal_spec`, so the only `Err` here
|
||
// would be a bug; fail the gate safely rather than ship an unproven fix.
|
||
let Ok(dis) = proof_discharge(&spec.contract, &spec.formalizations, &router, &mut cache)
|
||
else {
|
||
return FormalOutcome {
|
||
proved: 0,
|
||
refuted: 0,
|
||
unproved: spec.formalizations.len(),
|
||
proof_uj: 0,
|
||
all_proved: false,
|
||
entries: Vec::new(),
|
||
};
|
||
};
|
||
|
||
let (mut proved, mut refuted, mut unproved) = (0usize, 0usize, 0usize);
|
||
let mut entries = Vec::new();
|
||
for e in &dis.entries {
|
||
// Only obligations that were actually formalized belong to THIS
|
||
// gate; unformalized ones are the operational gates' business and
|
||
// the bridge records them separately (demoted, never dropped).
|
||
let (verdict, closed_by, counter_model, uj) = match &e.status {
|
||
DischargeStatus::Proved(r) => {
|
||
proved += 1;
|
||
("proved", r.closed_by.map(|t| format!("{t:?}")), None, r.total_uj)
|
||
}
|
||
DischargeStatus::Unproved(r) if r.refuted => {
|
||
refuted += 1;
|
||
("refuted", None, r.counter_model.clone(), r.total_uj)
|
||
}
|
||
DischargeStatus::Unproved(r) => {
|
||
unproved += 1;
|
||
("unproved", None, None, r.total_uj)
|
||
}
|
||
DischargeStatus::Unformalized => continue,
|
||
};
|
||
entries.push(FormalEntry {
|
||
obligation: e.obligation.text.clone(),
|
||
verdict: verdict.into(),
|
||
closed_by,
|
||
counter_model,
|
||
uj,
|
||
});
|
||
}
|
||
let supplied = proved + refuted + unproved;
|
||
// The gate: at least one formalization, and every one proved. Any
|
||
// refutation or unproven goal fails it (and reverts the fix).
|
||
let all_proved = supplied > 0 && refuted == 0 && unproved == 0;
|
||
let proof_uj = entries.iter().map(|e| e.uj).sum();
|
||
|
||
// Evidence an auditor can re-check independently of this report.
|
||
let evidence = self.workspace.join(".joule-fix/formal-discharge.json");
|
||
if let Some(dir) = evidence.parent() {
|
||
let _ = std::fs::create_dir_all(dir);
|
||
}
|
||
if let Ok(j) = serde_json::to_string_pretty(&dis) {
|
||
let _ = std::fs::write(&evidence, j);
|
||
}
|
||
|
||
FormalOutcome { proved, refuted, unproved, proof_uj, all_proved, entries }
|
||
}
|
||
|
||
/// The current per-location findings (short-format diagnostic lines).
|
||
fn current_findings(&self) -> Result<Vec<String>, HarnessError> {
|
||
let (_, lint_out) = self.run(
|
||
"cargo",
|
||
&["clippy", "--workspace", "--message-format=short", "--quiet"],
|
||
)?;
|
||
Ok(lint_out
|
||
.lines()
|
||
.filter(|l| l.contains(".rs:") && (l.contains(": warning:") || l.contains(": error:")))
|
||
.map(str::to_string)
|
||
.collect())
|
||
}
|
||
|
||
/// The induced-skill tier: for each remaining finding whose message
|
||
/// matches a stored skill, apply the line transform deterministically.
|
||
/// Zero inference; the gates still judge the result like anyone else's.
|
||
fn skill_pass(&self) -> Result<usize, HarnessError> {
|
||
let mut store = SkillStore::load(&self.skill_store);
|
||
if store.skills.is_empty() {
|
||
return Ok(0);
|
||
}
|
||
let mut applied = 0usize;
|
||
for finding in self.current_findings()? {
|
||
let (Some(path), Some(key)) = (finding.split(':').next(), message_key(&finding)) else {
|
||
continue;
|
||
};
|
||
if !path.ends_with(".rs") {
|
||
continue;
|
||
}
|
||
let Some(skill) = store.skills.iter_mut().find(|s| s.message_key == key) else {
|
||
continue;
|
||
};
|
||
let full = self.workspace.join(path);
|
||
let Ok(content) = std::fs::read_to_string(&full) else { continue };
|
||
let mut lines: Vec<String> = content.lines().map(str::to_string).collect();
|
||
let mut hit = false;
|
||
for line in lines.iter_mut() {
|
||
if line.trim() == skill.old_line {
|
||
let indent: String = line.chars().take_while(|c| c.is_whitespace()).collect();
|
||
*line = format!("{indent}{}", skill.new_line);
|
||
hit = true;
|
||
break;
|
||
}
|
||
}
|
||
if hit {
|
||
let mut out = lines.join("\n");
|
||
if content.ends_with('\n') {
|
||
out.push('\n');
|
||
}
|
||
if std::fs::write(&full, out).is_ok() {
|
||
skill.hits += 1;
|
||
applied += 1;
|
||
}
|
||
}
|
||
}
|
||
if applied > 0 {
|
||
store.save(&self.skill_store);
|
||
}
|
||
Ok(applied)
|
||
}
|
||
|
||
/// Induce skills from a SHIPPED stochastic fix. The rule is anchored to
|
||
/// the finding's OFFENDING LINE: when it vanished from the fixed file,
|
||
/// its replacement is the new line sharing the longest common prefix
|
||
/// (models reformat around the fix; the lesson is the line, not the
|
||
/// file). Only gate-verified lessons compile; a reverted fix teaches
|
||
/// nothing — and a badly-induced skill cannot ship damage either, since
|
||
/// every application faces the same gates.
|
||
fn induce_skills(&self, snapshot: &[(String, String, String, String)]) {
|
||
let mut store = SkillStore::load(&self.skill_store);
|
||
let mut induced = false;
|
||
for (path, key, offending, old_content) in snapshot {
|
||
if offending.is_empty() || store.skills.iter().any(|s| s.message_key == *key) {
|
||
continue;
|
||
}
|
||
let Ok(new_content) = std::fs::read_to_string(self.workspace.join(path)) else {
|
||
continue;
|
||
};
|
||
let new_trimmed: Vec<&str> =
|
||
new_content.lines().map(str::trim).filter(|l| !l.is_empty()).collect();
|
||
if new_trimmed.contains(&offending.as_str()) {
|
||
continue; // the offending line survived: nothing was learned
|
||
}
|
||
let old_set: BTreeSet<&str> = old_content.lines().map(str::trim).collect();
|
||
let common_prefix = |a: &str, b: &str| -> usize {
|
||
a.bytes().zip(b.bytes()).take_while(|(x, y)| x == y).count()
|
||
};
|
||
let Some((best, plen)) = new_trimmed
|
||
.iter()
|
||
.filter(|l| !old_set.contains(**l))
|
||
.map(|l| (*l, common_prefix(l, offending)))
|
||
.max_by_key(|(_, p)| *p)
|
||
else {
|
||
continue;
|
||
};
|
||
// The replacement must visibly descend from the offending line.
|
||
if plen < 6.max(offending.len() / 4) {
|
||
continue;
|
||
}
|
||
store.skills.push(Skill {
|
||
message_key: key.clone(),
|
||
old_line: offending.clone(),
|
||
new_line: best.to_string(),
|
||
hits: 0,
|
||
});
|
||
induced = true;
|
||
}
|
||
if induced {
|
||
store.save(&self.skill_store);
|
||
}
|
||
}
|
||
|
||
/// One L3 consultation: prompt = the remaining findings plus the touched
|
||
/// files' contents; reply = SEARCH/REPLACE blocks, applied verbatim.
|
||
/// Returns true when the model changed anything. The GATES decide whether
|
||
/// any of it survives — this function trusts nothing it applies. The
|
||
/// model's command is metered and its energy enters the run's figure
|
||
/// ([`run_l3`](Self::run_l3)).
|
||
fn l3_pass(&self) -> Result<bool, HarnessError> {
|
||
let cmd = self.l3_cmd.as_ref().expect("caller checked");
|
||
|
||
let all = self.current_findings()?;
|
||
let findings: Vec<&str> = all.iter().map(String::as_str).take(8).collect();
|
||
let mut files: BTreeSet<String> = BTreeSet::new();
|
||
for f in &findings {
|
||
if let Some(path) = f.split(':').next() {
|
||
if path.ends_with(".rs") && self.workspace.join(path).exists() {
|
||
files.insert(path.to_string());
|
||
}
|
||
}
|
||
}
|
||
let single_file = (files.len() == 1).then(|| files.iter().next().cloned().unwrap());
|
||
let mut prompt = if let Some(f) = &single_file {
|
||
// Whole-file replacement: the easier task for a small model, and
|
||
// the gates plus the diff guard bound the blast radius.
|
||
format!(
|
||
"Fix the Rust lint findings below by correcting the file. Reply with the COMPLETE corrected contents of {f} in a single ```rust code fence. No explanation.\n\nFindings:\n"
|
||
)
|
||
} else {
|
||
String::from(
|
||
"Fix the following Rust lint findings. Reply ONLY with one or more blocks of the form:\n <<<<<<< SEARCH <path>\n<exact text to find>\n=======\n<replacement>\n>>>>>>> REPLACE\n\nFindings:\n",
|
||
)
|
||
};
|
||
for f in &findings {
|
||
prompt.push_str(f);
|
||
prompt.push('\n');
|
||
}
|
||
for path in &files {
|
||
if let Ok(body) = std::fs::read_to_string(self.workspace.join(path)) {
|
||
prompt.push_str(&format!("\n--- {path} ---\n{body}"));
|
||
}
|
||
}
|
||
|
||
let reply = self.run_l3(cmd, prompt.as_bytes())?;
|
||
|
||
if self.apply_search_replace(&reply) {
|
||
return Ok(true);
|
||
}
|
||
if let Some(f) = &single_file {
|
||
return Ok(self.apply_fenced_file(&reply, f));
|
||
}
|
||
Ok(false)
|
||
}
|
||
|
||
/// Run the L3 command on `prompt` and meter it: its stdout, with the
|
||
/// window's [`L3Energy`] added to this run's tally.
|
||
///
|
||
/// The command is spawned as [`l3_script`] says, waiting on its gate.
|
||
/// The tree meter (where this host has one) is rooted at that process and
|
||
/// reads it at rest; the machine-wide span opens; the gate line and the
|
||
/// prompt go to its stdin, and it runs. Its stdout is read to the end, it
|
||
/// is waited for without being reaped, so its exited count is still
|
||
/// readable, and the tree meter's span is stopped on it; then it is
|
||
/// reaped and the machine-wide span closed. [`grade_l3`] grades the two.
|
||
fn run_l3(&self, cmd: &str, prompt: &[u8]) -> Result<String, HarnessError> {
|
||
use std::io::{Read, Write};
|
||
let (script, direct_child) = l3_script(cmd);
|
||
// The per-process counter's liveness probe burns about 300 ms of CPU
|
||
// on this thread the first time: here, before anything is spawned.
|
||
let _ = sandbox_meter::process_energy_status();
|
||
let mut child = Command::new("sh")
|
||
.args(["-c", &script])
|
||
.current_dir(&self.workspace)
|
||
.stdin(std::process::Stdio::piped())
|
||
.stdout(std::process::Stdio::piped())
|
||
.stderr(std::process::Stdio::null())
|
||
.spawn()
|
||
.map_err(|e| HarnessError::Spawn(format!("L3 cmd: {e}")))?;
|
||
let pid = child.id();
|
||
// `None` off macOS, where the per-process counter is not live, or
|
||
// where the process cannot be read.
|
||
let tree = TreeMeter::for_process(pid);
|
||
let tree_start = tree.as_ref().map(TreeMeter::start);
|
||
|
||
let mut acc = self.meter.borrow_mut();
|
||
let machine = acc.meter.start();
|
||
if let Some(mut stdin) = child.stdin.take() {
|
||
// The gate, then the prompt; dropping stdin closes it. A command
|
||
// that stops reading early closes the pipe, and the rest of the
|
||
// prompt is its own business, as it always was.
|
||
let _ = stdin.write_all(b"\n").and_then(|()| stdin.write_all(prompt));
|
||
}
|
||
let mut reply = Vec::new();
|
||
if let Some(mut out) = child.stdout.take() {
|
||
let _ = out.read_to_end(&mut reply);
|
||
}
|
||
let reading = match (&tree, tree_start) {
|
||
(Some(tree), Some(start)) => {
|
||
// Exited and not reaped: the stop walk reads its final record.
|
||
// Should the wait fail, the walk reads whatever the process is
|
||
// then, and its gaps say so.
|
||
let _ = wait_exited_unreaped(pid);
|
||
Some(tree.stop(start))
|
||
}
|
||
_ => None,
|
||
};
|
||
let status = child.wait();
|
||
let m = machine.stop(&mut acc.meter);
|
||
let by_class = m.devices.iter().map(|d| (d.class, d.measured_uj.unwrap_or(d.estimated_uj))).collect();
|
||
let l3 = grade_l3(reading.as_ref(), by_class, direct_child);
|
||
acc.tally.add_l3(&l3);
|
||
acc.l3 = Some(l3);
|
||
status.map_err(|e| HarnessError::Spawn(format!("L3 cmd: {e}")))?;
|
||
Ok(String::from_utf8_lossy(&reply).into_owned())
|
||
}
|
||
|
||
/// Apply a whole-file reply: the first fenced code block becomes the
|
||
/// file's new contents. Trusts nothing — the gates judge the result.
|
||
fn apply_fenced_file(&self, reply: &str, path: &str) -> bool {
|
||
let Some(open) = reply.find("```") else { return false };
|
||
let after = &reply[open + 3..];
|
||
let Some(nl) = after.find('\n') else { return false };
|
||
let body = &after[nl + 1..];
|
||
let Some(close) = body.find("\n```") else { return false };
|
||
let new_content = &body[..close + 1];
|
||
if new_content.trim().is_empty() {
|
||
return false;
|
||
}
|
||
std::fs::write(self.workspace.join(path), new_content).is_ok()
|
||
}
|
||
|
||
/// Apply SEARCH/REPLACE blocks. Unparseable or non-matching blocks are
|
||
/// skipped — the model gets no error channel and no second chance; the
|
||
/// lint-delta gate will simply find its work insufficient.
|
||
fn apply_search_replace(&self, reply: &str) -> bool {
|
||
let mut applied = false;
|
||
let mut rest = reply;
|
||
while let Some(start) = rest.find("<<<<<<< SEARCH ") {
|
||
let block = &rest[start + "<<<<<<< SEARCH ".len()..];
|
||
let Some(nl) = block.find('\n') else { break };
|
||
let path = block[..nl].trim().to_string();
|
||
let body = &block[nl + 1..];
|
||
let (Some(sep), Some(end)) = (body.find("\n=======\n"), body.find("\n>>>>>>> REPLACE")) else {
|
||
break;
|
||
};
|
||
if sep < end {
|
||
let search = &body[..sep];
|
||
let replace = &body[sep + "\n=======\n".len()..end];
|
||
let full = self.workspace.join(&path);
|
||
// Path safety belongs to the frame gate, but directory
|
||
// traversal never even gets applied.
|
||
if !path.contains("..") && full.exists() {
|
||
if let Ok(content) = std::fs::read_to_string(&full) {
|
||
if content.contains(search) {
|
||
let new_content = content.replacen(search, replace, 1);
|
||
if std::fs::write(&full, new_content).is_ok() {
|
||
applied = true;
|
||
}
|
||
}
|
||
}
|
||
}
|
||
}
|
||
rest = &body[end..];
|
||
}
|
||
applied
|
||
}
|
||
|
||
/// The run's contract: the gates, stated as obligations.
|
||
fn contract(&self, frame: &[String], findings: usize) -> Contract {
|
||
Contract {
|
||
joulecontract: "0.8.0".into(),
|
||
subject: format!("L1 lint remediation of {findings} findings in {}", self.workspace.display()),
|
||
rigor_target: Rigor::Jr2,
|
||
pre: vec!["baseline captured: test failures and lint findings recorded before any edit".into()],
|
||
post: vec![
|
||
"build succeeds after the fix".into(),
|
||
"no test failures beyond the recorded baseline".into(),
|
||
"lint finding count strictly decreased".into(),
|
||
],
|
||
inv: vec![format!(
|
||
"total diff within {} changed lines",
|
||
self.max_diff_lines
|
||
)],
|
||
frame: frame.to_vec(),
|
||
ceiling: Ceiling {
|
||
enpi_joules: self.ceiling_joules,
|
||
unit: "EOC-J".into(),
|
||
enb_ref: ContentAddress::of_bytes(b"joule-fix L1 EnB v0: host cargo pipeline, no inference"),
|
||
derivation: None, // honestly unanchored until an energy office signs a basis
|
||
},
|
||
sector_equivalence: None,
|
||
amends: None,
|
||
}
|
||
}
|
||
|
||
/// Build the receipt: one discharge entry per obligation, result taken
|
||
/// from the matching gate's ACTUAL outcome.
|
||
#[allow(clippy::too_many_arguments)]
|
||
fn receipt(
|
||
&self,
|
||
contract: &Contract,
|
||
op: &CodingOp,
|
||
energy: &EnergyTally,
|
||
meter_envelope: &[u8],
|
||
gates: &[GateOutcome],
|
||
before: usize,
|
||
after: usize,
|
||
) -> Result<Receipt, HarnessError> {
|
||
let gate_for = |kind: &ObligationKind, text: &str| -> &GateOutcome {
|
||
let name = match (kind, text) {
|
||
(ObligationKind::Pre, _) => "baseline",
|
||
(ObligationKind::Post, t) if t.starts_with("build") => "build",
|
||
(ObligationKind::Post, t) if t.starts_with("no test") => "tests-vs-baseline",
|
||
(ObligationKind::Post, _) => "lint-delta",
|
||
(ObligationKind::Inv, _) => "diff-guard",
|
||
(ObligationKind::Frame, _) => "frame",
|
||
};
|
||
gates.iter().find(|g| g.gate == name).expect("gate exists")
|
||
};
|
||
|
||
let harness_key = ContentAddress::of_bytes(self.signing.verifying_key().as_bytes());
|
||
let tier_addr = ContentAddress::of_bytes(b"joule-fix L1 lawful pipeline v0");
|
||
let qualification = Qualification {
|
||
attestation: ContentAddress::of_bytes(b"joule-fix gate suite v0: cargo build/test/clippy as deterministic verifiers"),
|
||
signer_key: harness_key.clone(),
|
||
valid_until: u64::MAX,
|
||
validated_at: 0,
|
||
root: Some(TrustRoot::ReferenceImpl),
|
||
};
|
||
|
||
let discharge: Vec<DischargeEntry> = contract
|
||
.obligations()
|
||
.into_iter()
|
||
.map(|ob| {
|
||
let gate = gate_for(&ob.kind, &ob.text);
|
||
let is_frame = ob.kind == ObligationKind::Frame;
|
||
DischargeEntry {
|
||
obligation: ob,
|
||
tier: tier_addr.clone(),
|
||
tier_class: TierClass::Deterministic,
|
||
tier_operator_keys: BTreeSet::from([harness_key.clone()]),
|
||
result: if gate.passed {
|
||
DischargeResult::Closed
|
||
} else {
|
||
DischargeResult::Undischarged {
|
||
reason: format!("{}: {}", gate.gate, gate.detail),
|
||
}
|
||
},
|
||
mode: is_frame.then_some(FrameMode::Observed),
|
||
qualification: Some(qualification.clone()),
|
||
verifier_keys: BTreeSet::from([harness_key.clone()]),
|
||
// Self-run harness: verifier == generator party, stated
|
||
// plainly. Independence computes false and the receipt
|
||
// grades accordingly — that's the honest local ceiling.
|
||
verifier_entity: None,
|
||
engagement: Some(Engagement {
|
||
selected_by: self.steward.clone(),
|
||
compensated_by: self.steward.clone(),
|
||
}),
|
||
recourse: None,
|
||
re_discharged_by: None,
|
||
}
|
||
})
|
||
.collect();
|
||
|
||
// An attributed figure is an apportionment of a real SoC reading:
|
||
// ModelBased, never Metered (a process is not a shunt), and anchored
|
||
// to the sealed sandbox meter receipt that carries it. Unless every
|
||
// window was attributed, the figure is an estimate, and Unaccounted
|
||
// (energy estimated where the substrate exposes no reading) is the
|
||
// honest class.
|
||
let provenance = energy.energy_class();
|
||
let energy_anchor =
|
||
energy.attributed().then(|| ContentAddress::of_bytes(meter_envelope));
|
||
// No MeterBinding: that attests a Metered (direct-shunt) figure, which
|
||
// this is not. The energy_anchor is the ModelBased evidence path.
|
||
let meter: Option<MeterBinding> = None;
|
||
|
||
Ok(Receipt {
|
||
contract: contract
|
||
.content_address()
|
||
.map_err(|e| HarnessError::Contract(e.to_string()))?,
|
||
transition: joule_code_joulecontract::bridge_id(&op.prior),
|
||
generator: Generator {
|
||
system: format!("joule-fix v0 (L1 lawful: clippy --fix + rustfmt; {before}→{after} findings)"),
|
||
version_digest: ContentAddress::of_bytes(env!("CARGO_PKG_VERSION").as_bytes()),
|
||
attestation: None, // self-run: honestly generator_unattested
|
||
attestation_signer: None,
|
||
key_set: BTreeSet::from([harness_key.clone()]),
|
||
entity: None,
|
||
human_principals: vec![self.steward.clone()],
|
||
loop_governance: None,
|
||
},
|
||
discharge,
|
||
execution: vec![tier_addr],
|
||
joules_spent: energy.figure_uj() as f64 / 1e6,
|
||
meter,
|
||
energy_anchor,
|
||
joules_allowed: contract.ceiling.enpi_joules,
|
||
provenance,
|
||
enb_ref: contract.ceiling.enb_ref.clone(),
|
||
grid_mix: None,
|
||
register_pin: ContentAddress::of_bytes(b"joule-fix register v0"),
|
||
evidence: None, // local receipt: evidence:external, stated not hidden
|
||
claimed_profile: Profile {
|
||
rigor: Rigor::Jr1, // self-verified: independence computes false
|
||
energy: provenance,
|
||
governance: GovernanceClass::Declared,
|
||
},
|
||
receipt_signer: harness_key,
|
||
})
|
||
}
|
||
}
|
||
|
||
#[cfg(test)]
|
||
mod tests {
|
||
use super::*;
|
||
|
||
fn sh(dir: &std::path::Path, cmd: &str) {
|
||
let ok = Command::new("sh")
|
||
.arg("-c")
|
||
.arg(cmd)
|
||
.current_dir(dir)
|
||
.output()
|
||
.map(|o| o.status.success())
|
||
.unwrap_or(false);
|
||
assert!(ok, "setup command failed: {cmd}");
|
||
}
|
||
|
||
/// Build a scratch git crate with deterministic, clippy-fixable findings.
|
||
fn scratch_crate(label: &str) -> PathBuf {
|
||
let dir = std::env::temp_dir().join(format!("joule-fix-test-{label}-{}", std::process::id()));
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
std::fs::create_dir_all(dir.join("src")).unwrap();
|
||
std::fs::write(
|
||
dir.join("Cargo.toml"),
|
||
"[package]\nname = \"scratch\"\nversion = \"0.1.0\"\nedition = \"2021\"\n\n[workspace]\n",
|
||
)
|
||
.unwrap();
|
||
std::fs::write(
|
||
dir.join("src/main.rs"),
|
||
r#"fn answer() -> u64 { return 42; }
|
||
fn main() { let x: u64 = answer(); println!("{}", x); }
|
||
#[test]
|
||
fn answers() { assert_eq!(answer(), 42); }
|
||
"#,
|
||
)
|
||
.unwrap();
|
||
// A repo-local identity: the harness's own ship commit must work in
|
||
// any environment, including a CI container with no global git
|
||
// identity (where it used to fail silently and leave the tree dirty).
|
||
sh(&dir, "git init -q && git config user.email t@t && git config user.name t && git add -A && git commit -qm init");
|
||
dir
|
||
}
|
||
|
||
fn git_out(dir: &std::path::Path, args: &[&str]) -> String {
|
||
let o = Command::new("git").args(args).current_dir(dir).output().unwrap();
|
||
assert!(o.status.success(), "git {args:?}: {}", String::from_utf8_lossy(&o.stderr));
|
||
String::from_utf8_lossy(&o.stdout).trim().to_string()
|
||
}
|
||
|
||
#[test]
|
||
fn verified_fix_end_to_end_ships_with_receipt() {
|
||
let dir = scratch_crate("ship");
|
||
let before = git_out(&dir, &["rev-parse", "HEAD"]);
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
// A test's cargo runs build in the scratch crate's own `target/`:
|
||
// `--target-dir` follows the subcommand and outranks an inherited
|
||
// `CARGO_TARGET_DIR`, under which every scratch crate (each named
|
||
// `scratch`) would share one target directory with the other tests'.
|
||
let own_target = dir.join("target");
|
||
assert_eq!(
|
||
h.cargo_args(&["test", "--workspace"]),
|
||
["test", "--target-dir", own_target.to_str().unwrap(), "--workspace"]
|
||
);
|
||
let report = h.run_once().unwrap();
|
||
assert!(own_target.join("debug").is_dir(), "the scratch crate did not build in its own target directory");
|
||
|
||
assert!(report.findings_before > 0, "scratch crate has findings");
|
||
assert!(report.shipped, "gates: {:?}", report.gates);
|
||
assert!(report.gates.iter().all(|g| g.passed));
|
||
assert_eq!(report.findings_after, Some(0));
|
||
// Shipped means committed: the fix is a commit on the reported branch,
|
||
// on top of where the run started, and nothing is left uncommitted.
|
||
let branch = report.branch.clone().expect("a shipped fix names its branch");
|
||
assert_eq!(git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]), branch);
|
||
assert_eq!(git_out(&dir, &["rev-parse", "HEAD~1"]), before, "one commit on top of the start");
|
||
assert!(git_out(&dir, &["status", "--porcelain", "--untracked-files=no"]).is_empty(), "shipped, yet the tree is dirty");
|
||
// Work ran, so the figure is never zero — attributed or estimated.
|
||
assert!(report.total_uj() > 0, "{} µJ ({})", report.total_uj(), report.meter_source);
|
||
assert!(report.uj_per_verified_fix().is_some_and(|uj| uj > 0));
|
||
|
||
// Both receipts grade the figure by how it was obtained.
|
||
eprintln!(
|
||
"joule-fix run: attributed={} total_uj={} soc_cpu_uj={} attributed_uj={} ({})",
|
||
report.attributed, report.total_uj(), report.soc_cpu_uj, report.attributed_uj, report.meter_source
|
||
);
|
||
assert_eq!(report.receipt.joules_spent, report.total_uj() as f64 / 1e6);
|
||
let sealed = sandbox_meter::jcr1::open(&report.meter_envelope).expect("meter envelope").payload;
|
||
let seals = |grade: &str| sealed.windows(grade.len()).any(|w| w == grade.as_bytes());
|
||
if report.attributed {
|
||
assert_eq!(report.receipt.provenance, EnergyClass::ModelBased);
|
||
assert!(seals("ModelBased") && !seals("Estimator"), "meter envelope grade");
|
||
} else {
|
||
assert_eq!(report.receipt.provenance, EnergyClass::Unaccounted);
|
||
assert!(report.receipt.energy_anchor.is_none());
|
||
assert!(
|
||
seals("Estimator") && !seals("ModelBased"),
|
||
"an estimate sealed in the meter envelope as ModelBased"
|
||
);
|
||
}
|
||
// Where the meter cannot read CPU energy at all, nothing is attributed.
|
||
#[cfg(all(target_os = "macos", target_arch = "aarch64"))]
|
||
if sandbox_meter::ioreport_status() != sandbox_meter::IoReportStatus::Live {
|
||
assert!(!report.attributed, "attributed with no live CPU rail ({:?})", sandbox_meter::ioreport_status());
|
||
}
|
||
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
|
||
assert!(!report.attributed, "the unattributed fallback never attributes");
|
||
|
||
// The receipt validates locally and tells the truth about itself:
|
||
// self-verified ⇒ independence false ⇒ JR-1 ceiling, stated.
|
||
let v = validate(&report.contract, &report.receipt).unwrap();
|
||
assert!(v.permits(&report.receipt.claimed_profile), "claim: {}", v.claim());
|
||
assert!(report.envelope_json.contains("in-toto"));
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// A fix that passes every gate but cannot be committed did not ship.
|
||
/// The harness used to discard `git commit`'s result and report
|
||
/// `shipped: true` with a branch name while the fix sat uncommitted.
|
||
/// That is what a CI container with no git identity produced.
|
||
#[test]
|
||
fn a_fix_whose_commit_is_rejected_is_never_reported_shipped() {
|
||
let dir = scratch_crate("commit-rejected");
|
||
sh(&dir, "printf '#!/bin/sh\\nexit 1\\n' > .git/hooks/pre-commit && chmod +x .git/hooks/pre-commit");
|
||
let before = git_out(&dir, &["rev-parse", "HEAD"]);
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
match h.run_once() {
|
||
Err(HarnessError::Ship(msg)) => assert!(msg.contains("git commit"), "{msg}"),
|
||
other => panic!("a rejected commit must not ship: {:?}", other.map(|r| (r.shipped, r.branch))),
|
||
}
|
||
assert_eq!(git_out(&dir, &["rev-parse", "HEAD"]), before, "nothing was committed");
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// When the fix's branch already exists, the harness must not commit the
|
||
/// fix onto whatever branch happens to be checked out.
|
||
#[test]
|
||
fn a_fix_never_lands_on_the_current_branch_when_its_own_branch_exists() {
|
||
let dir = scratch_crate("branch-exists");
|
||
let before = git_out(&dir, &["rev-parse", "HEAD"]);
|
||
let current = git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]);
|
||
git_out(&dir, &["branch", &format!("joule-fix/{}", &before[..12])]);
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
match h.run_once() {
|
||
Err(HarnessError::Ship(msg)) => assert!(msg.contains("checkout -b"), "{msg}"),
|
||
other => panic!("an existing branch must stop the ship: {:?}", other.map(|r| (r.shipped, r.branch))),
|
||
}
|
||
assert_eq!(git_out(&dir, &["rev-parse", "--abbrev-ref", "HEAD"]), current);
|
||
assert_eq!(git_out(&dir, &["rev-parse", "HEAD"]), before, "the fix was committed onto {current}");
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// One metered cargo window, as `run_attributed` reports it.
|
||
fn window(soc_cpu_uj: u64, attributed_uj: u64, attributed: bool) -> Attribution {
|
||
let source = if attributed { "ioreport-energy-model" } else { "estimator" };
|
||
window_read_by(soc_cpu_uj, attributed_uj, attributed, source)
|
||
}
|
||
|
||
/// [`window`], its figure read by the probe named `source`.
|
||
fn window_read_by(soc_cpu_uj: u64, attributed_uj: u64, attributed: bool, source: &'static str) -> Attribution {
|
||
Attribution {
|
||
soc_cpu_uj,
|
||
attributed_uj,
|
||
proc_cpu_secs: 1.0,
|
||
busy_cpu_secs: if attributed_uj > 0 { 4.0 } else { 0.0 },
|
||
share: if attributed_uj > 0 { 0.25 } else { 0.0 },
|
||
wall: Duration::from_secs(1),
|
||
attributed,
|
||
// cargo runs its work in descendants: never a per-child reading.
|
||
child_energy_uj: None,
|
||
source,
|
||
}
|
||
}
|
||
|
||
/// An attributed run's meter source names the probes its windows were read
|
||
/// by, as the meter reported them — never a counter it did not read.
|
||
#[test]
|
||
fn an_attributed_run_names_the_probes_that_read_it() {
|
||
let mut t = EnergyTally::default();
|
||
t.add(&window_read_by(10_000_000, 2_500_000, true, "rapl-powercap"));
|
||
t.add(&window_read_by(30_000_000, 7_500_000, true, "rapl-powercap"));
|
||
assert!(t.attributed());
|
||
let source = t.source(&["rapl-powercap", "nvml-total-energy"]);
|
||
assert_eq!(source, "attributed(ModelBased over rapl-powercap HwShunt)");
|
||
assert!(!source.contains("IOReport"), "{source}");
|
||
|
||
t.add(&window_read_by(10_000_000, 2_500_000, true, "composite"));
|
||
assert_eq!(t.source(&[]), "attributed(ModelBased over composite+rapl-powercap HwShunt)");
|
||
|
||
// An estimate names the meter's sources, not any window's.
|
||
let mut est = EnergyTally::default();
|
||
est.add(&window(20_000_000, 0, false));
|
||
assert!(est.source(&["ioreport-energy-model"]).starts_with("estimated(Unaccounted)"));
|
||
assert!(est.source(&[]).contains("no live energy counter"));
|
||
}
|
||
|
||
/// A run whose windows were estimated is sealed as an estimate, and never
|
||
/// as an apportioned zero. This is every macOS 27.0.1 host checked, where
|
||
/// the meter has no live CPU counter. main sealed 0 J `ModelBased` there,
|
||
/// and the core fix alone still sealed the apportioned estimate
|
||
/// `ModelBased` in the meter envelope, and 0 J whenever the tick counters
|
||
/// missed every window.
|
||
#[test]
|
||
fn an_unattributed_run_is_sealed_as_an_estimate_never_an_apportioned_zero() {
|
||
let mut t = EnergyTally::default();
|
||
// The machine tick counters missed this window: share 0.
|
||
t.add(&window(20_000_000, 0, false));
|
||
t.add(&window(40_000_000, 10_000_000, false));
|
||
assert!(!t.attributed());
|
||
assert_eq!(t.figure_uj(), 60_000_000, "the unapportioned estimate");
|
||
assert_eq!(t.energy_class(), EnergyClass::Unaccounted);
|
||
let records = t.meter_records();
|
||
assert_eq!(records.len(), 1, "cargo windows are the CPU's alone: {records:?}");
|
||
let r = &records[0];
|
||
assert_eq!(r.provenance, sandbox_meter::Provenance::Estimator);
|
||
assert_eq!((r.measured_uj, r.estimated_uj), (None, 60_000_000));
|
||
r.check_provenance().unwrap();
|
||
|
||
// Even when every window's share was lost, the run is not free.
|
||
let mut missed = EnergyTally::default();
|
||
missed.add(&window(20_000_000, 0, false));
|
||
assert_eq!(missed.figure_uj(), 20_000_000);
|
||
}
|
||
|
||
/// Each run on a Harness seals its own cargo windows only. The tally a
|
||
/// run leaves behind (here with a stale window added on top, so the
|
||
/// assertion does not depend on run 1's figure) never reaches the next
|
||
/// run's figure, grade or receipts.
|
||
#[test]
|
||
fn a_second_run_seals_only_its_own_cargo_windows() {
|
||
const STALE_UJ: u64 = 1_000_000_000_000_000; // 1 GJ: no scratch run comes near it
|
||
let dir = scratch_crate("rerun");
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
let first = h.run_once().unwrap();
|
||
assert!(first.shipped, "gates: {:?}", first.gates);
|
||
{
|
||
// Run 1's windows are still in the tally when run 1 returns.
|
||
let acc = h.meter.borrow();
|
||
assert!(acc.tally.windows > 0, "run 1 metered its cargo calls");
|
||
assert_eq!(acc.tally.soc_uj, first.soc_cpu_uj);
|
||
}
|
||
h.meter.borrow_mut().tally.add(&window(STALE_UJ, STALE_UJ, true));
|
||
|
||
let second = h.run_once().unwrap();
|
||
eprintln!(
|
||
"joule-fix rerun: first soc_cpu_uj={} second soc_cpu_uj={} attributed={} ({})",
|
||
first.soc_cpu_uj, second.soc_cpu_uj, second.attributed, second.meter_source
|
||
);
|
||
assert!(second.soc_cpu_uj < STALE_UJ, "run 2 sealed an earlier run's windows: {} µJ", second.soc_cpu_uj);
|
||
assert!(second.attributed_uj < STALE_UJ, "{}", second.attributed_uj);
|
||
assert!(second.total_uj() > 0, "run 2's own cargo calls ran");
|
||
assert!(second.receipt.joules_spent < STALE_UJ as f64 / 1e6);
|
||
assert_eq!(second.receipt.joules_spent, second.total_uj() as f64 / 1e6);
|
||
let acc = h.meter.borrow();
|
||
assert_eq!(acc.tally.soc_uj, second.soc_cpu_uj, "the tally holds run 2's windows alone");
|
||
assert_eq!(acc.tally.attributed(), second.attributed);
|
||
drop(acc);
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// `ModelBased` only when every window was attributed: one estimated
|
||
/// window makes the sum an estimate. main labelled the run attributed if
|
||
/// any window was, and never reset that between runs.
|
||
#[test]
|
||
fn a_run_is_attributed_only_when_every_window_was() {
|
||
let mut all = EnergyTally::default();
|
||
all.add(&window(10_000_000, 2_500_000, true));
|
||
all.add(&window(30_000_000, 7_500_000, true));
|
||
assert!(all.attributed());
|
||
assert_eq!(all.figure_uj(), 10_000_000, "the apportioned reading");
|
||
assert_eq!(all.energy_class(), EnergyClass::ModelBased);
|
||
let records = all.meter_records();
|
||
assert_eq!(records.len(), 1, "{records:?}");
|
||
assert_eq!((records[0].class, records[0].provenance), (DeviceClass::Cpu, sandbox_meter::Provenance::ModelBased));
|
||
records[0].check_provenance().unwrap();
|
||
|
||
let mut mixed = all;
|
||
mixed.add(&window(20_000_000, 0, false));
|
||
assert!(!mixed.attributed());
|
||
assert_eq!(mixed.figure_uj(), 60_000_000, "the unapportioned estimate");
|
||
assert_eq!(mixed.energy_class(), EnergyClass::Unaccounted);
|
||
assert_eq!(mixed.meter_records()[0].provenance, sandbox_meter::Provenance::Estimator);
|
||
|
||
// Nothing metered is not an attribution either.
|
||
assert!(!EnergyTally::default().attributed());
|
||
}
|
||
|
||
#[test]
|
||
fn l3_fix_passes_the_same_gates() {
|
||
// A finding clippy --fix can NOT auto-fix (approx_constant): L1
|
||
// leaves it, the configured L3 subprocess fixes it, the gates verify.
|
||
let dir = scratch_crate("l3ship");
|
||
std::fs::write(
|
||
dir.join("src/main.rs"),
|
||
"fn main() { let pi = 3.14; println!(\"{}\", pi); }\n",
|
||
)
|
||
.unwrap();
|
||
// The mock L3 fixer: a deterministic stand-in at the exact seam a
|
||
// jouleclaw decode binary plugs into.
|
||
let fixer = dir.join("mock-l3.sh");
|
||
std::fs::write(
|
||
&fixer,
|
||
"#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
|
||
'<<<<<<< SEARCH src/main.rs' \
|
||
'fn main() { let pi = 3.14; println!(\"{}\", pi); }' \
|
||
'=======' \
|
||
'fn main() { let pi = std::f64::consts::PI; println!(\"{}\", pi); }' \
|
||
'>>>>>>> REPLACE'\n",
|
||
)
|
||
.unwrap();
|
||
sh(&dir, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");
|
||
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
h.l3_cmd = Some("./mock-l3.sh".into());
|
||
let report = h.run_once().unwrap();
|
||
|
||
assert!(report.findings_before > 0);
|
||
assert!(report.shipped, "gates: {:?}", report.gates);
|
||
assert_eq!(report.findings_after, Some(0));
|
||
assert_eq!(report.receipt.discharge.len(), report.contract.obligations().len());
|
||
// The op records the stochastic tier; the receipt still validates.
|
||
assert!(report.local_claim.contains("JR-1"));
|
||
let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("std::f64::consts::PI"));
|
||
|
||
// The model's window was metered and is in the run's figure. The
|
||
// mock is a shell script that forks `cat`: on a host that reads the
|
||
// model's own process, that reaped `cat` is a gap, so the window is
|
||
// an estimate holding the reading and the machine-wide figure.
|
||
let l3 = report.l3.clone().expect("the L3 window was metered");
|
||
eprintln!("l3 window: {l3:?}; run total {} µJ ({})", report.total_uj(), report.meter_source);
|
||
assert!(l3.machine_uj > 0 && l3.figure_uj >= l3.machine_uj, "{l3:?}");
|
||
assert!(l3.direct_child, "`./mock-l3.sh` is a plain argv");
|
||
assert!(!report.attributed, "an L3 window is never attributed");
|
||
assert!(report.total_uj() >= l3.figure_uj, "{} µJ total < the L3 window's {l3:?}", report.total_uj());
|
||
assert!(report.meter_source.contains("L3 model"), "{}", report.meter_source);
|
||
if let Some(read) = l3.process_cpu_uj {
|
||
assert_eq!(l3.figure_uj, read + l3.machine_uj, "{l3:?}");
|
||
assert!(l3.partial_because.iter().any(|w| w.contains("reaped")), "the forked `cat`: {l3:?}");
|
||
assert!(l3.partial_because.iter().any(|w| w.contains("exited")), "the script exited: {l3:?}");
|
||
}
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// The L3 window's grading, pure: a reading of the model's process tree
|
||
/// is never attributed — whatever the gaps, it is an estimate of the
|
||
/// window, the reading plus the machine-wide figure, and it always says
|
||
/// why it is partial; no reading is the machine-wide figure alone.
|
||
#[test]
|
||
fn the_l3_window_is_never_attributed_and_a_reading_is_an_estimate() {
|
||
use sandbox_meter::TreeGap;
|
||
let reading = |cpu_nj: u64, gaps: Vec<TreeGap>| TreeReading {
|
||
cpu_uj: cpu_nj.div_ceil(1_000),
|
||
cpu_nj,
|
||
processes: 1,
|
||
pids: vec![4242],
|
||
wall: Duration::from_secs(2),
|
||
gaps,
|
||
};
|
||
let machine = 40_000_000;
|
||
let cpu = || vec![(DeviceClass::Cpu, machine)];
|
||
|
||
// The shape every model that exits in its window has.
|
||
let exited = grade_l3(Some(&Ok(reading(3_000_000_001, vec![TreeGap::Exited { pid: 4242 }]))), cpu(), true);
|
||
assert_eq!(exited.partial_because, vec![TreeGap::Exited { pid: 4242 }.to_string()]);
|
||
assert_eq!((exited.process_cpu_uj, exited.figure_uj), (Some(3_000_001), 3_000_001 + machine), "rounded up");
|
||
|
||
// No gap seen: the model was not read at its exit. Still an estimate.
|
||
let no_gap = grade_l3(Some(&Ok(reading(3_000_000_000, vec![]))), cpu(), true);
|
||
assert_eq!(no_gap.partial_because, vec![NOT_READ_AT_EXIT.to_string()]);
|
||
assert_eq!(no_gap.figure_uj, 3_000_000 + machine);
|
||
|
||
let gpu = grade_l3(Some(&Ok(reading(5_000, vec![TreeGap::Exited { pid: 1 }, TreeGap::Gpu { ns: 9 }]))), cpu(), false);
|
||
assert_eq!(gpu.partial_because.len(), 2, "{gpu:?}");
|
||
assert_eq!(gpu.figure_uj, 5 + machine);
|
||
assert!(!gpu.direct_child);
|
||
|
||
let no_reading = grade_l3(Some(&Err(TreeError::RootGone { pid: 4242 })), cpu(), true);
|
||
assert_eq!((no_reading.process_cpu_uj, no_reading.figure_uj), (None, machine));
|
||
assert!(no_reading.partial_because[0].contains("no reading"), "{no_reading:?}");
|
||
|
||
let no_meter = grade_l3(None, cpu(), true);
|
||
assert_eq!((no_meter.process_cpu_uj, no_meter.figure_uj), (None, machine));
|
||
assert!(no_meter.partial_because.is_empty());
|
||
|
||
// In the tally: an estimate, as `run_l3` adds it.
|
||
for l3 in [&exited, &no_gap, &no_meter] {
|
||
let mut t = EnergyTally::default();
|
||
t.add_l3(l3);
|
||
assert!(!t.attributed(), "{l3:?}");
|
||
assert_eq!(t.figure_uj(), l3.figure_uj, "{l3:?}");
|
||
assert_eq!(t.energy_class(), EnergyClass::Unaccounted, "never a reading of a partial window");
|
||
}
|
||
}
|
||
|
||
/// The L3 window's machine-wide figure is sealed one record per device
|
||
/// class: a GPU the meter read (an Apple GPU rail, NVML on Linux) is a
|
||
/// `Gpu` record, never folded into the CPU's. The records sum to the
|
||
/// run's figure, and the receipt builds from them.
|
||
#[test]
|
||
fn the_l3_windows_device_classes_are_sealed_apart() {
|
||
use sandbox_meter::TreeGap;
|
||
let reading = TreeReading {
|
||
cpu_uj: 3_000_000,
|
||
cpu_nj: 3_000_000_000,
|
||
processes: 1,
|
||
pids: vec![7],
|
||
wall: Duration::from_secs(1),
|
||
gaps: vec![TreeGap::Exited { pid: 7 }],
|
||
};
|
||
let machine = vec![(DeviceClass::Cpu, 30_000_000), (DeviceClass::Gpu, 10_000_000)];
|
||
let l3 = grade_l3(Some(&Ok(reading)), machine, true);
|
||
assert_eq!((l3.machine_uj, l3.figure_uj), (40_000_000, 43_000_000), "{l3:?}");
|
||
|
||
let mut t = EnergyTally::default();
|
||
t.add(&window(20_000_000, 5_000_000, true));
|
||
t.add_l3(&l3);
|
||
assert_eq!(t.figure_uj(), 63_000_000);
|
||
let records = t.meter_records();
|
||
let by_class: Vec<(DeviceClass, Option<u64>, u64, sandbox_meter::Provenance)> =
|
||
records.iter().map(|r| (r.class, r.measured_uj, r.estimated_uj, r.provenance)).collect();
|
||
let est = sandbox_meter::Provenance::Estimator;
|
||
assert_eq!(
|
||
by_class,
|
||
[(DeviceClass::Cpu, None, 53_000_000, est), (DeviceClass::Gpu, None, 10_000_000, est)],
|
||
"the CPU: the cargo window, the reading and the machine's CPU; the GPU apart"
|
||
);
|
||
let receipt = sandbox_meter::Receipt::build(
|
||
sandbox_schema::ContentId::of_bytes(b"prior"),
|
||
sandbox_schema::Tier::S0,
|
||
records,
|
||
1,
|
||
[3u8; 8],
|
||
)
|
||
.expect("one record per class");
|
||
assert_eq!(receipt.total.estimated_uj, t.figure_uj());
|
||
|
||
// A second L3 window adds to its class's record.
|
||
t.add_l3(&l3);
|
||
assert_eq!(t.meter_records()[1].estimated_uj, 20_000_000);
|
||
assert_eq!(t.meter_records().iter().map(|r| r.estimated_uj).sum::<u64>(), t.figure_uj());
|
||
}
|
||
|
||
/// A plain argv is `exec`ed after the gate, so the model is the meter's
|
||
/// root process; anything that needs the shell runs as its script.
|
||
#[test]
|
||
fn a_plain_l3_command_is_execed_after_the_gate_and_a_shell_command_is_not() {
|
||
let (script, direct) = l3_script(" granite-fix /models/granite-4.0-h_snapshot ");
|
||
assert!(direct);
|
||
assert_eq!(script, "IFS= read -r joule_fix_gate || exit 1\nexec granite-fix /models/granite-4.0-h_snapshot\n");
|
||
assert!(l3_script("./mock-l3.sh").1);
|
||
assert!(l3_script("/bin/model --threads 8 -m a.gguf").1);
|
||
for shell in [
|
||
"model | tee log",
|
||
"model; true",
|
||
"MODEL_THREADS=8 model",
|
||
"model > out",
|
||
"model \"a b\"",
|
||
"model $HOME/x",
|
||
"~/bin/model",
|
||
"model &",
|
||
"",
|
||
] {
|
||
let (script, direct) = l3_script(shell);
|
||
assert!(!direct, "{shell:?}");
|
||
assert!(script.starts_with("IFS= read -r joule_fix_gate || exit 1\n"), "{script}");
|
||
assert!(!script.contains("exec "), "{script}");
|
||
}
|
||
}
|
||
|
||
/// The stand-in model's marker and report, in its working directory (the
|
||
/// scratch workspace).
|
||
const STAND_IN_MARKER: &str = ".l3-stand-in";
|
||
const STAND_IN_REPORT: &str = ".l3-stand-in-report";
|
||
|
||
/// This process's own CPU energy count, nJ: `proc_pid_rusage(getpid(),
|
||
/// RUSAGE_INFO_V6)`'s `ri_energy_nj`, read with a bare buffer of the
|
||
/// struct's 464 bytes at its SDK offset, 336. Written out here, sharing
|
||
/// no code with the meter it checks.
|
||
#[cfg(target_os = "macos")]
|
||
fn own_energy_nj() -> u64 {
|
||
extern "C" {
|
||
fn proc_pid_rusage(pid: i32, flavor: i32, buffer: *mut std::ffi::c_void) -> i32;
|
||
}
|
||
let mut buf = [0u64; 58];
|
||
// SAFETY: `buf` is 464 writable bytes, the size of `rusage_info_v6`.
|
||
let rc = unsafe { proc_pid_rusage(std::process::id() as i32, 6, buf.as_mut_ptr().cast()) };
|
||
assert_eq!(rc, 0, "proc_pid_rusage on this process");
|
||
buf[336 / 8]
|
||
}
|
||
|
||
#[cfg(not(target_os = "macos"))]
|
||
fn own_energy_nj() -> u64 {
|
||
0
|
||
}
|
||
|
||
/// Not a test of its own: the stand-in L3 model, run as a subprocess by
|
||
/// [`the_l3_models_energy_enters_the_run_total_as_its_own_count_says`]
|
||
/// (this test binary, filtered to this test). It reads its prompt to the
|
||
/// end, does a fixed amount of CPU work, leaves the core (which folds its
|
||
/// count), and writes its own count and the prompt's length to its
|
||
/// working directory. Anywhere without its marker it returns at once.
|
||
#[test]
|
||
#[ignore = "a subprocess stand-in, run by the L3 energy test"]
|
||
fn l3_stand_in_model() {
|
||
use std::io::Read;
|
||
let Ok(iterations) = std::fs::read_to_string(STAND_IN_MARKER) else { return };
|
||
let iterations: u64 = iterations.trim().parse().expect("the marker holds an iteration count");
|
||
let mut prompt = Vec::new();
|
||
std::io::stdin().read_to_end(&mut prompt).expect("the prompt");
|
||
let mut x = 1u64;
|
||
for i in 0..iterations {
|
||
x = std::hint::black_box(x.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(i));
|
||
}
|
||
std::thread::sleep(Duration::from_millis(20));
|
||
std::fs::write(STAND_IN_REPORT, format!("{} {} {x}", own_energy_nj(), prompt.len())).expect("the report");
|
||
}
|
||
|
||
/// The L3 model's energy is now in the run's figure. The model here is a
|
||
/// stand-in that burns a fixed amount of CPU and then reports its own
|
||
/// energy count, read from inside it before it exits: the oracle, which
|
||
/// shares no code with the tree meter. Where this host reads the model's
|
||
/// process (macOS, the per-process counter live) the window's reading of
|
||
/// it agrees with that count to within the shell's start-up before the
|
||
/// gate (in the oracle, not the window) and the stand-in's tear-down
|
||
/// after its report (in the window, not the oracle); the window is an
|
||
/// estimate, partial because the model exited in it; and its figure, the
|
||
/// reading plus the machine-wide figure, is what the run's tally holds.
|
||
/// Elsewhere it is the machine-wide figure. Two windows, accumulated.
|
||
#[test]
|
||
fn the_l3_models_energy_enters_the_run_total_as_its_own_count_says() {
|
||
// About a second of one core, unoptimized; a fixed amount of work,
|
||
// however loaded the host.
|
||
const ITERATIONS: u64 = 150_000_000;
|
||
let dir = scratch_crate("l3-energy");
|
||
std::fs::write(dir.join(STAND_IN_MARKER), ITERATIONS.to_string()).unwrap();
|
||
let exe = std::env::current_exe().expect("this test binary");
|
||
let cmd = format!("{} tests::l3_stand_in_model --exact --ignored", exe.display());
|
||
let h = Harness::new(&dir).unwrap();
|
||
let prompt = vec![b'p'; 100_000];
|
||
let reads_processes =
|
||
cfg!(target_os = "macos") && sandbox_meter::process_energy_status() == sandbox_meter::CounterStatus::Live;
|
||
|
||
let mut figures = 0u64;
|
||
for window in 1..=2u64 {
|
||
let reply = h.run_l3(&cmd, &prompt).expect("the stand-in ran");
|
||
assert!(reply.contains("1 passed"), "the stand-in did not run: {reply}");
|
||
let report = std::fs::read_to_string(dir.join(STAND_IN_REPORT)).expect("the stand-in's report");
|
||
let mut fields = report.split_whitespace().map(|f| f.parse::<u64>().unwrap());
|
||
let (oracle_nj, prompt_len) = (fields.next().unwrap(), fields.next().unwrap());
|
||
assert_eq!(prompt_len, prompt.len() as u64, "the model read the whole prompt, and not the gate");
|
||
let acc = h.meter.borrow();
|
||
let l3 = acc.l3.clone().expect("the window was metered");
|
||
eprintln!("l3 window {window}: oracle {oracle_nj} nJ (the model's own count); {l3:?}");
|
||
figures += l3.figure_uj;
|
||
assert_eq!(acc.tally.windows, window);
|
||
assert_eq!(acc.tally.figure_uj(), figures, "the run's figure holds every L3 window");
|
||
assert!(!acc.tally.attributed());
|
||
assert!(l3.machine_uj > 0, "{l3:?}");
|
||
if reads_processes {
|
||
assert!(l3.direct_child, "setup: {cmd} is a plain argv");
|
||
let read = l3.process_cpu_uj.unwrap_or_else(|| panic!("no reading of the model: {l3:?}"));
|
||
let oracle_uj = oracle_nj / 1_000;
|
||
let ratio = read as f64 / oracle_uj as f64;
|
||
assert!(oracle_uj > 100_000, "setup: the stand-in's work read {oracle_uj} µJ");
|
||
assert!((0.8..=1.25).contains(&ratio), "the window read {read} µJ of a model that counted {oracle_uj} µJ");
|
||
assert!(l3.partial_because.iter().any(|w| w.contains("exited")), "{l3:?}");
|
||
assert_eq!(l3.figure_uj, read + l3.machine_uj);
|
||
// CI's macOS energy job greps for this line: the oracle ran.
|
||
eprintln!("l3 model process: window {window} read {read} µJ of a model that counted {oracle_uj} µJ");
|
||
} else {
|
||
assert_eq!((l3.process_cpu_uj, l3.figure_uj), (None, l3.machine_uj), "{l3:?}");
|
||
}
|
||
}
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
#[test]
|
||
fn shipped_l3_fix_induces_a_skill_that_closes_the_recurrence_without_a_model() {
|
||
let store = std::env::temp_dir().join(format!("joule-fix-skills-{}.json", std::process::id()));
|
||
let _ = std::fs::remove_file(&store);
|
||
|
||
// ---- First occurrence: the model (mock) fixes it; skill induced.
|
||
let a = scratch_crate("skill-a");
|
||
std::fs::write(
|
||
a.join("src/main.rs"),
|
||
"fn main() {\n let pi = 3.14;\n println!(\"{}\", pi);\n}\n",
|
||
)
|
||
.unwrap();
|
||
std::fs::write(
|
||
a.join("mock-l3.sh"),
|
||
"#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
|
||
'```rust' \
|
||
'fn main() {' \
|
||
' let pi = std::f64::consts::PI;' \
|
||
' println!(\"{}\", pi);' \
|
||
'}' \
|
||
'```'\n",
|
||
)
|
||
.unwrap();
|
||
sh(&a, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");
|
||
let mut h = Harness::new(&a).unwrap();
|
||
h.skill_store = store.clone();
|
||
h.l3_cmd = Some("./mock-l3.sh".into());
|
||
let first = h.run_once().unwrap();
|
||
assert!(first.shipped, "gates: {:?}", first.gates);
|
||
let stored = SkillStore::load(&store);
|
||
assert_eq!(stored.skills.len(), 1, "the verified fix must induce");
|
||
|
||
// ---- Recurrence, DIFFERENT crate, NO model configured at all: the
|
||
// induced skill closes it deterministically.
|
||
let b = scratch_crate("skill-b");
|
||
std::fs::write(
|
||
b.join("src/main.rs"),
|
||
"fn circumference(r: f64) -> f64 {\n let pi = 3.14;\n 2.0 * pi * r\n}\nfn main() { println!(\"{}\", circumference(1.0)); }\n",
|
||
)
|
||
.unwrap();
|
||
sh(&b, "git add -A && git -c user.email=t@t -c user.name=t commit -qm pi2");
|
||
let mut h2 = Harness::new(&b).unwrap();
|
||
h2.skill_store = store.clone();
|
||
h2.l3_cmd = None; // no model exists here
|
||
let second = h2.run_once().unwrap();
|
||
assert!(second.shipped, "gates: {:?}", second.gates);
|
||
assert_eq!(second.findings_after, Some(0));
|
||
assert!(!second.receipt.discharge[0].obligation.text.is_empty());
|
||
let src = std::fs::read_to_string(b.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("std::f64::consts::PI"));
|
||
assert!(src.contains(" let pi"), "indentation preserved");
|
||
assert_eq!(SkillStore::load(&store).skills[0].hits, 1);
|
||
|
||
let _ = std::fs::remove_file(&store);
|
||
let _ = std::fs::remove_dir_all(&a);
|
||
let _ = std::fs::remove_dir_all(&b);
|
||
}
|
||
|
||
#[test]
|
||
fn l3_garbage_is_caught_by_the_gate_and_reverted() {
|
||
// The mock model emits a build-breaking "fix": the gate must catch
|
||
// it, revert it, and put the refusal on the record. This is the
|
||
// weak-model-made-safe property, tested.
|
||
let dir = scratch_crate("l3refuse");
|
||
std::fs::write(
|
||
dir.join("src/main.rs"),
|
||
"fn main() { let pi = 3.14; println!(\"{}\", pi); }\n",
|
||
)
|
||
.unwrap();
|
||
let fixer = dir.join("mock-l3.sh");
|
||
std::fs::write(
|
||
&fixer,
|
||
"#!/bin/sh\ncat > /dev/null\nprintf '%s\\n' \
|
||
'<<<<<<< SEARCH src/main.rs' \
|
||
'fn main() { let pi = 3.14; println!(\"{}\", pi); }' \
|
||
'=======' \
|
||
'fn main() { this is not rust at all }' \
|
||
'>>>>>>> REPLACE'\n",
|
||
)
|
||
.unwrap();
|
||
sh(&dir, "chmod +x mock-l3.sh && git add -A && git -c user.email=t@t -c user.name=t commit -qm pi");
|
||
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
h.l3_cmd = Some("./mock-l3.sh".into());
|
||
let report = h.run_once().unwrap();
|
||
|
||
assert!(!report.shipped, "broken fix must not ship");
|
||
let build_gate = report.gates.iter().find(|g| g.gate == "build").unwrap();
|
||
assert!(!build_gate.passed);
|
||
// Reverted: the original (lint and all) is back.
|
||
let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("3.14"));
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
#[test]
|
||
fn failed_gate_reverts_and_never_ships() {
|
||
let dir = scratch_crate("refuse");
|
||
// A test that pins the lint: fixing `return 42;` to `42` breaks it.
|
||
std::fs::write(
|
||
dir.join("src/main.rs"),
|
||
r#"fn answer() -> u64 { return 42; }
|
||
fn main() { let x: u64 = answer(); println!("{}", x); }
|
||
#[test]
|
||
fn pins_source_text() {
|
||
// The needle is assembled at runtime so the assert's own text doesn't
|
||
// satisfy it (include_str! includes this test too).
|
||
let src = include_str!("main.rs");
|
||
let needle = ["ret", "urn 42;"].concat();
|
||
assert!(src.contains(&needle), "fix would break this test");
|
||
}
|
||
"#,
|
||
)
|
||
.unwrap();
|
||
sh(&dir, "git add -A && git -c user.email=t@t -c user.name=t commit -qm pin");
|
||
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
let report = h.run_once().unwrap();
|
||
|
||
assert!(!report.shipped, "the pinned test must block shipping");
|
||
assert!(report.branch.is_none());
|
||
let tests_gate = report.gates.iter().find(|g| g.gate == "tests-vs-baseline").unwrap();
|
||
assert!(!tests_gate.passed);
|
||
// The work tree was reverted — the fix is gone.
|
||
let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("return 42;"));
|
||
// And the refusal is on the record: an undischarged obligation.
|
||
assert!(report
|
||
.receipt
|
||
.discharge
|
||
.iter()
|
||
.any(|e| matches!(&e.result, DischargeResult::Undischarged { reason } if reason.contains("tests-vs-baseline"))));
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
/// A `.joule-fix/formal.json` over a netting postcondition (pre=0, post=1,
|
||
/// frame=2): the post is formalized as the SMT goal `net_def`; pre and frame
|
||
/// stay natural language (demoted, never dropped). `net_def` is the `net`
|
||
/// expression — `(- debits credits)` proves, `(+ debits credits)` refutes.
|
||
fn write_formal_spec(dir: &std::path::Path, net_def: &str) {
|
||
use proof_schema::{GoalKind, SpecGrounding};
|
||
let contract = Contract {
|
||
joulecontract: "joulecontract/0.6".into(),
|
||
subject: "scratch netting".into(),
|
||
rigor_target: Rigor::Jr2,
|
||
pre: vec!["debits and credits are integers".into()],
|
||
post: vec!["when debits == credits, the net is zero".into()],
|
||
inv: vec![],
|
||
frame: vec!["the ledger row".into()],
|
||
ceiling: Ceiling {
|
||
enpi_joules: 10.0,
|
||
unit: "joules/settlement".into(),
|
||
enb_ref: ContentAddress::of_bytes(b"enb"),
|
||
derivation: None,
|
||
},
|
||
sector_equivalence: None,
|
||
amends: None,
|
||
};
|
||
let statement = format!(
|
||
"(declare-const debits Int)(declare-const credits Int)(declare-const net Int)\
|
||
(assert (= net {net_def}))(assert (= debits credits))(assert (not (= net 0)))"
|
||
);
|
||
let f = Formalization {
|
||
obligation: 1,
|
||
statement,
|
||
kind: GoalKind::Decidable,
|
||
grounding: SpecGrounding::CrossChecked,
|
||
};
|
||
let spec = serde_json::json!({ "contract": contract, "formalizations": [f] });
|
||
std::fs::create_dir_all(dir.join(".joule-fix")).unwrap();
|
||
std::fs::write(dir.join(".joule-fix/formal.json"), spec.to_string()).unwrap();
|
||
}
|
||
|
||
/// Whether the formal-tier tests run against a real `z3`.
|
||
///
|
||
/// They follow this repo's z3 convention (proof-solvers, joulecontract-
|
||
/// proof, and the standards-build workflow's "Install z3" step): a suite
|
||
/// passes with or without a solver, and asserts something either way.
|
||
/// With `z3` the SMT rung decides the obligation and its verdict is
|
||
/// asserted. Without it the obligation is Unproved, never a fabricated
|
||
/// proof, and the formal gate fails closed, so the fix is reverted — that
|
||
/// is asserted instead. Neither branch returns without asserting, and each
|
||
/// logs which one ran.
|
||
///
|
||
/// Where a solver is supposed to be installed (a CI job that installs z3,
|
||
/// a dev box), set `JOULE_FIX_EXPECT_Z3=1`: a missing `z3` then FAILS
|
||
/// these tests rather than quietly taking the solverless branch.
|
||
fn z3_for_formal_test(test: &str) -> bool {
|
||
let present = proof_solvers::z3_available();
|
||
let expected = std::env::var("JOULE_FIX_EXPECT_Z3").as_deref() == Ok("1");
|
||
assert!(present || !expected, "{test}: JOULE_FIX_EXPECT_Z3=1, but there is no working `z3` on PATH");
|
||
eprintln!(
|
||
"{test}: z3 {}",
|
||
if present { "present, asserting its verdict" } else { "absent, asserting the formal gate fails closed" }
|
||
);
|
||
present
|
||
}
|
||
|
||
/// Without a solver nothing decides the obligation: it is Unproved (not
|
||
/// proved, and not refuted either: there is no counter-model without a
|
||
/// solver), the formal gate fails and says why, and the fix is reverted
|
||
/// although every other gate passed.
|
||
fn assert_the_formal_gate_failed_closed(dir: &std::path::Path, report: &RunReport) {
|
||
let formal = report.formal.as_ref().expect("formal gate ran");
|
||
assert_eq!((formal.proved, formal.refuted, formal.unproved), (0, 0, 1), "{:?}", formal.entries);
|
||
assert!(!formal.all_proved);
|
||
let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
|
||
assert!(!g.passed);
|
||
assert!(g.detail.contains("no z3 on PATH") && !g.detail.contains("real z3"), "{}", g.detail);
|
||
assert!(
|
||
report.gates.iter().filter(|g| g.gate != "formal-proof").all(|g| g.passed),
|
||
"only the undecided proof blocks this fix: {:?}",
|
||
report.gates
|
||
);
|
||
assert!(!report.shipped, "an undecided formal obligation must block shipping");
|
||
let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("return 42;"), "the operational fix was reverted");
|
||
assert!(dir.join(".joule-fix/formal-discharge.json").exists(), "the discharge evidence is written either way");
|
||
}
|
||
|
||
#[test]
|
||
fn a_proven_formal_obligation_lets_the_fix_ship() {
|
||
let z3 = z3_for_formal_test("a_proven_formal_obligation_lets_the_fix_ship");
|
||
let dir = scratch_crate("formal-ok");
|
||
write_formal_spec(&dir, "(- debits credits)"); // the correct postcondition
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
let report = h.run_once().unwrap();
|
||
|
||
if z3 {
|
||
let formal = report.formal.as_ref().expect("formal gate ran");
|
||
assert!(formal.all_proved, "entries: {:?}", formal.entries);
|
||
assert_eq!((formal.proved, formal.refuted, formal.unproved), (1, 0, 0));
|
||
assert!(formal.proof_uj > 0, "the proof attempt was accounted joules");
|
||
let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
|
||
assert!(g.passed);
|
||
assert!(report.shipped, "all gates incl. formal green: {:?}", report.gates);
|
||
// the discharge evidence was written for an auditor
|
||
assert!(dir.join(".joule-fix/formal-discharge.json").exists());
|
||
} else {
|
||
assert_the_formal_gate_failed_closed(&dir, &report);
|
||
}
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
#[test]
|
||
fn a_refuted_formal_obligation_reverts_the_fix() {
|
||
let z3 = z3_for_formal_test("a_refuted_formal_obligation_reverts_the_fix");
|
||
let dir = scratch_crate("formal-refute");
|
||
write_formal_spec(&dir, "(+ debits credits)"); // the BUG: z3 finds a counter-model
|
||
let mut h = Harness::new(&dir).unwrap();
|
||
h.skill_store = dir.join("skills.json");
|
||
let report = h.run_once().unwrap();
|
||
|
||
if z3 {
|
||
let formal = report.formal.as_ref().expect("formal gate ran");
|
||
assert_eq!(formal.refuted, 1, "z3 refuted the false postcondition");
|
||
assert!(!formal.all_proved);
|
||
// the witness rode through from the cascade
|
||
assert!(formal.entries.iter().any(|e| e.verdict == "refuted"));
|
||
let g = report.gates.iter().find(|g| g.gate == "formal-proof").unwrap();
|
||
assert!(!g.passed);
|
||
// a refuted formal obligation reverts the fix exactly like a failed test
|
||
assert!(!report.shipped, "a refuted proof must block shipping");
|
||
let src = std::fs::read_to_string(dir.join("src/main.rs")).unwrap();
|
||
assert!(src.contains("return 42;"), "the operational fix was reverted");
|
||
} else {
|
||
assert_the_formal_gate_failed_closed(&dir, &report);
|
||
}
|
||
|
||
let _ = std::fs::remove_dir_all(&dir);
|
||
}
|
||
|
||
#[test]
|
||
fn the_shipped_formal_template_parses_and_validates() {
|
||
// Guards `formal.example.json` against schema drift: the template we
|
||
// tell users to copy must always deserialize and index validly.
|
||
let path = concat!(env!("CARGO_MANIFEST_DIR"), "/formal.example.json");
|
||
let text = std::fs::read_to_string(path).expect("template present");
|
||
let spec: FormalSpec = serde_json::from_str(&text).expect("template parses");
|
||
assert_eq!(spec.formalizations.len(), 1);
|
||
for f in &spec.formalizations {
|
||
assert!(
|
||
f.obligation < spec.contract.obligations().len(),
|
||
"template formalization indexes a real obligation"
|
||
);
|
||
}
|
||
}
|
||
}
|