docs: onboarding-wizard contract revision 9 (sol r8 NEW-9 residual: prefix-derived seed tuples + seed-origin gate; NEW-10: target-result authorization on every replay mode)

2026-08-26 22:56:59 -05:00
parent eff3b91478
commit 535ac2d860
1 changed files with 204 additions and 58 deletions
@@ -152,6 +152,33 @@ explicit read authority on the recorded seed targets and asserts B's
 replay access events; replay-affected count equalities are scoped to
 the mutation event class (NEW-9).
 Revision 9 (sol re-review 7: NEW-9 residual, NEW-10): the seed
 boundary becomes server-complete and oracle-free. The **canonical
 seed key set** is fence-independent (epoch id plus the fixed
 seed-role list), while the full tuple set is **prefix-derived**: each
 position's scope and payload digest derive from the committed
 predecessors' recorded fence outcomes, the derivable members at any
 state are the committed prefix plus the next unrecorded position,
 the pre-first-company state derives exactly the seed-company tuple,
 and an out-of-order shared declaration is refused recording nothing
 (§4.3, §3.4). The epoch gains one immutable **seed-origin account**
 — the first admin the finalize transaction created — and a
 **seed-boundary gate** evaluated after fresh-mutation authorization
 and before fence presence can affect the response: a submitter on a
 canonical seed key who is neither the seed-origin account nor holds
 target-result read authority on the position's recorded targets
 receives the constant-shape bounded conflict, identical across the
 recorded and unrecorded worlds, creating nothing in either — so
 §5.2 eligibility alone can never originate a seed fence and the
 eligible-wrong-actor race on the top-level seed-company key is
 closed (NEW-9; witnesses §6.7: the two-world control and the
 top-level origination race). Target-result authorization extends to
 **every replay mode**: an `actor-bound` replay requires the recorded
 actor to hold live read authority on every record the recorded
 outcome references, actor equality remaining an additional
 condition, never a substitute — a creator whose grants were revoked
 is refused, not replayed (NEW-10; §6.7 lost-target-grant witness).
 Scope: the Gateway-backed product onboarding wizard. Out of scope: the
 host-local install wizard (`mosaic wizard`, which drives host install and
 gateway bootstrap and is not this artifact — audit REPORT.md layer 3);
@@ -368,7 +395,11 @@ the named authority:
   the fixed example set (§4.3). A resumed run — including a fresh
   client holding none of the original run's transient state —
   reconstructs the same ordered sequence and the same deterministic
-   §4.3 keys from that canonical state alone. Because the seed
+   §4.3 keys from that canonical state alone, prefix-wise: each
   position's scope and payload derive from the committed
   predecessors' recorded outcomes, so the run walks the order and
   never precomputes a tuple past the next unrecorded position
   (§4.3 shared-declaration boundary). Because the seed
   parameter is immutable (§3.1), the re-derived sequence is
   byte-stable across every re-run and resume: the same keys carry
   the same payload digests, so already-committed mutations replay
@@ -382,9 +413,13 @@ the named authority:
   parameter is provenance the derivation reads, never a value any
   later step may change.
   The first company is created by the ordinary top-level company
-   command under §5.2's eligibility policy, with the new admin as actor,
+   command under §5.2's eligibility policy, with the new admin — the
   epoch's §4.3 seed-origin account — as actor,
   naming the admin as initial `owner` in the same audited operation
-   (contract 2 §4.3). The initial estate, initial project, and initial
+   (contract 2 §4.3); the §4.3 seed-boundary gate reserves
   origination of the canonical seed tuples to that account, while
   the same command outside the canonical seed key set follows §5.2
   unchanged. The initial estate, initial project, and initial
   workspace with seeded example data (D4, D11) follow through hierarchy
   commands (contract 1 §5.1) under the admin's `owner` authority
   (contract 2 §4.3). Seeded examples are ordinary workspace content
@@ -438,19 +473,24 @@ collects no sensitive category, so v1 ships no custody surface.
     never the recorded outcome. If authorization passes, the
     submission's declared replay mode equals the recorded row's, and
     the recorded scope and payload digest equal the submission's,
-     the row's replay mode decides the actor rule: an `actor-bound`
+     the submitter must pass **target-result authorization** — in
-     row additionally requires the recorded actor to equal the
+     every replay mode. Returning a
     submitter; a `shared` row replays for an authorized submitter
     who also passes **target-result authorization**. Returning a
     recorded outcome is a read of the canonical records that
