jcp/SPEC.md

@@ -256,16 +256,38 @@ principal. Steering is an issuer power, like revocation (§4.3): an
 **amendment** is a soft revoke that re-bounds the run rather than killing it.
 
 A checkpoint cites the active grant and a content-addressed state commitment,
-signed by the agent. An amendment cites a checkpoint, is signed by the grant's
-issuer, MUST differ from the agent, and MUST only **tighten** — the
-continuation's budget is at most the checkpoint grant's, so steering can never
-escalate a running agent's authority; it MAY also hand the agent a new
-instruction-set commitment. The run resumes under a **continuation grant** the
-issuer re-issues to the same agent with the amended budget, linked back to the
-steered grant. This continuation is an issuer re-binding, not a holder
-delegation — an auditor verifies it alongside the signed checkpoint+amendment
-pair, which together record who intervened, when, and how. Conformance class
-**C21**.
+signed by the agent. It MAY also state what the run has **spent** so far: a
+cumulative microjoule figure with the provenance grade of §5. An amendment
+cites a checkpoint, is signed by the grant's issuer, MUST differ from the
+agent, and MUST only **tighten**; it MAY also hand the agent a new
+instruction-set commitment.
+
+What "tighten" is measured against is normative, and it is the **remainder**,
+not the issued budget:
+
+- Where the checkpoint states its spend, an amendment MUST NOT set a budget
+  above `grant.budget_uj − spent.uj`, saturating at zero. Both the amending
+  side and the verifying side MUST enforce this: an enforcement point handed a
+  signed amendment never calls the amending routine, so a check that lives only
+  there is not a check.
+- Where the checkpoint states no spend, the ceiling is the issued
+  `grant.budget_uj`. This is the weaker rule and is retained so that a
+  checkpoint written before the field existed remains valid; implementations
+  MUST NOT read an absent spend as zero spend, and SHOULD report the remainder
+  as unknown rather than as the full budget.
+- A declared spend is cumulative, so across one run it MUST NOT decrease, and a
+  checkpoint that once stated a spend MUST NOT later omit it. Otherwise an agent
+  recovers its full issued ceiling by going quiet.
+
+The figure is the agent's own signed claim, not an independent measurement; its
+`provenance` grade travels with it so the amender can see which kind of claim it
+is, and a deployment that needs more binds receipts (§5) to the checkpoint.
+
+The run resumes under a **continuation grant** the issuer re-issues to the same
+agent with the amended budget, linked back to the steered grant. This
+continuation is an issuer re-binding, not a holder delegation — an auditor
+verifies it alongside the signed checkpoint+amendment pair, which together
+record who intervened, when, and how. Conformance class **C21**.
 
 ### 4.8 Dual ceilings: a money budget beside the joule budget (OPTIONAL)
 
@@ -740,7 +762,7 @@ enforced budget make the dangerous action unreachable rather than observed.
 Behavioral scoring MAY be layered above as a secondary signal; it is never the
 gate.
 - **C20 — standing grants:** an event-triggered firing mints a strictly-weaker child that traces to the standing grant; the wrong event class, an exhausted firing count, and a firing past the cumulative budget are each refused without advancing the ledger; a policy that would amplify its grant is refused at author time.
-- **C21 — checkpoints + amendments:** an agent checkpoints its own state; only the grant's issuer — a principal distinct from the agent — may amend, only to tighten; an agent steering itself, a non-issuer amending, a widening amendment, and an amendment bound to a different checkpoint are each refused.
+- **C21 — checkpoints + amendments:** an agent checkpoints its own state; only the grant's issuer — a principal distinct from the agent — may amend, only to tighten, and only up to what the grant has **left** at that checkpoint; an agent steering itself, a non-issuer amending, a widening amendment, an amendment above the remainder of a checkpoint that stated its spend, and an amendment bound to a different checkpoint are each refused.
 - **C23 — receipt binds its payload + profile migration:** a `jcp/2` receipt commits the `payload_hash` it decided over; substituting only the payload (same grant, action, and cost) fails verification — the forgery a payload-blind receipt could not detect; and receipts published under `jcp/1` still verify, because the verifier recomputes the preimage under the profile the receipt names rather than assuming one.
 - **C24 — caveats:** a caveat embedded in the grant is enforced offline by the decision point; `PayloadIs` makes a grant one-shot (a replay with different arguments is denied `caveat-unsatisfied`); `MaxCostUj` bounds a single invocation independently of the cumulative budget; a caveat may narrow below the capability; attenuation inherits every parent caveat and refuses to drop one; and a grant with no caveats encodes byte-identically to one minted before they existed.
 - **C22 — dual ceilings:** a money ceiling beside the joule ceiling is enforced independently — the first to bind denies (`funds-exceeded` / `budget-exceeded`), a foreign-currency cost is refused `currency-mismatch` rather than converted, an allow debits both dimensions and a deny debits neither, and an absent money ceiling encodes byte-identically to a joules-only grant (so its content id and signature are unchanged). Attenuation narrows money independently: dropping, raising, or re-denominating a bounded parent's ceiling is refused; a plain attenuation inherits it.

