amadan
spec: host lifecycle claim rev 6.28, region HA L1-L20 adopted at their sections
Adds relocating (phase table, recovery region:<r>, box-owned app admission registration), automatic termination fence records and the fence.<box> journal reference, released coverage, writers-stopped observation, the relocation exception to CC11, retained-row reconcile, the files publisher as a replication exception with files reachability, census and enrollment rules (L5, L6, L19, L20), and a moving-to-relocating conversion for a source terminated before the flip (moves 7.19). Pending joint round 18. The Codex analysis is committed beside the spec.
Co-Authored-By: Codex <noreply@openai.com> Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+1150
−116
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+711 −116docs/superpowers/specs/CODEX-ANALYSIS-REGION-HA-L1-L20.md+439 −0
CI cancelled — superseded by a newer push — run details
diff --git a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md| index a580637d5..f342d3961 100644 |
| --- a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| +++ b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| @@ -1,6 +1,6 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-06, **rev 6.27**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-06, **rev 6.28**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| 6.5 added the R6-4 rule. Rev 6.6 added writer epochs (R7-1, amadan #225). |
| Rev 6.7 answered the moves session's notes on §6.4a. Rev 6.8 rewrote §6.4a |
| around writer sessions, for joint round 8. Rev 6.10 answers joint round 10 |
| @@ -27,7 +27,9 @@ and states the narrowed born-covered rule. Rev 6.25 answers the moves |
| spec's rev 7.17 notes (a delete's parks are scoped; a create's first |
| admission declares nothing). Rev 6.26 answers joint round 17's R17-2 (a |
| delete may use the whole-host staging scope). Joint round 17 was CLEAN. Rev 6.27 records Paul's rulings on #236 |
| -(§1.1) and marks §5.9, §6.6, §7.3 and §10.1 ruled, as amended there. Rev 6.9 answered |
| +(§1.1) and marks §5.9, §6.6, §7.3 and §10.1 ruled, as amended there. |
| +Rev 6.28 adopts region HA spec 1 rev 5.4's L1 to L20 (amadan #236) at their sections, pending joint round 18. |
| +Rev 6.9 answered |
| joint round 9 |
| (R9-1 to R9-4) and takes **Paul's ruling R6 (2026-10-04): a box never |
| reuses its local database. Every writer start restores from the |
| @@ -125,9 +127,14 @@ where this section and the proposal text differ, this section wins. |
| evidence. Fencing **execution** needs only that verified |
| `terminated` read. The D5 destroyed-local exception (discharging a |
| fenced box's `park-local` chores without retiring the disk) applies |
| - only when the same read's running-time volume records show every |
| - attached EBS volume `DeleteOnTermination: true`; otherwise those |
| - chores stay open on the operator path. |
| + only with H19's volume-record evidence from enrollment through the |
| + last running record, showing every attached EBS volume had |
| + `DeleteOnTermination: true` and none was removed; otherwise those |
| + chores stay open on the operator path. The worker first persists the |
| + immutable enrollment fence in D2. Each affected claim transition |
| + retains that reference and its host-specific loss consequences before |
| + effects; console quarantine and D4 loss-record materialization are |
| + not prerequisites on this automatic path. |
| - **Operator-attested, for anything not proven terminated** (`stopped`, |
| unclear, missing from the EC2 API): D2 as written; the operator |
| attests the maintained compute fence, a cold quarantine start, and, |
| @@ -163,9 +170,10 @@ where this section and the proposal text differ, this section wins. |
| disabled and no clean-close certificate is issued, until a reviewed |
| Litestream fix or upgrade (#234) makes a certificate safe. Revisit then. |
| -Region HA spec 1 rev 5.4 asks for further claim changes (its §9, L1 to |
| -L20, including a same-region `relocating` op kind). They are not part of |
| -this spec until answered on #236 and adopted in a later revision. |
| +L1-L20 are adopted in rev 6.28 at the sections named in |
| +`docs/superpowers/specs/CODEX-ANALYSIS-REGION-HA-L1-L20.md`, pending joint |
| +round 18, which must include the two-box-per-region model, L18, and the |
| +analysis's extra witnesses (§11). |
| ## 2. The object |
| @@ -286,7 +294,10 @@ Field rules: |
| - **`op.intent`** holds the operation's reconstruction inputs. It is |
| written in the **same CAS** that starts the operation, before any other |
| object is touched (J-N4). |
| -- **`op.journal`** holds the operation's durable phase data. |
| +- **`op.journal`** holds the operation's durable phase data. Relocation |
| + persists §4’s exact source/target enrollments, app-admission and |
| + roster observations, pins, installation identities, evidence, |
| + replacement history and retry counts in its intent and journal. |
| - **`op.exec`** names the one box allowed to run the host's process, or |
| `none`. **`op.participants`** are the boxes the operation involves. Both |
| are per box, per phase (J-D1). See §4. |
| @@ -341,7 +352,12 @@ Field rules: |
| scope is bound to one before its first step runs. Each operation also defines which of them block its own |
| release to `serving`. A release keeps any obligation owned by other |
| lifecycle work (J-D8). |
| -- **`lost`** is the quarantine list for declared-lost boxes (§7). |
| +- **`lost`** records declared-lost boxes (§7), including permanently |
| + ineligible terminated enrollments as well as operator quarantine. |
| + Enrollment-qualified `evidence_refs`, stable `loss_refs` and pending |
| + automatic loss consequences survive operation replacement, `free` |
| + and holder replacement until D4’s durable records contain them. |
| + Automatic termination does not invent a quarantine revision. |
| - **Box references** (`op.exec`, `op.participants`, `holder.writer_box`, |
| admissions' `box`, `writes_lost.box`, `inventory` keys, `lost`, |
| `box:<b>` owners, execution-lease keys) are **opaque identifiers |
| @@ -349,8 +365,11 @@ Field rules: |
| name exactly one machine: two machines presenting one reference would |
| be one box to the claim and defeat the `op.exec == box` check. How a |
| box obtains a unique reference, and refuses claim work when it cannot |
| - prove uniqueness, is the box-identity design's (amadan #212); until |
| - that lands, deployments must not let two boxes share a label. |
| + prove uniqueness follows §1.1 P3 and D2: platform references use |
| + #212 option B’s label key, bound by the sole roster to verified |
| + `boxid` evidence and immutable enrollment/cloud identity. Rebinding |
| + an enrollment to another machine is refused. Existing references |
| + also require the configured tofu instance-ID match at enrollment. |
| - **`retired_incarnations`** keeps the most recent 32 incarnations that |
| held this host. A create whose incarnation appears there is refused |
| (R3-12). |
| @@ -384,7 +403,18 @@ operation. That storage is: |
| - `parked/` and `superseded/`; |
| - the host's local files. |
| -The serving process's ordinary replication is the one exception. |
| +The admitted session’s files publisher is an ordinary-replication exception |
| +alongside database replication. It is bound immutably to |
| +`{location,generation,session}` and may publish only content objects and the |
| +manifest under that session’s authorized files prefix. |
| + |
| +Content objects are create-only. Manifest replacement is conditional and |
| +ordered by its sequence. File deletion is a manifest tombstone, not a |
| +bare-key object deletion. |
| + |
| +The publisher participates in fencing, producer shutdown, request deadlines |
| +and retirement evidence. A new session creates a new generation-bound |
| +publisher. |
| Every destructive storage call names **an exact object version**: a |
| `DeleteObject` with `VersionId`, or a `CopyObject` from |
| @@ -470,7 +500,8 @@ listing snapshot. Admission checks happen at: |
| - every spawn (wake, Seed, a probe, a recovery); |
| - restore and any other local mutation; |
| -- reconcile's decision to create or keep a row; |
| +- reconcile's decision to create a row, or retain it subject to the |
| + bounded retention exception below; |
| - a door read. |
| Admission requires all of: |
| @@ -482,6 +513,27 @@ Admission requires all of: |
| **Region equality alone never grants admission.** Ordinary wake and a |
| recovery probe are distinct permissions (J-D1). |
| +Reconcile may retain an existing row between direct claim checks, with a |
| +maximum ten-minute sweep interval. This exception grants only retention of |
| +the row. |
| + |
| +Creating a row, changing its ownership or installation, reopening a hold, |
| +materializing state, admitting a writer and spawning application code still |
| +require fresh authority. Existing activator or registry state is not a |
| +substitute. |
| + |
| +Relocation participants follow the operation’s phase table. Former executors |
| +remain held until exact inventory-bound local retirement archives and |
| +removes their rows. Reconcile never deletes such a row by hostname alone. |
| + |
| +Executor-change notifications trigger prompt fresh reads for affected rows. |
| +Read failure retains existing state, creates no row and grants no additional |
| +permission. It does not terminate already-authorized ordinary serving solely |
| +because the control read failed. |
| + |
| +CC10 clears a stale hold only on the current serving executor with a |
| +matching installation and expected `hold_op`. |
| + |
| **C5. Revocation needs stop evidence** (§6.1) from every box that may run |
| the host, **or** a lost-box fence (§7). |
| @@ -507,6 +559,7 @@ covers background passes (§6.4) and door reads (§6.5) (J-N8, J-N10). |
| | `deleting`, `parking` | this (§5.2) | the console's pass for the claim steps; each obligation's owner for its chore | |
| | `purging` | this (§5.3) | the console's pass | |
| | `placing` | this (§5.4) | the console's pass | |
| +| `relocating` | this (§4), region HA §5.8 | `region:<r>` | |
| | `moving`, `landing`, `reverting`, `restoring` | move-any-app | as that spec names, one writer per transition | |
| | `pushing` | later | later | |
| @@ -518,8 +571,112 @@ not by itself transfer execution authority: `op.exec` changes only by a |
| CAS that cites stop evidence or a lost-box fence. |
| Only one operation runs at a time, and a new one starts from `serving`. |
| -The start CAS also fails if any open obligation names a region or box the |
| -new operation will write (CC11). A pending chore there must finish first. |
| +Except for the relocation exception below, the start CAS also fails if |
| +any open obligation names a region or box the new operation will write |
| +(CC11). A pending chore there must finish first. |
| + |
| +A `relocating` start may coexist with a `park-generation` obligation in its |
| +region when the operation writes a fresh generation and the shared |
| +live-object view protects every database baseline, files reference and |
| +operation pin that relocation may read. |
| + |
| +The exception does not authorize writing into or resurrecting a generation |
| +already selected for retirement. New pins must be established under the |
| +required leases and fresh claim authority before conflicting retirement can |
| +proceed. |
| + |
| +Whole-location `park-replica` obligations, overlapping staging retirement |
| +and local retirement on any box the operation will materialize remain |
| +blocking. A dead source’s local obligation does not block a failover that |
| +writes only a different target. |
| + |
| +This exception applies only to relocation. Other operation starts retain |
| +CC11. Existing chores retain their original operation identity and remain |
| +executable after the new operation starts. |
| + |
| +**Same-region relocation (L1).** `relocating` changes the executor of a |
| +supported single-executor host within its current region. It starts only from `serving`. It preserves the holder |
| +incarnation, ownership binding, record region and `holder.location`. It is |
| +mutually exclusive with every other host operation. |
| + |
| +Its recovery owner is `region:<r>`. Any eligible enrolled worker of that |
| +region may replay its journal under the required leases. Regional recovery |
| +authority does not grant that worker execution authority: only `op.exec` may |
| +install or admit a writer where the phase permits it. |
| + |
| +The start CAS records the exact source and target boxes and enrollments, |
| +region, reason, source stamp and generation, roster observation, |
| +app-admission identity, and any termination-fence reference. Every |
| +transition compares the operation ID, expected phase and claim ETag. |
| +Replacement history, evidence, pins, installation identities and retry |
| +counts remain durable within the same operation. |
| + |
| +| Phase | Execution authority | Permitted work | |
| +|---|---|---| |
| +| `starting` | Source, or `none` for an evidenced failover | Existing source service; new source admission only after its D6 authority is active | |
| +| `releasing` | Source until its full stop evidence | Source admission only before the durable admission fence closes; then release work only | |
| +| `pinning` | `none`, preserving the prior stamp | Select and journal exact recovery versions | |
| +| `installing` | Selected target, with a new installation stamp | Build the prepared generation and materialize inventoried local state; no writer admission | |
| +| `installed` | Selected target | Verify prepared authority and complete that target’s local installation receipt; no writer admission | |
| +| `probing` | Selected target | Cold probe admissions only | |
| +| `probe-failed` | Failed target until full stop evidence or a fence | Release and cleanup only | |
| +| `serving` | Successful target | Ordinary serving under the latest admitted generation and stamp | |
| + |
| +A transition revoking execution cites complete stop evidence or a valid |
| +lost-box fence and preserves the previous stamp when it installs nothing. A |
| +transition granting execution for a new installation writes its resulting |
| +claim generation as `holder.stamp`. Every materializing box is added to |
| +`touched.boxes` before its first effect. |
| + |
| +The prepared generation is opened at most once. The first probe may keep the |
| +installation stamp only under §6.4a’s existing `KeepStamp` condition. Later |
| +attempts admit fresh generations and restore their actual predecessors. |
| +Neither recovery nor final release resets `holder.generation` or |
| +`holder.stamp` to the original prepared installation. |
| + |
| +Each target supplies a local installation receipt bound to its box, |
| +enrollment and the journalled stamp of the CAS that granted that |
| +installation execution authority. Later writer stamps do not invalidate that |
| +receipt. The target must complete that receipt before entering `probing`. |
| +After the first admission in that installation’s lineage, recovery |
| +must not replay the original files, environment or timer installation. |
| + |
| +Replacement follows region HA §5.8’s phase-specific table. An unopened |
| +completed prepared generation may be reused by a replacement that makes its |
| +own local installation. Loss after admission requires nested recovery from |
| +the latest admitted lineage. Every abandoned local installation receives an |
| +exact `park-local` obligation unless its destruction is separately |
| +established. |
| + |
| +Source termination during `starting` or `releasing` may convert the existing |
| +operation to failover. The conversion records the fence, revokes source |
| +execution, preserves the stamp and removes only that source from the |
| +acknowledgement barrier. A replacement participant must acknowledge before |
| +performing phase work. |
| + |
| +**A move whose source is terminated before its flip (moves 7.19).** A |
| +termination fence for the source of a `moving` operation that has not |
| +reached its flip (the instance record's commit has not happened) may |
| +convert that operation to `relocating` in one CAS: it records the fence |
| +(`fence.<box>`), sets `op.exec = "none"`, preserves `holder.stamp` and |
| +`holder.generation`, starts `relocating` at `pinning` in the source's |
| +region, and leaves every obligation untouched. The move's staging park |
| +(`park-replica` scoped `moves/<host>/<op id>`, owned by the target |
| +region) keeps its own operation id and stays executable under the new |
| +operation, as every chore does (C2); it does not block the conversion or |
| +the relocation's release. After the flip this conversion is refused; the |
| +move's own §7.10 recovery applies. |
| + |
| +The operation permits two target replacements. Exhaustion records `stuck` |
| +without resetting the count or inventing stop evidence. Necessary denial and |
| +cleanup continue; another handover requires valid evidence and explicit |
| +recovery authority. |
| + |
| +Successful release requires the selected target’s verified probe and |
| +completed admission/publication steps. It preserves all outstanding |
| +obligations. Disjoint generation parks and former-box local retirement do |
| +not block serving on the new executor. Whole-location retirement, |
| +conflicting local retirement and `quiet_after` remain binding. |
| ## 5. This spec's operations |
| @@ -541,11 +698,17 @@ new operation will write (CC11). A pending chore there must finish first. |
| was absent. A 412 means something wrote the claim since, possibly a |
| purge fence. The create then restarts from step 0, with a new |
| registration. The claim moves from free or absent (§9) to |
| - `{holder: new, op: {creating, id, intent: {record body, key}}}`. This |
| + `{holder: new, op: {creating, id, intent: {record body, key, executor, |
| + enrollment}}}`. Select the executor once using P5-D2's `choose()` |
| + before this CAS and persist the exact box and enrollment. This |
| is refused if the incarnation is in `retired_incarnations`, or if the |
| app holds a purge reservation (§5.3). |
| 3. `CreateRecord`, create-only. |
| -4. **CAS** `op` to `serving` and set `exec` to the record region's box. |
| +4. **CAS** `op` to `serving` and set `exec` to the exact box recorded in |
| + the create intent, validating its recorded enrollment and required |
| + acknowledgement. |
| + Completion and recovery never substitute another box. If that box |
| + cannot complete, cancel only after P5-D6's uncertain effects settle. |
| 5. **Recovery,** by the console's claim-recovery pass, which lists |
| `control/hosts/` every few minutes and handles claims whose `op` is not |
| `serving` and older than five minutes: |
| @@ -706,9 +869,9 @@ replays it. Moves and placements therefore exclude each other. |
| ### 5.9 Console operation contracts (rev 6.18, RULED, as amended by §1.1) |
| -**Status: ruled 2026-10-06, as amended by §1.1 (originally proposed).** These close the gaps Plan 5's draft found (P5-D1 to P5-D6). Each says where it would land in §2, §5, §6, §8 and §9 once ruled, and how amadan #232 (host ownership; Paul decides its direction) would change it. Paul's decisions are listed in amadan #236. |
| +**Status: ruled 2026-10-06, as amended by §1.1.** These contracts close the gaps Plan 5's draft found (P5-D1 to P5-D6) and govern §2, §5, §6, §8 and §9. Apply amadan #232's ownership and backfill direction as ruled in §1.1. Paul's decisions are listed in amadan #236. |
| -The text below depends on the proposed §7.3 and §10.1 contracts. It does not treat them as approved. The referenced #212 design is also unsettled: its current header recommends an alternative and records unresolved review findings. |
| +The dependencies in §7.3 and §10.1 are ruled, as amended by §1.1. Box references follow §1.1 P3's label-key ruling for #212. |
| All additions are additive. IDs are random 128-bit values encoded as 32 lowercase hexadecimal characters. Timestamps use UTC RFC3339Nano. Structured values stored in `op.intent` or `op.journal` are JSON-encoded strings, preserving their existing `map[string]string` representation. |
| @@ -760,22 +923,39 @@ For an absent claim, `absent` is true and `etag` and `gen` are omitted. The cons |
| A registration lasts **90 seconds**, renewed every **20 seconds**. The owner stops issuing work five seconds before its acknowledged expiry. Draining treats it as expired only five seconds after expiry. These rules require clock skew bounded by five seconds; inability to satisfy that bound refuses admission. |
| -Only the exact owner tuple may renew. Renewal cannot recreate a missing entry, revive an expired controller, change its incarnation, or cross an app ID or epoch. An ambiguous renewal does not extend the controller’s acknowledged deadline. Another console recovers the claim; it does not impersonate the registration owner. |
| +Only the exact owner tuple may renew. Renewal cannot recreate a missing entry, revive an expired controller, change its incarnation, or cross an app ID or epoch. An ambiguous renewal does not extend the controller’s acknowledged deadline. The operation’s named recovery owner recovers the claim; it does not impersonate the registration owner. |
| The ordering remains: |
| 1. Read and retain the claim observation. |
| 2. Register while admission is open and no purge reservation exists. |
| -3. Bind the server-assigned incarnation. |
| +3. Bind the server-assigned incarnation for create, or the existing |
| + holder incarnation for another host-operation start. |
| 4. Re-read admission as the final check. |
| 5. Attempt the claim CAS **once**, against the original observation. |
| -A conflict restarts the entire sequence with a new operation ID, registration and creation time. Accepted operations may finish while admission is closed. Their existing registrations may renew, but no new registration is admitted. |
| +A conflict restarts the entire sequence with a new operation ID and registration, and a new creation time for create. Other operation starts retain the existing holder incarnation. Accepted operations may finish while admission is closed. Their existing registrations may renew, but no new registration is admitted. |
| Recovery removes a completed registration only after its claim and effect journal establish completion or cancellation. Expiry alone never removes a registration whose claim still names its operation. Before discarding an expired, unaccepted start, recovery invalidates its saved claim revision, or records evidence that it has already changed. Purge uses P5-D4’s fence procedure. |
| Other host-operation starts use the same registration mechanism with their own `kind`, saved claim observation and existing incarnation. This lets placement and purge drain delayed move or delete starts as well as creates. |
| +A regional worker starting `relocating` registers the start under the same |
| +app-admission protocol, using an owner tuple `{box, enrollment, controller}` |
| +instead of a console owner. Its authority is limited to registrations for |
| +eligible hosts in its region. It grants no backend-effect, placement, purge |
| +or roster-writing authority. |
| + |
| +The registration binds the saved claim observation, existing holder |
| +incarnation, app ID and admission epoch. Closed admission or an exclusive |
| +app operation refuses the start. The worker revalidates admission |
| +immediately before its single start CAS. Purge and placement drain these |
| +registrations using the same saved-revision fencing rules as other starts. |
| + |
| +Recovery of an accepted relocation proceeds from the claim and does not |
| +impersonate an expired registration owner. Missing registration authority |
| +makes the start unsupported. |
| + |
| Admission is **never deleted**. Recreation requires the old purge to be complete, its journal absent, and its effects drained. The new app reserves a new `app_id`, then conditionally reopens admission with a higher epoch. Old renewals and removals consequently cannot affect it. |
| Rejected alternatives: |
| @@ -819,7 +999,7 @@ They contain `box`, `enrollment`, `boot_id`, `reservation`, `directory_revision` |
| A missing report, unknown actor, duplicate record, ambiguous identity, unexplained route, partial listing or undecodable body refuses adoption or the affected operation. |
| -For a **new, single-executor host**, evaluate the complete eligible set. Choose the greatest hexadecimal SHA-256 of: |
| +For a **new, single-executor host**, use region HA's `choose()` over the complete eligible set: prefer a box running no instance of this app, then the most headroom (until spec 2, the fewest claimed hosts), then the greatest hexadecimal SHA-256 of: |
| ```text |
| host + "\x00" + box-reference |
| @@ -827,6 +1007,16 @@ host + "\x00" + box-reference |
| Break a tie by the smallest box reference. Persist the selected box and enrollment in the create intent. Selection happens once; recovery never substitutes a newly available box. The selected participant must satisfy D7 and the first-phase acknowledgement barrier before completion. |
| +Selection precedes the initial create claim CAS and every backend effect. |
| +If the selected box cannot complete, P5-D6 cancellation first settles all |
| +uncertain effects; a missing acknowledgement alone does not settle them. |
| + |
| +A move keeps the requested target region as input and uses `choose()` |
| +once to select its target box and enrollment in the start CAS. Readiness, |
| +installation, evidence and recovery bind to that selection. Replacement |
| +requires an explicit fenced transition legal under the moves protocol; |
| +relocation's replacement table does not authorize move replacement (L15). |
| + |
| For **legacy adoption**, selection is not scheduling. Require evidence identifying exactly one current installation owner. A hibernating installation still has an owner. Zero or multiple provable owners refuse adoption pending repair. |
| `op.exec` remains singular. Records whose intended behavior requires several simultaneous serving boxes, including applicable everywhere/static shapes and nonempty `Record.Replicas`, cannot be silently reduced to one executor. Independent replica records with distinct hosts may each have one executor. A route-only installation with no representable holder is unsupported; do not fabricate a provisioning record during adoption. |
| @@ -841,7 +1031,7 @@ Rejected alternatives: |
| **Effect of #232:** Yes. Its adoption direction replaces §9’s lazy entry points with the frozen, deployment-wide backfill. The census above remains necessary, but only the backfill may adopt. Doors and recovery refuse unclaimed legacy records, and orphan cleanup honors `control/hosts-quarantine.json`. |
| -**PAUL:** Accept #232’s backfill-only adoption and temporary create freeze, or retain lazy adoption with the complete census above. Recommended default: accept backfill-only adoption. Neither option permits choosing a winner among conflicting legacy records automatically. |
| +**Ruled (§1.1 P4):** Use #232’s backfill-only adoption and temporary create freeze. Choosing a winner among conflicting legacy records automatically remains forbidden. |
| --- |
| @@ -874,9 +1064,9 @@ fence_id, inventory_sha256, local_journal_sha256 |
| The box retains the corresponding durable admission fence. It may not reopen the evidenced installation merely because the operation’s worker restarted. |
| -Each obligation gains `evidence_refs`, containing immutable receipt keys and digests, or the accepted Plan 8 loss-record reference. These references survive operation replacement. Discovery chores retain their discovery operation ID. |
| +Each obligation gains `evidence_refs`, containing immutable receipt keys and digests, an accepted Plan 8 loss-record reference, or D2’s verified automatic enrollment-fence reference. These references survive operation replacement. Discovery chores retain their discovery operation ID. |
| -A remote park scope is bound only after evidence covers **every box that could still write that location**. Its `evidence_at` is the latest original evidence time among those sources. A lost-box source uses the declaration’s persisted `fenced_at`. Retries never replace either with the current time. |
| +A remote park scope is bound only after evidence covers **every box that could still write that location**. Its `evidence_at` is the latest original evidence time among those sources. A lost-box source uses the declaration’s persisted `fenced_at`, or the automatic fence’s persisted original observation time. Retries never replace either with the current time. |
| For legacy discovery, the non-serving box establishes stop or empty evidence under cleanup-only authority. The current executor’s existence elsewhere does not prove that box empty. An unavailable box requires the existing lost-box procedure or remains pending. |
| @@ -893,7 +1083,7 @@ The regional adapter shall: |
| 1. Verify its own enrollment, region and access to the exact bucket. |
| 2. Acquire and renew all required replica and staging-work leases. |
| 3. Freshly validate the claim, obligation, phase, immutable scope and evidence. |
| -4. Obtain the moves-owned live-set view bound to that claim observation. |
| +4. Obtain P6-D3’s combined database and files live-set view bound to that claim observation. |
| 5. Execute Plan 4’s exact-version park. |
| 6. Acknowledge with the chore’s own operation ID, updating `quiet_after` in the same CAS. |
| @@ -907,6 +1097,11 @@ Rejected alternatives: |
| - Empty heartbeat or missing inventory entry as empty disk: neither is a complete scan. |
| - Recomputing evidence time on retry: this loses the original retirement horizon. |
| +Automatic termination uses D2’s immutable enrollment-fence transport, |
| +with D3/D4’s claim-bound host consequences before effects. Console |
| +materialization of loss records may follow recovery; it preserves the |
| +fence’s original observation time and every pending loss identity. |
| + |
| **Effect of #232:** No change to parking or evidence. Backfill becomes the source of adoption discovery chores. |
| --- |
| @@ -1030,7 +1225,7 @@ Rejected alternatives: |
| **Effect of #232:** Record-backed placement is unchanged because ownership does not transfer. Minted, route-only hosts remain app-name-owned under #232; that does not supply a lifecycle transfer protocol for them. |
| -**PAUL:** Accept this limited flagged placement scope, or require general fleet/stateful placement before activation. Recommended default: accept the limited scope and specify stateful fleet transfer separately. Unsupported placement must refuse the whole request, not partly update the app. |
| +**Ruled (§1.1 P5):** Use the limited record-backed placement scope; stateful fleet transfer needs its own spec. Unsupported placement must refuse the whole request, not partly update the app. |
| --- |
| @@ -1038,6 +1233,12 @@ Rejected alternatives: |
| *Extend §5.1, §5.2, §5.3 and §8.* |
| +The create intent records P5-D2’s selected executor and enrollment in |
| +the initial claim CAS, before effects. Completion and recovery use only |
| +that selection. If it cannot complete, cancellation follows the effect |
| +settlement rules below; missing acknowledgement never permits discarding |
| +an unresolved effect. |
| + |
| A create’s initial claim intent includes: |
| ```text |
| @@ -1103,7 +1304,7 @@ Rejected alternatives: |
| **Effect of #232:** Yes. Reuse its `acq` identity, pending/committed marker states, incarnation binding and conditional detach. Its proposed first-route ordering must be amended so lifecycle intent exists before this create writes the marker. Add its cross-family verification before record creation. Reuse its app-name operation journal rather than creating a competing rename journal. |
| -**PAUL:** The record-backed rename/account-transfer refusal is the same migration-scope decision already raised by #232. Recommended default: retain the refusal until the transfer protocol exists. |
| +**Ruled (§1.1 P6):** Refuse record-backed rename and account transfer until the transfer protocol exists. |
| ## 6. Mechanisms |
| @@ -1134,9 +1335,31 @@ certified as stopped just because its parent exited. Its host needs the |
| cleanup operation first. A box without cgroup delegation cannot produce |
| evidence, so lifecycle operations on its hosts are refused. |
| +**Release before full stop (L10).** Release may collect a distinct |
| +`writers-stopped` observation while the host’s replicator remains open. It requires the durable admission fence, |
| +settled spawn reservations, drained application and timer work, an empty |
| +complete containment tree, and a complete privileged descriptor scan. |
| + |
| +The only permitted database, WAL or SHM holders are descriptors positively |
| +identified as belonging to this host’s admitted replicator, bound to the |
| +agent’s process-start identity, boot, controller and writer session. Other |
| +descriptors in the same process are not exempt. An incomplete scan or |
| +uncertain identity fails the observation. |
| + |
| +This observation permits the fenced release controller to perform the final |
| +database sync and files/wake-state flush. It grants no execution handover, |
| +retirement acknowledgement, clean-close certificate or writer admission. |
| + |
| +The controller then closes or terminates and joins every producer. Full stop |
| +evidence still requires the unrestricted §6.1 checks, including no remaining |
| +database holders. `Collect` retains that meaning. |
| + |
| +A successful final sync does not prove all maintenance producers stopped |
| +(P6-D4). Failed producer shutdown leaves release pending or stuck. |
| + |
| **Probes (CC13).** Every lifecycle probe renders the **held** config and |
| materializes the **held** release (`RenderHeld`, `MaterializeHeld`) |
| -before it spawns. That covers moves, reverts and a future push. A probe |
| +before it spawns. That covers moves, reverts, relocation and a future push. A probe |
| never uses whatever the ordinary passes last wrote. |
| ### 6.2 Parking, by exact version (J-N1, J-N6, J-N7, J-D5) |
| @@ -1222,7 +1445,9 @@ So the sweep lists: |
| that completes after its move's cleanup would otherwise stay there for |
| good; |
| - every generation within the live `holder.location` other than |
| - `holder.generation` (the moves spec's dead generations). |
| + `holder.generation`, selecting only versions outside the combined |
| + database and files live set below. Protected files may remain after |
| + their generation’s database objects have been retired. |
| Anything found is parked as a further retirement event (§6.2), under a |
| new obligation the sweeping box owns, with a `park` scope (§2). On a |
| @@ -1278,12 +1503,32 @@ or being retired here, so reaching one as a needed baseline refuses, and |
| alerts. Only this region's generations in the run are part of this |
| bucket's live set. |
| +**Files in the live set (L13).** The live-object view includes the |
| +manifests from the selected files pin through the current admission, every running operation’s pinned manifest, |
| +and every object those manifests reference. Database and files protection |
| +are computed independently and combined before retirement. |
| + |
| +`files/<generation>/` belongs to that generation for classification. A |
| +generation park retires only versions outside the combined live set. |
| +Referenced files may outlive retirement of that generation’s database |
| +objects. |
| + |
| +Every destructive step, including replay of a persisted retirement manifest, |
| +revalidates the live view. Unknown classification or conflicting authority |
| +refuses mutation. Classification remains possible after an exact source |
| +version has already been deleted. |
| + |
| +Completion means all currently eligible residue has been retired and the |
| +normal horizon verified. Protected file objects remain live; when no live |
| +manifest references them, the at-rest sweep owns their retirement. |
| + |
| **What a sweep never touches (Q3, R4-3).** This spec owns the sweep, so |
| it owns this rule. The **live set** is the triple |
| `{authoritative region, holder.location, holder.generation}`, together |
| -with the exact object versions the moves spec supplies for that |
| -generation, including any pinned noncurrent version (moves owns |
| -generation-specific live-object selection). |
| +with the exact object versions supplied by P6-D3, including pinned |
| +noncurrent versions, unfinished database baselines, operation pins and |
| +the independently computed files live set above. Moves and relocation |
| +use this combined view. |
| - **In the authoritative region's bucket only**, the sweep never parks or |
| deletes an object version in the live set. It never touches the |
| @@ -1296,7 +1541,8 @@ generation-specific live-object selection). |
| The authoritative region is the region of the holder's current |
| installation, as the claim names it. That is `op.exec`'s region while |
| -serving, or what the moves spec's phase table names during a move. |
| +serving, what the moves spec's phase table names during a move, or the |
| +unchanged region of a relocation. |
| The marker's format and its If-Match write rules are the moves spec's |
| (rev 7.4 §6.4). The sweep reads the live set under the same fresh claim |
| @@ -1307,7 +1553,8 @@ raises an alert. |
| On acknowledging, the owner CASes the claim's `quiet_after[region]` to at |
| least `evidence time + H`. Any install into that region's host namespace |
| waits until `quiet_after` has passed: a create's first wake, a move's |
| -landing, a push. This holds even after `free`. |
| +landing, a relocation's target installation, a push. This holds even |
| +after `free`. |
| IAM: the box needs `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| `s3:DeleteObjectVersion` on its own data bucket. Today it has only |
| @@ -1480,7 +1727,10 @@ issues any upload**. It requires: |
| - an op kind that permits writing: **never `creating`, `deleting`, |
| `parking`, `purging` or `placing`** (R10-4). A first writer comes after |
| `CompleteCreate`, under `serving`, and nothing writes while a placement |
| - runs; |
| + runs. For `relocating`, §4's phase table is also mandatory: no admission |
| + in `pinning`, `installing`, `installed` or `probe-failed`; `probing` |
| + admits cold probes only, and source admission in `starting` or |
| + `releasing` requires the stated authority and open admission fence; |
| - `op.exec == this box`. **Only `op.exec` may open replication, in every |
| op kind.** At most one box writes a host's replica at any time, and |
| `op.exec` names it. A landing target, a probe box or a recovering |
| @@ -1531,7 +1781,7 @@ the `park-generation` chore (§2): `{region, generation}`, owned by |
| The admission never replaces the operation. Kind, id, phase, intent, participants, |
| obligations and the rest of the journal are kept. **Recovery inside |
| -`landing`, `restoring`, `reverting` or a probe is therefore an |
| +`landing`, `restoring`, `reverting`, `relocating` or a probe is therefore an |
| `AdmitWriter` within that operation**, never a new operation (R8-2). The |
| moves spec's phase table says when `op.exec` is handed to which box. |
| @@ -1661,6 +1911,31 @@ reached, and where their wording differs, this text wins. |
| whose target gave its evidence (dirty flag known and clear) and |
| which no declared-lost box ended. It speaks for two sessions only: |
| the target's probe session and the source's cut session. |
| + - `released` accounts for the exact predecessor session through a completed |
| + live-box release. It is legal only for a cold admission under |
| + `relocating`, bound to the current operation and phase. |
| + |
| + The predecessor is the last admission entry, using the existing holder |
| + fallback only when the list is empty. Its box, session and generation must |
| + match the release journal and full stop receipt. The receipt must identify |
| + the same incarnation and released installation. |
| + |
| + The release records the stopped database’s final TXID and the final |
| + files/wake-state manifest sequence. The verified recovery pin must reach |
| + those values. For a nonempty database, coverage applies only to the first |
| + admission opening the prepared generation built from that pin. |
| + |
| + For an evidenced zero-position database, coverage may instead apply to the |
| + first cold empty-bootstrap admission bound to that release, after the final |
| + files and wake-state pin is verified. No zero-position snapshot or anchor is |
| + written. |
| + |
| + `released` suppresses only the ordinary loss declaration for that matched |
| + predecessor. It does not certify request completion, permit warm admission, |
| + set `covered`, or suppress other required declarations. Subsequent |
| + admissions must establish their own coverage; they cannot reuse the |
| + operation’s earlier release. |
| + |
| - `""`: anything else. Without a certificate it records |
| `writes_lost` (the predecessor). A return the console released because the target is |
| lost is `""`, and it declares **every target session since the |
| @@ -1683,12 +1958,13 @@ reached, and where their wording differs, this text wins. |
| the list, the library records it in the admitting CAS. **Alerts:** |
| the admitting box raises one alert per declaration after the CAS |
| succeeds, and retries until delivered; the console's durable loss |
| - record (proposed §7.3 D4) is the long-term copy, so trimming a |
| + record (§7.3 D4) is the long-term copy, so trimming a |
| covered entry never loses a declaration. |
| 3. **The baseline** of a cold admission is the predecessor |
| generation's remote, as far as it goes, with two cases. A prepared |
| generation (built by a landing, a push or a dirty rollback from a |
| - sealed archive, before any writer) is restored from its own pinned |
| + sealed archive, or by relocation from a journalled recovery pin, |
| + before any writer) is restored from its own pinned |
| snapshot in the admitting box's region, and is opened at most once, |
| so a restarted probe takes a fresh generation restored from it. In |
| an unfinished run the baseline is the newest generation in the run |
| @@ -1743,7 +2019,10 @@ reached, and where their wording differs, this text wins. |
| - any other region: left uncovered, no chore, and the walk goes on. |
| It is legal wherever a writer may run, and refused in `creating`, |
| - `deleting`, `parking`, `purging` and `placing`. Retirement of a |
| + `deleting`, `parking`, `purging` and `placing`. Under `relocating`, |
| + `PublishGeneration` also requires §4's phase-specific writer authority |
| + and P6-D3's verified publication; recognizing the kind alone grants |
| + no permission in installation or cleanup phases. Retirement of a |
| superseded generation happens only through it, or through item 6. A |
| writer that dies before this CAS leaves its entries for the next |
| publication. Chore ids are opaque. |
| @@ -1768,8 +2047,10 @@ reached, and where their wording differs, this text wins. |
| 8. **A new agent process** stops any app it finds running for a host, |
| admits a new session, and only then restarts the app. It never |
| reattaches to a unit started under a dead session. |
| -9. **Lost boxes.** A declared-lost box's timers are declared on the |
| - console's record, and alerted. Adoption sets `holder.writer_box` to |
| +9. **Lost boxes.** A declared-lost box's timers are durably declared and |
| + alerted under §7.3 D4. The automatic path first retains the loss |
| + consequences in the claim, pending the console's durable record. |
| + Adoption sets `holder.writer_box` to |
| the box running the pre-release process; before the first writer of |
| a new incarnation it is `""`. |
| @@ -1988,7 +2269,7 @@ every console. But safety does not depend on draining them. |
| ### 6.6 Box-side contracts (rev 6.19, RULED, as amended by §1.1) |
| -**Status: ruled 2026-10-06, as amended by §1.1 (originally proposed).** These close the gaps Plan 6's draft found (P6-D1 to P6-D8). They reference the proposed §5.9, §7.3 and §10.1 as dependencies, not as approved text. Paul's decisions are listed in amadan #236. Not yet read against amadan #234's discussion text (the certificate analysis rests on the pinned Litestream v0.5.14 source). |
| +**Status: ruled 2026-10-06, as amended by §1.1.** These contracts close the gaps Plan 6's draft found (P6-D1 to P6-D8). Their dependencies in §5.9, §7.3 and §10.1 are ruled on the same basis. Paul's decisions are listed in amadan #236. The certificate analysis rests on the pinned Litestream v0.5.14 source; §1.1 P7 rules cold-only activation. |
| #### P6-D1. Privileged stop collection and durable evidence |
| @@ -2009,7 +2290,24 @@ The collector derives artifact paths, unit names and cgroups from validated inve |
| Under hostguard, the collector validates ordinary operation authority or the cleanup authority defined in P6-D6. It durably records a fresh `fence_id` and the exact target tuple in the existing local guard state. Every app-code admission, root launch and host-work reservation checks this fence. The fence denies new work for the evidenced session without retiring its installation stamp. |
| -The collector then releases hostguard. The agent closes its matching in-memory admission fence, cancels and joins selected work, drains timer deliveries and spawn attempts, stops all application roles, and closes or terminates every replication and maintenance producer. It returns a drain acknowledgement bound to the collector’s fence and controller tuple. `FenceAndStop`’s process-local object is not serialized as evidence. |
| +The collector then releases hostguard. The agent closes its matching |
| +in-memory admission fence, cancels and joins selected application work, |
| +drains timer deliveries and spawn attempts, and stops all application |
| +roles. For full stop evidence it must also close or terminate and join |
| +every replication and maintenance producer. The release path may collect |
| +the intermediate observation below before that producer shutdown. |
| + |
| +For a release, the root collector may first return the distinct |
| +`writers-stopped` observation under §6.1. It validates individual |
| +replicator descriptors and the drained application and timer work, then |
| +allows the fenced controller to sync the database and flush files and |
| +wake state. That intermediate result is not a stop receipt. The agent |
| +then closes or terminates and joins every producer before the full |
| +checks below. `Collect` retains its unrestricted full-stop meaning. |
| + |
| +After producer shutdown, the agent returns a drain acknowledgement bound |
| +to the collector’s fence and controller tuple. `FenceAndStop`’s |
| +process-local object is not serialized as evidence. |
| Root independently verifies: |
| @@ -2041,7 +2339,7 @@ Rejected alternatives: |
| Use `control/host-actors.json` as the sole enrollment and placement authority. The box’s effective placement region, pools, namespace and regional bucket must agree with its enrollment and the existing provisioning predicates. A disagreement with local configuration refuses claim work. A region code, fleet label or heartbeat never identifies an executor by itself. |
| -Legacy adoption uses P5-D2’s complete census and exactly one proven installation owner. Preserve its refusals for multi-serving records, nonempty `Record.Replicas`, unexplained foreign routes and route-only installations without a representable holder. This proposal does not decide #232’s backfill-versus-lazy-adoption question. |
| +Legacy adoption uses P5-D2’s complete census and exactly one proven installation owner. Preserve its refusals for multi-serving records, nonempty `Record.Replicas`, unexplained foreign routes and route-only installations without a representable holder. Adoption follows #232’s backfill-only ruling in §1.1 P4. |
| Extend the existing per-box inventory with typed entries for: |
| @@ -2071,6 +2369,12 @@ A crash resumes the journal. A successor at the same path or row key is never re |
| Completed inventory snapshots remain in the retirement journal. Retired-stamp fencing records remain operational metadata; retirement must not remove the records that prevent stale work from returning. |
| +C4 permits retaining a row between direct claim checks for at most ten |
| +minutes, with prompt reads on executor-change notification. It grants |
| +no execution or materialization authority. Relocation participant rows |
| +follow §4; former executors remain held until the exact inventory-bound |
| +retirement above archives and removes their rows. |
| + |
| Local-record loss triggers reconstruction from the claim, complete local census and retirement journals. Claim-based initialization does not establish that existing artifacts belong to the current installation. Ambiguous ownership blocks initialization and materialization. |
| An untouched box may acknowledge only with P5-D3’s complete `empty` receipt. Missing inventory is never equivalent to an explicitly proven empty inventory. |
| @@ -2086,7 +2390,7 @@ Rejected alternatives: |
| *Extend §6.1, §6.2a and §6.4a. The corresponding provider contract belongs in moves §5.1, §7.6–§7.8 and §9.1–§9.2.* |
| -Moves supplies one typed provider for held inputs, prepared-generation authority, publication and live-object selection. Plan 6 consumes that provider; it does not interpret arbitrary journal strings or introduce another held-input format. |
| +Moves and relocation share one typed provider for held inputs, prepared-generation authority, publication and live-object selection. Plan 6 consumes that provider; it does not interpret arbitrary journal strings or introduce another held-input format. |
| Each result is bound to the observed claim ETag, holder incarnation, installation stamp, writer session, operation ID, phase, executor and relevant region. |
| @@ -2096,17 +2400,73 @@ For forward probes, these identities must match `move.inputs`. For source recove |
| `RenderHeld` writes a move-bound acknowledgement even when the rendered bytes are unchanged. `MaterializeHeld` stages and selects the exact authorized release. Both use the captured hostguard selection. Immediately before app execution, validate the actual executable and composed launch environment against the same identities. Ordinary config and adoption passes continue to skip held rows. |
| -Prepared restore authority includes the owning operation/phase, completed install manifest identity, pinned snapshot and anchor versions, required TXID, and the claim evidence that the generation has not previously been opened. Only the admitting CAS consumes that opening. A restarted probe receives a fresh cold generation. A path or `build-intent.json` alone grants no prepared restore authority. |
| - |
| -Restoration follows moves §5.1, including verified file trailers, contiguous replay with its overlap rule, required final position and SQLite integrity verification. Plan 7b selection alone proves none of those checks. |
| - |
| -Position zero follows the existing empty-bootstrap contract: no `[1,0]` snapshot or `[0,0]` anchor. Nonempty prepared generations require acknowledged snapshot and anchor writes and a completed install manifest before opening. Ordinary cold generations follow the existing first-upload publication sequence. |
| +Moves and relocation use one prepared-generation provider. Its source is |
| +either a validated move staging seal or a journalled same-region recovery |
| +pin. Both bind exact source versions, incarnation, operation, phase and |
| +destination region. |
| + |
| +The provider verifies complete restore input, contiguous replay, the |
| +required final position and database integrity. For a nonzero position it |
| +writes deterministic build intent, acknowledged snapshot and level-0 anchor, |
| +then a completed install manifest naming their exact versions. |
| + |
| +Prepared authority requires that completed manifest and evidence that the |
| +generation has not previously been admitted. The first cold admission |
| +consumes the opening. Later admissions use ordinary predecessor selection. |
| + |
| +A zero-position database follows empty bootstrap and produces no invalid |
| +snapshot or anchor. In particular, it writes no `[1,0]` snapshot or |
| +`[0,0]` anchor. |
| + |
| +`installed` never rewinds into a remote rebuild. Local installation receipts |
| +remain box- and installation-stamp-specific. |
| + |
| +Publication follows moves’ prepared and ordinary cold-admission rules. |
| +Building alone does not publish `generation.json`; prepared publication |
| +follows admission and precedes replication opening. Ordinary |
| +fresh-generation publication requires its durable root. Only verified |
| +publication permits `PublishGeneration`. |
| + |
| +Prepared restore authority also binds the installation stamp, completed |
| +manifest identity, pinned snapshot and anchor versions, and required |
| +TXID. Only the admitting CAS consumes the opening. A path or |
| +`build-intent.json` alone grants no authority. Restoration retains moves |
| +§5.1's verified file trailers, contiguous replay overlap rule and SQLite |
| +integrity verification; Plan 7b selection alone proves none of them. |
| + |
| +Files selection is independent of database baseline selection. Before |
| +application execution, a cold admission establishes its files manifest from |
| +the newest valid manifest in the admitted predecessor chain, read by exact |
| +version. Missing or malformed data is not an empty-files bootstrap. |
| + |
| +Manifest entries retain validated origin-qualified references to immutable |
| +objects within the authorized incarnation location and region. Copying a |
| +manifest into a new generation does not reinterpret its object references |
| +relative to that generation. |
| + |
| +Manifest references are additive and old manifests remain readable. |
| +Legacy relative references are resolved and validated against their |
| +original manifest location before copying; a copied manifest must retain |
| +that origin. The session-bound publisher follows C3; files and database |
| +baseline selection stay independent. |
| + |
| +Every completed installation establishes a files manifest for its admitted |
| +generation before application execution. A same-region relocation may retain |
| +protected immutable object references within that region. |
| + |
| +A cross-region landing materializes and verifies destination-local objects |
| +from the sealed archive, then publishes a manifest referencing those |
| +destination objects. Source-region or staging cleanup must not invalidate |
| +the installed manifest. |
| + |
| +The cut archive remains part of the move protocol. The files manifest does |
| +not replace its sealed transfer or rollback evidence. |
| The publisher writes `generation.json` using the ETag of the marker being replaced, or create-only when genuinely absent. It validates the completed publication inputs and current admission authority before issuing the write. It returns a publication receipt identifying the acknowledged marker bytes and version. |
| After an ambiguous response, a fresh exact read may establish that those same bytes were published. A conflicting or superseding marker never permits an unconditional retry. Only verified publication permits `PublishGeneration` for the observed operation, phase, session, generation and region. |
| -The sweep view binds to the same fresh claim observation and moves’ authoritative-region table. It includes the installed generation, required pinned versions, protected marker versions and the entire unfinished predecessor run. An absent marker means origin only where the existing origin/unfinished-run rules explain it. |
| +The sweep view binds to the same fresh claim observation and the operation’s authoritative-region table. It includes the installed generation, required pinned versions, protected marker versions, the entire unfinished predecessor run and §6.2a’s independent files live set. Every destructive step, including persisted-manifest replay, revalidates this combined view. `files/<generation>/` is classified under that generation, while referenced objects remain protected independently of its database retirement. An absent marker means origin only where the existing origin/unfinished-run rules explain it. |
| Its generation classifier must classify every discovered or journalled source key, including exact versions already deleted during a retry. Classification uses validated namespace structure and durable manifest identity; it must not depend on successfully reopening a deleted source version. Unknown classifications refuse the affected retirement step. |
| @@ -2172,7 +2532,7 @@ Rejected alternatives: |
| - Using lease expiry as closure: it proves neither producer termination nor completed requests. |
| - Waiting for the retirement horizon to manufacture a certificate: elapsed time is not client-observed success. |
| -**PAUL:** Allow the first completed deployment to operate with cold-only admissions, or wait for certificate-capable replication. Recommended default: allow cold-only operation after the other activation gates pass, accepting restoration and new-generation costs at every admission. |
| +**Ruled (§1.1 P7):** Allow cold-only admissions after the other activation gates pass. Disable warm admission and issue no clean-close certificate until a reviewed Litestream fix or upgrade makes it safe. |
| #### P6-D5. Regional retirement authority and aggregate leases |
| @@ -2199,7 +2559,7 @@ Evidence for particular cases is: |
| - **Failed admission:** the closed admission attempt and joined builder/replicator, or positive durable evidence that no producer was opened. An empty object listing alone is insufficient. |
| - **Superseded generation while serving:** evidence for its former writer and builders, plus the existing publication/coverage authority. The successor’s running process need not be stopped. |
| - **Free-host residue:** retained retirement evidence covering the old producers, or fresh complete discovery evidence. A free claim alone proves no stop. |
| -- **Lost box:** the accepted loss record’s persisted `fenced_at`, following §7.3 D5. |
| +- **Lost box:** the accepted loss record’s persisted `fenced_at`, or the automatic fence’s persisted original observation time, following §7.3 D5. |
| The worker retains the original evidence, scope and retirement ID across retries. Later residue gets the further retirement event required by §6.2a. Claim or enrollment changes require reauthorization; they never silently rebind the old scope. |
| @@ -2310,12 +2670,21 @@ A probe uses the moves operation’s own attempt journal. One probe attempt is o |
| Add moves §5.2’s `hold_op` column, with empty default. Carry route incarnation/stamp ownership as required by P6-D2. Writing or clearing a hold is a guarded registry transaction conditional on that ownership and the expected operation. |
| -For normal release, the owning moves transition supplies release authority. For stale-hold recovery, require a fresh serving claim naming this box as executor and a matching local installation. Clear only the observed stale `hold_op`; never clear whatever operation happens to be present at execution time. |
| +For normal release, the owning moves or relocation transition supplies release authority. For stale-hold recovery, require a fresh serving claim naming this box as executor and a matching local installation. Clear only the observed stale `hold_op`; never clear whatever operation happens to be present at execution time. |
| Clearing a stale hold must preserve a failed-host denial. A `ready` projection does not override `wake_retry`, quarantine or admission authority. |
| Timer delivery and ordinary timer convergence refuse held rows without advancing bookkeeping. Moves retains its exact timer replacement and snapshot rules. Every timer mutation, including pruning and post-delivery bookkeeping, uses the original captured selection and matching registration identity. |
| +`relocating` holds use the existing timer rules: freeze ordinary convergence |
| +and delivery, drain in-flight delivery before the release snapshot, and |
| +restore exact registration and bookkeeping identities through |
| +`ReplaceTimers`. |
| + |
| +Once an installation has admitted a writer, recovery must not replay its |
| +original timer or files installation. Subsequent recovery follows the |
| +admitted lineage. |
| + |
| Rejected alternatives: |
| - Keeping failure counts only in activator memory: restarting the agent grants unlimited attempts. |
| @@ -2323,26 +2692,6 @@ Rejected alternatives: |
| - Clearing failure on a heartbeat or cached response: neither proves this admitted process is healthy. |
| - Re-admitting a session for each restart under a live replicator: it violates the session boundary. |
| ---- |
| - |
| -**FIRST PROMPT:** |
| -“Read /home/paulca/.cache/tmp/claude-1001/own/spec-p6-brief.md and do exactly what it says.” |
| - |
| -**WHAT:** |
| -Propose contracts closing Plan 6’s eight box-side gaps. |
| - |
| -**STATUS:** |
| -Complete draft above. Source inspected; #234 unavailable; no Opus review obtained. No files written. |
| - |
| -**NEEDED:** |
| -Decide whether initial activation may use cold-only admissions. |
| - |
| -**RECOMMENDED:** |
| -Read #234 and obtain joint authority review before incorporating or implementing these proposals. |
| - |
| -**SESSION:** |
| -Safe to close this read-only task. A concurrent Plan 6 file change was observed and left untouched. |
| - |
| ## 7. Lost boxes and execution fencing (J-D6, J-N3) |
| A claim CAS is bookkeeping, not fencing. A box can be partitioned from |
| @@ -2360,8 +2709,9 @@ While a host is under any operation, each participant box must hold an |
| the host's process tree using the cleanup-only operation (§6.1) and |
| refuses admission until it can read the claim again. |
| - **A fresh read that shows no operation, or shows this box is not a |
| - participant, ends the self-fence (CC9).** The box deletes its local |
| - execution-lease state. A stale local file must never keep a box fenced. |
| + participant, permits ending the self-fence (CC9).** Required cleanup |
| + must finish before the controller record is removed (§7.3 D6, D7). |
| + Completed stale state must not keep a box fenced. |
| - The lease is for **liveness only**. A whole-VM pause also stops the |
| watchdog, and on resume the app can write before the watchdog fires. |
| The lease is therefore never proof that a box has stopped (CC5). |
| @@ -2371,6 +2721,13 @@ While a host is under any operation, each participant box must hold an |
| ### 7.2 Declaring a box lost |
| +A valid automatic termination fence under §7.3 D2 revokes execution |
| +without operator action or a disk condition. Host-specific consequences |
| +are persisted in the claim under D3 and D4’s automatic-loss contract |
| +before effects; the console materializes D4 records later. Local |
| +discharge still needs D5’s separate evidence. Other cases use the |
| +operator path: |
| + |
| carlos ops host resolve <host> --declare-lost <box> |
| The move form, `carlos move resolve --declare-lost`, delegates to this |
| @@ -2378,8 +2735,8 @@ command and keeps the move spec's restrictions: before commit only, the |
| exact participant, the source refused, and loss confirmed explicitly. |
| The command **requires compute fencing, and nothing else (CC5)**. The |
| -operator supplies the box's instance id, and the CLI verifies through the |
| -cloud API, with the operator's own credentials, that the instance is |
| +CLI resolves the box's instance id from its enrolled identity and verifies |
| +through the cloud API, with the operator's own credentials, that the instance is |
| `stopped` or `terminated`. The console never holds EC2 rights. Lease |
| expiry alone is never accepted. |
| @@ -2392,13 +2749,15 @@ Two states it must also cover: |
| after a commit. Declaring it lost removes those chores, because its |
| local disk is gone with it. |
| -Only then does it remove the box's obligations and execution authority. |
| -It adds the box to `lost`, a quarantine list that survives the |
| -operation's release. A box on `lost` is refused admission for any host |
| -until its old state has been retired and an operator removes it with |
| -`--readmit`. **The returning box retires its own state (CC12).** On |
| -start, before anything else, it checks the claims of every host in its |
| -local inventory. For each host where it is on `lost`, it runs local |
| +Only then does the owning transition revoke the box's execution authority |
| +and discharge the exact local chores supported by D5's evidence. Remote |
| +chores remain owed. It adds the box to `lost`, which survives operation |
| +release. Operator-quarantined boxes remain denied until old state has |
| +been retired and an operator readmits them under D3. Automatically |
| +terminated enrollments are permanently ineligible and cannot be readmitted. |
| +**The returning box retires its own state (CC12).** On the |
| +operator-quarantined path, before startup work, it checks the claims of |
| +every host in its local inventory. For each host where it is on `lost`, it runs local |
| retirement (§6.3) under the host guard. Only then can it be readmitted. |
| **Cost.** This adds one renewal write per participant per 20 seconds, |
| @@ -2408,11 +2767,11 @@ traffic. |
| ### 7.3 Contracts for leases, lost boxes and the floor (rev 6.17, RULED, as amended by §1.1) |
| -**Status: ruled 2026-10-06, as amended by §1.1 (originally proposed).** These contracts close the gaps Plan 8's draft found (D2 to D6). They are under joint review and wait on Paul's rulings P1 to P3 in §10.1; nothing in production relies on them until then. Missing safety evidence always means unsupported or unknown, never success; all new JSON fields are additive. |
| +**Status: ruled 2026-10-06, as amended by §1.1.** These contracts close the gaps Plan 8's draft found (D2 to D6). Paul's rulings P1 to P3 apply; rev 6.28's HA amendments await joint round 18. Missing safety evidence always means unsupported or unknown, never success; all new JSON fields are additive. |
| #### D2. Fencing evidence binding and transport |
| -**Authority and identity.** Declare-lost and readmit require a person session and a successful `Store.IsOperator` check on every request. Service credentials, tenant ownership, ops-account ownership and `apiSystemRoller` membership do not independently grant this authority. Authorization errors refuse the request. |
| +**Authority and identity.** Operator-attested declare-lost and readmit require a person session and a successful `Store.IsOperator` check on every request. Service credentials, tenant ownership, ops-account ownership and `apiSystemRoller` membership do not independently grant this authority. Authorization errors refuse the request. |
| The shared actor directory defined in D7 binds each box reference to: |
| @@ -2428,13 +2787,43 @@ cloud: {provider, account, region, instance_id} |
| `enrollment` is an immutable random identifier for that machine enrollment. Cloud account, region and instance ID are enrolled facts, not values selected by the resolve request. Missing or ambiguous binding refuses declare-lost. |
| -Platform box references use #212’s collision-resistant ID. Empty IDs and the twin latch refuse claim work. Machine-ID uniqueness remains a deployment prerequisite. |
| +Platform box references use #212 option B’s label key, as ruled in §1.1 P3. Empty references and the twin latch refuse claim work. Machine-ID uniqueness remains a deployment prerequisite. Enrollment requires verified `internal/boxid` evidence and records its cloud identity. For a reference already present in claims or edges files, the verified instance ID must match the configured tofu `instance_id`. `control/host-actors.json` remains the sole membership authority; any retained `control/boxes/` evidence grants no separate membership authority. |
| A fleet label is unique only within its fleet and active enrollment. In deployment-wide claims, its reference is `fleet-<enrollment>`, where `enrollment` is 32 lowercase hexadecimal characters. The directory binds that reference to the fleet and its label. Existing fleet heartbeat keys remain unchanged. This is the necessary qualification of #212’s fleet-label exception for shared claim objects. |
| Labels are accepted at the CLI only when they resolve to exactly one enrolled reference. Every claim field, lease key and loss record uses the resolved reference. |
| -**Request binding.** Inspection returns a console-signed challenge containing: |
| +**Automatic termination (L2, L4).** An eligible regional worker may |
| +supply a lost-box fence without a person session when the exact roster |
| +`cloud` identity has a verified positive `terminated` observation from |
| +EventBridge or `DescribeInstances` (later, Auto Scaling activity history). |
| +Execution fencing requires no disk condition. `shutting-down`, lease |
| +expiry, API absence, an unverified identity and nonterminal observations |
| +are never automatic evidence. Stopped, unclear and missing instances |
| +retain the operator path below. The console receives no EC2 rights. |
| + |
| +Automatic termination evidence is an immutable, create-only record at |
| +`control/box-fences/<enrollment>.json`. It binds the box reference, |
| +enrollment, roster cloud identity, terminal observation, original |
| +observation time, evidence source and authenticated reporting worker. |
| +Consumers verify its key, digest, identity and authority. The record is a |
| +trusted worker report, not an AWS-signed attestation. |
| + |
| +**The fence's journal reference (moves C7).** Every claim transition that |
| +relies on a termination fence writes one readable reference to it in the |
| +operation's journal, under the key `fence.<box>`: a JSON string |
| +`{"enrollment", "key", "sha256"}` naming the box-fences record and the |
| +digest of the exact bytes verified. A `loss.<id>` entry written by the |
| +same transition cites the same reference in its intent. Consumers (a |
| +move's return, a relocation's recovery) accept the fence only through |
| +that reference, re-verifying the record against it; the key is never |
| +reused for another box or enrollment within the operation. |
| + |
| +New retirement scopes use the fence’s persisted original observation time. |
| +Existing scopes retain their earlier evidence bounds. Neither console |
| +processing nor retry time becomes new fencing evidence. |
| + |
| +**Operator request binding.** Inspection returns a console-signed challenge containing: |
| ```text |
| id, actor, issued_at, expires_at |
| @@ -2495,7 +2884,7 @@ loss_ids: declaration IDs |
| The directory is console-authored, root-signed and replaced with `If-Match`. Box processes may read it but may not author its authority. |
| -Before revoking claim authority, the console conditionally sets the exact enrolled box to `quarantined`, increments its quarantine revision and records the declaration ID. A partial declaration leaves this deny in force. It never automatically restores eligibility because a later claim write failed. |
| +On the operator-attested path, before revoking claim authority, the console conditionally sets the exact enrolled box to `quarantined`, increments its quarantine revision and records the declaration ID. A partial declaration leaves this deny in force. It never automatically restores eligibility because a later claim write failed. |
| Every new host admission and guarded host-state write reads and verifies this exact object alongside the claim. It refuses a missing enrollment, identity mismatch, quarantine, retirement or unreadable directory. This is an exact-object read, not a claim listing or a console-cache lookup. |
| @@ -2510,6 +2899,22 @@ loss_refs: declaration IDs |
| Loss references survive `free`, operation replacement and successor holders. Removing one claim’s `lost` entry never clears the global deny. |
| +Each affected claim transition independently binds the current holder, |
| +operation, phase and exact consequences. It retains the fence reference, |
| +adds the terminated box to `lost`, and durably records the host-specific |
| +recovery consequences and pending loss reporting before effects run. These |
| +references survive operation replacement, `free` and holder replacement. |
| + |
| +Automatic termination does not require a quarantine revision or operator |
| +attestation. The terminated enrollment is permanently ineligible and cannot |
| +be readmitted or rebound to another machine. |
| + |
| +Automatic claims retain enrollment-qualified fence references in |
| +`evidence_refs` and stable loss identities in `loss_refs`; they do not |
| +invent a `lost_revisions` quarantine revision. Every eligibility and |
| +admission check consumes this fence authority directly, including while |
| +the roster still says `active`. Unreadable authority refuses admission. |
| + |
| **Returning-machine startup.** Before starting the edge’s tenant work, root/background passes, timers or replicators, the returning machine verifies its enrollment and global quarantine state. Unreadable authority means no startup admission. |
| While quarantined, startup closes all host admission, drains existing work and constructs the union of: |
| @@ -2545,7 +2950,7 @@ entries: |
| The current private box report names the completion object’s digest. The console requires a fresh report under D7, matching enrollment, instance ID, boot ID and quarantine revision, and matching completion bytes. The receipt is durable retirement evidence; the fresh report establishes that this returning machine still reports that completed state. It is not hardware attestation and retains the existing trusted-box-writer model. |
| -**Readmission ordering.** Readmit binds to one enrollment and quarantine revision. The console: |
| +**Readmission ordering.** This path applies only to operator-quarantined enrollments not permanently fenced as terminated. Readmit binds to one enrollment and quarantine revision. The console: |
| 1. Confirms every accepted loss declaration and affected host has completed retirement or the explicitly accepted destroyed-local disposition. |
| 2. Removes per-host quarantine entries only where `lost_revisions[box]` equals the revision being cleared. |
| @@ -2554,7 +2959,7 @@ The current private box report names the completion object’s digest. The conso |
| An interrupted readmission leaves the global deny active. A concurrent declaration increments the revision and defeats the older final write. An older readmission cannot remove a newer per-host quarantine entry. |
| -**Successive declarations (rev 6.20).** A box may be declared lost more than once for the same host (for example, a stopped instance first, then confirmed disk destruction). Each declaration is freshly bound and carries a strictly newer quarantine revision; it may apply only its own confirmed consequences. An older revision is refused, and a readmission bound to an older revision cannot clear a newer one. |
| +**Successive operator declarations (rev 6.20).** A box may be declared lost more than once for the same host (for example, a stopped instance first, then confirmed disk destruction). Each operator-attested declaration is freshly bound and carries a strictly newer quarantine revision; it may apply only its own confirmed consequences. An older revision is refused, and a readmission bound to an older revision cannot clear a newer one. |
| Readmission grants no executor, installation stamp or writer session. Any subsequent writer uses fresh claim authority, a new admission and certified-remote restoration. A retired installation stamp cannot be reactivated through readmission. |
| @@ -2586,10 +2991,30 @@ result_claim_gen |
| `state` is `prepared`, `committed` or `conflicted`. The accepted evidence and confirmed consequences become immutable when prepared. Delivery bookkeeping does not alter them. |
| -The record is durable before claim authority changes. The successful claim CAS adds its ID to `loss_refs`. A retry determines success from that claim reference, even if the HTTP response or the later `committed` update was lost. A declaration against a different operation is stale, not a new invocation of the old intent. |
| +On the operator-attested path, the record is durable before claim authority changes. The successful claim CAS adds its ID to `loss_refs`. A retry determines success from that claim reference, even if the HTTP response or the later `committed` update was lost. A declaration against a different operation is stale, not a new invocation of the old intent. |
| The record and its claim references survive operation release, `free`, holder replacement and readmission. |
| +**Automatic loss persistence (L4).** The immutable D2 enrollment fence |
| +precedes each affected claim transition. The transition durably retains |
| +its exact host-specific consequences, fence reference, loss identity, |
| +timer knowledge, write declarations and pending reporting before any |
| +effects run. These retained values survive operation replacement, |
| +`free` and holder replacement; no console-authored record or quarantine |
| +revision is required before automatic recovery. |
| + |
| +The console later materializes the corresponding D4 host loss records and |
| +retires the roster entry. This work is idempotent. The claim retains loss |
| +identities, timer knowledge and admission declarations until the durable |
| +loss records contain them. A missing timer snapshot records `unknown`; a |
| +usable incomplete snapshot records `partial`. |
| + |
| +The materialized loss record carries the automatic authority variant: |
| +the verified fence reference and original observation time replace |
| +operator attestation and quarantine revision. Its consequences and |
| +alert work come from the retained claim evidence. Retries deduplicate |
| +by the retained loss identity and preserve original evidence bounds. |
| + |
| **Timers.** `timers` contains: |
| ```text |
| @@ -2627,9 +3052,9 @@ baseline reference |
| The recovery admission supplies each `remote_max_txid` from the baseline it actually validated. It must not substitute the current holder’s session for the journalled source cut session, or invent a zero for unreadable remote data. |
| -Retries deduplicate by declaration ID and source session tuple. Before a loss-bearing admission is trimmed or its holder removed, its completed declarations must be copied into the durable loss record with the admission’s claim generation. Failure retains the admission evidence and blocks that removal. |
| +Retries deduplicate by declaration ID and source session tuple. Before a loss-bearing admission is trimmed or its holder removed, its completed declarations must be copied into the durable loss record with the admission’s claim generation. Failure retains the admission evidence and blocks that removal, unless the automatic path preserves the same complete loss evidence independently of the admission or holder until D4 materialization. |
| -**Alerts.** Prepared accepted losses create durable pending alert work. Committed records drive timer-loss and write-loss alerts, including unknown timer inventory. Delivery retries per declaration and recipient. Missing recipients, missing delivery configuration or a send failure remain visible and pending; they do not count as notification. |
| +**Alerts.** Prepared accepted losses and automatic claim-bound consequences create durable pending alert work. Committed records drive timer-loss and write-loss alerts, including unknown timer inventory. Delivery retries per declaration and recipient. Missing recipients, missing delivery configuration or a send failure remain visible and pending; they do not count as notification. |
| A lost response must not cause a second declaration. Notification failure must not undo fencing or permit unrecorded loss. |
| @@ -2640,7 +3065,7 @@ Declare-lost changes only the consequences confirmed under D2 and committed thro |
| The successful claim CAS must: |
| - Bind the exact holder, operation, phase, enrolled box and accepted declaration. |
| -- Add the box to `lost`, record its quarantine revision and retain the durable loss reference. |
| +- Add the box to `lost` and retain the durable loss reference. Record its quarantine revision on the operator path, or its immutable enrollment-fence reference and pending host-specific loss consequences on the automatic path. |
| - Remove only that box’s participation or execution authority as the operation permits. |
| - Preserve writer-session provenance, admissions, inventory, touched history, unrelated obligations and quiet times. |
| - Record the operation’s recovery intent before any recovery effects run. |
| @@ -2653,13 +3078,33 @@ A subsequent execution handover belongs to the operation owner. Its CAS writes t |
| - Remote `park-replica`, `park-generation` and moves staging chores remain owed even when their former executor is lost. |
| - Regional work is reassigned to `region:<r>` while retaining its chore ID, original operation, retirement ID and immutable park scope. A suitable box in that region performs it. No available regional executor means the chore remains pending. |
| -- Only an exact `park-local` chore whose entire covered local storage is proven destroyed may be discharged without retirement. |
| +- Only an exact `park-local` chore with D2’s destroyed-storage attestation or the automatic H19 volume-record evidence below may be discharged without retirement. |
| - A stopped instance retains its local retirement obligation. |
| - `terminated` alone is insufficient for the destroyed-local exception because EBS volumes may survive termination. [AWS volume-preservation behavior](https://docs.aws.amazon.com/AWSEC2/latest/UserGuide/preserving-volumes-on-termination.html) |
| Discharging a chore uses `CompleteObligation` semantics, including discovery completion. It never removes all obligations merely because they name a box. |
| -New remote retirement scopes justified by the compute fence use the declaration’s persisted `fenced_at` and Plan 4’s normal late-completion horizon. Existing scopes retain their original evidence time. Retries do not restart the horizon, and compute fencing does not cancel already accepted object-store requests. |
| +A termination fence is sufficient to revoke execution regardless of volume |
| +evidence. Automatic discharge of an exact `park-local` obligation |
| +additionally requires the H19 volume-record evidence, bound to that |
| +enrollment and covering the storage represented by the obligation. The |
| +discharge records the evidence references and uses `CompleteObligation` |
| +semantics, including discovery completion. |
| + |
| +Missing, unreadable or disqualifying volume evidence leaves the local |
| +obligation open. It does not block recovery onto another eligible box that |
| +does not write the retired installation. It does not waive the obligation’s |
| +effect on `free` or permit reuse of the unresolved installation. |
| + |
| +Remote obligations retain their original identities, scopes and evidence |
| +times and remain owned by `region:<r>`. |
| + |
| +The H19 evidence covers volume records from enrollment through the last |
| +running record: every attached EBS volume has `DeleteOnTermination` and |
| +none has been removed. This is the ruled local-cleanup criterion; it |
| +does not establish destruction of snapshots, backups or detached copies. |
| + |
| +New remote retirement scopes justified by the compute fence use the declaration’s persisted `fenced_at`, or the automatic fence’s persisted original observation time, and Plan 4’s normal late-completion horizon. Existing scopes retain their original evidence time. Retries do not restart the horizon, and compute fencing does not cancel already accepted object-store requests. |
| **Moves.** Preserve all restrictions in moves §7.10: |
| @@ -2671,6 +3116,25 @@ New remote retirement scopes justified by the compute fence use the declaration |
| - Validated durable target data is recovered where available. |
| - The destroyed-local-only exception may discharge exact local chores after commit without reopening data authority. |
| +A valid automatic termination fence may replace operator-supplied |
| +compute-fence evidence for the existing move target-loss transitions. The |
| +move operation owner applies the transition; the regional placer supplies |
| +evidence only. |
| + |
| +Both data-authority paths remain restricted to the exact target and to |
| +before the instance record’s commit CAS. Rollback races commitment through |
| +that record CAS. Source loss remains refused by these move recovery paths. |
| + |
| +The transition preserves recovery of validated durable target data, |
| +retirement of any partial return lane, and all required write and timer loss |
| +declarations. Automatic consequences are durably recorded through the |
| +automatic-loss contract before effects, without waiting for console |
| +materialization. |
| + |
| +After commit, only the existing exact destroyed-local discharge may apply |
| +without a new operation. A termination fence does not convert an active move |
| +into relocation or independently authorize target replacement. |
| + |
| **Local-only declarations against a serving claim (rev 6.20).** An adopted host returns to `serving` with an empty `op.id` while discovery `park-local` chores may remain. A destroyed-local-only declaration is then legal against the serving claim, narrowly: it binds the claim revision and each discharged chore's original operation and retirement identity, discharges only those `park-local` chores, and changes nothing else (the serving executor, `holder.stamp`, sessions and every other obligation are preserved). |
| **Denial is durable before the guard is released (rev 6.20).** After an ambiguous lease renewal the box keeps the host guard until its denial is durable; if persisting the lost state fails, the on-disk state must still deny (it may never fail open to an older `active` record), and cleanup proceeds independently. |
| @@ -2744,9 +3208,17 @@ The first transition out of the operation’s initial phase requires an acknowle |
| The claim CAS that crosses the barrier preserves the acknowledgements. They are historical evidence that participants observed the operation, not permanent lease authority. Subsequent phases continue checking current lease health. A participant added later must acknowledge before its phase permits work. |
| +For relocation, a start bound to a valid source termination fence, or |
| +conversion after source termination in `starting` or `releasing`, removes |
| +only that source from the barrier. The selected target and every other |
| +required surviving participant still acknowledge. D7’s H14 protocol |
| +requires durable `pending` before checking executable-update state and |
| +refuses acknowledgement during an update. A replacement revalidates |
| +its enrollment, actual executable identity and floor before work. |
| + |
| **Restart and clearing.** A new controller first joins or excludes the previous controller and completes required cleanup. It never revives a lost handle. Rejoining the same operation requires fresh claim/quarantine checks and a newly acknowledged lease. |
| -A fresh claim read showing `serving`, `free` or that the box no longer participates clears only the stale execution-lease state, as CC9 requires. It does not clear quarantine, retired stamps, another operation’s fence or failed cleanup. |
| +A fresh claim read showing `serving`, `free` or that the box no longer participates permits clearing stale execution-lease state only after required cleanup has completed, as CC9 and D7 require. Controller records, including `lost`, remain present while cleanup is pending. Clearing does not clear quarantine, retired stamps or another operation’s fence. |
| Release cancels and joins renewal before conditionally deleting the ETag owned by that controller. Unknown ownership or a changed ETag leaves the object alone. Unconditional delete is forbidden. |
| @@ -2760,13 +3232,17 @@ Release cancels and joins renewal before conditionally deleting the ETag owned b |
| | `parking`, none left | console pass | §5.2 step 5 | |
| | `purging` | console pass | §5.3, from the reservation | |
| | `placing` | console pass | §5.4, from `intent` | |
| +| `relocating` | `region:<r>`, any eligible enrolled regional worker under the required leases | §4 phase table and durable journal; only `op.exec` may install or admit where permitted | |
| | move kinds | move-any-app | one writer per transition | |
| Claims are listed only by the recovery pass, never on a hot path. |
| **A stale hold (CC10).** Reconcile releases a held row whose `hold_op` is |
| -not the claim's current operation, on the box the claim names as executor |
| -of a `serving` host. |
| +not the claim's current operation, on the box a fresh claim names as |
| +executor of a `serving` host, with a matching installation and expected |
| +`hold_op` (P6-D8). C4's ten-minute row-retention exception grants no |
| +hold-clearing or execution authority. Former relocation executors stay |
| +held until P6-D2's exact inventory-bound retirement removes their rows. |
| ## 9. Legacy hosts (R2, J-N5) |
| @@ -2833,11 +3309,11 @@ because the instance is new. |
| ### 10.1 Release identity, the census and actor membership (rev 6.17, RULED, as amended by §1.1) |
| -**Status: ruled 2026-10-06, as amended by §1.1 (originally proposed).** D1 and D7 extend the floor from a protocol number to authenticated release identities, a persistent pre-exec guard on the system update path, and a root-signed actor directory with lifecycle and executable-activation reservations. They change the platform's update and membership machinery beyond the claim, so they wait on Paul: |
| +**Status: ruled 2026-10-06, as amended by §1.1.** D1 and D7 extend the floor from a protocol number to authenticated release identities, a persistent pre-exec guard on the system update path, and a root-signed actor directory with lifecycle and executable-activation reservations. |
| -- **P1 (D1):** which real release becomes the floor (recommended: the first tagged release containing the completed claim and moves integrations, box identity, the census and the guarded boot and recovery paths). |
| -- **P2 (D2):** the operator attestation boundary for declare-lost (recommended: operators attest the maintained compute fence, cold quarantine start and destroyed storage; the console does not independently verify cloud state). |
| -- **P3 (D7):** an explicit, operator-approved roster of boxes and consoles as the membership authority (recommended: enrollment controls eligibility; offline actors stay required until fenced or retired). |
| +- **P1 (D1):** The floor is the first tagged release containing the completed claim and moves integrations, box identity, the census and guarded boot and recovery paths. |
| +- **P2 (D2):** Verified automatic termination and operator-attested fencing are the distinct authority paths in §1.1 and D2. |
| +- **P3 (D7):** `control/host-actors.json` is the sole roster, with `boxid` enrollment and the automatic Auto Scaling exception below. Offline actors remain required until valid fencing or retirement. |
| #### D1. Release identity and offline floor enforcement |
| @@ -2989,7 +3465,37 @@ The initial directory must account for every machine that can serve deployment h |
| Enrollment, namespace expansion and reactivation require the current floor and identity checks before authority is granted. Removal requires explicit retirement or a retained compute-fence/quarantine record. Missing heartbeats and inventory expiry never remove an actor. |
| -**Reports.** Platform boxes continue reporting at #212’s ID-keyed private status path. Fleet boxes retain: |
| +Platform enrollment verifies `internal/boxid` evidence and records its |
| +account, region and instance ID in `cloud`. Existing claim or edges-file |
| +references must also match the configured tofu `instance_id` (§7.3 D2). |
| +No `control/boxes/` object is a second membership authority. |
| + |
| +**Automatic Auto Scaling enrollment (L19).** The console may |
| +automatically enroll an Auto Scaling box when verified `boxid` evidence and an authenticated worker’s fresh membership confirmation |
| +agree on the deployment account, expected AWS region, instance and |
| +roster-configured group. |
| + |
| +The confirmation binds an enrollment attempt and the roster group identity. |
| +It is immutable and consumed only for that attempt. Expired or superseded |
| +evidence requires a new immutable confirmation identity; replay of an old |
| +confirmation grants no enrollment. Each confirmation is create-only and |
| +records distinct enrollment-attempt and confirmation IDs, bound to the |
| +roster-configured group identity. |
| + |
| +A worker from another region may confirm only when every relevant active or |
| +quarantined enrollment in the target region has a positive `terminated` |
| +observation in the same pass. The console revalidates that the confirmation |
| +covers the current required set. Missing, partial or nonterminal |
| +observations refuse automatic enrollment. |
| + |
| +Cross-region confirmation grants no cross-region fencing, relocation, |
| +retirement or data access. Once enrolled, the new box performs local |
| +recovery through the normal regional contracts. |
| + |
| +Every other enrollment remains operator-approved. Floor and |
| +executable-identity requirements apply before authority is granted. |
| + |
| +**Reports.** Platform boxes continue reporting at #212 option B’s label-keyed private status path, bound to the enrolled identity. Fleet boxes retain: |
| ```text |
| fleets/<fleet>/status/boxes/<label>.json |
| @@ -3027,23 +3533,60 @@ moves_protocol, floor_sha256, floor_guard_ready, host_claim_enabled |
| The console reports on startup and every five minutes, using the same freshness policy as boxes. A load-balanced `/health` response is not a census of its backends. |
| -A report is fresh for at most **15 minutes**, matching `3 × status.SnapshotPeriod`, and must not be more than **5 seconds** in the reader’s future. Missing fields mean unsupported. An absent, stale, malformed or identity-mismatched report makes the required census fail. |
| +A report is fresh for at most **15 minutes**, matching `3 × status.SnapshotPeriod`, and must not be more than **5 seconds** in the reader’s future. Missing fields mean unsupported. An absent, stale, malformed or identity-mismatched report makes the required census fail, except for the narrowly scoped stale-report exception below. |
| + |
| +For a box-started relocation only, the census may accept a required |
| +console’s newest report beyond the normal freshness interval when the report |
| +passes every other current floor and identity check and its exact enrolled |
| +compute box has reported the D1 root guard armed for the same floor digest. |
| + |
| +The compute binding must cover the actual console executable and every |
| +replacement/bootstrap path. Guard readiness for an unrelated process or |
| +enrollment is insufficient. |
| -**Required actors.** For a protected start, the console checks: |
| +The report must be the newest report for that console enrollment, not a |
| +selected older passing report. A newer incompatible, malformed or |
| +identity-mismatched report refuses the exception. Future-time checks remain |
| +unchanged. |
| + |
| +Missing compute binding, missing guard evidence or a changed floor requires |
| +the ordinary fresh-report path. No other operation or actor receives this |
| +freshness exception. |
| + |
| +**Required actors.** For a protected start, the console, or the eligible regional worker starting relocation, checks: |
| - Every active box that could serve the host under its fleet, pool and placement rules. |
| - Every explicitly required participant, even if outside that candidate set. |
| -- Both source and target regions for a move. |
| +- Both source and target regions for a move, including its exact |
| + source and once-selected target box/enrollment. |
| - Every console able to mutate the relevant host namespace. |
| -- Its own running process directly, in addition to the published console reports. |
| +- Its own running process directly, in addition to the required published reports. |
| -Unknown placement scope refuses the start rather than narrowing the set. Offline enrolled actors remain required. An actor may be excluded as fenced only through its durable quarantine/retirement authority and maintained compute fence, never because it stopped reporting. |
| +Unknown placement scope refuses the start rather than narrowing the set. Offline enrolled actors remain required. An actor may be excluded as fenced only through its durable quarantine/retirement authority and maintained compute fence, or the valid enrollment-qualified termination fence below, never because it stopped reporting. |
| Every required actor must meet the protocol minimum, authenticated release minimum, root enforcement readiness and matching floor digest. Protected starts also require the lifecycle flag to be enabled in the participating processes. |
| These checks govern lifecycle starts, not continued ordinary serving traffic. |
| -**Serializing starts and executable changes.** Separate object reads cannot atomically exclude a concurrent downgrade. The directory therefore records reservations. |
| +A valid termination fence for an exact enrollment excludes that enrollment |
| +from required-actor census and from new execution or participant eligibility |
| +before the console updates the roster. Consumers read the |
| +enrollment-qualified fence authority directly. Missing reports alone never |
| +justify exclusion. |
| + |
| +A console enrollment may contain `compute:{box,enrollment}`. Enrollment and |
| +report validation must establish that the reported console process runs on |
| +that exact enrolled machine. Its trusted box report binds the console report |
| +to the machine and boot. |
| + |
| +A valid fence for that compute enrollment excludes the bound console |
| +instance. An absent, ambiguous or mismatched compute binding grants no |
| +exclusion. Other console instances remain required. |
| + |
| +Failure to read or validate fence authority refuses a protected start; it is |
| +not evidence that the actor is fenced. |
| + |
| +**Serializing starts and executable changes.** Separate object reads cannot atomically exclude a concurrent downgrade. The directory therefore records reservations for console-started operations; box-started relocation uses the H14 protocol below. |
| A lifecycle reservation contains: |
| @@ -3058,6 +3601,32 @@ The console creates it with a directory CAS after the complete census. That CAS |
| Reservations persist while the operation is held. A timeout does not release them. An ambiguous failed start is reconciled against the exact claim: if cancellation is needed, its expected claim revision must first be invalidated by a conditional claim write so a delayed start cannot subsequently succeed. |
| +**Box-started relocation (L6).** A box-started relocation uses the H14 |
| +participant/update protocol instead of a console-authored lifecycle |
| +reservation. Other operation starts retain |
| +their specified reservation requirements. |
| + |
| +Before the start CAS, the worker verifies the roster and refuses an |
| +executable activation reservation covering either source or target |
| +enrollment. |
| + |
| +Before acknowledging participation, a controller durably writes `pending`, |
| +then checks root’s update journal and update-begun marker. An active update |
| +prevents acknowledgement. Clearing an unacknowledged pending record requires |
| +proof that it granted no work and has no cleanup outstanding. |
| + |
| +Before beginning any executable change, root durably writes its update-begun |
| +marker, then completely scans controller state. Any controller record, |
| +including `lost`, an unreadable record or an incomplete scan refuses the |
| +update. All executable replacement and recovery paths use this boundary. |
| + |
| +Controller state remains present until D6’s fresh-claim clearing condition |
| +holds and its required cleanup has completed. Neither loss of the lease nor |
| +removal from the participant list alone proves cleanup complete. |
| + |
| +A participant that acknowledges after an update finishes revalidates its |
| +actual running identity and floor before acknowledgement. |
| + |
| An executable activation reservation names the affected enrollments, authorized current/target/recovery hashes and floor digest. It excludes overlapping lifecycle reservations and blocks new ones for those actors until the executable transaction finishes. The console creates it through the existing authorized system-update workflow; it is not an agent-written permission. |
| For rev 6.17, the complete update transaction, including automatic rollback, holds this reservation. This prevents an operation from starting against the candidate and then being downgraded by its prepared recovery path. |
| @@ -3066,7 +3635,7 @@ Root verifies and durably retains the signed reservation before beginning the tr |
| Private console/bootstrap replacement workflows must use the same reservation and floor boundary before the deployment is enabled. |
| -The floor, actor identities and reservation are revalidated at the operation’s start boundary. A failed gate writes no lifecycle intent or effects. If reservation creation succeeded but later work failed, reconciliation releases only that reservation through the rules above. |
| +The floor, actor identities and applicable reservation or relocation participant/update authority are revalidated at the operation’s start boundary. A failed gate writes no lifecycle intent or effects. If reservation creation succeeded but later work failed, reconciliation releases only that reservation through the rules above. |
| Before activation, legacy delete behavior remains only where §10 explicitly permits it. A caller must never begin a claim-based delete and then fall through to legacy cleanup. |
| @@ -3092,10 +3661,36 @@ paragraph: |
| It runs 30k+ seeds, with mutation checks that drop each guard and confirm |
| the model catches it. |
| +Joint round 18 must extend `internal/sim/hostlife` to **two boxes per |
| +region** (L18). The existing one-box-per-region model and clean joint |
| +rounds do not prove these amendments. Required cases include create |
| +spread, relocation by drain, termination during serving and every |
| +relocation phase, nested failover, stale edges files, unenrolled |
| +references, a volume without `DeleteOnTermination`, crashes during |
| +installation, late files uploads and late PUTs after termination. |
| + |
| +The additional witnesses are: |
| + |
| +- Relocation start racing purge or app-placement admission closure. |
| +- Empty-database drain with files and timers. |
| +- Generation parking while relocation pins referenced files. |
| +- Move landing, source cleanup, then target failure with an unchanged file. |
| +- Automatic target loss racing the record commit CAS. |
| +- A failed cleanup leaving a controller record that blocks executable updates. |
| +- First `released` admission followed by an uncertified failed probe. |
| +- Crash between prepared admission, marker publication and replication opening. |
| + |
| +The adverse-volume case must prove both that execution recovery proceeds |
| +and that local chores remain open. Add targeted tests against the real |
| +`hostclaim`, `park`, `stopevidence`, `hostfiles` and `hostexec` boundaries; |
| +model results do not replace those adapter tests. These are required |
| +evidence for joint round 18, not results established by this revision. |
| + |
| ## 12. Finding map |
| | Finding | Section | |
| |---|---| |
| +| Region HA L1-L20 | §1.1; §2; C3/C4; §4; §5.1; §5.9 P5-D1/P5-D2/P5-D3/P5-D6; §6.1; §6.2a; §6.4a; §6.6 P6-D1/P6-D2/P6-D3/P6-D8; §7.2; §7.3 D2-D6; §8; §10.1 D7; §11 | |
| | J-D1 | §2 `op.exec` and `op.participants`, C4, §4 | |
| | J-D2 | §2 `gen` | |
| | J-D3 | §6.1 | |
diff --git a/docs/superpowers/specs/CODEX-ANALYSIS-REGION-HA-L1-L20.md b/docs/superpowers/specs/CODEX-ANALYSIS-REGION-HA-L1-L20.md| new file mode 100644 |
| index 000000000..7ba058e27 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-ANALYSIS-REGION-HA-L1-L20.md |
| @@ -0,0 +1,439 @@ |
| +The HA direction is compatible with the claim’s ruled design, but several requests need tighter contracts before implementation. The largest gaps are relocation’s app-admission ordering, the empty-database case for `released`, durable loss accounting while the console is unavailable, and file-object retention across generations. |
| + |
| +I reviewed these local snapshots: |
| + |
| +| Source | Revision or tip | |
| +|---|---| |
| +| [Claim spec]( /home/paulca/amadan.net/carlos/platform/.claude/worktrees/replica-ownership/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md) | Rev 6.27, `989ee349` | |
| +| `origin/design-region-ha-rev5` | HA rev 5.4, `0c8ad11b` | |
| +| `origin/design-moves-any-region` | Moves rev 7.18, `da2832aa` | |
| +| `origin/main` | `9bed97b5` | |
| +| Plan 5, `feat/hostclaim-console` | `5422d8fc`, unmerged | |
| +| Plan 6, `feat/hostclaim-box` | `2bd3ea1f`, unmerged | |
| +| Plan 8, `feat/hostclaim-leases` | `ca5a79d8`, unmerged | |
| + |
| +“Covered” below means specified, unless explicitly described as implemented. Claim §1.1 overrides the older proposal wording, but explicitly leaves the remaining L1–L20 amendments pending. Several bodies still say “proposed” or “awaiting Paul”; those descriptions need editorial correction. |
| + |
| +**L1. Same-region `relocating`: adopt with changes.** |
| + |
| +There is no conflict with C1–C6 if relocation preserves the holder, uses the existing claim CAS, transfers execution only with evidence, and keeps admission phase-specific. It fills the stateful same-region transfer deliberately excluded from `placing` by P5-D5. It should remain a distinct operation, because moves’ `moving`/`landing` protocol includes cross-region staging, record-controlled commitment and rollback obligations that relocation does not share. |
| + |
| +Much of the machinery is already specified: C2 recovery, R6-4 stamps, prepared generations, cold admission, regional workers and exact retirement. The operation itself is new. |
| + |
| +Four points need changing or making explicit: |
| + |
| +- H14 removes the console’s **roster reservation**, not P5-D1’s **app-admission registration**. P5-D1 currently gives registrations a console-shaped owner. Relocation needs a box-owned form so purge and app placement can drain delayed starts. |
| +- A newly recognized kind must not accidentally permit writers in `installing`, `installed` or `probe-failed`. |
| +- Nested recovery must preserve the latest admitted generation and every abandoned installation’s cleanup. The original source is not the only box that can acquire local state. |
| +- Release to `serving` must explicitly permit retained generation and former-box chores. Applying moves K8’s “every obligation this operation created is gone” would contradict H19 and delay recovery. |
| + |
| +Insert in claim **§4**, with the recovery entry in **§8**: |
| + |
| +> `relocating` changes the executor of a supported single-executor host within its current region. It starts only from `serving`. It preserves the holder incarnation, ownership binding, record region and `holder.location`. It is mutually exclusive with every other host operation. |
| +> |
| +> Its recovery owner is `region:<r>`. Any eligible enrolled worker of that region may replay its journal under the required leases. Regional recovery authority does not grant that worker execution authority: only `op.exec` may install or admit a writer where the phase permits it. |
| +> |
| +> The start CAS records the exact source and target boxes and enrollments, region, reason, source stamp and generation, roster observation, app-admission identity, and any termination-fence reference. Every transition compares the operation ID, expected phase and claim ETag. Replacement history, evidence, pins, installation identities and retry counts remain durable within the same operation. |
| + |
| +Use this admission table: |
| + |
| +| Phase | Execution authority | Permitted work | |
| +|---|---|---| |
| +| `starting` | Source, or `none` for an evidenced failover | Existing source service; new source admission only after its D6 authority is active | |
| +| `releasing` | Source until its full stop evidence | Source admission only before the durable admission fence closes; then release work only | |
| +| `pinning` | `none`, preserving the prior stamp | Select and journal exact recovery versions | |
| +| `installing` | Selected target, with a new installation stamp | Build the prepared generation and materialize inventoried local state; no writer admission | |
| +| `installed` | Selected target | Verify prepared authority and complete that target’s local installation receipt; no writer admission | |
| +| `probing` | Selected target | Cold probe admissions only | |
| +| `probe-failed` | Failed target until full stop evidence or a fence | Release and cleanup only | |
| +| `serving` | Successful target | Ordinary serving under the latest admitted generation and stamp | |
| + |
| +Continue the normative text: |
| + |
| +> A transition revoking execution cites complete stop evidence or a valid lost-box fence and preserves the previous stamp when it installs nothing. A transition granting execution for a new installation writes its resulting claim generation as `holder.stamp`. Every materializing box is added to `touched.boxes` before its first effect. |
| +> |
| +> The prepared generation is opened at most once. The first probe may keep the installation stamp only under §6.4a’s existing `KeepStamp` condition. Later attempts admit fresh generations and restore their actual predecessors. Neither recovery nor final release resets `holder.generation` or `holder.stamp` to the original prepared installation. |
| +> |
| +> Each target supplies a local installation receipt bound to its box, enrollment and the journalled stamp of the CAS that granted that installation execution authority. Later writer stamps do not invalidate that receipt. After the first admission in that installation’s lineage, recovery must not replay the original files, environment or timer installation. |
| +> |
| +> Replacement follows region HA §5.8’s phase-specific table. An unopened completed prepared generation may be reused by a replacement that makes its own local installation. Loss after admission requires nested recovery from the latest admitted lineage. Every abandoned local installation receives an exact `park-local` obligation unless its destruction is separately established. |
| +> |
| +> Source termination during `starting` or `releasing` may convert the existing operation to failover. The conversion records the fence, revokes source execution, preserves the stamp and removes only that source from the acknowledgement barrier. A replacement participant must acknowledge before performing phase work. |
| +> |
| +> The operation permits two target replacements. Exhaustion records `stuck` without resetting the count or inventing stop evidence. Necessary denial and cleanup continue; another handover requires valid evidence and explicit recovery authority. |
| +> |
| +> Successful release requires the selected target’s verified probe and completed admission/publication steps. It preserves all outstanding obligations. Disjoint generation parks and former-box local retirement do not block serving on the new executor. Whole-location retirement, conflicting local retirement and `quiet_after` remain binding. |
| + |
| +Add to **P5-D1**: |
| + |
| +> A regional worker starting `relocating` registers the start under the same app-admission protocol, using an owner tuple `{box, enrollment, controller}` instead of a console owner. Its authority is limited to registrations for eligible hosts in its region. It grants no backend-effect, placement, purge or roster-writing authority. |
| +> |
| +> The registration binds the saved claim observation, existing holder incarnation, app ID and admission epoch. Closed admission or an exclusive app operation refuses the start. The worker revalidates admission immediately before its single start CAS. Purge and placement drain these registrations using the same saved-revision fencing rules as other starts. |
| +> |
| +> Recovery of an accepted relocation proceeds from the claim and does not impersonate an expired registration owner. Missing registration authority makes the start unsupported. |
| + |
| +**Code impact:** Main needs `KindRelocating`, validation and transition helpers in `hostclaim`, plus explicit phase checks in `AdmitWriter` and `PublishGeneration`. Their current kind blacklist would become too permissive if only the constant were added. Plan 5 needs box-owned admission registrations and purge/placement integration. Plan 6 needs relocation policy, installation, probe, release and recovery adapters. Plan 8 needs replacement-participant barriers and termination-aware transitions. Recovery must remain regional. |
| + |
| +**L2. Automatic termination fencing: adopt as written.** |
| + |
| +Already ruled by claim **§1.1 P2**, overriding the operator-only portion of **§7.3 D2**. H19 correctly separates execution fencing from storage cleanup. This satisfies C5; it does not relax C6 or accept lease expiry, `shutting-down`, API absence or an unverified identity. |
| + |
| +The remaining specification work is consolidating the operative ruling into D2 and identifying the evidence transport through L4. Moves’ consequences remain constrained by L14. |
| + |
| +**Code impact:** Main’s `termfence.Verify` already rejects nonterminal and identity-mismatched observations, but binds to `boxid.Identity`, not the roster enrollment. Plan 8’s loss validation still requires operator attestation and a nonzero quarantine revision, so it needs a distinct automatic authority variant. Plans 5 and 6 must consume that variant through their evidence providers. |
| + |
| +**L3. Automatic discharge of local chores: adopt with changes.** |
| + |
| +The execution/storage distinction is already covered by **§1.1 P2** and **§7.3 D5**. Regional ownership already exists in **P5-D3/P6-D5**. |
| + |
| +The phrase “no recovery step waits on them” needs a scope: recovery onto a different box proceeds, but outstanding obligations still block `free`, and an unresolved local chore still makes its own box ineligible. |
| + |
| +Add to **§7.3 D5**: |
| + |
| +> A termination fence is sufficient to revoke execution regardless of volume evidence. Automatic discharge of an exact `park-local` obligation additionally requires the H19 volume-record evidence, bound to that enrollment and covering the storage represented by the obligation. The discharge records the evidence references and uses `CompleteObligation` semantics, including discovery completion. |
| +> |
| +> Missing, unreadable or disqualifying volume evidence leaves the local obligation open. It does not block recovery onto another eligible box that does not write the retired installation. It does not waive the obligation’s effect on `free` or permit reuse of the unresolved installation. |
| +> |
| +> Remote obligations retain their original identities, scopes and evidence times and remain owned by `region:<r>`. |
| + |
| +The volume record is the ruled cleanup criterion. It is not proof that snapshots, backups or every detached copy have ceased to exist. |
| + |
| +**Code impact:** Plan 8’s `dischargeDestroyedLocal` supplies exact-obligation machinery, but needs the automatic evidence variant. Main’s obligation completion can be reused. Plan 5 must retain incomplete retirement status; Plan 6 must schedule remote recovery without waiting for unrelated dead-box local cleanup. |
| + |
| +**L4. Enrollment fence record and later console loss record: adopt with changes.** |
| + |
| +This conflicts with the unamended **D3/D4** ordering: console-authored quarantine and a durable host loss record currently precede authority changes. P2 rules automatic fencing, but does not supply the complete replacement persistence contract. |
| + |
| +A per-enrollment fence proves termination. It does not contain a particular host’s timer knowledge, move-loss consequences or pending alerts. Those must survive before the console returns. |
| + |
| +Add to **§7.3 D2–D4**: |
| + |
| +> Automatic termination evidence is an immutable, create-only record at `control/box-fences/<enrollment>.json`. It binds the box reference, enrollment, roster cloud identity, terminal observation, original observation time, evidence source and authenticated reporting worker. Consumers verify its key, digest, identity and authority. The record is a trusted worker report, not an AWS-signed attestation. |
| +> |
| +> Each affected claim transition independently binds the current holder, operation, phase and exact consequences. It retains the fence reference, adds the terminated box to `lost`, and durably records the host-specific recovery consequences and pending loss reporting before effects run. These references survive operation replacement, `free` and holder replacement. |
| +> |
| +> Automatic termination does not require a quarantine revision or operator attestation. The terminated enrollment is permanently ineligible and cannot be readmitted or rebound to another machine. |
| +> |
| +> The console later materializes the corresponding D4 host loss records and retires the roster entry. This work is idempotent. The claim retains loss identities, timer knowledge and admission declarations until the durable loss records contain them. A missing timer snapshot records `unknown`; a usable incomplete snapshot records `partial`. |
| +> |
| +> New retirement scopes use the fence’s persisted original observation time. Existing scopes retain their earlier evidence bounds. Neither console processing nor retry time becomes new fencing evidence. |
| + |
| +**Code impact:** Main needs retained fence/evidence references. Plan 8 needs an automatic record schema and loss transition path alongside its operator/quarantine path. Plan 5 needs console catch-up and durable reporting. Plan 6 needs fence consumption and preservation of loss-bearing admissions. Synthetic operator attestations would be incorrect. |
| + |
| +**L5. Census exclusion for terminated boxes and consoles: adopt with changes.** |
| + |
| +The direction follows P2 and H14, but **D7** currently excludes actors through quarantine/retirement authority. Console `compute` binding is new. |
| + |
| +Exclusion must also affect executor eligibility. Otherwise a box could leave the required census while its still-`active` roster entry remained selectable. |
| + |
| +Add to **§10.1 D7**: |
| + |
| +> A valid termination fence for an exact enrollment excludes that enrollment from required-actor census and from new execution or participant eligibility before the console updates the roster. Consumers read the enrollment-qualified fence authority directly. Missing reports alone never justify exclusion. |
| +> |
| +> A console enrollment may contain `compute:{box,enrollment}`. Enrollment and report validation must establish that the reported console process runs on that exact enrolled machine. Its trusted box report binds the console report to the machine and boot. |
| +> |
| +> A valid fence for that compute enrollment excludes the bound console instance. An absent, ambiguous or mismatched compute binding grants no exclusion. Other console instances remain required. |
| +> |
| +> Failure to read or validate fence authority refuses a protected start; it is not evidence that the actor is fenced. |
| + |
| +**Code impact:** The production roster/census provider remains outstanding in main and these branches. Plan 8’s `ActorDirectory` is an interface, not this implementation. Plan 5 consumes the revised census; Plan 6 consumes the revised eligibility and admission authority. |
| + |
| +**L6. Box-side exclusion against executable updates: adopt with changes.** |
| + |
| +H14 deliberately replaces **D7’s roster lifecycle reservation** for box-started relocation. The two-sided durable protocol is compatible with **D1/D6**, but “box-started operations” should not silently authorize future operation kinds. Scope this exception to relocation until another kind defines its contract. |
| + |
| +Add to **§10.1 D7**, with a reference from **D6**: |
| + |
| +> A box-started relocation uses the H14 participant/update protocol instead of a console-authored lifecycle reservation. Other operation starts retain their specified reservation requirements. |
| +> |
| +> Before the start CAS, the worker verifies the roster and refuses an executable activation reservation covering either source or target enrollment. |
| +> |
| +> Before acknowledging participation, a controller durably writes `pending`, then checks root’s update journal and update-begun marker. An active update prevents acknowledgement. Clearing an unacknowledged pending record requires proof that it granted no work and has no cleanup outstanding. |
| +> |
| +> Before beginning any executable change, root durably writes its update-begun marker, then completely scans controller state. Any controller record, including `lost`, an unreadable record or an incomplete scan refuses the update. All executable replacement and recovery paths use this boundary. |
| +> |
| +> Controller state remains present until D6’s fresh-claim clearing condition holds and its required cleanup has completed. Neither loss of the lease nor removal from the participant list alone proves cleanup complete. |
| +> |
| +> A participant that acknowledges after an update finishes revalidates its actual running identity and floor before acknowledgement. |
| + |
| +**Code impact:** Plan 8’s `hostexec.Open` writes `pending` but has no update-state check. `ClearStale` does not itself require successful cleanup before removing the record. Both need integration changes. Main’s root update paths need the marker and complete scan. Plan 6 supplies cleanup completion. Plan 5 keeps its ordinary console reservation path. |
| + |
| +**L7. Box enrollment through `boxid`: adopt as written.** |
| + |
| +Already substantially covered by **§1.1 P3**, **P5-D2**, **P6-D2** and opaque references in **§2**. The additional legacy binding to the configured tofu instance ID is a sensible enrollment check. |
| + |
| +The older D2 text about platform references using collision-resistant IDs is superseded by §1.1’s label-key ruling. `control/boxes/` may remain immutable evidence; it must not remain a second membership authority. |
| + |
| +**Code impact:** Reuse main’s `boxid` verifier. The outstanding roster provider must persist verified cloud identity and reject rebinding. Plans 5, 6 and 8 must all consume that same enrollment. No new claim identifier parser is needed. |
| + |
| +**L8. `choose()` recorded once during create: adopt as written.** |
| + |
| +Already ruled in **§1.1 P5-D2**. P5-D2/P5-D6 already require recording the chosen executor and enrollment before effects. Cancellation must still respect P5-D6’s uncertain-effect settlement; a missing acknowledgement is not permission to discard an unresolved effect. |
| + |
| +There is a direct implementation mismatch. |
| + |
| +**Code impact:** Main’s `BeginCreate` does not persist the selected executor. Plan 5’s `Controller.Attempt` writes the record before `Complete` calls `Authority.Executor`, allowing selection during completion and recovery. Move selection before the initial claim CAS, persist it, and make `CompleteCreate` reject substitution. Plan 6 acknowledges that exact selection. Plan 8 supplies its enrollment and barrier checks. |
| + |
| +**L9. Coverage `released`: adopt with changes.** |
| + |
| +This is new. Current **§6.4a item 2** defines only `sealed`, `clean-return` and empty coverage. A stopped database flushed into a verified remote recovery pin can establish predecessor coverage without proving every old request completed. Therefore `released` is compatible with P7’s cold-only ruling. |
| + |
| +It must not become a clean-close certificate, authorize warm admission, set retirement `covered`, or suppress later probe losses. |
| + |
| +There is also an uncovered zero-position case: HA says `N = 0` has no prepared database generation, while L9 permits `released` only when opening one. A clean empty-database drain would still declare a false loss. |
| + |
| +Add to **§6.4a, Admissions, coverage and retirement, item 2**: |
| + |
| +> `released` accounts for the exact predecessor session through a completed live-box release. It is legal only for a cold admission under `relocating`, bound to the current operation and phase. |
| +> |
| +> The predecessor is the last admission entry, using the existing holder fallback only when the list is empty. Its box, session and generation must match the release journal and full stop receipt. The receipt must identify the same incarnation and released installation. |
| +> |
| +> The release records the stopped database’s final TXID and the final files/wake-state manifest sequence. The verified recovery pin must reach those values. For a nonempty database, coverage applies only to the first admission opening the prepared generation built from that pin. |
| +> |
| +> For an evidenced zero-position database, coverage may instead apply to the first cold empty-bootstrap admission bound to that release, after the final files and wake-state pin is verified. No zero-position snapshot or anchor is written. |
| +> |
| +> `released` suppresses only the ordinary loss declaration for that matched predecessor. It does not certify request completion, permit warm admission, set `covered`, or suppress other required declarations. Subsequent admissions must establish their own coverage; they cannot reuse the operation’s earlier release. |
| + |
| +**Code impact:** Main and Plan 8’s `AdmitWriter` reject the new value. Add its constrained validation and preserve the distinction between `Coverage` and `Covered`. Plan 6’s admission-evidence provider must verify the receipt and pin. Plan 5 only needs accurate loss/report handling. Moves’ existing coverage meanings remain unchanged. |
| + |
| +**L10. Writers-stopped intermediate check: adopt with changes.** |
| + |
| +This is a new intermediate state, not a weakening of **§6.1/P6-D1**. Main’s `stopevidence.Collect` intentionally rejects open replicators and every database descriptor holder. |
| + |
| +The exception must identify individual descriptors, not merely allow the agent PID. File and timer mutation must also be drained before their “final” values are captured. |
| + |
| +Add to **§6.1**, implemented through **P6-D1**: |
| + |
| +> Release may collect a distinct `writers-stopped` observation while the host’s replicator remains open. It requires the durable admission fence, settled spawn reservations, drained application and timer work, an empty complete containment tree, and a complete privileged descriptor scan. |
| +> |
| +> The only permitted database, WAL or SHM holders are descriptors positively identified as belonging to this host’s admitted replicator, bound to the agent’s process-start identity, boot, controller and writer session. Other descriptors in the same process are not exempt. An incomplete scan or uncertain identity fails the observation. |
| +> |
| +> This observation permits the fenced release controller to perform the final database sync and files/wake-state flush. It grants no execution handover, retirement acknowledgement, clean-close certificate or writer admission. |
| +> |
| +> The controller then closes or terminates and joins every producer. Full stop evidence still requires the unrestricted §6.1 checks, including no remaining database holders. `Collect` retains that meaning. |
| + |
| +P6-D4’s Litestream shutdown defect still matters. A successful final sync does not prove all maintenance producers stopped. Failed producer shutdown leaves release pending or stuck. |
| + |
| +**Code impact:** Add a separate result/API in main’s `stopevidence`; preserve `Collect`. Plan 6 implements root collection, exact descriptor identity, flush ordering and producer joining. Plans 5 and 8 must continue rejecting this intermediate result wherever full stop evidence is required. |
| + |
| +**L11. Generation parks do not block relocation: adopt with changes.** |
| + |
| +This conflicts with **§4 CC11** as currently written and with main’s `StartGuard`. A narrow exception is justified, but “writes a fresh generation” is insufficient by itself: relocation also reads its database baseline and file objects. |
| + |
| +Add to **§4**: |
| + |
| +> A `relocating` start may coexist with a `park-generation` obligation in its region when the operation writes a fresh generation and the shared live-object view protects every database baseline, files reference and operation pin that relocation may read. |
| +> |
| +> The exception does not authorize writing into or resurrecting a generation already selected for retirement. New pins must be established under the required leases and fresh claim authority before conflicting retirement can proceed. |
| +> |
| +> Whole-location `park-replica` obligations, overlapping staging retirement and local retirement on any box the operation will materialize remain blocking. A dead source’s local obligation does not block a failover that writes only a different target. |
| +> |
| +> This exception applies only to relocation. Other operation starts retain CC11. Existing chores retain their original operation identity and remain executable after the new operation starts. |
| + |
| +**Code impact:** Add a relocation-aware guard or explicit access-scope API; do not weaken generic `StartGuard`. Main’s parker and Plan 6’s provider must support the concurrent live view. Plan 5’s other starts keep current blocking. Plan 8 supplies correct surviving-participant and target identities. |
| + |
| +**L12. Reconcile rows and ten-minute sweep: adopt with changes.** |
| + |
| +Typed route retirement is already covered by **P6-D2**, and stale-hold release by **§8 CC10/P6-D8**. The ten-minute retained-row exception is new and explicitly relaxes C4. |
| + |
| +It should apply only to retaining a projection. It cannot authorize materialization, reopening a hold or executing through an existing cached activator entry. |
| + |
| +Add to **C4**, referenced from **§8/P6-D2**: |
| + |
| +> Reconcile may retain an existing row between direct claim checks, with a maximum ten-minute sweep interval. This exception grants only retention of the row. |
| +> |
| +> Creating a row, changing its ownership or installation, reopening a hold, materializing state, admitting a writer and spawning application code still require fresh authority. Existing activator or registry state is not a substitute. |
| +> |
| +> Relocation participants follow the operation’s phase table. Former executors remain held until exact inventory-bound local retirement archives and removes their rows. Reconcile never deletes such a row by hostname alone. |
| +> |
| +> Executor-change notifications trigger prompt fresh reads for affected rows. Read failure retains existing state, creates no row and grants no additional permission. It does not terminate already-authorized ordinary serving solely because the control read failed. |
| +> |
| +> CC10 clears a stale hold only on the current serving executor with a matching installation and expected `hold_op`. |
| + |
| +**Code impact:** Main’s reconcile/activator integration must enforce that distinction. Plan 6 needs the phase policy, sweep, prompt invalidation and exact row retirement. Plans 5 and 8 supply operation notifications and authority; neither may treat retained rows as census or stop evidence. |
| + |
| +**L13. Files publisher as an ordinary-replication exception: adopt with changes.** |
| + |
| +This is new behavior under **C3**, with substantial consequences for **§6.2a/P6-D3**. |
| + |
| +Two concrete code gaps matter: |
| + |
| +1. Main’s `hostfiles` manifests contain relative `objects/...` references. Copying a manifest into `files/P/` makes restore seek those objects under `P`, rather than their original generation. |
| +2. Main’s `park.protected` promotes pinned objects to whole-generation protection. That is conservative, but cannot retire unused siblings while retaining individual files referenced by newer manifests. |
| + |
| +Add to **C3**: |
| + |
| +> The admitted session’s files publisher is an ordinary-replication exception alongside database replication. It is bound immutably to `{location,generation,session}` and may publish only content objects and the manifest under that session’s authorized files prefix. |
| +> |
| +> Content objects are create-only. Manifest replacement is conditional and ordered by its sequence. File deletion is a manifest tombstone, not a bare-key object deletion. |
| +> |
| +> The publisher participates in fencing, producer shutdown, request deadlines and retirement evidence. A new session creates a new generation-bound publisher. |
| + |
| +Add to **§6.2a/P6-D3**: |
| + |
| +> Files selection is independent of database baseline selection. Before application execution, a cold admission establishes its files manifest from the newest valid manifest in the admitted predecessor chain, read by exact version. Missing or malformed data is not an empty-files bootstrap. |
| +> |
| +> Manifest entries retain validated origin-qualified references to immutable objects within the authorized incarnation location and region. Copying a manifest into a new generation does not reinterpret its object references relative to that generation. |
| +> |
| +> The live-object view includes the manifests from the selected files pin through the current admission, every running operation’s pinned manifest, and every object those manifests reference. Database and files protection are computed independently and combined before retirement. |
| +> |
| +> `files/<generation>/` belongs to that generation for classification. A generation park retires only versions outside the combined live set. Referenced files may outlive retirement of that generation’s database objects. |
| +> |
| +> Every destructive step, including replay of a persisted retirement manifest, revalidates the live view. Unknown classification or conflicting authority refuses mutation. Classification remains possible after an exact source version has already been deleted. |
| +> |
| +> Completion means all currently eligible residue has been retired and the normal horizon verified. Protected file objects remain live; when no live manifest references them, the at-rest sweep owns their retirement. |
| + |
| +**Code impact:** Main needs additive manifest references and compatible readers, session-bound publisher authority, exact-version manifest reads, and separate files reachability in `park.View` and selection. Plan 6 owns integration with admissions, release and the provider. Plan 5’s deletes/purges must use the expanded retirement semantics. Plan 8 must include the publisher in cleanup and loss handling. |
| + |
| +This must preserve old manifest readability. Merely teaching the classifier the `files/` path is insufficient. |
| + |
| +**L14. Terminated move target: adopt with changes.** |
| + |
| +Automatic evidence is already ruled by P2. The move consequences are already tightly specified by **moves §7.10**, **§7.5** and **claim D5**. |
| + |
| +The old mandatory human confirmation cannot remain a prerequisite on the automatic path, but its loss consequences must still be durably recorded. |
| + |
| +Add to **§7.3 D5**, with the corresponding amendment in moves §7.10: |
| + |
| +> A valid automatic termination fence may replace operator-supplied compute-fence evidence for the existing move target-loss transitions. The move operation owner applies the transition; the regional placer supplies evidence only. |
| +> |
| +> Both data-authority paths remain restricted to the exact target and to before the instance record’s commit CAS. Rollback races commitment through that record CAS. Source loss remains refused by these move recovery paths. |
| +> |
| +> The transition preserves recovery of validated durable target data, retirement of any partial return lane, and all required write and timer loss declarations. Automatic consequences are durably recorded through the automatic-loss contract before effects, without waiting for console materialization. |
| +> |
| +> After commit, only the existing exact destroyed-local discharge may apply without a new operation. A termination fence does not convert an active move into relocation or independently authorize target replacement. |
| + |
| +**Code impact:** Plan 8’s `LossOperationOwner.ApplyLostBox` is a suitable integration seam, but needs automatic authority. Plan 5’s loss/recovery coordination and Plan 6’s move adapter must preserve record-before-claim commitment rules. Main’s termination verifier is reusable; no generic takeover helper should decide move recovery. |
| + |
| +**L15. Move target box chosen at start: adopt as written.** |
| + |
| +Moves **§19.2 K1/K2** already binds participants and execution to boxes. What is missing is selection from several eligible target boxes and persistent enrollment binding. |
| + |
| +The requested target region remains the user’s input. `choose()` selects the executor once. Readiness, install, evidence and recovery must use that box and enrollment. |
| + |
| +An “explicit fenced replacement” must have its own legal move transition. L15 does not make relocation’s replacement table applicable to a move. |
| + |
| +**Code impact:** The moves start path and Plan 5’s selection provider must persist the target. Plan 6 must reject readiness and installation from another box in the same region. Plan 8 must check the selected enrollment and any explicitly defined replacement barrier. Main’s singular `op.exec` already supports this shape. |
| + |
| +**L16. Shared prepared-generation builder: adopt with changes.** |
| + |
| +The safety contract is mostly already covered by **P6-D3**, **moves §7.6** and **§7.14**. The missing work is composing it with a same-region recovery pin. |
| + |
| +HA’s shortened probe ordering must not override moves’ prepared-generation publication contract. |
| + |
| +Add to **P6-D3**: |
| + |
| +> Moves and relocation use one prepared-generation provider. Its source is either a validated move staging seal or a journalled same-region recovery pin. Both bind exact source versions, incarnation, operation, phase and destination region. |
| +> |
| +> The provider verifies complete restore input, contiguous replay, the required final position and database integrity. For a nonzero position it writes deterministic build intent, acknowledged snapshot and level-0 anchor, then a completed install manifest naming their exact versions. |
| +> |
| +> Prepared authority requires that completed manifest and evidence that the generation has not previously been admitted. The first cold admission consumes the opening. Later admissions use ordinary predecessor selection. |
| +> |
| +> A zero-position database follows empty bootstrap and produces no invalid snapshot or anchor. |
| +> |
| +> `installed` never rewinds into a remote rebuild. Local installation receipts remain box- and installation-stamp-specific. |
| +> |
| +> Publication follows moves’ prepared and ordinary cold-admission rules. Building alone does not publish `generation.json`; prepared publication follows admission and precedes replication opening. Ordinary fresh-generation publication requires its durable root. Only verified publication permits `PublishGeneration`. |
| + |
| +**Code impact:** Main’s `genselect.Select` and `SelectPrepared` are reusable selectors, not builders or proof of full restore verification. Plan 6’s `Writer.Baseline` currently calls only ordinary `Select`; it needs the prepared path and typed provider. Plan 5 has no builder role. Plan 8 supplies controller and phase authority. |
| + |
| +**L17. Files manifest on every installation; relocation timer holds: adopt with changes.** |
| + |
| +Timer freezing, draining and exact replacement are largely covered by **P6-D8/moves §9.4**. Installation manifests are new. |
| + |
| +Cross-region moves need an explicit boundary: a target manifest cannot retain references into a source region that committed cleanup will park. |
| + |
| +Add to **P6-D3/P6-D8**, with matching changes in moves §6.1, §8 and §9.4: |
| + |
| +> Every completed installation establishes a files manifest for its admitted generation before application execution. A same-region relocation may retain protected immutable object references within that region. |
| +> |
| +> A cross-region landing materializes and verifies destination-local objects from the sealed archive, then publishes a manifest referencing those destination objects. Source-region or staging cleanup must not invalidate the installed manifest. |
| +> |
| +> The cut archive remains part of the move protocol. The files manifest does not replace its sealed transfer or rollback evidence. |
| +> |
| +> `relocating` holds use the existing timer rules: freeze ordinary convergence and delivery, drain in-flight delivery before the release snapshot, and restore exact registration and bookkeeping identities through `ReplaceTimers`. |
| +> |
| +> Once an installation has admitted a writer, recovery must not replay its original timer or files installation. Subsequent recovery follows the admitted lineage. |
| + |
| +**Code impact:** Main’s `hostfiles` and `ReplaceTimers` provide components. Plan 6 needs installation publication, durable wake-state integration and relocation hold checks. Plan 5 needs no independent transfer mechanism. Plan 8’s cleanup must drain these producers and deliveries. |
| + |
| +**L18. Two-box-per-region model: adopt as written, with additional witnesses.** |
| + |
| +This is required new evidence. Moves **§14.2.6** explicitly limits the existing model to one box per region, so the clean joint rounds do not prove these changes. |
| + |
| +Add these witnesses to the requested cases: |
| + |
| +- Relocation start racing purge or app-placement admission closure. |
| +- Empty-database drain with files and timers. |
| +- Generation parking while relocation pins referenced files. |
| +- Move landing, source cleanup, then target failure with an unchanged file. |
| +- Automatic target loss racing the record commit CAS. |
| +- A failed cleanup leaving a controller record that blocks executable updates. |
| +- First `released` admission followed by an uncertified failed probe. |
| +- Crash between prepared admission, marker publication and replication opening. |
| + |
| +The adverse-volume case must assert both outcomes: execution recovery proceeds, while local chores remain open. |
| + |
| +**Code impact:** `internal/sim/hostlife` is not in the inspected main tree. Extend the joint-model branch, then add targeted tests against the real `hostclaim`, `park`, `stopevidence`, `hostfiles` and `hostexec` boundaries. Plans 5, 6 and 8 each contribute race cases. Existing model results are not a substitute for those adapter tests. |
| + |
| +**L19. Automatic Auto Scaling enrollment: adopt with changes.** |
| + |
| +The direction is already incorporated by **§1.1 P3**, referencing H16/H17. The detailed confirmation protocol belongs in D7 and spec 4. |
| + |
| +The evidence must remain tied to the current enrollment attempt. A permanently create-only confirmation cannot mean “current group member” indefinitely. |
| + |
| +Add to **§10.1 D7**: |
| + |
| +> The console may automatically enroll an Auto Scaling box when verified `boxid` evidence and an authenticated worker’s fresh membership confirmation agree on the deployment account, expected AWS region, instance and roster-configured group. |
| +> |
| +> The confirmation binds an enrollment attempt and the roster group identity. It is immutable and consumed only for that attempt. Expired or superseded evidence requires a new immutable confirmation identity; replay of an old confirmation grants no enrollment. |
| +> |
| +> A worker from another region may confirm only when every relevant active or quarantined enrollment in the target region has a positive `terminated` observation in the same pass. The console revalidates that the confirmation covers the current required set. Missing, partial or nonterminal observations refuse automatic enrollment. |
| +> |
| +> Cross-region confirmation grants no cross-region fencing, relocation, retirement or data access. Once enrolled, the new box performs local recovery through the normal regional contracts. |
| +> |
| +> Every other enrollment remains operator-approved. Floor and executable-identity requirements apply before authority is granted. |
| + |
| +The confirmation format needs an attempt/confirmation ID so refreshing evidence does not overwrite the original create-only object. |
| + |
| +**Code impact:** This remains outstanding roster/spec-4 work. Reuse main’s `boxid`; implement confirmation validation and the narrow read-only AWS adapter. Plans 5 and 6 consume resulting eligibility. Plan 8 must not treat its existing directory interface as an implemented enrollment system. |
| + |
| +**L20. Stale console report for box-started relocation: adopt with changes.** |
| + |
| +H18 rules the narrow freshness exception. It is not yet incorporated into **D7’s operative report rules**, and is not implemented by the current branches. |
| + |
| +Add to **§10.1 D7**: |
| + |
| +> For a box-started relocation only, the census may accept a required console’s newest report beyond the normal freshness interval when the report passes every other current floor and identity check and its exact enrolled compute box has reported the D1 root guard armed for the same floor digest. |
| +> |
| +> The compute binding must cover the actual console executable and every replacement/bootstrap path. Guard readiness for an unrelated process or enrollment is insufficient. |
| +> |
| +> The report must be the newest report for that console enrollment, not a selected older passing report. A newer incompatible, malformed or identity-mismatched report refuses the exception. Future-time checks remain unchanged. |
| +> |
| +> Missing compute binding, missing guard evidence or a changed floor requires the ordinary fresh-report path. No other operation or actor receives this freshness exception. |
| + |
| +**Code impact:** Implement this in the outstanding census provider. Plan 5’s console-started operations keep ordinary freshness. Plan 6’s regional relocation starter selects this narrowly scoped policy. Plan 8 supplies authenticated guard and enrollment evidence. |
| + |
| +The implementation order should be: settle L1’s app-admission and phase contracts; add L4’s automatic loss persistence; implement L9–L13’s admission, stop and retention changes; then integrate relocation and the two-box model. Adding `relocating` to the kind list before its phase restrictions would create an authority gap. |
| + |
| +This was a source review. No files were written and no tests were run. |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +“Read /home/paulca/.cache/tmp/claude-1001/own/after236/ha-brief.md and do exactly what it says.” |
| + |
| +**WHAT:** |
| +Analyse HA requests L1–L20 against the claim, moves and implementation branches. |
| + |
| +**STATUS:** |
| +Complete. All twenty dispositions, proposed amendments and code impacts are above. |
| + |
| +**NEEDED:** |
| +Nothing for this read-only review. |
| + |
| +**RECOMMENDED:** |
| +Incorporate the amended contracts together, then validate the interacting changes in the joint model. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed or background processes started. |
| \ No newline at end of file |