-     outcome references, and fresh-mutation authorization is not
+     outcome references, and neither fresh-mutation authorization
-     read authorization on records another actor already created: a
+     nor recorded-actor identity is
-     shared replay therefore additionally requires the submitter to
+     read authorization on those records: every replay, `shared` or
     `actor-bound`, requires the submitter to
     hold, at replay time, read authority on every canonical record
     the recorded outcome references, under each record's owning
     contract's read-authorization rules (for the seed targets, the
     contract 2 grant model — RBAC §1.1 platform-admin standing
-     confers none of it). A submitter who passes the fresh-mutation
+     confers none of it). Actor equality is the additional
     `actor-bound` condition, never a substitute for target-result
     authorization: an `actor-bound` row replays only for the
     recorded actor, and only while that actor holds live
     target-result read authority — an original actor whose grants
     on the referenced records were since revoked is refused, not
     replayed (witness §6.7). A submitter who passes the fresh-mutation
     check but fails target-result authorization is refused with the
     same single bounded conflict error as a collision below —
     constant in shape, identifying no record, disclosing nothing of
@@ -479,29 +519,77 @@ collects no sensitive category, so v1 ships no custody surface.
     it executes nothing and discloses nothing of the recorded
     outcome.
   - **Shared-declaration boundary.** `shared` is a server-verified,
-     seed-only policy, never a caller privilege. The command layer
+     seed-only policy, never a caller privilege. The boundary has a
-     re-derives, from canonical state alone, the **canonical seed
+     fence-independent part and a prefix-derived part. The
-     tuple set** of the current bootstrap epoch: the exact
+     **canonical seed key set** — the (operation identifier, key)
-     (operation identifier, key, authorization scope, payload
+     pairs of §3.4's ordered seed sequence — is derived from the
-     digest) tuples of §3.4's ordered seed sequence, derived from
+     epoch id and the fixed seed-role list alone: the keys are
-     the epoch id, the immutable `bootstrap.seed-company-name`
+     deterministic and depend on no generated id, so membership is
-     provenance, and the fixed example set — the same derivation
+     decidable before any seed mutation has run and without
-     §3.4 requires of a fresh client. A submission declaring
+     consulting the fence table. The full **canonical seed tuple
-     `shared` whose tuple is not a member of that set is refused
+     set** is prefix-derived, because later seed tuples embed
-     with a single bounded refusal (contract 5 §4.2 validation
+     generated ids: the tuple at seed position k — its
-     class) that executes nothing and records no fence row. No
+     authorization scope and payload digest — is derived from the
-     other operation can carry a shared declaration, so no shared
+     epoch id, the immutable `bootstrap.seed-company-name`
-     fence row can exist outside the seed sequence — the seed-only
+     provenance, the fixed example set, and the canonical recorded
-     rule is enforced by the command layer, not by wizard
+     outcomes of positions 1 through k−1 (the ids the committed
-     convention. **Origination.** A shared fence row not yet
+     predecessor fence rows reference). At any canonical state
-     recorded is originated only by executing its seed mutation:
+     exactly these members are derivable: every committed-prefix
-     the originating submission passes the full fresh-mutation
+     tuple (read back from its fence row) and the next unrecorded
-     authorization for that seed command (§5.2 eligibility plus the
+     tuple in order. Before the first company exists, the derivable
-     hierarchy authority the command itself requires), and a
+     set is exactly the seed-company tuple. A fresh client derives
-     refused submission records no row (no-error replay below). An
+     the same way — §3.4's derivation is this walk: submit the
-     actor without the seed mutation's authority therefore cannot
+     sequence in order, learning each generated id from the
-     win an unrecorded seed key, and the recorded actor of every
+     returned recorded outcome or the submission's own execution,
-     shared row was authorized for the mutation the row fences.
+     never precomputing a tuple past the next position. A
     submission declaring `shared` whose (operation, key) is
     outside the canonical seed key set, whose tuple does not equal
     its position's derived tuple, or whose position lies past the
     next unrecorded position (out of order) is refused with a
     single bounded refusal (contract 5 §4.2 validation class) that
     executes nothing and records no fence row. No other operation
     can carry a shared declaration, so no shared fence row can
     exist outside the seed sequence — the seed-only rule is
     enforced by the command layer, not by wizard convention.
   - **Seed-boundary gate and origination.** The epoch has one
     immutable **seed-origin account**: the account the §3.3
     finalize transaction created as the epoch's first admin
     (identity §3) — provenance the epoch record fixes at finalize
     and nothing changes afterwards. Every mutating submission
     whose (operation, key) is in the canonical seed key set —
     whatever replay mode it declares — passes, after
     fresh-mutation authorization and before the fence table is
     consulted, the **seed-boundary gate**: the submitter is the
     seed-origin account, or holds §4.3 target-result read
     authority on the canonical records the position's recorded
     outcome references. A submitter satisfying neither is refused
     with the same single bounded conflict error as a collision —
     and because the gate is evaluated without consulting fence
     presence, the refusal is byte-shape-identical whether the seed
     fence and its targets exist or not: the recorded and
     unrecorded worlds are indistinguishable to that submitter, no
     mutation or fence row is created in either, and RBAC §7's
     no-existence-oracle rule holds at the seed boundary itself,
     not merely at an existing fence (witness §6.7). For an
     unrecorded position no recorded outcome exists to hold read
     authority on, so only the seed-origin account can proceed to
     origination: §5.2 eligibility alone never originates a seed
     fence, which closes the eligible-wrong-actor race on the
     top-level seed-company key. **Origination.** A seed fence row
     not yet recorded is originated only by the seed-origin account
     executing its seed mutation in order, passing the full
     fresh-mutation authorization for that seed command (§5.2
     eligibility plus the hierarchy authority the command itself
     requires); a refused submission records no row (no-error
     replay below). The recorded actor of every shared row is
     therefore the seed-origin account, authorized for the mutation
     the row fences. If the seed-origin account is banned or
     deleted while seed positions remain unoriginated, those
     positions are unoriginatable for this epoch — an accepted
     consequence of the immutable boundary; factory reset (§4.2),
     which opens a new epoch with a new first admin, is the
     recovery path. Recorded positions are unaffected: any admin
     holding target-result read authority replays them (§6.3).
   - **No error replay.** The fence row commits only with its
     mutation, so only committed outcomes are ever recorded. A failed
     or refused submission records no fence row; a retry executes
