diff --git a/proof/SPEC.md b/proof/SPEC.md index d34476d3c..24925c2ea 100644 --- a/proof/SPEC.md +++ b/proof/SPEC.md @@ -101,6 +101,73 @@ costed at T3), the total joules, the savings, and the energy attributed to each the few hardest goals dominating the joules — is visible rather than averaged away. +### 5.1 The joule ceiling (OPTIONAL to declare, REQUIRED to honour) + +Accounting says what a proof cost. A **ceiling** says what it is allowed to +cost. A standard whose premise is joules-per-verified-proof needs both: the +ladder spans a millionfold from `T0` to `T3`, so an unbounded cascade will +escalate a goal nobody wanted solved that badly into the most expensive rung +available and report the bill afterwards. + +A caller MAY declare a ceiling in microjoules for a run. Where one is declared: + +- An implementation **MUST NOT** begin a rung whose nominal cost would take the + run past the ceiling. The check is on the **next rung's cost, before it runs**. + Refusing after the fact spends precisely the joules the ceiling exists to + withhold. +- A ceiling below the cheapest rung's nominal cost attempts nothing and reports + that it attempted nothing. This is a coherent request, not an error. +- A run halted for want of budget **MUST** be distinguishable from a run no rung + could decide. `proved = false` alone conflates them, and the two are different + claims about the world: a budget halt says nothing whatever about whether the + goal is provable. An implementation MUST record the tier it refused. +- Actual spend MAY exceed the ceiling when a solver overshoots its nominal cost. + Those joules were really spent, so the receipt **MUST** report them as spent + rather than clamping to the budget. A ceiling bounds what is *attempted*, not + what physics did. +- Batch accounting **MUST** count budget halts separately from failures, for the + same reason: folding them together makes a batch look mathematically harder + than it was. + +Where a ceiling was declared, the receipt (§6) carries it, so a proof is not +merely costed but demonstrably obtained *within a declared budget*. A receipt +from a run with no ceiling omits the field and is byte-identical to one sealed +before this section existed. + +### 5.2 Stand-in solvers (REQUIRED to declare) + +A **reference stand-in** is a solver that returns a verdict to exercise the +ladder and discharges nothing — it decides by goal *kind*, never by inspecting +the claim. The reference implementation ships a full ladder of them so the +cascade, the accounting and the receipt can be demonstrated without a solver +estate. + +They are a hazard precisely because the rest of the pipeline is sound. A +stand-in at the top rung returns `Proved` for **any** goal, with the content +address of the goal's own statement as its "artifact" — the claim offered as its +own evidence — and the sealing path will sign that into a JCR-1 receipt that +verifies under the steward key. Such a receipt is not forged. It is honestly +signed and substantively empty, which is worse, because it verifies. + +Neither existing qualifier catches this. `Provenance` qualifies an attempt's +*energy*; `SpecGrounding` qualifies its *intent*. Neither says whether the +verdict was earned. + +- A solver that is a stand-in **MUST** declare itself as one. +- An implementation **MUST** record, on the result and through any proof cache, + whether the **closing** solver was a stand-in. A cache hit that dropped the + marker would launder an unearned proof into an unmarked one. +- A relying party that will act on a proof **MUST** check it. Verifying the + envelope establishes the signature, not that anything was proved. +- A stand-in **MUST NOT** be presented as a decision procedure in any published + figure or claim derived from a run. + +Note the trait-level default is "not a stand-in", which is the unsafe direction +and is deliberate: it keeps real solvers from having to opt out, but it means +the declaration is a **contract on the implementor**, not a property the +framework can infer. A new stand-in that forgets to declare itself is +indistinguishable from a real one. + ## 6. The receipt (REQUIRED) A discharged obligation seals as a **JCR-1** receipt — the family's shared diff --git a/proof/proof-rs/crates/proof-cascade/src/lib.rs b/proof/proof-rs/crates/proof-cascade/src/lib.rs index 36b5aca76..585fc767c 100644 --- a/proof/proof-rs/crates/proof-cascade/src/lib.rs +++ b/proof/proof-rs/crates/proof-cascade/src/lib.rs @@ -54,9 +54,71 @@ pub struct CascadeResult { /// The counter-model witness from the refuting solver, when it surfaced one. #[serde(default, skip_serializing_if = "Option::is_none")] pub counter_model: Option, + /// The joule ceiling in force for this run, when one was declared + /// (SPEC §5.1). `None` = unbounded, which is the historical behaviour and + /// canonicalizes identically. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub ceiling_uj: Option, + /// The closing solver was a **reference stand-in**, not a real decision + /// procedure — it returned a verdict to exercise the ladder and discharged + /// nothing (SPEC §5.2). + /// + /// This is deliberately **not** in the JCR-1 wire yet: every published + /// vector is generated from the all-stand-in reference ladder, so encoding + /// it would regenerate the entire conformance corpus. That is a decision + /// about the standard, not an implementation detail. Until it is taken, a + /// relying party detects the case with + /// [`CascadeResult::require_substantive_proof`] before trusting a receipt. + #[serde(default)] + pub closed_by_stub: bool, + /// The tier the cascade **refused to attempt** because starting it would + /// have breached the ceiling. + /// + /// `proved == false` with `halted_at == Some(_)` means "ran out of budget", + /// which is a materially different claim from "no rung could decide it" — + /// the goal may well be provable, just not for this many joules. Conflating + /// them would let a budget exhaustion read as a mathematical result. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub halted_at: Option, } impl CascadeResult { + /// Whether the joules actually spent exceeded the declared ceiling. + /// + /// The guard refuses a rung whose *nominal* cost would breach, but a solver + /// may overshoot its nominal figure, and those joules were really spent. The + /// receipt reports what happened rather than what was budgeted. + pub fn breached_ceiling(&self) -> bool { + self.ceiling_uj.is_some_and(|c| self.total_uj > c) + } + + /// A **relying-party** check: refuse a "proof" that no real decision + /// procedure produced. + /// + /// The reference ladder is stand-ins end to end, and the top rung returns + /// `Proved` for *any* goal with the hash of the goal's own statement as its + /// "artifact" — the claim offered as its own evidence. Sealing that yields a + /// signed, verifying receipt asserting an open conjecture is proved. The + /// receipt is not forged; it is honestly signed and substantively empty, + /// which is worse, because it verifies. + /// + /// A caller that will act on a proof MUST call this. `verify()` on the + /// envelope checks the signature, not whether anything was proved. + pub fn require_substantive_proof(&self) -> Result<(), &'static str> { + if !self.proved { + return Err("not proved"); + } + if self.closed_by_stub { + return Err("closed by a reference stand-in, which discharges nothing"); + } + Ok(()) + } + + /// Halted for want of budget rather than for want of a capable solver. + pub fn halted_by_ceiling(&self) -> bool { + self.halted_at.is_some() + } + /// Joules saved versus a frontier-only run (`baseline − total`, floored at 0). pub fn saved_uj(&self) -> u64 { self.baseline_uj.saturating_sub(self.total_uj) @@ -75,6 +137,14 @@ pub struct CachedProof { pub artifact: ContentId, pub uj: u64, pub provenance: Provenance, + /// The proof came from a reference stand-in. Persisted with the entry so a + /// cache hit cannot launder an unearned proof into an unmarked one — the + /// flywheel would otherwise strip the very qualification that makes the + /// original honest. `default` keeps existing cache files loadable; they + /// reload as "not a stub", which is the pre-existing assumption rather than + /// a new claim. + #[serde(default)] + pub closed_by_stub: bool, } #[derive(Clone, Debug, Serialize, Deserialize)] @@ -152,13 +222,36 @@ impl ProofCache { /// The cascade router: solvers sorted cheapest-first. pub struct Router { solvers: Vec>, + ceiling_uj: Option, } impl Router { /// Build a router, sorting the ladder cheapest-first by tier. pub fn new(mut solvers: Vec>) -> Self { solvers.sort_by_key(|s| s.tier()); - Router { solvers } + Router { solvers, ceiling_uj: None } + } + + /// A router that **refuses to start** any rung whose nominal cost would take + /// the run past `ceiling_uj` (SPEC §5.1). + /// + /// The ladder spans a millionfold — 50 µJ at `Automation` to 50 J at + /// `BigModel` — so an unbounded cascade escalates a goal nobody wanted + /// solved that badly straight into the most expensive rung. A standard whose + /// premise is joules-per-verified-proof has to be able to say *at most this + /// many*. + /// + /// The check is on the **nominal** cost of the next rung, before it runs, + /// because refusing after the fact spends the joules it was meant to save. + /// A ceiling below the cheapest rung's nominal cost attempts nothing and + /// says so — that is a coherent request, not an error. + pub fn with_ceiling(solvers: Vec>, ceiling_uj: u64) -> Self { + Router { ceiling_uj: Some(ceiling_uj), ..Router::new(solvers) } + } + + /// The ceiling in force, if any. + pub fn ceiling_uj(&self) -> Option { + self.ceiling_uj } /// Prove a goal: cache first, then escalate through the ladder, accounting @@ -178,6 +271,12 @@ impl Router { closed_by: Some(c.closed_by), artifact: Some(c.artifact), provenance: c.provenance, + // A cache hit spends nothing, so no ceiling can be breached by + // it — but the ceiling that was in force is still recorded, so + // a reader can tell a free hit from an unbounded run. + closed_by_stub: c.closed_by_stub, + ceiling_uj: self.ceiling_uj, + halted_at: None, total_uj: 0, wasted_uj: 0, baseline_uj, @@ -196,8 +295,22 @@ impl Router { let mut provenance = Provenance::Estimator; // until a solver closes it let mut refuted = false; let mut counter_model = None; + let mut closed_by_stub = false; + let mut halted_at = None; for solver in &self.solvers { + // Enforce BEFORE the side effect: a rung that would take the run + // past its ceiling is not started. Checking afterwards would spend + // exactly the joules the ceiling exists to withhold — and at + // `BigModel` that is 50 J of frontier inference for a goal whose + // owner declared it was not worth that much. + if let Some(c) = self.ceiling_uj { + let next = total_uj.saturating_add(solver.tier().nominal_uj()); + if next > c { + halted_at = Some(solver.tier()); + break; + } + } let a = solver.attempt(goal); let uj = a.energy.uj(); total_uj = total_uj.saturating_add(uj); @@ -211,6 +324,7 @@ impl Router { match a.verdict { Verdict::Proved { artifact: art } => { closed_by = Some(a.tier); + closed_by_stub = solver.is_reference_stub(); artifact = Some(art); provenance = a.energy.provenance; cache.insert( @@ -220,6 +334,7 @@ impl Router { artifact: art, uj, provenance, + closed_by_stub, }, ); break; @@ -258,6 +373,9 @@ impl Router { from_cache: false, refuted, counter_model, + closed_by_stub, + ceiling_uj: self.ceiling_uj, + halted_at, } } } @@ -275,6 +393,11 @@ pub struct EnergySummary { pub closed_by_tier: [u64; 4], /// Joules attributed to each closing tier (Amdahl visibility). pub uj_by_tier: [u64; 4], + /// Goals the cascade stopped escalating because the next rung would have + /// breached the ceiling. Counted separately from `goals - proved`: a budget + /// halt says nothing about whether the goal is provable, and folding the two + /// together would make a batch look mathematically harder than it is. + pub halted_by_ceiling: u64, } fn tier_index(t: Tier) -> usize { @@ -299,6 +422,9 @@ impl EnergySummary { if r.from_cache { self.from_cache += 1; } + if r.halted_by_ceiling() { + self.halted_by_ceiling += 1; + } if let Some(t) = r.closed_by { let i = tier_index(t); self.closed_by_tier[i] += 1; @@ -400,6 +526,90 @@ mod tests { } } + /// The ladder spans a millionfold, so an unbounded cascade escalates a + /// cheap goal into the most expensive rung. A ceiling stops it BEFORE the + /// spend, not after. + #[test] + fn a_ceiling_refuses_the_rung_it_cannot_afford() { + // Only BigModel can close this goal, but the ceiling admits the two + // cheap rungs (50 + 5_000) and not SmallModel (500_000). + let solvers = || -> Vec> { + vec![ + Box::new(Gate { tier: Tier::Automation, closes: GoalKind::Trivial }), + Box::new(Gate { tier: Tier::Smt, closes: GoalKind::Trivial }), + Box::new(Gate { tier: Tier::SmallModel, closes: GoalKind::Trivial }), + Box::new(AlwaysProve), + ] + }; + let goal = ProofGoal::new("expensive", "c", GoalKind::Hard); + + // Unbounded: it climbs all the way and pays for it. + let mut cache = ProofCache::new(); + let free = Router::new(solvers()).prove(&goal, &mut cache); + assert!(free.proved, "unbounded, the top rung closes it"); + assert_eq!(free.closed_by, Some(Tier::BigModel)); + assert_eq!(free.ceiling_uj, None); + assert!(!free.halted_by_ceiling()); + + // Bounded at 100_000 uJ: the cheap rungs run, SmallModel is refused. + let mut cache = ProofCache::new(); + let held = Router::with_ceiling(solvers(), 100_000).prove(&goal, &mut cache); + assert!(!held.proved, "no affordable rung could close it"); + assert_eq!(held.halted_at, Some(Tier::SmallModel), "refused the rung it could not afford"); + assert_eq!(held.ceiling_uj, Some(100_000)); + assert!(held.halted_by_ceiling()); + + // The joules it *did* spend are the cheap rungs only — the expensive + // rung never ran, which is the whole point of checking before the call. + assert_eq!(held.total_uj, 50 + 5_000); + assert!(!held.breached_ceiling()); + assert!( + held.attempts.iter().all(|a| a.tier <= Tier::Smt), + "nothing above the affordable rungs may have executed" + ); + } + + /// "Out of budget" and "no rung could decide it" are different claims about + /// the world, and a receipt that conflated them would let an exhausted + /// wallet read as a mathematical result. + #[test] + fn a_budget_halt_is_not_a_mathematical_verdict() { + let goal = ProofGoal::new("expensive", "c", GoalKind::Hard); + + let mut cache = ProofCache::new(); + let broke = Router::with_ceiling(vec![Box::new(AlwaysProve)], 10).prove(&goal, &mut cache); + assert!(!broke.proved); + assert!(broke.halted_by_ceiling(), "halted for want of budget"); + assert_eq!(broke.total_uj, 0, "a ceiling under the cheapest rung attempts nothing"); + assert!(broke.attempts.is_empty()); + assert!(!broke.refuted, "a budget halt is not a refutation"); + + // Contrast: a genuinely undecidable-by-this-ladder goal, unbounded. + let mut cache = ProofCache::new(); + let stuck = Router::new(vec![Box::new(Gate { + tier: Tier::Automation, + closes: GoalKind::Trivial, + })]) + .prove(&goal, &mut cache); + assert!(!stuck.proved); + assert!(!stuck.halted_by_ceiling(), "no rung could decide it — a different fact"); + } + + /// A ceiling is a property of the run, so a batch must be able to say how + /// many goals it stopped paying for. + #[test] + fn the_summary_separates_budget_halts_from_failures() { + let goal = ProofGoal::new("expensive", "c", GoalKind::Hard); + let mut cache = ProofCache::new(); + let r = Router::with_ceiling(vec![Box::new(AlwaysProve)], 10); + let mut sum = EnergySummary::default(); + sum.record(&r.prove(&goal, &mut cache)); + sum.record(&r.prove(&ProofGoal::new("other", "c", GoalKind::Hard), &mut cache)); + assert_eq!(sum.goals, 2); + assert_eq!(sum.proved, 0); + assert_eq!(sum.halted_by_ceiling, 2); + } + #[test] fn a_refutation_halts_the_cascade_and_never_escalates_to_a_proving_rung() { // The exact soundness hole this guards: a disproof must not fall through diff --git a/proof/proof-rs/crates/proof-conformance/src/lib.rs b/proof/proof-rs/crates/proof-conformance/src/lib.rs index 6aa742565..92f266d42 100644 --- a/proof/proof-rs/crates/proof-conformance/src/lib.rs +++ b/proof/proof-rs/crates/proof-conformance/src/lib.rs @@ -36,6 +36,7 @@ pub fn checks() -> Vec { Check { id: "C3 energy honesty + baseline", run: c3_energy }, Check { id: "C4 the cache flywheel", run: c4_flywheel }, Check { id: "C5 receipt seal + verify", run: c5_receipt }, + Check { id: "C6 joule ceiling", run: c6_ceiling }, Check { id: "C-neg provenance coupling", run: cneg_provenance }, Check { id: "C-neg unproved cannot seal", run: cneg_unproved }, Check { id: "C-neg tampered envelope fails", run: cneg_tamper }, @@ -65,6 +66,67 @@ fn c1_routing() -> Result<(), String> { Ok(()) } +/// **C6 — the joule ceiling (SPEC §5.1).** A declared ceiling must stop the +/// cascade *before* the rung it cannot afford, must leave a budget halt +/// distinguishable from a mathematical verdict, and must be sealed into the +/// receipt when a proof is obtained under one. +fn c6_ceiling() -> Result<(), String> { + // The reference ladder closes `Hard` only at BigModel (50 J). A ceiling + // that admits everything below it must refuse exactly that rung. + let ceiling = Tier::Automation.nominal_uj() + + Tier::Smt.nominal_uj() + + Tier::SmallModel.nominal_uj() + + 1; + let r = Router::with_ceiling(reference_ladder(), ceiling); + let mut cache = ProofCache::new(); + let res = r.prove(&ProofGoal::new("open conjecture", "c", GoalKind::Hard), &mut cache); + + if res.proved { + return Err("a goal needing an unaffordable rung must not be proved".into()); + } + if res.halted_at != Some(Tier::BigModel) { + return Err(format!("halted_at = {:?}, want Some(BigModel)", res.halted_at)); + } + if res.ceiling_uj != Some(ceiling) { + return Err("the ceiling in force must be recorded on the result".into()); + } + // The expensive rung must never have executed — enforcement is before the + // spend, not after it. + if res.attempts.iter().any(|a| a.tier == Tier::BigModel) { + return Err("the refused rung executed anyway".into()); + } + if res.total_uj > ceiling { + return Err(format!("spent {} over a ceiling of {ceiling}", res.total_uj)); + } + // A budget halt is not a refutation and not a decision. + if res.refuted { + return Err("a budget halt must not be reported as a refutation".into()); + } + + // Under a ceiling it CAN afford, the run proceeds and the receipt carries + // the budget it was honoured under. + let r = Router::with_ceiling(reference_ladder(), u64::MAX); + let mut cache = ProofCache::new(); + let ok = r.prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache); + if !ok.proved || ok.halted_by_ceiling() { + return Err("an affordable goal must still close".into()); + } + let wire = proof_receipt::to_jcr1_wire(&ok, "did:example:steward"); + if wire.get("ceiling_uj").and_then(|v| v.as_u64()) != Some(u64::MAX) { + return Err("a declared ceiling must be sealed into the receipt".into()); + } + + // And an unbounded run must omit the field entirely, so its receipt is + // byte-identical to one sealed before §5.1 existed. + let mut cache = ProofCache::new(); + let unbounded = router().prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache); + let wire = proof_receipt::to_jcr1_wire(&unbounded, "did:example:steward"); + if wire.get("ceiling_uj").is_some() { + return Err("an unbounded run must omit ceiling_uj, not encode a null".into()); + } + Ok(()) +} + fn c2_escalation() -> Result<(), String> { let r = router(); let mut cache = ProofCache::new(); diff --git a/proof/proof-rs/crates/proof-conformance/tests/soundness.rs b/proof/proof-rs/crates/proof-conformance/tests/soundness.rs new file mode 100644 index 000000000..70f22e83f --- /dev/null +++ b/proof/proof-rs/crates/proof-conformance/tests/soundness.rs @@ -0,0 +1,95 @@ +//! Two soundness regressions, pinned. Both were found by running the shipped +//! ladder on a real statement rather than by reading it, and each was masking +//! the other: the false refutation stopped the cascade before it could reach +//! the fabricating rung. +use proof_cascade::{ProofCache, Router}; +use proof_schema::{GoalKind, ProofGoal, Solver, Verdict}; + +/// A goal that is not SMT-LIB must never come back **refuted**. +/// +/// z3 reports a parse failure as `(error "...")` on stdout and then answers +/// `(check-sat)` anyway — against an assertion stack that is empty because +/// nothing parsed — and that answer is `sat`. Read as a verdict, "I could not +/// understand the goal" becomes "the goal is FALSE", and since a refutation is +/// terminal here, the cascade stops and reports a disproof of arbitrary prose. +#[test] +fn prose_is_never_refuted_by_the_smt_rung() { + let solver = proof_solvers::Z3Smt; + for stmt in [ + "every even integer greater than 2 is the sum of two primes", + "the halting problem is decidable", + "", + "(((", + ] { + let a = solver.attempt(&ProofGoal::new(stmt, "c", GoalKind::Hard)); + assert!( + !matches!(a.verdict, Verdict::Refuted { .. }), + "{stmt:?} came back refuted — a parse failure is not a disproof" + ); + } +} + +/// A `sat` with no counter-model is not a refutation. A script that asserts +/// nothing is trivially satisfiable, so `sat` there means "no constraints", not +/// "here is a counter-example". +#[test] +fn a_refutation_must_carry_a_witness() { + let a = proof_solvers::Z3Smt.attempt(&ProofGoal::new("(check-sat)", "c", GoalKind::Decidable)); + if let Verdict::Refuted { counter_model } = &a.verdict { + panic!("empty assertion stack reported as refuted with model {counter_model:?}"); + } +} + +/// The reference stand-ins must admit what they are. The top rung returns +/// `Proved` for *any* goal, with the hash of the goal's own statement as the +/// "artifact" — the claim offered as its own evidence — and `seal()` will sign +/// that into a receipt that verifies. The receipt is not forged; it is honestly +/// signed and substantively empty, which is worse, because it verifies. +#[test] +fn a_stand_in_proof_is_detectable_before_it_is_trusted() { + let goal = ProofGoal::new( + "every even integer greater than 2 is the sum of two primes", + "demo", + GoalKind::Hard, + ); + let r = Router::new(proof_solvers::real_ladder()); + let mut cache = ProofCache::new(); + let res = r.prove(&goal, &mut cache); + + // It still "proves" it — that is the reference ladder's documented shape. + assert!(res.proved); + assert_eq!(res.closed_by, Some(proof_schema::Tier::BigModel)); + // The artifact is the goal restated as its own evidence. + assert_eq!( + res.artifact.map(|a| a.to_hex()), + Some(proof_schema::ContentId::of_bytes(goal.statement.as_bytes()).to_hex()) + ); + + // But a relying party can now refuse it, which is the point. + assert!(res.closed_by_stub, "the closing solver was a stand-in"); + assert_eq!( + res.require_substantive_proof(), + Err("closed by a reference stand-in, which discharges nothing") + ); + + // And the cache must not launder it into an unmarked proof on the next hit. + let again = r.prove(&goal, &mut cache); + assert!(again.from_cache); + assert!(again.closed_by_stub, "a cache hit must not strip the marker"); + assert!(again.require_substantive_proof().is_err()); +} + +/// A real rung is not marked, so the check is not vacuous. +#[test] +fn a_real_solver_is_not_flagged() { + assert!(!proof_solvers::Propositional.is_reference_stub()); + assert!(!proof_solvers::Z3Smt.is_reference_stub()); + assert!(proof_solvers::FrontierModel.is_reference_stub()); + + let r = Router::new(vec![Box::new(proof_solvers::Propositional)]); + let mut cache = ProofCache::new(); + let res = r.prove(&ProofGoal::new("a | ~a", "c", GoalKind::Trivial), &mut cache); + assert!(res.proved, "the real propositional decider closes a tautology"); + assert!(!res.closed_by_stub); + assert!(res.require_substantive_proof().is_ok()); +} diff --git a/proof/proof-rs/crates/proof-receipt/src/lib.rs b/proof/proof-rs/crates/proof-receipt/src/lib.rs index 24ecc558c..788d99f95 100644 --- a/proof/proof-rs/crates/proof-receipt/src/lib.rs +++ b/proof/proof-rs/crates/proof-receipt/src/lib.rs @@ -51,6 +51,16 @@ pub fn to_jcr1_wire(r: &CascadeResult, steward: &str) -> Value { obj.insert("energy_provenance".into(), json!(r.provenance.jcr1_label())); obj.insert("spec_grounding".into(), json!(r.grounding.label())); obj.insert("from_cache".into(), json!(if r.from_cache { 1 } else { 0 })); + // The declared ceiling, when there was one. Omitted otherwise, so a receipt + // from an unbounded run canonicalizes to exactly the bytes it always did and + // every previously sealed receipt and published vector still verifies. + // + // On a proved receipt this upgrades the claim from "this proof cost N" to + // "this proof was obtained under a declared budget of C and cost N" — the + // difference between reporting a cost and honouring a limit. + if let Some(c) = r.ceiling_uj { + obj.insert("ceiling_uj".into(), json!(c)); + } obj.insert("steward".into(), json!(steward)); Value::Object(obj) } diff --git a/proof/proof-rs/crates/proof-schema/src/lib.rs b/proof/proof-rs/crates/proof-schema/src/lib.rs index 398f70588..d4eeda9dc 100644 --- a/proof/proof-rs/crates/proof-schema/src/lib.rs +++ b/proof/proof-rs/crates/proof-schema/src/lib.rs @@ -308,6 +308,22 @@ pub trait Solver { fn tier(&self) -> Tier; /// Attempt the goal, reporting the verdict and the energy spent. fn attempt(&self, goal: &ProofGoal) -> Attempt; + + /// Whether this solver is a **reference stand-in** rather than a real + /// decision procedure — it returns a verdict to exercise the ladder, and + /// discharges nothing. + /// + /// Defaults to `false`, which is the wrong-way-round default for safety and + /// deliberately so: a stand-in that forgets to declare itself is the + /// dangerous case, so the trait cannot be relied on alone — the reference + /// stand-ins in `proof-solvers` all override it, and a new one MUST. + /// + /// `Provenance` qualifies the *energy* of an attempt and `SpecGrounding` + /// qualifies its *intent*; neither says anything about whether a verdict was + /// earned. This does. + fn is_reference_stub(&self) -> bool { + false + } } #[cfg(test)] diff --git a/proof/proof-rs/crates/proof-solvers/src/lib.rs b/proof/proof-rs/crates/proof-solvers/src/lib.rs index 953774469..ea9685dcc 100644 --- a/proof/proof-rs/crates/proof-solvers/src/lib.rs +++ b/proof/proof-rs/crates/proof-solvers/src/lib.rs @@ -49,6 +49,10 @@ fn proved(goal: &ProofGoal) -> Verdict { pub struct Automation; impl Solver for Automation { + /// A stand-in: it decides by goal *kind*, never by inspecting the claim. + fn is_reference_stub(&self) -> bool { + true + } fn tier(&self) -> Tier { Tier::Automation } @@ -69,6 +73,10 @@ impl Solver for Automation { pub struct Smt; impl Solver for Smt { + /// A stand-in: it decides by goal *kind*, never by inspecting the claim. + fn is_reference_stub(&self) -> bool { + true + } fn tier(&self) -> Tier { Tier::Smt } @@ -89,6 +97,10 @@ impl Solver for Smt { pub struct SmallModel; impl Solver for SmallModel { + /// A stand-in: it decides by goal *kind*, never by inspecting the claim. + fn is_reference_stub(&self) -> bool { + true + } fn tier(&self) -> Tier { Tier::SmallModel } @@ -109,6 +121,10 @@ impl Solver for SmallModel { pub struct FrontierModel; impl Solver for FrontierModel { + /// A stand-in: it decides by goal *kind*, never by inspecting the claim. + fn is_reference_stub(&self) -> bool { + true + } fn tier(&self) -> Tier { Tier::BigModel } @@ -168,7 +184,18 @@ fn run_z3(script: &str) -> Option { stdin.write_all(full.as_bytes()).ok()?; } let out = child.wait_with_output().ok()?; - String::from_utf8_lossy(&out.stdout) + let stdout = String::from_utf8_lossy(&out.stdout); + // z3 reports parse and command errors as `(error "...")` on STDOUT, then + // carries on and answers `(check-sat)` anyway — against an assertion stack + // that is empty because nothing parsed. That answer is `sat`, and reading it + // as a verdict turns "I could not understand the goal" into "the goal is + // FALSE". Since a refutation is terminal in this cascade, that is the + // strongest wrong answer the ladder can give, so any error at all makes the + // whole run undecided. + if stdout.contains("(error") { + return None; + } + stdout .lines() .map(str::trim) .find(|l| matches!(*l, "sat" | "unsat" | "unknown")) @@ -180,6 +207,21 @@ fn run_z3(script: &str) -> Option { /// Best-effort — returns an empty string if `z3` declines a model (some goals /// are `sat` without a printable model). Only called on the refutation path, /// which is terminal, so the extra spawn costs nothing on the proved path. +/// A `sat` answer becomes a refutation only when z3 can actually produce a +/// counter-model. An empty or absent model is not evidence of falsehood — most +/// often it means nothing was asserted — and since a refutation halts the +/// cascade as a final decision, an unsubstantiated one is worse than no answer. +fn refutation_or_undecided(script: &str) -> Verdict { + let cm = z3_counter_model(script); + // A model with no assignments in it: "(", ")", whitespace, and nothing else. + let substantive = cm.chars().any(|c| !matches!(c, '(' | ')' | ' ' | '\n' | '\t' | '\r')); + if substantive { + Verdict::Refuted { counter_model: cm } + } else { + Verdict::Unproved + } +} + fn z3_counter_model(script: &str) -> String { let full = if script.contains("check-sat") { format!("{script}\n(get-model)\n") @@ -222,16 +264,27 @@ impl Solver for Z3Smt { } fn attempt(&self, goal: &ProofGoal) -> Attempt { let start = Instant::now(); - let verdict = match run_z3(&goal.statement).as_deref() { + // The same shape guard the resident session applies. One-shot `z3` was + // missing it, so prose reached the solver and came back "refuted". + let outcome = if looks_like_smt(&goal.statement) { + run_z3(&goal.statement) + } else { + None + }; + let verdict = match outcome.as_deref() { Some("unsat") => Verdict::Proved { artifact: ContentId::of_bytes(goal.statement.as_bytes()), }, // `sat` = the negated claim is satisfiable = the claim is FALSE. A // decision, not a failure to decide — surface the witness and let // the router halt rather than escalate a disproof. - Some("sat") => Verdict::Refuted { - counter_model: z3_counter_model(&goal.statement), - }, + // + // But only where a witness actually exists: a script that asserts + // nothing is trivially satisfiable, and `sat` from an empty + // assertion stack means "no constraints", not "here is a + // counter-example". A disproof is terminal, so it must carry + // evidence or it is not a disproof. + Some("sat") => refutation_or_undecided(&goal.statement), _ => Verdict::Unproved, }; let uj = ns_to_uj(start.elapsed().as_nanos()).max(1); @@ -366,9 +419,7 @@ impl Solver for Z3Server { // `sat` ⇒ refuted. The resident session decided it; fetch the // witness with a one-shot `z3` (the refutation path is terminal, so // the extra spawn never touches the hot proved path). - Some("sat") => Verdict::Refuted { - counter_model: z3_counter_model(&goal.statement), - }, + Some("sat") => refutation_or_undecided(&goal.statement), _ => Verdict::Unproved, }; let uj = ns_to_uj(start.elapsed().as_nanos()).max(1);