From 83142e1b7930730ff9824ed7d527430c6b783d07 Mon Sep 17 00:00:00 2001 From: fred Date: Thu, 27 Aug 2026 02:50:32 -0500 Subject: [PATCH] =?UTF-8?q?docs:=20onboarding-wizard=20contract=20revision?= =?UTF-8?q?=2011=20(sol=20r10=20NEW-12/13/14/15:=20world-independent=20suc?= =?UTF-8?q?cession=20with=20conferred=20position-1=20authority,=20unavaila?= =?UTF-8?q?ble-or-unable=20re-succession,=20=C2=A77.1=20predicate=20collap?= =?UTF-8?q?se=20with=20forward=20constraint,=20dual=20identity-surface=20d?= =?UTF-8?q?isclosure)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/requirements/onboarding-wizard.md | 319 ++++++++++++++++++------- 1 file changed, 236 insertions(+), 83 deletions(-) diff --git a/docs/requirements/onboarding-wizard.md b/docs/requirements/onboarding-wizard.md index e82de41c..4d1fed64 100644 --- a/docs/requirements/onboarding-wizard.md +++ b/docs/requirements/onboarding-wizard.md @@ -197,6 +197,38 @@ epoch, restoring D4 re-runnability and §4.4's strand-nothing rule (NEW-11; witnesses §6.7: succession recovery, origin-available refusal, succession race). +Revision 11 (sol re-review 9: NEW-12, NEW-13, NEW-14, NEW-15): succession +itself becomes oracle-free and strand-proof. Succession's conditions are +now **fence-independent**: the submitter's side is exactly platform-level +eligibility plus §5.2 top-level-create eligibility — never any authority +over, or reference to, committed seed records — and the origin's side is +the disjunction _unavailable or unable_: the current origin fails +identity §7.1's single account-unavailability predicate (today exactly +the better-auth ban), or lacks the seed-completion authority defined in +§4.3. Because every input is evaluated without consulting fence rows, +recorded outcomes, or the committed prefix, the command's outcome is +identical across the recorded and unrecorded worlds — the vacuous-prefix +oracle is gone (NEW-12). Successful succession **confers, in the same +transaction and inside its single audit event, the position-1 +initial-owner authority on the seed company where that position is +already originated** — exactly the authority origination of position 1 +would have self-conferred — so every successful successor holds +seed-completion authority by construction and no read-only capture can +strand the suffix; the _unable_ disjunct makes re-succession available +when a later designation loses that authority while staying +identity-eligible, and succession is repeatable across successive losses +(NEW-13). Condition (a)'s eligibility failure collapses to the one +predicate identity §7.1 actually defines, with a forward constraint +binding any future account-removal or account-disable contract to extend +that predicate and to preserve the epoch designation as a stable +reference (NEW-14). §1.2 now discloses both identity-surface additions — +the §7.3 finalize extension and the §7 item 12 succession command — and +succession appears in the §1.1 composed-surface inventory and the §7.8 +mapping amendment (NEW-15). Witnesses §6.7: the succession two-world +control, tenant-unprivileged successor completion, post-succession +grant-revocation re-succession, repeat succession, and empty-prefix +succession. + 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); @@ -230,26 +262,32 @@ through the extensibility rule §2.4). hierarchy commands and the rank-4 enrollment command (contract 5 §3.1 — built first), the settings command family (steps 1–2), the identity bootstrap and registration surface (step 3, including the - §3.3 finalize command), the mode reads (contract 6 §2.2 post-epoch; + §3.3 finalize command and the §4.3 seed-origin succession + command), the mode reads (contract 6 §2.2 post-epoch; the §2.3 bootstrap-status field pre-epoch), and the ordinary content commands used for example seeding (step 4). Two of these families (ranks 1 and 4) are in contract 5 §3.1's live rank-6 composition row; the other four are added by the disclosed §7.8 mapping amendment, without which their operations are unmapped and blocked under contract 5 §5. -2. **The wizard introduces no new mutation surface.** Every state change - it performs is an existing command with its own contract: user and - epoch writes under the identity contract §3, hierarchy writes under - contract 1 §5, grant writes under contract 2 §4, settings writes under - their owning command family. The one exception is the bootstrap - surface, where the wizard drives the bootstrap writer defined by - identity §3 **as amended by the disclosed §7.3 finalize - extension**: the writer's constraints (§3.1–§3.6) bind, and this - contract's single change to them — extending the epoch-closing - command to carry the §3.3 value set inside the same transaction — - is exactly the §7.3 amendment, severable and ratified with this - contract. Beyond that amendment, nothing is added to identity §3, - and no undisclosed authority exists. +2. **The wizard introduces no undisclosed mutation surface.** Every + state change it performs is an existing command with its own + contract: user and epoch writes under the identity contract §3, + hierarchy writes under contract 1 §5, grant writes under contract 2 + §4, settings writes under their owning command family. The + exceptions are exactly the **two disclosed amendments to identity + §3's epoch surface**, each severable and ratified with this + contract: the **§7.3 finalize extension** — the wizard drives the + bootstrap writer defined by identity §3, whose constraints + (§3.1–§3.6) bind, with this contract's single change extending the + epoch-closing command to carry the §3.3 value set inside the same + transaction — and the **§7 item 12 seed-origin succession command** + (§4.3), one mutating epoch-record command with its conferred-grant + clause. Beyond those two amendments, nothing is added to identity + §3, and no undisclosed authority exists; both surfaces appear in + the §1.1 composed-family inventory, the §7.8 mapping amendment, + and §6.1's inventories, so the D8 mapping and authorization-parity + witnesses cannot omit them. 3. **Wizard state derives from canonical state.** Each step renders the system's current configuration (read through the same commands) and applies deltas; the wizard does not keep an answer file whose contents @@ -419,10 +457,19 @@ the named authority: 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 - (recorded outcomes) rather than collide, regardless of any - hierarchy rename performed since — and, because every seed + byte-stable across every re-run and resume **under an unchanged + seed-origin designation**: the same keys carry the same payload + digests, so already-committed mutations replay (recorded + outcomes) rather than collide, regardless of any hierarchy rename + performed since. Where a payload field names the acting seed + origin — position 1's initial-owner field below — the derivation + reads the epoch record's **current designation at origination + time**: a committed position's tuple is pinned by its recorded + outcome and fence digest forever (replays compare against the + recorded digest, never a re-derived one), while an unrecorded + position's derived tuple names the current designation, so a §4.3 + succession changes derived payloads only for positions not yet + originated and can never collide a committed row — and, because every seed submission declares §4.3's `shared` replay mode, they replay for whichever currently eligible admin holding §4.3 target-result read authority on the recorded seed targets performs the re-run, @@ -431,10 +478,12 @@ 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 — 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 §4.3 seed-boundary gate reserves + command under §5.2's eligibility policy, with the epoch's §4.3 + seed-origin account — the account the designation names at + origination time, initially the new admin — as actor, naming that + same account as initial `owner` in the same audited operation + (contract 2 §4.3): the initial-owner field is bound to the current + designation, not to the historical first admin; the §4.3 seed-boundary gate reserves origination of the canonical seed tuples to the epoch's current seed-origin account — initially this admin, thereafter changed only by §4.3 seed-origin succession — while @@ -611,39 +660,81 @@ collects no sensitive category, so v1 ships no custody surface. - **Seed-origin succession.** Loss of the seed-origin account does not strand the epoch (D4, §4.4). The designation changes through exactly one mutating command, an amendment to identity - §3's epoch surface disclosed in §7 item 12: an eligible - platform admin — passing §5.2 fresh-mutation authorization in - full — submits succession naming itself the epoch's - seed-origin. The command succeeds only when, evaluated against - canonical state inside the succession transaction itself: - (a) the current seed-origin account fails identity §7.1 - eligibility (banned, deleted, or disabled) — succession while - the current origin remains eligible is refused — and (b) the - submitter holds §4.3 target-result read authority on every - canonical record referenced by the recorded outcomes of the - committed seed prefix (vacuously satisfied while no position - is committed). A submission failing either condition is + §3's epoch surface disclosed in §7 item 12: a platform admin + submits succession naming itself the epoch's seed-origin. The + command's outcome is **world-independent by construction**: + the submitter-side condition (b) is evaluated against + identity, platform-eligibility, and epoch-record state alone — + never against fence rows, recorded outcomes, the committed + prefix, or any grant attached to a seed record — and the + origin-side condition (a)'s only seed-scope input is the + origin's seed-completion authority, whose recorded-world + component is exactly the authority origination and succession + themselves confer (below), so in any two worlds differing only + in seed existence every condition evaluates identically and + succession carries no existence oracle; the evaluation + consults no fence row, so its timing is fence-independent too + (witness §6.7 two-world control). **Seed-completion authority** means: §5.2 top-level + create eligibility (the full fresh-mutation authorization + position 1 requires) plus, for an account currently designated + while position 1 stands originated, the position-1 + initial-owner authority on the seed company — exactly the + authority whose origination self-confers it (§3.4). The + command succeeds only when BOTH: (a) the current seed-origin + account is **unavailable or unable** — it fails identity + §7.1's account-unavailability predicate (today exactly the + better-auth ban; §5.2 records that no separate deactivated + state exists and identity §7.3 defers hard deletion), or it + lacks seed-completion authority — succession while the current + origin is both available and able is refused; and (b) the + submitter is an identity-§7.1-eligible platform admin holding + §5.2 top-level create eligibility. Condition (b) references no + seed record and no prefix: a tenant-unprivileged platform + admin passes or fails it identically whether or not any seed + position is committed. Any future contract adding an + account-removal or account-disable mechanism MUST extend + identity §7.1's single unavailability predicate to cover it + and MUST preserve the epoch record's designation as a stable + reference across it (a retained identifier or tombstone — + never a cascade that rewrites or nulls the designation outside + this command). A submission failing either condition is refused with the same single constant-shape bounded conflict as the seed-boundary gate, byte-shape-identical whichever - condition failed and whether any seed fence exists — so - succession adds no existence oracle (witness §6.7) — executes - nothing, and appends no event. Successful succession updates - the designation in the epoch record and appends one ordinary - mutation audit event recording the prior designation, the new - designation, and the acting principal; it rewrites no fence - row and no recorded outcome — rows already recorded immutably - retain their original actor. Concurrent successions serialize - on the epoch record: exactly one submitter commits and becomes - the seed-origin, and the loser, re-evaluated against the - committed winner, fails condition (a) — the now-current origin - is eligible — and receives the constant-shape refusal. The - seed-boundary gate and the origination rule always read the - epoch record's current designation: after succession the - successor originates the remaining suffix in order under its - own full fresh-mutation authorization, and the fence rows it - originates record the successor. Factory reset (§4.2) remains - the only path to a new epoch; it is never required to complete - an interrupted seed sequence. + condition failed and whether any seed fence exists, executes + nothing, and appends no event. Successful succession, in one + transaction, updates the designation in the epoch record, + **confers on the successor the position-1 initial-owner + authority on the seed company where position 1 stands + originated** — no more than originating position 1 from an + empty prefix would have self-conferred (§3.4), so succession + escalates nothing beyond the origination role it transfers — + and appends exactly one ordinary mutation audit event + recording the prior designation, the new designation, the + acting principal, and the conferred grant where one was + written; it rewrites no fence row and no recorded outcome — + rows already recorded immutably retain their original actor. + Every successful successor therefore holds seed-completion + authority at commit: a read-only or tenant-unprivileged + capture that strands the suffix cannot exist, and if a later + designation loses that authority while staying + identity-eligible, the _unable_ disjunct of condition (a) + makes re-succession available — succession is repeatable + across successive origin losses, by inability as well as by + unavailability (witnesses §6.7). Concurrent successions + serialize on the epoch record: exactly one submitter commits + and becomes the seed-origin, and the loser, re-evaluated + against the committed winner, fails condition (a) — the + now-current origin is identity-eligible and, holding the + just-conferred seed-completion authority, able — and receives + the constant-shape refusal. The seed-boundary gate and the + origination rule always read the epoch record's current + designation: after succession the successor originates the + remaining suffix in order under its own full fresh-mutation + authorization (supplied by the conferred authority plus its + own eligibility), and the fence rows it originates record the + successor. Factory reset (§4.2) remains the only path to a new + epoch; it is never required to complete an interrupted seed + sequence. - **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 @@ -706,10 +797,14 @@ collects no sensitive category, so v1 ships no custody surface. only the remainder executes, without duplication and without compensating rollback of completed commands. There is no wizard-level transaction spanning steps. Loss of the seed-origin - account mid-sequence is likewise recoverable without a new epoch: - §4.3 seed-origin succession designates an eligible successor, and - the resumed run completes the remaining suffix under the successor - — interrupted runs strand nothing even across origin-account loss. + account mid-sequence — by unavailability (identity §7.1) or by + loss of seed-completion authority — is likewise recoverable + without a new epoch: §4.3 seed-origin succession designates an + eligible successor, confers the position-1 authority where the + seed company exists, and the resumed run completes the remaining + suffix under the successor; succession is repeatable, so + interrupted runs strand nothing even across successive origin + losses. ## 5. Seeding authority (resolves contract 2 review NEW-1) @@ -974,30 +1069,72 @@ Binding on the implementing PRs: 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; **seed-origin succession witnesses (§4.3, NEW-11):** a - **succession recovery** — the seed-origin account commits a - proper seed prefix and is then banned (identity §7.1); an - eligible platform admin holding target-result read authority on - the committed prefix submits succession, the epoch record's - designation changes to the successor with exactly one mutation - audit event recording the prior designation, the new - designation, and the acting principal, and the successor's - resumed run replays the committed prefix (its access attributed - by §4.3 replay access events) and originates the remaining + mode; **seed-origin succession witnesses (§4.3, NEW-11 through + NEW-14):** a **succession recovery** — the seed-origin account + commits a proper seed prefix and is then banned (identity §7.1); + an eligible platform admin holding §5.2 top-level create + eligibility submits succession, the epoch record's designation + changes to the successor with exactly one mutation audit event + recording the prior designation, the new designation, the acting + principal, and the conferred position-1 grant, and the + successor's resumed run replays the committed prefix (its access + attributed by §4.3 replay access events, its read authority + supplied by the conferred grant) and originates the remaining suffix in order — the new fence rows record the successor, the pre-succession rows immutably retain the original origin, and the full seed set completes with no factory reset and no new epoch; an **origin-available succession refusal** — the same eligible admin submits succession while the current origin - remains §7.1-eligible — is refused with the single - constant-shape bounded conflict (asserted byte-shape-identical - to the collision refusal), changes no epoch record, and appends - no audit event; a **succession race** — with the origin banned, - two eligible, prefix-authorized admins submit succession - concurrently: the epoch record serializes them, exactly one - commits and becomes the designated origin with one audit event, - the loser receives the constant-shape refusal, and the seed - sequence completes exactly once under the winner; a submission that failed before commit + remains §7.1-eligible and holds seed-completion authority — is + refused with the single constant-shape bounded conflict + (asserted byte-shape-identical to the collision refusal), + changes no epoch record, and appends no audit event; a + **succession two-world control (NEW-12)** — the SAME + identity-eligible, §5.2-create-eligible platform admin holding + no grant on any seed record submits succession in two prepared + worlds with the current origin banned in both: one where a + proper seed prefix stands committed and one freshly finalized + epoch with no position committed — and in BOTH worlds the + command succeeds, the designation changes to the submitter, and + exactly one succession audit event appends, with the response + asserted equal in shape and error/success class across the + worlds and the evaluation asserted within a fence-independent + timing bound (it consults no fence row); the control is repeated + with a submitter failing condition (b) — refused + byte-shape-identically in both worlds, no record change, no + event in either — proving succession's outcome is a function of + fence-independent inputs only; a **tenant-unprivileged successor + completion (NEW-13)** — the successor of the two-world control's + recorded world, who held no seed-record authority before + succeeding, completes the entire remaining suffix using only the + conferred position-1 authority plus its own eligibility, proving + no read-only capture can strand the suffix; a **post-succession + grant-revocation re-succession (NEW-13)** — after an A→B + succession and further committed progress, B's conferred + position-1 authority is revoked while B remains + identity-eligible; an eligible, §5.2-create-eligible admin C + submits succession and succeeds through condition (a)'s _unable_ + disjunct, receives the conferred authority, and completes the + suffix — no factory reset, exactly one audit event for C's + succession; a **repeat succession (NEW-14)** — A is banned, B + succeeds and commits further prefix, B is then banned, C + succeeds and completes the suffix: each succession appends + exactly one event, every fence row records its true originator + (A's rows, B's rows, C's rows), and the seed set completes; an + **empty-prefix succession (NEW-13)** — the origin is banned + after finalize but before any seed position commits; the + successor succeeds (condition (b) evaluated with no seed record + in existence), originates the ENTIRE sequence, and position 1's + committed payload names the successor as initial owner — + asserting §3.4's derivation reads the current designation for + unrecorded positions; a **succession race** — with the origin + banned, two eligible, §5.2-create-eligible admins submit + succession concurrently: the epoch record serializes them, + exactly one commits and becomes the designated origin with one + audit event and the conferred authority, the loser receives the + constant-shape refusal (re-evaluated: the now-current origin is + eligible and able), and the seed sequence completes exactly once + under the winner; 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 @@ -1124,7 +1261,9 @@ contracts and are not additions: rank-4 enrollment families, is amended to name all six composed families — adding the settings command family, the identity bootstrap and registration surface (including the §3.3 finalize - command), the mode reads (contract 6 §2.2 and the §2.3 + command and the §4.3 seed-origin succession command, so the + official-tool mapping and §6.1's authorization-parity witnesses + cannot omit either), the mode reads (contract 6 §2.2 and the §2.3 bootstrap-status field), and the ordinary content commands used for example seeding — with one mapping row per newly named family. Without this amendment those operations are unmapped and blocked @@ -1156,13 +1295,27 @@ contracts and are not additions: 12. The **seed-origin succession command** (§4.3) — an amendment to identity §3's epoch surface, proposed and ratified here, severable: one mutating command that redesignates the epoch's - seed-origin to an eligible platform admin holding target-result - read authority on the committed seed prefix, valid only while - the current origin fails identity §7.1 eligibility; refusals + seed-origin to the submitter, valid only while the current + origin is **unavailable or unable** — it fails identity §7.1's + account-unavailability predicate (today exactly the better-auth + ban; future removal or disable contracts must extend that one + predicate and preserve the designation, §4.3) or lacks + seed-completion authority — and the submitter is an + identity-§7.1-eligible platform admin holding §5.2 top-level + create eligibility, a condition evaluated against identity, + platform-eligibility, and epoch-record state only, never + against fence rows or seed-record grants, so its outcome and + timing are fence-independent (no existence oracle). Refusals are the constant-shape §4.3 conflict regardless of which - condition failed, the change is one audited epoch-record write - serialized on the epoch record, and recorded fence rows are - never rewritten. Without this amendment a banned or deleted + condition failed; success is one audited epoch-record write + serialized on the epoch record that also confers, in the same + transaction and audit event, the position-1 initial-owner + authority on the seed company where position 1 has originated + — exactly the authority position-1 origination itself confers — + so every successor holds seed-completion authority at commit; + the command is repeatable (a later unavailable-or-unable + successor is succeeded the same way), and recorded fence rows + are never rewritten. Without this amendment a banned seed-origin account strands the unoriginated seed suffix, contradicting PRD D4's no-lock-in requirement (§4.4).