amadan
Joint round 2 brief (J1 fix only)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+41
−0
docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R2.md+41 −0
CI passed — run details
diff --git a/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R2.md b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R2.md| new file mode 100644 |
| index 000000000..1bb6d34aa |
| --- /dev/null |
| +++ b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R2.md |
| @@ -0,0 +1,41 @@ |
| +# Joint round 2 brief: the two-box model after J1 |
| + |
| +Round 1 (`CODEX-REVIEW-TWO-BOX-R1.md`, a2ef0203) did not pass. It found: |
| +- J1, the files live set is not region-aware (model); |
| +- J2 = F4 and J3 = F5, which are contracts owed by moves and the claim. |
| + |
| +J2 and J3 are posted on amadan carlos/platform #236 and have not been answered. This round reviews only the J1 fix. Do not re-judge J2 or J3. Say only whether anything in the fix changes them. |
| + |
| +**What changed (a2ef0203..dfab457c on `region-ha-two-box-build`, model code only):** |
| +- `55f03a6c`: |
| + - `filesLive`, `filesLiveSet` and `objectReferenced` take the key's region. |
| + - A files key is live only in its files home region. |
| + - New rule `files-live-region`, with witness `wLateManifestAfterMove`. In that witness a source's manifest PUT and a changed object are held past a cross-region move's cleanup. Both must then be retired in the former region. |
| +- `dfab457c`: the files home follows moves §5.1, as claim §6.2a points to it. |
| + - **Region HA's own phases:** |
| + - the executor's region; |
| + - the source region for the whole of `relocating`. The implementer widened this past the pin and the prepared generation, because two-box seed 1215 stalled without it. |
| + - **Moves' phases, the source region:** |
| + - while moving; |
| + - while landing, until the target's probe is admitted; |
| + - while restoring, including released. |
| + - **No home** while creating, deleting, parking or purging. |
| + - New rule `files-home-move-phases`, with witness `wMoveStoppedKeepsLiveFiles`. A park is queued during a move and runs in stopped. The source is then terminated, and the converted failover must serve with the keyed manifest. |
| + |
| +**Evidence:** |
| +- The implementer's report and the reviewer's review: `.superpowers/sdd/2026-10-07-region-ha-hostlife-two-box/joint-j1-report.md` and `joint-j1-review.md`. These are on local disk, not committed. |
| +- The gate passes at 300+300 seeds, and the 3,000-seed two-box run is unmutated with 0 failed. |
| +- One-box counters and traces are byte-identical (`ae19edaec4491fd3`). |
| +- The two-box counters hash is now `fea529f94642f661` (was `e948c4a35f07ccc3`). 44 of 300 two-box traces differ, and all of them pass. |
| +- The random sweep reaches neither new rule (0/3000 each). Their evidence is their witnesses, which fail under each mutation in both shapes. |
| +- An optional invariant, that no park archives the newest manifest in the files home, was ruled out. It would pre-empt the INV-3 evidence of the `files-live-set` and `files-live-set-moves-parks` witnesses. |
| + |
| +**Questions:** |
| +1. Is J1 closed? |
| +2. Is the phase table right against moves §5.1 and claim §6.2a? |
| + - Is "no home" right for creating, deleting, parking and purging? |
| + - Is the source region right for the whole of `relocating`? |
| +3. Is any new defect introduced? |
| +4. Should the ruled-out invariant be added anyway, given what it costs the existing witnesses? |
| + |
| +Give findings with P1/P2/P3 severity and file:line. End with a verdict on whether J1 is closed. |