carlos / platform Public
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,filesLiveSetandobjectReferencedtake the key's region. - A files key is live only in its files home region. - New rulefiles-live-region, with witnesswLateManifestAfterMove. 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 ofrelocating. 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 rulefiles-home-move-phases, with witnesswMoveStoppedKeepsLiveFiles. 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.mdandjoint-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(wase948c4a35f07ccc3). 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-setandfiles-live-set-moves-parkswitnesses.
Questions:
- Is J1 closed?
- 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? - Is any new defect introduced?
- 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.