spare: stop minting coverage a grant already carries #163

Merged
PerishFire merged 1 commit from land/spare-mint into main 2026-08-15 09:55:30 +00:00
Owner

spare: stop minting coverage a grant already carries

Every write by an operator wrote a second row: a @grant giving the creator
full coverage of what they had just made. Measured, that mint cost 0.54ms
against a 0.21ms insert, and it cost again indirectly — writing @grant bumps
its generation, so the next authority check re-read every grant row, and the
table it re-read had just grown by one. Creating rows was therefore quadratic,
and the ledger of authority grew one row per row of data, forever.

The mint is a grant the engine issues on the creator's behalf. Keel already
refuses a grant an operator could not have issued from live coverage; the
mirror of that rule is that a grant repeating coverage the operator already
holds carries nothing. It is no longer written. Actor birth keeps its
unconditional mint, because a newborn identity holds nothing yet.

That alone changed what a set may do. A holder who covers a row through its
root chain could hand it away only because the mint had given them coverage
independent of that chain: set checks before and after, and after the move
the row hangs under someone else. So the second law moved with the first. A
predicate is a statement about the row's content and is still required before
and after — that is what stops an author writing themselves out of author = "@me". Row and subtree coverage now answers the state the write started in:
you may move a thing out of your own reach, and afterwards it is not yours.
Taking is unaffected, because taking fails the check that runs first.

PATCH returned 404 after a successful hand-over, because the route read the
row back as the writer who had just given it away. A write that succeeded is
not a missing row: it answers 204 when the writer can no longer see what they
wrote.

Readings from the bench that found this, same machine, same three hundred
writes:

put across six rounds   0.92 → 6.23ms   becomes   0.20 → 0.22ms, flat
grants in the estate    303 → 1803      becomes   3, constant
mint alone              0.54ms          becomes   nothing to measure

allows left the documents. Both root projections described a non-mutating
probe that no face implements and no test calls; the seal says a person read
both sides, so leaving a promise the code does not keep would make the seal a
lie. If the probe is wanted it can arrive with its own tests.

Ectropy refused the first shape of this change twice — five parameters, then
four free functions sharing plan — and the second refusal was right: check,
shift, spans and broad were one receiver wearing four names. They are
Court now, and what a deed is asked to decide is one Case.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com

spare: stop minting coverage a grant already carries Every write by an operator wrote a second row: a `@grant` giving the creator full coverage of what they had just made. Measured, that mint cost 0.54ms against a 0.21ms insert, and it cost again indirectly — writing `@grant` bumps its generation, so the next authority check re-read every grant row, and the table it re-read had just grown by one. Creating rows was therefore quadratic, and the ledger of authority grew one row per row of data, forever. The mint is a grant the engine issues on the creator's behalf. Keel already refuses a grant an operator could not have issued from live coverage; the mirror of that rule is that a grant repeating coverage the operator already holds carries nothing. It is no longer written. `Actor` birth keeps its unconditional mint, because a newborn identity holds nothing yet. That alone changed what a `set` may do. A holder who covers a row through its root chain could hand it away only because the mint had given them coverage independent of that chain: `set` checks before and after, and after the move the row hangs under someone else. So the second law moved with the first. A predicate is a statement about the row's content and is still required before and after — that is what stops an author writing themselves out of `author = "@me"`. Row and subtree coverage now answers the state the write started in: you may move a thing out of your own reach, and afterwards it is not yours. Taking is unaffected, because taking fails the check that runs first. `PATCH` returned 404 after a successful hand-over, because the route read the row back as the writer who had just given it away. A write that succeeded is not a missing row: it answers 204 when the writer can no longer see what they wrote. Readings from the bench that found this, same machine, same three hundred writes: put across six rounds 0.92 → 6.23ms becomes 0.20 → 0.22ms, flat grants in the estate 303 → 1803 becomes 3, constant mint alone 0.54ms becomes nothing to measure `allows` left the documents. Both root projections described a non-mutating probe that no face implements and no test calls; the seal says a person read both sides, so leaving a promise the code does not keep would make the seal a lie. If the probe is wanted it can arrive with its own tests. Ectropy refused the first shape of this change twice — five parameters, then four free functions sharing `plan` — and the second refusal was right: `check`, `shift`, `spans` and `broad` were one receiver wearing four names. They are `Court` now, and what a deed is asked to decide is one `Case`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
spare: stop minting coverage a grant already carries
All checks were successful
guard / guard (pull_request) Successful in 2m10s
guard / guard (push) Successful in 1m59s
38b85ac543
spare: stop minting coverage a grant already carries

Every write by an operator wrote a second row: a `@grant` giving the creator
full coverage of what they had just made. Measured, that mint cost 0.54ms
against a 0.21ms insert, and it cost again indirectly — writing `@grant` bumps
its generation, so the next authority check re-read every grant row, and the
table it re-read had just grown by one. Creating rows was therefore quadratic,
and the ledger of authority grew one row per row of data, forever.

The mint is a grant the engine issues on the creator's behalf. Keel already
refuses a grant an operator could not have issued from live coverage; the
mirror of that rule is that a grant repeating coverage the operator already
holds carries nothing. It is no longer written. `Actor` birth keeps its
unconditional mint, because a newborn identity holds nothing yet.

That alone changed what a `set` may do. A holder who covers a row through its
root chain could hand it away only because the mint had given them coverage
independent of that chain: `set` checks before and after, and after the move
the row hangs under someone else. So the second law moved with the first. A
predicate is a statement about the row's content and is still required before
and after — that is what stops an author writing themselves out of `author =
"@me"`. Row and subtree coverage now answers the state the write started in:
you may move a thing out of your own reach, and afterwards it is not yours.
Taking is unaffected, because taking fails the check that runs first.

`PATCH` returned 404 after a successful hand-over, because the route read the
row back as the writer who had just given it away. A write that succeeded is
not a missing row: it answers 204 when the writer can no longer see what they
wrote.

Readings from the bench that found this, same machine, same three hundred
writes:

    put across six rounds   0.92 → 6.23ms   becomes   0.20 → 0.22ms, flat
    grants in the estate    303 → 1803      becomes   3, constant
    mint alone              0.54ms          becomes   nothing to measure

`allows` left the documents. Both root projections described a non-mutating
probe that no face implements and no test calls; the seal says a person read
both sides, so leaving a promise the code does not keep would make the seal a
lie. If the probe is wanted it can arrive with its own tests.

Ectropy refused the first shape of this change twice — five parameters, then
four free functions sharing `plan` — and the second refusal was right: `check`,
`shift`, `spans` and `broad` were one receiver wearing four names. They are
`Court` now, and what a deed is asked to decide is one `Case`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Land-Source: spare-mint@635f9320c5c1434b390d9c88c30334754c15a41a
Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
1 participant
Notifications
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
PerishLab/keel!163
No description provided.