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

dcharlot commented 2026-10-05 21:28:57 -04:00

Owner

Copy link

The hole

jcp-grant's checkpoint module promises, in its own words, that "an amendment
may only tighten … so steering can never escalate a running agent's authority."
Both amend and verify_amendment enforced that with:

if new_budget_uj > grant.grant.budget_uj {
    return Err(CheckpointError::Amplifies("amended budget exceeds the grant"));
}

That compares against the budget as issued. On a 1 000 µJ grant whose run
has already spent 900, an amendment of 1 000 passes as a "tightening" and hands
the run ten times its remainder. The steering mechanism built to re-bound a long
run could re-fund it instead.

The sweep that found this framed it as "Checkpoint carries no energy field",
which understates it. The missing field is why the check could not be written
correctly: there was nothing for it to measure against.

What changed

Checkpoint gains 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" on its own, without the verifier holding the whole
chain and without a missing link silently understating the total.

remaining_uj(grant, cp) derives the remainder, and returns None when the
checkpoint is silent. Unknown is not zero, and conflating them is exactly 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 in
order to fix a hole those checkpoints cannot express. The guarantee is only as
strong as the checkpoint — which remaining_uj returning None is how a
verifier finds out.

Enforced on both sides. amend refusing is not enough: a steward can sign an
over-budget amendment with its own key and hand it to an enforcement point,
which never calls amend.

What the figure is actually worth

Stated in the module docs rather than left implied: the checkpoint is authored
and signed by the agent — the party the remainder constrains — so its
declared spend is a claim, not an independent measurement. 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 the new checkpoint_follows(prev, next)
refuses a successor that declares less than its predecessor or drops a field it
once carried — otherwise an agent recovers its full issued ceiling simply by
going quiet. What this layer does not do is independently meter the run.

The wire change is additive, and that is checked

spent: None is skipped, so Checkpoint::id() and every sealed vector are
byte-identical to before the field existed. Regenerating the pack is the proof:
standing.json gains one entry and no published id or signature moves,
checkpoint included.

skip_serializing_if turned out to be load-bearing rather than tidy — the JCR-1
signed core forbids nulls, so removing it makes Checkpoint::id() fail outright
with DisallowedType("null") on every checkpoint that states no spend. Omission
is the only encoding the canonical form permits, and the field's doc comment now
says so where an editor would see it.

The new checkpoint_with_spend vector publishes the issued budget beside 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 rather than by a vector.

Spec

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

Verification

cargo test --workspace in jcp/jcp-rs: 407 passed, 0 failed. No new clippy
warnings (the one jcp-schema warning predates this branch).

Six falsifications run from the committed baseline, each reverting one thing and
confirming a test dies:

reverted	caught by
ceiling back to the issued budget	3 tests fail
absent spend read as zero spend	a_silent_checkpoint_keeps_the_older_weaker_ceiling
saturating_sub → wrapping_sub	a_spend_beyond_the_budget_leaves_nothing_rather_than_wrapping
verify-side check removed (kept only in amend)	verify_amendment_enforces_the_remainder_too
monotonicity branch removed	cumulative_spend_may_not_fall_or_go_silent_across_a_run
skip_serializing_if removed	5 unit tests + the pack's drift check

🤖 Generated with Claude Code

