ccbec44ab2
Some checks failed
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 2m24s
standards workspaces build + test / aac-rs (pull_request) Successful in 41s
standards workspaces build + test / joule-code-rs (pull_request) Successful in 45s
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 35s
standards workspaces build + test / map-rs (pull_request) Successful in 33s
standards workspaces build + test / mesh-rs (pull_request) Successful in 33s
standards workspaces build + test / openpay (pull_request) Successful in 2m22s
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Successful in 1m28s
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m50s
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m18s
standards workspaces build + test / proof-rs (pull_request) Successful in 1m15s
standards workspaces build + test / arl-rs (pull_request) Has been cancelled
standards workspaces build + test / joule-ui-rs (pull_request) Has been cancelled
standards workspaces build + test / jouledesk-rs (pull_request) Has been cancelled
standards workspaces build + test / joulehook-rs (pull_request) Has been cancelled
standards workspaces build + test / sense-rs (pull_request) Has been cancelled
standards workspaces build + test / smart-byte-rs (pull_request) Has been cancelled
standards workspaces build + test / macOS energy backend (jcp-energy) (pull_request) Has been cancelled
standards workspaces build + test / sandbox-rs (pull_request) Has been cancelled
The crate description promised "a JouleContract receipt with
hardware-measured joules sealed by a sandbox meter attestation". The crate
does not do that on a host without a live CPU energy counter (every macOS 27
host checked): there its receipts carry an estimate, sealed as JCR-1
`Estimator` / JouleContract `Unaccounted`, as its own module doc says. The
description now says the joules are graded by how they were obtained: a
hardware reading apportioned to the run and anchored to a sealed meter
envelope only where the host exposes a live CPU counter, an estimate sealed
as one everywhere else. Two `FormalEntry`/`FormalOutcome` docs that called
the proof cascade's `ModelBased` accounting "measured joules" are corrected
too.
`a_proven_formal_obligation_lets_the_fix_ship` and
`a_refuted_formal_obligation_reverts_the_fix` returned before asserting
anything when `z3` was absent, so on a solverless host (the joule-code-rs CI
job installs none) they passed in 0.00 s whatever the formal gate did. They
now follow the convention proof-solvers and joulecontract-proof already use,
and that the standards-build workflow's "Install z3" step documents: the
suite passes with or without a solver and asserts something either way. With
`z3` the solver's verdict is asserted as before. Without it, both assert the
gate fails closed: the obligation is Unproved (neither proved nor refuted),
the `formal-proof` gate fails while every other gate passes, the fix is
reverted and not shipped, and the discharge evidence is still written. Each
logs which branch it asserted. Where a solver is supposed to be installed,
`JOULE_FIX_EXPECT_Z3=1` turns a missing `z3` into a test failure instead of
the solverless branch; this is documented on the test helper and in
Cargo.toml beside the proof dependencies. No workflow is changed, so CI
still runs the solverless branch until a job installs z3 and sets the
variable.
The formal gate's detail, which a failed gate copies into its receipt entry,
and joule-fix's summary line both said "real z3" even with no solver on
PATH. They now say "no z3 on PATH: SMT goals left undecided" in that case.
Verified, 13/13 each way: with z3 on PATH; with z3 removed from PATH; with no
git identity (GIT_CONFIG_GLOBAL=/dev/null GIT_CONFIG_NOSYSTEM=1 and
user.useConfigOnly=true); and with no identity and no z3.
`JOULE_FIX_EXPECT_Z3=1` with no z3 fails both tests ("JOULE_FIX_EXPECT_Z3=1,
but there is no working `z3` on PATH"); with z3 present it passes.
Falsified: letting an unproved obligation pass the gate (`all_proved` without
`unproved == 0`) fails both tests with no z3 on PATH. The same mutation
against the previous tests passes both, in 0.00 s. Clippy --no-deps on the
crate is clean.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
40 lines
2.6 KiB
TOML
40 lines
2.6 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" }
|
|
|
|
[[bin]]
|
|
name = "joule-fix"
|
|
path = "src/bin/joule_fix.rs"
|