e2e4394eae
l3_pass ran the L3 command under no meter at all, so RunReport::total_uj, uj_per_verified_fix and both receipts omitted the model's energy: the most expensive tier of a run was the one the figure left out. The command now runs under sh, which waits for a gate line and then execs a plain argv, so the model is the very process a TreeMeter is rooted at and the shell's start-up stays outside the window. The tree meter reads it at rest, the machine-wide span opens, the gate and prompt are written, stdout is drained, the child is waited for with WNOWAIT and the tree span stopped on its exited record, then it is reaped. grade_l3 is the one place the window is graded: attributed only for a whole reading of a command the operator declared self-contained (JOULE_FIX_L3_SELF_CONTAINED, the gateway's rule); any partial reading - every model that exits in its window has the Exited gap - is an estimate, the reading plus the machine-wide figure (mesh's ProcessMeter rule), never a hardware figure of the whole; no reading (Linux, counter not live) is the machine-wide figure as a cargo window's. JCR-1 DeviceEnergy and JouleContract EnergyClass carry no coverage, so a partial window grades the run down, never up. RunReport::l3 says what was read and why it is partial. Tested against an oracle sharing no code: a stand-in model (this test binary) reports its own ri_energy_nj from inside; the window read 0.999 of it, twice. Co-Authored-By: Claude Opus 5.5 <[email protected]>
45 lines
2.8 KiB
TOML
45 lines
2.8 KiB
TOML
[package]
|
|
name = "joule-code-remediate"
|
|
description = "The reference verified-fix harness: scan a Rust workspace, remediate at the cheapest sufficient cascade tier (L1 lawful codemods first), gate every fix behind a verification pipeline whose stages ARE the contract obligations, and emit a JouleContract receipt whose joules are graded by how they were obtained: a hardware reading apportioned to the run and anchored to a sealed sandbox meter envelope only where the host exposes a live CPU energy counter, an estimate sealed as one everywhere else. A fix that fails its gate is reverted, never shipped."
|
|
version.workspace = true
|
|
edition.workspace = true
|
|
license.workspace = true
|
|
repository.workspace = true
|
|
rust-version.workspace = true
|
|
|
|
[dependencies]
|
|
joule-code-schema = { workspace = true }
|
|
joule-code-cargo = { workspace = true }
|
|
joule-code-joulecontract = { path = "../joule-code-joulecontract" }
|
|
joulecontract-schema = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-schema" }
|
|
joulecontract-receipt = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-receipt" }
|
|
joulecontract-wire = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-wire" }
|
|
sandbox-meter = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-meter" }
|
|
sandbox-schema = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-schema" }
|
|
ed25519-dalek = { workspace = true }
|
|
serde = { workspace = true }
|
|
serde_json = { workspace = true }
|
|
thiserror = { workspace = true }
|
|
|
|
# The formally-verified fix tier (SPEC: the rung above build+test). When a run
|
|
# carries a formalization (`.joule-fix/formal.json`), the harness discharges the
|
|
# fix's formal obligations through the joulecontract→proof vericoding bridge over
|
|
# a real `z3`, and a refuted/unproved obligation reverts the fix like any other
|
|
# failed gate. Decision-procedure ladder only — a formal gate must never fall
|
|
# through to a model stand-in (see `examples/formal_fix.rs`). Without `z3` on
|
|
# PATH an SMT obligation is Unproved and the gate fails closed; the formal-tier
|
|
# tests assert that branch on a solverless host, and `JOULE_FIX_EXPECT_Z3=1`
|
|
# makes a missing `z3` fail them instead (set it wherever z3 is installed).
|
|
joulecontract-proof = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-proof" }
|
|
proof-cascade = { path = "../../../../proof/proof-rs/crates/proof-cascade" }
|
|
proof-solvers = { path = "../../../../proof/proof-rs/crates/proof-solvers" }
|
|
proof-schema = { path = "../../../../proof/proof-rs/crates/proof-schema" }
|
|
|
|
# macOS: the L3 model's process is waited for without being reaped
|
|
# (`waitid` with `WNOWAIT`), so the tree meter reads its exited count.
|
|
[target.'cfg(target_os = "macos")'.dependencies]
|
|
libc = "0.2"
|
|
|
|
[[bin]]
|
|
name = "joule-fix"
|
|
path = "src/bin/joule_fix.rs"
|