Review brief: the joint model with two boxes per region (L18), round 1

You are an independent second reader, reviewing with the claim and moves sessions. Review internal/sim/hostlife at commit db4b2a09 on branch region-ha-two-box-build (the model; its code last changed in the final review's fix wave, 04c9487d to db4b2a09, item 4 under "Changes made while building"; the commits after db4b2a09 update this brief) against plan 1b-next rev 19, which Astra's round 18 accepted as "stage A ready to build":

• plan 1b-next rev 19 git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md (rulings 1 to 27; the dispositions of revs 2 to 19, rev 17's for this model's findings F1 to F3; request L21; Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's gate) and its findings CODEX-PLAN-REGION-HA-1BN-R1.md to R18.md;
• region HA spec 1 docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md on origin/main (rev 5.4, §24; H1 to H19; §2, §3, §5.2, §5.3, §5.4, §5.6, §5.8, §5.9, §5.10, §7, §9 L1 to L20);
• claim rev 6.30 git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md (§4 L1, §6.2a L13, §6.4a item 2, §7.3 D2 to D6, §11);
• moves rev 7.22 on this branch (§7.6, §7.10, §14.2);
• the plan that built it, docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md rev 11 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, CODEX-PLAN-REGION-HA-TWO-BOX-R1.md, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, CODEX-PLAN-REGION-HA-TWO-BOX-R2.md; "Rev 6: round 3 dispositions" answers round 3, CODEX-PLAN-REGION-HA-TWO-BOX-R3.md; "Rev 7: round 4 dispositions" answers round 4, CODEX-PLAN-REGION-HA-TWO-BOX-R4.md, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, CODEX-PLAN-REGION-HA-TWO-BOX-R5.md, and compares the worker's checks with Worker.Step; "Rev 9: round 6 dispositions" answers round 6, CODEX-PLAN-REGION-HA-TWO-BOX-R6.md, and compares every release and flush path with Task 7; "Rev 10: round 7 dispositions" answers round 7, CODEX-PLAN-REGION-HA-TWO-BOX-R7.md; "Rev 11: round 8 dispositions" answers round 8, CODEX-PLAN-REGION-HA-TWO-BOX-R8.md).

Fixed: do not re-argue

• H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate, 1b-next rev 19's rulings 1 to 27 as Astra read them; L21 is open and Paul's.
• The one-box shape is the baseline: its 300-seed COUNTERS line, a create-interruption trace and the trace hash of every one of its 300 seeds are byte-identical to rev 7.22's after every task (the line is below), so every one-box verdict of rev 7.22 stands (ruling 2 states the converted-move caveat).

The COUNTERS line at 5766a0e1, equal to the baseline (and unchanged at db4b2a09):

{"abandoned empty generation skipped":1,"abort":106,"admission: no predecessor writer, nothing declared":78,"admissions born covered: warm":62,"admissions born covered: whole-location park pending":1,"admissions covered at the commit park":2,"admissions covered: clean-return":2,"admissions covered: sealed":45,"admissions: cold":226,"admissions: warm":62,"app stopped: its session's agent is gone":4,"clean close refused: a process still runs":15,"clean close refused: start unfinished or agent gone":1,"clean close refused: uncertain":3,"clean close: certificate not acknowledged":1,"clean closes":69,"completed beyond H":134,"create restarted on 412":32,"declared-lost":2,"diag: staging newer than seal at install":2,"disk-lost":6,"disk-lost with the crash":15,"final: recovery admission run":25,"first uploads":92,"free after park":115,"freed":284,"holderless sweeps":115,"idle stop before replication opened":8,"local database purged":192,"ltx compactions":30,"ltx upload retries":1,"marker republished":1,"move-done":2,"open: PUT retried":4,"open: abandoned":4,"open: marker PUT retried":70,"open: waits for its first":35,"open: waits for the marker":310,"park scope bound":1520,"probe restarted":11,"publish: predecessor empty everywhere":78,"publish: predecessor left to its region":2,"purge failed: writer not started":12,"purge failures injected":520,"push":84,"replication opened":277,"replication refused: the session's agent is gone":1280,"restore anchors":100,"revert":2,"rollback-clean":3,"rollback: source database lost":1,"snapshot rotations":17,"stale signature refused":104,"stamp records lost":74,"start: environment not ready":467,"wake waited for a clean close":4,"why: configuration changed during the move @config":2,"why: cut deadline @local":1,"why: declared lost @probing":1,"why: landing deadline @checking":1,"writes declared lost":26,"writes_lost declared":105,"writes_lost: another session of a lost target":4,"writes_lost: the legacy identity (session 0)":30}

• The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul.
• The model's abstractions, as moves §14.2 lists them, plus this round's: a failover enters at pinning with the D6 barrier at the installing CAS (ruling 4); the stale edges file is the former executor's row (ruling 9); volume evidence is one flag per box (ruling 10); the files publisher runs in the two-box shape and a dead box's disk is never read there (ruling 11); files are objects named by manifests and files directories, created before they are named and bound to a region (plan ruling 25); the stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10) has no model step.

The guards, mapped

| Model rule | 1b-next rev 19 | Finding | Spec | Evidence | |---|---|---|---|---| | create-choice-once | BeginCreateOn, CompleteCreate never substitutes | R9-2 | §5.2, P5-D2, P5-D6 | expected miss; TestCreateNamesItsExecutorOnce | | reloc-start-guard | RelocationStartGuard | | §5.8, L11 | expected miss; TestRelocationStartGuardRefuses | | reloc-exec-ack-barrier | requireAcks (ToReleasing, ToInstalling, ToInstalled, ToProbing) | two-box R1 #4 | D6 | expected miss; TestReplacementWithoutAcknowledgementHoldsEachTransition | | reloc-ack-before-pinning | PinAfterRelease's requireAcks | R3-6 (rev 4 N6) | D6, §5.8 | expected miss; TestReplacedTargetAcknowledgesBeforePinning | | reloc-release-first | PinAfterRelease cites the release | | §5.8 A3-2, L10 | witness INV-1 | | reloc-release-deadline | Worker.releaseOverdue, ReleaseDeadline | R1-16 (ruling 14) | §5.8 | witness INV-3 | | reloc-pin-reaches-release | JournalPin's release bound | | §5.8 | expected miss (redundant with step 2) | | reloc-pin-claim-gen | RecoveryPinKey, JournalPin | R1-11 (ruling 16) | §5.8, B2-3 | witness INV-3 | | reloc-pin-evidenced-empty | JournalPin, StorePinner Empty | R1-13, R2-13 (ruling 15) | §6.4a | witness INV-2 | | reloc-failover-pin-delay | FailoverPinDelay | | §5.8 | expected miss (loss bound) | | reloc-exec-only-installs | §5.8 Exclusion; ToInstalling | | HA2 | expected miss; TestOnlyTheExecutorInstalls | | reloc-install-receipt | RecordLocalInstall, ToProbing | | §5.8 B1-2 | witness INV-4 with reloc-ensure-local | | reloc-ensure-local | Effects.EnsureLocal | R14-2 (rev 15) | §5.8 | witness INV-4 | | reloc-verify-receipt | Effects.VerifyReceipt, MarkStuck in probing | R15-1 (rev 16) | §5.8 (line 847) | witness INV-4 | | reloc-no-reinstall | RecordLocalInstall after PreparedOpened | | §5.8 B2-5 | witness timer | | reloc-prepared-opened-journal | prepared_opened, PreparedOpened | R11 S1 (rev 12) | B1-1, B2-5 | witness timer | | reloc-probe-attempts | BeginProbeAttempt, MaxProbeAttempts | R2-6 (ruling 19) | §5.8 limits | expected miss; TestProbeAttemptsCountedBeforeTheyAreMade | | reloc-released-coverage | relocationAdmission, coverageFor | | §6.4a item 2, L9 | witness INV-2 | | reloc-row-cases | RelocationRow, Task 9a | | §5.3, L12 | witness INV-6 with exec-admission and exec-writer | | reloc-replacement-cap | MaxTargetReplacements, stuckOn | R1-16, R2-16 | §5.8 | expected miss; TestStuckAfterTwoReplacements | | reloc-enrolled-only | eligibleBoxes, ExecutorChooser | | §2, HA7 | witness INV-27 | | reloc-drain-needs-writer | Worker.Start | R1-13 (ruling 11) | §5.8 | expected miss; TestDrainRefusedForANeverWokenHost | | fence-terminated-only | termfence.Verify, VerifyFence | | §5.9, H10 | expected miss; TestStoppedBoxNeverFenced | | fence-discharge-qualified | fenceBox with LocalDischarge, under a verified termination fence only | R2-7, two-box R7 #1 | §5.9, L3, H19, claim §7.3 D5 | witness INV-26; TestStoppedTargetKeepsItsLocalCleanup | | fence-declares-timers | the D4 loss record (timer knowledge) | R1-4 | §5.9, moves §7.10 | witness timer | | fence-reassigns-regional | fenceBox's region reassignment | R5-2 (rev 6) | L3, D2 | witness INV-3 | | reloc-source-loss | FenceSource | | §5.8 B1-6 | witness INV-2 | | reloc-replacement-table | ReplaceTarget | | §5.8 | expected miss; TestL18NestedFailover | | reloc-replace-not-owing | replaceTargetSlot, Worker.next | R5-1 (rev 6) | §2 | witness INV-3 | | reloc-exhausted-fence | FenceExhaustedTarget | R3-5, R8-1 (ruling 23) | §5.8 the bound | witness INV-1 | | files-pin-exact | RecoveryPin.FilesManifest, retained copy | R1-5 (ruling 21) | §5.8, B2-4 | expected miss (determinism); TestL18LateFileUploads | | files-live-set | the files live set, referencedOrigins | R11-1 (rev 12) | §5.6, L13, §6.2a | witness INV-4 | | files-prepared-seq-zero | CopyPinnedManifest, PreparedAuthority | R14-1 (rev 15) | R18-1, moves §7.6 | witness INV-28 | | files-pin-needs-key | Pin's needKey, filesPin's ErrFilesUnevidenced (ruling 25) | model F2, R17-1 (rev 18) | H6, §5.6, L21 | witness INV-4 (the L21 window); TestFailoverBeforeTheFirstManifest | | reloc-no-spare-bound | Worker.Step in probe-failed (ruling 26) | model F1 (rev 17) | §5.8 | witness INV-3; TestProbeFailedInATwoBoxRegion | | reloc-dead-target-bound | FenceTargetWithoutSpare, fenceTargetStuck | R17-2 (rev 18) | §5.8 | witness INV-3 | | reloc-abandoned-prepared | abandonPrepared, abandoned_prepared, CompleteRelocation (ruling 27) | model F3 (rev 17), R17-3 (rev 18) | §5.8 | expected miss (the at-rest sweep backstops); TestAbandonedPreparedGenerationParked | | reloc-stuck-refuses-admission | relocationAdmission's stuck check (ruling 9) | two-box R1 #2 | §5.8 | expected miss; TestStuckSourceRefusesAdmission | | ha-sole-box-eligibility | eligibleBoxes with region HA on | two-box R1 #3 | §2, HA7 | expected miss; TestHASoleBoxIsCheckedLikeAnyOther | | reloc-pin-delay-every-fence | JournalPin over every fence.<box>.observed_at | two-box R1 #5 | §5.8 | expected miss (loss bound); TestPinWaitsForEveryFenceObservation | | reloc-deadline-from-observed-at | FenceTargetWithoutSpare | two-box R1 #5, R17-2 | §5.8 | expected miss; TestDeadTargetDeadlineFromObservation | | tie-hash-host | ExecutorChooser's hash of the record's host | R18-2, two-box R1 #8 | P5-D2 | expected miss (determinism); TestTieHashFollowsTheHost | | files-origins-referenced | filesPin's referencedOrigins | R11-1 | §5.6, L13 | witness INV-3 | | files-objects-region-bound | the pin's region binding | claim §11 (the move case) | §5.6 | witness INV-3 | | files-live-set-moves-parks | claim §6.2a over moves' parks | model F4 (rev 4) | L13 | witness INV-3 | | reloc-clear-after-cleanup | Finish after a successful scoped cleanup (ruling 20) | R4-5, claim §11 | §5.10 | witness INV-29 | | fence-converts-committed-landing | none: model F5 (rev 4) | claim §11 (the record-commit race) | §5.9, moves §7.10 | witness INV-3 | | reloc-failover-ack-before-pin | PinFailover's requireAcks, the initial failover only | two-box R2 #1, R3 #1 | D6, §5.8 | expected miss (loss bound); TestFailoverPinWaitsForTheAcknowledgement | | reloc-name-before-pin | Worker.pinning's NameTarget before pinUnderLease | two-box R4 #1 | §5.8, moves §7.10 | expected miss (loss bound); TestConvertedMoveWaitsForATargetBeforeItsPin | | reloc-failover-start-guard | Worker.Start (Eligible, Admission.Register, Recheck), StartRelocation's RelocationStartGuard with the source fenced | two-box R4 #3 | §5.8, L11 | expected miss; TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica | | reloc-fence-pending-blocks | Worker.Step returns w.replace(...) before its phase switch | two-box R5 #1 | §5.8, §5.9 | expected miss; TestPendingTargetFenceHoldsThePhase | | reloc-release-needs-flush | Task 7 Release, releaseDrain, relocationFlushDB, ReleaseFlushFiles, ReleasePositions | two-box R6 #1 | §5.8 | expected miss; TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush | | operator-stop-unrecoverable-only | none (plan ruling 13; 1b-next writes no resolve) | two-box R7 #2 | §5.8 | expected miss; TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush | | reloc-release-needs-receipt | Task 7 Release, RecoveryReleaseDrain, ReleasePositions.Recorded | two-box R8 #1 | §5.8 | expected miss; TestReleaseRefusedAfterACrashBeforeTheReceipt, TestOperatorStopsATargetWithNoReceipt | | reloc-name-drops-move-target | NameTarget removes move_target_box from the participants (151261fe) | final review Important 1 | §5.8, moves §7.10 | expected miss (liveness); TestConvertedMoveDropsTheMoveTargetFromTheBarrier | | park-evidence-every-box | hostops RetirementEvidence.VerifyObligation, collectEvidence over the inventory | final review Important 2 (seed 819) | claim §6.2a | witness INV-10 (wParkEvidenceEveryBox) |

Changes made while building

Four things changed or arrived after the plan's rev 11 was accepted. Read the first, second and fourth as part of the model under review. The third is a request about 1b-next.

Readers read the code in two local worktrees, by path, not from a remote. The model is in /home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-two-box-build (branch region-ha-two-box-build). The 1b-next stage A build is in /home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-1b-next-build (branch region-ha-1b-next-build).

1. Two-box model fixes after the 3,000-seed sweep (cf566b41). The first sweep was void: the unmutated two-box model failed INV-10 on seeds 819, 1674, 2106 and 2627, which hid 19 of the 28 stale readings. The one-box shape and the 300-seed gate never reach those seeds. The diagnosis is committed as docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md (it covers the first two causes, and its follow-ups cover the third). cf566b41 fixes three causes:

• INV-10 has a SweepOwed exemption for files keys the at-rest sweep owns (spec §5.6, claim §6.2a, 1b-next ruling 21). The exemption also covers keys that moves' push, install and return parks keep live, including current-generation keys, which is wider than the diagnosis's dead-generation case, so INV-10 at an operation's end cannot tell those from a key a later chore should have parked. A park keeps such a key live; the key later goes obsolete; the sweep retires it. INV-10 at an operation's end used to fire before the sweep ran. final() still requires every such key to be retired, so a key the sweep never retires still fails the seed. Seeds 1674, 2106, 2627.
• Park-replica and park-superseded in a two-box region now wait for stop evidence from every other live box of the region, as hostops collectEvidence does (internal/hostops/evidence.go, lines 240 to 272). Before, the owner checked only its own box, so a sibling's replicator could still write after the region was parked. Seed 819. One divergence from hostops: the model's wait skips a sibling that is already stopped, where hostops would still wait for its evidence. One box is unaffected: the wait is gated on two boxes per region. Since 02ba19b4 the wait is the named rule park-evidence-every-box (region HA block of allRules), and its witness wParkEvidenceEveryBox scripts seed 819's shape: it holds with the rule, and under the mutation the host is freed with the sibling's late level-0 file as residue (INV-10).
• fence() replaces the target when a fenced source is also the operator-named target. This is the ruling-13 stand-in path only (the operator's resolve): it replays from pinning with the source eligible, and without this the replay stalled for ever (seed 236, INV-3). The worker's own target choices already exclude the source (1b-next ruling 26), and a model-wide source exclusion was tried and rejected because it breaks the three ruling 26 tests (TestProbeFailedInATwoBoxRegion, reloc-no-spare-bound and reloc-dead-target-bound), which rely on the operator's resolve returning the host to the source. Say whether the stand-in is faithful enough, or whether the model wants a real return-to-source action.

2. The two-box expectations file (5766a0e1, with df1a5f20 and 9ef58e4b). expected-outcomes.two-box.txt is new. mutate.sh reads it only at HOSTLIFE_BOXES=2 and it overrides the one-box file, which moves owns, rule by rule; a - line drops the base line. The raw result of the two-box 3,000-seed sweep was 118 caught, 39 expected, 3 STALE, 2 MISSED and 0 ERROR, exit 1. Five lines were reconciled afterwards by editing expectation files only. create-choice-once and reloc-replacement-table were STALE because the sweep catches them (239 and 2 of 3,000): df1a5f20 first dropped their lines from the one-box file, and 9ef58e4b restored the one-box file to its cf1a2bd5 content and put - lines for both in the two-box file instead, so the one-box file is as moves left it. exec-writer was STALE the same way (caught 1 of 3,000, seed 2319) and has a - line. timer-canonical and source-readiness were MISSED and are recorded as missed at two boxes (caught at one box). The three moves rules (exec-writer, timer-canonical, source-readiness) were rerun alone and exited 0; there was no complete second run. All 54 region HA rules were caught or expected. Results has the verdict lines and the arithmetic.

3. 1b-next stage A is being built, and the build changed 1b-next from rev 19. The branch is region-ha-1b-next-build (worktree .claude/worktrees/region-ha-1b-next-build; the code is under internal/hostclaim, internal/hostops, internal/hostguard, internal/hostbox and internal/hostrelocate). The ledger for the current state is /home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha-1b-next-build/.superpowers/sdd/2026-10-07-region-ha-1b-next-relocation/progress.md; read it at review time, because it moves. The changes below are those up to its Task 6 (4879c1e5); its Task 7 is implemented and in review, and has two open concerns, listed after the changes. The model was written against the rev 19 text, so please check that it mirrors each change below, and say for each one whether the model already has the behaviour, needs a step or a rule, or is right to leave it out.

• JournalPin refuses until every journaled fence has observed_at, so a converted move pins only after FenceSource plus 30 s (03da9300). Rev 19 relied on the worker's order. The nearest model rule is reloc-pin-delay-every-fence; check that it covers a converted move's source fence, which the move journals without observed_at.
• The create chooser is scoped to claim Plan 5's namespace and pool, and reads fences only for in-scope boxes (53f26ad6). The worker's chooser is scoped the same way (f9f254ac). No rule in the guards table names this scope.
• AdmissionFenced agrees with the guard's With: a retired fenced installation still reads as fenced, because absence is never evidence. probe also waits out quiet_after like every other execution action (cec08019).
• NameTarget drops a converted move's other-region target from the barrier in the same CAS (151261fe). Before, an other-region target that never acknowledged, or was dead, held the relocation in pinning for ever. The model now mirrors it (66379fb3, rule reloc-name-drops-move-target): relocNameTarget's CAS drops every participant outside the operation's region before it names the target. The model has no move_target_box, so it drops by region; the set is the same today, because only convertToRelocating leaves a box of another region among a relocation's participants (the move's target). TestConvertedMoveDropsTheMoveTargetFromTheBarrier stops the move's target before it acknowledges and requires the relocation to reach installing and serve; it fails under the mutation.
• A converted move's missing bound fence is an error, never "not fenced" (032db0d3). A journaled fence.<src> whose fence object cannot be read refuses the worker's pass.
• Other behaviour that the ledger records after rev 19: the HA chooser plugs into main's selectExecutor and keeps the plan's soft load rule (d1ce3f72); the relocation row's serving case calls main's hostbox.Serving, so a malformed serving claim holds its row (bfaa307d); writers-stopped allows only the replicator's identified descriptors, matched by process, number and path (e13f6941), with a deferred note that a kcmp ESRCH is assumed to be an exited thread without checking, which the final review is to fix. The model abstracts volume evidence as one flag per box (plan ruling 10), so these have no model step unless you say otherwise. Task 6 (4879c1e5) changed no rev 19 behaviour; it added a test.

Open questions from 1b-next Task 7 (the release receipt, commit 1ee322d6 when this was written), for the joint round. Both bear on What to check 21 and on reloc-release-needs-receipt:

• Controller restart detection. Whether "this process already flushed" is decided by boot ID plus controller ID alone, while main's claimLaunchOwner.local also compares the PID and the process start time. A restarted agent could offer its own drain where main requires recovery, if the controller ID survives a restart. This is the question What to check 21 asks of box.Epoch: is it a faithful stand-in for the boot and controller identity, or does the model need the PID and start-time check as well?
• The release receipt's .sig. StopReceiptReleases binds the receipt by digest, bytes, key and fields but does not verify the box's .sig, which main's console-side retirement check does. Say whether the model's receipt (two-box R8 #1) needs a signature step, or whether leaving it out is right. 4. The final review's fix wave (04c9487d to db4b2a09). The whole-branch review (.superpowers/sdd/2026-10-07-region-ha-hostlife-two-box/final-review.md) asked for these, and final-fix-report.md beside it has the evidence:

• 04c9487d: the release-and-journal block that relocReleasing, relocProbeFailed and the fence-pending path each carried is one helper, relocJournalRelease. The two-box COUNTERS line and every two-box seed's full trace over the gate's 300 seeds are unchanged.
• 66379fb3: reloc-name-drops-move-target, the mirror of 151261fe (item 3 above).
• 02ba19b4: cf566b41's region-wide evidence wait is the named rule park-evidence-every-box, with its witness (item 1 above).
• 028150d0: the operator's replay no longer excludes a released source; it excludes only a released failed target, as ruling 13 says (TestOperatorReplayKeepsAReleasedSourceEligible).
• 0c3deba4: the one-box identity tests pin one box per region whatever HOSTLIFE_BOXES says.
• 6b52cf73: exec-writer and reloc-replacement-table are rare 30000 at two boxes (caught 1 and 2 times in 3,000) instead of - lines.
• 819a76c4: stale comments.
• cdbfa1f7 and db4b2a09: reloc-name-drops-move-target is a liveness guard, so it has its direct test and a missed line in each expectation file, and no witness. park-evidence-every-box has no expectation line: its witness catches it at either shape.

With them the region HA block has 56 rules. The one-box COUNTERS line, the interruption trace and the 300 seed hashes are still byte-identical to the baseline, an unmutated two-box run of 3,000 seeds has 0 failed (at 819a76c4; the later commits change only a witness and the expectation files), and the two new rules classify alone as expected: at two boxes over 3,000 seeds park-evidence-every-box is CAUGHT (sweep 1 of 3000, seed 819; witness violated) and reloc-name-drops-move-target an EXPECTED-MISS, and at one box over 300 seeds the same, exit 0 both. No full sweep was run on this code.

Findings F1 to F3, closed, and the open window L21

The model's rev 2 raised F1 (no exit after a failed probe in a two-box region), F2 (a failover before the first files manifest lands mints a fresh instance.key) and F3 (an abandoned P never retired by its operation). 1b-next rev 17 to 19 closed them (rulings 25 to 27, rev 18 findings 1 to 3). The model now mirrors each fix. A mutation reopens each gap, and the finding tests pass because the gaps are closed. Check that each mirror is as strong as its guard. L21 stays open: the witness files-pin-needs-key scripts the window (a keyless pre-start manifest, a key minted after the start, rows sealed with it and replicated, the box terminated before the keyed manifest lands) and requires recovery to be stuck, never to install the database without its key. Say whether the model's window is the one L21 describes, and whether either candidate contract (pre-provisioning the key, or the replicator holding its first upload) would let the model drop plan ruling 17's restriction on the sweep.

Findings F4 to F6 (rev 4), open

The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22 places, and modelled a fix for each so the sweep converges: F4, moves' parks (push, landing install, rollback return) archive the files live set (rule files-live-set-moves-parks, plan ruling 21); F5, a landing committed by its record whose target is then terminated has no recovery owner, and the model converts it to a failover (rule fence-converts-committed-landing, plan ruling 20). F6 is model-only: FenceSource after a release leaves op.exec on a lost box until the pin (plan ruling 24). Say which plan or spec should own F4 and F5, and whether the model's fix is the one it should adopt.

Results

• Gate: GOFLAGS=-buildvcs=false nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v at 5766a0e1 passes in 5.2 s with the two summary lines 300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1 and 300 seeds, 0 failed, 468 completed operations; mutated="" boxes=2. TestWitnesses runs 102 witnesses, each held with every rule on, held under every proper subset of its mutation set, and violating its named failure under the whole set. The other 64 top-level tests are the direct tests (TestL18*, the finding tests and the guard tests in the table), all passing. gofmt -l is empty and go vet is clean. The one-box COUNTERS line (also sim_test.go:991's output) equals the baseline recorded before Task 1, and the one-box trace file and all 300 seed hashes are cmp-identical to the baseline's.
• Two-box 3,000-seed sweep: HOSTLIFE_BOXES=2 HOSTLIFE_PAR=2 nice -n 19 internal/sim/hostlife/mutate.sh 3000, one run, serial, on the code of cf566b41 (df1a5f20 and 5766a0e1 change only the expectation files and mutate.sh). The unmutated two-box model runs 3,000 seeds with 0 failed. Every verdict line of the log, 162 rules:

EXPECTED-MISS  claim-cas-opid [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  revalidate-before-effect [boxes=2]: sweep 17 of 3000 (first seed 71); witness none
CAUGHT  claim-op-exclusive [boxes=2]: sweep 661 of 3000 (first seed 3); witness none
CAUGHT  sign-before-safeuntil [boxes=2]: sweep 22 of 3000 (first seed 222); witness none
CAUGHT  sign-at-check [boxes=2]: sweep 8 of 3000 (first seed 355); witness none
CAUGHT  sdk-no-resign [boxes=2]: sweep 10 of 3000 (first seed 614); witness none
CAUGHT  location-per-incarnation [boxes=2]: sweep 13 of 3000 (first seed 2346); witness none
CAUGHT  fresh-admission [boxes=2]: sweep 9 of 3000 (first seed 213); witness none
EXPECTED-MISS  exec-admission [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  fresh-incarnation [boxes=2]: sweep 13 of 3000 (first seed 154); witness none
EXPECTED-MISS  touched-incomplete [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  recovery-pass [boxes=2]: sweep 2515 of 3000 (first seed 61); witness none
CAUGHT  legacy-discovery [boxes=2]: sweep 329 of 3000 (first seed 729); witness none
CAUGHT  obligations-block-ops [boxes=2]: sweep 2 of 3000 (first seed 287); witness none
CAUGHT  park-all-versions [boxes=2]: sweep 388 of 3000 (first seed 222); witness none
CAUGHT  park-by-version [boxes=2]: sweep 2482 of 3000 (first seed 451); witness none
CAUGHT  retirement-ids [boxes=2]: sweep 1535 of 3000 (first seed 1164); witness none
EXPECTED-MISS  hostguard [boxes=2]: sweep 0 of 3000; witness none (rare: caught at 30000 seeds)
CAUGHT  fence-by-installation [boxes=2]: sweep 172 of 3000 (first seed 678); witness violated
CAUGHT  fence-stamp [boxes=2]: sweep 154 of 3000 (first seed 8); witness held
CAUGHT  park-skip-lock [boxes=2]: sweep 2788 of 3000 (first seed 137); witness none
CAUGHT  purge-reserve-first [boxes=2]: sweep 2239 of 3000 (first seed 61); witness none
CAUGHT  purge-adopts [boxes=2]: sweep 1 of 3000 (first seed 1005); witness none
CAUGHT  admission-registration [boxes=2]: sweep 40 of 3000 (first seed 105); witness none
CAUGHT  purge-journal [boxes=2]: sweep 1973 of 3000 (first seed 15); witness none
EXPECTED-MISS  registration-check [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  registration-recovery [boxes=2]: sweep 2003 of 3000 (first seed 618); witness none
CAUGHT  purge-claim-fence [boxes=2]: sweep 22 of 3000 (first seed 105); witness none
CAUGHT  fence-etag [boxes=2]: sweep 24 of 3000 (first seed 128); witness none
CAUGHT  claim-never-deleted [boxes=2]: sweep 6 of 3000 (first seed 434); witness none
CAUGHT  cancelled-creates [boxes=2]: sweep 328 of 3000 (first seed 9); witness none
CAUGHT  orphan-no-deadline [boxes=2]: sweep 40 of 3000 (first seed 37); witness none
CAUGHT  orphan-order [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  door-by-version [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  door-reread [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  strict-spawn [boxes=2]: sweep 2 of 3000 (first seed 1626); witness held
CAUGHT  evidence-whole-tree [boxes=2]: sweep 6 of 3000 (first seed 85); witness violated
EXPECTED-MISS  watchdog-independent [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  evidence-from-state [boxes=2]: sweep 2661 of 3000 (first seed 80); witness none
CAUGHT  declare-lost-compute [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  lost-quarantine [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  participant-rows [boxes=2]: sweep 4 of 3000 (first seed 429); witness none
CAUGHT  floor-boot-recovery [boxes=2]: sweep 2133 of 3000 (first seed 471); witness none
CAUGHT  stale-hold-release [boxes=2]: sweep 2 of 3000 (first seed 211); witness none
CAUGHT  restore-by-generation [boxes=2]: sweep 57 of 3000 (first seed 154); witness none
CAUGHT  restore-overlap [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  restore-gap-closed [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  restore-anchor [boxes=2]: sweep 60 of 3000 (first seed 816); witness violated
CAUGHT  root-advance [boxes=2]: sweep 4 of 3000 (first seed 1512); witness violated
CAUGHT  anchor-acked [boxes=2]: sweep 5 of 3000 (first seed 315); witness violated
CAUGHT  return-stamp [boxes=2]: sweep 52 of 3000 (first seed 27); witness violated
CAUGHT  recovery-generation [boxes=2]: sweep 9 of 3000 (first seed 631); witness violated
CAUGHT  closed-marker [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  close-waits [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  newest-l0 [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  build-completion [boxes=2]: sweep 732 of 3000 (first seed 1957); witness violated
CAUGHT  writer-session [boxes=2]: sweep 1 of 3000 (first seed 631); witness violated
CAUGHT  admit-everywhere [boxes=2]: sweep 755 of 3000 (first seed 499); witness violated
STALE   exec-writer [boxes=2]: sweep 1 of 3000 (first seed 2319); witness held; but expected-outcomes.txt says missed
CAUGHT  remote-baseline [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  writes-lost [boxes=2]: sweep 5 of 3000 (first seed 965); witness violated
CAUGHT  admit-before-start [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  baseline-live [boxes=2]: sweep 1 of 3000 (first seed 900); witness violated
EXPECTED-MISS  admit-bind-op [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  valid-ltx [boxes=2]: sweep 11 of 3000 (first seed 654); witness violated
CAUGHT  close-evidence [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  quiet-before-ack [boxes=2]: sweep 105 of 3000 (first seed 62); witness none
CAUGHT  sweep-staging [boxes=2]: sweep 13 of 3000 (first seed 187); witness none
CAUGHT  straggler-sweep [boxes=2]: sweep 1144 of 3000 (first seed 19); witness none
CAUGHT  live-set-region [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  sweep-namespace [boxes=2]: sweep 984 of 3000 (first seed 88); witness violated
CAUGHT  seal-by-version [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  staging-quiet [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  commit-before-open [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated
EXPECTED-MISS  hold-op-open [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  start-check [boxes=2]: sweep 11 of 3000 (first seed 1642); witness none
CAUGHT  start-check-claim-gen [boxes=2]: sweep 10 of 3000 (first seed 75); witness held
CAUGHT  generation-conditional [boxes=2]: sweep 3 of 3000 (first seed 1851); witness violated
CAUGHT  markers-last [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  revert-journal [boxes=2]: sweep 7 of 3000 (first seed 840); witness none
CAUGHT  fence-converts-moving [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  rollback-journal [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  dirty-return [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  seal-return [boxes=2]: sweep 1 of 3000 (first seed 1674); witness violated
CAUGHT  clean-return-identity [boxes=2]: sweep 2 of 3000 (first seed 2319); witness violated
CAUGHT  foreign-region-uncovered [boxes=2]: sweep 1 of 3000 (first seed 1614); witness violated
CAUGHT  cover-at-park [boxes=2]: sweep 7 of 3000 (first seed 410); witness violated
CAUGHT  session-scoped-loss [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  probe-window [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  absent-marker-origin [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  persisted-park-scope [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  holderless-park [boxes=2]: sweep 548 of 3000 (first seed 1); witness violated
CAUGHT  covered-baseline-refused [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  restore-selected-baseline [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  unique-declarations [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated
CAUGHT  lost-return-park [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated
CAUGHT  scope-membership [boxes=2]: sweep 1213 of 3000 (first seed 73); witness violated
CAUGHT  abort-target-owner [boxes=2]: sweep 934 of 3000 (first seed 1); witness none
CAUGHT  target-park [boxes=2]: sweep 28 of 3000 (first seed 2319); witness none
CAUGHT  timer-freeze [boxes=2]: sweep 5 of 3000 (first seed 347); witness violated
MISSED  timer-canonical [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  cut-deadline [boxes=2]: sweep 34 of 3000 (first seed 555); witness none
EXPECTED-MISS  readiness-key [boxes=2]: sweep 0 of 3000; witness none
MISSED  source-readiness [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  readiness-quiet [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  files-carried [boxes=2]: sweep 11 of 3000 (first seed 204); witness none
EXPECTED-MISS  config-before-probe [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  recovery-current-inputs [boxes=2]: sweep 23 of 3000 (first seed 126); witness violated
STALE   create-choice-once [boxes=2]: sweep 239 of 3000 (first seed 250); witness none; but expected-outcomes.txt says missed
EXPECTED-MISS  reloc-start-guard [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-exec-ack-barrier [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  reloc-release-first [boxes=2]: sweep 22 of 3000 (first seed 17); witness violated
EXPECTED-MISS  reloc-pin-reaches-release [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-failover-pin-delay [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-exec-only-installs [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-install-receipt [boxes=2]: sweep 0 of 3000; witness held
CAUGHT  reloc-no-reinstall [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-released-coverage [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  reloc-row-cases [boxes=2]: sweep 0 of 3000; witness held
EXPECTED-MISS  reloc-replacement-cap [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  reloc-enrolled-only [boxes=2]: sweep 9 of 3000 (first seed 73); witness violated
EXPECTED-MISS  reloc-drain-needs-writer [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-ack-before-pinning [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  reloc-pin-claim-gen [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-pin-evidenced-empty [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-release-deadline [boxes=2]: sweep 54 of 3000 (first seed 55); witness violated
EXPECTED-MISS  reloc-probe-attempts [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  reloc-ensure-local [boxes=2]: sweep 5 of 3000 (first seed 2106); witness violated
CAUGHT  reloc-verify-receipt [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-prepared-opened-journal [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  fence-terminated-only [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  fence-discharge-qualified [boxes=2]: sweep 236 of 3000 (first seed 3); witness violated
CAUGHT  fence-declares-timers [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  fence-reassigns-regional [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-source-loss [boxes=2]: sweep 0 of 3000; witness violated
STALE   reloc-replacement-table [boxes=2]: sweep 2 of 3000 (first seed 2854); witness none; but expected-outcomes.txt says missed
CAUGHT  reloc-replace-not-owing [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-exhausted-fence [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  files-pin-exact [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  files-live-set [boxes=2]: sweep 50 of 3000 (first seed 661); witness violated
CAUGHT  files-prepared-seq-zero [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  reloc-no-spare-bound [boxes=2]: sweep 6 of 3000 (first seed 524); witness violated
CAUGHT  reloc-dead-target-bound [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  reloc-abandoned-prepared [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  files-pin-needs-key [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  reloc-stuck-refuses-admission [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  ha-sole-box-eligibility [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-pin-delay-every-fence [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-deadline-from-observed-at [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  tie-hash-host [boxes=2]: sweep 0 of 3000; witness none
CAUGHT  files-origins-referenced [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  files-objects-region-bound [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  files-live-set-moves-parks [boxes=2]: sweep 24 of 3000 (first seed 239); witness violated
CAUGHT  reloc-clear-after-cleanup [boxes=2]: sweep 0 of 3000; witness violated
CAUGHT  fence-converts-committed-landing [boxes=2]: sweep 0 of 3000; witness violated
EXPECTED-MISS  reloc-release-needs-receipt [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  operator-stop-unrecoverable-only [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-release-needs-flush [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-fence-pending-blocks [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-name-before-pin [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-failover-start-guard [boxes=2]: sweep 0 of 3000; witness none
EXPECTED-MISS  reloc-failover-ack-before-pin [boxes=2]: sweep 0 of 3000; witness none
sweep: 5 rule(s) ERROR, MISSED or STALE
EXIT=1

The raw result is 118 caught, 39 expected, 3 STALE, 2 MISSED, 0 ERROR, EXIT=1. Reconciliation, by expectation files only: the STALE create-choice-once and reloc-replacement-table are caught by the sweep, so df1a5f20 removed their missed lines and 9ef58e4b moved that to - lines in the two-box file (the one-box file is back to its cf1a2bd5 content); exec-writer is caught at two boxes, so the override drops its one-box line; timer-canonical and source-readiness are missed at two boxes, so the override records them as expected misses (each is caught at one box). The three moves rules were rerun alone and exited 0; there was no complete second run of the final classification. With the five reclassified the count is 121 caught and 41 expected, none unexpected, and all 54 region HA rules are caught or expected. The log's exit 1 and its five flagged lines are from the expectation files as they stood before those edits.

• Findings the model made while being built, beyond F1 to F6: five seeds violated with the rules on, all found by the 3,000-seed runs (the 300-seed gate never reaches them), and in each the model was changed, not a spec. Seeds 819, 1674, 2106 and 2627 failed INV-10 at an operation's end: 1674, 2106 and 2627 were an oracle that fired before the at-rest sweep retired a files key a park kept live (the first item under "Changes made while building"), and seed 819 was the park-replica owner checking only its own box's stop evidence (the second item). Seed 236 then failed INV-3 once those were fixed: the operator's resolve named the source as the target and fence() never replaced it (the third item). None is a 1b-next gap. Two more model-side corrections came from task reviews rather than seeds, and Task 5G closed both (Astra's round 7, findings 1 and 2): INV-26 was a tautology on the operation's discharges and the operator's discharge had no volume check, and the operator stopped slow targets as well as unrecoverable ones.

What to check

1. Each witness forces the interleaving its rule exists for, and nothing else fails under its mutation (the named failure is the first violation). Each direct test of a bound fails under its mutation.
2. The phase table as modelled against 1b-next rev 19 Task 1: every CAS's conditions, what each phase admits, who may act; the barrier on every phase change; MarkStuck's refusal between installed and a probe.
3. The release sequence's steps, its deadline, released coverage's binding to the flushed release, and a release whose session's replicator was gone (Flushed false: it declares).
4. The pin: the generation pinSource selects against genselect.Select, the claim-version binding against RecoveryPinKey, evidenced emptiness against 1b-next ruling 15, the files pin against B2-4.
5. EnsureLocal and VerifyReceipt against rev 15 and rev 16: the scoped cleanup that retires an unopened install (here: an execution lease that expired before its renewal), the restore under the same stamp, the receipt check after P opens, and that nothing compares content the admitted writers changed.
6. The fence: terminated only, a stuck operation consumes none, timers declared, regional chores passed to the region, local chores discharged only with qualifying evidence, and that no recovery step waits on volume evidence.
7. The replacement table, source loss, nested failover from holder.generation, the cap checked before a spare, the phase-sensitive exhausted fence, and the operator's resolve (plan ruling 13).
8. The files publisher, P's prepared manifest at sequence 0, INV-28, and the files live set against L13 and rev 12's referenced origins.
9. The one-box region (ruling 18): is a witness world with region 0 held at one box a faithful stand-in for a region HA region of one box, or does the round want a mixed sweep shape?
10. The expected misses: is each reason right, or is there an invariant the model should check?
11. The plan's rulings 13 to 19 (14, 16 and 17 as rev 3 rewrote them to mirror 1b-next rulings 26, 27 and 25): accept each, or say why it is wrong.
12. Dormancy: anything in the two-box code that changes a one-box outcome (the COUNTERS line and the trace comparisons say no; check the reasoning, ruling 1, and ruling 2's caveat on the converted move).
13. (Rev 4) Astra round 1's fixes: stuck refuses admission; region HA checks a sole box; durable acknowledgements, kept apart from controller readiness, gate every transition; every fence observation is retained and the deadline runs from observed_at; TestL18TerminationAtEveryExactPhase stops in exactly each phase, probe-failed included; each named guard's direct test fails without it.
14. (Rev 5) Astra round 2's fixes: PinFailover's barrier before the failover's pin (ruling 4 as amended: is the barrier at pinning equivalent to 1b-next's at starting?), the published-marker boundary, the adverse volume under a failover of the current executor, and the pinned manifest's generation parked at completion, which is the model's abstraction of the at-rest sweep (claim §6.2a) and the storage follow-up (1b-next ruling 21), not a CompleteRelocation step.
15. (Rev 6) Astra round 3's fix: only an initial failover (opState.PinFailover) waits for the acknowledgements before its pin; a converted move, a nested failover and a replay pin first (TestConvertedMovePinsBeforeAcknowledgement). Is the flag a faithful stand-in for 1b-next's starting?
16. (Rev 7) Astra round 4's fixes and the entry-point table in "Rev 7: round 4 dispositions": the target named before any pin on every path, relocPhaseName, and the failover started through Worker.Start's guards in their order. Is any entry point still ordered differently from 1b-next?
17. (Rev 8) Astra round 5's fix and the Worker.Step order table in "Rev 8: round 5 dispositions": a pending fence holds every regional transition, while the participant's own release and the box's other work stay schedulable. Is anything the model still runs while a fence is pending a Worker.Step transition?
18. (Rev 9) Astra round 6's fix and the release-path table in "Rev 9: round 6 dispositions": no release without the session's own flush or a recorded one, the replay of a recorded flush, and the operator's stop of a target that can never release (plan ruling 13). Is the single releaseRecord a faithful stand-in for both of 1b-next's recovery cases?
19. (Rev 10) Astra round 7's fixes: discharge only for a terminated box with qualifying evidence (INV-26 on the operation's discharges), and the operator's stop narrowed to an unrecoverable release. Is releaseUnrecoverable the right line between resume and stop?
20. (Rev 11) Astra round 8's fix: the receipt apart from the recorded positions, with the flushing controller's identity. Is the agent process (box.Epoch) a faithful stand-in for 1b-next's boot and controller identity?
21. (Rev 4) Claim §11's cases: the move with an unchanged file, the automatic target loss racing the record commit, the failed cleanup that blocks executable updates (INV-29), the forced open boundaries (four, the published marker before replication opens included). Are the file-object model (plan ruling 25) and the controller record faithful enough to stand for them, and is the coverage table in the plan's rev 4 section right about which findings only 1b-next's own tests can prove?

Output

Findings ranked P1 (a two-writer or data-loss path the model admits, a witness that does not prove its claim, a one-box change), P2 (a case from claim §11 or L18 not covered, a guard whose mutation is wrong, a 1b-next rev 16 guard the model does not mirror), P3 (clarity). Each gives the file and line, the problem, the evidence (a seed, a witness trace, a spec or plan line), and a concrete fix. End with a verdict: the round passes for the one-box and the two-box shape, or it does not, and what would make it pass; and, for each of F4 and F5, which plan or spec should change.