Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 15 Packages Wiki Activity Actions

joule-code-remediate: formal_fix prints each proof figure with its grade, not as "measured" #261

Merged
dcharlot merged 1 commit from fix/formal-fix-energy-label into main 2026-10-15 01:03:50 -04:00
Conversation 0 Commits 1 Files changed 1 +7 -4
dcharlot commented 2026-10-14 20:01:41 -04:00
Owner
Copy link

What was wrong

joule-code-remediate's formal_fix example printed each candidate's proof energy as "N µJ measured".

That figure is not a reading. On the decision-procedure ladder the example uses, it is wall time × proof-solvers' default power, a figure no host calibrated. CascadeResult grades it Estimator, and the harness's own FormalEntry docs say the same.

The fix

The example now prints the grade the result already carries:

── candidate A (the bug):  net = (+ debits credits)
   UNPROVED — z3 found a counter-model; the postcondition can fail   (590377 µJ, Estimator)
── candidate B (the fix):  net = (- debits credits)
   PROVED   by Some(Smt) — postcondition holds for all integers   (199948 µJ, Estimator)

That output is from a run on the build host with real z3.

How it was found

I searched main for energy figures labelled "measured" that are not readings. This was the only one left. The other hits either print their label according to the grade (energy_probe, l3-jouleclaw), or seal the receipt UNMETERED when the rail is not live (the wai meters).

🤖 Generated with Claude Code

## What was wrong `joule-code-remediate`'s `formal_fix` example printed each candidate's proof energy as "N µJ measured". That figure is not a reading. On the decision-procedure ladder the example uses, it is wall time × proof-solvers' default power, a figure no host calibrated. `CascadeResult` grades it `Estimator`, and the harness's own `FormalEntry` docs say the same. ## The fix The example now prints the grade the result already carries: ``` ── candidate A (the bug): net = (+ debits credits) UNPROVED — z3 found a counter-model; the postcondition can fail (590377 µJ, Estimator) ── candidate B (the fix): net = (- debits credits) PROVED by Some(Smt) — postcondition holds for all integers (199948 µJ, Estimator) ``` That output is from a run on the build host with real z3. ## How it was found I searched main for energy figures labelled "measured" that are not readings. This was the only one left. The other hits either print their label according to the grade (`energy_probe`, `l3-jouleclaw`), or seal the receipt UNMETERED when the rail is not live (the wai meters). 🤖 Generated with [Claude Code](https://claude.com/claude-code)
joule-code-remediate: formal_fix prints each proof figure with its grade, not as "measured"
All checks were successful
repository checks / lockfiles, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 1m2s
Details
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 6s
Details
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 1m39s
Details
standards workspaces build + test / macOS energy backends (pull_request) Successful in 6m14s
Details
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Successful in 2m20s
Details
2e88815b66 
The example printed each candidate's proof energy as "N µJ measured". On
the decision-procedure ladder it runs, that figure is wall time × the
proof-solvers default power, which no host calibrated: CascadeResult grades
it Estimator, and joule-code-remediate's own docs say so. The example now
prints the grade the result carries:

    UNPROVED — z3 found a counter-model ...   (590377 µJ, Estimator)
    PROVED   by Some(Smt) — ...               (199948 µJ, Estimator)

Found by a sweep of main for figures labelled "measured" that are not
readings. It was the only one left. The other hits print the grade
conditionally (energy_probe, l3-jouleclaw) or seal UNMETERED when the rail
is not live (the wai meters).

Co-Authored-By: Claude Opus 5.5 <[email protected]>
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
Transaction-Science/open-standards!261
No description provided.