carlos / platform Public

docs: the joint-round brief for the two-box model (L18) against plan 1b-next rev 19, round 1

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

Paul Campbell pushed by claude 2 weeks ago 08c77007e23619e4c7e4c556d6294268d9687629 parent 5766a0e

1 file changed, +316 −0

docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md +316 −0

diff --git a/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md

new file mode 100644

index 000000000..e17e50607

--- /dev/null

+++ b/docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md

@@ -0,0 +1,316 @@

+# 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 5766a0e1 on branch

+`region-ha-two-box-build` (the model; this brief is the next commit on the

+branch, so the tip holds the same model plus this file) 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:

+ `{"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

+|---|---|---|---|---|

+| reloc-replacement-cap | `MaxTargetReplacements`, `stuckOn` | R1-16, R2-16 | §5.8 | expected miss; `TestStuckAfterTwoReplacements` |

+| files-origins-referenced | `filesPin`'s `referencedOrigins` | R11-1 | §5.6, L13 | witness INV-3 |

+| 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` |

+## Changes made while building

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

+**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 (`task-6-diagnosis.md`, with the controller's rulings in `progress.md`) found three causes, and cf566b41 fixes them:

+- INV-10 has a `SweepOwed` exemption for files keys the at-rest sweep owns (spec §5.6, claim §6.2a, 1b-next ruling 21). 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 box is unaffected: the wait is gated on two boxes per region.

+- `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 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 operator tests of plan ruling 13. 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).** `expected-outcomes.two-box.txt` is new. `mutate.sh` reads it only at `HOSTLIFE_BOXES=2` and it overrides the one-box file rule by rule; the one-box file, which moves owns, is untouched except that df1a5f20 dropped two lines the two-box sweep contradicts. The two-box sweep result was 118 caught, 39 expected, 0 unexpected and 0 errors, and all 54 region HA rules were caught or expected. The override records that `timer-canonical` and `source-readiness` are missed at two boxes (caught at one box), and that `exec-writer` is caught at two boxes (1 of 3,000, seed 2319). `create-choice-once` and `reloc-replacement-table` are caught by the sweep (239 and 2 of 3,000) and by their direct tests, so they have no expectation line. Results has the verdict lines and how the five flagged ones were reclassified.

+**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`; its ledger is `.superpowers/sdd/2026-10-07-region-ha-1b-next-relocation/progress.md`, and the code is under `internal/hostclaim`, `internal/hostops`, `internal/hostguard`, `internal/hostbox` and `internal/hostrelocate`). Tasks 1 to 6 are built and reviewed, at 4879c1e5; Task 7 had just been dispatched. 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 nearest model rule is `reloc-name-before-pin`; check that the model also drops that target from the barrier.

+- 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 `progress.md` 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.

+## 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 sweep caught 118 rules and read 39 as expected misses, with 0 errors. The five lines it flagged were answered afterwards by editing only the expectation files, and the rules the override covers were rerun alone (exit 0), with no complete second run: `create-choice-once` and `reloc-replacement-table` are caught by the sweep, so df1a5f20 dropped their `missed` lines; `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). With those five reclassified, no rule is unexpected: the sweep's 118 catches plus the three that now read as caught are 121 caught, and its 39 expected misses plus the two the override adds are 41 expected. All 54 region HA rules are caught or expected. The sweep's own exit 1 and the five lines above 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.

+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.

+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`?

+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?

+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?

+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?

+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?

+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?

+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?

+## 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.