## The hole `jcp-grant`'s checkpoint module promises, in its own words, that *"an amendment may only tighten … so steering can never escalate a running agent's authority."* Both `amend` and `verify_amendment` enforced that with: ```rust if new_budget_uj > grant.grant.budget_uj { return Err(CheckpointError::Amplifies("amended budget exceeds the grant")); } ``` That compares against the budget as **issued**. On a 1 000 µJ grant whose run has already spent 900, an amendment of 1 000 passes as a "tightening" and hands the run ten times its remainder. The steering mechanism built to re-bound a long run could re-fund it instead. The sweep that found this framed it as "`Checkpoint` carries no energy field", which understates it. The missing field is *why* the check could not be written correctly: there was nothing for it to measure against. ## What changed `Checkpoint` gains `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" on its own, without the verifier holding the whole chain and without a missing link silently understating the total. `remaining_uj(grant, cp)` derives the remainder, and returns `None` when the checkpoint is silent. Unknown is not zero, and conflating them is exactly 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 in order to fix a hole those checkpoints cannot express. The guarantee is only as strong as the checkpoint — which `remaining_uj` returning `None` is how a verifier finds out. Enforced on **both** sides. `amend` refusing is not enough: a steward can sign an over-budget amendment with its own key and hand it to an enforcement point, which never calls `amend`. ## What the figure is actually worth Stated in the module docs rather than left implied: the checkpoint is authored and signed by the **agent** — the party the remainder constrains — so its declared spend is a claim, not an independent measurement. 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 the new `checkpoint_follows(prev, next)` refuses a successor that declares less than its predecessor or drops a field it once carried — otherwise an agent recovers its full issued ceiling simply by going quiet. What this layer does **not** do is independently meter the run. ## The wire change is additive, and that is checked `spent: None` is skipped, so `Checkpoint::id()` and every sealed vector are byte-identical to before the field existed. Regenerating the pack is the proof: `standing.json` gains one entry and **no published id or signature moves**, `checkpoint` included. `skip_serializing_if` turned out to be load-bearing rather than tidy — the JCR-1 signed core forbids nulls, so removing it makes `Checkpoint::id()` fail outright with `DisallowedType("null")` on every checkpoint that states no spend. Omission is the only encoding the canonical form permits, and the field's doc comment now says so where an editor would see it. The new `checkpoint_with_spend` vector publishes the issued budget beside 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 rather than by a vector. ## Spec §4.7 and C21 now make the remainder normative: both sides MUST enforce it, an absent spend MUST NOT be read as zero, and a declared spend MUST NOT decrease. ## Verification `cargo test --workspace` in `jcp/jcp-rs`: **407 passed, 0 failed.** No new clippy warnings (the one `jcp-schema` warning predates this branch). Six falsifications run from the committed baseline, each reverting one thing and confirming a test dies: | reverted | caught by | |---|---| | ceiling back to the issued budget | 3 tests fail | | absent spend read as zero spend | `a_silent_checkpoint_keeps_the_older_weaker_ceiling` | | `saturating_sub` → `wrapping_sub` | `a_spend_beyond_the_budget_leaves_nothing_rather_than_wrapping` | | verify-side check removed (kept only in `amend`) | `verify_amendment_enforces_the_remainder_too` | | monotonicity branch removed | `cumulative_spend_may_not_fall_or_go_silent_across_a_run` | | `skip_serializing_if` removed | 5 unit tests + the pack's drift check | 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-10-05 21:28:57 -04:00

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

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

dcharlot referenced this pull request 2026-10-07 09:15:05 -04:00

[superseded by #181] energy tests: assert what the probe reports, not what the host's scheduler allows #178

dcharlot force-pushed feat/checkpoint-energy from 9f0cfd74be to 9248799a6a 2026-10-07 10:07:41 -04:00 Compare

dcharlot referenced this pull request from a commit 2026-10-07 14:29:11 -04:00

wai-pack: the lock still named wai-quantum 0.3.36

dcharlot referenced this pull request 2026-10-07 14:29:13 -04:00

[obsolete] wai-pack: the lock still named wai-quantum 0.3.36 #182

dcharlot force-pushed feat/checkpoint-energy from 9248799a6a to 936d26761a 2026-10-08 10:29:44 -04:00 Compare

dcharlot referenced this pull request from a commit 2026-10-08 11:40:25 -04:00

ci: a rebase ran every path-filtered workflow, because `paths:` matches the push delta

dcharlot referenced this pull request 2026-10-08 11:41:09 -04:00

ci: a rebase ran every path-filtered workflow, because paths: matches the push delta #191

dcharlot merged commit 661050d1a4 into main 2026-10-08 19:55:19 -04:00

dcharlot referenced this pull request from a commit 2026-10-08 19:55:20 -04:00

Merge pull request 'jcp §4.7: an amendment may only tighten against what the grant has LEFT' (#165) from feat/checkpoint-energy into main

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!165

No description provided.