Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science ccbec44ab2 joule-code-remediate: the description grades its joules, and the z3 tests never pass silently ... 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]>		2026-09-30 20:10:38 -04:00
..
joule_fix.rs	joule-code-remediate: the description grades its joules, and the z3 tests never pass silently	2026-09-30 20:10:38 -04:00