jcp/conformance/v1/standing.json

@@ -8,6 +8,13 @@
     "id_hex": "ab4554898620355d49b9caa9105529533da047c944d9f8b5ab66ea8729aaf3f6",
     "signature_hex": "13a4432a4f615de526b981cb45220936a905ee89a824289396752b9e17a4a90ac7aa3c8bb82bf2f24c93bfe9a74bf1c2c0483174ef1d7f1b2dde7a1a416c4f09"
   },
+  "checkpoint_with_spend": {
+    "grant_budget_uj": 1000,
+    "id_hex": "f15f4226a853f2bb6e026afdf96f45599a29aa8c8e49e0904fc4c6fe115eede0",
+    "remaining_uj": 100,
+    "signature_hex": "a580b2eb89849c5740a4c4772bae6b662a3ade271e22320254647340a9eb45a27073352a7cee1079660a7ef5e93c303b15888a1964f62e3133e007291ca8940a",
+    "spent_uj": 900
+  },
   "continuation_grant": {
     "budget_uj": 400,
     "id_hex": "a901bad46c325834a3f90442cb74bbc0f5e0bd1ba1510de3e7abb749da610ac4",

jcp/jcp-rs/crates/jcp-conformance/src/bin/gen_vectors.rs

@@ -6,9 +6,9 @@
 use ed25519_dalek::SigningKey;
 use jcp_grant::issue;
 use jcp_grant::standing::{issue_policy, mint_on_trigger, MintLedger, TriggerEvent};
-use jcp_grant::checkpoint::{amend, apply_amendment, checkpoint};
+use jcp_grant::checkpoint::{amend, apply_amendment, checkpoint, remaining_uj, Spend};
 use jcp_runtime::{Price, Runtime};
-use jcp_schema::{Capability, ContentId, Did, Energy, Frame, FrameKind, Funds, Grant, Trust};
+use jcp_schema::{Capability, ContentId, Did, Energy, Frame, FrameKind, Funds, Grant, Provenance, Trust};
 
 fn main() {
     let out = std::env::args().nth(1).unwrap_or_else(|| "conformance/v1".to_string());
@@ -104,15 +104,35 @@ fn main() {
         capability: Capability::new(resource, ["read", "write"]),
         budget_uj: 1_000, expiry: 0, parent: None, delegate_depth: None, nonce: [6; 16], budget_funds: None, caveats: Vec::new(),
     }).expect("run grant");
-    let cp = checkpoint(&agent, &run_grant, ContentId::of_bytes(b"state-1"), 0, [7; 16]).expect("cp");
+    let cp = checkpoint(&agent, &run_grant, ContentId::of_bytes(b"state-1"), 0, [7; 16], None).expect("cp");
     let am = amend(&issuer, &run_grant, &cp, 400, Some(ContentId::of_bytes(b"instr")), [8; 16]).expect("amend");
     let cont = apply_amendment(&issuer, &run_grant, &cp, &am).expect("continuation");
 
+    // A second checkpoint that states what the run has already spent. Its
+    // `spent` field is omitted from the signed core when absent, so `checkpoint`
+    // above keeps the id and signature it had before the field existed — the
+    // two entries together pin that the extension is additive. This one pins
+    // the encoding of the field itself, including how `Provenance` is spelled
+    // inside the core. The remainder rule it enables is a refusal, and a
+    // refusal has nothing to sign, so it is pinned by C-checks, not a vector.
+    let spent_cp = checkpoint(
+        &agent, &run_grant, ContentId::of_bytes(b"state-2"), 1, [9; 16],
+        Some(Spend { uj: 900, provenance: Provenance::HwShunt }),
+    ).expect("spent cp");
+
     let standing_vectors = serde_json::json!({
         "standing_grant": {"id_hex": standing.grant.id().to_hex(), "signature_hex": hex::encode(&standing.signature)},
         "mint_policy": {"id_hex": ContentId::of(&policy.policy).unwrap().to_hex(), "signature_hex": hex::encode(&policy.signature)},
         "minted_child": {"id_hex": minted.grant.id().to_hex(), "parent_hex": minted.grant.parent.as_ref().map(|p| p.to_hex()), "budget_uj": minted.grant.budget_uj},
         "checkpoint": {"id_hex": cp.checkpoint.id().to_hex(), "signature_hex": hex::encode(&cp.signature)},
+        "checkpoint_with_spend": {
+            "id_hex": spent_cp.checkpoint.id().to_hex(),
+            "signature_hex": hex::encode(&spent_cp.signature),
+            // The grant's issued budget travels with the entry so a third
+            // party can recompute the remainder instead of taking it on faith.
+            "grant_budget_uj": run_grant.grant.budget_uj,
+            "spent_uj": 900, "remaining_uj": remaining_uj(&run_grant.grant, &spent_cp.checkpoint),
+        },
         "amendment": {"id_hex": am.amendment.id().to_hex(), "signature_hex": hex::encode(&am.signature), "new_budget_uj": am.amendment.new_budget_uj},
         "continuation_grant": {"id_hex": cont.grant.id().to_hex(), "parent_hex": cont.grant.parent.as_ref().map(|p| p.to_hex()), "budget_uj": cont.grant.budget_uj},
     });

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

@@ -31,7 +31,7 @@ use jcp_grant::{attenuate, attenuate_priced, caveats_narrow, issue, revoke, veri
 use jcp_runtime::{Price, Runtime};
 use jcp_schema::{
     canonical_cbor, from_canonical_cbor, Capability, ContentId, DenyReason, Did, Energy, Frame,
-    Caveat, FrameKind, Funds, Grant, SignedGrant, Trust, Verdict,
+    Caveat, FrameKind, Funds, Grant, Provenance, SignedGrant, Trust, Verdict,
 };
 
 /// A single conformance check.
@@ -653,7 +653,7 @@ fn c20_standing() -> Result<(), String> {
 
 
 fn c21_checkpoint() -> Result<(), String> {
-    use jcp_grant::checkpoint::{amend, apply_amendment, checkpoint, verify_amendment, verify_checkpoint, CheckpointError};
+    use jcp_grant::checkpoint::{amend, apply_amendment, checkpoint, remaining_uj, verify_amendment, verify_checkpoint, CheckpointError, Spend};
     // steward issues to a distinct agent.
     let steward = sk(1);
     let agent = sk(2);
@@ -661,7 +661,7 @@ fn c21_checkpoint() -> Result<(), String> {
     let g = grant(&steward, did(&agent), r, &["read", "write"], 1_000, 0);
 
     // The agent checkpoints its own state; the steward (distinct issuer) steers.
-    let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1; 16]).map_err(|e| format!("{e:?}"))?;
+    let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1; 16], None).map_err(|e| format!("{e:?}"))?;
     verify_checkpoint(&cp, &g).map_err(|e| format!("{e:?}"))?;
     let am = amend(&steward, &g, &cp, 400, Some(ContentId::of_bytes(b"instr")), [2; 16]).map_err(|e| format!("{e:?}"))?;
     verify_amendment(&am, &g, &cp).map_err(|e| format!("{e:?}"))?;
@@ -674,9 +674,40 @@ fn c21_checkpoint() -> Result<(), String> {
         return Err("continuation budget was not tightened".into());
     }
 
+    // An amendment may not restore budget the run has already spent. The old
+    // rule compared the amendment against the grant's ISSUED budget, so on a
+    // 1 000 µJ grant with 900 µJ already spent, an amendment of 1 000 passed
+    // as "tightening" while handing the run ten times its remainder.
+    let spent_cp = checkpoint(
+        &agent,
+        &g,
+        ContentId::of_bytes(b"state-2"),
+        1,
+        [3; 16],
+        Some(Spend { uj: 900, provenance: Provenance::HwShunt }),
+    )
+    .map_err(|e| format!("{e:?}"))?;
+    verify_checkpoint(&spent_cp, &g).map_err(|e| format!("{e:?}"))?;
+    if remaining_uj(&g.grant, &spent_cp.checkpoint) != Some(100) {
+        return Err("remaining budget was not derived from the checkpoint".into());
+    }
+    if !matches!(
+        amend(&steward, &g, &spent_cp, 1_000, None, [4; 16]),
+        Err(CheckpointError::Amplifies(_))
+    ) {
+        return Err("an amendment restored budget the run had already spent".into());
+    }
+    // At or under the remainder it is still allowed.
+    amend(&steward, &g, &spent_cp, 100, None, [5; 16]).map_err(|e| format!("{e:?}"))?;
+    // A checkpoint that states no spend keeps the older, weaker ceiling, and
+    // says so by having no remainder to report.
+    if remaining_uj(&g.grant, &cp.checkpoint).is_some() {
+        return Err("a checkpoint with no spend reported a remainder".into());
+    }
+
     // Negative: the agent cannot steer itself, even on a self-issued grant.
     let self_g = grant(&agent, did(&agent), ContentId::of_bytes(b"t"), &["read"], 100, 0);
-    let self_cp = checkpoint(&agent, &self_g, ContentId::of_bytes(b"s"), 0, [1; 16]).map_err(|e| format!("{e:?}"))?;
+    let self_cp = checkpoint(&agent, &self_g, ContentId::of_bytes(b"s"), 0, [1; 16], None).map_err(|e| format!("{e:?}"))?;
     if !matches!(amend(&agent, &self_g, &self_cp, 50, None, [2; 16]), Err(CheckpointError::SeparationOfDuties)) {
         return Err("an agent steered itself".into());
     }

jcp/jcp-rs/crates/jcp-conformance/tests/pack.rs

@@ -25,7 +25,9 @@
 //! - **`dual_ceilings.json`** — §4.8's money-beside-joules ceiling, including the
 //!   two refusals that make it real (`funds-exceeded`, `currency-mismatch`). Those
 //!   are negative vectors, and nothing executed them.
-//! - **`standing.json`** — the standing-grant lineage.
+//! - **`standing.json`** — the standing-grant lineage, and (added with §4.7's
+//!   remainder rule) the spend-bearing checkpoint whose arithmetic a third
+//!   party can redo.
 //!
 //! Note `legacy_jcp1.json` is deliberately absent from the drift check below: it is
 //! a frozen historical artifact ("not minted any more"), so regenerating it would
@@ -221,6 +223,26 @@ fn the_standing_lineage_links_as_far_as_the_pack_allows() {
         "a minted child may not exceed the amended ceiling"
     );
 
+    // The spend-bearing checkpoint (§4.7's remainder rule). Two things are
+    // checkable from the published files alone: the remainder is arithmetic a
+    // third party can redo, and the entry's id differs from `checkpoint`'s —
+    // which is what makes the additivity claim non-vacuous. `checkpoint` was
+    // generated with no spend and keeps the id it had before the field existed;
+    // this one carries the field and therefore cannot.
+    let sp = &d["checkpoint_with_spend"];
+    let issued = sp["grant_budget_uj"].as_u64().expect("the entry publishes the issued budget");
+    let spent = sp["spent_uj"].as_u64().expect("the entry publishes the spend");
+    let remaining = sp["remaining_uj"].as_u64().expect("the entry publishes the remainder");
+    assert_eq!(
+        issued.saturating_sub(spent), remaining,
+        "the published remainder is not the issued budget minus the spend"
+    );
+    assert!(remaining < issued, "a vector for the remainder rule must actually have spent something");
+    assert_ne!(
+        id("checkpoint_with_spend"), id("checkpoint"),
+        "a declared spend must change the checkpoint's id — it is signed, not advisory"
+    );
+
     let published: Vec<String> = ["standing_grant", "mint_policy", "minted_child", "amendment", "checkpoint", "continuation_grant"]
         .iter()
         .map(|k| id(k))

jcp/jcp-rs/crates/jcp-grant/src/checkpoint.rs

@@ -19,12 +19,29 @@
 //!   (§4.3); an amendment is a *soft revoke* that re-bounds the run instead of
 //!   killing it.
 //!
-//! An amendment may only **tighten**: the continuation's budget is at most the
-//! checkpoint grant's, so steering can never escalate a running agent's
-//! authority. Widening is just issuing a new grant, and is out of scope here.
+//! An amendment may only **tighten**, and the bar is what the grant has *left*
+//! at the checkpoint, not what it was issued with. The distinction is the whole
+//! point: on a 1 000 µJ grant whose run has already spent 900, an amendment of
+//! 1 000 reads as "tightening" against the issued figure while handing the run
+//! ten times its remainder. A checkpoint that states its [`Spend`] is therefore
+//! measured against [`remaining_uj`]; one that states nothing falls back to the
+//! issued budget, which is the older and weaker rule (see
+//! [`amendable_ceiling_uj`] for why the fallback is not a refusal). Widening is
+//! just issuing a new grant, and is out of scope here.
+//!
+//! What the spend figure is worth. The checkpoint is authored by the *agent* —
+//! the party the remainder constrains — so its declared spend is a claim, not
+//! an independent measurement, and the `provenance` grade travels with it so
+//! the amender can see which kind of claim it is. Two things make the claim
+//! hard to shrink: it is signed, so understating it is attributable, and it is
+//! cumulative, so [`checkpoint_follows`] catches a later checkpoint that
+//! declares less than an earlier one or drops the field it once carried. What
+//! this layer does not do is independently meter the run; a deployment that
+//! needs that binds receipts (§5) to the checkpoint instead of trusting the
+//! figure.
 
 use ed25519_dalek::{Signature, Signer, SigningKey, Verifier};
-use jcp_schema::{canonical_cbor, ContentId, Did, Grant, SignedGrant};
+use jcp_schema::{canonical_cbor, ContentId, Did, Grant, Provenance, SignedGrant};
 use serde::{Deserialize, Serialize};
 
 use crate::{issue, GrantError};
@@ -42,6 +59,45 @@ pub struct Checkpoint {
     /// Monotonic checkpoint index within the run.
     pub seq: u64,
     pub nonce: [u8; 16],
+    /// What the run has spent under this grant, as of this boundary.
+    ///
+    /// `None` is the historical shape and is skipped on the wire, so every
+    /// checkpoint written before this field existed keeps its
+    /// [`Checkpoint::id`] and the sealed conformance vectors are unchanged.
+    /// It is also the *weaker* shape — see [`remaining_uj`].
+    ///
+    /// `skip_serializing_if` is load-bearing, not tidiness: the JCR-1 signed
+    /// core forbids nulls, so without it `Checkpoint::id()` fails outright with
+    /// `DisallowedType("null")` on every checkpoint that states no spend.
+    /// Omission is the only encoding the canonical form permits.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub spent: Option<Spend>,
+}
+
+/// Energy spent under a grant up to a checkpoint, with the provenance of the
+/// figure.
+///
+/// Cumulative rather than since-the-previous-checkpoint: one checkpoint then
+/// answers "how much is left" on its own, without the verifier having to hold
+/// the whole chain and without a missing link silently understating the total.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct Spend {
+    /// Microjoules spent under this grant so far.
+    pub uj: u64,
+    /// How the figure was obtained. Carried because a budget decision made on
+    /// an `Estimator` figure is a different decision from one made on a
+    /// hardware reading, and the amendment it justifies is signed either way.
+    pub provenance: Provenance,
+}
+
+/// What the grant has left at this checkpoint, when the checkpoint says what
+/// it spent.
+///
+/// `None` when the checkpoint declares no spend. That is not zero — it is
+/// *unknown*, and the two must not be confused: treating unknown as zero
+/// would let an amendment hand back the whole grant.
+pub fn remaining_uj(grant: &Grant, cp: &Checkpoint) -> Option<u64> {
+    cp.spent.map(|s| grant.budget_uj.saturating_sub(s.uj))
 }
 
 impl Checkpoint {
@@ -114,20 +170,83 @@ impl From<GrantError> for CheckpointError {
     }
 }
 
