amadan
Astra joint round 1 (two-box model + 1b-next stage A): unedited
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+42
−0
docs/superpowers/plans/CODEX-REVIEW-TWO-BOX-R1.md+42 −0
diff --git a/docs/superpowers/plans/CODEX-REVIEW-TWO-BOX-R1.md b/docs/superpowers/plans/CODEX-REVIEW-TWO-BOX-R1.md| new file mode 100644 |
| index 000000000..437b1ca02 |
| --- /dev/null |
| +++ b/docs/superpowers/plans/CODEX-REVIEW-TWO-BOX-R1.md |
| @@ -0,0 +1,42 @@ |
| +**Relocation may not merge on this evidence.** I found one new P2 in model `db4b2a09` and confirmed that F4/F5 remain unresolved against built `fe144bab`. No new P1 finding. |
| + |
| +1. **P2 — The files live set protects residue in the wrong region.** |
| + [moves_test.go:1924](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build/internal/sim/hostlife/moves_test.go:1924) exempts `filesLive(c, k)` before checking the authoritative region. [regionha_test.go:2116](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build/internal/sim/hostlife/regionha_test.go:2116) considers the newest manifest from every region live. |
| + |
| + A reachable interleaving is: the source issues a delayed manifest PUT; a cross-region move completes and parks the source’s objects; the PUT lands afterward. Move stopping does not drain that pending request, and the target admission preserves the source generation in `genParent`. The old-region manifest then protects itself indefinitely through `newestManifest`, so the sweep refuses it. Claim §6.2a requires retirement in the former region; the model’s region-scoped residue oracle correctly still counts it as residue. |
| + |
| + **Fix:** make files liveness region-aware, including manifest references and object references. Add a deterministic witness holding the source manifest until after move cleanup, then require its retirement. This finding is established by static tracing, not an executed reproduction. |
| + |
| +2. **P2 — F4’s successful model behavior still depends on an unimplemented integration contract.** |
| + [regionha_test.go:2314](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build/internal/sim/hostlife/regionha_test.go:2314) preserves files across push, landing-install and rollback-return parks. Its witness is `wPushKeepsLiveFiles`; removing the guard prevents subsequent failover. |
| + |
| + The built landing adapter still falls back to a view without the files live set at [moveslandpark.go:48](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-1b-next-build/internal/host/moveslandpark.go:48). That path is dormant; this is not an enabled-production deletion finding. |
| + |
| + **Disposition:** claim §6.2a already owns the combined live-set requirement. Moves §7.6/§8.3 and the adapter implementation plan must explicitly apply it to these parks, with destructive-step tests. Accept F4’s intent, subject to the region qualification in finding 1. |
| + |
| +3. **P2 — F5’s committed-landing recovery owner exists only in the model.** |
| + [regionha_test.go:1594](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build/internal/sim/hostlife/regionha_test.go:1594) converts a committed landing whose target terminates into target-region failover. `wCommittedLandingTargetLost` exercises the record-commit race. |
| + |
| + Built relocation starts require `KindServing`; the existing conversion at [relocating.go:75](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-1b-next-build/internal/hostclaim/relocating.go:75) accepts `KindMoving`, not a committed landing. The final build fixes did not add this recovery owner. |
| + |
| + **Disposition:** moves §7.10 should own the record-first race decision, with matching claim and HA §5.8/§5.9 transitions. Target-region failover is a reasonable resolution, provided it preserves outstanding cleanup obligations and is tested on both sides of the commit. |
| + |
| +The remaining stage-A comparisons found no new mismatch: acknowledgement barriers, target naming, release recovery, pin binding, replacement limits, fence deadlines, EnsureLocal and post-opening receipt verification agree with the built code. `box.Epoch` adequately represents process identity for these interleavings. The final scanner, malformed-counter, observer and refusing-pass fixes require their implementation tests; the model cannot prove those details. |
| + |
| +I accept rulings 13–19 within their stated limits: |
| + |
| +| Ruling | Assessment | |
| +|---|---| |
| +| 13 | Accept the operator-resolution abstraction; it does not prove an implemented resolve command. | |
| +| 14 | Release and no-spare bounds match the build. | |
| +| 15 | Accept the restricted termination sweep alongside the explicit cases. | |
| +| 16 | Abandoned prepared generations match; the direct test distinguishes obligation ownership. | |
| +| 17 | Keyless recovery correctly refuses; L21 remains open. | |
| +| 18 | The mixed witness world adequately represents an HA-enabled one-box region. | |
| +| 19 | Publication order provides an independent check of prepared-manifest sequencing. | |
| + |
| +The L21 witness represents the stated window. Either proposed contract can remove its sweep exclusion only after ensuring the correct key is durably recoverable before database uploads depend on it. |
| + |
| +Formatting and shell-syntax checks passed. Go tests could not run because the sandbox refused creation of the build directory. The recorded sweeps and baseline comparisons therefore remain supplied evidence, not independently rerun results. |
| + |
| +**Verdict:** accept the existing one-box baseline evidence; the two-box round does **not** pass. Fix the regional files-live error, close F4/F5 with agreed contracts and corresponding implementation gates, then complete Task 11’s validation and CI requirements. Stage-A dormancy does not itself waive its “no open finding against relocation” merge condition. |
| \ No newline at end of file |