amadan
Review four answered; design revision 11: the historical term excludes only the empty terminals (unrecorded sent), the cutoff is the bound fixed before the rows are read, a look's start is the bound by what it observes rather than an order; the model's fixed cutoff, a later witness change, four tests; Within's early-result contract documented and guarded; the plan rewritten in terms of Within
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
10 files changed,
+182
−32
DISPOSITIONS-replicator-pinned-root.md+15 −0docs/superpowers/plans/2026-10-03-replicator-authority-plan.md+4 −4docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md+3 −3docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md+2 −2internal/authority/authority.go+14 −7internal/authority/authority_other.go+1 −0internal/authority/authority_unix.go+16 −1internal/authority/authority_unix_test.go+19 −0internal/ops/admissionmodel/model.go+14 −12internal/ops/admissionmodel/model_test.go+94 −3
diff --git a/DISPOSITIONS-replicator-pinned-root.md b/DISPOSITIONS-replicator-pinned-root.md| index af3093e23..5cc2170f8 100644 |
| --- a/DISPOSITIONS-replicator-pinned-root.md |
| +++ b/DISPOSITIONS-replicator-pinned-root.md |
| @@ -61,3 +61,18 @@ Opus: accept with fixes, no P1, one P2. Astra: accept with fixes, no P1, one P2. |
| | Astra: a successor under a failed discovery with only a pending registration; a token admitted one day and sent the next; `Recheck` without `AT_SYMLINK_NOFOLLOW`; a `0757` component | `TestLatchOverlayReachesSuccessor`, `TestHistoricalTermUsesTheAdmissionInstant`, `TestRecheckDoesNotFollowAReplacementLink`, `TestPlatformRuleOtherWritable`; the overlay-owner-only, follow-links and group-only mutants killed. | |
| | Astra (unobservable): `O_CLOEXEC` on `List`'s temporary description; post-open `fstat` failures | listed as unobservable by these fixtures. | |
| +## Review four (of `7ba5fc72`: the third review answered, design revision 10) |
| + |
| +Opus: accept with fixes, no P1, one P2. Astra: accept with fixes, no P1, two P2. Reports: `logs/opus-replroot-review4.md`, `logs/astra-replroot-review4.md`. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| Both P2: the design's historical term named `how in {finished, abandoned}` and so excluded `unrecorded`, a settlement whose transport did send; the model counted every settlement and was right | **Design revision 11**: the term excludes only the empty terminals (`unissued`, `cancelled`); `transport-lost` is never a value of `how`; `recovered-unknown` has its own interval. `TestHistoricalTermCountsUnrecordedSettlements`; the mutant filtering by `{finished, abandoned}` is killed. | |
| +| Astra 2, Opus P3-1: the model's cutoff was the running minimum, so the answer depended on row order | the bound is computed once and every settlement is compared with it; `TestHistoricalCutoffIsTheFixedBound` in both commit orders; the running-cutoff mutant is killed; the design says "fixed before the rows are read and never the running minimum". | |
| +| Opus P3-2, Astra 4: the delayed-send test did not test its subject | the proof is moved past the look by a later registration before the change; the send-time and no-historical-term mutants are killed. | |
| +| Opus P3-3, Astra 3: the plan classified by `Pin` where the dispositions say `Within` | the plan rewritten in terms of `Within(tenantRoot)` for relative and absolute spellings alike, with the sibling-under-one-pin and absolute-in-tree cases; the inventory code (Task 2's first slice) uses `Within`. | |
| +| Opus P3-4, Astra 5: `Parent` and `Within` for early results | documented: an `Absent` result and a `Link` before the last component carry the pin but no `Dir` or `Parent`; ask `Kind` first; `Within` answers false for them and for a nil root. | |
| +| Opus P3-5: the design's justification of the earlier-of rule, `closeNow`'s order, the invocation check missing from the look's list | revision 11 states what a look must do for its start to be the bound (the start stamped first; the witness, the chains, the invocation and the files each observed; order immaterial), the earlier-of rule as a backstop; `closeNow`'s last look is "as any look". | |
| +| Astra: a later witness change after an undiscovered file change did not move the witness | fixed. | |
| +| Astra 6: "closed once" in the spike note; the send test's comment | corrected. | |
| + |
diff --git a/docs/superpowers/plans/2026-10-03-replicator-authority-plan.md b/docs/superpowers/plans/2026-10-03-replicator-authority-plan.md| index 61aa37ec7..c0545298a 100644 |
| --- a/docs/superpowers/plans/2026-10-03-replicator-authority-plan.md |
| +++ b/docs/superpowers/plans/2026-10-03-replicator-authority-plan.md |
| @@ -1,10 +1,10 @@ |
| # The replicator's authority: the task plan for the policy-independent parts |
| -Date: 2026-10-03. For `docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md` (revision 9). This is the plan's steps 1 to 3 as tasks, each its own reviewed commit on `design-replicator-pinned-root`, each with the full `internal/ops`, `internal/lease`, `internal/usage`, `internal/registry` and `internal/activator` run. Step 0's admission model and step 1's first task (`internal/authority`) are done and under their third code review; the VFS spike (step 0's other half) needs a box with amd64 and arm64 and gates Part B only. Decisions 10 to 13 and approval H are parameters: nothing below chooses them, and nothing below is wired into a running fleet until the design's support conditions are declared or checked. |
| +Date: 2026-10-03. For `docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md` (revision 11). This is the plan's steps 1 to 3 as tasks, each its own reviewed commit on `design-replicator-pinned-root`, each with the full `internal/ops`, `internal/lease`, `internal/usage`, `internal/registry` and `internal/activator` run. Step 0's admission model and step 1's first task (`internal/authority`) are done, four code reviews answered; the VFS spike (step 0's other half) needs a box with amd64 and arm64 and gates Part B only. Decisions 10 to 13 and approval H are parameters: nothing below chooses them, and nothing below is wired into a running fleet until the design's support conditions are declared or checked. |
| ## Task 1 (done): `internal/authority` |
| -`Dir`, `Root`, `Walk`, `Confine`, `Result.Pin`, the Part A tests, descriptor accounting. Reviews one and two answered; review three running. |
| +`Dir`, `Root`, `Walk`, `Confine`, `Result.Parent`, `Result.Within`, `Result.Pin` (the platform root an absolute walk entered; never a tenancy boundary), the Part A tests, descriptor accounting. Reviews one to four answered. |
| ## Task 2: the inventory on `Dir`s (Part A's second half) |
| @@ -12,13 +12,13 @@ Date: 2026-10-03. For `docs/superpowers/specs/2026-10-03-replicator-pinned-roots |
| **The platform-link predicate on descriptors.** `resolvePlatformLinks(dir string)` becomes `platformDir(pins, dir string) (*authority.Dir, string)`: from the root's `Dir`, each remaining component is `Child(name, nil)`; a component that is a link (`ErrLink`) is read with `Readlink` from its directory's `Dir` and must satisfy exactly today's predicate (the link's directory the platform's, the link itself the platform's by `Lookat`'s facts, the target walked with `Walk(target, pins)`: relative from the link's directory, absolute from the pinned `/`, with `..` only in the leading run, which `Walk` enforces, no further link, which `Walk`'s `Link` class refuses, ending at a directory whose parent is the platform's); the result's `Dir` is the next component's parent and the walk continues beneath it. A tenant root so reached is `Confine`d once by the inventory before anything walks from it. The predicate's restrictions do not change; its error strings stay, because the Accept list and the rendering compare them. |
| -**`strictTreeDBs` on a `Dir`.** `strictTreeDBs(root string)` keeps its signature and its three string lists (paths spelled as today, `root` joined with the names the listing gave, so the Accept list and every existing test compare unchanged) and becomes a walk on `Dir`s: `List` for the entries; a subdirectory by `Child(name, &entry.Facts)` (a changed entry, `ENOTDIR`, `ErrLink` or absent is churn, as a vanished entry is today; any other error is "cannot be read"); a regular file's header by `OpenRegular(name, entry.Facts)`; a link's target by `Readlink` and `Walk(target, pins)` from the directory that listed it, classified by the design's explicit classes and nothing silent: `Directory`, or a database-named link, is "a link that may lead to a database"; `Regular` within the tenant's root (`Result.Pin == nil`) is a skipped link entry, as today; `Regular` under another pin (`Result.Pin != nil`) is "a link out of the tree"; `Link` is "a link to a link that may lead to a database" (today's classification followed it; this refuses rather than follows); `Other` is "a link to something that is neither a file nor a directory"; `Absent` is churn; `ErrAscentPastRoot`, `ErrOutside` and `ErrNotPlatform` are "a link out of the tree"; `ErrAscentAfterName`, `ErrNotDirectory` and every other error are "a link whose target cannot be looked at". Depth and dot-directory rules are unchanged. `statTarget` and `linktarget_*.go` are deleted. |
| +**`strictTreeDBs` on a `Dir`.** `strictTreeDBs(root string)` keeps its signature and its three string lists (paths spelled as today, `root` joined with the names the listing gave, so the Accept list and every existing test compare unchanged) and becomes a walk on `Dir`s: `List` for the entries; a subdirectory by `Child(name, &entry.Facts)` (a changed entry, `ENOTDIR`, `ErrLink` or absent is churn, as a vanished entry is today; any other error is "cannot be read"); a regular file's header by `OpenRegular(name, entry.Facts)`; a link's target by `Readlink` and `Walk(target, pins)` from the directory that listed it, classified by the design's explicit classes and nothing silent: `Directory`, or a database-named link, is "a link that may lead to a database"; `Regular` within the tenant's root (`Result.Within(tenantRoot)`, whether the target was spelled relative or absolute) is a skipped link entry, as today; `Regular` or `Directory` not within it (a sibling tenant under the same pin, another pin) is "a link out of the tree"; `Link` is "a link to a link that may lead to a database" (today's classification followed it; this refuses rather than follows); `Other` is "a link to something that is neither a file nor a directory"; `Absent` is churn; `ErrAscentPastRoot`, `ErrOutside` and `ErrNotPlatform` are "a link out of the tree"; `ErrAscentAfterName`, `ErrNotDirectory` and every other error are "a link whose target cannot be looked at". Depth and dot-directory rules are unchanged. `statTarget` and `linktarget_*.go` are deleted. |
| **`checkOwnedFile` on a chain.** The chain is acquired downward from the platform root as `Dir`s (the root, the predicate's result, each component by `Child`), never by `Lstat` of a joined path; each check it makes today (no link, one filesystem, a regular file with one name, the owner rules by kind, the `-wal`/`-shm`/`-journal` siblings regular with one name, by `Lookat` from the file's directory) is made on the retained chain; `fileFacts` gains the file's directory `Dir` (the design: one descriptor stack per owned file, counted in the fleet's rendering), kept for the fleet's life so every later look runs `Recheck` on it and `Lookat` of the file's name, and so litestream's opens (Part B, later) take it. `fleetInventory` closes the chains of files it does not keep. |
| **The namespace condition.** A route whose instance runs in its own mount namespace is classified in the agent's namespace and rendered as such; until the support condition is declared it is a refusal rule (a problem naming the route), not a silence. |
| -**Tests.** Every existing owners test keeps passing with its strings; added, from the design's Part A list at the inventory level: each link class rendered as written and none silent (a directory target, a database-named link, a regular file in the tree, a regular file under another pin, a link to a link, a FIFO target, an absent target, an ascent past the tenant root, an absolute target outside every pin, a non-platform component in an absolute target); a tenant root reached through systemd's relative link shape and through an absolute one; Astra 2's layout refused at the root; a swap of the tenant directory between the listing and the classification changing nothing; the retained chain's `Recheck` at the next look reporting a moved or replaced directory; the descriptor count per fleet equal to the retained stacks' total. |
| +**Tests.** Every existing owners test keeps passing with its strings; added, from the design's Part A list at the inventory level: each link class rendered as written and none silent (a directory target, a database-named link, a regular file in the tree, a regular file under another pin, a regular file in a sibling tenant under the same pin, an absolute target inside the tenant's own tree (skipped, not out of the tree), a link to a link, a FIFO target, an absent target, an ascent past the tenant root, an absolute target outside every pin, a non-platform component in an absolute target); a tenant root reached through systemd's relative link shape and through an absolute one; Astra 2's layout refused at the root; a swap of the tenant directory between the listing and the classification changing nothing; the retained chain's `Recheck` at the next look reporting a moved or replaced directory; the descriptor count per fleet equal to the retained stacks' total. |
| ## Task 3: required coverage (Part D) |
diff --git a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md| index 9213313b5..731e669ad 100644 |
| --- a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md |
| +++ b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md |
| @@ -1,6 +1,6 @@ |
| # The replicator's authority: retained descriptors, a durable admission, claims by identity |
| -Date: 2026-10-03. Status: design, revision 10 (revision 9's correction of the lower bound refined after the third code review: the historical term's threshold is the earlier of the registry proof and the last clean look's start, since a witness change is known only to be after the proof; an empty terminal, unissued or cancelled, never sent and is not a settlement for that term; and every look reads the witness and rechecks every retained chain before it inspects files, so a clean look's start bounds every kind of change. Revision 9 was one mechanics correction to the uncertainty's lower bound, found by the second code review of the admission model: an admission admitted before the last clean look, still in flight across a change after it and settled clean before the change was noticed, was outside the bound; the bound now also takes the admission instant of every admission settled at or after the last clean look's start; the invariant I2 is unchanged and the model's named test and schedules cover it). Revision 8 was the accepted text: revision 7 was accepted with fixes by Astra (no P1; one P2: a negative read-back was not conclusive while the admission writer could still commit, and the pending set had three definitions; one P3: the restore wording made a salt mismatch imply a snapshot), both applied here. Revision 6 was rejected by Astra on one P1: a discovery whose write failed had no rule for the admissions that settled before its retry, so the replayed interval could lose a settlement; and three P2s: a helper dying before its recorder started left an admission nobody could finish; the transition table lacked the abort edges and the pending set's cleanup; the lineage record cited a durability discipline the shadow state does not have; each answered here. Revision 5 was rejected by Astra on two P1s: the admission's insertion had no ordering point against discovery, so a discovery between the proof and the commit counted nothing and a later send fell outside the closed uncertainty; construction did not backfill already-closed intervals for a successor's new owners before acknowledgement; and P2s: the transition table and the helper-death rule disagreed and the recorder participant was synthesised while its worker could still run; proof-only callers of admit would have created admissions with no terminal; a terminal `.` lost the directory requirement; conflicting summaries; each answered here. Revision 4 was rejected by Astra on four P1s: the helper has several connections of its own and needs SQLite's within-process lock bookkeeping between them; the producer fence did not cover a helper that outlives the agent with an admission in hand; an intermediate fleet closed before acknowledging broke transitive protection; a fleet could be marked closed with a discovery uncommitted; and four P2s: a dead helper's admissions had no terminal in the running agent, the sleeping binding persisted a reusable inode, the lineage predicate named header fields that identify nothing, the walk's grammar refused a `.` target the predicate accepts; each answered here. Revision 3 was rejected by Astra on five P1s: two SQLite VFSs in one process cannot coordinate through POSIX locks, since the library's own per-inode bookkeeping is in-process; a recorder that abandons early could settle an admission before its transport ended; an admission-only barrier does not cover a discovery whose uncertainty write failed after every admission settled; links at acknowledgement contradicted acknowledging only after settlement, and an inherited uncertainty vanished at the next successor; the ledger's lock does not prove the old process gone; and four P2s: closure at zero pending and the margin's extra day, sleeping claims with no binding, absolute and `.` spellings in the walk, `(dev, ino)` as a lineage; each answered here. Revision 2 was rejected by Astra on three P1s: the VFS delegated SQLite's Unix file methods, which open the SHM and check moved files by pathname themselves; every settled admission wrote a permanent hold, so ordinary replication never read complete; a late owner-scoped extension did not reach successors that had already acknowledged; and six P2s: orphan admissions never terminated, `..` and chain edges unspecified, `dup` sharing the directory offset, the platform-link predicate not preserved and terminal links unclassified, the uid producer without a lifecycle, one billing owner not one replicator; each answered here. Revision 1 was rejected by Astra on five P1s: SQLite canonicalises a `/proc` pathname before it opens anything and this driver passes no `nofollow`; `os.Root` confines but re-resolves every name, so a swap between a listing and an inspection still moves the answer; a `Start` row is not an admission, since the meter sends without one; the attempt-derived window lost a request completed before the change was noticed and the days between an admission and a finish; `closed_at` was not a handover; plus the directory open before `O_DIRECTORY`, per-owner holds the ledger cannot store, a uid with no producer, I3 against Part D, and tests). Branch `design-replicator-pinned-root`, off `feat/carloku-metered-replicator-20261001` at `e1280811`. It answers the eleven findings the twentieth review deferred (`DISPOSITIONS-metered-replicator.md`, review twenty) and keeps decisions 10 to 13 and approval H (`DECISIONS-FOR-PAUL.md`, section D, on the launch branch) as parameters. Nothing is built, wired or applied. |
| +Date: 2026-10-03. Status: design, revision 11 (the fourth code review: the historical term's filter named `finished` and `abandoned` and so excluded `unrecorded`, a settlement whose transport did send; it now excludes only the empty terminals, `unissued` and `cancelled`; the look's order is stated as what safety needs rather than a sequence; the closing look agrees). Revision 10 was revision 9's correction of the lower bound refined after the third code review: the historical term's threshold is the earlier of the registry proof and the last clean look's start, since a witness change is known only to be after the proof; an empty terminal, unissued or cancelled, never sent and is not a settlement for that term; and every look reads the witness and rechecks every retained chain before it inspects files, so a clean look's start bounds every kind of change. Revision 9 was one mechanics correction to the uncertainty's lower bound, found by the second code review of the admission model: an admission admitted before the last clean look, still in flight across a change after it and settled clean before the change was noticed, was outside the bound; the bound now also takes the admission instant of every admission settled at or after the last clean look's start; the invariant I2 is unchanged and the model's named test and schedules cover it). Revision 8 was the accepted text: revision 7 was accepted with fixes by Astra (no P1; one P2: a negative read-back was not conclusive while the admission writer could still commit, and the pending set had three definitions; one P3: the restore wording made a salt mismatch imply a snapshot), both applied here. Revision 6 was rejected by Astra on one P1: a discovery whose write failed had no rule for the admissions that settled before its retry, so the replayed interval could lose a settlement; and three P2s: a helper dying before its recorder started left an admission nobody could finish; the transition table lacked the abort edges and the pending set's cleanup; the lineage record cited a durability discipline the shadow state does not have; each answered here. Revision 5 was rejected by Astra on two P1s: the admission's insertion had no ordering point against discovery, so a discovery between the proof and the commit counted nothing and a later send fell outside the closed uncertainty; construction did not backfill already-closed intervals for a successor's new owners before acknowledgement; and P2s: the transition table and the helper-death rule disagreed and the recorder participant was synthesised while its worker could still run; proof-only callers of admit would have created admissions with no terminal; a terminal `.` lost the directory requirement; conflicting summaries; each answered here. Revision 4 was rejected by Astra on four P1s: the helper has several connections of its own and needs SQLite's within-process lock bookkeeping between them; the producer fence did not cover a helper that outlives the agent with an admission in hand; an intermediate fleet closed before acknowledging broke transitive protection; a fleet could be marked closed with a discovery uncommitted; and four P2s: a dead helper's admissions had no terminal in the running agent, the sleeping binding persisted a reusable inode, the lineage predicate named header fields that identify nothing, the walk's grammar refused a `.` target the predicate accepts; each answered here. Revision 3 was rejected by Astra on five P1s: two SQLite VFSs in one process cannot coordinate through POSIX locks, since the library's own per-inode bookkeeping is in-process; a recorder that abandons early could settle an admission before its transport ended; an admission-only barrier does not cover a discovery whose uncertainty write failed after every admission settled; links at acknowledgement contradicted acknowledging only after settlement, and an inherited uncertainty vanished at the next successor; the ledger's lock does not prove the old process gone; and four P2s: closure at zero pending and the margin's extra day, sleeping claims with no binding, absolute and `.` spellings in the walk, `(dev, ino)` as a lineage; each answered here. Revision 2 was rejected by Astra on three P1s: the VFS delegated SQLite's Unix file methods, which open the SHM and check moved files by pathname themselves; every settled admission wrote a permanent hold, so ordinary replication never read complete; a late owner-scoped extension did not reach successors that had already acknowledged; and six P2s: orphan admissions never terminated, `..` and chain edges unspecified, `dup` sharing the directory offset, the platform-link predicate not preserved and terminal links unclassified, the uid producer without a lifecycle, one billing owner not one replicator; each answered here. Revision 1 was rejected by Astra on five P1s: SQLite canonicalises a `/proc` pathname before it opens anything and this driver passes no `nofollow`; `os.Root` confines but re-resolves every name, so a swap between a listing and an inspection still moves the answer; a `Start` row is not an admission, since the meter sends without one; the attempt-derived window lost a request completed before the change was noticed and the days between an admission and a finish; `closed_at` was not a handover; plus the directory open before `O_DIRECTORY`, per-owner holds the ledger cannot store, a uid with no producer, I3 against Part D, and tests). Branch `design-replicator-pinned-root`, off `feat/carloku-metered-replicator-20261001` at `e1280811`. It answers the eleven findings the twentieth review deferred (`DISPOSITIONS-metered-replicator.md`, review twenty) and keeps decisions 10 to 13 and approval H (`DECISIONS-FOR-PAUL.md`, section D, on the launch branch) as parameters. Nothing is built, wired or applied. |
| ## What stands today |
| @@ -44,11 +44,11 @@ The VFS is the plan's first spike and it must prove, before anything else of Par |
| **Proof and admission are two things.** Fleet construction, `Open` and every watch tick ask the ownership *proof* (today's `admit`: the witness unchanged, the fleet not stale) and create nothing; only the request gate (`lease.RequestGate`, asked by the helper for each physical request) performs an *admission*, which is a proof followed by a row, so an idle healthy fleet has no admission and nothing bars its days. **The admission is a row, written before the send, with one ordering point against discovery.** Under a *discovery mutex* on the fleet (a new requirement: today `admit` and `lookAgain` do not share one, and the admission comments allow a discovery to run unlocked; this design serialises registration, the recheck and the start of a discovery on it) the gate checks the proof and, if the fleet is not stale and no discovery is in progress, registers the admission in the fleet's in-memory *pending set* with its `admitted_at`; it releases the mutex and commits the row in the durability ledger's own database (`admissions`: `token`, `fleet_id`, `owner account and app`, `admitted_at`, `transport_done_at`, `recorder_started_at`, `recorder_done_at`, `settled_at`, `how`), `synchronous=FULL`, within a bounded budget; after the commit it takes the mutex again and, if the fleet went stale or a discovery began since registration, marks the row `unissued` and refuses. Discovery, under the same mutex, sets the in-progress flag and counts the pending set, durable or not yet, as unsettled admissions when it computes its lower bound, and a registered admission that the discovery has counted and that then commits is inside the uncertainty (it was counted); one that commits after the discovery began is refused. So an admission is either counted by every discovery that follows its registration or refused, and Astra's 23:58:10 sequence (proof, discovery, commit, a send on the 4th) ends in a refusal at the recheck, not a send outside the uncertainty. The gate waits for the commit. A commit that does not return within the budget refuses the request (`ErrAdmissionNotDurable`; litestream sees a failed upload and does not advance) and the goroutine that awaited it stays to see the commit land and then marks the row `how = unissued, settled_at = now` in its own transaction, so a late commit never authorises anything and never blocks a day; if the process dies between, recovery classifies the row as below. The meter's `Start` row carries the token (`Start` may still fail or be late, as today; what is now mandatory is the admission, not the `Start`). An admission has two participants, the transport and the recorder, and is settled by whichever finishes last. The transport writes `transport_done_at` from the SDK middleware's finalize step, or `transport-lost` when its helper is proven gone (below). The recorder writes `recorder_done_at` with its outcome: `finished` (`Finish`), `abandoned` (`Abandon`), or `unrecorded` (the request path, when `Start` failed and made no attempt row, which today calls neither; it now writes this terminal); the recorder participant is never synthesised while its worker can still run: today's meter lets recording workers outlive the request path, and the admission stays unsettled (barring) until that worker finishes or abandons. The recorder runs in the agent, fed by the helper's messages over the fleet socket (`Start`, `Finish`, `Abandon` with the token), and the agent *registers* the recorder participant when it receives `Start` (`recorder_started_at`, under an agent-owned lifecycle guard per helper); a `Start` that the agent receives after it has begun the helper's termination handling is refused (the guard is closed first, then the socket drained, so registration and exit handling cannot interleave). The participant that finds the other already done writes `settled_at = max(transport_done_at, recorder_done_at)` and `how`, and performs, in that same transaction, the uncertainty extension or closure below. **The transition table is authoritative and is the plan's model:** states `registered` (in memory only), `admitted` (durable), `transport done`, `recorder done`, `settled`; edges `registered → admitted` (the commit), `admitted → unissued` (the recheck after the commit found the fleet stale or a discovery begun, or the gate's budget elapsed before the answer was returned: the row is rewritten as the terminal and the helper never receives the token), `registered → cancelled` (the admission writer has returned with a definite failure, or the writer's handle is closed and a fresh read then finds no row: the registration leaves the pending set), `admitted → transport done | recorder done`, `transport done → settled` (the recorder's completion), `recorder done → settled` (the transport's completion or `transport-lost`), and `admitted | transport done | recorder done → recovered-unknown` at process recovery only (all missing timestamps `now`); `transport-lost` is a transport completion, not a terminal, so an admission whose recorder is still running after its helper died stays `recorder pending`. **The pending set has one contract.** It holds every registration not yet resolved, and an entry leaves it in exactly two ways, both under the discovery mutex: (a) the admission row is durable, at which point the row carries the responsibility (the removal follows the commit, so a discovery sees the entry or the row and never neither); (b) the cancellation is *conclusive*, at which point the empty-settlement result is recorded for every discovery that counted it (the pending-discovery latch's counted set, or the open uncertainty's closure test, which ranges over rows and pending registrations alike), so an uncertainty that waited only on it closes then. The same empty-settlement rule applies to a counted admission that ends `unissued`. **A cancellation is conclusive only when the admission writer can no longer commit:** the writer is one goroutine owning the transaction, the gate's budget expiring refuses the request but does not resolve the registration, and the registration waits for the writer to return. A writer that returns having committed takes `admitted` (then `unissued`, since the request was refused); one that returns with a definite failure takes `cancelled`; one that cannot tell (the connection lost around the commit) is resolved by a read-back by `token` that begins only after the writer's handle is closed, on a read transaction opened after that close, so nothing it fails to find can be committed afterwards: a row found takes `admitted → unissued`; none found takes `cancelled`; the read is retried until it answers. There is no edge out of `cancelled`. Astra's sequence (the writer still running at the budget's expiry and the discovery's count, a read at 23:58:00.040, the commit at 23:58:00.050) cannot declare a cancellation, because the read waits for the writer; the writer's commit resolves it as `unissued`, and the discovery that counted it is told once. Every terminal write is keyed by `token` and idempotent, retried until it commits. Admissions are the ledger's pending state moved to before the send and given an owner. |
| -**Two kinds of hold.** A *barrier* is the ledger's completeness rule: a day is not published complete for an admission's owner while an admission of that owner admitted on or before that day is unsettled (box-wide while Part C2's owner scope is not in use); it is a query over `admissions`, writes nothing, and lifts at settlement. An *uncertainty* is a row (`uncertainties`: `id`, `fleet_id`, `from`, `to` null while open, `reason`) written when a fleet's authority is found changed (by the witness, by `Recheck`, by a changed file), in the transaction that also writes the holds for the days of `[from, now]` for every owner the uncertainty reaches: `bound = min(the registry proof, the last clean look's start)`; `from = min(bound, the earliest admitted_at among the fleet's admissions that are unsettled, or settled with how in {finished, abandoned} and settled_at >= bound) - margin` (revision 9: the first two terms alone missed an admission admitted before the look, in flight across the change, and settled clean before the discovery; such a settlement wrote nothing permanent, so its admission instant must bound the uncertainty; revision 10: the threshold is the bound itself, not the look alone, because a witness change is known only to be after the proof, and an empty terminal, unissued or cancelled, is excluded since it never sent). A look begins by reading the witness and running `Recheck` on every retained chain, then inspects the files, so a look that finds nothing is clean against every kind of change from its start. If discovery finds no admission of the fleet unsettled, the uncertainty is opened and closed in that transaction (`to = discovery + margin`). While an uncertainty is open, settlements of that fleet's admissions extend it: each settlement, in its own transaction, writes the holds for every day of `[its admitted_at, its settled_at]` for every owner the uncertainty reaches, and the last settlement closes it with `to = max(discovery, that settlement) + margin` and materialises every day of the closed interval, the margin's extra day across midnight included; recovery uses the same helper and advances the publication watermark past the days it materialised. An admission that settles while no uncertainty of its fleet is open writes nothing permanent: the ordinary day of an unchanged fleet becomes complete when its barrier lifts. The multiple-midnights sequence (admitted on the 2nd, the change at 23:58:10, sent on the 3rd, finished on the 4th) holds the 2nd, 3rd and 4th through the settlement's interval, whichever participant finished last; the request completed before the change was noticed is inside the lower bound as today. **If the discovery transaction fails** the barrier is not enough (every admission may already be settled): discovery first latches a *pending discovery* in the ledger's in-memory failure overlay (`latchFailure`, extended to carry the lower bound and the owners reached), which the publisher's snapshot already overlays and detects across a drain (today's `snapshotOnce` and `drainFailures` behaviour, extended rather than replaced: a failed drain must not stop the overlay from making the snapshot incomplete), so every day from the bound reads incomplete for those owners until the uncertainty commits; the fleet refuses every request meanwhile and retries the write. The latch carries the lower bound, the owners reached and the tokens of the admissions the discovery counted; settlements of those admissions meanwhile find no uncertainty open and write no hold, but their rows record `settled_at` as always. **The replay is one transaction:** it opens the uncertainty with the original `from`; for each counted token whose row is settled it writes the holds for `[its admitted_at, its settled_at]` for every owner reached (and for a token that was cancelled or unissued, nothing); if any counted token is still unsettled the uncertainty stays open and the usual settlement rule closes it later; otherwise it closes with `to = replay instant + margin` (which is no earlier than the discovery and every counted settlement) and materialises every day of the closed interval; the overlay clears only after that commit, so no snapshot sees neither the latch nor the row. Astra's sequence (T counted at 23:58:10 on the 2nd, the write failing, T settling at 00:02 on the 4th, the replay at 00:03) writes the 2nd, 3rd and 4th through T's interval and closes at 00:04 on the 4th, and a successor constructed after the replay backfills that closed interval for its owners; the fleet cannot be marked `closed` while the discovery is uncommitted (above); a process that dies with the latch held leaves a fleet not `closed`, which recovery covers from the fleet's `opened_at`. |
| +**Two kinds of hold.** A *barrier* is the ledger's completeness rule: a day is not published complete for an admission's owner while an admission of that owner admitted on or before that day is unsettled (box-wide while Part C2's owner scope is not in use); it is a query over `admissions`, writes nothing, and lifts at settlement. An *uncertainty* is a row (`uncertainties`: `id`, `fleet_id`, `from`, `to` null while open, `reason`) written when a fleet's authority is found changed (by the witness, by `Recheck`, by a changed file), in the transaction that also writes the holds for the days of `[from, now]` for every owner the uncertainty reaches: `bound = min(the registry proof, the last clean look's start)`; `from = min(bound, the earliest admitted_at among the fleet's admissions that are unsettled, or settled with settled_at >= bound and how not in {unissued, cancelled}) - margin`, the bound fixed before the rows are read and never the running minimum (revision 9: the first two terms alone missed an admission admitted before the look, in flight across the change, and settled clean before the discovery; such a settlement wrote nothing permanent, so its admission instant must bound the uncertainty; revision 10: the threshold is the bound itself, not the look alone; revision 11: every settlement whose transport ran counts, `unrecorded` included, and only the empty terminals, which never sent, are excluded; `transport-lost` is a transport completion, never a value of `how`; a `recovered-unknown` row has its own interval and need not be counted here). **What a look must do for its start to be the bound:** the look's start instant is stamped before its first observation, and every observation it makes (the witness, `Recheck` of every retained chain, the route's recorded invocation against systemd's, the files) sees any change that persists, so a look that finds nothing is clean against every kind of change from its start; the order of the observations within a look does not matter for that, and the earlier-of rule (the proof and the look) is kept as a backstop for a look built without one of them. If discovery finds no admission of the fleet unsettled, the uncertainty is opened and closed in that transaction (`to = discovery + margin`). While an uncertainty is open, settlements of that fleet's admissions extend it: each settlement, in its own transaction, writes the holds for every day of `[its admitted_at, its settled_at]` for every owner the uncertainty reaches, and the last settlement closes it with `to = max(discovery, that settlement) + margin` and materialises every day of the closed interval, the margin's extra day across midnight included; recovery uses the same helper and advances the publication watermark past the days it materialised. An admission that settles while no uncertainty of its fleet is open writes nothing permanent: the ordinary day of an unchanged fleet becomes complete when its barrier lifts. The multiple-midnights sequence (admitted on the 2nd, the change at 23:58:10, sent on the 3rd, finished on the 4th) holds the 2nd, 3rd and 4th through the settlement's interval, whichever participant finished last; the request completed before the change was noticed is inside the lower bound as today. **If the discovery transaction fails** the barrier is not enough (every admission may already be settled): discovery first latches a *pending discovery* in the ledger's in-memory failure overlay (`latchFailure`, extended to carry the lower bound and the owners reached), which the publisher's snapshot already overlays and detects across a drain (today's `snapshotOnce` and `drainFailures` behaviour, extended rather than replaced: a failed drain must not stop the overlay from making the snapshot incomplete), so every day from the bound reads incomplete for those owners until the uncertainty commits; the fleet refuses every request meanwhile and retries the write. The latch carries the lower bound, the owners reached and the tokens of the admissions the discovery counted; settlements of those admissions meanwhile find no uncertainty open and write no hold, but their rows record `settled_at` as always. **The replay is one transaction:** it opens the uncertainty with the original `from`; for each counted token whose row is settled it writes the holds for `[its admitted_at, its settled_at]` for every owner reached (and for a token that was cancelled or unissued, nothing); if any counted token is still unsettled the uncertainty stays open and the usual settlement rule closes it later; otherwise it closes with `to = replay instant + margin` (which is no earlier than the discovery and every counted settlement) and materialises every day of the closed interval; the overlay clears only after that commit, so no snapshot sees neither the latch nor the row. Astra's sequence (T counted at 23:58:10 on the 2nd, the write failing, T settling at 00:02 on the 4th, the replay at 00:03) writes the 2nd, 3rd and 4th through T's interval and closes at 00:04 on the 4th, and a successor constructed after the replay backfills that closed interval for its owners; the fleet cannot be marked `closed` while the discovery is uncommitted (above); a process that dies with the latch held leaves a fleet not `closed`, which recovery covers from the fleet's `opened_at`. |
| **Who an uncertainty reaches, and what a fleet inherits.** Reach is computed over the chain, not stored per uncertainty: every fleet row names its predecessor, and a fleet's *unacknowledged ancestry* is the set of ancestors reached by following predecessors through fleets that have not been acknowledged (an acknowledged step ends the walk, because acknowledgement copies). An uncertainty, whenever it is opened, extended or closed, writes holds for the owners of its fleet and of every fleet whose unacknowledged ancestry contains that fleet (a query at write time, so an uncertainty discovered after a successor's construction reaches it, and so does one on a grandparent when the parent closed unopened without acknowledging); and **construction backfills**: the transaction that writes a new fleet's `open` row also writes, for the new fleet's owners, the holds of every interval already held by any uncertainty of its unacknowledged ancestry, open or closed (a successor built at 23:58:20 against a fleet whose uncertainty closed at 23:58:10 holds the 2nd for its owners from its first instant, before any acknowledgement), and the publisher's pending-discovery overlay reaches a fleet's owners through the same ancestry query; the barrier for an owner consults the unsettled admissions of its fleet and of its whole unacknowledged ancestry. Acknowledgement is terminal and **root-first**: a fleet may acknowledge its predecessor only when the predecessor is `closed` and has itself acknowledged its own predecessor (or has none), and it copies the predecessor's effective set (own and inherited, open and closed) into its inherited set (`inherited`: `fleet_id`, `uncertainty_id`) and writes holds for the closed ones its owners have not been held for, in one transaction; after that the chain walk stops there and the copy carries on. Astra's sequence: A has U open and an admission unsettled; B is built (its ancestry: A) and closes unopened without acknowledging; C is built against B (its ancestry: B, then A, since B has not acknowledged); on the 4th A's settlement extends U and the write reaches X, B's owners and C's owners through the ancestry; when A closes, B acknowledges A (root-first), then C acknowledges B and inherits U. Under owner scope the October sequence: Y, built at 23:58:20 with A in its ancestry, is barred on the 3rd by A's unsettled admission and held on the 4th by the settlement's write. |
| -**The fleet journal and the handover.** One row per fleet (`fleets`: `fleet_id`, `box`, `witness_generation`, `owners`, `opened_at`, `state`, `predecessor`, `acknowledged_by`). States and the transaction each is written in: `open` at build, before any admission, with the construction links above; `stale` when an uncertainty is opened; `closing` when the helper has exited and the fleet has released its witness; `closed` when every admission of the fleet is settled and no discovery of the fleet is uncommitted (a discovery whose write failed is retried, and the closure transaction carries any still-pending discovery's uncertainty with it, so a fleet is closed with that uncertainty committed or not closed at all; the recorder exposes a wait on settlement; `closeNow` waits, bounded, and past the bound the row stays `closing`, with its admissions still barring and its uncertainties still open: a late worker is a late settlement, and nothing about it is lost). Before the helper is told to stop, `closeNow` keeps today's ordering: replication stops first, then one last look at the files and one last reading of the witness, then the witness is released; a change found by that last look is a discovery like any other. A successor acknowledges a predecessor only when the predecessor is `closed`, or when recovery has closed it; acknowledgement writes `acknowledged_by`, copies the predecessor's effective uncertainties (its own and inherited, open and closed) into the successor's inherited set, and writes holds for the closed ones the successor's owners have not yet been held for, in one transaction. A `closed` predecessor whose effective set is empty contributes nothing: routine replacement of a healthy chain holds no day. An unopened intermediate fleet (built and closed without replicating) has its construction links and is acknowledged like any other, so the chain's barriers and inheritance pass through it. |
| +**The fleet journal and the handover.** One row per fleet (`fleets`: `fleet_id`, `box`, `witness_generation`, `owners`, `opened_at`, `state`, `predecessor`, `acknowledged_by`). States and the transaction each is written in: `open` at build, before any admission, with the construction links above; `stale` when an uncertainty is opened; `closing` when the helper has exited and the fleet has released its witness; `closed` when every admission of the fleet is settled and no discovery of the fleet is uncommitted (a discovery whose write failed is retried, and the closure transaction carries any still-pending discovery's uncertainty with it, so a fleet is closed with that uncertainty committed or not closed at all; the recorder exposes a wait on settlement; `closeNow` waits, bounded, and past the bound the row stays `closing`, with its admissions still barring and its uncertainties still open: a late worker is a late settlement, and nothing about it is lost). Before the helper is told to stop, `closeNow` keeps today's ordering: replication stops first, then one last look (the witness, the chains and the files, as any look), then the witness is released; a change found by that last look is a discovery like any other. A successor acknowledges a predecessor only when the predecessor is `closed`, or when recovery has closed it; acknowledgement writes `acknowledged_by`, copies the predecessor's effective uncertainties (its own and inherited, open and closed) into the successor's inherited set, and writes holds for the closed ones the successor's owners have not yet been held for, in one transaction. A `closed` predecessor whose effective set is empty contributes nothing: routine replacement of a healthy chain holds no day. An unopened intermediate fleet (built and closed without replicating) has its construction links and is acknowledged like any other, so the chain's barriers and inheritance pass through it. |
| **The producer fence, and recovery at process start.** The ledger's own lock does not prove the old process gone: `DurabilityLedger.Close` releases it when its bounded wait ends with work in flight, and a request admitted before could still be sent after. So dispatch is fenced separately: a *producer fence*, an `flock` on `admissions.lock` in the ledger's directory, taken by the agent before its first admission on an open file description it then passes to every helper it starts (over the same `SCM_RIGHTS` message as the directories, before the helper may send anything; a helper that has not received it refuses to dispatch), never released by a timeout and released by the kernel only when the agent and every helper holding that description have exited; every admission's commit requires the fence held (checked under the ledger's mutex before `BEGIN`). A helper that outlives its agent with an admission in hand therefore still holds the fence, and a new agent cannot take it, and so cannot recover, until that helper is gone; a helper's exit is observed by the agent as its child's `waitpid`, never inferred from a closed socket, and `PR_SET_PDEATHSIG` is set in the helper as a convenience that shortens the wait and proves nothing. Recovery requires the fence, which is the verified termination of every old producer. Recovery takes the fence first and, holding it, in one transaction before any fleet is built: every admission of this box that is unsettled is classified `how = recovered-unknown` with all three timestamps `now`, an uncertainty opened and closed for it at once over `[admitted_at - margin, now + margin]` for its owner (box-wide while owner scope is not in use), its days materialised; every fleet not `closed` is marked `closed` with an uncertainty over `[min(opened_at, its earliest admission) - margin, now + margin]` if it had none open, or its open uncertainty closed at `now + margin` and materialised; every fleet with no `acknowledged_by` is acknowledged, root-first, by the first fleet the new process builds, with the inheritance and holds above. Orphans therefore terminate, conservatively, and nothing blocks beyond its recovery; a producer that is somehow still alive cannot send, because the fence is no longer its. |
diff --git a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md| index 3d549fd24..f34f93395 100644 |
| --- a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md |
| +++ b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md |
| @@ -18,11 +18,11 @@ Findings for `2026-10-03-replicator-pinned-roots-design.md`: the first two secti |
| Plan step 0's second spike is code, kept in tree at `internal/ops/admissionmodel` (not wired, imported by nothing): Part C's transition table (`registered`, `admitted`, `transport done`, `recorder done`, `settled`, `unissued`, `cancelled`, `recovered-unknown`), the barrier and the uncertainty, the pending set under the discovery mutex, the pending-discovery latch and its one-transaction replay, construction backfill, reach over the unacknowledged ancestry, root-first acknowledgement, helper death with the lifecycle guard, the producer fence and process recovery, as plain Go over an integer clock with no SQLite. The model keeps a *truth* apart from the ledger it simulates (when the authority really changed, when each transport really began and ended, which helpers outlived the agent) and the tests check the ledger's answers against it. |
| -- **The named sequences are tests**, one each: an unchanged fleet holds nothing; the three-midnight interval in both completion orders (closes at the settlement plus the margin); Astra's commit-after-discovery (unissued, the uncertainty closed once by the empty settlement); review 7's budget expiry then commit; a definite failure cancels and an ambiguous commit is read back either way with the pending set empty after; zero-pending discovery closes at once and holds the margin's extra day across midnight; a failed discovery's latch bars and refuses until the replay, which with nothing pending closes at the replay instant plus the margin; review 6's replay with a counted settlement (the 2nd, 3rd and 4th held, closed at 00:04, a successor built after the replay backfilled); Astra's A, B, C construction and root-first acknowledgement (C refused before B acknowledged A; C inherits U); helper death before and after recorder registration, a `Start` refused after the guard closed; the fence outliving the agent (recovery refused until the helper is gone; recovered-unknown covers the transport that finished after the crash); a healthy chain contributing nothing; and the lower bound reaching a request completed before the change was noticed (the clean look minus the margin). |
| +- **The named sequences are tests**, one each: an unchanged fleet holds nothing; the three-midnight interval in both completion orders (closes at the settlement plus the margin); Astra's commit-after-discovery (unissued, the uncertainty closed by the empty settlement); review 7's budget expiry then commit; a definite failure cancels and an ambiguous commit is read back either way with the pending set empty after; zero-pending discovery closes at once and holds the margin's extra day across midnight; a failed discovery's latch bars and refuses until the replay, which with nothing pending closes at the replay instant plus the margin; review 6's replay with a counted settlement (the 2nd, 3rd and 4th held, closed at 00:04, a successor built after the replay backfilled); Astra's A, B, C construction and root-first acknowledgement (C refused before B acknowledged A; C inherits U); helper death before and after recorder registration, a `Start` refused after the guard closed; the fence outliving the agent (recovery refused until the helper is gone; recovered-unknown covers the transport that finished after the crash); a healthy chain contributing nothing; and the lower bound reaching a request completed before the change was noticed (the clean look minus the margin). |
| - **The boundaries are separate actions** (after the first code review): the writer's commit, the gate's answer (the recheck), a definite failure, an ambiguous return and its read-back, the send (the helper beginning the transport, which needs a durable issued row, recorded as a violation otherwise; a dead helper's send is a no-op, since a dead helper does nothing), the helper's proven exit (the guard closes) and the drain (transport-lost, unrecorded) are each their own step, so a schedule can put a discovery, a budget expiry or a crash between a commit and its answer, hold a token for a day before sending, or ask for a recorder's `Start` between the exit and the drain. The composites the named tests use (`WriterReturns`, `HelperDies`) are those steps in order. |
| - **Randomised schedules**: every action above in random interleavings over about four days, 120 steps a schedule, one owner per fleet (owner scope; the box-wide default is a superset); after each step: the barrier, stated from the chain and not from the publisher (for every fleet and every owner of it, a durable unsettled admission of that fleet or of any fleet in its unacknowledged ancestry bars the owner from its day on, whether or not the token was ever handed out), the hazard invariant (once the ledger knows of a change, every day on which a transport overlapped the true change is incomplete for its owner; after a crash, every sent admission unsettled at the crash likewise; an issued token never sent has no transport and is covered by the barrier and recovery, not this oracle), a terminal state never changing, and a closed fleet having no latch or pending registration; at quiescence every fleet's owners hold every interval of every uncertainty on its whole chain, no uncertainty is open, and a day with no uncertainty reaching an owner is complete. `ADMISSION_MODEL_SEEDS=30000` passes in about six seconds; the default is 400. Publication is revisable by construction: a day published complete can be re-marked by a later hold (the design's materialisation and watermark), and the hazard invariant is satisfied by that retraction; the barrier's purpose is to make retraction rare, not to make it unnecessary. |
| - **What the runs found.** The first runs found the model's own bookkeeping wrong (an owner the fleet did not have; a crash-killed helper's transport end unset). After the second code review made the change its own action, discovered by a later look, Opus's sequence (an admission admitted before the last clean look, in flight across a change after it, settled clean before the discovery) showed the design's lower bound missing that admission's earlier day: **revision 9 of the design** adds the admission instant of every admission settled at or after the last clean look's start to the bound, and the mutant restoring revision 8's rule is killed by the named test. That is the one interleaving the design did not name that the model has found, within the actions it represents and the invariants it checks; the claim is no wider than that. |
| -- **Mutants, in a tree copy**, each killed by a named test or a schedule. After the third code review: the threshold as the later of proof and look, as the look alone, the historical term including empty terminals, the proof not refusing a moved witness, the crash duplicating a landed row, `Close` without its unsettled loop, the latch overlay reaching the fleet's owners only. After the second code review: revision 8's bound (the in-flight test), the bound without the proof (the proof test), the bound without the clean look (the lower-bound test), a landed ambiguous row not durable until read-back, the open interval dropped from construction backfill (the per-step inheritance check), the replay's per-token writes dropped (the replay-while-open test), a read-back leaving the pending set entry. Removing the closed-implies-no-unsettled *check* removes an oracle; the mechanism mutant it exists for, `Close` without its unsettled-admissions loop, is killed by it (an unanswered durable row). Putting the send's terminal check before its gate is equivalent in the schedules tested (a settled, issued, unsent token exists after a clean stop, but no schedule sends it afterwards). After the first code review: the budget expiry a no-op (its own test, with no discovery); the barrier owner-only, or over issued rows only (the successor-barred test and the schedules); the pending set skipped at registration; the guard ignored, and the drain before the guard; the replay clearing the latch without the lower bound's holds (a named test: the schedules did not reach it in 3000 seeds); the send unchecked; a close without the replay (the closed-implies-no-latch check); acknowledgement copying the predecessor's own uncertainties only (not equivalent: a schedule found a fifth fleet's owner unheld for the first fleet's uncertainty, because the chain's copies are how a closed interval reaches a fleet built after its predecessor acknowledged); the answer ignoring the refusal; a read-back while the writer runs (the named test; the later commit would land on a cancelled registration, which the terminal check reports). Equivalent under this model: the unacknowledged-ancestry walk not stopping at an acknowledged step (over-reach writes the same holds). Not equivalent, though once claimed so here: the registry proof in the bound (Astra's schedule: a build, a clean look a day later, a discovery a day after that, with no admission: only the proof reaches the first day; and Opus's: a witness change known only to be after the proof; both are named tests). First: no construction backfill (reach); the pending set not counted (the commit-after-discovery tests); no recheck after commit (the same test, and a hazard at seed 264); the replay dropping counted settlements (hazard); the replay closing at the discovery instant (liveness and the latch tests); a settlement writing no interval (hazard); recovery ignoring the fence (the fence test); helper death without transport-lost (an uncertainty open at quiescence); the lower bound ignoring the clean look (the lower-bound test; the 30000-schedule sweep alone did not find it, which is why that sequence is a named test); the lower bound ignoring the earliest unsettled admission (liveness, because the model's proof then reached too far); unrecorded synthesised for a registered worker (the guard test); recovery skipping unclosed fleets (an uncertainty open at quiescence); acknowledgement not root-first and reach ignoring successors (reach). An epoch check made redundant by the stale state is the one equivalent mutant, noted in the model. |
| +- **Mutants, in a tree copy**, each killed by a named test or a schedule. After the fourth code review: the historical term filtered to finished and abandoned (the unrecorded test), the cutoff as the running minimum (the fixed-bound test in both row orders), the historical term using the send instant, the historical term dropped, a later witness change ignored (the proof test). After the third code review: the threshold as the later of proof and look, as the look alone, the historical term including empty terminals, the proof not refusing a moved witness, the crash duplicating a landed row, `Close` without its unsettled loop, the latch overlay reaching the fleet's owners only. After the second code review: revision 8's bound (the in-flight test), the bound without the proof (the proof test), the bound without the clean look (the lower-bound test), a landed ambiguous row not durable until read-back, the open interval dropped from construction backfill (the per-step inheritance check), the replay's per-token writes dropped (the replay-while-open test), a read-back leaving the pending set entry. Removing the closed-implies-no-unsettled *check* removes an oracle; the mechanism mutant it exists for, `Close` without its unsettled-admissions loop, is killed by it (an unanswered durable row). Putting the send's terminal check before its gate is equivalent in the schedules tested (a settled, issued, unsent token exists after a clean stop, but no schedule sends it afterwards). After the first code review: the budget expiry a no-op (its own test, with no discovery); the barrier owner-only, or over issued rows only (the successor-barred test and the schedules); the pending set skipped at registration; the guard ignored, and the drain before the guard; the replay clearing the latch without the lower bound's holds (a named test: the schedules did not reach it in 3000 seeds); the send unchecked; a close without the replay (the closed-implies-no-latch check); acknowledgement copying the predecessor's own uncertainties only (not equivalent: a schedule found a fifth fleet's owner unheld for the first fleet's uncertainty, because the chain's copies are how a closed interval reaches a fleet built after its predecessor acknowledged); the answer ignoring the refusal; a read-back while the writer runs (the named test; the later commit would land on a cancelled registration, which the terminal check reports). Equivalent under this model: the unacknowledged-ancestry walk not stopping at an acknowledged step (over-reach writes the same holds). Not equivalent, though once claimed so here: the registry proof in the bound (Astra's schedule: a build, a clean look a day later, a discovery a day after that, with no admission: only the proof reaches the first day; and Opus's: a witness change known only to be after the proof; both are named tests). First: no construction backfill (reach); the pending set not counted (the commit-after-discovery tests); no recheck after commit (the same test, and a hazard at seed 264); the replay dropping counted settlements (hazard); the replay closing at the discovery instant (liveness and the latch tests); a settlement writing no interval (hazard); recovery ignoring the fence (the fence test); helper death without transport-lost (an uncertainty open at quiescence); the lower bound ignoring the clean look (the lower-bound test; the 30000-schedule sweep alone did not find it, which is why that sequence is a named test); the lower bound ignoring the earliest unsettled admission (liveness, because the model's proof then reached too far); unrecorded synthesised for a registered worker (the guard test); recovery skipping unclosed fleets (an uncertainty open at quiescence); acknowledgement not root-first and reach ignoring successors (reach). An epoch check made redundant by the stale state is the one equivalent mutant, noted in the model. |
| - **What the model does not cover**, by construction: the latch clearing after the commit as two instants (the replay is one step here; the rule stays with the ledger's tests), a snapshot between those instants, the recorder worker's lifetime and the socket drain as separate events, the fence as anything but helper liveness, retries of a failed terminal or replay write, the ledger's commit latency on a box's disk under the replicator's request rate (the spike's other half, which needs a box), Part C2's owner scope beyond the owner-scoped holds the model writes, and process kills inside a transaction (the model's transactions are atomic by fiat; the ledger's are SQLite's). |
| ## The fork's pathname entry points (read 2026-10-03 08:25, every call, not a sample) |
diff --git a/internal/authority/authority.go b/internal/authority/authority.go| index 280b5d532..600aaae4e 100644 |
| --- a/internal/authority/authority.go |
| +++ b/internal/authority/authority.go |
| @@ -11,6 +11,7 @@ type Facts struct { |
| Dev, Ino uint64 |
| UID uint32 |
| Mode uint32 // the file type and permission bits as the kernel has them |
| + Size int64 // for a regular file; not part of Same or Equal, since it changes as the file is written |
| } |
| // Same reports whether two facts name the same object of the same type: |
| @@ -115,13 +116,16 @@ func (p *Pins) match(f Facts) *Root { |
| } |
| // Result is what a Walk found: the kind of the last component, its facts, |
| -// for a directory a retained Dir for it, for anything else the retained |
| -// Dir that holds it (Parent), and for an absolute spelling the pinned |
| -// root it entered (nil for a relative walk, which stays in the root it |
| -// started in). Pin is the platform root, never a tenancy boundary: two |
| -// tenants beneath one pin share it, so Within is the question to ask of |
| -// a target. Close releases what the walk opened and nothing it was given; |
| -// Parent and Dir are valid until then. |
| +// for a directory a retained Dir for it, for a regular file or an "other" |
| +// the retained Dir that holds it (Parent), and for an absolute spelling |
| +// the pinned root it entered (nil for a relative walk, which stays in the |
| +// root it started in). An Absent result, and a Link found before the last |
| +// component, are classified early: they carry the Pin but no Dir or |
| +// Parent, so ask Kind first; Within answers false for them. Pin is the |
| +// platform root, never a tenancy boundary: two tenants beneath one pin |
| +// share it, so Within is the question to ask of a resolved target. Close |
| +// releases what the walk opened and nothing it was given; Parent and Dir |
| +// are valid until then. |
| type Result struct { |
| Kind Kind |
| Facts Facts |
| @@ -137,6 +141,9 @@ type Result struct { |
| // and compared by identity. A walk that popped above root, or entered |
| // another pin, answers false. It is only meaningful before Close. |
| func (r *Result) Within(root *Dir) bool { |
| + if root == nil { |
| + return false |
| + } |
| start := r.Dir |
| if r.Kind != Directory { |
| start = r.Parent |
diff --git a/internal/authority/authority_other.go b/internal/authority/authority_other.go| index cfe6869e5..ffc361322 100644 |
| --- a/internal/authority/authority_other.go |
| +++ b/internal/authority/authority_other.go |
| @@ -38,6 +38,7 @@ type Root struct { |
| } |
| func OpenRoot(*Dir, string, Platform) (*Root, error) { return nil, ErrUnsupported } |
| +func SlashRoot(*Dir, Platform) (*Root, error) { return nil, ErrUnsupported } |
| func (r *Root) Ancestry() []Facts { return nil } |
| func (r *Root) AncestryChanged() (bool, error) { return true, ErrUnsupported } |
| func (r *Root) Close() error { return nil } |
diff --git a/internal/authority/authority_unix.go b/internal/authority/authority_unix.go| index af08fc6fc..c4139caf6 100644 |
| --- a/internal/authority/authority_unix.go |
| +++ b/internal/authority/authority_unix.go |
| @@ -28,7 +28,7 @@ type Dir struct { |
| } |
| func factsOf(st *unix.Stat_t) Facts { |
| - return Facts{Dev: uint64(st.Dev), Ino: uint64(st.Ino), UID: st.Uid, Mode: uint32(st.Mode)} |
| + return Facts{Dev: uint64(st.Dev), Ino: uint64(st.Ino), UID: st.Uid, Mode: uint32(st.Mode), Size: st.Size} |
| } |
| func kindOf(mode uint32) Kind { |
| @@ -492,6 +492,21 @@ func OpenRoot(slash *Dir, path string, platform Platform) (*Root, error) { |
| return &Root{Dir: cur, Path: path, slash: slash, comps: comps, ancestry: ancestry, platform: platform}, nil |
| } |
| +// SlashRoot pins the slash itself as a root: the deliberate form of what |
| +// OpenRoot refuses by accident ("/"). An absolute walk against pins that |
| +// hold it enters at once. The slash must pass the platform rule; it is |
| +// not confined (it has no parent to pop to) and Close closes nothing, |
| +// since the slash is the caller's. |
| +func SlashRoot(slash *Dir, platform Platform) (*Root, error) { |
| + if err := slash.live(); err != nil { |
| + return nil, err |
| + } |
| + if !platformOK(slash.facts, platform) { |
| + return nil, &EdgeError{Name: "/", Err: ErrNotPlatform} |
| + } |
| + return &Root{Dir: slash, Path: "/", slash: slash, platform: platform}, nil |
| +} |
| + |
| // Ancestry is the facts of each component of the root's walk, top down. |
| func (r *Root) Ancestry() []Facts { return append([]Facts(nil), r.ancestry...) } |
diff --git a/internal/authority/authority_unix_test.go b/internal/authority/authority_unix_test.go| index 1acd54167..72a4e0a8d 100644 |
| --- a/internal/authority/authority_unix_test.go |
| +++ b/internal/authority/authority_unix_test.go |
| @@ -726,6 +726,25 @@ func TestWithinAndMatchedPin(t *testing.T) { |
| } |
| } |
| +// Within against no root, and for an early result, answers false. |
| +func TestWithinEarlyResults(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "d")) |
| + link(t, "d", filepath.Join(base, "ld")) |
| + res, err := slash.Walk("d", nil) |
| + if err != nil || res.Within(nil) { |
| + t.Fatalf("Within(nil): %v %v", res.Within(nil), err) |
| + } |
| + res.Close() |
| + for _, sp := range []string{"nothing", "ld/x"} { |
| + res, err := slash.Walk(sp, nil) |
| + if err != nil || res.Parent != nil || res.Dir != nil || res.Within(slash) { |
| + t.Fatalf("Walk(%q): parent %v dir %v within %v err %v", sp, res.Parent, res.Dir, res.Within(slash), err) |
| + } |
| + } |
| +} |
| + |
| // Recheck looks at each edge without following a link: a retained |
| // directory renamed aside and replaced by a link to itself is a changed |
| // edge, though the link resolves to the same directory. |
diff --git a/internal/ops/admissionmodel/model.go b/internal/ops/admissionmodel/model.go| index afe8db335..2fc809157 100644 |
| --- a/internal/ops/admissionmodel/model.go |
| +++ b/internal/ops/admissionmodel/model.go |
| @@ -316,8 +316,8 @@ func (m *Model) Change(f *Fleet) { |
| func (m *Model) WitnessChange(f *Fleet) { |
| if f.ChangedAt == unset { |
| f.ChangedAt = m.Now |
| - f.witnessMoved = true |
| } |
| + f.witnessMoved = true // a later witness change after an undiscovered file change still moves the witness |
| } |
| // Register is the gate's first half: under the discovery mutex, proof then |
| @@ -557,22 +557,24 @@ func (m *Model) Discover(f *Fleet, fail bool) { |
| } |
| f.DiscoveredAt = m.Now |
| counted := map[int]*Admission{} |
| - from := f.proof |
| - if f.lastCleanLook < from { |
| - from = f.lastCleanLook |
| + // the bound is fixed before the rows are read: the earlier of the |
| + // registry proof and the last clean look's start |
| + bound := f.proof |
| + if f.lastCleanLook < bound { |
| + bound = f.lastCleanLook |
| } |
| + from := bound |
| for _, a := range f.Admissions { |
| if a.unsettled() { |
| counted[a.Token] = a |
| } |
| - // revision 9: an admission settled (both participants complete; |
| - // not an empty terminal, which never sent) at or after the earlier |
| - // of the registry proof and the last clean look's start may have |
| - // been in flight across the change, so its admission instant bounds |
| - // the uncertainty too (the second code review found the look case; |
| - // the third, the proof case: a witness change the look may not have |
| - // read is known only to be after the proof) |
| - if a.unsettled() || (a.State == Settled && a.SettledAt >= from) { |
| + // revisions 9 and 10: an admission settled (both participants |
| + // complete, whatever the recorder's outcome, unrecorded included; |
| + // not an empty terminal, which never sent) at or after the bound |
| + // may have been in flight across the change, so its admission |
| + // instant lowers from too; the cutoff is the bound, never the |
| + // running minimum, so the answer does not depend on row order |
| + if a.unsettled() || (a.State == Settled && a.SettledAt >= bound) { |
| if a.AdmittedAt < from { |
| from = a.AdmittedAt |
| } |
diff --git a/internal/ops/admissionmodel/model_test.go b/internal/ops/admissionmodel/model_test.go| index 2682d00a7..d40ea9377 100644 |
| --- a/internal/ops/admissionmodel/model_test.go |
| +++ b/internal/ops/admissionmodel/model_test.go |
| @@ -544,8 +544,8 @@ func TestReadBackOnlyAfterTheHandleCloses(t *testing.T) { |
| must(t, m) |
| } |
| -// A send needs a durable, issued admission and a live helper; the model |
| -// records the attempt otherwise. |
| +// A send needs a durable, issued admission; the model records an attempt |
| +// without one. A dead helper's send is a no-op (a dead helper does nothing). |
| func TestSendNeedsDurableIssuedAdmission(t *testing.T) { |
| m := New(1) |
| m.Now = at(1, 10, 0) |
| @@ -761,7 +761,9 @@ func TestHistoricalTermExcludesEmptyTerminals(t *testing.T) { |
| } |
| // Review 3 (Astra): a token admitted on one day and sent the next: the |
| -// historical term uses the admission instant, not the send. |
| +// historical term uses the admission instant, not the send. The proof is |
| +// moved past the look by a later registration, so only the historical |
| +// term can reach day 1 (review 4). |
| func TestHistoricalTermUsesTheAdmissionInstant(t *testing.T) { |
| m := New(1) |
| m.Now = at(1, 9, 0) |
| @@ -772,6 +774,9 @@ func TestHistoricalTermUsesTheAdmissionInstant(t *testing.T) { |
| m.Send(a) |
| m.Now = at(2, 0, 30) |
| m.Look(f) |
| + m.Now = at(2, 0, 32) |
| + p := m.Register(f, alice) // the proof moves past the look |
| + m.WriterFails(p) |
| m.Now = at(2, 0, 35) |
| m.Change(f) |
| m.Now = at(2, 0, 40) |
| @@ -784,6 +789,92 @@ func TestHistoricalTermUsesTheAdmissionInstant(t *testing.T) { |
| held(t, m, alice, 1, 2) |
| } |
| +// Review 4 (both): a settlement whose recorder ended unrecorded still |
| +// sent; it counts for the historical term like any settlement. |
| +func TestHistoricalTermCountsUnrecordedSettlements(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 0) |
| + a := issue(t, m, f, alice) |
| + m.Now = at(2, 0, 30) |
| + m.Look(f) |
| + m.Now = at(2, 0, 35) |
| + p := m.Register(f, alice) |
| + m.WriterFails(p) |
| + m.Now = at(2, 0, 40) |
| + m.Change(f) |
| + m.Now = at(2, 0, 50) |
| + m.TransportDone(a) |
| + m.RecorderDone(a, "unrecorded") |
| + if a.State != Settled || a.How != "unrecorded" { |
| + t.Fatalf("%s %q", a.State, a.How) |
| + } |
| + m.Now = at(2, 1, 0) |
| + m.Look(f) |
| + if u := f.Uncertainties[0]; u.From != at(1, 22, 59) { |
| + t.Fatalf("from %d, want %d", u.From, at(1, 22, 59)) |
| + } |
| + held(t, m, alice, 1, 2) |
| + must(t, m) |
| +} |
| + |
| +// Review 4 (Astra): a witness change after an undiscovered file change |
| +// still moves the witness, so the next proof refuses the request. |
| +func TestLaterWitnessChangeRefusesTheProof(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 10, 0) |
| + m.Change(f) |
| + m.Now = at(1, 10, 5) |
| + m.WitnessChange(f) |
| + m.Now = at(1, 10, 10) |
| + if m.Register(f, alice) != nil { |
| + t.Fatal("a request admitted after the witness moved") |
| + } |
| + if f.DiscoveredAt != at(1, 10, 10) { |
| + t.Fatal("the proof did not discover") |
| + } |
| +} |
| + |
| +// Review 4 (both): the cutoff is the bound, fixed before the rows are |
| +// read, so a settlement before the bound never qualifies through another |
| +// row's earlier admission, in either row order. |
| +func TestHistoricalCutoffIsTheFixedBound(t *testing.T) { |
| + for _, reversed := range []bool{false, true} { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 50) |
| + a2 := m.Register(f, alice) // the slow writer |
| + m.Now = at(1, 23, 55) |
| + a1 := m.Register(f, alice) |
| + first, second := a1, a2 |
| + if reversed { |
| + first, second = a2, a1 |
| + } |
| + m.WriterCommits(first) |
| + m.GateAnswers(first) |
| + m.WriterCommits(second) |
| + m.GateAnswers(second) |
| + m.Send(a1) |
| + m.Send(a2) |
| + m.Now = at(1, 23, 58) |
| + finish(m, a2) // settled before the bound; a1 stays unsettled |
| + m.Now = at(2, 0, 30) |
| + m.Look(f) |
| + p := m.Register(f, alice) |
| + m.WriterFails(p) |
| + m.Now = at(2, 0, 40) |
| + m.Change(f) |
| + m.Look(f) |
| + if u := f.Uncertainties[0]; u.From != at(1, 23, 54) { |
| + t.Fatalf("reversed=%v: from %d, want a1's admission minus the margin %d (a2 settled before the bound must not count)", reversed, u.From, at(1, 23, 54)) |
| + } |
| + } |
| +} |
| + |
| // Review 3 (Astra 3): a landed ambiguous commit, then a crash before the |
| // read-back: one row, recovered-unknown, held. |
| func TestLandedAmbiguousThenCrash(t *testing.T) { |