amadan
plans: two-box joint model rev 3, synced to plan 1b-next rev 19: model rulings 14, 16 and 17 now mirror 1b-next rulings 26, 27 and 25 (no-spare and dead-target bounds, every unopened P recorded and parked, files pinned only with instance.key); the finding tests pass because the gaps are closed, four guards reopen them under mutation, and a witness scripts the L21 window failing safe; Task 5A dry-run with the one-box COUNTERS byte-identical
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+608
−32
docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md+608 −32
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 58b1a5b11..37f66a9e5 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,14 +1,41 @@ |
| -# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 2) |
| +# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 3) |
| > **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 16** 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). |
| +**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:** Seven tasks 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 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). `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 16** `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (Astra's round 16: "stage A ready to build, stage B contracts complete"; 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 `R16.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. |
| +**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 3: sync to 1b-next rev 19 |
| + |
| +Rev 2 reported three gaps in 1b-next rev 16 (F1 to F3). 1b-next fixed them in rev 17, tightened the fixes in rev 18 (Astra's round 17 found each only partly closed), and Astra accepted rev 19 as "stage A ready to build" (round 18 raised test gaps only). Rev 3 replaces the model's own stand-ins for F1 to F3 (rev 2's rulings 14, 16 and 17) with mirrors of 1b-next's fixes, turns the three finding tests into evidence that the gaps are closed, adds a mutation check that reopens each gap, and models the open request L21 as an explicit window. Everything is in one new task, **Task 5A**, a patch on Task 5's tree; Task 6's patch is regenerated on top of it (one more `expected-outcomes.txt` line). Tasks 1 to 5 are unchanged. |
| + |
| +| Gap | 1b-next fix | Model rule (new) | Mutation reopens it | Evidence | |
| +|---|---|---|---|---| |
| +| F2 | ruling 25 as rev 18 amended it: when a writer was admitted and the pinned database is nonempty, the pinned manifest must carry a live `instance.key` (`needKey`, `liveEntry`); otherwise `ErrFilesUnevidenced` and `stuck`. No manifest at all is the same case. | `files-pin-needs-key` (`selectPin`, `manifestHasKey`) | pins the keyless files; the install mints a fresh key over the sealed rows | witness `files-pin-needs-key` (INV-4, the L21 window); `TestFailoverBeforeTheFirstManifest` (now: stuck, nothing installed) | |
| +| F1 | ruling 26: `probe-failed` with no eligible spare is stuck `ReleaseDeadline` after `probe_failed_since`, never sent to the source | `reloc-no-spare-bound` (`relocProbeFailed`) | waits for a spare for ever | witness `reloc-no-spare-bound` (INV-3); `TestProbeFailedInATwoBoxRegion` (now also: waits before the deadline, never names the source) | |
| +| F1 | rev 18 finding 2: a dead target with no spare is fenced into `stuck` `ReleaseDeadline` after its `observed_at` (`FenceTargetWithoutSpare`, sharing `fenceTargetStuck` with the exhausted fence) | `reloc-dead-target-bound` (`replaceTarget`, `fenceTargetStuck`) | the fence is never consumed and nothing moves | witness `reloc-dead-target-bound` (INV-3) | |
| +| F3 | ruling 27 and rev 18 finding 3: every unopened P is journaled in `abandoned_prepared` before it is replaced or dropped (`abandonPrepared`: install, the replacement table's nested branch, and here also the nested relocation after `probe-failed` and the operator's replay) and parked by the serving CAS | `reloc-abandoned-prepared` (`abandonPrepared`, `opState.Abandoned`, replacing rev 2's `Built`) | records nothing | `TestAbandonedPreparedGenerationParked`, now on both paths (`installing`, and rev 18's `probe-failed` before any admission); an expected miss, because the model's at-rest sweep, which ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it | |
| + |
| +**L21, explicit.** The witness `files-pin-needs-key` (`wL21Window`) scripts the open window: the cold admission's pre-start manifest copy lands without `instance.key` (§5.6 copies it before the app starts), the app mints the key after it starts, writes and replicates rows sealed with it, and the box is terminated before the publisher's manifest carrying the key lands. With the rule the failover is stuck and installs nothing; without it the keyless pin installs a fresh key over the sealed rows (INV-4). The window itself stays open (L21 is Paul's: the platform pre-provisions the key, or the replicator holds its first upload until the key's manifest lands). Recovery there is stuck by design and no operator replay accepts a keyless pin, so the sweep, which must converge, never terminates such an executor (ruling 17, rewritten). |
| + |
| +**Other effects.** The `files-live-set` witness now names INV-3: with the chain's live manifest archived, the failover finds no keyed manifest and is stuck, where rev 2 showed the fresh key (INV-4). Ruling 25 turned that data loss into a stuck operation. `fenceExhaustedTarget` keeps its rule and now calls the shared `fenceTargetStuck`. The two-box sweep's summary is unchanged (300 seeds, 0 failed, 480 completed): the sweep never reaches the new refusals. |
| + |
| +**New gaps in 1b-next rev 19:** none found. One observation for the round: F3's fix cannot be caught by any invariant in the model, because the at-rest sweep cleans up first. Its value is that the operation owns the cleanup, which the direct test checks. |
| + |
| +**Dry run (2026-10-08).** The worktree's model at fbdad381 was copied into a scratch module, Task 1 was reapplied from its prose, and the rev 2 patches for Tasks 2 to 5 were applied from this document. Task 5A and the regenerated Task 6 were then applied, and the gate was run after each, niced, at default seeds: |
| + |
| +| After | One-box | Two-box | Gate | |
| +|---|---|---|---| |
| +| Task 5 (rev 2) | 300, 0 failed, 483; COUNTERS byte-identical | 300, 0 failed, 480 | ok | |
| +| Task 5A | 300, 0 failed, 483; COUNTERS byte-identical | 300, 0 failed, 480 | ok. The 23 region HA witnesses hold, hold under every proper subset, and violate their named failure under their set. Each of the three finding tests fails under its mutation. | |
| +| Task 6 | the same | the same | ok. `HOSTLIFE_LIST=1 mutate.sh 0 @regionha` lists 37 rules, 145 in all. | |
| + |
| +No mutation sweep was run. The scratch module was then removed. |
| ## Rev 2: sync to 1b-next rev 16 |
| @@ -92,11 +119,11 @@ Each was a gap or a conflict between the authorities. Each says what it costs if |
| 10. **Volume evidence is one flag per box.** H19 and §5.9: the fence never reads it; only automatic discharge of the dead box's `park-local` chores does. The model draws `DeleteOnTermination` per box and the discharge rule reads it in the fence CAS; the recorder, the two-hour bound and `removed_volumes` are plan 1b's unit tests, and 1b-next ruling 3 keeps production discharge off until the roster records an enrollment time. *Cost if wrong:* the adverse-volume case still proves what claim §11 asks: recovery proceeds and the chores stay open. |
| 11. **The files publisher exists where region HA is enabled, which the model ties to the two-box shape.** Spec §5.6 is region HA's; the one-box model has no publisher and carries files at the cut (`StopFiles`), and a converted move keeps that stand-in. In the two-box shape the executor publishes a manifest whenever its files or wake state change, whether or not the app runs, and a dead box's disk is never read (`deadBoxFiles`). *Cost if wrong:* a one-box drain would also want it; the one-box shape has no drain. |
| 12. **The review findings are on the branch now** (amended in rev 2). `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R16.md` sit beside 1b-next rev 16. The hazards the model must catch were taken from them and from the dispositions tables of revs 2 to 16; the "What changed, by task" table above names the finding each rule answers, and Task 7's table carries a column for it. Findings about stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10, the lifecycle property of rev 14 to 16) have no model step and are listed as such. |
| -13. **The operator's resolve (`carlos ops host resolve`) has three cases.** The spec names the command and leaves its effect open. Nothing moves away from a live box without its stop evidence: a live source still `op.exec` in `starting` or `releasing` with no release journaled is returned to `serving` (the relocation is abandoned); a live target `op.exec` without a release is sent to `probe-failed`, where it runs its release; otherwise (op.exec none, released or lost, a dead executor first declared lost as claim D2's operator path does) the operation is replayed from `pinning` with the replacement count reset, the exclusions cleared, the source eligible again, and an empty listing accepted (`Resolved`). *Cost if wrong:* one function in `console_test.go`; the guards are unchanged. |
| -14. **`probe-failed` with no eligible spare is stuck after `releaseDeadline`** (finding F1). 1b-next waits with no bound; without a bound the two-box sweep does not converge. *Cost if wrong:* if the claim session prefers another exit (the source as a spare, a deadline in the worker), the model's `relocProbeFailed` changes one branch. |
| +13. **The operator's resolve (`carlos ops host resolve`) has three cases.** The spec names the command and leaves its effect open. Nothing moves away from a live box without its stop evidence: a live source still `op.exec` in `starting` or `releasing` with no release journaled is returned to `serving` (the relocation is abandoned); a live target `op.exec` without a release is sent to `probe-failed`, where it runs its release; otherwise (op.exec none, released or lost, a dead executor first declared lost as claim D2's operator path does) the operation is replayed from `pinning` with the replacement count reset, the exclusions cleared, the source eligible again, and an empty listing accepted (`Resolved`); never a keyless files pin for a nonempty database (rev 3, ruling 17). *Cost if wrong:* one function in `console_test.go`; the guards are unchanged. |
| +14. **(Rev 3) `probe-failed` or a dead target with no spare is stuck after `releaseDeadline`, mirroring 1b-next ruling 26 and rev 18 finding 2** (finding F1, closed). In `probe-failed` with no eligible spare, the operation is stuck `releaseDeadline` after `probe_failed_since` (rule `reloc-no-spare-bound`). A dead target with no spare is fenced into `stuck` `releaseDeadline` after its termination, with the fence consumed (rule `reloc-dead-target-bound`, `fenceTargetStuck`). Neither ever names the source. Only the operator's resolve may, by plan ruling 13. Rev 2's version of this ruling was the model's own stand-in with no guard. *Cost if wrong:* in a two-box region a failed drain waits for the deadline and then for an operator, rather than returning to the source automatically, as 1b-next ruling 26 accepts. |
| 15. **Termination is drawn only where region HA owns the loss.** The sweep terminates a box only when the claim names it, if at all, as a serving executor, a relocation's participant or a chore's owner, and never a box holding a legacy host before its adoption. A participant of a move, landing, rollback, revert, push, create or delete is recovered from a lost box by moves' and the claim's declare-lost paths (L14), which the model walks for a stopped box, and a push never starts on a terminated executor. *Cost if wrong:* those paths are untested under termination here; the brief lists it under "After this plan". |
| -16. **Every prepared generation an operation built and no writer opened is parked in the serving CAS** (finding F3), with a scoped `park-generation` in the source region. *Cost if wrong:* if 1b-next leaves abandoned P builds to the at-rest sweep, the claim's INV-10 at the operation's end has to say so. |
| -17. **The sweep never terminates an executor none of whose files manifests has landed** (finding F2). `TestFailoverBeforeTheFirstManifest` keeps the loss visible. *Cost if wrong:* the gap is hidden from the sweep; the direct test still fails if the behaviour changes. |
| +16. **(Rev 3) Every unopened P is recorded when it is replaced or dropped, and parked at completion, mirroring 1b-next ruling 27 and rev 18 finding 3** (finding F3, closed). `abandonPrepared` journals it in `opState.Abandoned` (`abandoned_prepared`) on every path: install, the replacement table's nested branch, the nested relocation after `probe-failed`, and the operator's replay. The serving CAS queues a scoped `park-generation` for each one in the source region (rule `reloc-abandoned-prepared`). An opened P is part of the writer lineage and is never listed. This replaces rev 2's list of every built P. *Cost if wrong:* the model's at-rest sweep is the backstop, as it is in 1b-next. That is why the rule's mutation is an expected miss, shown by a direct test. |
| +17. **(Rev 3) A nonempty database pins only files that carry `instance.key`, mirroring 1b-next ruling 25 as rev 18 amended it, and the L21 window fails safe** (finding F2, closed). In the two-box shape, a pin for a holder with an admitted writer and a nonempty pinned database needs a pinned manifest that carries a live `instance.key`. With no manifest, or a keyless one (the pre-start copy of §5.6), the operation is stuck (rule `files-pin-needs-key`), and no operator replay accepts a keyless pin. The window between the app minting the key and the first keyed manifest landing is L21, still open. A host terminated inside it cannot be recovered by any relocation, so the sweep, which must converge, never terminates such an executor (`regionHAOwnsLoss`). The witness `files-pin-needs-key` and `TestFailoverBeforeTheFirstManifest` script the window. *Cost if wrong:* the sweep never meets the L21 refusal; the witness and the test do, and they fail if the refusal goes. |
| 18. **A one-box region inside the two-box shape is a witness world's** (`regionWorld(1)`, `oneBoxRegion`): region HA on, region 0 kept at one box by its group (H5's minimum is per region), regions 1 and 2 with two. The sweep's one-box shape has region HA off, so L18's one-box cases are direct tests, not seeds. *Cost if wrong:* a one-box-region interleaving the scenarios do not script is unexplored; the joint round may ask for a mixed sweep shape. |
| 19. **INV-28 is new: a timer is never declared lost while the manifest its box published last in that generation carries it.** It is the oracle for P's prepared manifest at sequence 0 (the seq order must be the publication order); it reads the issue order the model records in each manifest blob. *Cost if wrong:* a manifest landing out of order with a timer added and then removed would be a false positive; the timer would be delivered, and delivered timers are never declared. |
| @@ -119,7 +146,7 @@ Each was a gap or a conflict between the authorities. Each says what it costs if |
| 2. **The receipt after P opens.** A box whose install journal is gone after P's first admission must stop the operation, never admit again over a missing install, and never compare content the admitted writers changed. Expect `stuck`, then the operator's resolve. Task 2 `verifyReceipt`; Task 5 witness `reloc-verify-receipt`. |
| 3. **The exhausted fence while the source still executes.** Three targets die in `starting`; the source must keep `op.exec`, its phase and its release, and only `stuck` is new. Expect no second writer. Task 3 `fenceExhaustedTarget`; Task 5 witness `reloc-exhausted-fence`. |
| 4. **P's prepared manifest sequence.** The session publisher in P must sort after the prepared manifest, or a later pin takes stale files and timers. Expect seq 0 and INV-28 to hold. Task 4 `buildPreparedFiles`; Task 5 witness `files-prepared-seq-zero`. |
| -5. **The three findings.** F1 (no exit after a failed probe in a two-box region), F2 (a failover before the first manifest lands), F3 (abandoned P builds). Each has a direct test that reproduces the gap and a ruling that bounds it. Tell us if a ruling hides something the specs should fix instead. |
| +5. **The three findings, closed (rev 3).** F1, F2 and F3 are now mirrors of 1b-next rev 19's fixes, each with a mutation that reopens it. The L21 window is scripted (witness `files-pin-needs-key`): recovery must be stuck there and must never install a database without its key. Tell us if a mirror is weaker than its 1b-next guard. |
| ## File Structure |
| @@ -5259,9 +5286,555 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| --- |
| +### Task 5A: 1b-next rev 17 to 19's fixes for findings F1 to F3, and the L21 window (rev 3; 1b-next rulings 25 to 27, rev 18 findings 1 to 3, request L21) |
| + |
| +The model's stand-ins for findings F1 to F3 are replaced by mirrors of the fixes in 1b-next, and each gap gets a mutation check that reopens it. Each rule's comment names the 1b-next function it mirrors. |
| + |
| +| Rule | 1b-next rev 19 | What the model does | |
| +|---|---|---| |
| +| `files-pin-needs-key` | `Pin`'s `needKey`, `filesPin`'s `ErrFilesUnevidenced`, `liveEntry(InstanceKeyPath)` (ruling 25 as amended) | In the two-box shape, a pin for a nonempty database with an admitted writer needs a pinned manifest that carries `instance.key`. Otherwise it marks the operation `stuck`, and the operator's replay never overrides that. | |
| +| `reloc-no-spare-bound` | `Worker.Step` in `probe-failed` (ruling 26) | the existing bound, now a named guard | |
| +| `reloc-dead-target-bound` | `FenceTargetWithoutSpare`, `fenceTargetStuck` (rev 18 finding 2) | `replaceTarget` with no spare, `releaseDeadline` after the termination, consumes the fence into `stuck` (phase-sensitive, shared with `fenceExhaustedTarget`) | |
| +| `reloc-abandoned-prepared` | `abandonPrepared`, `abandoned_prepared`, `CompleteRelocation` (ruling 27, rev 18 finding 3) | every unopened P is recorded before it is replaced or dropped, on every path, and parked at serving; replaces rev 2's `Built` | |
| + |
| +The finding tests now pass because the gaps are closed (`TestFailoverBeforeTheFirstManifest`: stuck, nothing installed; `TestProbeFailedInATwoBoxRegion`: waits, then stuck, then the operator's resolve; `TestAbandonedPreparedGenerationParked`: both paths). Three new witnesses cover `files-pin-needs-key` (the L21 window, `wL21Window`), `reloc-no-spare-bound` and `reloc-dead-target-bound`. `regionHAOwnsLoss` now spares an executor whose newest landed manifest carries no key (ruling 17). |
| + |
| +**Files:** |
| +- Modify: `regionha_test.go` (`selectPin`, `pinnedManifestOf`, `manifestHasKey`, `abandonPrepared`, `handExec`, `relocationLeftovers`, `relocProbeFailed`, `replaceTarget`, `fenceExhaustedTarget`, `fenceTargetStuck`, `regionHAOwnsLoss`), `world_test.go` (`opState.Abandoned`), `console_test.go` (the operator's replay records an unopened P), `rules_test.go`, `witness_test.go` (three entries; `files-live-set` names INV-3), `regionha_witness_test.go` (`wL21Window`, `wNoSpareBound`, `wDeadTargetBound`), `regionha_cases_test.go` (the three finding tests, `dropPBeforeAdmission`) |
| + |
| +- [ ] **Step 1: Apply the patch** |
| + |
| +```diff |
| +diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go |
| +index 00a0dee..c2abe9b |
| +--- a/internal/sim/hostlife/console_test.go |
| ++++ b/internal/sim/hostlife/console_test.go |
| +@@ -1267,6 +1267,7 @@ func (w *world) operator() { |
| + n.Op.Stuck, n.Op.Phase, n.Op.FailedAt, n.Op.Release = "", "probe-failed", w.now, nil |
| + what = "sent its live target to probe-failed" |
| + default: |
| ++ w.abandonPrepared(n) |
| + n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true |
| + n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1 |
| + n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil |
| +diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go |
| +index 9a52eea..6086dcb |
| +--- a/internal/sim/hostlife/regionha_cases_test.go |
| ++++ b/internal/sim/hostlife/regionha_cases_test.go |
| +@@ -620,14 +620,16 @@ func TestOnlyTheExecutorInstalls(t *testing.T) { |
| + } |
| + } |
| + |
| +-// ---------- findings: hazards the model shows in 1b-next rev 16 ---------- |
| +- |
| +-// TestFailoverBeforeTheFirstManifest (finding F2): a host none of whose |
| +-// files manifests has landed is terminated; 1b-next pins its files as |
| +-// empty (StorePinner: "Empty for a host that never published files"), so |
| +-// the install mints a fresh instance.key over data sealed with the old |
| +-// one. The model reproduces it (INV-4); the sweep never terminates such |
| +-// an executor (model ruling 17). |
| ++// ---------- findings F1 to F3, closed by 1b-next rev 17 to 19 ---------- |
| ++ |
| ++// TestFailoverBeforeTheFirstManifest (finding F2, closed by 1b-next |
| ++// ruling 25 as rev 18 amended it): a host none of whose files manifests |
| ++// has landed is terminated. The pin refuses files that carry no |
| ++// instance.key for a nonempty database, the operation is stuck, and |
| ++// nothing is installed: no fresh key over sealed data. The database is |
| ++// unrecoverable by relocation (L21); the operator's replay never accepts |
| ++// the keyless pin. Under the mutation of files-pin-needs-key the install |
| ++// mints a fresh key (INV-4) and this test fails. |
| + func TestFailoverBeforeTheFirstManifest(t *testing.T) { |
| + w := twoBoxWitness() |
| + from := w.boxes[0] |
| +@@ -637,21 +639,24 @@ func TestFailoverBeforeTheFirstManifest(t *testing.T) { |
| + w.running(t, from) |
| + w.hold = nil |
| + w.terminate(from) |
| +- w.drive(400, func() bool { |
| +- return len(w.violations) > 0 || w.claim.Op.Kind == "serving" && w.claim.Op.Exec != from.ID |
| +- }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) |
| +- if len(w.violations) == 0 || !contains([]int{4}, invNumber(w.violations[0])) { |
| +- t.Fatalf("finding F2 no longer reproduces (want INV-4): %v", w.violations) |
| ++ w.drive(400, func() bool { return len(w.violations) > 0 }, w.actAll(), w.recoveryPass, w.wakeExec) |
| ++ w.mustHold(t) |
| ++ c := w.claim |
| ++ if c.Op.Kind != "relocating" || c.Op.Stuck == "" || c.Op.Pin != nil || c.Op.Prepared != "" { |
| ++ t.Fatalf("the failover did not stop at an unevidenced files pin: %s", w.state()) |
| ++ } |
| ++ if w.stats["pin: files unevidenced, no instance.key"] == 0 { |
| ++ t.Fatalf("the pin never refused: %v", w.stats) |
| + } |
| + } |
| + |
| +-// TestProbeFailedInATwoBoxRegion (finding F1): a drain's target cannot |
| +-// run the app; its probe fails and it releases. 1b-next's worker looks |
| +-// for a spare with no bound (Worker.Step: "no eligible box yet: a later |
| +-// pass may find one"), and replaceTargetSlot refuses the source, so in a |
| +-// two-box region the host serves nowhere until an operator acts. The |
| +-// model marks it stuck after the release deadline (model ruling 14) and |
| +-// the operator's resolve returns it to the source (model ruling 13). |
| ++// TestProbeFailedInATwoBoxRegion (finding F1, closed by 1b-next ruling |
| ++// 26): a drain's target cannot run the app; its probe fails and it |
| ++// releases. With no spare the worker waits, and ReleaseDeadline after |
| ++// probe_failed_since the operation is stuck; nothing names the source |
| ++// automatically. The operator's resolve returns the host to the source |
| ++// (plan ruling 13). Under the mutation of reloc-no-spare-bound the |
| ++// operation waits for ever (INV-3) and this test fails. |
| + func TestProbeFailedInATwoBoxRegion(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| +@@ -659,38 +664,66 @@ func TestProbeFailedInATwoBoxRegion(t *testing.T) { |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| ++ w.reach(t, 1500, "probe-failed with the target released", func() bool { |
| ++ c := w.claim |
| ++ return c.Op.Phase == "probe-failed" && c.Op.Release != nil && c.Op.Release.Box == to.ID |
| ++ }, w.actAll(), w.recoveryPass) |
| ++ w.drive(releaseDeadline/2, never, w.actAll(), w.recoveryPass) |
| ++ if c := w.claim; c.Op.Stuck != "" || c.Op.Tgt == from.ID { |
| ++ t.Fatalf("before the deadline the operation is stuck or names the source: %s", w.state()) |
| ++ } |
| + w.reach(t, 1500, "stuck with no spare", func() bool { return w.claim.Op.Stuck == "no eligible box for the nested relocation" }, w.actAll(), w.recoveryPass) |
| + w.servingOn(t, from) |
| + w.finish(t) |
| + w.mustHold(t) |
| + } |
| + |
| +-// TestAbandonedPreparedGenerationParked (finding F3): a target replaced |
| +-// at installing leaves its partial build of P behind (the replacement |
| +-// builds a fresh P'); 1b-next's CompleteRelocation queues park-local |
| +-// chores only. The model parks every unopened P in the serving CAS |
| +-// (model ruling 16); without it INV-10 finds P's objects at the release. |
| ++// TestAbandonedPreparedGenerationParked (finding F3, closed by 1b-next |
| ++// ruling 27 and rev 18 finding 3): an unopened P is recorded on every |
| ++// path that drops it and parked at completion. installing: the target |
| ++// is replaced at installing and the replacement builds P'. probe-failed: |
| ++// the probe deadline passes before any admission, the target is then |
| ++// terminated, and the replacement table's nested branch drops P. Under |
| ++// the mutation of reloc-abandoned-prepared INV-10 finds P's objects. |
| + func TestAbandonedPreparedGenerationParked(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) |
| +- third := w.extraBox(0, 30) |
| +- w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass) |
| +- p := w.claim.Op.Prepared |
| +- w.terminate(to) |
| +- w.reach(t, 100, "replaced", func() bool { return w.claim.Op.Exec == third.ID }, w.act(third)) |
| +- if w.claim.Op.Prepared == p { |
| +- t.Fatalf("the replacement at installing kept P") |
| ++ for _, path := range []string{"installing", "probe-failed"} { |
| ++ t.Run(path, func(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) |
| ++ third := w.extraBox(0, 30) |
| ++ w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass) |
| ++ p := w.claim.Op.Prepared |
| ++ if path == "probe-failed" { |
| ++ w.dropPBeforeAdmission(t, from, to) |
| ++ } else { |
| ++ w.terminate(to) |
| ++ } |
| ++ w.reach(t, 300, "P dropped", func() bool { return w.claim.Op.Prepared != p }, w.actAll(), w.recoveryPass) |
| ++ w.servingOn(t, third) |
| ++ if w.stats["relocation: abandoned prepared generation parked"] == 0 { |
| ++ t.Fatalf("the abandoned P %q was not parked at serving", p) |
| ++ } |
| ++ w.finish(t) |
| ++ w.mustHold(t) |
| ++ }) |
| + } |
| +- w.servingOn(t, third) |
| +- if w.stats["relocation: abandoned prepared generation parked"] == 0 { |
| +- t.Fatalf("the abandoned P %q was not parked at serving", p) |
| ++} |
| ++ |
| ++// dropPBeforeAdmission is rev 18 finding 3's trace: the target freezes |
| ++// in probing until the probe deadline passes with P unopened, the worker |
| ++// moves it to probe-failed, and it is terminated there. |
| ++func (w *world) dropPBeforeAdmission(t *testing.T, from, to *box) { |
| ++ w.reach(t, 1500, "probing", func() bool { return w.claim.Op.Phase == "probing" }, w.act(from, to), w.recoveryPass) |
| ++ to.Frozen = true |
| ++ w.reach(t, 3*probeDeadline, "probe-failed before any admission", func() bool { return w.claim.Op.Phase == "probe-failed" }, w.act(from), w.recoveryPass) |
| ++ if preparedOpened(w.claim) { |
| ++ t.Fatalf("P was opened") |
| + } |
| +- w.finish(t) |
| +- w.mustHold(t) |
| ++ w.terminate(to) |
| + } |
| + |
| + // invNumber is the n of the first "INV-n" in a violation, 0 if none. |
| +diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go |
| +index 47effbe..9d8e987 |
| +--- a/internal/sim/hostlife/regionha_test.go |
| ++++ b/internal/sim/hostlife/regionha_test.go |
| +@@ -243,9 +243,38 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry { |
| + } |
| + pin.ManKey, pin.ManVer, pin.ManSeq, pin.ManGen = mk, mv, ms, mg |
| + } |
| ++ // 1b-next ruling 25 as rev 18 amended it (finding F2; rule |
| ++ // files-pin-needs-key): when a writer was admitted and the pinned |
| ++ // database is nonempty, the pinned manifest must carry a live |
| ++ // instance.key, or the operation is stuck; no operator replay accepts |
| ++ // it, since a database is never installed without its key. The L21 |
| ++ // window (the app mints the key after it starts, and its first |
| ++ // manifest with the key has not landed) ends here. The mutation pins |
| ++ // what it found, rev 16's behaviour. Only the two-box shape has a |
| ++ // files publisher (ruling 11) |
| ++ if w.perRegion > 1 && on("files-pin-needs-key") && h.Session != 0 && n > 0 && !manifestHasKey(w.pinnedManifestOf(b.Region, pin)) { |
| ++ w.stats["pin: files unevidenced, no instance.key"]++ |
| ++ w.markStuck(c, fmt.Sprintf("the pinned files carry no instance.key for a nonempty database (TXID %d)", n)) |
| ++ return nil |
| ++ } |
| + return pin |
| + } |
| + |
| ++// pinnedManifestOf is the manifest pin names, read by version. |
| ++func (w *world) pinnedManifestOf(r int, pin *pinEntry) *blob { |
| ++ if pin.ManKey == "" { |
| ++ return nil |
| ++ } |
| ++ if v := w.buckets[r].byID(pin.ManKey, pin.ManVer); v != nil && !v.Marker { |
| ++ return v.B |
| ++ } |
| ++ return nil |
| ++} |
| ++ |
| ++// manifestHasKey: the manifest carries a live instance.key (InstanceKeyPath, |
| ++// liveEntry): its files directory names one. |
| ++func manifestHasKey(m *blob) bool { return m != nil && m.Files != nil && m.Files.Key != 0 } |
| ++ |
| + // restoreUpTo restores generation gen of region r from its current |
| + // listing, capped at TXID upto: the newest current snapshot at or below |
| + // upto as the root, then the planner's rule (ltx.IsContiguous, highest |
| +@@ -406,13 +435,13 @@ func (w *world) markStuck(c *claim, why string) { |
| + // source, when it is alive and its fence did not discharge it, and every |
| + // other box this operation handed op.exec to. |
| + func (w *world) relocationLeftovers(n *claim, op opState) { |
| +- // every prepared generation this operation built and no writer ever |
| +- // opened is a dead generation of holder.location: its remote build is |
| +- // retired by a park-generation queued here (model ruling 16; 1b-next's |
| +- // CompleteRelocation queues park-local chores only, and nothing else |
| +- // retires an abandoned P's objects before the at-rest sweep) |
| ++ // every prepared generation the operation abandoned unopened |
| ++ // (abandoned_prepared) is a dead generation of holder.location: its |
| ++ // remote build is retired by a park-generation queued here, beside the |
| ++ // park-local chores (1b-next ruling 27, CompleteRelocation; plan ruling |
| ++ // 16). An opened P is part of the writer lineage and never listed |
| + if h := n.Holder; h != nil { |
| +- for _, g := range op.Built { |
| ++ for _, g := range op.Abandoned { |
| + if g == h.Gen || w.ancestorGen(h.Location, h.Gen, g) { |
| + continue |
| + } |
| +@@ -581,12 +610,30 @@ func (w *world) relocPinning(b *box, c *claim) { |
| + } |
| + } |
| + |
| ++// abandonPrepared is abandonPrepared(c) in hostclaim (1b-next ruling |
| ++// 27, rev 18 finding 3): before an unopened P is replaced or dropped, it |
| ++// is journaled in abandoned_prepared, so the serving CAS parks it. Every |
| ++// path that replaces or drops P calls it: install, the replacement |
| ++// table's nested branch, the nested relocation after probe-failed and the |
| ++// operator's replay. The mutation of reloc-abandoned-prepared records |
| ++// nothing, which reopens finding F3. |
| ++func (w *world) abandonPrepared(n *claim) { |
| ++ p := n.Op.Prepared |
| ++ if p == "" || preparedOpened(n) || hasStr(n.Op.Abandoned, p) || !on("reloc-abandoned-prepared") { |
| ++ return |
| ++ } |
| ++ n.Op.Abandoned = append(n.Op.Abandoned, p) |
| ++} |
| ++ |
| + // handExec is install() in hostclaim: op.exec to box at phase with |
| + // prepared generation P, a new stamp (this CAS's), journaled as |
| + // install_stamp, no receipt, the probe attempts reset for the new |
| + // executor (BeginProbeAttempt counts per box), and the box noted as owing |
| + // a park-local should it be abandoned. |
| + func (w *world) handExec(n *claim, box int, phase, prepared string) { |
| ++ if prepared != n.Op.Prepared { |
| ++ w.abandonPrepared(n) // install replaces an unopened P (1b-next ruling 27) |
| ++ } |
| + n.Op.Exec, n.Op.Phase, n.Op.Prepared = box, phase, prepared |
| + n.Holder.Stamp = w.issueStamp(n, box) |
| + n.Op.InstallStamp = n.Holder.Stamp |
| +@@ -594,9 +641,6 @@ func (w *world) handExec(n *claim, box int, phase, prepared string) { |
| + n.Op.Receipt = nil |
| + } |
| + n.Op.Attempts = 0 |
| +- if prepared != "" && !hasStr(n.Op.Built, prepared) { |
| +- n.Op.Built = append(n.Op.Built, prepared) |
| +- } |
| + n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box) |
| + n.Boxes = addUniq(n.Boxes, box) |
| + } |
| +@@ -989,7 +1033,11 @@ func (w *world) relocProbeFailed(b *box, c *claim) { |
| + } |
| + next := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op, op.Exec)...) |
| + if next == nil { |
| +- if w.now > op.FailedAt+releaseDeadline { |
| ++ // 1b-next ruling 26 (rev 17, finding F1; rule reloc-no-spare-bound): |
| ++ // with no spare ReleaseDeadline after probe_failed_since, stuck; |
| ++ // never the source, which the operator's resolve alone may name. |
| ++ // The mutation waits for a spare for ever, rev 16's behaviour |
| ++ if on("reloc-no-spare-bound") && w.now > op.FailedAt+releaseDeadline { |
| + w.markStuck(c, "no eligible box for the nested relocation") |
| + } |
| + return |
| +@@ -1001,6 +1049,7 @@ func (w *world) relocProbeFailed(b *box, c *claim) { |
| + if !w.nameReplacement(n, next.ID, "pinning") { |
| + return n.Op.Stuck != "" // stuck: the CAS records it |
| + } |
| ++ w.abandonPrepared(n) |
| + n.Op.Exec = -1 |
| + n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil |
| + n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| +@@ -1181,13 +1230,15 @@ func (w *world) regionHAOwnsLoss(b *box) bool { |
| + switch c.Op.Kind { |
| + case "serving", "relocating": |
| + if c.Op.Exec == b.ID && w.perRegion > 1 { |
| +- // finding F2 (model ruling 17): an executor none of whose files |
| +- // manifests has landed (an adopted legacy host before its first |
| +- // publication, a new host before its first manifest lands) would |
| +- // fail over to a fresh instance.key; the sweep leaves it alone, |
| +- // and TestFailoverBeforeTheFirstManifest shows the loss |
| ++ // the L21 window (plan ruling 17): an executor whose newest |
| ++ // landed manifest carries no instance.key (none landed yet, or |
| ++ // only the pre-start copy) is unrecoverable by any relocation: |
| ++ // its failover is stuck by design (1b-next ruling 25) and never |
| ++ // converges, so the sweep leaves it alone; the witness for |
| ++ // files-pin-needs-key and TestFailoverBeforeTheFirstManifest |
| ++ // show it fail safe |
| + _, _, _, _, m := w.newestManifest(b.Region, c.Holder.Location, c.Holder.Gen) |
| +- return m != nil |
| ++ return manifestHasKey(m) |
| + } |
| + return true |
| + } |
| +@@ -1470,6 +1521,14 @@ func (w *world) replaceTarget(n *claim, x *box) bool { |
| + } |
| + next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...) |
| + if next == nil { |
| ++ if on("reloc-dead-target-bound") && w.now > x.TerminatedAt+releaseDeadline { |
| ++ // FenceTargetWithoutSpare (1b-next rev 18 finding 2): the fence |
| ++ // is consumed ReleaseDeadline after its observed_at and the |
| ++ // operation is stuck; the mutation waits for a spare for ever |
| ++ w.stats["relocation: dead target with no spare fenced"]++ |
| ++ w.fenceTargetStuck(n, x, fmt.Sprintf("box %d terminated and no spare in %d steps", x.ID, releaseDeadline)) |
| ++ return true |
| ++ } |
| + w.stats["relocation: target lost, no spare yet"]++ |
| + return false |
| + } |
| +@@ -1486,6 +1545,7 @@ func (w *world) replaceTarget(n *claim, x *box) bool { |
| + case !late || !on("reloc-replacement-table"): |
| + w.handExec(n, next.ID, "installed", n.Op.Prepared) // P was never opened: to' makes its own local install and opens it |
| + default: |
| ++ w.abandonPrepared(n) |
| + n.Op.Exec, n.Op.Phase = -1, "pinning" |
| + n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil |
| + n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| +@@ -1509,8 +1569,14 @@ func (w *world) replaceTarget(n *claim, x *box) bool { |
| + // mutation is rev 8's: always op.exec none at pinning, which revokes a |
| + // live source without its stop evidence. |
| + func (w *world) fenceExhaustedTarget(n *claim, x *box) { |
| +- why := fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements) |
| + w.stats["relocation: exhausted target fenced"]++ |
| ++ w.fenceTargetStuck(n, x, fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements)) |
| ++} |
| ++ |
| ++// fenceTargetStuck is 1b-next's fenceTargetStuck, the body |
| ++// FenceExhaustedTarget and FenceTargetWithoutSpare share (rev 18): phase |
| ++// sensitive as above; an unopened P is kept for the operator. |
| ++func (w *world) fenceTargetStuck(n *claim, x *box, why string) { |
| + if on("reloc-exhausted-fence") && n.Op.Exec >= 0 && n.Op.Exec != x.ID { |
| + n.Op.Stuck = why |
| + return |
| +diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go |
| +index 2b90792..2523a7f |
| +--- a/internal/sim/hostlife/regionha_witness_test.go |
| ++++ b/internal/sim/hostlife/regionha_witness_test.go |
| +@@ -751,3 +751,74 @@ func wRelocPinEvidencedEmpty(t *testing.T, w *world) { |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| + } |
| ++ |
| ++// rev 3: 1b-next rev 17 to 19's fixes for findings F1 to F3, and L21 |
| ++ |
| ++// wL21Window (files-pin-needs-key): the L21 window, explicit. The cold |
| ++// admission's pre-start manifest copy has landed without instance.key |
| ++// (§5.6 copies the manifest before the app starts); the app minted the |
| ++// key after it started, wrote rows sealed with it and replicated them; |
| ++// the publisher's manifest carrying the key has not landed when the box |
| ++// is terminated. Recovery fails safe: the pin refuses, the operation is |
| ++// stuck, and no database is installed without its key. Without the rule |
| ++// the keyless manifest is pinned and the install mints a fresh key over |
| ++// the sealed rows (INV-4). |
| ++func wL21Window(t *testing.T, w *world) { |
| ++ w.twoBox() |
| ++ from := w.boxes[0] |
| ++ w.serve(from, 1, app0) |
| ++ h := w.claim.Holder |
| ++ w.issued++ |
| ++ pre := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: 1, Base: w.issued} // the pre-start copy: no files, no key |
| ++ k := manifestKey(h.Location, h.Gen, 1) |
| ++ w.buckets[0].objs[k] = []*version{{ID: w.newVer(), B: pre}} |
| ++ from.pubGen, from.pubSeq = h.Gen, 1 |
| ++ w.holdKey(h.Location + "files/") // the manifest with the key never lands |
| ++ w.running(t, from) |
| ++ w.appWrite(from) |
| ++ w.replicate(from) |
| ++ w.drive(30, never, w.act(from)) // the rows' uploads land; the manifest stays held |
| ++ w.terminate(from) |
| ++ w.drive(400, func() bool { return len(w.violations) > 0 || w.claim.Op.Stuck != "" }, w.actAll(), w.recoveryPass, w.wakeExec) |
| ++ if len(w.violations) == 0 { |
| ++ if c := w.claim; c.Op.Stuck == "" || c.Op.Prepared != "" { |
| ++ w.violate("INV-3 (witness): the L21 failover neither stopped nor installed: %s", w.state()) |
| ++ } |
| ++ } |
| ++} |
| ++ |
| ++// wNoSpareBound (reloc-no-spare-bound, F1): a drain's target fails its |
| ++// probe in a two-box region; with the bound the operation is stuck and |
| ++// the operator returns the host to the source; without it, it waits. |
| ++func wNoSpareBound(t *testing.T, w *world) { |
| ++ w.twoBox() |
| ++ from, to := w.boxes[0], w.boxes[3] |
| ++ to.FailApp = true |
| ++ w.serve(from, 1, app0) |
| ++ w.running(t, from) |
| ++ w.drainTo(t, to) |
| ++ w.servingOn(t, from) |
| ++ w.finish(t) |
| ++} |
| ++ |
| ++// wDeadTargetBound (reloc-dead-target-bound, rev 18 finding 2): the |
| ++// drain's target is terminated at installing and the group launches no |
| ++// replacement (region 0 kept at one box: a capacity shortage), so no |
| ++// spare exists. With the bound the fence is consumed ReleaseDeadline |
| ++// later, the operation is stuck, and the operator's replay serves the |
| ++// host on the source; without it nothing moves. |
| ++func wDeadTargetBound(t *testing.T, w *world) { |
| ++ w.twoBox() |
| ++ 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.oneBoxRegion[0] = true |
| ++ if !w.relocPhase(t, "installing", w.act(from, to), w.recoveryPass) { |
| ++ return |
| ++ } |
| ++ w.terminate(to) |
| ++ w.servingOn(t, from) |
| ++ w.finish(t) |
| ++} |
| +diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go |
| +index ac25284..7af7a80 |
| +--- a/internal/sim/hostlife/rules_test.go |
| ++++ b/internal/sim/hostlife/rules_test.go |
| +@@ -181,4 +181,9 @@ var allRules = []string{ |
| + "files-pin-exact", // region HA §5.8 the pinned recovery set, B2-4 (RecoveryPin.FilesManifest, StorePinner, ruling 21's retained copy): the local install applies the manifest version the pin names; the mutation reads the newest at install time. A determinism rule: a later PUT adds a version nothing reads (expected miss) |
| + "files-live-set", // region HA §5.6, L13, claim §6.2a (the classifier's files live set, 1b-next rev 12 finding 1's referenced origins): a park-generation never archives the live manifest of the chain, holder.generation's, P's or the pinned one; the mutation archives them with their dead generation |
| + "files-prepared-seq-zero", // claim rev 6.30 R18-1, moves rev 7.22 §7.6, 1b-next rev 15 finding 1 (CopyPinnedManifest, PreparedAuthority.FilesSeq 0): P's prepared manifest is at sequence 0 and the session publisher starts at 1; the mutation keeps the source's sequence, so a later pin takes the stale prepared manifest over the session's (INV-28) |
| ++ // plan 1b-next rev 17 to 19's fixes for the model's findings F1 to F3 (rev 3 of this plan) |
| ++ "reloc-no-spare-bound", // 1b-next ruling 26 (rev 17, F1): probe-failed with no eligible spare is stuck ReleaseDeadline after probe_failed_since, never sent to the source; the mutation waits for ever (INV-3) |
| ++ "reloc-dead-target-bound", // 1b-next rev 18 finding 2 (FenceTargetWithoutSpare): a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at; the mutation waits for ever (INV-3) |
| ++ "reloc-abandoned-prepared", // 1b-next ruling 27, rev 18 finding 3 (abandonPrepared, abandoned_prepared): every unopened P that is replaced or dropped, on every path, is parked at completion; the mutation records none (INV-10) |
| ++ "files-pin-needs-key", // 1b-next ruling 25 as rev 18 amended it (F2, L21): a nonempty database with an admitted writer pins only a manifest carrying instance.key, else stuck; the mutation pins it keyless and the install mints a fresh key (INV-4) |
| + } |
| +diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go |
| +index 34544e7..5b7fa77 |
| +--- a/internal/sim/hostlife/witness_test.go |
| ++++ b/internal/sim/hostlife/witness_test.go |
| +@@ -218,8 +218,8 @@ var witnesses = []witness{ |
| + "the executor registers a timer whose manifest never lands and is terminated; the fence drops the timer silently", wFenceDeclaresTimers}, |
| + {"reloc-enrolled-only", "reloc-enrolled-only", "INV-27", |
| + "the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly}, |
| +- {"files-live-set", "files-live-set", "INV-4", |
| +- "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover's install starts over data sealed with a key no manifest carries", wFilesLiveSet}, |
| ++ {"files-live-set", "files-live-set", "INV-3", |
| ++ "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover finds no manifest carrying instance.key: stuck, never served (rev 3: 1b-next ruling 25 makes the loss fail safe; with files-pin-needs-key also gone it is INV-4)", wFilesLiveSet}, |
| + {"reloc-pin-claim-gen", "reloc-pin-claim-gen", "INV-3", |
| + "a pinner observed the first round after the source's release and stalled; after the target wrote into P and died, its stale selection of generation_from is journaled for the nested pinning, and the build waits forever for objects generation_from's own park retired", wRelocPinClaimGen}, |
| + {"reloc-release-deadline", "reloc-release-deadline", "INV-3", |
| +@@ -240,6 +240,13 @@ var witnesses = []witness{ |
| + "a failover whose listing finds nothing although the writes are durable: with the rule the operation is stuck until an operator resolves it on a listing that shows them; without it the pin is empty and the install loses the durable writes", wRelocPinEvidencedEmpty}, |
| + {"files-prepared-seq-zero", "files-prepared-seq-zero", "INV-28", |
| + "the source's manifests reach sequence 3; P's prepared manifest keeps 3, the probe session publishes its timer at 1, and the nested failover pins and declares from the stale prepared manifest", wFilesPreparedSeqZero}, |
| ++ // rev 3: 1b-next rev 17 to 19's fixes for the model's findings, and the L21 window |
| ++ {"files-pin-needs-key", "files-pin-needs-key", "INV-4", |
| ++ "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window}, |
| ++ {"reloc-no-spare-bound", "reloc-no-spare-bound", "INV-3", |
| ++ "F1: a drain's target fails its probe in a two-box region with no spare; with the bound the operation is stuck and the operator's resolve returns the host to the source, without it it waits for ever", wNoSpareBound}, |
| ++ {"reloc-dead-target-bound", "reloc-dead-target-bound", "INV-3", |
| ++ "rev 18 finding 2: the target dies at installing and no spare is launched; with the bound the fence is consumed into stuck and the operator's replay serves on the source, without it nothing moves", wDeadTargetBound}, |
| + } |
| + |
| + // TestWitnesses is the deterministic half of the mutation evidence. |
| +diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go |
| +index 19ce89d..cfb51f7 |
| +--- a/internal/sim/hostlife/world_test.go |
| ++++ b/internal/sim/hostlife/world_test.go |
| +@@ -826,7 +826,7 @@ type opState struct { |
| + Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19) |
| + PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1) |
| + Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted |
| +- Built []string // every prepared generation this operation built: one no writer opened is parked at serving (model ruling 16) |
| ++ Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27) |
| + |
| + // journal |
| + ReportAt int |
| +@@ -1221,7 +1221,7 @@ func (c *claim) clone() *claim { |
| + n.Op.Excluded = append([]int(nil), c.Op.Excluded...) |
| + n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...) |
| + n.Op.Discharged = append([]int(nil), c.Op.Discharged...) |
| +- n.Op.Built = append([]string(nil), c.Op.Built...) |
| ++ n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...) |
| + if r := c.Op.Release; r != nil { |
| + cp := *r |
| + cp.Files = r.Files.clone() |
| +``` |
| + |
| +- [ ] **Step 2: Run the gate, the new witnesses, and the finding tests under their mutations** |
| + |
| +```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/task5a.log | grep -E "seeds, |^--- FAIL|^ --- FAIL|^ok|^FAIL" |
| +diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5a.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL |
| +for r in files-pin-needs-key reloc-no-spare-bound reloc-dead-target-bound files-live-set; do |
| + HOSTLIFE_WITNESS=$r nice -n 19 go test ./internal/sim/hostlife/ -run '^TestWitnesses$' -count=1 -v 2>&1 | grep -E "witness .* under" | sed 's/^ *witness_test.go:[0-9]*: //' | cut -c1-160 |
| +done |
| +for pair in files-pin-needs-key:TestFailoverBeforeTheFirstManifest reloc-no-spare-bound:TestProbeFailedInATwoBoxRegion reloc-abandoned-prepared:TestAbandonedPreparedGenerationParked; do |
| + HOSTLIFE_MUTATE=${pair%%:*} nice -n 19 go test ./internal/sim/hostlife/ -run "^${pair#*:}\$" -count=1 2>&1 | grep -E '^(ok|FAIL|--- FAIL)' | head -1 | sed "s/^/${pair%%:*}: /" |
| +done |
| +``` |
| + |
| +Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 480 completed operations; mutated="" boxes=2`; `ok`; `ONE-BOX-COUNTERS-IDENTICAL`. Witnesses: `files-pin-needs-key` held, then `violated: ... INV-4: ... instance.key ... over data sealed with ...`; `reloc-no-spare-bound` and `reloc-dead-target-bound` held, then `violated: ... INV-3 (witness): serving on the new executor not reached`; `files-live-set` held, then `violated: ... INV-3`. Every finding test line is `--- FAIL`: each mutation reopens its gap. |
| + |
| +- [ ] **Step 3: Commit** |
| + |
| +```bash |
| +git add internal/sim/hostlife/ |
| +git commit -m "sim: plan 1b-next rev 19's fixes for the model's findings: a nonempty database pins only files that carry instance.key (the L21 window fails safe), probe-failed and a dead target with no spare go stuck after the deadline with the fence consumed, and every unopened P is recorded on every path and parked at completion |
| + |
| +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 33 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 15 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 37 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 16 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` |
| @@ -5270,10 +5843,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..0db8d08 100644 |
| +index 72504e3..9e372fb |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| -@@ -21,3 +21,18 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| +@@ -21,3 +21,19 @@ 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) |
| @@ -5292,8 +5865,9 @@ index 72504e3..0db8d08 100644 |
| +fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation |
| +reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover) |
| +files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads, and the fence declares what no landed manifest carries; TestL18LateFileUploads shows the pinned version applied |
| ++reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation |
| diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh |
| -index c583d97..883996e 100755 |
| +index c583d97..883996e |
| --- a/internal/sim/hostlife/mutate.sh |
| +++ b/internal/sim/hostlife/mutate.sh |
| @@ -9,6 +9,9 @@ |
| @@ -5406,11 +5980,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`, `33`, `141`, `ok`. |
| +Expected (the dry run's): `SYNTAX-OK`, `37`, `145`, `ok`. |
| - [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)** |
| -Run only when Tasks 1 to 5 are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| +Run only when Tasks 1 to 5A are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| ```bash |
| export GOFLAGS=-buildvcs=false |
| @@ -5418,7 +5992,7 @@ mkdir -p $TMPDIR/hostlife-sim && nice -n 19 go test -c -o $TMPDIR/hostlife-sim/h |
| HOSTLIFE_BOXES=2 HOSTLIFE_PAR=2 nice -n 19 internal/sim/hostlife/mutate.sh 3000 2>&1 | tee $TMPDIR/twobox/sweep-two-box-3000.log |
| ``` |
| -Expected: exit 0; every rule `CAUGHT` or `EXPECTED-MISS`, none `MISSED`, `STALE` or `ERROR`, every verdict tagged `[boxes=2]`. Each of the 20 witnessed region HA rules is `CAUGHT` with `witness violated` (the two combinations, `reloc-install-receipt` and `reloc-row-cases`, are listed `missed` and report `EXPECTED-MISS ... witness held` alone); the two-box sweep may also catch one-box rules it did not before (a wider catch is fine). A `STALE` region HA rule means the sweep caught what this plan says it cannot: read the seed, and either move the rule to a witness or correct the reason. Record the verdict lines for Task 7. Do not rerun the whole sweep for one fix: a rule that needs rework reruns alone (`HOSTLIFE_BOXES=2 HOSTLIFE_PAR=1 nice -n 19 internal/sim/hostlife/mutate.sh 3000 <rule>`), or the region HA rules together (`... mutate.sh 3000 @regionha`). The one-box sweep is not rerun this revision (ruling 2). No 30,000-seed run. |
| +Expected: exit 0; every rule `CAUGHT` or `EXPECTED-MISS`, none `MISSED`, `STALE` or `ERROR`, every verdict tagged `[boxes=2]`. Each of the 23 witnessed region HA rules is `CAUGHT` with `witness violated` (the two combinations, `reloc-install-receipt` and `reloc-row-cases`, are listed `missed` and report `EXPECTED-MISS ... witness held` alone); the two-box sweep may also catch one-box rules it did not before (a wider catch is fine). A `STALE` region HA rule means the sweep caught what this plan says it cannot: read the seed, and either move the rule to a witness or correct the reason. Record the verdict lines for Task 7. Do not rerun the whole sweep for one fix: a rule that needs rework reruns alone (`HOSTLIFE_BOXES=2 HOSTLIFE_PAR=1 nice -n 19 internal/sim/hostlife/mutate.sh 3000 <rule>`), or the region HA rules together (`... mutate.sh 3000 @regionha`). The one-box sweep is not rerun this revision (ruling 2). No 30,000-seed run. |
| Afterwards: `rm -rf $TMPDIR/hostlife-sim`. |
| @@ -5433,14 +6007,14 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| --- |
| -### Task 7: The joint-round brief (against 1b-next rev 16) |
| +### Task 7: The joint-round brief (against 1b-next rev 19) |
| **Files:** |
| - Create: `docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md` |
| - [ ] **Step 1: Write the brief** |
| -The brief is for Astra (the independent second reader) and for the claim and moves sessions, who review the model together against 1b-next rev 16. It follows the shape of `CODEX-PLAN-REGION-HA-1BN-BRIEF-16.md` (on `origin/plan-region-ha-1b-next`): what to review, the authorities, what is fixed, what to check, the output wanted. Its content is this plan's evidence, so it is written last, from the logs in `$TMPDIR/twobox/`: |
| +The brief is for Astra (the independent second reader) and for the claim and moves sessions, who review the model together against 1b-next rev 19. It follows the shape of the latest `CODEX-PLAN-REGION-HA-1BN-BRIEF-*.md` (on `origin/plan-region-ha-1b-next`): what to review, the authorities, what is fixed, what to check, the output wanted. Its content is this plan's evidence, so it is written last, from the logs in `$TMPDIR/twobox/`: |
| ```markdown |
| # Review brief: the joint model with two boxes per region (L18), round 1 |
| @@ -5448,24 +6022,24 @@ The brief is for Astra (the independent second reader) and for the claim and mov |
| You are an independent second reader, reviewing with the claim and moves |
| sessions. Review `internal/sim/hostlife` at the commit named in the |
| prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| -16, which Astra's round 16 accepted as "stage A ready to build": |
| +19, which Astra's round 18 accepted as "stage A ready to build": |
| -- plan 1b-next rev 16 `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (rulings 1 to 24; the dispositions of revs 2 to 16; Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's gate) and its findings `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R16.md`; |
| +- plan 1b-next rev 19 `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (rulings 1 to 27; the dispositions of revs 2 to 19, rev 17's for this model's findings F1 to F3; request L21; Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's gate) and its findings `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R18.md`; |
| - 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 2 (its rulings 1 to 19 and its findings F1 to F3). |
| +- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 3 (its rulings 1 to 19; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3). |
| ## Fixed: do not re-argue |
| -- H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate, 1b-next rev 16's rulings 1 to 24 as Astra read them. |
| +- H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate, 1b-next rev 19's rulings 1 to 27 as Astra read them; L21 is open and Paul's. |
| - The one-box shape is the baseline: its 300-seed COUNTERS line is byte-identical to rev 7.22's after every task (`<paste the line>`), so every one-box verdict of rev 7.22 stands (ruling 2 states the converted-move caveat). |
| - The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul. |
| - The model's abstractions, as moves §14.2 lists them, plus this round's: a failover enters at `pinning` with the D6 barrier at the installing CAS (ruling 4); the stale edges file is the former executor's row (ruling 9); volume evidence is one flag per box (ruling 10); the files publisher runs in the two-box shape and a dead box's disk is never read there (ruling 11); a manifest carries its files as content, so 1b-next's object origins are the chain's newest manifest; the stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10) has no model step. |
| ## The guards, mapped |
| -| Model rule | 1b-next rev 16 | Finding | Spec | Evidence | |
| +| Model rule | 1b-next rev 19 | Finding | Spec | Evidence | |
| |---|---|---|---|---| |
| | create-choice-once | `BeginCreateOn`, `CompleteCreate` never substitutes | R9-2 | §5.2, P5-D2, P5-D6 | expected miss; `TestCreateNamesItsExecutorOnce` | |
| | reloc-start-guard | `RelocationStartGuard` | | §5.8, L11 | expected miss; `TestRelocationStartGuardRefuses` | |
| @@ -5500,23 +6074,25 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| | files-pin-exact | `RecoveryPin.FilesManifest`, retained copy | R1-5 (ruling 21) | §5.8, B2-4 | expected miss (determinism); `TestL18LateFileUploads` | |
| | files-live-set | the files live set, `referencedOrigins` | R11-1 (rev 12) | §5.6, L13, §6.2a | witness INV-4 | |
| | files-prepared-seq-zero | `CopyPinnedManifest`, `PreparedAuthority` | R14-1 (rev 15) | R18-1, moves §7.6 | witness INV-28 | |
| +| files-pin-needs-key | `Pin`'s `needKey`, `filesPin`'s `ErrFilesUnevidenced` (ruling 25) | model F2, R17-1 (rev 18) | H6, §5.6, L21 | witness INV-4 (the L21 window); `TestFailoverBeforeTheFirstManifest` | |
| +| reloc-no-spare-bound | `Worker.Step` in `probe-failed` (ruling 26) | model F1 (rev 17) | §5.8 | witness INV-3; `TestProbeFailedInATwoBoxRegion` | |
| +| reloc-dead-target-bound | `FenceTargetWithoutSpare`, `fenceTargetStuck` | R17-2 (rev 18) | §5.8 | witness INV-3 | |
| +| reloc-abandoned-prepared | `abandonPrepared`, `abandoned_prepared`, `CompleteRelocation` (ruling 27) | model F3 (rev 17), R17-3 (rev 18) | §5.8 | expected miss (the at-rest sweep backstops); `TestAbandonedPreparedGenerationParked` | |
| -## Findings the model raises against 1b-next rev 16 |
| +## Findings F1 to F3, closed, and the open window L21 |
| -- **F1.** In a two-box region a drain whose target fails its probe has no exit: `replaceTargetSlot` refuses the source and `Worker.Step` waits in `probe-failed` with no bound. The model marks it stuck after the release deadline and lets the operator's resolve name the source (plan rulings 13, 14; `TestProbeFailedInATwoBoxRegion`). Is a bounded wait and the source as an operator-only spare what the claim wants, or should `probe-failed` return to the released source itself? |
| -- **F2.** A failover before the host's first files manifest lands pins empty files and mints a fresh `instance.key` over sealed data (INV-4; `TestFailoverBeforeTheFirstManifest`). The sweep avoids it (plan ruling 17). Should adoption and creation publish platform files before region HA may fail a host over, or should the pin refuse a host whose database has data and whose files never landed? |
| -- **F3.** An abandoned prepared generation's remote build is never retired by the operation (`CompleteRelocation` queues park-local only). The model parks it in the serving CAS (plan ruling 16; `TestAbandonedPreparedGenerationParked`). Should 1b-next do the same, or should the claim's INV-10 at an operation's end exempt it for the at-rest sweep? |
| +The model's rev 2 raised F1 (no exit after a failed probe in a two-box region), F2 (a failover before the first files manifest lands mints a fresh `instance.key`) and F3 (an abandoned P never retired by its operation). 1b-next rev 17 to 19 closed them (rulings 25 to 27, rev 18 findings 1 to 3). The model now mirrors each fix. A mutation reopens each gap, and the finding tests pass because the gaps are closed. Check that each mirror is as strong as its guard. L21 stays open: the witness `files-pin-needs-key` scripts the window (a keyless pre-start manifest, a key minted after the start, rows sealed with it and replicated, the box terminated before the keyed manifest lands) and requires recovery to be stuck, never to install the database without its key. Say whether the model's window is the one L21 describes, and whether either candidate contract (pre-provisioning the key, or the replicator holding its first upload) would let the model drop plan ruling 17's restriction on the sweep. |
| ## Results |
| - Gate: `<the two summary lines, the witness count, the direct tests>`. |
| - Two-box 3,000-seed sweep: `<every verdict line from $TMPDIR/twobox/sweep-two-box-3000.log>`. |
| -- Findings the model made while being built, beyond F1 to F3: `<each seed or witness that violated with the rules on, what it showed, and whether the model or a spec was changed; "none" if none>`. |
| +- Findings the model made while being built, beyond F1 to F3 (rev 3 found none in 1b-next rev 19): `<each seed or witness that violated with the rules on, what it showed, and whether the model or a spec was changed; "none" if none>`. |
| ## What to check |
| 1. Each witness forces the interleaving its rule exists for, and nothing else fails under its mutation (the named failure is the first violation). Each direct test of a bound fails under its mutation. |
| -2. The phase table as modelled against 1b-next rev 16 Task 1: every CAS's conditions, what each phase admits, who may act; the barrier on every phase change; `MarkStuck`'s refusal between `installed` and a probe. |
| +2. The phase table as modelled against 1b-next rev 19 Task 1: every CAS's conditions, what each phase admits, who may act; the barrier on every phase change; `MarkStuck`'s refusal between `installed` and a probe. |
| 3. The release sequence's steps, its deadline, `released` coverage's binding to the flushed release, and a release whose session's replicator was gone (`Flushed` false: it declares). |
| 4. The pin: the generation `pinSource` selects against `genselect.Select`, the claim-version binding against `RecoveryPinKey`, evidenced emptiness against 1b-next ruling 15, the files pin against B2-4. |
| 5. EnsureLocal and VerifyReceipt against rev 15 and rev 16: the scoped cleanup that retires an unopened install (here: an execution lease that expired before its renewal), the restore under the same stamp, the receipt check after P opens, and that nothing compares content the admitted writers changed. |
| @@ -5525,7 +6101,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| 8. The files publisher, P's prepared manifest at sequence 0, INV-28, and the files live set against L13 and rev 12's referenced origins. |
| 9. The one-box region (ruling 18): is a witness world with region 0 held at one box a faithful stand-in for a region HA region of one box, or does the round want a mixed sweep shape? |
| 10. The expected misses: is each reason right, or is there an invariant the model should check? |
| -11. The plan's rulings 13 to 19 and findings F1 to F3: accept each, or say why it is wrong. |
| +11. The plan's rulings 13 to 19 (14, 16 and 17 as rev 3 rewrote them to mirror 1b-next rulings 26, 27 and 25): accept each, or say why it is wrong. |
| 12. Dormancy: anything in the two-box code that changes a one-box outcome (the COUNTERS line says no; check the reasoning, ruling 1, and ruling 2's caveat on the converted move). |
| ## Output |
| @@ -5539,7 +6115,7 @@ Fill every `<...>` from the logs; none may remain. |
| ```bash |
| git add docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md |
| -git commit -m "docs: the joint-round brief for the two-box model (L18) against plan 1b-next rev 16, round 1 |
| +git commit -m "docs: the joint-round brief for the two-box model (L18) against plan 1b-next rev 19, round 1 |
| Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| rm -rf $TMPDIR/twobox $TMPDIR/hostlife-sim |
| @@ -5558,14 +6134,14 @@ Then hand the brief to the Codex second reader as memory `codex-second-reader.md |
| | Claim D4's loss record materialized by the console from a fence (R5) | the console's claim-recovery pass | |
| | Termination of a move's, landing's, rollback's, push's, create's or delete's participant | moves' and the claim's declare-lost paths under termination; plan ruling 15 keeps the sweep off them | |
| | A mixed sweep shape (one-box and two-box regions in one world) | the joint round's answer to What to check 9 (plan ruling 18) | |
| -| F1 to F3's resolutions | the joint round; then a rev 3 of this plan and of 1b-next | |
| +| L21's durability contract (pre-provisioned `instance.key`, or the replicator holding its first upload) | Paul; then plan ruling 17's sweep restriction can go | |
| | Stage B's integration (6b's wake, stop and reconcile assemblies; moves Plans 1 and 2) | 1b-next's stage B re-plan; no model step | |
| | The one-box mutation sweep at 3,000 seeds on this revision | the next revision's sweep, or Paul's say-so (ruling 2) | |
| | 30,000-seed baselines of either shape | Paul's say-so | |
| ## Self-review |
| -- **1b-next rev 16 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 33 rules); 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, 37 rules; rev 3 added four for rev 17 to 19); 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 the existing `fence-converts-moving` witness. §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. |