@@ -510,8 +598,9 @@ collects no sensitive category, so v1 ships no custody surface.
     pair serialize on the fence's unique constraint: exactly one
     executes. The loser waits for the winner's transaction to
     resolve; if it committed, the loser is handled as a replay
-     (fresh-mutation authorization first — and, for a shared row,
+     (fresh-mutation authorization, the seed-boundary gate where
-     target-result authorization — then the recorded outcome, or
+     the key is a seed key, and target-result authorization first —
     then the recorded outcome, or
     the collision refusal on mismatch); if it aborted, no fence row
     exists and the loser executes. The loser never performs a second
     mutation and is never left without a defined response.
@@ -770,20 +859,64 @@ Binding on the implementing PRs:
   nothing, changes no fence row, and appends no mutation audit
   event — proving the recorded target is neither returned nor
   confirmed to exist and RBAC §7's no-existence-oracle rule holds
-   at the fence; a **non-seed shared declaration** — an ordinary
+   at the fence; the **two-world seed-boundary control (§4.3
   seed-boundary gate)** — the SAME eligible non-originator actor
   submits the exact canonical seed-company tuple in two prepared
   worlds: one where the seed fence and its targets exist (the
   recorded world) and one freshly finalized epoch where they do
   not (the unrecorded world, before any seed command has run) —
   and in both worlds receives the identical bounded conflict
   refusal (asserted byte-shape-identical across the two worlds and
   to the collision refusal), executes nothing, and creates no
   mutation, fence row, or hierarchy node in either — proving the
   response is computed without consulting fence presence, the
   recorded and unrecorded worlds are indistinguishable to that
   actor, and no eligible wrong actor can originate the top-level
   seed fence; a **non-seed shared declaration** — an ordinary
   hierarchy or content command whose tuple is outside the
   canonical seed tuple set, submitted with `shared` declared by an
   actor fully authorized for the mutation — is refused with the
   §4.3 validation refusal, executes nothing, and records no fence
-   row (asserted absent); an **unrecorded-seed-key race** — with
+   row (asserted absent); an **out-of-order shared declaration** —
-   one seed tuple deliberately left unrecorded, an actor lacking
+   with the seed prefix committed through position k, the
-   that seed command's hierarchy authority races the authorized
+   seed-origin account submits the position k+2 tuple (past the
   next unrecorded position), constructed by the test harness from
   ids it obtained out of band — and is refused with the §4.3
   validation refusal, executes nothing, and records no fence row,
   proving the prefix-aware derivation rejects positions the
   canonical walk cannot yet derive; an **unrecorded-seed-key
   race** in two variants — (child variant) with one child seed
   tuple deliberately left unrecorded, an actor lacking that seed
   command's hierarchy authority races the seed-origin account's
   resume for the same (operation, key): the unauthorized
   submission receives the authorization refusal and records no
-   fence row, the authorized submission executes afresh, and the
+   fence row, the origin account's submission executes afresh, and
-   resulting fence row records the authorized actor — proving
+   the resulting fence row records the seed-origin account;
-   origination of a missing seed fence is bound to full
+   (top-level variant, NEW-9) with the seed-company tuple
-   fresh-mutation authorization; a submission that failed before commit
+   unrecorded, an eligible platform admin who is not the
   seed-origin account — passing §5.2 fresh-mutation authorization
   in full, since the top-level command requires no hierarchy
   authority — races the seed-origin account for the seed-company
   (operation, key): the non-originator receives the constant
   bounded conflict refusal from the seed-boundary gate and
   records no fence row and no company, the seed-origin account
   executes afresh, and the resulting fence row records the
   seed-origin account — proving origination of a missing seed
   fence is bound to the seed-origin account, not to eligibility
   alone; an **actor-bound lost-target-grant replay (NEW-10)** — an
   actor creates a non-seed top-level company under an
   `actor-bound` key, grants a second account `owner`, and the
   second account then revokes every grant the creator held on the
   company; the creator, still authenticated and eligible,
   resubmits the exact recorded (operation, key, scope, payload,
   mode) tuple — actor equality holds but live target-result
   authorization fails, so the submission is refused with the
   single bounded conflict, executes nothing, returns nothing of
   the recorded outcome, and appends no access or mutation event;
   re-granting the creator read authority and resubmitting returns
   the recorded outcome — proving actor equality is never a
   substitute for live target-result read authority on any replay
   mode; a submission that failed before commit
   leaves no fence row and its retry executes; two concurrent resumed
   runs executing the seed sequence yield exactly one seed set — per
   key, exactly one mutation and one mutation audit event exist, and
@@ -860,21 +993,34 @@ contracts and are not additions:
   envelope, proposed and ratified here, severable from the rest of
   this contract. Including the **replay mode**: each keyed
   submission declares `actor-bound` (default) or `shared`, the
-   declaration is recorded in the fence row, a shared row replays
+   declaration is recorded in the fence row, and every replay — in
-   for a freshly authorized actor whose scope and payload digest
+   either mode — requires the submitter, freshly authorized with
-   match and who additionally passes the §4.3 target-result
+   matching scope and payload digest, to pass the §4.3
-   authorization — read authority on every canonical record the
+   target-result authorization: read authority, live at replay
-   recorded outcome references, refused otherwise with the
+   time, on every canonical record the recorded outcome
-   constant-shape conflict that preserves RBAC §7's
+   references, refused otherwise with the constant-shape conflict
-   no-existence-oracle rule — while an actor-bound row also
+   that preserves RBAC §7's no-existence-oracle rule. An
-   requires recorded-actor
+   actor-bound row additionally requires recorded-actor equality —
-   equality, and a declared-mode mismatch is a collision. Including
+   never as a substitute for target-result authority — and a
   declared-mode mismatch is a collision. Including
   the **shared-declaration boundary**: `shared` is server-verified
-   against the epoch's canonical seed tuple set re-derived from
+   against the epoch's canonical seed key set (fence-independent,
-   canonical state, a shared declaration outside that set is
+   derived from the epoch id and the fixed seed-role list) and its
-   refused recording nothing, and origination of a missing seed
+   prefix-derived canonical seed tuple set — each position's scope
-   fence requires the full fresh-mutation authorization for that
+   and digest derived from the committed predecessors' recorded
-   seed command (§4.3). Including the **replay access event**: a
+   outcomes — with a shared declaration outside the key set, off
   its position's derived tuple, or past the next unrecorded
   position refused recording nothing (§4.3). Including the
   **seed-boundary gate**: the epoch's immutable seed-origin
   account is the first admin the finalize transaction created;
   every submission on a canonical seed key must be that account
   or hold target-result read authority on the position's recorded
   targets, refused otherwise with the constant-shape conflict
   evaluated before fence presence — so recorded and unrecorded
   worlds are indistinguishable to the refused submitter — and
   origination of a missing seed fence is reserved to the
   seed-origin account passing the full fresh-mutation
   authorization for that seed command (§4.3). Including the **replay access event**: a
   distinct non-mutation audit event class, appended on every
   shared replay, recording the accessing actor, the current
   request's correlation ids, and the fence row returned — the