amadan
docs: region HA plan 1b-next rev 19 removes a box mid-relocation in the property and asserts the chooser's hash winner
Astra round 18: two P2 test gaps, both accepted. The lifecycle property gains same-operation replacement events, plus a scripted run of round 18's trace: probe fails, release, replaced, cleanup blocked, crash. Its oracle now requires participating boxes to be ready and excluded boxes to have no controller, record or journal entry left, with no reopening. 200 seeds pass, and mutations still kill the lifecycle guards. The chooser test computes the equal-load hash winners independently for two hostnames that pick opposite boxes; a constant hostname fails it. No production defect was found. Dry-run in task order on 3407d114.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+133
−8
docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md+133 −8
diff --git a/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md b/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md| index 954891827..42a0b7d80 100644 |
| --- a/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md |
| +++ b/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md |
| @@ -1,4 +1,4 @@ |
| -# Region HA 1b-next: Relocation, Row Cases, Create Choice and Fences Implementation Plan (rev 18) |
| +# Region HA 1b-next: Relocation, Row Cases, Create Choice and Fences Implementation Plan (rev 19) |
| > **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. |
| @@ -10,6 +10,17 @@ |
| **Spec:** `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md`, rev 5.4 with §24 (rulings H1 to H19 final). Read §0, §2, §5.2, §5.3, §5.8, §5.9, §5.10, §9 (L1 to L20, accepted) and §24 first. Then the claim spec rev 6.30 on `origin/design-replica-ownership` (`docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`): §1.1's activation gate, §4 ("Same-region relocation (L1)" and the relocation exception to CC11), §5.1 and P5-D2/P5-D6 (the create intent), §6.1 ("Release before full stop (L10)"), §6.4a item 2 (`released`), §7.3 D2 ("Automatic termination (L2, L4)", "The fence's journal reference") and D4 ("Automatic loss persistence"). Then moves rev 7.22 on `origin/design-moves-any-region` §7.6 ("One install routine, two sources", L16 and L17) and §7.10 (the pre-flip conversion). The contracts note `docs/superpowers/notes/2026-10-07-region-ha-contracts.md` gives `hostfiles` v2, `CopyManifest`, `Publish` and `boxchoice`. Plan 1b (`docs/superpowers/plans/2026-10-06-region-ha-1b-claim-readers.md`) lists in "Waits for the claim" what this plan now builds. |
| +## Rev 19: round 18 dispositions |
| + |
| +Astra's round 18 (`CODEX-PLAN-REGION-HA-1BN-R18.md`) resolved all three round 17 findings, accepted rulings 1 to 27, and raised two P2 test gaps. Both were checked against the plan's tests and accepted; none is declined. Neither exposed a production defect: the new events and oracle found no failing seed in the unchanged code. Stage A was dry-run on a clean 3407d114 in task order. The lifecycle property passed 200 seeds, niced, and then each lifecycle guard was removed in turn. |
| + |
| +| # | Stage | Evidence checked | Disposition | What changed | Where | |
| +|---|---|---|---|---|---| |
| +| 1 (P2) | A | The property's events only started and completed operations. Its recovery oracle wanted every relocation to be ready again on this box. So it could not express a box excluded from an operation that goes on, and it would have rejected correct recovery there. | accepted | New events: `replaced` (this box, the target, is replaced within the same operation by `sp2`, and the relocation continues) and `probeFailedAndReleased`. In every fourth seed, a script follows round 18's trace: target installed, probe fails, release journaled, replaced, cleanup blocked, a pass, an agent crash, then the random events and recovery. The oracle now asks a participating box to be ready, and an excluded box to have finished its cleanup: no controller, no hostexec record, no journaled participation, with the operation still running. New invariant (i): nothing for an operation opens again on a box excluded from it. Invariants (a), cleanup before clear, and (h), persistence across a crash, stay. | Task 7 (`TestRelocationControllerLifecycleProperties`) | |
| +| 2 (P2) | A | `TestExecutorChooserSpreadsThenBalancesThenHashes` took the first choice as given and derived its later expectations from it. A chooser that hashed a constant instead of the record's host passed. | accepted | `TestExecutorChooserHashesTheRecordsHostOnEqualLoads` uses equal loads. It computes the winner independently (the greatest SHA-256 of host + "\x00" + box id, claim P5-D2) for `shop.bab.oncarlos.com` (box-b) and `cafe.bab.oncarlos.com` (box-a). The test itself asserts that the two winners differ, and requires `Choose` to return each one. Substituting a constant hostname in `ExecutorChooser.Choose` fails it (cafe chose box-b). | Task 2 | |
| + |
| +Mutation check (property at 200 seeds, `-failfast`): `Sweep` finishing a participation whose box is excluded, killed at seed 4 (the excluded box never finishes its cleanup). Rev 14's guards, rechecked under the new events, were all killed again: the cleanup before a clear (seed 1, (a)), the verified forget (seed 3, (b)), lost-controller recovery (seed 10), the journal before the open (seed 1, (b)), the close before the clear (seed 6), and the restart path's verification (seed 1, (b)). |
| + |
| ## Rev 18: round 17 dispositions |
| Astra's round 17 (`CODEX-PLAN-REGION-HA-1BN-R17.md`) rated F1 to F3 as only partly closed, with one P1 and two P2s. It accepted ruling 26 and its cost. All three findings were checked against the rev 17 code, reproduced, and accepted; none is declined. |
| @@ -404,7 +415,7 @@ Left out, with where it goes: |
| - **Go environment.** `GOFLAGS=-buildvcs=false`. Leave `GOCACHE` at its default; if the sandbox refuses it, `GOCACHE=$TMPDIR/gocache` for that command. Socket tests need `TMPDIR=/tmp/k` (`mkdir -p /tmp/k`). Run tests niced (`nice -n 19`), targeted with `-run`; never the full `-race` suite, and no simulation sweeps. Scratch goes under `$TMPDIR`. |
| - **Gate before each commit:** `go build ./... && go vet ./<pkgs>/ && gofmt -l <dirs>` (empty), the task's targeted tests, then `GOOS=darwin go build ./... && GOOS=windows go build ./...`. (`GOOS=windows go vet ./internal/...` fails on main's own test files, `release/versions_test.go`, `appconfig/syncexec_test.go` and `activator/activator_test.go`; vet the task's packages instead.) |
| - Commit messages: lowercase `area:` prefix and a sentence stating the behaviour, then a blank line and `Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>`. Work on a branch cut from `origin/main` (suggested `region-ha-1b-next`). Merging is Paul's call, through `amadan branch merge`, and only after Task 11. |
| -- **Dry run.** Tasks 1 to 7 were applied in order to `origin/main` at 3407d114, built, vetted, cross-built for darwin, windows and linux/arm64, and their tests run; nineteen guards were each removed in turn and their test watched to fail (rev 1), then rev 2's twenty-five, rev 3's eleven, rev 4's eight, rev 5's seven, rev 6's eleven, rev 7's three, rev 8's two, rev 9's two, rev 10's one, rev 11's four, rev 12's four, rev 13's four, rev 14's ten killed mutations of the lifecycle property, rev 15's twelve, rev 16's, rev 17's eight and rev 18's five (listed in the Self-review); from rev 10 on, stage A is also applied one task at a time in plan order, building and testing after each. Then the code was removed; only this document is committed. |
| +- **Dry run.** Tasks 1 to 7 were applied in order to `origin/main` at 3407d114, built, vetted, cross-built for darwin, windows and linux/arm64, and their tests run; nineteen guards were each removed in turn and their test watched to fail (rev 1), then rev 2's twenty-five, rev 3's eleven, rev 4's eight, rev 5's seven, rev 6's eleven, rev 7's three, rev 8's two, rev 9's two, rev 10's one, rev 11's four, rev 12's four, rev 13's four, rev 14's ten killed mutations of the lifecycle property, rev 15's twelve, rev 16's, rev 17's eight, rev 18's five and rev 19's two (listed in the Self-review); from rev 10 on, stage A is also applied one task at a time in plan order, building and testing after each. Then the code was removed; only this document is committed. |
| ## Review Focus |
| @@ -3018,6 +3029,8 @@ import ( |
| "context" |
| "crypto/ed25519" |
| "crypto/rand" |
| + "crypto/sha256" |
| + "encoding/hex" |
| "encoding/json" |
| "errors" |
| "strings" |
| @@ -3092,6 +3105,36 @@ func TestExecutorChooserSpreadsThenBalancesThenHashes(t *testing.T) { |
| } |
| } |
| +// Round 18 finding 2: with equal loads the winner is the greatest |
| +// SHA-256 of host + "\x00" + box id (claim P5-D2), computed here |
| +// independently of boxchoice. The two hostnames are chosen so that their |
| +// winners differ: a chooser that hashed anything but the record's host |
| +// would get at least one of them wrong. |
| +func TestExecutorChooserHashesTheRecordsHostOnEqualLoads(t *testing.T) { |
| + ctx := context.Background() |
| + winner := func(host string) string { |
| + a := sha256.Sum256([]byte(host + "\x00box-a")) |
| + b := sha256.Sum256([]byte(host + "\x00box-b")) |
| + if hex.EncodeToString(a[:]) > hex.EncodeToString(b[:]) { |
| + return "box-a" |
| + } |
| + return "box-b" |
| + } |
| + hosts := []string{"shop.bab.oncarlos.com", "cafe.bab.oncarlos.com"} |
| + if winner(hosts[0]) == winner(hosts[1]) { |
| + t.Fatal("the fixture's hostnames must choose opposite boxes") |
| + } |
| + for _, host := range hosts { |
| + x, _, _, _ := chooserFixture(t, "box-a", "box-b") |
| + r := chooserRecord() |
| + r.Holder.Host = host |
| + got, err := x.Choose(ctx, hostclaim.Observed{Host: host, Absent: true}, r) |
| + if err != nil || got.Box != winner(host) { |
| + t.Fatalf("%s: chose %+v %v, want %s", host, got, err, winner(host)) |
| + } |
| + } |
| +} |
| + |
| func TestExecutorChooserNeverNamesAFencedLostOrUnknownBox(t *testing.T) { |
| ctx := context.Background() |
| absent := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Absent: true} |
| @@ -9865,6 +9908,9 @@ func newLifeWorld(t *testing.T) *lifeWorld { |
| c.Binding = b |
| // hostexec's own Cleanup hook is the same scoped cleanup, |
| // bound to the binding (Task 8a); it does not count for (a). |
| + if cur := w.current(); cur.Op.ID == b.Op && !slices.Contains(cur.Op.Participants, "src") { |
| + w.violate(fmt.Sprintf("(i) %s opened again after this box was excluded from it", b.Op)) |
| + } |
| gen := w.generation() |
| c.Cleanup = func(context.Context) error { return w.cleanupScoped(context.Background(), b.Op, false, gen) } |
| opened, err := OpenRelocationController(ctx, c) |
| @@ -10043,12 +10089,56 @@ func (w *lifeWorld) startRelocation() { |
| w.ops++ |
| id := fmt.Sprintf("rel-%d", w.ops) |
| from, to := "src", "dst" |
| - if w.current().Op.Exec == "dst" { |
| - from, to = "dst", "src" |
| + if exec := w.current().Op.Exec; exec != "" && exec != "src" && exec != "none" { |
| + from, to = exec, "src" |
| } |
| w.claim(func(c *hostclaim.Claim) error { |
| c.Op = hostclaim.Op{Kind: hostclaim.KindRelocating, ID: id, Phase: hostclaim.PhaseStarting, Exec: from, Participants: []string{from, to}, |
| - Intent: map[string]string{"region": "ie", "source_box": from, "target_box": to, "target_enrollment": map[string]string{"src": strings.Repeat("a", 32), "dst": strings.Repeat("d", 32)}[to]}} |
| + Intent: map[string]string{"region": "ie", "source_box": from, "target_box": to, "target_enrollment": map[string]string{"src": strings.Repeat("a", 32), "dst": strings.Repeat("d", 32), "sp2": strings.Repeat("e", 32)}[to]}} |
| + return nil |
| + }) |
| +} |
| + |
| +// replaced is the worker replacing this box, the target, within the same |
| +// operation (rev 19, round 18 finding 1): after its release in |
| +// probe-failed, or at any target phase, the relocation goes on with sp2 |
| +// and this box is no longer a participant. Its controller, record and |
| +// journal must go, and nothing for this operation may open again here. |
| +func (w *lifeWorld) replaced() bool { |
| + c := w.current() |
| + if c.Op.Kind != hostclaim.KindRelocating || c.Op.Intent["target_box"] != "src" { |
| + return false |
| + } |
| + w.claim(func(c *hostclaim.Claim) error { |
| + if c.Op.Journal == nil { |
| + c.Op.Journal = map[string]string{} |
| + } |
| + c.Op.Participants = append(slices.DeleteFunc(slices.Clone(c.Op.Participants), func(b string) bool { return b == "src" }), "sp2") |
| + c.Op.Intent["target_box"], c.Op.Intent["target_enrollment"] = "sp2", strings.Repeat("e", 32) |
| + if c.Op.Phase != hostclaim.PhaseStarting && c.Op.Phase != hostclaim.PhaseReleasing { |
| + c.Op.Exec, c.Op.Phase = "none", hostclaim.PhasePinning |
| + for _, k := range []string{"local_install", "probe", "prepared", "prepared_opened", "install_stamp", "release", "release.phase", "probing_since", "probe_failed_since"} { |
| + delete(c.Op.Journal, k) |
| + } |
| + } |
| + c.Op.Journal["excluded_targets"] = `["src"]` |
| + c.Op.Journal["exec_ack.sp2"] = "{}" |
| + return nil |
| + }) |
| + return true |
| +} |
| + |
| +// probeFailedAndReleased moves this box, the target, to probe-failed with |
| +// its release journaled (the worker's and its own half, in short). |
| +func (w *lifeWorld) probeFailedAndReleased() { |
| + w.claim(func(c *hostclaim.Claim) error { |
| + if c.Op.Journal == nil { |
| + c.Op.Journal = map[string]string{} |
| + } |
| + c.Op.Phase = hostclaim.PhaseProbeFailed |
| + c.Op.Journal["probe_failed_since"] = w.clock.wall.Format(time.RFC3339Nano) |
| + c.Op.Journal["release"] = `{"released_by":"src"}` |
| + c.Op.Journal["release.phase"] = hostclaim.PhaseProbeFailed |
| return nil |
| }) |
| } |
| @@ -10245,7 +10335,12 @@ func (w *lifeWorld) recoverAll() { |
| } |
| func (w *lifeWorld) event(r *rand.Rand) string { |
| - switch n := r.Intn(15); n { |
| + switch n := r.Intn(16); n { |
| + case 15: |
| + if w.replaced() { |
| + return "this box replaced in the same operation" |
| + } |
| + return "no replacement (not the target)" |
| case 14: |
| w.install() |
| return "the target's installation (P built)" |
| @@ -10343,6 +10438,24 @@ func TestRelocationControllerLifecycleProperties(t *testing.T) { |
| if w.current().Op.Journal["local_install"] == "" { |
| t.Fatalf("seed %d: the local install was not journaled: %+v", seed, w.current().Op) |
| } |
| + if seed%4 == 2 { |
| + // Round 18's trace: the target's probe fails, it |
| + // releases, it is replaced while the relocation goes |
| + // on elsewhere, its cleanup blocks, the agent crashes. |
| + w.pass() |
| + w.probeFailedAndReleased() |
| + if !w.replaced() { |
| + t.Fatalf("seed %d: this box was not the target to replace: %+v", seed, w.current().Op) |
| + } |
| + w.mu.Lock() |
| + w.block = make(chan struct{}) |
| + w.mu.Unlock() |
| + w.pass() |
| + w.check("replaced with its cleanup blocked") |
| + w.crash() |
| + w.check("agent crash after the replacement") |
| + trace = append(trace, "probe failed, released, replaced, cleanup blocked, crash") |
| + } |
| } |
| for i := 0; i < 30; i++ { |
| ev := w.event(r) |
| @@ -10355,10 +10468,21 @@ func TestRelocationControllerLifecycleProperties(t *testing.T) { |
| // (e) Faults stop. |
| w.recoverAll() |
| trace = append(trace, "faults stop") |
| + // A participating box is ready again; an excluded one (rev 19) |
| + // has finished its cleanup: no controller, no record, no |
| + // journaled participation, while the relocation goes on. |
| ready := func() bool { |
| c := w.current() |
| - if c.Op.Kind != hostclaim.KindRelocating || !slices.Contains(c.Op.Participants, "src") || c.Op.Journal["exec_ack.src"] == "" { |
| - return c.Op.Kind != hostclaim.KindRelocating |
| + if c.Op.Kind != hostclaim.KindRelocating { |
| + return true |
| + } |
| + if !slices.Contains(c.Op.Participants, "src") { |
| + _, exists, _ := w.record() |
| + retained, err := w.e.Controllers.Retained() |
| + return !exists && err == nil && len(retained) == 0 && len(w.open()) == 0 |
| + } |
| + if c.Op.Journal["exec_ack.src"] == "" { |
| + return false |
| } |
| obs, err := hostclaim.Read(w.ctx, w.inner, w.host) |
| return err == nil && w.e.Ready(w.ctx, obs) == nil |
| @@ -13504,3 +13628,4 @@ Expected: exit 0. Exit 2 is pending: wait and read again. Exit 1: read the log a |
| - **Rev 16 guards** (the table in the Rev 16 dispositions): the stuck-on-lost-receipt step and the exact receipt comparison are killed by their tests; both `EnsureLocal` calls removed together are killed by the property, seed 182. Rev 14's lifecycle guards are killed again under the crash event. |
| - **Rev 17 guards**, each removed in turn and its test watched to fail: the abandoned-P journal in `install`; the serving CAS's park; the opened-P exclusion; `filesPin`'s refusal; the release-evidence exception; the worker's `stuck` on `ErrFilesUnevidenced`; the `probe-failed` bound; the wait before it. Eight in all. |
| - **Rev 18 guards**, each removed in turn and its test watched to fail: the keyless-manifest refusal; the key required only for a nonempty database; the dead-target-without-spare bound; that bound consuming the fence; `ReplaceTarget` recording the unopened P it drops. Five in all. |
| +- **Rev 19 guards**, removed and their tests watched to fail: `Sweep` finishing an excluded participation (the property, seed 4); the record's host as the chooser's hash input (`TestExecutorChooserHashesTheRecordsHostOnEqualLoads`). Two in all. |