amadan
Region HA two-box model plan: Astra round 1 findings (1 P1, 7 P2), unedited
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+71
−0
docs/superpowers/plans/CODEX-PLAN-REGION-HA-TWO-BOX-R1.md+71 −0
diff --git a/docs/superpowers/plans/CODEX-PLAN-REGION-HA-TWO-BOX-R1.md b/docs/superpowers/plans/CODEX-PLAN-REGION-HA-TWO-BOX-R1.md| new file mode 100644 |
| index 000000000..5f5d11ba4 |
| --- /dev/null |
| +++ b/docs/superpowers/plans/CODEX-PLAN-REGION-HA-TWO-BOX-R1.md |
| @@ -0,0 +1,71 @@ |
| +Reviewed `3c74454f`. I found one P1 and seven P2 findings. |
| + |
| +1. **P1 — Task 1, Step 4: create recovery changes the original one-box behavior.** |
| + The [new cancellation path](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:490) applies regardless of `perRegion`. Concrete trace: persist the create’s record, stop its selected box, then run recovery after 15 steps. The baseline waits for a regional box; the new code cancels the incarnation immediately. Identical aggregate counters across 300 seeds do not establish identity for this trace. |
| + **Fix:** preserve the baseline selection/recovery path when `perRegion == 1`; enable recorded-executor cancellation in the HA shape. Add a deterministic comparison covering this interruption. |
| + |
| +2. **P2 — Task 2, Step 1: `stuck` does not refuse source admissions.** |
| + The [new source-admission branch](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:846) checks phase and row readiness, but neither `admits` nor `admitWriter` checks `Op.Stuck`. An exhausted-target fence during `starting` deliberately preserves the live source and its ready row. Ordinary wakes can therefore admit another writer while the operation is stuck. Stopping `relocate()` does not stop that admission path. This misses 1b-next’s `relocationAdmission` refusal and R1-16. |
| + **Fix:** enforce the stuck refusal at writer admission and add a stuck-source wake test that fails when the guard is removed. |
| + |
| +3. **P2 — Tasks 2–3, Step 1: the sole-box shortcut bypasses HA eligibility.** |
| + [`chooseBoxExcept`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:2102) returns the only live box before checking enrollment, executable, secrets, `lost`, or outstanding `park-local`. This affects HA-enabled one-box regions and depleted two-box regions. The unenrolled-reference scenario avoids exposing it because its sole unenrolled box cannot run the fence worker yet; create selection can still choose it. |
| + **Fix:** retain the shortcut only for the original non-HA shape. Apply all eligibility checks in HA worlds, including when one candidate remains, and test each refusal. |
| + |
| +4. **P2 — Task 2, Step 1: the acknowledgement model does not match `requireAcks`.** |
| + The [`installed` transition](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:1487) and [`probing` transition](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:1598) omit acknowledgement checks that 1b-next’s `ToInstalled` and `ToProbing` require. Elsewhere, `leasesSeen` requires current leases, whereas `requireAcks` checks durable acknowledgement entries and the participant separately checks controller readiness. The model therefore both removes permitted traces and admits forbidden transitions. |
| + **Fix:** represent recorded acknowledgements separately from current controller readiness, mirror each transition’s barrier, and test replacement participants that have not acknowledged. |
| + |
| +5. **P2 — Tasks 2 and 5A, Step 1: fence deadlines use different evidence from 1b-next.** |
| + [`relocPinning`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:1398) skips the delay whenever a release exists. `JournalPin` checks every retained fence observation even after a release—for example, after replacing a terminated target during a drain. Separately, the [dead-target deadline](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:5627) starts at actual termination, rather than the fence record’s `observed_at`. Delayed observation can consequently make the model mark an operation stuck immediately. |
| + **Fix:** retain observation times independently of termination and fence consumption. Apply the pin delay to all relevant observations and test delayed observation plus target replacement after release. |
| + |
| +6. **P2 — Task 5, Step 1: the phase tests do not establish their advertised coverage.** |
| + [`relocPhase`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:4628) accepts any later phase. Multiple workers can advance the operation within one tick, so a fault labelled `pinning` can occur during `installing`. The [termination matrix](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:3896) also omits `probe-failed` and adds a spare before the fault: its one-box case has two live boxes, and its two-box case has three. |
| + **Fix:** stop between individual actor transitions, assert the exact phase and live topology immediately before injection, include `probe-failed`, and launch replacements through the modeled group after loss. |
| + |
| +7. **P2 — Tasks 5–6, Step 1: five guards lack mutation-sensitive evidence.** |
| + The [plan explicitly lists](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:3693) five rules for which no direct test fails under mutation: `reloc-exec-only-installs`, `files-pin-exact`, `reloc-failover-pin-delay`, `reloc-exec-ack-barrier`, and `reloc-pin-reaches-release`. Their classification as determinism, loss-bound, or redundant guards explains a sweep miss, but does not replace a discriminating test. In particular, the files test lands the held manifest **after recovery completes**, so reading “latest” during installation produces the same result as reading the pin. |
| + **Fix:** add direct tests for each boundary. Land the newer manifest between pinning and installation; inspect unauthorized writes when only a non-executor acts; assert deadline/barrier states before they pass; inject a pin selection short of the journaled release. These require no additional seed sweep. |
| + |
| +8. **P2 — Tasks 4–5, Step 1, and Task 7, Step 1: required claim §11 cases remain outside the model.** |
| + The [coverage claim](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md:6145) exceeds the scenarios supplied. Missing cases include move landing → source cleanup → target failure with an unchanged file; automatic target loss racing record commit; and failed controller cleanup retaining an update-blocking record. The generic installation-crash test also does not force the prepared-admission → marker → replication-opening boundaries. Calling these Stage B integration work does not satisfy the claim’s separate executable-model requirement. |
| + **Fix:** add explicit model events and witnesses for those boundaries before claiming the milestone complete. Model file-object references sufficiently to exercise unchanged-file recovery after source cleanup. |
| + |
| +The past-findings mapping is therefore incomplete: |
| + |
| +| Findings or guards | What this model cannot currently establish | |
| +|---|---| |
| +| R1-2 | Pin selection under a location lease, including loss before publication; selection and journaling are collapsed. | |
| +| R1-4 and its follow-ups | Durable automatic-loss evidence surviving operation replacement; timer declarations do not model retained reporting evidence. | |
| +| R2-7 | Discovery completion when the final local chore is discharged; filtering obligations does not model that state. | |
| +| R11-1 | Origin authorization after admission trimming; manifests carry file content directly and use an untrimmed ancestry map. | |
| +| Controller findings across R2–R15 and R18-1 | Cleanup failures, lifetime locks, durable participation, update refusal, and removal during an ongoing operation. | |
| +| R18-2 | Host-dependent hash selection; `tieHash` uses the constant host, and the create test does not exercise two hostnames choosing opposite winners. | |
| +| Compilation, adapter, privilege and wiring findings | These remain production-boundary checks; independent model rules cannot detect their reintroduction. | |
| + |
| +F1–F3 have explicit mutation paths in Task 5A. F3’s invariant miss is reasonable **provided its operation-owned cleanup test remains mutation-sensitive**. L21 remains open as instructed; I am not requesting a different ruling or more seeds. |
| + |
| +I checked patch application and Go syntax/formatting in memory for the three new Go files through their later revisions. I could not reproduce compilation, tests, or mutation results in this read-only session. No files changed. |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Review the two-box plan at `3c74454f` using brief 1. |
| + |
| +**WHAT:** |
| +Check model fidelity, coverage, mutation strength and one-box identity. |
| + |
| +**STATUS:** |
| +Review complete: one P1 and seven P2 findings. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Correct the model guards and coverage, then revise the joint-round evidence mapping. |
| + |
| +**SESSION:** |
| +Safe to close — no files changed or processes left running. |
| + |
| +**Verdict: not ready.** |
| \ No newline at end of file |