[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"