+/// The most an amendment at this checkpoint may grant.
+///
+/// The remainder where the checkpoint declares its spend; the whole grant
+/// otherwise. The fallback is deliberately the old, weaker rule rather than a
+/// refusal: a checkpoint written before `spent` existed is still a valid
+/// checkpoint, and rejecting it would break running deployments to fix a hole
+/// it cannot express. What it does mean is that the guarantee is only as
+/// strong as the checkpoint — which [`remaining_uj`] returning `None` is how a
+/// verifier finds out.
+fn amendable_ceiling_uj(grant: &Grant, cp: &Checkpoint) -> u64 {
+    remaining_uj(grant, cp).unwrap_or(grant.budget_uj)
+}
+
+/// Check that `next` is a lawful successor to `prev` within one run.
+///
+/// Each object on its own is well-formed; this is the relationship between
+/// them, and it is where an understated spend becomes visible. A declared
+/// spend is cumulative, so across a chain it may only rise, and a checkpoint
+/// that once declared a figure may not later go silent — otherwise an agent
+/// could check in at 900 µJ spent, then check in again saying nothing, and
+/// recover the whole issued budget as its ceiling.
+///
+/// Callers that keep the chain SHOULD run this before honouring an amendment
+/// at `next`. It is deliberately not folded into [`verify_checkpoint`], which
+/// is given one checkpoint and cannot see a predecessor it was never handed.
+pub fn checkpoint_follows(prev: &Checkpoint, next: &Checkpoint) -> Result<(), CheckpointError> {
+    if next.grant_id != prev.grant_id {
+        return Err(CheckpointError::ChainBroken("checkpoints name different grants"));
+    }
+    if next.author != prev.author {
+        return Err(CheckpointError::ChainBroken("checkpoints have different authors"));
+    }
+    if next.seq <= prev.seq {
+        return Err(CheckpointError::ChainBroken("checkpoint seq did not advance"));
+    }
+    match (prev.spent, next.spent) {
+        (Some(p), Some(n)) if n.uj < p.uj => Err(CheckpointError::Amplifies(
+            "cumulative spend fell between checkpoints",
+        )),
+        (Some(_), None) => Err(CheckpointError::Amplifies(
+            "a checkpoint that declared its spend later declared none",
+        )),
+        _ => Ok(()),
+    }
+}
+
+/// Say which ceiling was exceeded, since the two are different claims.
+fn amplify_reason(cp: &Checkpoint) -> &'static str {
+    if cp.spent.is_some() {
+        "amended budget exceeds what the grant has left at this checkpoint"
+    } else {
+        "amended budget exceeds the grant"
+    }
+}
+
 /// Emit a checkpoint. The signer MUST be the grant's `subject` — only the
 /// running agent commits to its own state.
