| 1 | # Joint round 2 brief: the two-box model after J1 |
| 2 | |
| 3 | Round 1 (`CODEX-REVIEW-TWO-BOX-R1.md`, a2ef0203) did not pass. It found: |
| 4 | - J1, the files live set is not region-aware (model); |
| 5 | - J2 = F4 and J3 = F5, which are contracts owed by moves and the claim. |
| 6 | |
| 7 | 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. |
| 8 | |
| 9 | **What changed (a2ef0203..dfab457c on `region-ha-two-box-build`, model code only):** |
| 10 | - `55f03a6c`: |
| 11 | - `filesLive`, `filesLiveSet` and `objectReferenced` take the key's region. |
| 12 | - A files key is live only in its files home region. |
| 13 | - 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. |
| 14 | - `dfab457c`: the files home follows moves §5.1, as claim §6.2a points to it. |
| 15 | - **Region HA's own phases:** |
| 16 | - the executor's region; |
| 17 | - 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. |
| 18 | - **Moves' phases, the source region:** |
| 19 | - while moving; |
| 20 | - while landing, until the target's probe is admitted; |
| 21 | - while restoring, including released. |
| 22 | - **No home** while creating, deleting, parking or purging. |
| 23 | - 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. |
| 24 | |
| 25 | **Evidence:** |
| 26 | - 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. |
| 27 | - The gate passes at 300+300 seeds, and the 3,000-seed two-box run is unmutated with 0 failed. |
| 28 | - One-box counters and traces are byte-identical (`ae19edaec4491fd3`). |
| 29 | - The two-box counters hash is now `fea529f94642f661` (was `e948c4a35f07ccc3`). 44 of 300 two-box traces differ, and all of them pass. |
| 30 | - The random sweep reaches neither new rule (0/3000 each). Their evidence is their witnesses, which fail under each mutation in both shapes. |
| 31 | - 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. |
| 32 | |
| 33 | **Questions:** |
| 34 | 1. Is J1 closed? |
| 35 | 2. Is the phase table right against moves §5.1 and claim §6.2a? |
| 36 | - Is "no home" right for creating, deleting, parking and purging? |
| 37 | - Is the source region right for the whole of `relocating`? |
| 38 | 3. Is any new defect introduced? |
| 39 | 4. Should the ruled-out invariant be added anyway, given what it costs the existing witnesses? |
| 40 | |
| 41 | Give findings with P1/P2/P3 severity and file:line. End with a verdict on whether J1 is closed. |
| 42 | |
amadan