docs: onboarding-wizard contract revision 11 (sol r10 NEW-12/13/14/15: world-independent succession with conferred position-1 authority, unavailable-or-unable re-succession, §7.1 predicate collapse with forward constraint, dual identity-surface disclosure)
ci/woodpecker/pr/ci Pipeline was successful
ci/woodpecker/pr/ci Pipeline was successful
This commit is contained in:
@@ -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).
|
||||
|
||||
|
||||
Reference in New Issue
Block a user