| 1 | # Review brief: the joint model with two boxes per region (L18), round 1 |
| 2 | |
| 3 | You are an independent second reader, reviewing with the claim and moves |
| 4 | sessions. Review `internal/sim/hostlife` at commit db4b2a09 on branch |
| 5 | `region-ha-two-box-build` (the model; its code last changed in the final |
| 6 | review's fix wave, 04c9487d to db4b2a09, item 4 under "Changes made while |
| 7 | building"; the commits after db4b2a09 update this brief) against plan 1b-next rev |
| 8 | 19, which Astra's round 18 accepted as "stage A ready to build": |
| 9 | |
| 10 | - 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`; |
| 11 | - 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); |
| 12 | - 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); |
| 13 | - moves rev 7.22 on this branch (§7.6, §7.10, §14.2); |
| 14 | - 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`). |
| 15 | |
| 16 | ## Fixed: do not re-argue |
| 17 | |
| 18 | - 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. |
| 19 | - 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). |
| 20 | |
| 21 | The COUNTERS line at 5766a0e1, equal to the baseline (and unchanged at db4b2a09): |
| 22 | |
| 23 | `{"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}` |
| 24 | |
| 25 | - The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul. |
| 26 | - 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. |
| 27 | |
| 28 | ## The guards, mapped |
| 29 | |
| 30 | | Model rule | 1b-next rev 19 | Finding | Spec | Evidence | |
| 31 | |---|---|---|---|---| |
| 32 | | create-choice-once | `BeginCreateOn`, `CompleteCreate` never substitutes | R9-2 | §5.2, P5-D2, P5-D6 | expected miss; `TestCreateNamesItsExecutorOnce` | |
| 33 | | reloc-start-guard | `RelocationStartGuard` | | §5.8, L11 | expected miss; `TestRelocationStartGuardRefuses` | |
| 34 | | reloc-exec-ack-barrier | `requireAcks` (`ToReleasing`, `ToInstalling`, `ToInstalled`, `ToProbing`) | two-box R1 #4 | D6 | expected miss; `TestReplacementWithoutAcknowledgementHoldsEachTransition` | |
| 35 | | reloc-ack-before-pinning | `PinAfterRelease`'s `requireAcks` | R3-6 (rev 4 N6) | D6, §5.8 | expected miss; `TestReplacedTargetAcknowledgesBeforePinning` | |
| 36 | | reloc-release-first | `PinAfterRelease` cites the release | | §5.8 A3-2, L10 | witness INV-1 | |
| 37 | | reloc-release-deadline | `Worker.releaseOverdue`, `ReleaseDeadline` | R1-16 (ruling 14) | §5.8 | witness INV-3 | |
| 38 | | reloc-pin-reaches-release | `JournalPin`'s release bound | | §5.8 | expected miss (redundant with step 2) | |
| 39 | | reloc-pin-claim-gen | `RecoveryPinKey`, `JournalPin` | R1-11 (ruling 16) | §5.8, B2-3 | witness INV-3 | |
| 40 | | reloc-pin-evidenced-empty | `JournalPin`, `StorePinner` Empty | R1-13, R2-13 (ruling 15) | §6.4a | witness INV-2 | |
| 41 | | reloc-failover-pin-delay | `FailoverPinDelay` | | §5.8 | expected miss (loss bound) | |
| 42 | | reloc-exec-only-installs | §5.8 Exclusion; `ToInstalling` | | HA2 | expected miss; `TestOnlyTheExecutorInstalls` | |
| 43 | | reloc-install-receipt | `RecordLocalInstall`, `ToProbing` | | §5.8 B1-2 | witness INV-4 with reloc-ensure-local | |
| 44 | | reloc-ensure-local | `Effects.EnsureLocal` | R14-2 (rev 15) | §5.8 | witness INV-4 | |
| 45 | | reloc-verify-receipt | `Effects.VerifyReceipt`, `MarkStuck` in probing | R15-1 (rev 16) | §5.8 (line 847) | witness INV-4 | |
| 46 | | reloc-no-reinstall | `RecordLocalInstall` after `PreparedOpened` | | §5.8 B2-5 | witness timer | |
| 47 | | reloc-prepared-opened-journal | `prepared_opened`, `PreparedOpened` | R11 S1 (rev 12) | B1-1, B2-5 | witness timer | |
| 48 | | reloc-probe-attempts | `BeginProbeAttempt`, `MaxProbeAttempts` | R2-6 (ruling 19) | §5.8 limits | expected miss; `TestProbeAttemptsCountedBeforeTheyAreMade` | |
| 49 | | reloc-released-coverage | `relocationAdmission`, `coverageFor` | | §6.4a item 2, L9 | witness INV-2 | |
| 50 | | reloc-row-cases | `RelocationRow`, Task 9a | | §5.3, L12 | witness INV-6 with exec-admission and exec-writer | |
| 51 | | reloc-replacement-cap | `MaxTargetReplacements`, `stuckOn` | R1-16, R2-16 | §5.8 | expected miss; `TestStuckAfterTwoReplacements` | |
| 52 | | reloc-enrolled-only | `eligibleBoxes`, `ExecutorChooser` | | §2, HA7 | witness INV-27 | |
| 53 | | reloc-drain-needs-writer | `Worker.Start` | R1-13 (ruling 11) | §5.8 | expected miss; `TestDrainRefusedForANeverWokenHost` | |
| 54 | | fence-terminated-only | `termfence.Verify`, `VerifyFence` | | §5.9, H10 | expected miss; `TestStoppedBoxNeverFenced` | |
| 55 | | 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` | |
| 56 | | fence-declares-timers | the D4 loss record (timer knowledge) | R1-4 | §5.9, moves §7.10 | witness timer | |
| 57 | | fence-reassigns-regional | `fenceBox`'s region reassignment | R5-2 (rev 6) | L3, D2 | witness INV-3 | |
| 58 | | reloc-source-loss | `FenceSource` | | §5.8 B1-6 | witness INV-2 | |
| 59 | | reloc-replacement-table | `ReplaceTarget` | | §5.8 | expected miss; `TestL18NestedFailover` | |
| 60 | | reloc-replace-not-owing | `replaceTargetSlot`, `Worker.next` | R5-1 (rev 6) | §2 | witness INV-3 | |
| 61 | | reloc-exhausted-fence | `FenceExhaustedTarget` | R3-5, R8-1 (ruling 23) | §5.8 the bound | witness INV-1 | |
| 62 | | files-pin-exact | `RecoveryPin.FilesManifest`, retained copy | R1-5 (ruling 21) | §5.8, B2-4 | expected miss (determinism); `TestL18LateFileUploads` | |
| 63 | | files-live-set | the files live set, `referencedOrigins` | R11-1 (rev 12) | §5.6, L13, §6.2a | witness INV-4 | |
| 64 | | files-prepared-seq-zero | `CopyPinnedManifest`, `PreparedAuthority` | R14-1 (rev 15) | R18-1, moves §7.6 | witness INV-28 | |
| 65 | | 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` | |
| 66 | | reloc-no-spare-bound | `Worker.Step` in `probe-failed` (ruling 26) | model F1 (rev 17) | §5.8 | witness INV-3; `TestProbeFailedInATwoBoxRegion` | |
| 67 | | reloc-dead-target-bound | `FenceTargetWithoutSpare`, `fenceTargetStuck` | R17-2 (rev 18) | §5.8 | witness INV-3 | |
| 68 | | 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` | |
| 69 | | reloc-stuck-refuses-admission | `relocationAdmission`'s stuck check (ruling 9) | two-box R1 #2 | §5.8 | expected miss; `TestStuckSourceRefusesAdmission` | |
| 70 | | ha-sole-box-eligibility | `eligibleBoxes` with region HA on | two-box R1 #3 | §2, HA7 | expected miss; `TestHASoleBoxIsCheckedLikeAnyOther` | |
| 71 | | reloc-pin-delay-every-fence | `JournalPin` over every `fence.<box>.observed_at` | two-box R1 #5 | §5.8 | expected miss (loss bound); `TestPinWaitsForEveryFenceObservation` | |
| 72 | | reloc-deadline-from-observed-at | `FenceTargetWithoutSpare` | two-box R1 #5, R17-2 | §5.8 | expected miss; `TestDeadTargetDeadlineFromObservation` | |
| 73 | | tie-hash-host | `ExecutorChooser`'s hash of the record's host | R18-2, two-box R1 #8 | P5-D2 | expected miss (determinism); `TestTieHashFollowsTheHost` | |
| 74 | | files-origins-referenced | `filesPin`'s `referencedOrigins` | R11-1 | §5.6, L13 | witness INV-3 | |
| 75 | | files-objects-region-bound | the pin's region binding | claim §11 (the move case) | §5.6 | witness INV-3 | |
| 76 | | files-live-set-moves-parks | claim §6.2a over moves' parks | model F4 (rev 4) | L13 | witness INV-3 | |
| 77 | | reloc-clear-after-cleanup | `Finish` after a successful scoped cleanup (ruling 20) | R4-5, claim §11 | §5.10 | witness INV-29 | |
| 78 | | fence-converts-committed-landing | none: model F5 (rev 4) | claim §11 (the record-commit race) | §5.9, moves §7.10 | witness INV-3 | |
| 79 | | 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` | |
| 80 | | reloc-name-before-pin | `Worker.pinning`'s `NameTarget` before `pinUnderLease` | two-box R4 #1 | §5.8, moves §7.10 | expected miss (loss bound); `TestConvertedMoveWaitsForATargetBeforeItsPin` | |
| 81 | | 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` | |
| 82 | | reloc-fence-pending-blocks | `Worker.Step` returns `w.replace(...)` before its phase switch | two-box R5 #1 | §5.8, §5.9 | expected miss; `TestPendingTargetFenceHoldsThePhase` | |
| 83 | | reloc-release-needs-flush | Task 7 `Release`, `releaseDrain`, `relocationFlushDB`, `ReleaseFlushFiles`, `ReleasePositions` | two-box R6 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheFlush`, `TestReleaseReplaysTheRecordedFlush` | |
| 84 | | operator-stop-unrecoverable-only | none (plan ruling 13; 1b-next writes no resolve) | two-box R7 #2 | §5.8 | expected miss; `TestOperatorResumesASlowRelease`, `TestOperatorResumesARecordedFlush` | |
| 85 | | reloc-release-needs-receipt | Task 7 `Release`, `RecoveryReleaseDrain`, `ReleasePositions.Recorded` | two-box R8 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheReceipt`, `TestOperatorStopsATargetWithNoReceipt` | |
| 86 | | 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` | |
| 87 | | park-evidence-every-box | hostops `RetirementEvidence.VerifyObligation`, `collectEvidence` over the inventory | final review Important 2 (seed 819) | claim §6.2a | witness INV-10 (`wParkEvidenceEveryBox`) | |
| 88 | |
| 89 | ## Changes made while building |
| 90 | |
| 91 | 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. |
| 92 | |
| 93 | 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`). |
| 94 | |
| 95 | **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: |
| 96 | |
| 97 | - 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. |
| 98 | - 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). |
| 99 | - `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. |
| 100 | |
| 101 | **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. |
| 102 | |
| 103 | **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. |
| 104 | |
| 105 | - `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`. |
| 106 | - 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. |
| 107 | - `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). |
| 108 | - `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. |
| 109 | - 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. |
| 110 | - 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. |
| 111 | |
| 112 | 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`: |
| 113 | |
| 114 | - 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? |
| 115 | - 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. |
| 116 | **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: |
| 117 | |
| 118 | - 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. |
| 119 | - 66379fb3: `reloc-name-drops-move-target`, the mirror of 151261fe (item 3 above). |
| 120 | - 02ba19b4: cf566b41's region-wide evidence wait is the named rule `park-evidence-every-box`, with its witness (item 1 above). |
| 121 | - 028150d0: the operator's replay no longer excludes a released source; it excludes only a released failed target, as ruling 13 says (`TestOperatorReplayKeepsAReleasedSourceEligible`). |
| 122 | - 0c3deba4: the one-box identity tests pin one box per region whatever `HOSTLIFE_BOXES` says. |
| 123 | - 6b52cf73: `exec-writer` and `reloc-replacement-table` are `rare 30000` at two boxes (caught 1 and 2 times in 3,000) instead of `-` lines. |
| 124 | - 819a76c4: stale comments. |
| 125 | - 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. |
| 126 | |
| 127 | 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. |
| 128 | |
| 129 | |
| 130 | ## Findings F1 to F3, closed, and the open window L21 |
| 131 | |
| 132 | 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. |
| 133 | |
| 134 | ## Findings F4 to F6 (rev 4), open |
| 135 | |
| 136 | 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. |
| 137 | |
| 138 | ## Results |
| 139 | |
| 140 | - 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. |
| 141 | - 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: |
| 142 | |
| 143 | ``` |
| 144 | EXPECTED-MISS claim-cas-opid [boxes=2]: sweep 0 of 3000; witness held |
| 145 | CAUGHT revalidate-before-effect [boxes=2]: sweep 17 of 3000 (first seed 71); witness none |
| 146 | CAUGHT claim-op-exclusive [boxes=2]: sweep 661 of 3000 (first seed 3); witness none |
| 147 | CAUGHT sign-before-safeuntil [boxes=2]: sweep 22 of 3000 (first seed 222); witness none |
| 148 | CAUGHT sign-at-check [boxes=2]: sweep 8 of 3000 (first seed 355); witness none |
| 149 | CAUGHT sdk-no-resign [boxes=2]: sweep 10 of 3000 (first seed 614); witness none |
| 150 | CAUGHT location-per-incarnation [boxes=2]: sweep 13 of 3000 (first seed 2346); witness none |
| 151 | CAUGHT fresh-admission [boxes=2]: sweep 9 of 3000 (first seed 213); witness none |
| 152 | EXPECTED-MISS exec-admission [boxes=2]: sweep 0 of 3000; witness held |
| 153 | CAUGHT fresh-incarnation [boxes=2]: sweep 13 of 3000 (first seed 154); witness none |
| 154 | EXPECTED-MISS touched-incomplete [boxes=2]: sweep 0 of 3000; witness held |
| 155 | CAUGHT recovery-pass [boxes=2]: sweep 2515 of 3000 (first seed 61); witness none |
| 156 | CAUGHT legacy-discovery [boxes=2]: sweep 329 of 3000 (first seed 729); witness none |
| 157 | CAUGHT obligations-block-ops [boxes=2]: sweep 2 of 3000 (first seed 287); witness none |
| 158 | CAUGHT park-all-versions [boxes=2]: sweep 388 of 3000 (first seed 222); witness none |
| 159 | CAUGHT park-by-version [boxes=2]: sweep 2482 of 3000 (first seed 451); witness none |
| 160 | CAUGHT retirement-ids [boxes=2]: sweep 1535 of 3000 (first seed 1164); witness none |
| 161 | EXPECTED-MISS hostguard [boxes=2]: sweep 0 of 3000; witness none (rare: caught at 30000 seeds) |
| 162 | CAUGHT fence-by-installation [boxes=2]: sweep 172 of 3000 (first seed 678); witness violated |
| 163 | CAUGHT fence-stamp [boxes=2]: sweep 154 of 3000 (first seed 8); witness held |
| 164 | CAUGHT park-skip-lock [boxes=2]: sweep 2788 of 3000 (first seed 137); witness none |
| 165 | CAUGHT purge-reserve-first [boxes=2]: sweep 2239 of 3000 (first seed 61); witness none |
| 166 | CAUGHT purge-adopts [boxes=2]: sweep 1 of 3000 (first seed 1005); witness none |
| 167 | CAUGHT admission-registration [boxes=2]: sweep 40 of 3000 (first seed 105); witness none |
| 168 | CAUGHT purge-journal [boxes=2]: sweep 1973 of 3000 (first seed 15); witness none |
| 169 | EXPECTED-MISS registration-check [boxes=2]: sweep 0 of 3000; witness held |
| 170 | CAUGHT registration-recovery [boxes=2]: sweep 2003 of 3000 (first seed 618); witness none |
| 171 | CAUGHT purge-claim-fence [boxes=2]: sweep 22 of 3000 (first seed 105); witness none |
| 172 | CAUGHT fence-etag [boxes=2]: sweep 24 of 3000 (first seed 128); witness none |
| 173 | CAUGHT claim-never-deleted [boxes=2]: sweep 6 of 3000 (first seed 434); witness none |
| 174 | CAUGHT cancelled-creates [boxes=2]: sweep 328 of 3000 (first seed 9); witness none |
| 175 | CAUGHT orphan-no-deadline [boxes=2]: sweep 40 of 3000 (first seed 37); witness none |
| 176 | CAUGHT orphan-order [boxes=2]: sweep 0 of 3000; witness violated |
| 177 | EXPECTED-MISS door-by-version [boxes=2]: sweep 0 of 3000; witness none |
| 178 | EXPECTED-MISS door-reread [boxes=2]: sweep 0 of 3000; witness none |
| 179 | CAUGHT strict-spawn [boxes=2]: sweep 2 of 3000 (first seed 1626); witness held |
| 180 | CAUGHT evidence-whole-tree [boxes=2]: sweep 6 of 3000 (first seed 85); witness violated |
| 181 | EXPECTED-MISS watchdog-independent [boxes=2]: sweep 0 of 3000; witness held |
| 182 | CAUGHT evidence-from-state [boxes=2]: sweep 2661 of 3000 (first seed 80); witness none |
| 183 | CAUGHT declare-lost-compute [boxes=2]: sweep 0 of 3000; witness violated |
| 184 | CAUGHT lost-quarantine [boxes=2]: sweep 0 of 3000; witness violated |
| 185 | CAUGHT participant-rows [boxes=2]: sweep 4 of 3000 (first seed 429); witness none |
| 186 | CAUGHT floor-boot-recovery [boxes=2]: sweep 2133 of 3000 (first seed 471); witness none |
| 187 | CAUGHT stale-hold-release [boxes=2]: sweep 2 of 3000 (first seed 211); witness none |
| 188 | CAUGHT restore-by-generation [boxes=2]: sweep 57 of 3000 (first seed 154); witness none |
| 189 | CAUGHT restore-overlap [boxes=2]: sweep 0 of 3000; witness violated |
| 190 | CAUGHT restore-gap-closed [boxes=2]: sweep 0 of 3000; witness violated |
| 191 | CAUGHT restore-anchor [boxes=2]: sweep 60 of 3000 (first seed 816); witness violated |
| 192 | CAUGHT root-advance [boxes=2]: sweep 4 of 3000 (first seed 1512); witness violated |
| 193 | CAUGHT anchor-acked [boxes=2]: sweep 5 of 3000 (first seed 315); witness violated |
| 194 | CAUGHT return-stamp [boxes=2]: sweep 52 of 3000 (first seed 27); witness violated |
| 195 | CAUGHT recovery-generation [boxes=2]: sweep 9 of 3000 (first seed 631); witness violated |
| 196 | CAUGHT closed-marker [boxes=2]: sweep 0 of 3000; witness violated |
| 197 | CAUGHT close-waits [boxes=2]: sweep 0 of 3000; witness violated |
| 198 | CAUGHT newest-l0 [boxes=2]: sweep 0 of 3000; witness violated |
| 199 | CAUGHT build-completion [boxes=2]: sweep 732 of 3000 (first seed 1957); witness violated |
| 200 | CAUGHT writer-session [boxes=2]: sweep 1 of 3000 (first seed 631); witness violated |
| 201 | CAUGHT admit-everywhere [boxes=2]: sweep 755 of 3000 (first seed 499); witness violated |
| 202 | STALE exec-writer [boxes=2]: sweep 1 of 3000 (first seed 2319); witness held; but expected-outcomes.txt says missed |
| 203 | CAUGHT remote-baseline [boxes=2]: sweep 0 of 3000; witness violated |
| 204 | CAUGHT writes-lost [boxes=2]: sweep 5 of 3000 (first seed 965); witness violated |
| 205 | CAUGHT admit-before-start [boxes=2]: sweep 0 of 3000; witness violated |
| 206 | CAUGHT baseline-live [boxes=2]: sweep 1 of 3000 (first seed 900); witness violated |
| 207 | EXPECTED-MISS admit-bind-op [boxes=2]: sweep 0 of 3000; witness held |
| 208 | CAUGHT valid-ltx [boxes=2]: sweep 11 of 3000 (first seed 654); witness violated |
| 209 | CAUGHT close-evidence [boxes=2]: sweep 0 of 3000; witness violated |
| 210 | CAUGHT quiet-before-ack [boxes=2]: sweep 105 of 3000 (first seed 62); witness none |
| 211 | CAUGHT sweep-staging [boxes=2]: sweep 13 of 3000 (first seed 187); witness none |
| 212 | CAUGHT straggler-sweep [boxes=2]: sweep 1144 of 3000 (first seed 19); witness none |
| 213 | CAUGHT live-set-region [boxes=2]: sweep 0 of 3000; witness violated |
| 214 | CAUGHT sweep-namespace [boxes=2]: sweep 984 of 3000 (first seed 88); witness violated |
| 215 | CAUGHT seal-by-version [boxes=2]: sweep 0 of 3000; witness violated |
| 216 | CAUGHT staging-quiet [boxes=2]: sweep 0 of 3000; witness violated |
| 217 | CAUGHT commit-before-open [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated |
| 218 | EXPECTED-MISS hold-op-open [boxes=2]: sweep 0 of 3000; witness held |
| 219 | CAUGHT start-check [boxes=2]: sweep 11 of 3000 (first seed 1642); witness none |
| 220 | CAUGHT start-check-claim-gen [boxes=2]: sweep 10 of 3000 (first seed 75); witness held |
| 221 | CAUGHT generation-conditional [boxes=2]: sweep 3 of 3000 (first seed 1851); witness violated |
| 222 | CAUGHT markers-last [boxes=2]: sweep 0 of 3000; witness violated |
| 223 | CAUGHT revert-journal [boxes=2]: sweep 7 of 3000 (first seed 840); witness none |
| 224 | CAUGHT fence-converts-moving [boxes=2]: sweep 0 of 3000; witness violated |
| 225 | CAUGHT rollback-journal [boxes=2]: sweep 0 of 3000; witness violated |
| 226 | CAUGHT dirty-return [boxes=2]: sweep 0 of 3000; witness violated |
| 227 | CAUGHT seal-return [boxes=2]: sweep 1 of 3000 (first seed 1674); witness violated |
| 228 | CAUGHT clean-return-identity [boxes=2]: sweep 2 of 3000 (first seed 2319); witness violated |
| 229 | CAUGHT foreign-region-uncovered [boxes=2]: sweep 1 of 3000 (first seed 1614); witness violated |
| 230 | CAUGHT cover-at-park [boxes=2]: sweep 7 of 3000 (first seed 410); witness violated |
| 231 | CAUGHT session-scoped-loss [boxes=2]: sweep 0 of 3000; witness violated |
| 232 | CAUGHT probe-window [boxes=2]: sweep 0 of 3000; witness violated |
| 233 | CAUGHT absent-marker-origin [boxes=2]: sweep 0 of 3000; witness violated |
| 234 | CAUGHT persisted-park-scope [boxes=2]: sweep 0 of 3000; witness violated |
| 235 | CAUGHT holderless-park [boxes=2]: sweep 548 of 3000 (first seed 1); witness violated |
| 236 | CAUGHT covered-baseline-refused [boxes=2]: sweep 0 of 3000; witness violated |
| 237 | CAUGHT restore-selected-baseline [boxes=2]: sweep 0 of 3000; witness violated |
| 238 | CAUGHT unique-declarations [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated |
| 239 | CAUGHT lost-return-park [boxes=2]: sweep 1 of 3000 (first seed 2319); witness violated |
| 240 | CAUGHT scope-membership [boxes=2]: sweep 1213 of 3000 (first seed 73); witness violated |
| 241 | CAUGHT abort-target-owner [boxes=2]: sweep 934 of 3000 (first seed 1); witness none |
| 242 | CAUGHT target-park [boxes=2]: sweep 28 of 3000 (first seed 2319); witness none |
| 243 | CAUGHT timer-freeze [boxes=2]: sweep 5 of 3000 (first seed 347); witness violated |
| 244 | MISSED timer-canonical [boxes=2]: sweep 0 of 3000; witness none |
| 245 | CAUGHT cut-deadline [boxes=2]: sweep 34 of 3000 (first seed 555); witness none |
| 246 | EXPECTED-MISS readiness-key [boxes=2]: sweep 0 of 3000; witness none |
| 247 | MISSED source-readiness [boxes=2]: sweep 0 of 3000; witness none |
| 248 | EXPECTED-MISS readiness-quiet [boxes=2]: sweep 0 of 3000; witness none |
| 249 | CAUGHT files-carried [boxes=2]: sweep 11 of 3000 (first seed 204); witness none |
| 250 | EXPECTED-MISS config-before-probe [boxes=2]: sweep 0 of 3000; witness none |
| 251 | CAUGHT recovery-current-inputs [boxes=2]: sweep 23 of 3000 (first seed 126); witness violated |
| 252 | STALE create-choice-once [boxes=2]: sweep 239 of 3000 (first seed 250); witness none; but expected-outcomes.txt says missed |
| 253 | EXPECTED-MISS reloc-start-guard [boxes=2]: sweep 0 of 3000; witness none |
| 254 | EXPECTED-MISS reloc-exec-ack-barrier [boxes=2]: sweep 0 of 3000; witness none |
| 255 | CAUGHT reloc-release-first [boxes=2]: sweep 22 of 3000 (first seed 17); witness violated |
| 256 | EXPECTED-MISS reloc-pin-reaches-release [boxes=2]: sweep 0 of 3000; witness none |
| 257 | EXPECTED-MISS reloc-failover-pin-delay [boxes=2]: sweep 0 of 3000; witness none |
| 258 | EXPECTED-MISS reloc-exec-only-installs [boxes=2]: sweep 0 of 3000; witness none |
| 259 | EXPECTED-MISS reloc-install-receipt [boxes=2]: sweep 0 of 3000; witness held |
| 260 | CAUGHT reloc-no-reinstall [boxes=2]: sweep 0 of 3000; witness violated |
| 261 | CAUGHT reloc-released-coverage [boxes=2]: sweep 0 of 3000; witness violated |
| 262 | EXPECTED-MISS reloc-row-cases [boxes=2]: sweep 0 of 3000; witness held |
| 263 | EXPECTED-MISS reloc-replacement-cap [boxes=2]: sweep 0 of 3000; witness none |
| 264 | CAUGHT reloc-enrolled-only [boxes=2]: sweep 9 of 3000 (first seed 73); witness violated |
| 265 | EXPECTED-MISS reloc-drain-needs-writer [boxes=2]: sweep 0 of 3000; witness none |
| 266 | EXPECTED-MISS reloc-ack-before-pinning [boxes=2]: sweep 0 of 3000; witness none |
| 267 | CAUGHT reloc-pin-claim-gen [boxes=2]: sweep 0 of 3000; witness violated |
| 268 | CAUGHT reloc-pin-evidenced-empty [boxes=2]: sweep 0 of 3000; witness violated |
| 269 | CAUGHT reloc-release-deadline [boxes=2]: sweep 54 of 3000 (first seed 55); witness violated |
| 270 | EXPECTED-MISS reloc-probe-attempts [boxes=2]: sweep 0 of 3000; witness none |
| 271 | CAUGHT reloc-ensure-local [boxes=2]: sweep 5 of 3000 (first seed 2106); witness violated |
| 272 | CAUGHT reloc-verify-receipt [boxes=2]: sweep 0 of 3000; witness violated |
| 273 | CAUGHT reloc-prepared-opened-journal [boxes=2]: sweep 0 of 3000; witness violated |
| 274 | EXPECTED-MISS fence-terminated-only [boxes=2]: sweep 0 of 3000; witness none |
| 275 | CAUGHT fence-discharge-qualified [boxes=2]: sweep 236 of 3000 (first seed 3); witness violated |
| 276 | CAUGHT fence-declares-timers [boxes=2]: sweep 0 of 3000; witness violated |
| 277 | CAUGHT fence-reassigns-regional [boxes=2]: sweep 0 of 3000; witness violated |
| 278 | CAUGHT reloc-source-loss [boxes=2]: sweep 0 of 3000; witness violated |
| 279 | STALE reloc-replacement-table [boxes=2]: sweep 2 of 3000 (first seed 2854); witness none; but expected-outcomes.txt says missed |
| 280 | CAUGHT reloc-replace-not-owing [boxes=2]: sweep 0 of 3000; witness violated |
| 281 | CAUGHT reloc-exhausted-fence [boxes=2]: sweep 0 of 3000; witness violated |
| 282 | EXPECTED-MISS files-pin-exact [boxes=2]: sweep 0 of 3000; witness none |
| 283 | CAUGHT files-live-set [boxes=2]: sweep 50 of 3000 (first seed 661); witness violated |
| 284 | CAUGHT files-prepared-seq-zero [boxes=2]: sweep 0 of 3000; witness violated |
| 285 | CAUGHT reloc-no-spare-bound [boxes=2]: sweep 6 of 3000 (first seed 524); witness violated |
| 286 | CAUGHT reloc-dead-target-bound [boxes=2]: sweep 0 of 3000; witness violated |
| 287 | EXPECTED-MISS reloc-abandoned-prepared [boxes=2]: sweep 0 of 3000; witness none |
| 288 | CAUGHT files-pin-needs-key [boxes=2]: sweep 0 of 3000; witness violated |
| 289 | EXPECTED-MISS reloc-stuck-refuses-admission [boxes=2]: sweep 0 of 3000; witness none |
| 290 | EXPECTED-MISS ha-sole-box-eligibility [boxes=2]: sweep 0 of 3000; witness none |
| 291 | EXPECTED-MISS reloc-pin-delay-every-fence [boxes=2]: sweep 0 of 3000; witness none |
| 292 | EXPECTED-MISS reloc-deadline-from-observed-at [boxes=2]: sweep 0 of 3000; witness none |
| 293 | EXPECTED-MISS tie-hash-host [boxes=2]: sweep 0 of 3000; witness none |
| 294 | CAUGHT files-origins-referenced [boxes=2]: sweep 0 of 3000; witness violated |
| 295 | CAUGHT files-objects-region-bound [boxes=2]: sweep 0 of 3000; witness violated |
| 296 | CAUGHT files-live-set-moves-parks [boxes=2]: sweep 24 of 3000 (first seed 239); witness violated |
| 297 | CAUGHT reloc-clear-after-cleanup [boxes=2]: sweep 0 of 3000; witness violated |
| 298 | CAUGHT fence-converts-committed-landing [boxes=2]: sweep 0 of 3000; witness violated |
| 299 | EXPECTED-MISS reloc-release-needs-receipt [boxes=2]: sweep 0 of 3000; witness none |
| 300 | EXPECTED-MISS operator-stop-unrecoverable-only [boxes=2]: sweep 0 of 3000; witness none |
| 301 | EXPECTED-MISS reloc-release-needs-flush [boxes=2]: sweep 0 of 3000; witness none |
| 302 | EXPECTED-MISS reloc-fence-pending-blocks [boxes=2]: sweep 0 of 3000; witness none |
| 303 | EXPECTED-MISS reloc-name-before-pin [boxes=2]: sweep 0 of 3000; witness none |
| 304 | EXPECTED-MISS reloc-failover-start-guard [boxes=2]: sweep 0 of 3000; witness none |
| 305 | EXPECTED-MISS reloc-failover-ack-before-pin [boxes=2]: sweep 0 of 3000; witness none |
| 306 | sweep: 5 rule(s) ERROR, MISSED or STALE |
| 307 | EXIT=1 |
| 308 | ``` |
| 309 | |
| 310 | 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. |
| 311 | - 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. |
| 312 | |
| 313 | ## What to check |
| 314 | |
| 315 | 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. |
| 316 | 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. |
| 317 | 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). |
| 318 | 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. |
| 319 | 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. |
| 320 | 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. |
| 321 | 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). |
| 322 | 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. |
| 323 | 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? |
| 324 | 10. The expected misses: is each reason right, or is there an invariant the model should check? |
| 325 | 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. |
| 326 | 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). |
| 327 | 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. |
| 328 | 15. (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. |
| 329 | 16. (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`? |
| 330 | 17. (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? |
| 331 | 18. (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? |
| 332 | 19. (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? |
| 333 | 20. (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? |
| 334 | 21. (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? |
| 335 | 14. (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? |
| 336 | |
| 337 | ## Output |
| 338 | |
| 339 | 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. |
| 340 | |
amadan