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

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<String>,
+    /// 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<u64>,
+    /// 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<Tier>,
 }
 
 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<Box<dyn Solver>>,
+    ceiling_uj: Option<u64>,
 }
 
 impl Router {
     /// Build a router, sorting the ladder cheapest-first by tier.
     pub fn new(mut solvers: Vec<Box<dyn Solver>>) -> 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<Box<dyn Solver>>, 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<u64> {
+        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<Box<dyn Solver>> {
+            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

proof/proof-rs/crates/proof-conformance/src/lib.rs

@@ -36,6 +36,7 @@ pub fn checks() -> Vec<Check> {
         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();

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());
+}

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)
 }

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)]

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<String> {
         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<String> {
 /// 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);