vh
c3a97c1b64
`.forever` was the only way to say three different things — "this is durable",
"I have not answered yet", "I am still looking" — and the census said it was
carrying all three: 17 of 24 live booths (70%, up from 54% the day before).
Three of the four booths in the fleet awaiting an answer had been pinned by
hand as well, and 10 of the 17 were younger than the TTL, so the sentinel had
bought them nothing and was pressed pre-emptively.
Only the first meaning is what `keep` means. The other two are facts the
service already held and did not consult.
KEPT `.forever` present never swept (unchanged)
HELD an open pick, or marks we cannot read never swept (new)
EPHEMERAL everything else 24h (unchanged)
Viewing is activity: a deliberately-served response from a booth's own page
route writes `.viewed`, which is a dotfile and not a `.lock` dotfile, so
`_newest_mtime` already counts it. There is no new arithmetic — `booth_age_seconds`,
`is_expired` and `expires_in` are unchanged. Machine reads are excluded on
purpose: an agent must not be able to hold its own booth open by polling for
the answer it is waiting on.
The hold is unbounded, and what makes that safe is visibility plus two exits
that already existed. Every surface whose chrome the Booth owns says
`held until answered` where the countdown was, and `booth rm` / the UI x /
`DELETE /b/<n>` take a held booth exactly as they take a kept one. A hold is
protection from the timer, never from the operator.
Three cross-frontier panels ran and each found a class the others could not:
* the paraphrase panel found that two reads of one file are not one read of
one state — the contract's `is_held(marks_for(c), read_error(c))` could
resolve to `([], None)`, the pair that deletes. `hold_read` is one read.
* the code-review panel found, 4-of-4, that the booth header's board branch
rendered no lifetime at all; and that five of seven invariant tests passed
under the change that defeats them.
* the bug-hunt panel found four more paths where a failed read still
authorized a delete, and a `record_view` that followed a planted symlink.
`is_held` became `hold_reason`, which returns the reason rather than a bool
beside a string that can disagree with it.
Prediction, to re-count on or after 2026-10-06: the `.forever` rate falls to
the booths that are genuinely durable references. Only 4 booths carry marks at
all, so this rests on both halves of the unit; a null result cannot distinguish
a wrong diagnosis from a habit that outlived its need.
406 tests (341 before). Contract: docs/contracts/u4_derived_lifetime.contract.md
41 lines
2.5 KiB
Markdown
41 lines
2.5 KiB
Markdown
# Five of seven INV falsifiers did not falsify anything
|
|
|
|
_2026-09-22 · booth_
|
|
|
|
The U4 contract carried seven invariants, each with a *Falsifiable:* line, and
|
|
each had a test. **The code-review panel showed that five of the seven tests
|
|
would still pass under a change that defeats the invariant they name.** Gróa's
|
|
"per INV entry, what would still pass" section is the single most useful thing
|
|
either panel produced on this unit.
|
|
|
|
| INV | what the test asserted | what still passed |
|
|
|---|---|---|
|
|
| 1 (no new arithmetic) | the clock moved after a view | special-casing `.viewed` inside `_newest_mtime` — the exact new arithmetic INV-1 forbids |
|
|
| 3 (`is_held` is pure) | the right answer, once | `is_held` doing I/O, or `return True` unconditionally |
|
|
| 4 (every surface says why) | a substring on `GET /` | dropping the line from the booth header, the marks page, or the board branch |
|
|
| 5 (a view cannot fail a request) | `record_view` did not raise | a second `touch` outside the guard, 500ing all three routes |
|
|
| 6 (unreadable marks hold) | the corrupt booth survived | a sweeper that deletes nothing at all (no doomed sibling in the fixture) |
|
|
| 7 (machine reads do not hold) | `.viewed` was absent | a handler writing any other non-dot file, holding the booth open just as well |
|
|
|
|
**The shape of the error is the same every time: the test asserted the OUTCOME
|
|
the author was thinking about, not the DISCRIMINATOR the invariant names.** A
|
|
green test proved the happy path and nothing about the invariant. Writing the
|
|
falsifiable line in the contract did not produce a falsifying test — it produced
|
|
a test that *cited* one.
|
|
|
|
Fixed by rewriting each to fail under the change that defeats it: same-mtime
|
|
equivalence with an arbitrary non-lock dotfile (plus a `.lock` that must NOT
|
|
count); `is_held` called with marks belonging to a booth that does not exist on
|
|
disk; one test per rendered surface, each rendering only its own; the three
|
|
routes GET against a chmod'd booth; a doomed sibling; the AGE asserted rather
|
|
than the marker. **The board-header pair was verified RED against the pre-fix
|
|
template rather than assumed** — which is the step that makes "fixed, not
|
|
amended" trustworthy.
|
|
|
|
**The method to keep: for each invariant, name a change that defeats it and ask
|
|
whether the test goes red.** If you cannot name one, the invariant is not
|
|
falsifiable yet. Regin and Kimi independently proposed this as a contract-time
|
|
"vacuity pass"; heid rates this round the strongest evidence for it so far, and
|
|
it is a `/heid*` skill proposal sitting with the operator, not a change to this
|
|
repo.
|