pool: recover held slots on restart — an empty memory is not an empty pool #41

Merged

larandar merged 1 commit from pool/40-restart-recovery into fastlane

2026-09-03 22:42:44 +00:00

larandar commented

2026-09-03 22:41:13 +00:00

Owner

Closes the gap #39 flagged in its own doc comment and PR body. OpenSpec 30 amended to v0.1.2 alongside — the package never specified recovery at all, so this was a package gap rather than a Session that missed its scope.

The bug

Cycle::new started every slot Available. Correct for a pool that has never run, wrong for every restart after the first: a process that comes back while drones hold slots believed the pool was empty and would hand the same identities to a second set of occupants.

This is the failure #37 prevents, arriving through a door #37 does not watch. That rule is stated per transition — nothing infers a slot is free — and a restart takes no transition. An empty map is not an inference; the process simply never knew. The guarantee has to hold over the initial state too, or it does not hold.

The fix

Occupancy is durable. Cycle::recover reconstructs each slot from the ledger, and new is gone rather than deprecated, so no caller can accidentally start empty.

Ordering errs toward held, in both directions. The write precedes the stamp, so a process dying anywhere after it leaves a slot recorded as held for an occupancy that may never have gone live — recoverable by an operator's release, costing one slot out of ten. Recording after the hand-out would instead leave a window where a live drone holds a slot nothing remembers, and that cost is unbounded. The record clears only after revoke and rotate have succeeded, for the same reason in reverse.

A refusal is not a crash. When the stamp is refused, nothing was handed out and nothing is live, so the record is compensated immediately rather than waiting for a human. An interrupted process cannot reach that compensation — which is exactly why the write comes first.

Unreadable state denies rather than defaulting. "I do not know what is held" and "nothing is held" are different answers, and only one is safe. A damaged ledger fails the constructor, so a cycle that does not know what it holds cannot be built and therefore cannot allocate — structural, not a check someone can forget to write. Torn tail tolerated, torn middle refused, matching operations.rs.

Verification

Gate green: fmt stable, clippy --workspace --all-targets -D warnings clean, cargo test --workspace passing — 103 lib tests, up from 96.

claim	how it is proven
a restart comes back still held	same session, assignment and grant after reconstruction
a restart does not double-allocate	second cycle's checkout returns `Exhausted`
a completed slot returns available	and at its new generation, so occupancies stay distinguishable
a crash between write and stamp holds the slot	the crash state is written directly, then recovered and released
a refusal does not strand a slot	available again after restart
a damaged ledger refuses	`OccupancyUnavailable`, and the cycle cannot be constructed
a torn tail survives	the complete line loads, the partial one is dropped

One test was honest about its limits rather than faked. A capture double cannot die between two awaits, so the crash-window test writes what the crash would have left and says so in the comment. Pretending otherwise would have made it a test of the double.

Still not here

