amadan
docs: the diagnosis of the unmutated two-box sweep failures, for the joint round
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
1 file changed,
+175
−0
docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md+175 −0
diff --git a/docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md b/docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md| new file mode 100644 |
| index 000000000..0fe3075df |
| --- /dev/null |
| +++ b/docs/superpowers/notes/2026-10-08-region-ha-two-box-sweep-diagnosis.md |
| @@ -0,0 +1,175 @@ |
| +<!-- Task 6 diagnosis of the unmutated two-box failures (seeds 819, 1674, 2106, 2627, 236), copied unedited from the build ledger for the joint round. --> |
| +# Task 6 diagnosis: the four unmutated two-box INV-10 seeds |
| + |
| +HEAD cf1a2bd5 (region-ha-two-box-build). Read-only for code. Instrumentation and the fix trials ran on `git archive` copies under $TMPDIR, since removed. Single seeds only, `nice -n 19`, `GOCACHE=$TMPDIR/gocache`. |
| + |
| +## Verdict |
| + |
| +There are two causes, not one. |
| + |
| +| seed | residue INV-10 reports | cause | class | |
| +|---|---|---|---| |
| +| 2106 | `r1:instances/h/files/m-000001`. Files manifest, generation `""` (origin), seq 1, v5, landed t=6. | A park-generation kept it while it was live. It went obsolete later, and nothing but the at-rest sweep retires it. | (c) oracle | |
| +| 1674 | `r2:instances/h/15/g-push26/files/m-000001`. Files manifest, generation `push26`, seq 1, v12, landed t=1565. | same | (c) oracle | |
| +| 2627 | `r1:instances/h/files/objects/7-1`. Files object (key 7, env 1), generation `""`, v4, landed t=6. | same (an object, kept because it was referenced) | (c) oracle | |
| +| 819 | `r2:instances/h/0000/…03-…03.ltx` (v34, t=405) and `…04-…04.ltx` (v35, t=413). Legacy-location level-0 LTX, generation `""`. | A delete's regional park-replica ran on the sibling box with only its own stop evidence. The writer kept replicating after the park. | (a) model-only | |
| + |
| +How to reproduce: build `go test -c -o $BIN ./internal/sim/hostlife/`, then run `HOSTLIFE_BOXES=2 HOSTLIFE_SEED=<n> $BIN -test.run '^TestHostLifecycle$' -test.v` (sim_test.go `sweep()`: `HOSTLIFE_SEED` runs one seed verbose and prints its trace). All four reproduce exactly as in the sweep log. |
| + |
| +## Cause 1 (seeds 2106, 1674, 2627): obsolete files keys, class (c) |
| + |
| +### Mechanism |
| + |
| +`doObligation`'s park-generation keep (protocol_test.go, the `o.Kind == "park-generation"` block) is `genOf(o.Prefix,k) != retire || w.filesLive(w.claim,k) || …`. A dead generation's manifest or object that is still in the files live set is kept. That is correct, and spec-mandated. Being in the live set means one of two things: |
| +- it is the newest landed manifest of the admitted chain (`newestManifest` walks `genParent`, so a generation with no manifest yet inherits its predecessor's), or |
| +- a live manifest references it (`objectReferenced`). |
| + |
| +The chore then completes. Later the kept key leaves the live set: a newer generation publishes its own manifest, or the last manifest that referenced the object is parked. No chore covers it any more. The only retirer is the at-rest `sweep()` (moves_test.go). That runs only when the claim is `serving` and the box owns no obligation. INV-10 at the next operation's release (`release()` in moves_test.go, `residueAtEnd`) reports the key unless an open park still covers its prefix (`owed`). |
| + |
| +Instrumented traces (DIAG = keep decisions and PUT/delete landings): |
| +- **2106.** At t=6 legacy box 1 publishes `files/m-000001` and `files/objects/7-1` (gen `""`). At t=78 the cold admission `rec10` supersedes `""`. ob11 (park-generation `""`) runs at t=83 and t=87 and keeps `files/m-000001` (filesLive=true, because rec10 has no manifest yet); it finishes at t=144. At t=156 `g-rec10/files/m-000001` lands, so `""`'s manifest is now obsolete. rl12 pins rec10's manifest, not `""`'s, so `relocationLeftovers`' pinned-manifest park (regionha_test.go:603-628) queues ob14 for rec10, not for `""`. The serving windows between operations are too short for `sweep()`: ob14 holds region 1's boxes until t=616, and mv16 starts at t=619. mv16 (rolled back) releases at t=2589 just after its last chore (ob26, t=2586) is acknowledged. The result is INV-10. The key is deleted at t=2770 by the later delete's parking. |
| +- **1674.** At t=1565 push26 publishes `g-push26/files/m-000001`. At t=1612 the cold admission rec32 (during mv31) supersedes push26. ob33 (park-generation push26) keeps the manifest (filesLive=true, because rec32 has none) and finishes at t=1912. At t=2774 `g-rb36/files/m-000000` lands (the rollback's return install), so push26's manifest is now obsolete. mv31 releases at t=3352 and INV-10 fires. Deleted at t=3585. |
| +- **2627.** `files/objects/7-1` (gen `""`) is kept by ob12 (park-generation `""`, t=1217 and t=1246) and by the push and return parks (`keepFilesLive`), because `g-push11/files/m-000001` references it. ob20 parks push11's manifest (deleted at t=2842). The rollback had already uploaded its own `g-mv15/files/objects/7-1` (t=2693) for `g-rb16/files/m-000000`, so the gen-`""` object is now unreferenced. mv15 releases at t=3849 and INV-10 fires. It is retired at t=4030 by a park-sweep. |
| + |
| +### Why (c) |
| + |
| +- Region HA spec 1 §5.6 (docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:633-643): a dead generation's `files/<generation>/` "is retired with that generation, by the `park-generation` chore … **except objects that a manifest in the live set still names** (L13) … The at-rest sweep treats `files/` as part of the location". No chore re-parks a kept key when it later drops out of the live set. That is left to the at-rest sweep (claim §6.2a). |
| +- 1b-next rev 19, ruling 21 (plan line 383): the pinned manifest is retained by the pinner. The retained copy is left to the storage follow-up. Ruling 27 (plan line 389) adds an earlier owner only for **abandoned prepared generations**, and states "The at-rest sweep stays the backstop". F3 (plan line 48) is scoped the same way. Neither plan nor spec gives completion (relocation or move) any duty for an obsolete files manifest or object of an older generation. |
| +- The model already admits the abstraction for one path: regionha_test.go:603-612 says "in 1b-next rev 19 completion queues only the local chores and the abandoned prepared generations; an obsolete files manifest is the at-rest sweep's (claim §6.2a) … The model parks it at once so INV-10 can check the residue at completion". That covers only the **pinned** manifest's generation at a **relocation's** completion. These three seeds reach the same state by other routes: a generation superseded by a cold admission or a push, a rollback's return install, and an object rather than a manifest. |
| +- Real code would leave the same keys until its at-rest sweep. That is designed behaviour, not a protocol gap, so this is not (b). INV-10 at an operation's end counts them as residue, which the spec does not require, so the oracle is too strict. |
| + |
| +## Cause 2 (seed 819): the sibling's park-replica, class (a) |
| + |
| +### Mechanism |
| + |
| +At t=23 a legacy host is adopted on box 2 (region 2), and at t=26 `delete del10` starts. `parkingObligations` queues the region-2 park-replica (ob15) as a regional chore. `ownsObligation` gives it to any live box of the region, so box 5, box 2's sibling, runs it. The pre-park check in `doObligation` is: |
| + |
| +```go |
| +if (o.Kind == "park-replica" || o.Kind == "park-superseded") && (c.Op.Exec != b.ID || c.Holder == nil) { |
| + if !w.evidence(b, o.Op) { return } |
| +``` |
| + |
| +`evidence(b, …)` kills and certifies **b's own** process tree. The DIAG at t=93, 224, 266, 357 and 358 shows box 5 passing it while `region box 2 procs=2 row=true db=true`. ob15 parks region 2 and finishes at t=358. Box 2's replicator is still running. It PUTs `0000/…03-…03.ltx` (t=405) and `…04-…04.ltx` (t=413) into region 2. Its own park-local (ob17) stops it only at t=1052. Nothing parks region 2 again, so at `free` (t=2015) INV-10 fires. A later park-sweep retires the keys at t=2291 and t=2541. |
| + |
| +### Why (a) |
| + |
| +- The comment in that block says "the owner first proves **the region's box** runs nothing for the host": a one-box assumption. With one box per region, the chore's owner is the writer, and `evidence` stops it. With two boxes it proves nothing about the sibling. |
| +- The real code collects stop evidence from every box. `hostops.RetirementEvidence.VerifyObligation` → `collectEvidence` → `evidenceBoxes` is the `Inventory`: every roster box, or the touched discovery boxes (internal/hostops/evidence.go:240-272, 336-372; internal/hostops/backfill.go:240-259). `hostclaim/delete.go:74` queues the delete's park-replica as `Owner: "region:"+r`. The real worker cannot park region 2 before box 2's evidence exists. |
| + |
| +## Proposed fix (smallest; trial patch beside this file: task-6-diagnosis.patch, `git apply --check` clean) |
| + |
| +1. **Oracle (cause 1).** Add `SweepOwed bool` to `version` (world_test.go). Add `markSweepOwed(r, k)` (regionha_test.go), which is called: |
| + - in `doObligation`'s park-generation keep (protocol_test.go), when a key of the retiring generation is kept only because `filesLive` holds; |
| + - in `keepFilesLive` (regionha_test.go; it gains a region argument from its three callers in moves_test.go), on the same condition. |
| + |
| + `residueOf(true)` (sim_test.go) skips `SweepOwed` versions as it skips `Straggler`. `residue()` (no exemption) is unchanged, so `final()`'s "residue never retired" and quiescence still require the at-rest sweep to retire them. Only keys a park deliberately left as live are exempt: a `files-live-set*` mutation that archives them marks nothing, and P's own keys are never of the retiring generation. |
| +2. **Model (cause 2).** `evidence()` (protocol_test.go) records `b.StopEvidence[opID] = true` when it certifies. `StopEvidence` is a new box field that `forget()` leaves alone, since it is a published record. In `doObligation`'s park-replica/park-superseded pre-check, `if w.perRegion > 1`, the owner returns until every other live box of the region that is not on `c.Lost` has `StopEvidence[o.Op]`. The writer supplies it when it runs the same regional chore or its park-local. |
| + |
| +Trial results (scratch copies): |
| +- Both fixes: 819, 1674, 2106 and 2627 pass. |
| +- Fix 1 alone: 1674, 2106 and 2627 pass, and the 2106 trace is byte-identical to the unfixed one apart from the VIOLATION line, so the fix is oracle-only. 819 still fails. |
| +- Fix 2 alone: 819 passes. 2106 and 2627 also pass, but only because the extra waits change the schedule. 1674 still fails, so fix 2 does not address cause 1. |
| + |
| +**One-box impact: none.** |
| +- Fix 2 is gated on `perRegion > 1`. |
| +- Fix 1 marks only files keys, and only the two-box shape creates them (`publishFiles`, and `preparedManifestHere` behind `perRegion > 1`). |
| +- Neither touches the RNG. |
| + |
| +Checked: one-box single-seed traces for 1, 76, 388, 819, 1674, 2106 and 2627 are byte-identical between the HEAD and fixed binaries, and so is `TestOneBoxCreateInterruptionTrace`'s `HOSTLIFE_TRACE_OUT`. Not run (per the rules): the 300-seed `TestOneBoxSeedTraces` hash file, the two-box gate, and the 3,000-seed sweep. |
| + |
| +## Follow-ups before Task 7 |
| + |
| +- Fix 2 changes two-box schedules for many seeds. After applying, re-run the two-box gate and one unmutated 3,000-seed two-box sweep. Then re-run the 35 baseline-only region HA rules, and the evidence-related rules `evidence-whole-tree`, `evidence-from-state` and `persisted-park-scope` (their witnesses and the sweep). |
| +- Fix 1 adds an exemption to INV-10. Re-run the files rules alone (`files-live-set`, `files-live-set-moves-parks`, `reloc-abandoned-prepared`) to confirm they are still caught. |
| +- Fix 2's model is scoped to the region (a box PUTs only into its own region's `instances/`, per IAM). The real code is roster-wide. `moves/` parks, which siblings in other regions may write, keep today's owner-only evidence, as the one-box shape already does. |
| + |
| +# Follow-up: seed 236 INV-3 after patch v1 (2026-10-08) |
| + |
| +## Verdict: (b), a latent liveness gap in the model; nothing in the patch is at fault. Fixed in patch v2. |
| + |
| +Patch v1 changes two-box schedules from the first stop-evidence wait onwards. The seed 236 traces at cf1a2bd5 and under v1 part at t≈200, so under v1 seed 236 is a different run. That run reaches a state that cf1a2bd5's code cannot get out of either. |
| +- The SweepOwed change only alters what the oracle reads. |
| +- The sibling-evidence wait never fires in this run (the implementer's print shows this). |
| +- v1 touches none of the code below: `fence()`, `fenceSource`, `relocPinning`, and the operator's resolve. |
| + |
| +## Mechanism (traced with a diagnostic print on a $TMPDIR copy) |
| + |
| +1. rl15 drains box 0 to box 3 in region 0. At t=996 it is stuck because box 3 cannot release. At t=1113 the operator stops box 3. At t=1253 the operator's resolve (console_test.go, the stuck-relocation branch, model ruling 13) replays it from pinning. That sets `Tgt=-1`, `Excluded=nil` and `Resolved=true`, and `Resolved` makes the **source eligible as a target again** (`relocExcept`, regionha_test.go:115-122). |
| +2. Box 3 is lost, so region 0's only eligible box is the source. `relocNameTarget` names **box 0 as the target** (`Src == Tgt == 0`), and the pin lands at t=1264. |
| +3. Box 0 is terminated at t=1391. Box 122 fences it at t=1457. In `fence()`'s CAS switch (regionha_test.go ~1640) the `Src == x.ID` case comes first, so only `fenceSource` runs. At pinning, after the release, that function changes nothing but liveness. The `Tgt == x.ID` case (`replaceTarget`) is never reached, so the CAS puts box 0 on `lost` and leaves `op.Tgt = 0`. |
| +4. From then on `relocPinning` finds `Pin != nil` and `Tgt >= 0`, so it never renames the target. Its `ToInstalling` CAS refuses `contains(n.Lost, to)`. Every pass is a no-op. The diagnostic print at t=3601-6001 shows `src=0 tgt=0 exec=-1 phase=pinning pin=true stuck="" lost=[2 5 1 4 3 0]`, while boxes 122 and 123 are enrolled and eligible (`old=false key=true owesLocal=false`). No obligation is pending, nothing is stuck, so the operator never acts, and the result is INV-3. The "waits at pinning: no box in region 0" line at t=1404 is only the one-time alert from `recoveryPass`. It was raised while the region was empty, before 122 and 123 enrolled, and it is not why the run stalls. |
| + |
| +## Would 1b-next's real worker stall here? No: the state cannot arise. |
| + |
| +- `Worker.next` (plan, `func (w Worker) next`, ≈ line 7110) always excludes `c.Op.Intent["source_box"]`. Ruling 26 (plan line 388) says "a relocation's target is never its source (the start CAS, `replaceTargetSlot`)". |
| +- The same ruling says "the operator's resolve is the claim's: it may return the host to the source, **as the model's ruling 13 does**". The model's `Resolved` re-eligibility is therefore its own stand-in for an operator command that 1b-next does not build. |
| +- The real `Worker.Step` checks the source's fence and the target's fence separately (plan ≈ lines 6935-6960), so a dead target would reach `w.replace` on a later pass. |
| + |
| +So this is a model-only liveness gap. It is reachable only through the model's resolve. |
| + |
| +## Fix (patch v2 = v1 + one hunk), regionha_test.go `fence()` |
| + |
| +```go |
| +case n.Op.Kind == "relocating" && n.Op.Src == x.ID: |
| + w.fenceSource(n, x) |
| + if n.Op.Tgt == x.ID && !w.replaceTarget(n, x) { |
| + return false // no spare yet |
| + } |
| +``` |
| + |
| +When the source fenced is also the named target (only after a resolve), its fence is a target loss as well. The model treats it as one, using the existing replacement table (`replaceTarget`), with its cap and its no-spare bound (`FenceTargetWithoutSpare`, which makes it stuck for the operator). With no spare yet, the fence waits for a later pass, just as the plain target branch does. |
| + |
| +## Checks (copies under $TMPDIR; the worktree's applied v1 is untouched) |
| + |
| +- `task-6-diagnosis.patch` is now v2. `git apply --check` passes on a clean `git archive cf1a2bd5`, and the applied tree matches the tested tree. `task-6-diagnosis-delta.patch` is the single hunk on top of v1; `git apply --check` passes against the worktree as it stands. |
| +- gofmt is clean and vet is ok. `TestWitnesses` (unmutated) passes. |
| +- Two-box single seeds 236, 819, 1674, 2106 and 2627 all pass. |
| + - 236 now passes the 1457 fence; box 122 is then named. After further losses rl15 completes on box 123 at t=2019, and the host is freed at t=3582. |
| + - 819, 1674, 2106 and 2627: the traces are byte-identical to v1's. |
| +- One-box single seeds 1, 236, 819, 1674, 2106 and 2627, and `TestOneBoxCreateInterruptionTrace`, are byte-identical between cf1a2bd5 and v2. |
| + |
| +**One-box impact.** None in practice. The hunk changes behaviour only when `Src == Tgt == x` at a fence. In either shape the old code then stalls for ever: no stuck flag is set, so no operator resolve follows, and INV-3 fires. The one-box 3,000-seed run is clean, so no one-box seed there reaches the branch. The hunk is not gated on `perRegion`, so one-box also loses the latent stall. If the gate's 300-seed `TestOneBoxSeedTraces` hash file ever differs, gate it on `w.perRegion > 1`. Not run here (single seeds only): the gate, `TestOneBoxSeedTraces`, and the 3,000-seed runs. |
| + |
| +**Note for expected-outcomes.** v2 adds no rule. `reloc-replacement-cap`, `reloc-dead-target-bound` and `operator-stop-unrecoverable-only` now also guard this path, so read their sweep results again after the rerun. |
| + |
| +# Follow-up 2: excluding the source at every target choice (coordinator ruling, 2026-10-08) |
| + |
| +## The target-choice sites, and how each maps to `Worker.next` |
| + |
| +| model site (cf1a2bd5) | what it chooses | 1b-next | excludes the source at HEAD? | |
| +|---|---|---|---| |
| +| regionha_test.go:51, drain start: `chooseBoxExcept(from.Region, app, from.ID)` | a drain's target | `Worker.Start`'s eligible target; the start CAS (ruling 26) | yes, always | |
| +| regionha_test.go:1808, `failoverStart`: `chooseBoxExcept(x.Region, app, x.ID)` | a failover's target | `Worker.Start` with a fence | yes, always | |
| +| regionha_test.go:829, `relocNameTarget`: `relocExcept(op)` | the target named at pinning (converted move, resolve replay) | `Worker.pinning` → `w.next` → `NameTarget` | yes, **unless `op.Resolved`** | |
| +| regionha_test.go:1269, probe-failed nested: `relocExcept(op, op.Exec)` | the nested relocation's target | `Worker.Step` probe-failed → `w.next` | yes, **unless `op.Resolved`** | |
| +| regionha_test.go:1886, `replaceTarget`: `relocExcept(n.Op, x.ID)` | a dead target's replacement | `Worker.replace` → `w.next` | yes, **unless `op.Resolved`** | |
| + |
| +console_test.go:429 chooses a move's target in another region, which is not a relocation choice. The only way the source gets back in is `relocExcept`'s `if !op.Resolved`, which only the operator's resolve sets (console_test.go:1287, model ruling 13). Every automatic path already excludes the source, exactly as `Worker.next` does. |
| + |
| +## Tried: `relocExcept` always excludes `op.Src` (with `Resolved` kept only for "an empty listing is accepted") |
| + |
| +Built as `task-6-diagnosis-srcexcl.patch` (v1 + the change + comments; applies cleanly to cf1a2bd5). With it, Src == Tgt cannot occur. The only other place that sets `Tgt == Src` is a `pushing` op, which never becomes `relocating`. So the `fence()` hunk is not needed. Results: |
| +- **Pass:** |
| + - Two-box seeds 236, 819, 1674, 2106 and 2627 all pass. 236 passes without the `fence()` hunk. |
| + - One-box seed 1 is byte-identical. |
| + - The 300-seed `TestOneBoxSeedTraces` matches `$TMPDIR/twobox/baseline-seeds.txt`. |
| +- **Fail: three deterministic tests (ruling 26's operator path).** They are `TestProbeFailedInATwoBoxRegion`, witness `reloc-no-spare-bound` (`wNoSpareBound`) and witness `reloc-dead-target-bound` (`wDeadTargetBound`). All three violate INV-3 with the rule ON. Each scenario is a two-box region whose target fails or dies, with no spare. The bound makes the operation stuck. The operator's resolve then replays it from pinning, but with the source excluded and no spare, nothing is eligible, so it waits for ever. |
| + |
| + These witnesses tell the rule apart from its mutation only because the resolve can return the host to the source. Plan ruling 26 (line 388) relies on exactly that: "It alerts, and the op waits for `carlos ops host resolve` … The operator's resolve is the claim's: it may return the host to the source, as the model's ruling 13 does." With the source excluded, rule and mutation both end in INV-3, so the witnesses stop working. |
| + |
| + The same stall should show up in the random two-box sweep. A quarter of second boxes have `FailApp`, so a drain onto one in a region with no spare ends at the same operator replay. |
| + |
| +## Conclusion and recommendation |
| + |
| +1b-next's automatic paths cannot produce Src == Tgt, and the model's automatic paths already match them. The model produces it only through ruling 13's resolve, which models "return the host to the source" as **naming the source as a relocation target**. That is the root cause. But simply excluding the source there removes the operator's only way out that ruling 26 relies on, and it breaks three tests. To exclude the source from the resolve and keep liveness, the model needs a separate operator transition that returns the host to the source **without naming it as a target**. For example: abandon the relocation and serve on the source with a fresh stamp, so its wake runs a cold admission from `holder.generation`. That is a new operator action outside 1b-next, it needs a ruling, and its effects would need witness and sweep coverage. I have not built it. |
| + |
| +Options: |
| +1. **Keep v2** (`task-6-diagnosis.patch`, unchanged): the resolve still names the source (ruling 13 as written), and the `fence()` hunk handles its one aftermath (the source fenced while it is the named target). All checks pass: |
| + - `git apply --check` is clean. |
| + - gofmt and vet are clean. |
| + - Every non-sweep test passes (witnesses and cases included). |
| + - Seeds 236, 819, 1674, 2106 and 2627 pass with two boxes. |
| + - One-box seed 1, the 300-seed hashes and the interruption trace are byte-identical to `$TMPDIR/twobox/baseline-*`. |
| +2. **Source exclusion everywhere** (`task-6-diagnosis-srcexcl.patch`): this follows the ruling literally, but it fails the three ruling-26 tests and probably fails sweep liveness. It needs a ruling on how the operator's "return to the source" works, plus that transition, before it can be used. |
| + |
| +`task-6-diagnosis.patch` is left as v2, because the requested revision does not pass verification. The worktree is untouched. |