carlos / platform Public

Clone
git clone https://amadan.net/carlos/platform

Plain git — no account needed to clone.

Download

Download this file

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.