+/// `spent` is `Option` rather than a plain figure because a run that genuinely
+/// cannot meter itself must be able to say so, and because the difference
+/// matters: `None` means *unknown*, not zero, and an amendment at an
+/// unknown-spend checkpoint falls back to the weaker whole-grant ceiling.
+/// It is a parameter rather than a second constructor so that every call site
+/// decides visibly.
+#[allow(clippy::too_many_arguments)]
 pub fn checkpoint(
     agent_sk: &SigningKey,
     grant: &SignedGrant,
     state_hash: ContentId,
     seq: u64,
     nonce: [u8; 16],
+    spent: Option<Spend>,
 ) -> Result<SignedCheckpoint, CheckpointError> {
     let author = Did::from_verifying_key(&agent_sk.verifying_key());
     if author != grant.grant.subject {
         return Err(CheckpointError::NotTheSubject);
     }
-    let cp = Checkpoint { grant_id: grant.grant.id(), author, state_hash, seq, nonce };
+    let cp = Checkpoint { grant_id: grant.grant.id(), author, state_hash, seq, nonce, spent };
     let bytes = canonical_cbor(&cp).map_err(GrantError::from)?;
     let signature = agent_sk.sign(&bytes).to_bytes().to_vec();
     Ok(SignedCheckpoint { checkpoint: cp, signature })
@@ -166,8 +285,16 @@ pub fn amend(
     if amender == cp.checkpoint.author {
         return Err(CheckpointError::SeparationOfDuties);
     }
-    if new_budget_uj > grant.grant.budget_uj {
-        return Err(CheckpointError::Amplifies("amended budget exceeds the grant"));
+    // The ceiling is what the grant has LEFT, not what it was issued with.
+    //
+    // Comparing against `grant.budget_uj` was the bug: on a 1 000 000 µJ grant
+    // whose run had already spent 900 000, an amendment of 1 000 000 passed as
+    // "tightening" while handing the run ten times its remainder. An amendment
+    // is a soft revoke, and a soft revoke that restores spent budget is an
+    // escalation — which is exactly what this module's own documentation says
+    // steering can never do.
+    if new_budget_uj > amendable_ceiling_uj(&grant.grant, &cp.checkpoint) {
+        return Err(CheckpointError::Amplifies(amplify_reason(&cp.checkpoint)));
     }
     let amendment = Amendment {
         checkpoint_id: cp.checkpoint.id(),
@@ -198,8 +325,8 @@ pub fn verify_amendment(
     if sa.amendment.amender == cp.checkpoint.author {
         return Err(CheckpointError::SeparationOfDuties);
     }
-    if sa.amendment.new_budget_uj > grant.grant.budget_uj {
-        return Err(CheckpointError::Amplifies("amended budget exceeds the grant"));
+    if sa.amendment.new_budget_uj > amendable_ceiling_uj(&grant.grant, &cp.checkpoint) {
+        return Err(CheckpointError::Amplifies(amplify_reason(&cp.checkpoint)));
     }
     let vk = sa.amendment.amender.verifying_key().map_err(GrantError::from)?;
     let bytes = canonical_cbor(&sa.amendment).map_err(GrantError::from)?;
@@ -272,7 +399,7 @@ mod tests {
     #[test]
     fn checkpoint_round_trips_and_binds_to_subject() {
         let (_steward, agent, g) = setup();
-        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16]).unwrap();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16], None).unwrap();
         verify_checkpoint(&cp, &g).unwrap();
         assert_eq!(cp.checkpoint.author, g.grant.subject);
     }
@@ -281,14 +408,14 @@ mod tests {
     fn agent_may_not_checkpoint_a_grant_it_does_not_hold() {
         let (steward, _agent, g) = setup();
         // The steward is not the subject — its checkpoint is refused.
-        let r = checkpoint(&steward, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16]);
+        let r = checkpoint(&steward, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16], None);
         assert!(matches!(r, Err(CheckpointError::NotTheSubject)));
     }
 
     #[test]
     fn issuer_amends_and_run_continues_under_tighter_budget() {
         let (steward, agent, g) = setup();
-        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16]).unwrap();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16], None).unwrap();
         let am = amend(&steward, &g, &cp, 400, Some(ContentId::of_bytes(b"new-instructions")), [2u8; 16]).unwrap();
         verify_amendment(&am, &g, &cp).unwrap();
         let cont = apply_amendment(&steward, &g, &cp, &am).unwrap();
