amadan
Review three answered; design revision 10: the historical term's threshold is the earlier of the proof and the clean look, empty terminals excluded, and every look reads the witness and rechecks every chain first; the model gains a witness change the proof discovers, crash deduplication of a landed row, one row per token, seven tests; authority gains Result.Parent and Within, keeps the pin on absent and linked tails, and tests a sibling tenant under one pin, a replacement link at Recheck and an other-writable component; dispositions mark superseded rows and the spike note's claims are corrected
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
8 files changed,
+392
−39
DISPOSITIONS-replicator-pinned-root.md+19 −3docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md+3 −3docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md+3 −3internal/authority/authority.go+31 −10internal/authority/authority_unix.go+4 −4internal/authority/authority_unix_test.go+97 −2internal/ops/admissionmodel/model.go+43 −10internal/ops/admissionmodel/model_test.go+192 −4
CI passed — run details
diff --git a/DISPOSITIONS-replicator-pinned-root.md b/DISPOSITIONS-replicator-pinned-root.md| index 603daacf2..af3093e23 100644 |
| --- a/DISPOSITIONS-replicator-pinned-root.md |
| +++ b/DISPOSITIONS-replicator-pinned-root.md |
| @@ -9,17 +9,17 @@ Opus: accept with fixes, no P1, three P2. Astra: reject, five P2, two P3. Report |
| | Finding | Disposition | |
| |---|---| |
| | Astra 2, Opus P2-1: an acquired tenant directory cannot become a confinement boundary | `(*Dir).Confine()` marks an acquired Dir as a root while keeping its ancestry; `TestConfinedTenantRoot` (ascent refused from the root and from beneath it, the edge above still rechecked). The platform-link predicate anchors a relative target at the link's directory under the platform root, so systemd's `../private/...` still resolves; the pinned set must include that directory's root. | |
| -| Astra 3, Opus P3-2: `Recheck` and `Child(expect)` compared identity only | `Facts.Equal` (identity, owner, mode) in both; `TestRootPlatformWalk` chmods an ancestor and sees a changed edge and a failed platform rule, then the restore. `Same` stays for listing-to-acquisition identity. | |
| +| Astra 3, Opus P3-2: `Recheck` and `Child(expect)` compared identity only | `Facts.Equal` (identity, owner, mode) in both; `TestRootPlatformWalk` chmods an ancestor and sees a changed edge and a failed platform rule, then the restore. (Superseded wording: `Same` is used only by `List`'s identity check of its fresh description; acquisition compares every retained fact.) | |
| | Astra 6: slash itself a pinned root | matched before any component; `TestSlashPinned`. | |
| | Opus P3-1: intermediates above a pin kept in a result | closed when the pin is entered; the descriptor test counts one descriptor for a result beneath a deeper pin. | |
| | Opus P3-4: ELOOP not mapped | `ENOTDIR` or `ELOOP` from the directory open is looked at once and named `ErrLink`. | |
| | Opus P3-5: `OpenRoot` on `/` or with `..` | refused (`ErrBadName`); a root is beneath slash. | |
| | Opus P3-3: a Dir under a concurrent Close | documented as single-owner; the design's shutdown ordering keeps it; a lock is not added now. | |
| -| Astra 5, Opus P2-2: the foreign-owned component never isolated; the pop not distinguished from kernel `..`; leaks unobserved | the platform predicate takes `Facts`, so a test refuses one inode below an accepted slash; `TestAscentIsTheRetainedParent` moves `b` under another parent and asks for `..`; `TestDescriptorsAreReleased` (linux) counts `/proc/self/fd` across every failing and succeeding walk, three failing roots, a refused `Child`, a `List` and a `Close`, with spellings that leave intermediates open on the way; the swap test closes its result. Sixteen authority mutants run in a tree copy, all killed, including removal of each flag, kernel `..` for the pop, the uid check, each close site, `Result.Close` as a no-op, `Dir.Close` without the syscall, a dup for `List`, no expect check, no `Confine`, and the pin's intermediates kept; the `List` identity check's close is equivalent (`openat(fd, ".")` cannot be another directory). | |
| +| Astra 5, Opus P2-2: the foreign-owned component never isolated; the pop not distinguished from kernel `..`; leaks unobserved | the platform predicate takes `Facts`, so a test refuses one inode below an accepted slash; `TestAscentIsTheRetainedParent` moves `b` under another parent and asks for `..`; `TestDescriptorsAreReleased` (linux) counts `/proc/self/fd` across every failing and succeeding walk, three failing roots, a refused `Child`, a `List` and a `Close`, with spellings that leave intermediates open on the way; the swap test closes its result. Sixteen authority mutants run in a tree copy, all killed (superseded by the precise statement under review two: not every flag and not every close site were observable then), including kernel `..` for the pop, the uid check, `Result.Close` as a no-op, `Dir.Close` without the syscall, a dup for `List`, no expect check, no `Confine`, and the pin's intermediates kept; the `List` identity check's close is equivalent (`openat(fd, ".")` cannot be another directory). | |
| | Opus: `/..` refused where today folds it | stated in `doc.go` as intended. | |
| | Astra 1, Opus P2-3: the model's barrier owner-only and its invariant tautological; multi-owner fleets | the barrier is the design's (a durable unsettled admission bars its fleet's owners and every successor's through the unacknowledged ancestry, issued or not); the invariant is stated from the chain, the publisher from reach; `TestSuccessorBarredByPredecessorAdmission` (day 3 before settlement, and through a closed unacknowledged intermediate); the driver builds one owner per fleet. | |
| | 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. | |
| +| 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 over-reach is equivalent under the model; the proof term was claimed equivalent here and is not (superseded by review two's Astra 3 and review three's Opus P2-1). | |
| | 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) |
| @@ -45,3 +45,19 @@ Opus: accept with fixes, no P1, one P2. Astra: accept with fixes, no P1, two P2, |
| **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. |
| +## Review three (of `0a527924`: the second review answered, design revision 9) |
| + |
| +Opus: accept with fixes, no P1, one P2. Astra: accept with fixes, no P1, one P2. Reports: `logs/opus-replroot-review3.md`, `logs/astra-replroot-review3.md`. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| Opus P2-1: revision 9's threshold was the last clean look's start, but a witness change is known only to be after the proof; a request settled between such a change and a clean look was missed | **Design revision 10**: the threshold is the earlier of the proof and the look (the bound itself), 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. The model has a witness change kind that the proof discovers (and a look, in the design's ordering); `TestLowerBoundThresholdIsTheEarlierOfProofAndLook` is Opus's sequence with the look told to miss the witness; `TestLowerBoundThresholdIsNotTheLater` is Opus P3-5's; the mutants `max(proof, look)`, look-only and the proof not refusing a moved witness are killed. | |
| +| Astra 1: `Result.Pin` cannot tell sibling tenants beneath one pin apart; the pin was dropped on absent and linked tails; the first pin would have passed for the matched one | `Result.Parent` (the retained holder of a non-directory result) and `Result.Within(root)` (identity along the retained stack); the pin kept on every classified return; `TestWithinAndMatchedPin` with two pins, a sibling tenant, an intermediate link and relative spellings; the first-pin and Within-ignores-parent mutants killed. Opus's note stands: `Pin` is the platform root, never a tenancy boundary; the inventory asks `Within` against the tenant's root and identity against claimants. | |
| +| Astra 2, Opus (over-hold): the design's "settled_at at or after" included empty terminals | revision 10 excludes unissued and cancelled (never sent); `TestHistoricalTermExcludesEmptyTerminals`; the mutant including terminals is killed. | |
| +| Astra 3, Opus P3-2: a crash after a landed ambiguous commit represented the row twice | the crash appends only a row not yet durable; a one-row-per-token check after every step; `TestLandedAmbiguousThenCrash`; the mutant killed. | |
| +| Opus P3-3: a dead clause in the inheritance check | removed. | |
| +| Opus P3-4, Astra 4: the spike note's oracle claim and the self-contradicting sentence; superseded disposition rows unmarked; the dead-helper send, "closes once", the send-order explanation, the crash-hazard wording | `Close` without its unsettled loop is a mechanism mutant and the closed-fleet check kills it; the sentence rewritten; the rows above marked superseded; the wording corrected in the note and the tests. | |
| +| Opus P3-5: the landed-ambiguous test did not assert both outcomes; the in-flight test would not kill a `max` threshold | both outcomes asserted; the `max` sequence is a named test. | |
| +| 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. | |
| + |
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 f28149b6d..9213313b5 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 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. |
| +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. |
| ## 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 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. |
| +**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 (both participants complete; not an empty terminal, which never sent) at or after that lower bound (one admitted before it 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 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`. |
| +**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`. |
| **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 31d77a776..3d549fd24 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 |
| @@ -19,10 +19,10 @@ 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 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. |
| +- **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 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. |
| +- **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. |
| - **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 e958ef008..280b5d532 100644 |
| --- a/internal/authority/authority.go |
| +++ b/internal/authority/authority.go |
| @@ -115,17 +115,38 @@ 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, 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. |
| +// 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. |
| type Result struct { |
| - Kind Kind |
| - Facts Facts |
| - Dir *Dir |
| - Pin *Root |
| - owned []*Dir |
| + Kind Kind |
| + Facts Facts |
| + Dir *Dir |
| + Parent *Dir |
| + Pin *Root |
| + owned []*Dir |
| +} |
| + |
| +// Within reports whether the result lies beneath root (or is root): the |
| +// retained stack of the result's directory (the directory itself for a |
| +// directory result, its holder otherwise) is walked up by parent pointers |
| +// 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 { |
| + start := r.Dir |
| + if r.Kind != Directory { |
| + start = r.Parent |
| + } |
| + for d := start; d != nil; d = d.parent { |
| + if d == root || d.facts.Same(root.facts) { |
| + return true |
| + } |
| + } |
| + return false |
| } |
| // Close closes the directories the walk acquired, deepest first. |
diff --git a/internal/authority/authority_unix.go b/internal/authority/authority_unix.go| index d6f2bf188..af08fc6fc 100644 |
| --- a/internal/authority/authority_unix.go |
| +++ b/internal/authority/authority_unix.go |
| @@ -388,10 +388,10 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| switch { |
| case errors.Is(ee.Err, unix.ENOENT): |
| res.Close() |
| - return Result{Kind: Absent}, nil |
| + return Result{Kind: Absent, Pin: res.Pin}, nil |
| case errors.Is(ee.Err, ErrLink): |
| res.Close() |
| - return Result{Kind: Link}, nil |
| + return Result{Kind: Link, Pin: res.Pin, Facts: Facts{}}, nil |
| } |
| } |
| return fail(err) |
| @@ -406,12 +406,12 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| } |
| if k == Absent { |
| res.Close() |
| - return Result{Kind: Absent}, nil |
| + return Result{Kind: Absent, Pin: res.Pin}, nil |
| } |
| if wantDir && k != Directory { |
| return fail(&EdgeError{Name: c, Err: ErrNotDirectory}) |
| } |
| - res.Kind, res.Facts = k, f |
| + res.Kind, res.Facts, res.Parent = k, f, cur |
| if k == Directory { |
| child, err := cur.Child(c, &f) |
| if err != nil { |
diff --git a/internal/authority/authority_unix_test.go b/internal/authority/authority_unix_test.go| index 46216e49f..1acd54167 100644 |
| --- a/internal/authority/authority_unix_test.go |
| +++ b/internal/authority/authority_unix_test.go |
| @@ -472,8 +472,15 @@ func TestWalkClasses(t *testing.T) { |
| 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) |
| + if err != nil || res.Pin != nil || res.Parent != root.Dir { |
| + t.Fatalf("a relative walk names a pin, or no parent: %v %v %v", res.Pin, res.Parent, err) |
| + } |
| + // the pin survives an absent or a linked tail beneath it |
| + for _, sp := range []string{"/r/nothing", "/r/d/nothing/x", "/r/ld/inner"} { |
| + res, err := root.Walk(sp, pins) |
| + if err != nil || res.Pin != root { |
| + t.Fatalf("Walk(%q): pin %v err %v", sp, res.Pin, err) |
| + } |
| } |
| // an unreadable platform directory before the pin keeps its errno |
| mkdir(t, filepath.Join(base, "locked", "x")) |
| @@ -660,3 +667,91 @@ func TestSlashPinned(t *testing.T) { |
| res.Close() |
| } |
| } |
| + |
| +// Two tenants beneath one platform pin: Pin is the same for both, so the |
| +// inventory asks Within against the tenant's own root; a second pin is |
| +// the matched one, not the first. |
| +func TestWithinAndMatchedPin(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "plat", "alice", "d")) |
| + mkdir(t, filepath.Join(base, "plat", "bob")) |
| + write(t, filepath.Join(base, "plat", "alice", "file"), "x") |
| + write(t, filepath.Join(base, "plat", "bob", "file"), "x") |
| + link(t, "d", filepath.Join(base, "plat", "alice", "ld")) |
| + mkdir(t, filepath.Join(base, "other", "sub")) |
| + write(t, filepath.Join(base, "other", "sub", "file"), "x") |
| + plat, err := OpenRoot(slash, "plat", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer plat.Close() |
| + other, err := OpenRoot(slash, "other", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer other.Close() |
| + pins := &Pins{Slash: slash, Roots: []*Root{plat, other}, Platform: me} |
| + alice := child(t, plat.Dir, "alice") |
| + alice.Confine() |
| + cases := []struct { |
| + spelling string |
| + kind Kind |
| + pin *Root |
| + inAlice bool |
| + }{ |
| + {"/plat/alice/file", Regular, plat, true}, |
| + {"/plat/bob/file", Regular, plat, false}, |
| + {"/plat/alice/d", Directory, plat, true}, |
| + {"/plat/alice/ld/x", Link, plat, false}, |
| + {"/other/sub/file", Regular, other, false}, |
| + {"/other/sub", Directory, other, false}, |
| + {"file", Regular, nil, true}, |
| + {"d", Directory, nil, true}, |
| + {".", Directory, nil, true}, |
| + } |
| + for _, c := range cases { |
| + res, err := alice.Walk(c.spelling, pins) |
| + if err != nil || res.Kind != c.kind || res.Pin != c.pin { |
| + t.Errorf("Walk(%q): kind %v pin %v err %v", c.spelling, res.Kind, res.Pin, err) |
| + continue |
| + } |
| + if res.Kind != Link && res.Kind != Absent && res.Within(alice) != c.inAlice { |
| + t.Errorf("Walk(%q): Within(alice) = %v, want %v", c.spelling, !c.inAlice, c.inAlice) |
| + } |
| + if res.Kind == Regular && !res.Within(slash) { |
| + t.Errorf("Walk(%q): not within slash", c.spelling) |
| + } |
| + res.Close() |
| + } |
| +} |
| + |
| +// 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. |
| +func TestRecheckDoesNotFollowAReplacementLink(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "a", "b")) |
| + b := child(t, child(t, slash, "a"), "b") |
| + if err := os.Rename(filepath.Join(base, "a", "b"), filepath.Join(base, "a", "real")); err != nil { |
| + t.Fatal(err) |
| + } |
| + link(t, "real", filepath.Join(base, "a", "b")) |
| + if err := b.Recheck(); !edgeIs(err, ErrChanged) { |
| + t.Fatalf("a link in the retained directory's place: %v", err) |
| + } |
| +} |
| + |
| +// The platform rule refuses other-writable as well as group-writable. |
| +func TestPlatformRuleOtherWritable(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "o", "x")) |
| + if err := os.Chmod(filepath.Join(base, "o"), 0o757); err != nil { |
| + t.Fatal(err) |
| + } |
| + if _, err := OpenRoot(slash, "o/x", me); !edgeIs(err, ErrNotPlatform) { |
| + t.Fatalf("other-writable component: %v", err) |
| + } |
| +} |
diff --git a/internal/ops/admissionmodel/model.go b/internal/ops/admissionmodel/model.go| index 6b63bb034..afe8db335 100644 |
| --- a/internal/ops/admissionmodel/model.go |
| +++ b/internal/ops/admissionmodel/model.go |
| @@ -136,6 +136,7 @@ type Fleet struct { |
| helperStopped bool |
| guardClosed bool |
| drained bool |
| + witnessMoved bool |
| // truth |
| ChangedAt Time // the instant authority truly changed (unset if never) |
| @@ -298,13 +299,27 @@ func (m *Model) Look(f *Fleet) { |
| } |
| } |
| -// Change is the truth: the fleet's authority changes now, unseen. |
| +// Change is the truth: the fleet's authority changes now, unseen, in a |
| +// way the next look's file inspection finds. |
| func (m *Model) Change(f *Fleet) { |
| if f.ChangedAt == unset { |
| f.ChangedAt = m.Now |
| } |
| } |
| +// WitnessChange is the truth: the registry's ownership witness moves now, |
| +// unseen. The design has every look read the witness first, so a look |
| +// discovers it too; the proof at the next registration discovers it as |
| +// well. A model in which the look misses it (the mutant the third review |
| +// named) leaves a request completed between the change and the look |
| +// unheld unless the bound's threshold is the earlier of proof and look. |
| +func (m *Model) WitnessChange(f *Fleet) { |
| + if f.ChangedAt == unset { |
| + f.ChangedAt = m.Now |
| + f.witnessMoved = true |
| + } |
| +} |
| + |
| // Register is the gate's first half: under the discovery mutex, proof then |
| // registration in the pending set. It returns nil when refused. |
| func (m *Model) Register(f *Fleet, o Owner) *Admission { |
| @@ -315,6 +330,10 @@ func (m *Model) Register(f *Fleet, o Owner) *Admission { |
| if !f.owns(o) { |
| panic("model: an admission for an owner the fleet does not have") |
| } |
| + if f.witnessMoved && f.DiscoveredAt == unset { |
| + m.Discover(f, false) // the proof reads the witness: a moved witness is the discovery |
| + return nil |
| + } |
| f.proof = m.Now // the gate's proof: the witness read unchanged now |
| m.nextToken++ |
| a := &Admission{Token: m.nextToken, Fleet: f, Owner: o, AdmittedAt: m.Now, State: Registered, writerRunning: true, epoch: f.epoch, |
| @@ -546,12 +565,14 @@ func (m *Model) Discover(f *Fleet, fail bool) { |
| 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) { |
| + // 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) { |
| if a.AdmittedAt < from { |
| from = a.AdmittedAt |
| } |
| @@ -813,9 +834,11 @@ func (m *Model) Crash(helperSurvives func(*Fleet) bool) { |
| } |
| a.writerRunning = false |
| if landed { // the commit landed before the crash: a durable unanswered row |
| - a.Durable = true |
| + if !a.Durable { // a landed ambiguous row is already represented |
| + a.Durable = true |
| + f.Admissions = append(f.Admissions, a) |
| + } |
| a.State = Admitted |
| - f.Admissions = append(f.Admissions, a) |
| } else { |
| a.State = Cancelled |
| a.How = "lost-with-process" |
| @@ -979,6 +1002,16 @@ func (m *Model) Check() error { |
| m.final[a.Token] = a.State |
| } |
| } |
| + // one durable row per token |
| + for _, f := range m.Fleets { |
| + seen := map[int]bool{} |
| + for _, a := range f.Admissions { |
| + if seen[a.Token] { |
| + return fmt.Errorf("fleet %d represents T%d twice", f.ID, a.Token) |
| + } |
| + seen[a.Token] = true |
| + } |
| + } |
| // a closed fleet has no uncommitted discovery, nothing pending and no |
| // durable unsettled admission |
| for _, f := range m.Fleets { |
| @@ -1013,7 +1046,7 @@ func (m *Model) Check() error { |
| } |
| if u.open() { |
| for _, a := range u.Counted { |
| - if a.State != Settled || u.Fleet.latch != nil { |
| + if a.State != Settled { |
| continue |
| } |
| for d := dayOf(a.AdmittedAt); d <= dayOf(a.SettledAt); d++ { |
diff --git a/internal/ops/admissionmodel/model_test.go b/internal/ops/admissionmodel/model_test.go| index b089770fb..2682d00a7 100644 |
| --- a/internal/ops/admissionmodel/model_test.go |
| +++ b/internal/ops/admissionmodel/model_test.go |
| @@ -142,7 +142,7 @@ func TestThreeMidnightsBothOrders(t *testing.T) { |
| // Astra's fifth-review sequence: proof, discovery, commit, a send on the |
| // 4th. The commit after the discovery began is refused (unissued) and the |
| -// uncertainty that counted it closes once. |
| +// uncertainty that counted it is closed by the empty settlement. |
| func TestCommitAfterDiscoveryIsUnissued(t *testing.T) { |
| m := New(1) |
| m.Now = at(2, 23, 57) |
| @@ -169,7 +169,7 @@ func TestCommitAfterDiscoveryIsUnissued(t *testing.T) { |
| // Review 7's sequence: the budget expires while the writer still runs, the |
| // discovery counts the registration, then the writer commits. One final |
| -// outcome, unissued, and the uncertainty closes once. |
| +// outcome, unissued, and the uncertainty is closed by the empty settlement. |
| func TestBudgetExpiryThenCommit(t *testing.T) { |
| m := New(1) |
| m.Now = at(2, 23, 58) |
| @@ -661,6 +661,182 @@ func TestLowerBoundReachesInFlightAcrossCleanLook(t *testing.T) { |
| must(t, m) |
| } |
| +// Review 3 (Opus P2-1): a witness change between the last proof and a |
| +// clean look; a request in flight across it settles before the look; the |
| +// bound's threshold is the earlier of proof and look, so its day is held. |
| +// In the design every look reads the witness first and discovers at once; |
| +// here the look is told to miss it, which is the stronger case. |
| +func TestLowerBoundThresholdIsTheEarlierOfProofAndLook(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, 5) |
| + p := m.Register(f, alice) // proves the witness at 00:05 |
| + m.WriterFails(p) |
| + m.Now = at(2, 0, 10) |
| + m.WitnessChange(f) |
| + m.Now = at(2, 0, 20) |
| + finish(m, t1) // clean settlement, nothing permanent |
| + m.Now = at(2, 0, 30) |
| + f.lastCleanLook = m.Now // a look that read the files only (the mutant the review named) |
| + m.Now = at(2, 1, 0) |
| + if m.Register(f, alice) != nil { |
| + t.Fatal("the proof did not refuse on a moved witness") |
| + } |
| + 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) |
| + // and the design's own ordering: a look reads the witness and discovers |
| + m2 := New(1) |
| + m2.Now = at(1, 9, 0) |
| + g := m2.Build(alice) |
| + m2.Now = at(1, 10, 0) |
| + m2.WitnessChange(g) |
| + m2.Now = at(1, 10, 30) |
| + m2.Look(g) |
| + if g.DiscoveredAt != at(1, 10, 30) { |
| + t.Fatal("a look did not discover a moved witness") |
| + } |
| +} |
| + |
| +// Review 3 (Opus P3-5): the threshold is min(proof, look), not max: the |
| +// change just after the look, T settles, a later registration moves the |
| +// proof past T's settlement, the next look discovers. |
| +func TestLowerBoundThresholdIsNotTheLater(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 |
| + m.Now = at(2, 0, 31) |
| + m.Change(f) |
| + m.Now = at(2, 0, 40) |
| + finish(m, t1) |
| + m.Now = at(2, 0, 50) |
| + p := m.Register(f, alice) // moves the proof past T1's settlement |
| + m.WriterFails(p) |
| + 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 3 (Astra 2): an empty terminal (unissued) is not a settlement |
| +// for the historical term: a registration from day 1 whose commit lands |
| +// after the look on day 2 and is refused does not pull the bound to day 1. |
| +func TestHistoricalTermExcludesEmptyTerminals(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 23, 0) |
| + f := m.Build(alice) |
| + tr := m.Register(f, alice) |
| + m.BudgetExpires(tr) |
| + m.Now = at(2, 9, 0) |
| + m.Look(f) |
| + m.Now = at(2, 9, 10) |
| + p := m.Register(f, alice) |
| + m.WriterFails(p) |
| + m.Now = at(2, 9, 20) |
| + m.WriterCommits(tr) |
| + m.GateAnswers(tr) |
| + if tr.State != Unissued { |
| + t.Fatal(tr.State) |
| + } |
| + m.Now = at(2, 10, 0) |
| + m.Change(f) |
| + m.Look(f) |
| + if u := f.Uncertainties[0]; u.From != at(2, 8, 59) { |
| + t.Fatalf("from %d, want the clean look minus the margin %d (the unissued row must not reach day 1)", u.From, at(2, 8, 59)) |
| + } |
| + complete(t, m, alice, 1) |
| +} |
| + |
| +// Review 3 (Astra): a token admitted on one day and sent the next: the |
| +// historical term uses the admission instant, not the send. |
| +func TestHistoricalTermUsesTheAdmissionInstant(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 0) |
| + a := hold(t, m, f, alice) |
| + m.Now = at(2, 0, 10) |
| + m.Send(a) |
| + m.Now = at(2, 0, 30) |
| + m.Look(f) |
| + m.Now = at(2, 0, 35) |
| + m.Change(f) |
| + m.Now = at(2, 0, 40) |
| + finish(m, a) |
| + 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 the admission minus the margin %d", u.From, at(1, 22, 59)) |
| + } |
| + held(t, m, alice, 1, 2) |
| +} |
| + |
| +// 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) { |
| + seen := 0 |
| + for seed := int64(1); seed <= 16; seed++ { |
| + m := New(seed) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + m.WriterAmbiguous(a) |
| + if !a.landed { |
| + continue |
| + } |
| + seen++ |
| + m.Crash(func(*Fleet) bool { return false }) |
| + m.Now = at(1, 10, 5) |
| + m.Recover() |
| + n := 0 |
| + for _, x := range f.Admissions { |
| + if x.Token == a.Token { |
| + n++ |
| + } |
| + } |
| + if n != 1 || a.State != RecoveredUnknown { |
| + t.Fatalf("seed %d: %d rows, state %s", seed, n, a.State) |
| + } |
| + held(t, m, alice, 1) |
| + must(t, m) |
| + } |
| + if seen == 0 { |
| + t.Fatal("no seed landed") |
| + } |
| +} |
| + |
| +// Review 3 (Astra): a successor under a failed discovery whose only |
| +// counted item is a pending registration: nothing durable bars, no |
| +// uncertainty row exists, so only the latch overlay through the ancestry |
| +// can hold the successor's owner. |
| +func TestLatchOverlayReachesSuccessor(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + A := m.Build(alice) |
| + m.Now = at(1, 10, 0) |
| + m.Register(A, alice) // pending, writer running |
| + m.Change(A) |
| + m.Discover(A, true) |
| + m.Now = at(1, 11, 0) |
| + m.Build(bob) |
| + held(t, m, bob, 1) |
| + held(t, m, alice, 1) |
| + 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) { |
| @@ -681,6 +857,7 @@ func TestLowerBoundProofTerm(t *testing.T) { |
| // 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) { |
| + landedSeen, absentSeen := 0, 0 |
| for seed := int64(1); seed <= 12; seed++ { |
| m := New(seed) |
| m.Now = at(1, 10, 0) |
| @@ -708,6 +885,14 @@ func TestLandedAmbiguousCommitBarsBeforeReadBack(t *testing.T) { |
| complete(t, m, bob, 1) |
| _ = B |
| must(t, m) |
| + if a.landed { |
| + landedSeen++ |
| + } else { |
| + absentSeen++ |
| + } |
| + } |
| + if landedSeen == 0 || absentSeen == 0 { |
| + t.Fatalf("both outcomes must be seen: landed %d absent %d", landedSeen, absentSeen) |
| } |
| } |
| @@ -888,9 +1073,12 @@ func runSchedule(seed int64, steps int) (err error) { |
| 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 { |
| + switch m.rnd.Intn(3) { |
| + case 0: |
| m.Change(g) // the truth changes, unseen until a look |
| - } else { |
| + case 1: |
| + m.WitnessChange(g) // seen by the next look or proof |
| + default: |
| m.Change(g) |
| m.Discover(g, m.rnd.Intn(3) == 0) |
| } |