| Filename | Latest commit message | Latest commit date |
|---|---|---|
2e88815b66
All checks were successful
repository checks / lockfiles, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 1m2s
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 6s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 1m39s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 6m14s
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Successful in 2m20s
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]>
|
||
| .. | ||
| formal_fix.rs | ||