@@ -309,7 +436,7 @@ mod tests {
             budget_uj: 1_000, expiry: 0, parent: None, delegate_depth: None, nonce: [0u8; 16], budget_funds: None, caveats: Vec::new(),
         };
         let g = issue(&agent, self_grant).unwrap();
-        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16]).unwrap();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16], None).unwrap();
         let r = amend(&agent, &g, &cp, 100, None, [2u8; 16]);
         assert!(matches!(r, Err(CheckpointError::SeparationOfDuties)));
     }
@@ -318,7 +445,7 @@ mod tests {
     fn a_non_issuer_cannot_amend() {
         let (_steward, agent, g) = setup();
         let stranger = SigningKey::from_bytes(&[9u8; 32]);
-        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16]).unwrap();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16], None).unwrap();
         let r = amend(&stranger, &g, &cp, 100, None, [2u8; 16]);
         assert!(matches!(r, Err(CheckpointError::NotTheIssuer)));
     }
@@ -326,7 +453,7 @@ mod tests {
     #[test]
     fn an_amendment_may_only_tighten() {
         let (steward, agent, g) = setup();
-        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16]).unwrap();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16], None).unwrap();
         let r = amend(&steward, &g, &cp, 5_000, None, [2u8; 16]);
         assert!(matches!(r, Err(CheckpointError::Amplifies(_))));
     }
