amadan
Review two answered; design revision 9: the uncertainty's lower bound also takes the admission instant of every admission settled at or after the last clean look's start (an in-flight request across a change, settled clean before the discovery, was outside it); the model's change is its own action discovered by a later look, a landed ambiguous row is durable at once, a per-step inheritance check, closed implies no unsettled admission, explicit quiescence, five new tests; authority reports the pin an absolute walk ended beneath, keeps the errno before a pin, and its tests distinguish Equal from Same, observe close-on-exec and count descriptors across refused opens, ancestry rewalks and Root.Close; dispositions and the spike note corrected
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
10 files changed,
+379
−34
DISPOSITIONS-replicator-pinned-root.md+24 −0docs/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+8 −3internal/authority/authority_linux_test.go+52 −1internal/authority/authority_unix.go+15 −4internal/authority/authority_unix_test.go+48 −3internal/authority/doc.go+3 −2internal/ops/admissionmodel/model.go+81 −11internal/ops/admissionmodel/model_test.go+143 −5
CI passed — run details
diff --git a/DISPOSITIONS-replicator-pinned-root.md b/DISPOSITIONS-replicator-pinned-root.md| index 1f7923bf3..603daacf2 100644 |
| --- a/DISPOSITIONS-replicator-pinned-root.md |
| +++ b/DISPOSITIONS-replicator-pinned-root.md |
| @@ -21,3 +21,27 @@ Opus: accept with fixes, no P1, three P2. Astra: reject, five P2, two P3. Report |
| | Astra 4: boundaries collapsed; two tests that could not kill their subject | commit, answer, failure, ambiguous return, read-back, send, exit and drain are separate actions; `TestBudgetExpiryWithoutDiscovery`, `TestBetweenCommitAndAnswer` (a discovery and a crash between), `TestReadBackOnlyAfterTheHandleCloses`, `TestSendNeedsDurableIssuedAdmission`, a fresh eligible participant in the guard test; the three-midnight test now sends on the 3rd. | |
| | Opus: `Close` without the replay; acknowledgement holds possibly redundant; the proof term never binding; `unackAncestry` over-reach | a closed-implies-no-latch check; acknowledgement copying own-only is not equivalent (a schedule found it); the proof term and the over-reach are equivalent under the model and the spike note says why. | |
| | Astra 7, Opus P3-6: a leaked result in the swap test; the spike note's header and overstated claims | fixed; the note's header, the boundary and barrier claims, and the three-midnight comment corrected. | |
| + |
| +## Review two (of `50a6f056`: the first review answered) |
| + |
| +Opus: accept with fixes, no P1, one P2. Astra: accept with fixes, no P1, two P2, two P3. Reports: `logs/opus-replroot-review2.md`, `logs/astra-replroot-review2.md`. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| Opus P2-1: the driver never produced the window between a change and its discovery, and that window hid a gap in the design's lower bound (an admission admitted before the last clean look, in flight across a change after it, settled clean before the discovery: its earlier day stayed complete) | **Design revision 9**: the bound also takes the admission instant of every admission settled at or after the last clean look's start (I2 unchanged; the ruling is mechanics under the design's own invariant, recorded here and in the design's status line for the owner to see). The driver's `Change` is its own action, discovered by a later `Look`; `TestLowerBoundReachesInFlightAcrossCleanLook` is Opus's sequence with the exact `from`; the 30000-schedule sweep passes with changes free-running; the mutant restoring revision 8's rule is killed. | |
| +| Astra 1: a landed ambiguous commit invisible to the barrier until read-back | the row is durable when it lands (bars like any durable unsettled row) while the registration stays pending until the read-back transfers it; `TestLandedAmbiguousCommitBarsBeforeReadBack` (owner and successor, both outcomes); the mutant deferring durability is killed. | |
| +| Astra 2: `Child(expect)` and `Equal` not distinguished by tests | `Child` after a mode-only change and with an owner-different expectation; `Recheck` after an injected owner change; mutants `Equal → Same` in `Child`, `Equal` without uid, without mode, all killed. | |
| +| Astra 3: the proof term is not an equivalent mutant | `TestLowerBoundProofTerm` (Astra's schedule, exact `from`); the equivalence claim withdrawn; the mutant killed. | |
| +| Astra 4, Opus P3-1: the mutation claims exceeded the tests | the descriptor test now covers `d/nothing/x`, `d/ld/x`, `d/inner/../x`, a refused `OpenRegular`, the ancestry rewalk in both outcomes, a three-component `Root.Close`, and observes `FD_CLOEXEC` on acquired and opened descriptors; the claim below names what is killed, what is equivalent and what is unobservable. | |
| +| Opus P3-2: an absolute spelling from a confined tenant reaches another pin and the result could not say so | `Result.Pin` names the pinned root an absolute walk ended beneath (nil for a relative walk); `doc.go` reworded to "a relative walk never leaves the root it started in". | |
| +| Opus P3-3: every pre-pin error became `ErrOutside` | only `ENOENT`, `ENOTDIR` and `ErrLink` do; the rest keep their errno (tested with `EACCES`). | |
| +| Opus P3-4: the slash pin only reachable by tests | documented at the branch; kept. | |
| +| Opus P3-5: no step-by-step inheritance invariant | `Check` requires, after every step, each fleet's owners held for every interval of its effective set (closed whole; open through the discovery and through each counted settlement); the open-interval backfill mutant is killed. | |
| +| Opus P3-6: `Confine` changes a shared Dir | documented: the tenant root's owner calls it once, before handing the Dir on. | |
| +| Astra: `Closed` should imply no durable unsettled admission; quiescence explicit | both added to `Check` and `CheckQuiescent`. | |
| +| Astra: a replay with one settled token and one unresolved registration; a held token sent after the crash | `TestReplayWritesSettledTokenWhileOpen`, `TestFenceHeldTokenSentAfterCrash`. | |
| +| Opus: `Send` read the ledger's terminal state before the gate | reordered: the gate's conditions first. | |
| +| Wording (both): `ReadBack`'s comment, the dead-helper send, "closes once", `authority.go`'s Same comment, twelve not thirteen, the "no interleaving found" claim | corrected in the code and the spike note; the claim is limited to the represented actions and tested invariants. | |
| + |
| +**What the authority mutants establish, precisely.** Killed by a named assertion: each of `O_DIRECTORY`, `O_NOFOLLOW` (`Child`), `O_NONBLOCK` (`OpenRegular`), `O_CLOEXEC` (both opens, by `F_GETFD`); kernel `..` for the pop; the uid check and the mode check of the platform walk; `Child` comparing identity only, `Equal` without uid or without mode; `Recheck` checking identity only or this edge only; `AncestryChanged` without its platform recheck or its deferred close; `List` by `dup`; `Child` without the expect check; no `Confine`; the pin's intermediates kept; `Result.Pin` unset; the pre-pin errno lost; `Result.Close` a no-op; `Dir.Close` without the syscall; `Root.Close` a no-op; the close on `Walk`'s error path, on an absent or a linked intermediate, on `OpenRoot`'s error path, on `Child`'s expect mismatch, on `OpenRegular`'s mismatch. Equivalent: the close in `List`'s identity check (`openat(fd, ".")` cannot be another directory); `O_RDONLY` (zero). Unobservable by these tests: `O_NOCTTY` (no terminal in the test), and the in-loop `..` checks made dead by the grammar pass. |
| + |
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 fbdf5f855..f28149b6d 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 8; 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 9 (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 |
| @@ -10,7 +10,7 @@ The replicator (`internal/ops/litestream_metered.go`, `litestream_owners.go`; pa |
| **I1, identity through retained descriptors.** (a) *Containment*: no operation of the replicator or of litestream on a tenant's files resolves a pathname above the directory the fleet accepted for that file; (b) *retention*: the descriptor that listed a directory is the descriptor against which its entries are inspected, its links read, their targets classified and its files opened, for that look, so the inspection uses the same directory authority as the listing and acquisition refuses a mismatching identity (an entry inside a retained directory can still change; what cannot happen is an answer about one directory being applied to another); (c) *acceptance*: an owned file is opened by the descriptor of its accepted directory with no link followed in the last component, and the opened file's `(dev, ino)` equals the accepted facts before any use. Retention is authority over directories and checked identities, not a frozen inventory, and it has two roots: the *accepted traversal root* (a platform root or a tenant root) through which acquisition and link classification may traverse retained ancestors, and the *accepted immediate directory* of an owned file, which every data open uses and nothing else. Ancestor replacement cannot redirect an operation, and an identity mismatch at acquisition refuses use; entries inside a retained directory can change, and a swap put back between two looks is not detected by looking; what (a) to (c) promise is that no operation is steered by such a change, and that every change a look does see is held for. Ascent never uses the kernel's `..`: it pops the retained stack. Each acquisition compares what it opened with the facts of the entry it was acquired from, and each later look compares every named edge (parent descriptor, name) with the retained child's facts, so a moved or replaced component is seen as a change at the next look. |
| -**I2, a durable admission, two kinds of hold.** No request is sent until a row naming it (fleet, owner, admission instant) is durable. A *barrier* is temporary: a day is not published complete for an admission's owner while that admission is unsettled, and lifts when it settles. An *uncertainty* is permanent: an interval written when a fleet's authority is found changed, from the earlier of today's lower bound (the registry proof, the last clean look's start) and the earliest admission of the fleet then unsettled, minus the margin, open until every admission of the fleet is settled, then closed at the latest settlement plus the margin; it holds its days for the fleet's owners and for every owner linked to it (below). An admission that settles with no uncertainty open on its fleet writes nothing permanent: the ordinary day of an unchanged fleet becomes complete. Discovery and its first hold are recorded in one transaction; if that transaction fails, a publication-visible *pending discovery* (the ledger's failure latch, extended with the lower bound) bars every day from that bound for every owner the fleet reaches until the write succeeds, and the fleet refuses every request meanwhile. Settlement is the last of the recorder's and the transport's completions, written by whichever lands last, with the upper bound no earlier than both. A fleet reaches, from its construction, every uncertainty and every unsettled admission of every ancestor not yet acknowledged, existing or discovered later; acknowledgement is root-first and copies the predecessor's whole effective set, open and closed, into the successor's; a fleet's construction materialises, for its owners, every interval its ancestry already holds; a fleet is never closed with a discovery of its own uncommitted. A discovery whose write failed is replayed as one transaction that opens the uncertainty at the original lower bound, materialises the settlement of every admission it counted that settled meanwhile, and closes it only if none of them remains unsettled; the overlay clears after that commit and never before. |
| +**I2, a durable admission, two kinds of hold.** No request is sent until a row naming it (fleet, owner, admission instant) is durable. A *barrier* is temporary: a day is not published complete for an admission's owner while that admission is unsettled, and lifts when it settles. An *uncertainty* is permanent: an interval written when a fleet's authority is found changed, from the earliest of today's lower bound (the registry proof, the last clean look's start) and the admission instant of every admission of the fleet then unsettled or settled at or after the last clean look's start (one admitted before the look and still in flight across the change may have settled clean before the change was noticed), minus the margin, open until every admission of the fleet is settled, then closed at the latest settlement plus the margin; it holds its days for the fleet's owners and for every owner linked to it (below). An admission that settles with no uncertainty open on its fleet writes nothing permanent: the ordinary day of an unchanged fleet becomes complete. Discovery and its first hold are recorded in one transaction; if that transaction fails, a publication-visible *pending discovery* (the ledger's failure latch, extended with the lower bound) bars every day from that bound for every owner the fleet reaches until the write succeeds, and the fleet refuses every request meanwhile. Settlement is the last of the recorder's and the transport's completions, written by whichever lands last, with the upper bound no earlier than both. A fleet reaches, from its construction, every uncertainty and every unsettled admission of every ancestor not yet acknowledged, existing or discovered later; acknowledgement is root-first and copies the predecessor's whole effective set, open and closed, into the successor's; a fleet's construction materialises, for its owners, every interval its ancestry already holds; a fleet is never closed with a discovery of its own uncommitted. A discovery whose write failed is replayed as one transaction that opens the uncertainty at the original lower bound, materialises the settlement of every admission it counted that settled meanwhile, and closes it only if none of them remains unsettled; the overlay clears after that commit and never before. |
| **I3, one billing owner and one replication authority by file identity.** A file is billed to one `(account, app)` and replicated by one authority (the external replicator, the activator's hibernation path, or this fleet; today the first two exist and the fleet is unwired); any number of routes of that one owner may claim it through any spelling; two owners on one `(dev, ino)`, or two replication authorities, whether the file is listed or skipped, whether a claimant is live or hibernating, make it unowned (or refused for this fleet) with every claimant named, until an explicit handover of authority exists; every claimant's own authority check must pass; a claim with no identity yet is recorded and reconciled when it resolves; identity grouping is a look, not a snapshot, and relaxes none of today's hard-link, sidecar or filesystem checks; a database's lineage (which replica prefix continues) is a durable record in the shadow state, not an inode number; a required platform database that cannot be reached is an incomplete box. |
| @@ -44,7 +44,7 @@ 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: `from = min(the registry proof, the last clean look's start, the earliest admitted_at of the fleet's admissions then unsettled) - margin`. 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: `from = min(the registry proof, the last clean look's start, the earliest admitted_at among the fleet's admissions that are unsettled or whose settled_at is at or after the last clean look's start) - margin` (revision 9: the second term 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). 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. |
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 e8defb10a..31d77a776 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 |
| @@ -21,8 +21,8 @@ Plan step 0's second spike is code, kept in tree at `internal/ops/admissionmodel |
| - **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 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 and a live helper, and is recorded as a violation otherwise), 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 admission unsettled at the crash likewise), 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 first runs found** was in the model's own bookkeeping, not the design: the driver admitted an owner the fleet did not have (the model now refuses that, as the design implies), and a helper the crash killed left its transport's true end unset so the hazard looked open forever. The design's rules held once the truth was kept correctly; no interleaving the design does not already name was found. |
| -- **Mutants, in a tree copy**, each killed by a named test or a schedule. 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), and the registry proof dropped from the lower bound (every change here is seen by the next look, so the proof is never the earlier term; a witness change the file look cannot see would need its own change kind, which the design does not have). 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 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 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. Two of the second review's suggestions are not mechanism mutants and survive as expected: removing the closed-implies-no-unsettled check is removing an oracle (no mechanism mutant trips it yet), and putting the send's terminal check before its gate is equivalent in the states the model reaches (a terminal admission is never issued and unsent). 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), and and the registry proof is **not** equivalent (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; a named test holds it). 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 7a920e5de..e958ef008 100644 |
| --- a/internal/authority/authority.go |
| +++ b/internal/authority/authority.go |
| @@ -14,7 +14,8 @@ type Facts struct { |
| } |
| // Same reports whether two facts name the same object of the same type: |
| -// identity, which is what acquisition checks against a listing. |
| +// identity alone. List uses it to check its fresh description is this |
| +// directory; Child(expect) and Recheck use Equal. |
| func (f Facts) Same(o Facts) bool { |
| return f.Dev == o.Dev && f.Ino == o.Ino && f.Mode&modeTypeMask == o.Mode&modeTypeMask |
| } |
| @@ -114,12 +115,16 @@ func (p *Pins) match(f Facts) *Root { |
| } |
| // Result is what a Walk found: the kind of the last component, its facts, |
| -// and, for a directory, a retained Dir for it. Close releases what the |
| -// walk opened and nothing it was given. |
| +// for a directory a retained Dir for it, and for an absolute spelling the |
| +// pinned root it ended beneath (nil for a relative walk, which stays in |
| +// the root it started in), so a caller can tell a file reached under |
| +// another root from one under its own. Close releases what the walk |
| +// opened and nothing it was given. |
| type Result struct { |
| Kind Kind |
| Facts Facts |
| Dir *Dir |
| + Pin *Root |
| owned []*Dir |
| } |
diff --git a/internal/authority/authority_linux_test.go b/internal/authority/authority_linux_test.go| index 4144a8e62..4b7ce98a4 100644 |
| --- a/internal/authority/authority_linux_test.go |
| +++ b/internal/authority/authority_linux_test.go |
| @@ -6,6 +6,8 @@ import ( |
| "os" |
| "path/filepath" |
| "testing" |
| + |
| + "golang.org/x/sys/unix" |
| ) |
| func openFDs(t *testing.T) int { |
| @@ -28,6 +30,7 @@ func TestDescriptorsAreReleased(t *testing.T) { |
| write(t, filepath.Join(r, "f"), "x") |
| link(t, "f", filepath.Join(r, "l")) |
| write(t, filepath.Join(r, "d", "inner", "zz"), "x") |
| + link(t, "inner", filepath.Join(r, "d", "ld")) |
| mkdir(t, filepath.Join(base, "other")) |
| write(t, filepath.Join(base, "other", "f"), "x") |
| mkdir(t, filepath.Join(base, "w", "x")) |
| @@ -42,7 +45,7 @@ func TestDescriptorsAreReleased(t *testing.T) { |
| // failing spellings that leave intermediate directories open on the |
| // way: "/other/f" (a platform directory outside every pin), "d/inner/zz/x" |
| // (a file where a directory is needed, two levels down), "d/inner/zz/" |
| - for _, sp := range []string{"d/inner", "d/inner/", "f", "l", "nothing", "d/nothing", "f/x", "f/", "l/x", "/r/d/inner", "/r/f", "/w/x", "/other", "/other/f", "d/inner/zz/x", "d/inner/zz/", "/", "../x", "d/../f"} { |
| + for _, sp := range []string{"d/inner", "d/inner/", "f", "l", "nothing", "d/nothing", "d/nothing/x", "d/ld/x", "d/inner/../x", "f/x", "f/", "l/x", "/r/d/inner", "/r/f", "/w/x", "/other", "/other/f", "d/inner/zz/x", "d/inner/zz/", "/", "../x", "d/../f"} { |
| res, err := root.Walk(sp, pins) |
| if res.Kind == Directory && err == nil && res.Dir != root.Dir { |
| if openFDs(t) <= before { |
| @@ -66,6 +69,54 @@ func TestDescriptorsAreReleased(t *testing.T) { |
| if _, err := OpenRoot(slash, "r/d/missing", me); err == nil { |
| t.Fatal("a root with a missing last component built") |
| } |
| + // a refused OpenRegular, and the ancestry rewalk in both outcomes |
| + _, fFacts, _ := root.Lookat("f") |
| + wrongF := fFacts |
| + wrongF.Ino++ |
| + if _, err := root.OpenRegular("f", wrongF); err == nil { |
| + t.Fatal("another file opened") |
| + } |
| + if _, err := root.OpenRegular("l", fFacts); err == nil { |
| + t.Fatal("a link opened") |
| + } |
| + if changed, err := root.AncestryChanged(); changed || err != nil { |
| + t.Fatal(changed, err) |
| + } |
| + os.Chmod(r, 0o775) |
| + if changed, _ := root.AncestryChanged(); !changed { |
| + t.Fatal("not changed") |
| + } |
| + os.Chmod(r, 0o755) |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("after refused opens and two ancestry rewalks: %d open, %d before", n, before) |
| + } |
| + // a multi-component root's Close releases every descriptor of its walk |
| + mkdir(t, filepath.Join(base, "m", "n", "o")) |
| + mno, err := OpenRoot(slash, "m/n/o", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + if n := openFDs(t); n != before+3 { |
| + t.Fatalf("a three-component root holds %d descriptors, want 3", n-before) |
| + } |
| + mno.Close() |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("after Root.Close: %d open, %d before", n, before) |
| + } |
| + // every descriptor the package opens is close-on-exec |
| + for _, fd := range []int{root.fd, slash.fd} { |
| + if flags, err := unix.FcntlInt(uintptr(fd), unix.F_GETFD, 0); err != nil || flags&unix.FD_CLOEXEC == 0 { |
| + t.Fatalf("fd %d not close-on-exec: %v %v", fd, flags, err) |
| + } |
| + } |
| + fh, err := root.OpenRegular("f", fFacts) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + if flags, err := unix.FcntlInt(fh.Fd(), unix.F_GETFD, 0); err != nil || flags&unix.FD_CLOEXEC == 0 { |
| + t.Fatalf("OpenRegular's fd not close-on-exec: %v %v", flags, err) |
| + } |
| + fh.Close() |
| if n := openFDs(t); n != before { |
| t.Fatalf("after List and three failed roots: %d descriptors open, %d before", n, before) |
| } |
diff --git a/internal/authority/authority_unix.go b/internal/authority/authority_unix.go| index dbc2ab66c..d6f2bf188 100644 |
| --- a/internal/authority/authority_unix.go |
| +++ b/internal/authority/authority_unix.go |
| @@ -267,7 +267,9 @@ func (d *Dir) Recheck() error { |
| // or from anything acquired beneath it cannot pop past it. Its retained |
| // ancestry stays, so Recheck still sees every edge above it. This is how |
| // a tenant root acquired beneath a platform root becomes the tenant's |
| -// boundary. |
| +// boundary. It is not undone, and it changes the Dir for every holder: |
| +// only the owner of a tenant root calls it, once, before handing the Dir |
| +// to anything that walks from it. |
| func (d *Dir) Confine() { d.root = true } |
| // Walk classifies a captured link target. A relative spelling is walked |
| @@ -310,6 +312,7 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| } |
| p = p.parent |
| } |
| + res := Result{} |
| cur := d |
| entered := true // a relative walk is already beneath its root |
| if abs { |
| @@ -319,11 +322,11 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| cur = pins.Slash |
| entered = false |
| if pin := pins.match(pins.Slash.facts); pin != nil { |
| - cur = pin.Dir // slash itself is pinned |
| + cur = pin.Dir // slash itself is pinned (OpenRoot refuses "/", so only a caller pinning its own slash reaches this) |
| entered = true |
| + res.Pin = pin |
| } |
| } |
| - res := Result{} |
| fail := func(err error) (Result, error) { |
| res.Close() |
| return Result{}, err |
| @@ -345,7 +348,14 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| if !entered { |
| child, err := cur.Child(c, nil) |
| if err != nil { |
| - return fail(&EdgeError{Name: c, Err: ErrOutside}) |
| + // absent, a file or a link where a directory is needed: the |
| + // spelling leads outside every pin; any other error (EACCES, |
| + // EMFILE, EIO) is itself, with its errno |
| + var ee *EdgeError |
| + if errors.As(err, &ee) && (errors.Is(ee.Err, unix.ENOENT) || errors.Is(ee.Err, unix.ENOTDIR) || errors.Is(ee.Err, ErrLink)) { |
| + return fail(&EdgeError{Name: c, Err: ErrOutside}) |
| + } |
| + return fail(err) |
| } |
| if !platformOK(child.facts, pins.Platform) { |
| child.Close() |
| @@ -356,6 +366,7 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| res.Close() // the platform directories above the pin are not kept |
| cur = pin.Dir |
| entered = true |
| + res.Pin = pin |
| } else { |
| res.owned = append(res.owned, child) |
| cur = child |
diff --git a/internal/authority/authority_unix_test.go b/internal/authority/authority_unix_test.go| index 60dc9206f..46216e49f 100644 |
| --- a/internal/authority/authority_unix_test.go |
| +++ b/internal/authority/authority_unix_test.go |
| @@ -152,6 +152,13 @@ func TestRootPlatformWalk(t *testing.T) { |
| if err := r.Recheck(); err != nil { |
| t.Fatalf("Recheck after the mode was restored: %v", err) |
| } |
| + // an owner change of a retained ancestor, by injecting the retained |
| + // facts (a test cannot chown): the edge reads as changed |
| + r.parent.facts.UID++ |
| + if err := r.Recheck(); !edgeIs(err, ErrChanged) { |
| + t.Fatalf("Recheck after an owner change: %v", err) |
| + } |
| + r.parent.facts.UID-- |
| if err := os.Rename(filepath.Join(base, "a", "b"), filepath.Join(base, "a", "c")); err != nil { |
| t.Fatal(err) |
| } |
| @@ -347,6 +354,26 @@ func TestListAndChildExpect(t *testing.T) { |
| if _, err := slash.Child("sub", &one[3].Facts); !edgeIs(err, ErrChanged) { |
| t.Fatalf("changed entry acquired: %v", err) |
| } |
| + // the same entry with only its mode changed, and with only its owner |
| + // different in the expectation, is a changed entry too |
| + _, subFacts, _ := slash.Lookat("sub") |
| + if err := os.Chmod(filepath.Join(base, "sub"), 0o700); err != nil { |
| + t.Fatal(err) |
| + } |
| + if _, err := slash.Child("sub", &subFacts); !edgeIs(err, ErrChanged) { |
| + t.Fatalf("mode-only change acquired: %v", err) |
| + } |
| + _, subFacts, _ = slash.Lookat("sub") |
| + otherOwner := subFacts |
| + otherOwner.UID++ |
| + if _, err := slash.Child("sub", &otherOwner); !edgeIs(err, ErrChanged) { |
| + t.Fatalf("an owner difference acquired: %v", err) |
| + } |
| + if c, err := slash.Child("sub", &subFacts); err != nil { |
| + t.Fatalf("the unchanged entry refused: %v", err) |
| + } else { |
| + c.Close() |
| + } |
| for _, bad := range []string{"", ".", "..", "a/b", "a\x00"} { |
| if _, err := slash.Child(bad, nil); !errors.Is(err, ErrBadName) { |
| t.Fatalf("Child(%q): %v", bad, err) |
| @@ -433,12 +460,30 @@ func TestWalkClasses(t *testing.T) { |
| } |
| res.Close() |
| } |
| - // the result of an absolute walk into the pinned root is the pinned Dir |
| + // the result of an absolute walk into the pinned root is the pinned Dir, |
| + // and says which pin it ended beneath; a relative walk names none |
| res, err := root.Walk("/r", pins) |
| - if err != nil || res.Dir != root.Dir { |
| - t.Fatalf("/r is not the pinned root: %v %v", res.Dir, err) |
| + if err != nil || res.Dir != root.Dir || res.Pin != root { |
| + t.Fatalf("/r is not the pinned root: %v %v %v", res.Dir, res.Pin, err) |
| } |
| res.Close() |
| + res, err = root.Walk("/r/f", pins) |
| + if err != nil || res.Pin != root { |
| + t.Fatalf("/r/f does not name its pin: %v %v", res.Pin, err) |
| + } |
| + res, err = root.Walk("f", pins) |
| + if err != nil || res.Pin != nil { |
| + t.Fatalf("a relative walk names a pin: %v %v", res.Pin, err) |
| + } |
| + // an unreadable platform directory before the pin keeps its errno |
| + mkdir(t, filepath.Join(base, "locked", "x")) |
| + os.Chmod(filepath.Join(base, "locked"), 0o000) |
| + defer os.Chmod(filepath.Join(base, "locked"), 0o755) |
| + if os.Geteuid() != 0 { |
| + if _, err := root.Walk("/locked/x", pins); !edgeIs(err, unix.EACCES) { |
| + t.Fatalf("EACCES before the pin: %v", err) |
| + } |
| + } |
| // a walk without pins cannot take an absolute spelling anywhere |
| if _, err := root.Walk("/r/f", nil); !errors.Is(err, ErrOutside) { |
| t.Fatalf("absolute without pins: %v", err) |
diff --git a/internal/authority/doc.go b/internal/authority/doc.go| index 7179486e2..a3839367a 100644 |
| --- a/internal/authority/doc.go |
| +++ b/internal/authority/doc.go |
| @@ -9,8 +9,9 @@ |
| // and resolves it relative to the descriptor alone, with O_NOFOLLOW. List |
| // uses a fresh open file description each time. Walk classifies a captured |
| // link target by components from an anchor, popping the retained stack for |
| -// a leading run of ".." rather than asking the kernel for "..", and never |
| -// leaves the root it started in. A Root is a Dir reached from a pinned "/" |
| +// a leading run of ".." rather than asking the kernel for ".."; a relative |
| +// walk never leaves the root it started in, and an absolute one ends |
| +// beneath a pinned root or is refused, and says which root (Result.Pin). A Root is a Dir reached from a pinned "/" |
| // by a walk whose every component is the platform's. |
| // |
| // Two choices differ from today's pathname code on purpose. An absolute |
diff --git a/internal/ops/admissionmodel/model.go b/internal/ops/admissionmodel/model.go| index 205ddea8b..6b63bb034 100644 |
| --- a/internal/ops/admissionmodel/model.go |
| +++ b/internal/ops/admissionmodel/model.go |
| @@ -420,21 +420,32 @@ func (m *Model) WriterAmbiguous(a *Admission) { |
| a.handleClosed = true |
| a.Refused = true |
| a.landed = m.rnd.Intn(2) == 0 |
| + if a.landed { |
| + // the row exists whether or not the writer knows: it bars like any |
| + // durable unsettled row; the registration stays pending until the |
| + // read-back transfers the responsibility |
| + a.Durable = true |
| + a.Fleet.Admissions = append(a.Fleet.Admissions, a) |
| + } |
| } |
| // ReadBack decides an ambiguous registration on a read opened after the |
| // writer's handle closed: a row found takes admitted then unissued; none |
| // found is a conclusive cancellation. A read while the writer could still |
| -// commit is not conclusive: the guard on writerRunning is that rule, and |
| -// a model without it lets a cancelled registration's row land later, |
| -// which Check reports as a terminal that did not hold. |
| +// commit is not conclusive: both guards below (the writer not running, |
| +// its handle closed) say so and either alone suffices in the states the |
| +// model reaches; a model without them lets a cancelled registration's |
| +// row land later, which Check reports as a terminal that did not hold. |
| func (m *Model) ReadBack(a *Admission) bool { |
| if !m.Alive || a.State != Registered || a.writerRunning || !a.handleClosed { |
| return false |
| } |
| if a.landed { |
| - a.writerRunning = true // the commit is the writer's, seen by the read |
| - m.WriterCommits(a) |
| + // the read finds the row: the registration leaves the pending set |
| + // and the row carries it; the request was refused, so unissued |
| + a.State = Admitted |
| + delete(a.Fleet.pending, a.Token) |
| + m.logf("T%d read back: committed", a.Token) |
| m.GateAnswers(a) |
| return true |
| } |
| @@ -446,15 +457,15 @@ func (m *Model) ReadBack(a *Admission) bool { |
| // an issued token and the fence (a live helper of a live agent, or a |
| // helper that outlived its agent still holding the fence's description). |
| func (m *Model) Send(a *Admission) { |
| - if a.SentAt != unset || a.State.Terminal() { |
| - return |
| + if a.SentAt != unset || !a.Fleet.helperAlive { |
| + return // sent already, or a dead helper, which does nothing |
| } |
| if !a.Durable || !a.Issued { |
| m.Violations = append(m.Violations, fmt.Sprintf("T%d sent without a durable issued admission", a.Token)) |
| return |
| } |
| - if !a.Fleet.helperAlive { |
| - return // a dead helper does nothing; the held token dies with it |
| + if a.State.Terminal() { |
| + return |
| } |
| a.SentAt = m.Now |
| m.logf("T%d sent", a.Token) |
| @@ -534,6 +545,13 @@ func (m *Model) Discover(f *Fleet, fail bool) { |
| for _, a := range f.Admissions { |
| if a.unsettled() { |
| counted[a.Token] = a |
| + } |
| + // revision 9: an admission settled at or after the last clean |
| + // look's start may have been in flight across the change, so its |
| + // admission instant bounds the uncertainty too (one admitted before |
| + // the look and settled clean after it is the case the second code |
| + // review found) |
| + if a.unsettled() || (a.State == Settled && a.SettledAt >= f.lastCleanLook) { |
| if a.AdmittedAt < from { |
| from = a.AdmittedAt |
| } |
| @@ -961,11 +979,53 @@ func (m *Model) Check() error { |
| m.final[a.Token] = a.State |
| } |
| } |
| - // a closed fleet has no uncommitted discovery and nothing pending |
| + // a closed fleet has no uncommitted discovery, nothing pending and no |
| + // durable unsettled admission |
| for _, f := range m.Fleets { |
| - if f.State == Closed && (f.latch != nil || len(f.pending) > 0) { |
| + if f.State != Closed { |
| + continue |
| + } |
| + if f.latch != nil || len(f.pending) > 0 { |
| return fmt.Errorf("fleet %d closed with a latch or a pending registration", f.ID) |
| } |
| + for _, a := range f.Admissions { |
| + if a.Durable && a.unsettled() { |
| + return fmt.Errorf("fleet %d closed with T%d unsettled", f.ID, a.Token) |
| + } |
| + } |
| + } |
| + // inheritance at every step: each fleet's owners are held for every |
| + // interval of every uncertainty on its own and inherited set and on |
| + // its unacknowledged ancestry: a closed one whole, an open one through |
| + // its discovery and through each counted settlement |
| + for _, g := range m.Fleets { |
| + for _, u := range effective(g) { |
| + to := u.To |
| + if u.open() { |
| + to = u.DiscoveryAt |
| + } |
| + for d := dayOf(u.From); d <= dayOf(to); d++ { |
| + for _, o := range g.Owners { |
| + if !m.Holds[d][o] { |
| + return fmt.Errorf("inheritance: fleet %d's owner %s not held for U%d (fleet %d) day %d", g.ID, o, u.ID, u.Fleet.ID, d) |
| + } |
| + } |
| + } |
| + if u.open() { |
| + for _, a := range u.Counted { |
| + if a.State != Settled || u.Fleet.latch != nil { |
| + continue |
| + } |
| + for d := dayOf(a.AdmittedAt); d <= dayOf(a.SettledAt); d++ { |
| + for _, o := range g.Owners { |
| + if !m.Holds[d][o] { |
| + return fmt.Errorf("inheritance: fleet %d's owner %s not held for T%d's settlement under U%d day %d", g.ID, o, a.Token, u.ID, d) |
| + } |
| + } |
| + } |
| + } |
| + } |
| + } |
| } |
| // barrier, stated from the chain: for every fleet G and every owner of |
| // G, a durable unsettled admission of G or of any fleet in G's |
| @@ -1030,6 +1090,16 @@ func (m *Model) CheckQuiescent() error { |
| if err := m.Check(); err != nil { |
| return err |
| } |
| + for _, a := range m.Admissions { |
| + if !a.State.Terminal() { |
| + return fmt.Errorf("T%d not terminal at quiescence (%s)", a.Token, a.State) |
| + } |
| + } |
| + for _, f := range m.Fleets { |
| + if f.latch != nil || len(f.pending) > 0 || f.State != Closed { |
| + return fmt.Errorf("fleet %d not quiescent: latch %v pending %d state %d", f.ID, f.latch != nil, len(f.pending), f.State) |
| + } |
| + } |
| for _, g := range m.Fleets { |
| for p := g; p != nil; p = p.Pred { |
| for _, u := range p.Uncertainties { |
diff --git a/internal/ops/admissionmodel/model_test.go b/internal/ops/admissionmodel/model_test.go| index 679fffd60..b089770fb 100644 |
| --- a/internal/ops/admissionmodel/model_test.go |
| +++ b/internal/ops/admissionmodel/model_test.go |
| @@ -632,6 +632,144 @@ func TestReplayHoldsTheLowerBoundWhileOpen(t *testing.T) { |
| must(t, m) |
| } |
| +// Review 2 (Opus P2-1): T1 admitted and sent before the last clean look, |
| +// still in flight across a change after it, settled clean before the |
| +// change is noticed: the bound must reach T1's admission, so the day |
| +// before the look is held. |
| +func TestLowerBoundReachesInFlightAcrossCleanLook(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 0) |
| + t1 := issue(t, m, f, alice) |
| + m.Now = at(2, 0, 30) |
| + m.Look(f) // clean, T1 in flight |
| + m.Now = at(2, 0, 35) |
| + t2 := m.Register(f, alice) // moves the proof, then fails |
| + m.WriterFails(t2) |
| + m.Now = at(2, 0, 40) |
| + m.Change(f) |
| + m.Now = at(2, 0, 50) |
| + finish(m, t1) // no uncertainty open: nothing permanent |
| + m.Now = at(2, 1, 0) |
| + m.Look(f) // the discovery |
| + u := f.Uncertainties[0] |
| + if u.From != at(1, 22, 59) { |
| + t.Fatalf("from %d, want T1's admission minus the margin %d", u.From, at(1, 22, 59)) |
| + } |
| + held(t, m, alice, 1, 2) |
| + must(t, m) |
| +} |
| + |
| +// Review 2 (Astra 3): the registry proof is the earlier term when no |
| +// admission has moved it since the build and a clean look came later. |
| +func TestLowerBoundProofTerm(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(2, 9, 0) |
| + m.Look(f) |
| + m.Now = at(3, 9, 0) |
| + m.Discover(f, false) |
| + u := f.Uncertainties[0] |
| + if u.From != at(1, 8, 59) { |
| + t.Fatalf("from %d, want the proof minus the margin %d", u.From, at(1, 8, 59)) |
| + } |
| + held(t, m, alice, 1, 2, 3) |
| +} |
| + |
| +// Review 2 (Astra 1): an ambiguous commit that landed bars its owner, and |
| +// a successor's, before the read-back; one that did not land bars nobody. |
| +func TestLandedAmbiguousCommitBarsBeforeReadBack(t *testing.T) { |
| + for seed := int64(1); seed <= 12; seed++ { |
| + m := New(seed) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + m.WriterAmbiguous(a) |
| + m.Now = at(1, 11, 0) |
| + B := m.Build(bob) |
| + if a.landed { |
| + held(t, m, alice, 1) |
| + held(t, m, bob, 1) |
| + } else { |
| + complete(t, m, alice, 1) |
| + complete(t, m, bob, 1) |
| + } |
| + must(t, m) |
| + m.ReadBack(a) |
| + if a.landed && a.State != Unissued { |
| + t.Fatalf("seed %d: landed row read back as %s", seed, a.State) |
| + } |
| + if !a.landed && a.State != Cancelled { |
| + t.Fatalf("seed %d: absent row read back as %s", seed, a.State) |
| + } |
| + complete(t, m, alice, 1) |
| + complete(t, m, bob, 1) |
| + _ = B |
| + must(t, m) |
| + } |
| +} |
| + |
| +// Review 2 (Astra): a replay with one settled token and one unresolved |
| +// registration: the uncertainty stays open, so the settled token's days |
| +// come from the replay's own writes and nothing else. |
| +func TestReplayWritesSettledTokenWhileOpen(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 0) |
| + t1 := issue(t, m, f, alice) |
| + m.Now = at(2, 9, 0) |
| + m.Look(f) |
| + m.Now = at(2, 9, 30) |
| + r := m.Register(f, alice) // pending, its writer running |
| + m.Change(f) |
| + m.Discover(f, true) |
| + if len(f.latch.Counted) != 2 { |
| + t.Fatal("both not counted") |
| + } |
| + m.Now = at(3, 9, 0) |
| + finish(m, t1) |
| + m.Now = at(3, 9, 5) |
| + m.Replay(f) |
| + u := f.Uncertainties[0] |
| + if !u.open() { |
| + t.Fatal("closed with a registration unresolved") |
| + } |
| + held(t, m, alice, 1, 2, 3) |
| + must(t, m) |
| + m.WriterCommits(r) |
| + m.GateAnswers(r) |
| + if u.open() || r.State != Unissued { |
| + t.Fatalf("after the registration resolved: open=%v %s", u.open(), r.State) |
| + } |
| +} |
| + |
| +// Review 2 (Astra): a token held and never sent before the crash; the |
| +// surviving helper sends it after, under the fence; recovery covers it. |
| +func TestFenceHeldTokenSentAfterCrash(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 23, 50) |
| + f := m.Build(alice) |
| + a := hold(t, m, f, alice) |
| + m.Crash(func(*Fleet) bool { return true }) |
| + m.Now = at(2, 0, 10) |
| + m.SurvivingHelperTransport(a) // the first send, after the agent died |
| + if a.SentAt != at(2, 0, 10) { |
| + t.Fatalf("sent at %d", a.SentAt) |
| + } |
| + m.Now = at(2, 0, 20) |
| + m.SurvivingHelperDies(f) |
| + if !m.Recover() { |
| + t.Fatal("recovery refused") |
| + } |
| + held(t, m, alice, 1, 2) |
| + if err := m.CheckQuiescent(); err != nil { |
| + t.Fatal(err) |
| + } |
| +} |
| + |
| // Randomised schedules: every action the design names, in random |
| // interleavings over several days, with the invariants checked after each |
| // step and the end state checked at quiescence. |
| @@ -747,15 +885,15 @@ func runSchedule(seed int64, steps int) (err error) { |
| } |
| } |
| case 11: |
| + m.Look(m.Fleets[m.rnd.Intn(len(m.Fleets))]) // a look: clean, or the discovery of an earlier change |
| + case 12: |
| g := m.Fleets[m.rnd.Intn(len(m.Fleets))] |
| if m.rnd.Intn(2) == 0 { |
| + m.Change(g) // the truth changes, unseen until a look |
| + } else { |
| m.Change(g) |
| + m.Discover(g, m.rnd.Intn(3) == 0) |
| } |
| - m.Look(g) |
| - case 12: |
| - g := m.Fleets[m.rnd.Intn(len(m.Fleets))] |
| - m.Change(g) |
| - m.Discover(g, m.rnd.Intn(3) == 0) |
| case 13: |
| for _, g := range m.Fleets { |
| if g.latch != nil && m.rnd.Intn(2) == 0 { |