| 1 | # Astra: L18 joint round, round 2 (stage B Task 11) |
| 2 | |
| 3 | 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. |
| 4 | |
| 5 | **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. |
| 6 | |
| 7 | **Finding 2, the completion protocol.** The model now has eleven new rules covering: |
| 8 | - the probe stop under an owned fence; |
| 9 | - C10 discharge first and the mark last, retried from the claim; |
| 10 | - the completion barrier for successors, including drain, move and push; |
| 11 | - the completion pass in claim mode with region HA off (ruling 82); |
| 12 | - N6's handover. |
| 13 | |
| 14 | Crash and refusal witnesses exist for each (commits 52ab8507, 363055fe, d2e97bf1). |
| 15 | |
| 16 | **Finding 3, delayed source.** |
| 17 | - Built: catch-up hold after completion (ruling 85, a092ddc2, b1aacf79). |
| 18 | - Modelled: rule `reloc-completed-catchup-hold`, witness `wDelayedSourceHoldsItsRow`. |
| 19 | - The residual is modelled as built: after a successor op replaces the serving op, the row stays ready until park-local. |
| 20 | |
| 21 | **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`. |
| 22 | |
| 23 | **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`. |
| 24 | |
| 25 | **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. |
| 26 | - (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. |
| 27 | - (b) The source's admission fence closes at the stop, earlier than ruling 28's end of release. |
| 28 | - (c) Rev 7.20's `opened` phase and settle window are gone. |
| 29 | |
| 30 | **Judge:** |
| 31 | 1. Are findings 2–4 closed? |
| 32 | 2. Is ruling 86 sound? Can the exemption admit a successor while a live box still holds participation? |
| 33 | 3. Do assumptions (a)–(c) match the built code? If not, which side is wrong? |
| 34 | 4. Is the ruling-85 residual acceptable while dormant? |
| 35 | 5. Anything new? |
| 36 | |
| 37 | Give findings P1/P2/P3 with file:line. End with a verdict: may relocation merge dormant once finding 1 lands? |
| 38 | |
amadan