5cec3a0fbd
The vericoding seam existed but had only ever closed propositional
tautologies (p | !p) in tests — which proves the plumbing, not the claim.
This makes the claim real:
- a z3-gated integration test discharges a genuine arithmetic postcondition
("if debits equal credits, the net settlement is zero") encoded as an
SMT-LIB2 goal whose negation z3 finds unsat — i.e. the property holds for
all integers. It closes at the SMT tier with real measured joules; the
pre/frame obligations, having no formalization, stay Unformalized (demoted,
never faked). Where z3 is absent the obligation shows Unproved, never a
fabricated pass — the standard's honesty rule holds in CI too.
- a runnable example (`cargo run -p joulecontract-proof --example vericode`)
prints the per-obligation ledger end to end: the postcondition PROVED at
the SMT tier with its measured energy, the unformalized obligations honestly
marked, and discharged=false because the whole contract isn't proved. This
is the artifact the "45% of AI code fails in production" pitch needs — a
contract clause machine-proved, priced in joules.
6 lib tests (z3-gated test skips cleanly without a solver); example clean;
clippy clean.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
72 lines
3.1 KiB
Rust
72 lines
3.1 KiB
Rust
//! Vericoding a contract, end to end: declare obligations, formalize the ones
|
|
//! that have a formal meaning, discharge them through the JouleProof cascade,
|
|
//! and print the per-obligation ledger with measured joules.
|
|
//!
|
|
//! Run: `cargo run -p joulecontract-proof --example vericode`
|
|
//! (needs `z3` on PATH for the SMT rung; without it the postcondition shows
|
|
//! Unproved rather than a fabricated pass — the standard never fakes a proof.)
|
|
|
|
use joulecontract_proof::{discharge, DischargeStatus, Formalization};
|
|
use joulecontract_schema::{Ceiling, ContentAddress, Contract, Rigor};
|
|
use proof_cascade::{ProofCache, Router};
|
|
use proof_schema::{GoalKind, SpecGrounding};
|
|
use proof_solvers::{real_ladder, z3_available};
|
|
|
|
fn main() {
|
|
// A real unit of work and what it must honor.
|
|
let contract = Contract {
|
|
joulecontract: "joulecontract/0.6".into(),
|
|
subject: "settlement batch writer".into(),
|
|
rigor_target: Rigor::Jr2,
|
|
pre: vec!["the input batch is well-formed".into()],
|
|
post: vec!["if debits equal credits, the net settlement is zero".into()],
|
|
inv: vec![],
|
|
frame: vec!["ledger table".into()],
|
|
ceiling: Ceiling {
|
|
enpi_joules: 10.0,
|
|
unit: "joules/batch".into(),
|
|
enb_ref: ContentAddress::of_bytes(b"enb-2026"),
|
|
derivation: None,
|
|
},
|
|
sector_equivalence: None,
|
|
amends: None,
|
|
};
|
|
|
|
// Formalize the postcondition (index 1: pre=0, post=1, frame=2). Its
|
|
// negation being unsat means the property holds for all integers.
|
|
let post = Formalization {
|
|
obligation: 1,
|
|
statement: "(declare-const debits Int)\n\
|
|
(declare-const credits Int)\n\
|
|
(declare-const net Int)\n\
|
|
(assert (= net (- debits credits)))\n\
|
|
(assert (= debits credits))\n\
|
|
(assert (not (= net 0)))"
|
|
.into(),
|
|
kind: GoalKind::Decidable,
|
|
grounding: SpecGrounding::CrossChecked,
|
|
};
|
|
|
|
let router = Router::new(real_ladder());
|
|
let mut cache = ProofCache::new();
|
|
let report = discharge(&contract, &[post], &router, &mut cache).unwrap();
|
|
|
|
println!("contract: {}", report.contract);
|
|
if !z3_available() {
|
|
println!("(z3 not found on PATH — the SMT obligation will show Unproved, never faked)\n");
|
|
}
|
|
for entry in &report.entries {
|
|
let status = match &entry.status {
|
|
DischargeStatus::Proved(r) => {
|
|
format!("PROVED at {:?} · {} µJ", r.closed_by.unwrap(), r.total_uj)
|
|
}
|
|
DischargeStatus::Unproved(r) => format!("UNPROVED · {} µJ burned", r.total_uj),
|
|
DischargeStatus::Unformalized => "UNFORMALIZED (binds, undischargeable by proof)".into(),
|
|
};
|
|
println!(" [{}] {:?}: {}\n → {}", entry.index, entry.obligation.kind, entry.obligation.text, status);
|
|
}
|
|
println!(
|
|
"\n{} proved · {} unproved · {} unformalized · {} µJ total · discharged={}",
|
|
report.proved, report.unproved, report.unformalized, report.total_uj, report.discharged()
|
|
);
|
|
}
|