jcp §4.7: an amendment may only tighten against what the grant has LEFT #165

Merged

dcharlot merged 1 commit from feat/checkpoint-energy into main 2026-10-08 19:55:19 -04:00

Conversation 0 Commits 1 Files changed 6 +419 -36

2026-10-08

Transaction Science

jcp §4.7: an amendment may only tighten against what the grant has LEFT ...

Both `amend` and `verify_amendment` compared the amended budget against
`grant.budget_uj` — the budget as ISSUED. On a 1 000 µJ grant whose run had
already spent 900, an amendment of 1 000 passed as a "tightening" while handing
the run ten times its remainder, contradicting the module's own guarantee that
"steering can never escalate a running agent's authority". The hole was not
that the check was missing; it was that the checkpoint had no way to say what
had been spent, so there was nothing for the check to measure against.

`Checkpoint` now carries `spent: Option<Spend>` — a cumulative microjoule
figure with its §5 provenance grade. Cumulative rather than per-interval, so
one checkpoint answers "how much is left" without the verifier holding the
whole chain and without a missing link silently understating the total.
`remaining_uj` derives the remainder and returns `None` when the checkpoint is
silent: unknown is not zero, and conflating them is how an amendment hands back
a whole grant.

The ceiling is now the remainder where the checkpoint states its spend, and the
issued budget where it does not. The fallback is deliberately the old, weaker
rule rather than a refusal — a checkpoint written before the field existed is
still a valid checkpoint, and rejecting it would break running deployments to
fix a hole it cannot express. Enforced on both sides: `amend` refusing is not
enough, because an enforcement point handed a signed amendment never calls
`amend`.

What the figure is worth, stated rather than implied: the checkpoint is authored
by the agent, so its declared spend is a signed claim, not an independent
measurement. Two things make it hard to shrink — it is attributable, and
`checkpoint_follows` catches a later checkpoint that declares less than an
earlier one or drops a field it once carried, which would otherwise let an agent
recover its full ceiling by going quiet.

Wire change is additive: `spent: None` is skipped, so `Checkpoint::id()` and
every sealed vector are byte-identical to before the field existed. Regenerating
the pack proves it — `standing.json` gains one entry and no published id or
signature moves. The new `checkpoint_with_spend` vector publishes the issued
budget alongside the spend so a third party can redo the arithmetic, and its id
necessarily differs from `checkpoint`'s, which is what makes the additivity
claim non-vacuous. The remainder rule itself is a refusal, and a refusal has
nothing to sign, so it is pinned by C21 and unit tests instead.

SPEC §4.7 and C21 updated: the remainder is normative, both sides MUST enforce
it, an absent spend MUST NOT be read as zero, and a declared spend MUST NOT
decrease.

Co-Authored-By: Claude Opus 5 <[email protected]>

936d26761a

• View at this point in history

2026-10-08 10:27:01 -04:00