From 7597bc5aa98667f1617723f733b4af531f95dd2c Mon Sep 17 00:00:00 2001 From: David Charlot Date: Wed, 26 Aug 2026 08:50:28 -0400 Subject: [PATCH 1/2] =?UTF-8?q?proof:=20give=20the=20cascade=20a=20joule?= =?UTF-8?q?=20ceiling=20(SPEC=20=C2=A75.1)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `grep -rn "ceiling\|budget" proof-rs/crates/**/*.rs` returned nothing. The standard whose entire premise is joules-per-verified-proof could measure joules, attribute them per tier, disclose escalation waste and seal the total — and had no way to say "spend at most this many". That matters because the ladder spans a millionfold: 50 uJ at `Automation`, 50 J at `BigModel`. An unbounded cascade escalates a goal nobody wanted solved that badly straight into the most expensive rung and reports the bill afterwards, which is accounting rather than control. `Router::with_ceiling` refuses to *begin* any rung whose nominal cost would take the run past the ceiling. The check is deliberately on the next rung's cost before it runs: refusing afterwards spends exactly the joules the ceiling exists to withhold, and at T3 that is 50 J of frontier inference for a goal whose owner had declared it was not worth that much. Four distinctions the design turns on: - **A budget halt is not a mathematical verdict.** `proved = false` alone conflates "no rung could decide it" with "we stopped paying", which are different claims about the world — the second says nothing whatever about whether the goal is provable. `halted_at` records the refused tier so a reader cannot mistake an exhausted wallet for a result. - **A budget halt is not a refutation** either, and must not reach the receipt as one. - **Actual spend may exceed the ceiling** when a solver overshoots its nominal cost. Those joules were really spent, so the receipt reports them rather than clamping to the budget: a ceiling bounds what is attempted, not what physics did. `breached_ceiling()` surfaces the gap instead of hiding it. - **A ceiling below the cheapest rung attempts nothing and says so.** That is a coherent request, not an error. The receipt carries `ceiling_uj` when one was declared, which upgrades a proved receipt's claim from "this cost N" to "this was obtained under a declared budget of C and cost N". Omitted when absent, so an unbounded run canonicalizes to exactly the bytes it always did — the published vectors still verify untouched, which C6 asserts directly rather than leaving to trust. Batch accounting counts budget halts separately from failures for the same reason as above: folding them together makes a batch look mathematically harder than it was. Verified: 34 workspace tests pass, conformance passes all 10 classes including the new C6, published vectors unchanged on disk, no new clippy warnings (the two in `meter.rs` are pre-existing and that file is untouched). --- proof/SPEC.md | 33 ++++ .../proof-rs/crates/proof-cascade/src/lib.rs | 165 +++++++++++++++++- .../crates/proof-conformance/src/lib.rs | 62 +++++++ .../proof-rs/crates/proof-receipt/src/lib.rs | 10 ++ 4 files changed, 269 insertions(+), 1 deletion(-) diff --git a/proof/SPEC.md b/proof/SPEC.md index d34476d3c..1231fce2b 100644 --- a/proof/SPEC.md +++ b/proof/SPEC.md @@ -101,6 +101,39 @@ 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. + ## 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..85c8ec484 100644 --- a/proof/proof-rs/crates/proof-cascade/src/lib.rs +++ b/proof/proof-rs/crates/proof-cascade/src/lib.rs @@ -54,9 +54,37 @@ 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 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) + } + + /// 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) @@ -152,13 +180,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 +229,11 @@ 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. + ceiling_uj: self.ceiling_uj, + halted_at: None, total_uj: 0, wasted_uj: 0, baseline_uj, @@ -197,7 +253,20 @@ impl Router { let mut refuted = false; let mut counter_model = None; + 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); @@ -258,6 +327,8 @@ impl Router { from_cache: false, refuted, counter_model, + ceiling_uj: self.ceiling_uj, + halted_at, } } } @@ -275,6 +346,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 +375,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 +479,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-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) } -- 2.54.0 (Apple Git-157) From 0ad7ef9d67a0e8145769f0ac120b494c24901ad5 Mon Sep 17 00:00:00 2001 From: David Charlot Date: Wed, 26 Aug 2026 09:07:18 -0400 Subject: [PATCH 2/2] =?UTF-8?q?proof:=20two=20soundness=20bugs=20that=20we?= =?UTF-8?q?re=20hiding=20each=20other=20(SPEC=20=C2=A75.2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Found by running the shipped ladder on a real statement instead of reading it. Each bug masked the other, so fixing the first exposed the second. **1. Any non-SMT goal was reported as REFUTED.** `Z3Smt` piped `goal.statement` — an arbitrary string — straight into `z3 -in -smt2`. z3 reports a parse failure as `(error "...")` on STDOUT, then answers `(check-sat)` anyway, against an assertion stack that is empty because nothing parsed. That answer is `sat`, and `run_z3` scanned for the first line equal to `sat|unsat|unknown` and skipped the error line entirely. `sat` maps to `Verdict::Refuted`. So "I could not understand the goal" became "the goal is FALSE" — and because a refutation is terminal in this cascade, that was final. Feeding it Goldbach's conjecture returned `refuted: true` with the counter-model `"(\n)"`. Three fixes, because each catches a case the others miss: - an `(error` anywhere in z3's output makes the run undecided, never a verdict; - `Z3Smt` now applies the same `looks_like_smt` shape guard the resident `Z3Server` already had — one call site had simply been missed; - a `sat` becomes a refutation only when a substantive counter-model exists. A script asserting nothing is trivially satisfiable, so `sat` from an empty assertion stack means "no constraints", not "here is a counter-example". The shape guard alone would not catch this: `(check-sat)` is well-formed SMT. Note the stderr redirect was a red herring — z3 writes these errors to stdout. **2. With the false refutation gone, the cascade reaches a rung that proves anything.** `FrontierModel` (T3) returns `Proved` for every goal, and the "artifact" is `ContentId::of_bytes(goal.statement)` — the claim offered as its own evidence. `seal()` gates only on `proved`, so this signs into a JCR-1 receipt that verifies under the steward key. The demonstration is a 438-byte receipt asserting `verdict: "proved", closed_by: "T3"` for Goldbach's conjecture. It is not forged; it is honestly signed and substantively empty, which is worse, because it verifies. Neither existing qualifier catches it: `Provenance` qualifies an attempt's energy, `SpecGrounding` its intent, and neither says whether the verdict was earned. So `Solver::is_reference_stub()` is now declared by all four stand-ins, `CascadeResult::closed_by_stub` records whether the **closing** solver was one, and `require_substantive_proof()` is the relying-party check. The proof cache persists the marker, because a cache hit that dropped it would launder an unearned proof into an unmarked one. `closed_by_stub` is deliberately NOT in the JCR-1 wire yet. Every published vector is generated from the all-stand-in `reference_ladder()` — including an `("open conjecture", Hard)` case sealed as proved at T3 — so encoding it would regenerate the entire conformance corpus. That is a decision about the standard rather than an implementation detail, and it is left open rather than taken quietly. Until it is, the marker is on the result and the check is available. The trait default is "not a stand-in", which is the unsafe direction, and §5.2 says so plainly: it spares real solvers an opt-out, but it makes the declaration a contract on the implementor rather than something the framework can infer. Verified: 38 workspace tests pass (4 new soundness tests pinning both bugs and the cache-laundering path), conformance passes all 10 classes, published vectors unchanged on disk. --- proof/SPEC.md | 34 +++++++ .../proof-rs/crates/proof-cascade/src/lib.rs | 47 +++++++++ .../proof-conformance/tests/soundness.rs | 95 +++++++++++++++++++ proof/proof-rs/crates/proof-schema/src/lib.rs | 16 ++++ .../proof-rs/crates/proof-solvers/src/lib.rs | 67 +++++++++++-- 5 files changed, 251 insertions(+), 8 deletions(-) create mode 100644 proof/proof-rs/crates/proof-conformance/tests/soundness.rs diff --git a/proof/SPEC.md b/proof/SPEC.md index 1231fce2b..24925c2ea 100644 --- a/proof/SPEC.md +++ b/proof/SPEC.md @@ -134,6 +134,40 @@ 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 85c8ec484..585fc767c 100644 --- a/proof/proof-rs/crates/proof-cascade/src/lib.rs +++ b/proof/proof-rs/crates/proof-cascade/src/lib.rs @@ -59,6 +59,18 @@ pub struct CascadeResult { /// 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. /// @@ -80,6 +92,28 @@ impl CascadeResult { 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() @@ -103,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)] @@ -232,6 +274,7 @@ impl Router { // 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, @@ -252,6 +295,7 @@ 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 { @@ -280,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( @@ -289,6 +334,7 @@ impl Router { artifact: art, uj, provenance, + closed_by_stub, }, ); break; @@ -327,6 +373,7 @@ impl Router { from_cache: false, refuted, counter_model, + closed_by_stub, ceiling_uj: self.ceiling_uj, halted_at, } 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-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); -- 2.54.0 (Apple Git-157)