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

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
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs
View file

@ -107,7 +107,10 @@ fn postcondition_goal(net_definition: &str) -> String {
} }
/// Discharge the post-condition (obligation index 1: pre=0, post=1, frame=2) /// 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 { fn judge(label: &str, net_definition: &str) -> bool {
let contract = netting_contract(); let contract = netting_contract();
let formalization = Formalization { let formalization = Formalization {
@ -130,8 +133,8 @@ fn judge(label: &str, net_definition: &str) -> bool {
match &entry.status { match &entry.status {
DischargeStatus::Proved(result) => { DischargeStatus::Proved(result) => {
println!( println!(
" PROVED by {:?} — postcondition holds for all integers ({} µJ measured)", " PROVED by {:?} — postcondition holds for all integers ({} µJ, {:?})",
result.closed_by, result.total_uj result.closed_by, result.total_uj, result.provenance
); );
println!(" → formal gate ACCEPTS this fix."); println!(" → formal gate ACCEPTS this fix.");
true true
@ -147,7 +150,7 @@ fn judge(label: &str, net_definition: &str) -> bool {
} else { } else {
"no decision procedure available to decide it (z3 absent)" "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)."); println!(" → formal gate REFUSES this fix (it would be reverted, never shipped).");
false false
} }