From 2e88815b66e0dd46d65e9c2e01b07373d383b8a0 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Wed, 14 Oct 2026 20:01:38 -0400 Subject: [PATCH] joule-code-remediate: formal_fix prints each proof figure with its grade, not as "measured" MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../joule-code-remediate/examples/formal_fix.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs index 545e7e21a..a52a10cbe 100644 --- a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs +++ b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs @@ -107,7 +107,10 @@ fn postcondition_goal(net_definition: &str) -> String { } /// Discharge the post-condition (obligation index 1: pre=0, post=1, frame=2) -/// for one candidate fix, and report the verdict + measured joules. +/// for one candidate fix, and report the verdict and the joules the cascade +/// accounted for it, with their grade. On this ladder that grade is +/// `Estimator` (wall time × proof-solvers' uncalibrated default power), so the +/// figure is printed as an estimate, never as a measurement. fn judge(label: &str, net_definition: &str) -> bool { let contract = netting_contract(); let formalization = Formalization { @@ -130,8 +133,8 @@ fn judge(label: &str, net_definition: &str) -> bool { match &entry.status { DischargeStatus::Proved(result) => { println!( - " PROVED by {:?} — postcondition holds for all integers ({} µJ measured)", - result.closed_by, result.total_uj + " PROVED by {:?} — postcondition holds for all integers ({} µJ, {:?})", + result.closed_by, result.total_uj, result.provenance ); println!(" → formal gate ACCEPTS this fix."); true @@ -147,7 +150,7 @@ fn judge(label: &str, net_definition: &str) -> bool { } else { "no decision procedure available to decide it (z3 absent)" }; - println!(" UNPROVED — {why} ({} µJ measured)", result.total_uj); + println!(" UNPROVED — {why} ({} µJ, {:?})", result.total_uj, result.provenance); println!(" → formal gate REFUSES this fix (it would be reverted, never shipped)."); false } -- 2.54.0 (Apple Git-157)