amadan
docs: two-box model plan rev 11, Astra round 8: root's stop receipt tracked apart from the recorded positions with the flushing controller's identity, the identity traces over the gate's seeds 1..n, Task 5H and the round 8 dispositions
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+332
−10
docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md+332 −10
diff --git a/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md| index a016048d3..762e3bd1f 100644 |
| --- a/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md |
| +++ b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md |
| @@ -1,15 +1,36 @@ |
| -# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 10) |
| +# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 11) |
| > **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. |
| **Goal:** Extend `internal/sim/hostlife`, the joint executable model of the host lifecycle claim and instance moves, from one box per region to one or two boxes per region, with region HA's `relocating` operation modelled as spec 1 §5.8 and plan 1b-next **rev 19** define it (drain, failover, pinning, the replacement table, `stuck`), every case claim rev 6.30 §11 and spec L18 name for region HA's validation milestone as a scenario in a one-box and in a two-box region, and one mutation check per guard; then write the brief for the joint round that gates the merge of relocation (claim §1.1, R18-3; plan 1b-next Task 11). |
| -**Architecture:** Thirteen tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D, rev 8 Task 5E, rev 9 Task 5F, rev 10 Task 5G) over one Go test package (every file is `_test.go`; nothing here is product code). Task 1 generalises the world's shape (`boxesPerRegion`, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed `relocate` with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, `prepared_opened` journaled, three probe attempts counted before they are made, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from `serving`, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 5D (rev 7) answers round 4: the target is named before any pin on every path, the phase predicates know `PinFailover`, and a failover passes Worker.Start's guards. Task 5E (rev 8) answers round 5: a pending fence holds the phase, as Worker.Step's early return does. Task 5F (rev 9) answers round 6: a release needs its own flush or the positions it recorded. Task 5G (rev 10) answers round 7: a stopped box keeps its local cleanup, and the operator stops only a target whose release cannot come. Task 6 wires the shape and the region HA rule group into `mutate.sh` and `expected-outcomes.txt`. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in `rules_test.go` whose comment names the 1b-next function it mirrors. |
| +**Architecture:** Fourteen tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D, rev 8 Task 5E, rev 9 Task 5F, rev 10 Task 5G, rev 11 Task 5H) over one Go test package (every file is `_test.go`; nothing here is product code). Task 1 generalises the world's shape (`boxesPerRegion`, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed `relocate` with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, `prepared_opened` journaled, three probe attempts counted before they are made, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from `serving`, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 5D (rev 7) answers round 4: the target is named before any pin on every path, the phase predicates know `PinFailover`, and a failover passes Worker.Start's guards. Task 5E (rev 8) answers round 5: a pending fence holds the phase, as Worker.Step's early return does. Task 5F (rev 9) answers round 6: a release needs its own flush or the positions it recorded. Task 5G (rev 10) answers round 7: a stopped box keeps its local cleanup, and the operator stops only a target whose release cannot come. Task 5H (rev 11) answers round 8: recorded positions finish a release only for their own controller or with root's receipt. Task 6 wires the shape and the region HA rule group into `mutate.sh` and `expected-outcomes.txt`. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in `rules_test.go` whose comment names the 1b-next function it mirrors. |
| **Tech Stack:** Go 1.26 test files, standard library only (the model imports nothing else; `hash/fnv` for the tie-break stand-in over the box id in Tasks 1 to 5A; from Task 5B `crypto/sha256` over the host, as 1b-next hashes it). `go test ./internal/sim/hostlife/` is the gate; `mutate.sh` runs the prebuilt binary per rule. |
| **Spec:** region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4 with §24; rulings H1 to H19 in §0; §2 words; §3 invariants HA1 to HA7; §5.2 create; §5.3 rows; §5.4 edges; §5.6 files; §5.8 relocation; §5.9 the fence; §5.10 updates; §7 failure modes; §9 L1 to L20). Plan 1b-next **rev 19** (rev 2 of this plan synced to rev 16; rev 3 adds rulings 25 to 27, the "Rev 17" to "Rev 19" dispositions and request L21) `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (Astra's round 18: "stage A ready to build"; its rulings 1 to 24, its dispositions tables for revs 2 to 16, Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's merge gate) and the review findings beside it, `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R18.md`. Claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 "Same-region relocation (L1)"; §6.2a "Files in the live set (L13)"; §6.4a item 2; §7.3 D2 to D6; §11 "Region HA's validation milestone" and the additional witnesses). Moves rev 7.22 on this branch, `docs/superpowers/specs/2026-10-02-move-any-app-design.md` (§7.6, §7.10 the conversion; §14.2 the model, its evidence policy and the harness). The model's own rules are in `internal/sim/hostlife/rules_test.go`; read `world_test.go`'s package comment and §14.2 before Task 1. |
| +## Rev 11: round 8 dispositions |
| + |
| +Astra's round 8 (`CODEX-PLAN-REGION-HA-TWO-BOX-R8.md`, against `54a37976`) found both round 7 findings resolved and raised one P2 and one P3. Its verdict was "not ready". Both are accepted. The P2 is fixed in a new **Task 5H**, a patch on Task 5G's tree, and Task 6's patch is regenerated on top of it. The P3 is fixed in Task 1 Step 1's identity test; the later tasks' patches do not touch that file. |
| + |
| +| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |
| +|---|---|---|---|---|---| |
| +| R8 #1 (P2) | Correct. In 1b-next rev 19 (Task 7), `Release` records the flushed positions before the producers drain and before root persists the stop receipt. After a restart the request names the recorded identity, `RecoveryReleaseDrain` refuses, and only root's durable receipt finishes the release. A retry by the same controller resumes at the producers' drain. Rev 9's `releaseRecord` replayed the positions alone, so a crash between the record and the receipt looked like a finished stop. | accepted | `releaseRecord` now keeps the flushing controller (`Ctl`, the agent process: `box.Epoch`) and `Receipt`, root's persisted stop receipt, apart from the positions. The release sequence ends at the record. The next step, by the same controller, is the producers' drain and the receipt, and only then is the release returned. After a restart a record with a receipt replays. A record without one is refused, so there is no release and the deadline makes the operation stuck. `releaseUnrecoverable` counts a record as recoverable only with the receipt, or while its own controller still runs. This is the new rule `reloc-release-needs-receipt`. Its mutation replays the positions alone, as rev 10 did. It is an expected miss: the replayed release is the flushed one, so no invariant fails. | Task 5H | `TestReleaseRefusedAfterACrashBeforeTheReceipt`: the source records, then crashes before the receipt. No release and no pin appear, it is stuck at the deadline, and the resolve returns the host to the source. `TestOperatorStopsATargetWithNoReceipt`: the same for a failed target, which the operator stops before the host serves elsewhere. Both fail under the mutation. The other side of the receipt, a crash after it, is `TestReleaseReplaysTheRecordedFlush` and `TestOperatorResumesARecordedFlush`, whose release sequence now runs through the receipt before the crash. | |
| +| R8 #2 (P3) | Correct. `TestOneBoxSeedTraces` hashed seeds 0 to 299, and the gate's sweep runs 1 to 300. | accepted | The identity loop runs `1..n`, the gate's range, and its 300 lines are seeds 1 to 300. | Task 1 Step 1 | (coverage) | |
| + |
| +Astra also noted that R5-3 (HA-disabled reconcile) and R5-5 (the env file's deletion) rest on 1b-next's own tests. They join the adapter-only rows of "Past findings, and where their evidence lives" (rev 4); the model has no step for either. |
| + |
| +**Dry run (2026-10-08).** The scratch module was rebuilt from the baseline. The corrected identity test was added and the baseline's traces recorded with it, and Task 1 was applied from prose. The patches for Tasks 2 to 5G were applied from this document, then Task 5H and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's. The seed file runs 1 to 300. |
| + |
| +| After | One-box COUNTERS and traces | Two-box | Gate | |
| +|---|---|---|---| |
| +| Tasks 1 to 5G | identical | as in rev 10 | ok | |
| +| Task 5H | identical | 300, 0 failed, 483. The release's receipt is its own step, so the sweep's trajectories moved: 9 receipts persisted, 12 releases refused, and 2 targets stopped by the operator. | ok. The two new tests pass and fail under `reloc-release-needs-receipt`. Both replay tests still pass. | |
| +| Task 6 | the same | the same | ok. `@regionha` lists 54 rules, 162 in all. | |
| + |
| +No mutation sweep was run, and the scratch module was then removed. |
| + |
| ## Rev 10: round 7 dispositions |
| Astra's round 7 (`CODEX-PLAN-REGION-HA-TWO-BOX-R7.md`, against `979c38da`) found round 6's finding resolved and raised two new P2s. Its verdict was "not ready". Both are accepted and fixed in a new **Task 5G**, a patch on Task 5F's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5F are unchanged. |
| @@ -218,6 +239,7 @@ Astra's round 1 on this plan (`CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, against `3c7 |
| | R2-5, R3-2, R4-5, R5-4, R12-1, R13-1, R13-2, R14-2, R15-2, R18-1 | controller lifecycle: cleanup failures, lifetime locks, durable participation, removal during an ongoing operation | Task 7 `TestRelocationControllerLifecycleProperties` (200 seeds, invariants (a) to (i)) and its named tests. The model keeps only claim §11's case, a failed cleanup keeping the update-blocking record (witness `reloc-clear-after-cleanup`). | |
| | R18-2 | host-dependent hash selection | Task 2 `TestExecutorChooserHashesTheRecordsHostOnEqualLoads`, and this model's `TestTieHashFollowsTheHost` | |
| | R1-1, R3-1, R3-3, R4-N1 to N3, R6-1, R7-1, R8-2, R9-1, R10-1, R12-2, R14-3 | compilation, adapters, privileges, kernel descriptors, production wiring | the production-boundary tests each disposition names (Tasks 2, 3, 4, 7, 9a, 10) | |
| +| R5-3, R5-5 (added in rev 11, Astra round 8) | the HA-disabled reconcile; the env file's deletion in the release flush | 1b-next's own tests (Task 9a `TestReconcileWithoutAFenceObserverIsTodays`; Task 7 `TestReleaseFlushFilesCarriesTheLastWakeStateAndEnv`); the model has no step for either | |
| **Dry run (2026-10-08).** The scratch module was built from the baseline. The identity tests were added and the baseline's two trace files recorded. Task 1 was applied from its prose, and the patches for Tasks 2 to 6 from this document, one at a time. After each task: build, vet, gofmt, the gate, and both trace files compared byte for byte with the baseline's. |
| @@ -505,7 +527,7 @@ func TestOneBoxSeedTraces(t *testing.T) { |
| } |
| mask := regexp.MustCompile(`admission=\[[^\]]*\]`) |
| var out []string |
| - for seed := int64(0); seed < int64(seedsFromEnv(300)); seed++ { |
| + for seed := int64(1); seed <= int64(seedsFromEnv(300)); seed++ { // the gate's seeds, 1..n (rev 11, Astra round 8) |
| w := runSeed(seed, true) |
| sum := sha256.Sum256([]byte(mask.ReplaceAllString(strings.Join(w.trace, "\n"), "admission=[masked]"))) |
| out = append(out, fmt.Sprintf("%d %x %d", seed, sum[:8], len(w.trace))) |
| @@ -9790,9 +9812,306 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| --- |
| +### Task 5H: Astra's round 8: recorded positions are not proof of a stop (rev 11) |
| + |
| +This is described in "Rev 11: round 8 dispositions" above. It contains: |
| +- `releaseRecord`, which gains `Ctl` and `Receipt`. |
| +- `relocRelease`'s record step, followed by a separate receipt step, under the rule `reloc-release-needs-receipt`. |
| +- `releaseUnrecoverable`, updated to match. |
| +- The helper `recordWithoutReceipt` and the tests `TestReleaseRefusedAfterACrashBeforeTheReceipt` and `TestOperatorStopsATargetWithNoReceipt`, with the two replay tests' comments updated. |
| + |
| +**Files:** |
| +- Modify: `world_test.go` (`releaseRecord`), `regionha_test.go` (`relocRelease`), `console_test.go` (`releaseUnrecoverable`), `rules_test.go`, `regionha_round1_test.go` |
| + |
| +- [ ] **Step 1: Apply the patch** |
| + |
| +```diff |
| +diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go |
| +index 9c219e2..d8aae45 100644 |
| +--- a/internal/sim/hostlife/console_test.go |
| ++++ b/internal/sim/hostlife/console_test.go |
| +@@ -1346,9 +1346,11 @@ func (w *world) operator() { |
| + |
| + // releaseUnrecoverable is the operator's check before it stops a live |
| + // target that has not released (rev 10, Astra round 7): only when no |
| +-// release can ever come. That needs no flush recorded for this stop, and |
| +-// either the session's replicator or the box's files directory gone for |
| +-// good (relocRelease refuses without either). Any other release, a slow |
| ++// release can ever come. That needs no usable flush record for this |
| ++// stop (rev 11: a record counts only with root's durable receipt, or while |
| ++// the controller that recorded it is still running), and either the |
| ++// session's replicator or the box's files directory gone for good |
| ++// (relocRelease refuses without either). Any other release, a slow |
| + // acknowledgement or a recorded flush not yet journaled, is resumed: the |
| + // resolve clears stuck and sends the target back to probe-failed. The |
| + // mutation of operator-stop-unrecoverable-only stops every such target, |
| +@@ -1358,8 +1360,9 @@ func (w *world) releaseUnrecoverable(b *box, c *claim) bool { |
| + return true |
| + } |
| + h := c.Holder |
| +- if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen { |
| +- return false // a recorded flush: the release replays it |
| ++ if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen && |
| ++ (r.Receipt || r.Ctl == b.Epoch || !on("reloc-release-needs-receipt")) { |
| ++ return false // a recorded flush with root's receipt, or its own controller still alive to finish it (rev 11) |
| + } |
| + replicator := b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session |
| + files := b.Files != nil && b.Files.Inc == h.Inc |
| +diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go |
| +index 4e8d93b..59c8f7b 100644 |
| +--- a/internal/sim/hostlife/regionha_round1_test.go |
| ++++ b/internal/sim/hostlife/regionha_round1_test.go |
| +@@ -811,12 +811,14 @@ func TestReleaseRefusedAfterACrashBeforeTheFlush(t *testing.T) { |
| + } |
| + |
| + // TestReleaseReplaysTheRecordedFlush (reloc-release-needs-flush; rev 9, |
| +-// Astra round 6): the source's release sequence completes and records |
| +-// its flushed positions (ReleasePositions), and its agent crashes before |
| +-// the release is journaled. The restarted agent has no replicator for |
| +-// the session, but the record is durable: the release is replayed with |
| +-// the recorded positions, Flushed, and the drain completes. The mutation |
| +-// records nothing and journals the remote position with Flushed false. |
| ++// Astra round 6; rev 11, round 8): the source's release sequence |
| ++// completes, records its flushed positions (ReleasePositions), and root |
| ++// persists the stop receipt; its agent then crashes before the release |
| ++// is journaled. The restarted agent has no replicator for the session, |
| ++// but the record and the receipt are durable: the release is replayed |
| ++// with the recorded positions, Flushed, and the drain completes. The |
| ++// mutation of reloc-release-needs-flush records nothing and journals the |
| ++// remote position with Flushed false. |
| + func TestReleaseReplaysTheRecordedFlush(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| +@@ -830,7 +832,7 @@ func TestReleaseReplaysTheRecordedFlush(t *testing.T) { |
| + } |
| + var r *releaseEntry |
| + for i := 0; i < 60 && r == nil; i++ { |
| +- r = w.relocRelease(from, w.claim.clone()) // steps 1 to 3 and the record, not yet journaled |
| ++ r = w.relocRelease(from, w.claim.clone()) // steps 1 to 3, the record and the receipt, not yet journaled |
| + w.tick() |
| + } |
| + if r == nil || !r.Flushed { |
| +@@ -913,9 +915,9 @@ func TestOperatorResumesASlowRelease(t *testing.T) { |
| + |
| + // TestOperatorResumesARecordedFlush (operator-stop-unrecoverable-only; |
| + // rev 10, Astra round 7 finding 2): the failed target completes its |
| +-// release sequence and records it, then its agent restarts (the |
| +-// session's replicator is gone) before the release is journaled, and the |
| +-// deadline passes. The recorded flush is a release waiting to be |
| ++// release sequence, records it and gets root's receipt (rev 11), then its |
| ++// agent restarts (the session's replicator is gone) before the release is |
| ++// journaled, and the deadline passes. The recorded flush is a release waiting to be |
| + // journaled: the resolve resumes it, the target replays the record, and |
| + // the nested relocation serves. The mutation stops the box. |
| + func TestOperatorResumesARecordedFlush(t *testing.T) { |
| +@@ -923,7 +925,7 @@ func TestOperatorResumesARecordedFlush(t *testing.T) { |
| + from, to := w.probeFailedTarget(t) |
| + var r *releaseEntry |
| + for i := 0; i < 60 && r == nil; i++ { |
| +- r = w.relocRelease(to, w.claim.clone()) // steps 1 to 3 and the record, not journaled |
| ++ r = w.relocRelease(to, w.claim.clone()) // steps 1 to 3, the record and the receipt, not journaled |
| + w.tick() |
| + } |
| + if r == nil { |
| +@@ -976,6 +978,85 @@ func TestStoppedTargetKeepsItsLocalCleanup(t *testing.T) { |
| + w.mustHold(t) |
| + } |
| + |
| ++// recordWithoutReceipt runs b's release sequence until its flushed |
| ++// positions are recorded, and stops before the producers drain and root |
| ++// persists the receipt. |
| ++func (w *world) recordWithoutReceipt(t *testing.T, b *box) { |
| ++ for i := 0; i < 60 && b.relRecord == nil; i++ { |
| ++ w.relocRelease(b, w.claim.clone()) |
| ++ w.tick() |
| ++ } |
| ++ if r := b.relRecord; r == nil || r.Receipt { |
| ++ t.Fatalf("no record without a receipt on box %d: %+v %s", b.ID, r, w.state()) |
| ++ } |
| ++} |
| ++ |
| ++// TestReleaseRefusedAfterACrashBeforeTheReceipt (reloc-release-needs-receipt; |
| ++// rev 11, Astra round 8): the source records its flushed positions, and |
| ++// its agent crashes before root persists the stop receipt. The positions |
| ++// are not proof of the stop: the restarted agent's release is refused |
| ++// (RecoveryReleaseDrain), no release or pin appears, the deadline makes |
| ++// the operation stuck, and the resolve returns the host to its source. |
| ++// TestReleaseReplaysTheRecordedFlush is the other side: the crash after |
| ++// the receipt, replayed. The mutation replays the positions alone. |
| ++func TestReleaseRefusedAfterACrashBeforeTheReceipt(t *testing.T) { |
| ++ w := twoBoxWitness() |
| ++ from, to := w.boxes[0], w.boxes[3] |
| ++ w.serve(from, 1, app0) |
| ++ w.running(t, from) |
| ++ w.published(t, from) |
| ++ w.drainTo(t, to) |
| ++ w.appWrite(from) |
| ++ if !w.stepUntil(t, 1500, "releasing", w.atPhase("releasing")) { |
| ++ w.mustHold(t) |
| ++ } |
| ++ w.recordWithoutReceipt(t, from) |
| ++ w.crash(from) |
| ++ for i := 0; i < releaseDeadline+20; i++ { |
| ++ w.tick(w.act(from, to)) |
| ++ c := w.claim |
| ++ if c.Op.Release != nil || c.Op.Pin != nil { |
| ++ t.Fatalf("a release or a pin from recorded positions with no receipt (step %d): %s", i, w.state()) |
| ++ } |
| ++ if c.Op.Stuck != "" { |
| ++ break |
| ++ } |
| ++ } |
| ++ if c := w.claim; c.Op.Stuck == "" || c.Op.Phase != "releasing" { |
| ++ t.Fatalf("not stuck in releasing at the release deadline: %s", w.state()) |
| ++ } |
| ++ w.finish(t) |
| ++ w.mustHold(t) |
| ++ if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID { |
| ++ t.Fatalf("the operator's resolve did not return the host to its source: %s", w.state()) |
| ++ } |
| ++} |
| ++ |
| ++// TestOperatorStopsATargetWithNoReceipt (reloc-release-needs-receipt, |
| ++// operator-stop-unrecoverable-only; rev 11, Astra round 8): the failed |
| ++// target records its flushed positions and its agent restarts before root |
| ++// persists the receipt. Its release can never come, so the operator stops |
| ++// it, and the next resolve replays the operation; the host serves |
| ++// elsewhere. The mutation treats the positions as recoverable and resumes |
| ++// a release that replays them. |
| ++func TestOperatorStopsATargetWithNoReceipt(t *testing.T) { |
| ++ w := twoBoxWitness() |
| ++ _, to := w.probeFailedTarget(t) |
| ++ w.recordWithoutReceipt(t, to) |
| ++ w.crash(to) |
| ++ if !w.reach(t, 3000, "serving after the operator's stop and replay", func() bool { |
| ++ c := w.claim |
| ++ return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != to.ID |
| ++ }, w.actAll(), w.recoveryPass, w.wakeExec, w.resolveOnly) { |
| ++ w.mustHold(t) |
| ++ } |
| ++ if !to.Destroyed || w.stats["operator stopped a target that cannot release"] == 0 || w.stats["release journaled: failed target"] != 0 { |
| ++ t.Fatalf("the target was not stopped, or released from positions with no receipt: %v %s", w.stats, w.state()) |
| ++ } |
| ++ w.finish(t) |
| ++ w.mustHold(t) |
| ++} |
| ++ |
| + // TestPinNeverShortOfTheRelease (reloc-pin-reaches-release): the listing |
| + // lags behind the journaled release (its newest file is not yet visible); |
| + // no pin is journaled short of the release's final_txid. |
| +diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go |
| +index 1407d22..1d4677f 100644 |
| +--- a/internal/sim/hostlife/regionha_test.go |
| ++++ b/internal/sim/hostlife/regionha_test.go |
| +@@ -146,11 +146,29 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry { |
| + } |
| + if r := b.relRecord; r != nil && on("reloc-release-needs-flush") && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen { |
| + // a flush this box recorded for this stop (ReleasePositions.Recorded): |
| +- // the release is replayed with the recorded positions, never |
| +- // flushed or guessed again (rev 9) |
| ++ // never flushed or guessed again (rev 9). Rev 11 (Astra round 8): |
| ++ // the positions are not proof of the stop. The controller that |
| ++ // recorded them resumes at the producers' drain, and root persists |
| ++ // the receipt (step 4); after a restart only root's durable receipt |
| ++ // for the recorded identity finishes the release, and with none |
| ++ // RecoveryReleaseDrain refuses: no release, and the deadline |
| ++ // makes the operation stuck. The mutation of |
| ++ // reloc-release-needs-receipt replays the positions alone, as rev |
| ++ // 10 did |
| ++ switch { |
| ++ case r.Receipt || !on("reloc-release-needs-receipt"): |
| ++ if r.Ctl != b.Epoch { |
| ++ w.stats["release: replayed from the recorded positions"]++ |
| ++ } |
| ++ case r.Ctl == b.Epoch: |
| ++ r.Receipt = true // the producers drain; root persists the receipt |
| ++ w.stats["release: receipt persisted"]++ |
| ++ default: |
| ++ w.stats["release: recorded positions without a receipt, refused"]++ |
| ++ return nil |
| ++ } |
| + e := r.E |
| + e.Files, e.Timers = r.E.Files.clone(), append([]int(nil), r.E.Timers...) |
| +- w.stats["release: replayed from the recorded positions"]++ |
| + return &e |
| + } |
| + prefix := dataKey(h.Location, h.Gen, "") |
| +@@ -227,8 +245,13 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry { |
| + Files: files, Timers: append([]int(nil), b.Timers...), At: w.now} |
| + if on("reloc-release-needs-flush") { |
| + // ReleasePositions.Record: durable before the producers close |
| +- b.relRecord = &releaseRecord{Op: c.Op.ID, Phase: c.Op.Phase, E: *e} |
| ++ b.relRecord = &releaseRecord{Op: c.Op.ID, Phase: c.Op.Phase, E: *e, Ctl: b.Epoch} |
| + b.relRecord.E.Files, b.relRecord.E.Timers = files.clone(), append([]int(nil), b.Timers...) |
| ++ if on("reloc-release-needs-receipt") { |
| ++ // the producers' drain and root's receipt are the next step: |
| ++ // a crash here leaves positions and no receipt (rev 11) |
| ++ return nil |
| ++ } |
| + } |
| + return e |
| + } |
| +diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go |
| +index a35e999..eef576e 100644 |
| +--- a/internal/sim/hostlife/rules_test.go |
| ++++ b/internal/sim/hostlife/rules_test.go |
| +@@ -197,6 +197,7 @@ var allRules = []string{ |
| + "files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3) |
| + "reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29) |
| + "fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3) |
| ++ "reloc-release-needs-receipt", // rev 11 (Astra round 8; 1b-next rev 19 Task 7 Release, RecoveryReleaseDrain): recorded positions finish a release only for the controller that recorded them, or with root's durable receipt after a restart; the mutation replays the positions alone (TestReleaseRefusedAfterACrashBeforeTheReceipt, TestOperatorStopsATargetWithNoReceipt) |
| + "operator-stop-unrecoverable-only", // rev 10 (Astra round 7; plan ruling 13, no 1b-next code): the operator stops a live target that has not released only when its release is unrecoverable (no recorded flush, and the session's replicator or its files gone); otherwise the resolve resumes the release; the mutation stops every such target (TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush) |
| + "reloc-release-needs-flush", // rev 9 (Astra round 6; 1b-next rev 19 Task 7 Release, relocationFlushDB, ReleaseFlushFiles, ReleasePositions): a release needs the session's own replicator and the box's own files directory, or the positions it recorded for this stop; otherwise none, and the deadline makes the operation stuck; the mutation journals the remote position with Flushed false (TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush) |
| + "reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase) |
| +diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go |
| +index af8e364..7d5827e 100644 |
| +--- a/internal/sim/hostlife/world_test.go |
| ++++ b/internal/sim/hostlife/world_test.go |
| +@@ -936,6 +936,15 @@ type opState struct { |
| + type releaseRecord struct { |
| + Op, Phase string |
| + E releaseEntry |
| ++ // Ctl is the flushing controller's identity: the agent process |
| ++ // (box.Epoch) that flushed and recorded (rev 11). Receipt is root's |
| ++ // durable stop receipt for this stop, persisted after the producers |
| ++ // drained (step 4), tracked apart from the recorded positions: only |
| ++ // the same controller may finish from the positions alone, and after a |
| ++ // restart the release needs the receipt too (1b-next Task 7 Release, |
| ++ // RecoveryReleaseDrain; Astra round 8) |
| ++ Ctl int |
| ++ Receipt bool |
| + } |
| + |
| + type releaseEntry struct { |
| +``` |
| + |
| +- [ ] **Step 2: Run the gate, the identity traces, and the new tests under their mutation** |
| + |
| +```bash |
| +gofmt -l internal/sim/hostlife/; nice -n 19 go vet ./internal/sim/hostlife/ |
| +nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task5h.log | grep -E "seeds, |^--- FAIL|^ --- FAIL|^ok|^FAIL" |
| +diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5h.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL |
| +HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null |
| +cmp $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/trace.txt && cmp $TMPDIR/twobox/baseline-seeds.txt $TMPDIR/twobox/seeds.txt && echo ONE-BOX-TRACES-IDENTICAL |
| +HOSTLIFE_MUTATE=reloc-release-needs-receipt nice -n 19 go test ./internal/sim/hostlife/ -run '^(TestReleaseRefusedAfterACrashBeforeTheReceipt|TestOperatorStopsATargetWithNoReceipt)$' -count=1 -v 2>&1 | grep -cE '^--- FAIL' |
| +``` |
| + |
| +Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=2`, `ok`, `ONE-BOX-COUNTERS-IDENTICAL`, `ONE-BOX-TRACES-IDENTICAL`, `2`. |
| + |
| +- [ ] **Step 3: Commit** |
| + |
| +```bash |
| +git add internal/sim/hostlife/ |
| +git commit -m "sim: Astra's round 8 on the two-box model: root's stop receipt is tracked apart from the recorded positions, with the flushing controller's identity; only that controller finishes from the positions, and after a restart the receipt is needed too |
| + |
| +Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| +``` |
| + |
| +--- |
| + |
| ### Task 6: The harness: `mutate.sh`'s shape and the region HA group, `expected-outcomes.txt`, and the revision's one sweep (moves §14.2; the evidence policy) |
| -`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 53 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 27 region HA rules that are not caught alone, each with its reason and the direct test that shows it. |
| +`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 54 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 28 region HA rules that are not caught alone, each with its reason and the direct test that shows it. |
| **Files:** |
| - Modify: `internal/sim/hostlife/mutate.sh`, `internal/sim/hostlife/expected-outcomes.txt` |
| @@ -9801,10 +10120,10 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| ```diff |
| diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt |
| -index 72504e3..b70bf86 100644 |
| +index 72504e3..f46fe7b 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| -@@ -21,3 +21,30 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| +@@ -21,3 +21,31 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
| @@ -9835,6 +10154,7 @@ index 72504e3..b70bf86 100644 |
| +reloc-fence-pending-blocks missed a fidelity guard: under the mutation the phase moves on while a dead target's fence waits for a spare, and the fence is consumed later by the replacement table at whatever phase the operation reached, which no model invariant distinguishes; TestPendingTargetFenceHoldsThePhase fails under the mutation |
| +reloc-release-needs-flush missed a fidelity guard: the mutation's unflushed release is legal in the model (the next admission declares what the remote does not hold, as writes_lost), so no invariant fails, but 1b-next refuses it and waits for the deadline; TestReleaseRefusedAfterACrashBeforeTheFlush and TestReleaseReplaysTheRecordedFlush fail under the mutation |
| +operator-stop-unrecoverable-only missed a fidelity guard on the operator's resolve: the mutation stops a target that could still release, and the declared loss and replay that follow are legal in the model, so no invariant fails; TestOperatorResumesASlowRelease and TestOperatorResumesARecordedFlush fail under the mutation |
| ++reloc-release-needs-receipt missed a fidelity guard: under the mutation recorded positions replay without root's receipt, and the release they journal is the flushed one, so no model invariant fails, but 1b-next refuses it after a restart; TestReleaseRefusedAfterACrashBeforeTheReceipt and TestOperatorStopsATargetWithNoReceipt fail under the mutation |
| diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh |
| index c583d97..883996e 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| @@ -9949,11 +10269,11 @@ HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 | wc -l |
| nice -n 19 go test ./internal/sim/hostlife/ -count=1 2>&1 | tail -1 |
| ``` |
| -Expected (the dry run's): `SYNTAX-OK`, `53`, `161`, `ok`. |
| +Expected (the dry run's): `SYNTAX-OK`, `54`, `162`, `ok`. |
| - [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)** |
| -Run only when Tasks 1 to 5G are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| +Run only when Tasks 1 to 5H are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| ```bash |
| export GOFLAGS=-buildvcs=false |
| @@ -9997,7 +10317,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| - region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4, §24; H1 to H19; §2, §3, §5.2, §5.3, §5.4, §5.6, §5.8, §5.9, §5.10, §7, §9 L1 to L20); |
| - claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 L1, §6.2a L13, §6.4a item 2, §7.3 D2 to D6, §11); |
| - moves rev 7.22 on this branch (§7.6, §7.10, §14.2); |
| -- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 10 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, `CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, and compares the worker's checks with `Worker.Step`; "Rev 9: round 6 dispositions" answers round 6, `CODEX-PLAN-REGION-HA-TWO-BOX-R6.md`, and compares every release and flush path with Task 7; "Rev 10: round 7 dispositions" answers round 7, `CODEX-PLAN-REGION-HA-TWO-BOX-R7.md`). |
| +- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 11 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, `CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, and compares the worker's checks with `Worker.Step`; "Rev 9: round 6 dispositions" answers round 6, `CODEX-PLAN-REGION-HA-TWO-BOX-R6.md`, and compares every release and flush path with Task 7; "Rev 10: round 7 dispositions" answers round 7, `CODEX-PLAN-REGION-HA-TWO-BOX-R7.md`; "Rev 11: round 8 dispositions" answers round 8, `CODEX-PLAN-REGION-HA-TWO-BOX-R8.md`). |
| ## Fixed: do not re-argue |
| @@ -10063,6 +10383,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| | reloc-fence-pending-blocks | `Worker.Step` returns `w.replace(...)` before its phase switch | two-box R5 #1 | §5.8, §5.9 | expected miss; `TestPendingTargetFenceHoldsThePhase` | |
| | reloc-release-needs-flush | Task 7 `Release`, `releaseDrain`, `relocationFlushDB`, `ReleaseFlushFiles`, `ReleasePositions` | two-box R6 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheFlush`, `TestReleaseReplaysTheRecordedFlush` | |
| | operator-stop-unrecoverable-only | none (plan ruling 13; 1b-next writes no resolve) | two-box R7 #2 | §5.8 | expected miss; `TestOperatorResumesASlowRelease`, `TestOperatorResumesARecordedFlush` | |
| +| reloc-release-needs-receipt | Task 7 `Release`, `RecoveryReleaseDrain`, `ReleasePositions.Recorded` | two-box R8 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheReceipt`, `TestOperatorStopsATargetWithNoReceipt` | |
| ## Findings F1 to F3, closed, and the open window L21 |
| @@ -10099,6 +10420,7 @@ The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22 |
| 18. (Rev 8) Astra round 5's fix and the `Worker.Step` order table in "Rev 8: round 5 dispositions": a pending fence holds every regional transition, while the participant's own release and the box's other work stay schedulable. Is anything the model still runs while a fence is pending a `Worker.Step` transition? |
| 19. (Rev 9) Astra round 6's fix and the release-path table in "Rev 9: round 6 dispositions": no release without the session's own flush or a recorded one, the replay of a recorded flush, and the operator's stop of a target that can never release (plan ruling 13). Is the single `releaseRecord` a faithful stand-in for both of 1b-next's recovery cases? |
| 20. (Rev 10) Astra round 7's fixes: discharge only for a terminated box with qualifying evidence (INV-26 on the operation's discharges), and the operator's stop narrowed to an unrecoverable release. Is `releaseUnrecoverable` the right line between resume and stop? |
| +21. (Rev 11) Astra round 8's fix: the receipt apart from the recorded positions, with the flushing controller's identity. Is the agent process (`box.Epoch`) a faithful stand-in for 1b-next's boot and controller identity? |
| 14. (Rev 4) Claim §11's cases: the move with an unchanged file, the automatic target loss racing the record commit, the failed cleanup that blocks executable updates (INV-29), the forced open boundaries (four, the published marker before replication opens included). Are the file-object model (plan ruling 25) and the controller record faithful enough to stand for them, and is the coverage table in the plan's rev 4 section right about which findings only 1b-next's own tests can prove? |
| ## Output |
| @@ -10138,7 +10460,7 @@ Then hand the brief to the Codex second reader as memory `codex-second-reader.md |
| ## Self-review |
| -- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 53 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4, rev 8 one for round 5, rev 9 one for round 6, rev 10 one for round 7); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function. |
| +- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 54 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4, rev 8 one for round 5, rev 9 one for round 6, rev 10 one for round 7, rev 11 one for round 8); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function. |
| - **L18 and claim §11.** Every L18 case is a `TestL18*` with one-box and two-box subtests; claim §11's extras are direct tests or witnesses, each listed in "Rev 4: round 1 dispositions". §5.8's table (Task 2), the release (Tasks 2, 4), the pin (Tasks 2, 4), P's build (Tasks 2, 4), the local install, EnsureLocal and VerifyReceipt (Task 2), the probe (Task 2), the replacement table, source loss and the exhausted fence (Task 3), the cap and stuck (Tasks 2, 3), what a relocation leaves behind (Tasks 2, 4). §5.9 (Task 3). §5.2 (Tasks 1, 5). §5.3 (Task 2). §5.6 (Task 4). §5.10 is root's and the participant's controller: not modelled. |
| - **Placeholders.** Every task carries its dry-run patch. The brief's `<...>` fields are filled from logs in Task 7 Step 1 and may not remain. |
| - **Type consistency.** The patches compiled and passed in order; `go vet` was clean after each. |