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
         }