No live effects. Occupancy and PoolDirectory have no Kanidm or OpenBao implementations; both wait on sa-vedanta (flake-ops#98).
No held-slot alerting. held() is what an alert reads; raising it is #11's mandate on flake-ops#470's plane.

Closes #40

Closes the gap [#39](https://jo.et0.pw/Ting/Vedanta/pulls/39) flagged in its own doc comment and PR body. [OpenSpec 30](https://jo.et0.pw/Ting/Vedanta/wiki/OpenSpec-30-agent-identity-pool-lifecycle) amended to **v0.1.2** alongside — the package never specified recovery at all, so this was a package gap rather than a Session that missed its scope. ## The bug `Cycle::new` started every slot `Available`. Correct for a pool that has never run, wrong for every restart after the first: a process that comes back while drones hold slots believed the pool was empty and would hand the same identities to a second set of occupants. **This is the failure [#37](https://jo.et0.pw/Ting/Vedanta/issues/37) prevents, arriving through a door #37 does not watch.** That rule is stated per transition — nothing *infers* a slot is free — and a restart takes no transition. An empty map is not an inference; the process simply never knew. The guarantee has to hold over the **initial state** too, or it does not hold. ## The fix Occupancy is durable. `Cycle::recover` reconstructs each slot from the ledger, and **`new` is gone rather than deprecated**, so no caller can accidentally start empty. **Ordering errs toward held, in both directions.** The write precedes the stamp, so a process dying anywhere after it leaves a slot recorded as held for an occupancy that may never have gone live — recoverable by an operator's release, costing one slot out of ten. Recording *after* the hand-out would instead leave a window where a live drone holds a slot nothing remembers, and that cost is unbounded. The record clears only after revoke and rotate have succeeded, for the same reason in reverse. **A refusal is not a crash.** When the stamp is refused, nothing was handed out and nothing is live, so the record is compensated immediately rather than waiting for a human. An interrupted process cannot reach that compensation — which is exactly why the write comes first. **Unreadable state denies rather than defaulting.** *"I do not know what is held"* and *"nothing is held"* are different answers, and only one is safe. A damaged ledger fails the constructor, so a cycle that does not know what it holds cannot be built and therefore cannot allocate — structural, not a check someone can forget to write. Torn tail tolerated, torn middle refused, matching `operations.rs`. ## Verification Gate green: fmt stable, `clippy --workspace --all-targets -D warnings` clean, `cargo test --workspace` passing — **103 lib tests, up from 96**. | claim | how it is proven | |---|---| | a restart comes back still held | same session, assignment and grant after reconstruction | | a restart does not double-allocate | second cycle's checkout returns `Exhausted` | | a completed slot returns available | and at its **new** generation, so occupancies stay distinguishable | | a crash between write and stamp holds the slot | the crash state is written directly, then recovered and released | | a refusal does not strand a slot | available again after restart | | a damaged ledger refuses | `OccupancyUnavailable`, and the cycle cannot be constructed | | a torn tail survives | the complete line loads, the partial one is dropped | **One test was honest about its limits rather than faked.** A capture double cannot die between two awaits, so the crash-window test writes what the crash *would* have left and says so in the comment. Pretending otherwise would have made it a test of the double. ## Still not here - **No live effects.** `Occupancy` and `PoolDirectory` have no Kanidm or OpenBao implementations; both wait on `sa-vedanta` ([flake-ops#98](https://jo.et0.pw/lar.ad/flake-ops/issues/98)). - **No held-slot alerting.** `held()` is what an alert reads; raising it is [#11](https://jo.et0.pw/Ting/Vedanta/issues/11)'s mandate on [flake-ops#470](https://jo.et0.pw/lar.ad/flake-ops/issues/470)'s plane. Closes #40

larandar added 1 commit

2026-09-03 22:41:14 +00:00

pool: recover held slots on restart — an empty memory is not an empty pool (#40 ) 550d8c284e

`Cycle::new` started every slot available. Correct for a pool that has never
run, wrong for every restart after the first: a process that comes back while
drones hold slots believed the pool was empty and would hand the same identities
to a second set of occupants.

This is the failure the explicit-release rule prevents, arriving through a door
that rule does not watch. It is stated per transition — nothing INFERS a slot is
free — and a restart takes no transition. An empty map is not an inference; the
process simply never knew. So the guarantee has to hold over the initial state
too, or it does not hold.

Occupancy is now durable. `Cycle::recover` reconstructs each slot from the
ledger; `new` is gone rather than deprecated, so no caller can accidentally
start empty.

ORDERING ERRS TOWARD HELD, IN BOTH DIRECTIONS. The write precedes the stamp, so
a process dying anywhere after it leaves a slot recorded as held for an
occupancy that may never have gone live — recoverable by an operator's release,
costing one slot out of ten. Recording after the hand-out would instead leave a
window where a live drone holds a slot nothing remembers, and that cost is
unbounded. The record clears only after revoke and rotate have succeeded, for
the same reason in reverse.

A REFUSAL IS NOT A CRASH. When the stamp is refused, nothing was handed out and
nothing is live, so the record is compensated immediately instead of waiting for
a human. An interrupted process cannot reach that compensation, which is exactly
why the write comes first.

UNREADABLE STATE DENIES RATHER THAN DEFAULTING. "I do not know what is held" and
"nothing is held" are different answers and only one is safe. A damaged ledger
fails the constructor, so a cycle that does not know what it holds cannot be
built and therefore cannot allocate — structural, not a check someone can forget
to write. Torn tail tolerated, torn middle refused, as in the operation journal.

The crash-window test writes what the crash would have left rather than
pretending a double can die between two awaits, and says so.

larandar merged commit 550d8c284e into fastlane

2026-09-03 22:42:44 +00:00

larandar deleted branch pool/40-restart-recovery

2026-09-03 22:42:44 +00:00

No reviewers

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

Ting/Vedanta!41

No description provided.

Rows
Columns