amadan
Astra brief: L18 joint round, round 2
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+37
−0
docs/superpowers/plans/CODEX-REVIEW-L18-JOINT-ROUND-FINAL-BRIEF-2.md+37 −0
CI cancelled — superseded by a newer push — run details
CI log
=== gate === cd launchctx && go vet ./... && go test ./... -count=1 ok amadan.net/carlos/platform.git/launchctx 0.012s ? amadan.net/carlos/platform.git/launchctx/controlname [no test files] ? amadan.net/carlos/platform.git/launchctx/wireid [no test files] go vet ./... gofmt -l .: clean go test ./... -count=1 -timeout 30m amadan: job cancelled — a newer push superseded it
diff --git a/docs/superpowers/plans/CODEX-REVIEW-L18-JOINT-ROUND-FINAL-BRIEF-2.md b/docs/superpowers/plans/CODEX-REVIEW-L18-JOINT-ROUND-FINAL-BRIEF-2.md| new file mode 100644 |
| index 000000000..0aa7364b6 |
| --- /dev/null |
| +++ b/docs/superpowers/plans/CODEX-REVIEW-L18-JOINT-ROUND-FINAL-BRIEF-2.md |
| @@ -0,0 +1,37 @@ |
| +# Astra: L18 joint round, round 2 (stage B Task 11) |
| + |
| +Your round 1 (`CODEX-REVIEW-L18-JOINT-ROUND-FINAL.md`) found four P2s. This round reviews the model on `region-ha-two-box-build` at ded69314 against the built code on `region-ha-1b-next-build` at ca282378. |
| + |
| +**Finding 1** (moves' `restoring` loses source files protection) has been asked of the moves session on #236 and is not fixed yet. Re-judge it only to confirm it is still the only open item. |
| + |
| +**Finding 2, the completion protocol.** The model now has eleven new rules covering: |
| +- the probe stop under an owned fence; |
| +- C10 discharge first and the mark last, retried from the claim; |
| +- the completion barrier for successors, including drain, move and push; |
| +- the completion pass in claim mode with region HA off (ruling 82); |
| +- N6's handover. |
| + |
| +Crash and refusal witnesses exist for each (commits 52ab8507, 363055fe, d2e97bf1). |
| + |
| +**Finding 3, delayed source.** |
| +- Built: catch-up hold after completion (ruling 85, a092ddc2, b1aacf79). |
| +- Modelled: rule `reloc-completed-catchup-hold`, witness `wDelayedSourceHoldsItsRow`. |
| +- The residual is modelled as built: after a successor op replaces the serving op, the row stays ready until park-local. |
| + |
| +**Finding 4, C1/C11 fallbacks.** These are modelled as current behaviour (`reloc-c1-failed-release-refused`, `reloc-c11-later-attempt-refused`), with switches `claimC1` and `claimC11`. |
| + |
| +**New since round 1.** The model found a deadlock in the built code. A completion box was terminated before discharge while a purge held admission closed. The fix, ruling 86 (ca282378, model ded69314): a purge or delete passes the barrier when the completion box's termination fence verifies. `StartGuard` gains `fencedCompletion`. |
| + |
| +**Modelling assumptions to check against the code.** The model's report is `.superpowers/sdd/2026-10-07-region-ha-hostlife-two-box/l18-f2f4-report.md` on the two-box worktree. |
| +- (a) The probe stop is a clean close that certifies the session, so N6's wake continues the prepared generation. If root's stop does not certify, that wake is cold and declares writes lost. |
| +- (b) The source's admission fence closes at the stop, earlier than ruling 28's end of release. |
| +- (c) Rev 7.20's `opened` phase and settle window are gone. |
| + |
| +**Judge:** |
| +1. Are findings 2–4 closed? |
| +2. Is ruling 86 sound? Can the exemption admit a successor while a live box still holds participation? |
| +3. Do assumptions (a)–(c) match the built code? If not, which side is wrong? |
| +4. Is the ruling-85 residual acceptable while dormant? |
| +5. Anything new? |
| + |
| +Give findings P1/P2/P3 with file:line. End with a verdict: may relocation merge dormant once finding 1 lands? |