b5cce1b398
The formal tier is now a live gate, not just an example. When a run carries
`<workspace>/.joule-fix/formal.json` (a domain JouleContract + the
Formalizations encoding the obligations the fix must honor), the harness
discharges them through the joulecontract→proof vericoding bridge over a real
z3, as a seventh gate `formal-proof`. A refuted or unproven obligation fails the
gate and reverts the fix exactly like a failed test — the rung above build+test.
- Decision-procedure ladder only ([Propositional, Z3Smt]); a formal gate must
not fall through to a model stand-in.
- The spec is loaded + validated UP FRONT (indices, duplicates), before any
edit, so a malformed spec fails on a clean tree rather than mid-run (which
would otherwise leave the operational fix un-reverted).
- Per-obligation discharge written to .joule-fix/formal-discharge.json as
re-checkable evidence; proof joules reported (ModelBased, in-process) beside
the cargo-attributed gate energy. No formal.json ⇒ no formal gate, run is
identical to before.
Live, both directions, on real z3:
- correct postcondition (net = debits - credits): formal-proof ✓ (proved by
Smt, 0.10 J), all seven gates green, fix ships.
- buggy postcondition (net = debits + credits): all six OPERATIONAL gates
green, but formal-proof ✗ (1 refuted, counter-model debits=credits=1⇒net=2),
fix REVERTED, refusal receipt. An operationally-valid lint fix refused
because its formal claim was disproved.
Two harness tests (proven→ships, refuted→reverts), gated on z3 availability.
Example's soundness note updated (the proof crate now halts on refutation).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
37 lines
2.2 KiB
TOML
37 lines
2.2 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 with hardware-measured joules sealed by a sandbox meter attestation. 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`).
|
|
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"
|