@@ -334,10 +461,164 @@ mod tests {
     #[test]
     fn a_forged_amendment_for_another_checkpoint_is_refused() {
         let (steward, agent, g) = setup();
-        let cp1 = checkpoint(&agent, &g, ContentId::of_bytes(b"s1"), 0, [1u8; 16]).unwrap();
-        let cp2 = checkpoint(&agent, &g, ContentId::of_bytes(b"s2"), 1, [2u8; 16]).unwrap();
+        let cp1 = checkpoint(&agent, &g, ContentId::of_bytes(b"s1"), 0, [1u8; 16], None).unwrap();
+        let cp2 = checkpoint(&agent, &g, ContentId::of_bytes(b"s2"), 1, [2u8; 16], None).unwrap();
         let am = amend(&steward, &g, &cp1, 400, None, [3u8; 16]).unwrap();
         // The amendment was authored for cp1; presented against cp2 it fails.
         assert!(matches!(verify_amendment(&am, &g, &cp2), Err(CheckpointError::ChainBroken(_))));
     }
+    // ---- the remainder rule -------------------------------------------------
+
+    #[test]
+    fn an_amendment_may_not_restore_spent_budget() {
+        // The hole this field exists to close. Before `spent`, both `amend` and
+        // `verify_amendment` compared against `grant.budget_uj` — the budget as
+        // ISSUED — so this amendment was accepted as a tightening while handing
+        // the run ten times what it had left.
+        let (steward, agent, g) = setup();
+        let cp = checkpoint(
+            &agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16],
+            Some(Spend { uj: 900, provenance: Provenance::HwShunt }),
+        )
+        .unwrap();
+        assert_eq!(remaining_uj(&g.grant, &cp.checkpoint), Some(100));
+        assert!(matches!(
+            amend(&steward, &g, &cp, 1_000, None, [2u8; 16]),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        // One microjoule over the remainder is still over it.
+        assert!(matches!(
+            amend(&steward, &g, &cp, 101, None, [2u8; 16]),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        // At the remainder exactly, it is allowed.
+        let am = amend(&steward, &g, &cp, 100, None, [3u8; 16]).unwrap();
+        verify_amendment(&am, &g, &cp).unwrap();
+        let cont = apply_amendment(&steward, &g, &cp, &am).unwrap();
+        assert_eq!(cont.grant.budget_uj, 100);
+    }
+
+    #[test]
+    fn verify_amendment_enforces_the_remainder_too() {
+        // `amend` refusing is not enough: a steward could sign an over-budget
+        // amendment with its own key and hand it straight to an enforcement
+        // point, which never calls `amend`. The check has to live on the
+        // verifying side as well.
+        let (steward, agent, g) = setup();
+        let cp = checkpoint(
+            &agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16],
+            Some(Spend { uj: 900, provenance: Provenance::Estimator }),
+        )
+        .unwrap();
+        let forged = Amendment {
+            checkpoint_id: cp.checkpoint.id(),
+            amender: did(&steward),
+            new_budget_uj: 1_000,
+            instruction_id: None,
+            nonce: [7u8; 16],
+        };
+        let sig = steward.sign(&canonical_cbor(&forged).unwrap()).to_bytes().to_vec();
+        let signed = SignedAmendment { amendment: forged, signature: sig };
+        assert!(matches!(
+            verify_amendment(&signed, &g, &cp),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        // And the continuation cannot be minted from it either.
+        assert!(matches!(
+            apply_amendment(&steward, &g, &cp, &signed),
+            Err(CheckpointError::Amplifies(_))
+        ));
+    }
+
+    #[test]
+    fn a_silent_checkpoint_keeps_the_older_weaker_ceiling() {
+        // Unknown is not zero, but it is also not a refusal: a checkpoint from
+        // before the field existed is still valid, and says so by having no
+        // remainder to report.
+        let (steward, agent, g) = setup();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16], None).unwrap();
+        assert_eq!(remaining_uj(&g.grant, &cp.checkpoint), None);
+        amend(&steward, &g, &cp, 1_000, None, [2u8; 16]).unwrap();
+        assert!(matches!(
+            amend(&steward, &g, &cp, 1_001, None, [3u8; 16]),
+            Err(CheckpointError::Amplifies(_))
+        ));
+    }
+
+    #[test]
+    fn a_spend_beyond_the_budget_leaves_nothing_rather_than_wrapping() {
+        // An overspend is a real state — enforcement is per-debit and a final
+        // debit can land over the line. The remainder saturates at zero; it
+        // must not underflow into a vast ceiling.
+        let (steward, agent, g) = setup();
+        let cp = checkpoint(
+            &agent, &g, ContentId::of_bytes(b"s"), 0, [1u8; 16],
+            Some(Spend { uj: 4_000, provenance: Provenance::HwShunt }),
+        )
+        .unwrap();
+        assert_eq!(remaining_uj(&g.grant, &cp.checkpoint), Some(0));
+        assert!(matches!(
+            amend(&steward, &g, &cp, 1, None, [2u8; 16]),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        // Zero is the only lawful continuation: the run may be wound down
+        // under a grant that can no longer buy anything, which is different
+        // from killing it outright (§4.3).
+        amend(&steward, &g, &cp, 0, None, [3u8; 16]).unwrap();
+    }
+
+    #[test]
+    fn the_spend_field_does_not_change_an_existing_checkpoint() {
+        // The wire extension is additive: `spent: None` is skipped, so the
+        // signed core is byte-identical to the shape that predates the field
+        // and every sealed vector still verifies.
+        let (_steward, agent, g) = setup();
+        let cp = checkpoint(&agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16], None).unwrap();
+        let bytes = canonical_cbor(&cp.checkpoint).unwrap();
+        assert!(
+            !bytes.windows(5).any(|w| w == b"spent"),
+            "an absent spend must not appear in the signed bytes"
+        );
+        // And a stated spend does change the id — it is signed, not advisory.
+        let with = checkpoint(
+            &agent, &g, ContentId::of_bytes(b"state-1"), 0, [1u8; 16],
+            Some(Spend { uj: 0, provenance: Provenance::Estimator }),
+        )
+        .unwrap();
+        assert_ne!(
+            with.checkpoint.id(), cp.checkpoint.id(),
+            "a declared spend of zero is a claim, and differs from no claim"
+        );
+    }
+
+    #[test]
+    fn cumulative_spend_may_not_fall_or_go_silent_across_a_run() {
+        let (_steward, agent, g) = setup();
+        let mk = |seq: u64, n: u8, spend: Option<Spend>| {
+            checkpoint(&agent, &g, ContentId::of_bytes(b"s"), seq, [n; 16], spend)
+                .unwrap()
+                .checkpoint
+        };
+        let first = mk(0, 1, Some(Spend { uj: 900, provenance: Provenance::HwShunt }));
+        let rose = mk(1, 2, Some(Spend { uj: 950, provenance: Provenance::HwShunt }));
+        checkpoint_follows(&first, &rose).unwrap();
+        let fell = mk(1, 3, Some(Spend { uj: 100, provenance: Provenance::HwShunt }));
+        assert!(matches!(
+            checkpoint_follows(&first, &fell),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        let silent = mk(1, 4, None);
+        assert!(matches!(
+            checkpoint_follows(&first, &silent),
+            Err(CheckpointError::Amplifies(_))
+        ));
+        // Going from silent to stated is fine — that is a deployment turning
+        // metering on mid-run, not an agent walking a figure back.
+        checkpoint_follows(&mk(0, 5, None), &rose).unwrap();
+        // And the chain checks are still chain checks.
+        assert!(matches!(
+            checkpoint_follows(&rose, &first),
+            Err(CheckpointError::ChainBroken(_))
+        ));
+    }
 }