carlos / platform Public

docs: the two-box brief names model commit db4b2a09 and states the final review's fix wave: the 151261fe mirror by region, park-evidence-every-box and its witness, and the one release-and-journal helper

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Paul Campbell pushed by claude 2 weeks ago 10ac836d5461a4f6516a01dbe71b9ee415258284 parent db4b2a0

1 file changed, +23 −8

docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md +23 −8

CI passed — run details

diff --git a/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md

index 6f74dc28f..97ac6dead 100644

--- a/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md

+++ b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md

@@ -1,10 +1,10 @@

# Review brief: the joint model with two boxes per region (L18), round 1

You are an independent second reader, reviewing with the claim and moves

-sessions. Review `internal/sim/hostlife` at commit 9ef58e4b on branch

-`region-ha-two-box-build` (the model; its code has not changed since

-cf566b41, and the sim commits after that touch only the expectation files and

-`mutate.sh`; the commits after 9ef58e4b add this brief and a diagnosis note) against plan 1b-next rev

+sessions. Review `internal/sim/hostlife` at commit db4b2a09 on branch

+`region-ha-two-box-build` (the model; its code last changed in the final

+review's fix wave, 04c9487d to db4b2a09, item 4 under "Changes made while

+building"; the commits after db4b2a09 update this brief) against plan 1b-next rev

19, which Astra's round 18 accepted as "stage A ready to build":

- 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`;

@@ -18,7 +18,7 @@ cf566b41, and the sim commits after that touch only the expectation files and

- 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, a create-interruption trace and the trace hash of every one of its 300 seeds are byte-identical to rev 7.22's after every task (the line is below), so every one-box verdict of rev 7.22 stands (ruling 2 states the converted-move caveat).

- The COUNTERS line at 5766a0e1, equal to the baseline:

+ The COUNTERS line at 5766a0e1, equal to the baseline (and unchanged at db4b2a09):

`{"abandoned empty generation skipped":1,"abort":106,"admission: no predecessor writer, nothing declared":78,"admissions born covered: warm":62,"admissions born covered: whole-location park pending":1,"admissions covered at the commit park":2,"admissions covered: clean-return":2,"admissions covered: sealed":45,"admissions: cold":226,"admissions: warm":62,"app stopped: its session's agent is gone":4,"clean close refused: a process still runs":15,"clean close refused: start unfinished or agent gone":1,"clean close refused: uncertain":3,"clean close: certificate not acknowledged":1,"clean closes":69,"completed beyond H":134,"create restarted on 412":32,"declared-lost":2,"diag: staging newer than seal at install":2,"disk-lost":6,"disk-lost with the crash":15,"final: recovery admission run":25,"first uploads":92,"free after park":115,"freed":284,"holderless sweeps":115,"idle stop before replication opened":8,"local database purged":192,"ltx compactions":30,"ltx upload retries":1,"marker republished":1,"move-done":2,"open: PUT retried":4,"open: abandoned":4,"open: marker PUT retried":70,"open: waits for its first":35,"open: waits for the marker":310,"park scope bound":1520,"probe restarted":11,"publish: predecessor empty everywhere":78,"publish: predecessor left to its region":2,"purge failed: writer not started":12,"purge failures injected":520,"push":84,"replication opened":277,"replication refused: the session's agent is gone":1280,"restore anchors":100,"revert":2,"rollback-clean":3,"rollback: source database lost":1,"snapshot rotations":17,"stale signature refused":104,"stamp records lost":74,"start: environment not ready":467,"wake waited for a clean close":4,"why: configuration changed during the move @config":2,"why: cut deadline @local":1,"why: declared lost @probing":1,"why: landing deadline @checking":1,"writes declared lost":26,"writes_lost declared":105,"writes_lost: another session of a lost target":4,"writes_lost: the legacy identity (session 0)":30}`

@@ -83,17 +83,19 @@ cf566b41, and the sim commits after that touch only the expectation files and

| reloc-release-needs-flush | Task 7 `Release`, `releaseDrain`, `relocationFlushDB`, `ReleaseFlushFiles`, `ReleasePositions` | two-box R6 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheFlush`, `TestReleaseReplaysTheRecordedFlush` |

| reloc-release-needs-receipt | Task 7 `Release`, `RecoveryReleaseDrain`, `ReleasePositions.Recorded` | two-box R8 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheReceipt`, `TestOperatorStopsATargetWithNoReceipt` |

## Changes made while building

-Three things changed or arrived after the plan's rev 11 was accepted. Read the first two as part of the model under review. The third is a request about 1b-next.

+Four things changed or arrived after the plan's rev 11 was accepted. Read the first, second and fourth as part of the model under review. The third is a request about 1b-next.

Readers read the code in two local worktrees, by path, not from a remote. The model is in `/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build` (branch `region-ha-two-box-build`). The 1b-next stage A build is in `/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-1b-next-build` (branch `region-ha-1b-next-build`).

**1. Two-box model fixes after the 3,000-seed sweep (cf566b41).** The first sweep was void: the unmutated two-box model failed INV-10 on seeds 819, 1674, 2106 and 2627, which hid 19 of the 28 stale readings. The one-box shape and the 300-seed gate never reach those seeds. The diagnosis is committed as `docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md` (it covers the first two causes, and its follow-ups cover the third). cf566b41 fixes three causes:

- INV-10 has a `SweepOwed` exemption for files keys the at-rest sweep owns (spec §5.6, claim §6.2a, 1b-next ruling 21). The exemption also covers keys that moves' push, install and return parks keep live, including current-generation keys, which is wider than the diagnosis's dead-generation case, so INV-10 at an operation's end cannot tell those from a key a later chore should have parked. A park keeps such a key live; the key later goes obsolete; the sweep retires it. INV-10 at an operation's end used to fire before the sweep ran. `final()` still requires every such key to be retired, so a key the sweep never retires still fails the seed. Seeds 1674, 2106, 2627.

-- Park-replica and park-superseded in a two-box region now wait for stop evidence from every other live box of the region, as hostops `collectEvidence` does (`internal/hostops/evidence.go`, lines 240 to 272). Before, the owner checked only its own box, so a sibling's replicator could still write after the region was parked. Seed 819. One divergence from hostops: the model's wait skips a sibling that is already stopped, where hostops would still wait for its evidence. One box is unaffected: the wait is gated on two boxes per region.

+- Park-replica and park-superseded in a two-box region now wait for stop evidence from every other live box of the region, as hostops `collectEvidence` does (`internal/hostops/evidence.go`, lines 240 to 272). Before, the owner checked only its own box, so a sibling's replicator could still write after the region was parked. Seed 819. One divergence from hostops: the model's wait skips a sibling that is already stopped, where hostops would still wait for its evidence. One box is unaffected: the wait is gated on two boxes per region. Since 02ba19b4 the wait is the named rule `park-evidence-every-box` (region HA block of `allRules`), and its witness `wParkEvidenceEveryBox` scripts seed 819's shape: it holds with the rule, and under the mutation the host is freed with the sibling's late level-0 file as residue (INV-10).

- `fence()` replaces the target when a fenced source is also the operator-named target. This is the ruling-13 stand-in path only (the operator's resolve): it replays from `pinning` with the source eligible, and without this the replay stalled for ever (seed 236, INV-3). The worker's own target choices already exclude the source (1b-next ruling 26), and a model-wide source exclusion was tried and rejected because it breaks the three ruling 26 tests (`TestProbeFailedInATwoBoxRegion`, `reloc-no-spare-bound` and `reloc-dead-target-bound`), which rely on the operator's resolve returning the host to the source. Say whether the stand-in is faithful enough, or whether the model wants a real return-to-source action.

**2. The two-box expectations file (5766a0e1, with df1a5f20 and 9ef58e4b).** `expected-outcomes.two-box.txt` is new. `mutate.sh` reads it only at `HOSTLIFE_BOXES=2` and it overrides the one-box file, which moves owns, rule by rule; a `-` line drops the base line. The raw result of the two-box 3,000-seed sweep was 118 caught, 39 expected, 3 STALE, 2 MISSED and 0 ERROR, exit 1. Five lines were reconciled afterwards by editing expectation files only. `create-choice-once` and `reloc-replacement-table` were STALE because the sweep catches them (239 and 2 of 3,000): df1a5f20 first dropped their lines from the one-box file, and 9ef58e4b restored the one-box file to its cf1a2bd5 content and put `-` lines for both in the two-box file instead, so the one-box file is as moves left it. `exec-writer` was STALE the same way (caught 1 of 3,000, seed 2319) and has a `-` line. `timer-canonical` and `source-readiness` were MISSED and are recorded as missed at two boxes (caught at one box). The three moves rules (`exec-writer`, `timer-canonical`, `source-readiness`) were rerun alone and exited 0; there was no complete second run. All 54 region HA rules were caught or expected. Results has the verdict lines and the arithmetic.

@@ -103,7 +105,7 @@ Readers read the code in two local worktrees, by path, not from a remote. The mo

- `JournalPin` refuses until every journaled fence has `observed_at`, so a converted move pins only after `FenceSource` plus 30 s (03da9300). Rev 19 relied on the worker's order. The nearest model rule is `reloc-pin-delay-every-fence`; check that it covers a converted move's source fence, which the move journals without `observed_at`.

- The create chooser is scoped to claim Plan 5's namespace and pool, and reads fences only for in-scope boxes (53f26ad6). The worker's chooser is scoped the same way (f9f254ac). No rule in the guards table names this scope.

- `AdmissionFenced` agrees with the guard's `With`: a retired fenced installation still reads as fenced, because absence is never evidence. `probe` also waits out `quiet_after` like every other execution action (cec08019).

-- `NameTarget` drops a converted move's other-region target from the barrier in the same CAS (151261fe). Before, an other-region target that never acknowledged, or was dead, held the relocation in `pinning` for ever. The nearest model rule is `reloc-name-before-pin`; check that the model also drops that target from the barrier.

+- `NameTarget` drops a converted move's other-region target from the barrier in the same CAS (151261fe). Before, an other-region target that never acknowledged, or was dead, held the relocation in `pinning` for ever. The model now mirrors it (66379fb3, rule `reloc-name-drops-move-target`): `relocNameTarget`'s CAS drops every participant outside the operation's region before it names the target. The model has no `move_target_box`, so it drops by region; the set is the same today, because only `convertToRelocating` leaves a box of another region among a relocation's participants (the move's target). `TestConvertedMoveDropsTheMoveTargetFromTheBarrier` stops the move's target before it acknowledges and requires the relocation to reach `installing` and serve; it fails under the mutation.

- A converted move's missing bound fence is an error, never "not fenced" (032db0d3). A journaled `fence.<src>` whose fence object cannot be read refuses the worker's pass.

- Other behaviour that the ledger records after rev 19: the HA chooser plugs into main's `selectExecutor` and keeps the plan's soft load rule (d1ce3f72); the relocation row's serving case calls main's `hostbox.Serving`, so a malformed serving claim holds its row (bfaa307d); `writers-stopped` allows only the replicator's identified descriptors, matched by process, number and path (e13f6941), with a deferred note that a kcmp ESRCH is assumed to be an exited thread without checking, which the final review is to fix. The model abstracts volume evidence as one flag per box (plan ruling 10), so these have no model step unless you say otherwise. Task 6 (4879c1e5) changed no rev 19 behaviour; it added a test.

@@ -111,6 +113,19 @@ Open questions from 1b-next Task 7 (the release receipt, commit 1ee322d6 when th

- Controller restart detection. Whether "this process already flushed" is decided by boot ID plus controller ID alone, while main's `claimLaunchOwner.local` also compares the PID and the process start time. A restarted agent could offer its own drain where main requires recovery, if the controller ID survives a restart. This is the question What to check 21 asks of `box.Epoch`: is it a faithful stand-in for the boot and controller identity, or does the model need the PID and start-time check as well?

- The release receipt's `.sig`. `StopReceiptReleases` binds the receipt by digest, bytes, key and fields but does not verify the box's `.sig`, which main's console-side retirement check does. Say whether the model's receipt (two-box R8 #1) needs a signature step, or whether leaving it out is right.

+**4. The final review's fix wave (04c9487d to db4b2a09).** The whole-branch review (`.superpowers/sdd/2026-10-07-region-ha-hostlife-two-box/final-review.md`) asked for these, and `final-fix-report.md` beside it has the evidence:

+- 04c9487d: the release-and-journal block that `relocReleasing`, `relocProbeFailed` and the fence-pending path each carried is one helper, `relocJournalRelease`. The two-box COUNTERS line and every two-box seed's full trace over the gate's 300 seeds are unchanged.

+- 66379fb3: `reloc-name-drops-move-target`, the mirror of 151261fe (item 3 above).

+- 02ba19b4: cf566b41's region-wide evidence wait is the named rule `park-evidence-every-box`, with its witness (item 1 above).

+- 028150d0: the operator's replay no longer excludes a released source; it excludes only a released failed target, as ruling 13 says (`TestOperatorReplayKeepsAReleasedSourceEligible`).

+- 0c3deba4: the one-box identity tests pin one box per region whatever `HOSTLIFE_BOXES` says.

+- 6b52cf73: `exec-writer` and `reloc-replacement-table` are `rare 30000` at two boxes (caught 1 and 2 times in 3,000) instead of `-` lines.

+- 819a76c4: stale comments.

+- cdbfa1f7 and db4b2a09: `reloc-name-drops-move-target` is a liveness guard, so it has its direct test and a `missed` line in each expectation file, and no witness. `park-evidence-every-box` has no expectation line: its witness catches it at either shape.

+With them the region HA block has 56 rules. The one-box COUNTERS line, the interruption trace and the 300 seed hashes are still byte-identical to the baseline, an unmutated two-box run of 3,000 seeds has 0 failed (at 819a76c4; the later commits change only a witness and the expectation files), and the two new rules classify alone as expected: at two boxes over 3,000 seeds `park-evidence-every-box` is CAUGHT (sweep 1 of 3000, seed 819; witness violated) and `reloc-name-drops-move-target` an EXPECTED-MISS, and at one box over 300 seeds the same, exit 0 both. No full sweep was run on this code.

## Findings F1 to F3, closed, and the open window L21