carlos / platform Public

sim: reloc-name-drops-move-target is a liveness guard: its witness is dropped and expected-outcomes.two-box.txt records it missed, with TestConvertedMoveDropsTheMoveTargetFromTheBarrier as its direct test

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

Paul Campbell pushed by claude 2 weeks ago cdbfa1f736b2d9e12f80d380a5ce2f9fcb9b4c45 parent 819a76c

6 files changed, +22 −38

internal/sim/hostlife/expected-outcomes.two-box.txt +1 −0
internal/sim/hostlife/regionha_round1_test.go +19 −0
internal/sim/hostlife/regionha_test.go +1 −1
internal/sim/hostlife/regionha_witness_test.go +0 −34
internal/sim/hostlife/rules_test.go +1 −1
internal/sim/hostlife/witness_test.go +0 −2

diff --git a/internal/sim/hostlife/expected-outcomes.two-box.txt b/internal/sim/hostlife/expected-outcomes.two-box.txt

index ee551b1d0..e087c74b1 100644

--- a/internal/sim/hostlife/expected-outcomes.two-box.txt

+++ b/internal/sim/hostlife/expected-outcomes.two-box.txt

@@ -9,3 +9,4 @@ source-readiness missed at two boxes the sweep reaches it 0 of 3000; at one box

exec-writer rare 30000 caught at two boxes by the random sweep only rarely (1 / 3000, seed 2319: INV-11 generation.json published before its snapshot landed), so a 3,000-seed sweep may miss it by chance; the base line's one-box miss does not hold here

create-choice-once - caught at two boxes by the random sweep (239 / 3000, first seed 250); the base line's one-box miss does not hold here (TestCreateNamesItsExecutorOnce also fails under the mutation)

reloc-replacement-table rare 30000 caught at two boxes by the random sweep only rarely (2 / 3000, first seed 2854), so a 3,000-seed sweep may miss it by chance; the base line's one-box miss does not hold here (TestL18NestedFailover also fails under the mutation)

+reloc-name-drops-move-target missed liveness: under the mutation a converted move's own target stays on the barrier, which stalls only when that box never acknowledges; the sweep never terminates a move's participants (plan ruling 15) and its controllers acknowledge within a step of the conversion; TestConvertedMoveDropsTheMoveTargetFromTheBarrier stops the move's target and fails under the mutation

diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go

index fba56eb3c..0f8555f01 100644

--- a/internal/sim/hostlife/regionha_round1_test.go

+++ b/internal/sim/hostlife/regionha_round1_test.go

@@ -605,6 +605,25 @@ func TestConvertedMoveWaitsForATargetBeforeItsPin(t *testing.T) {

w.mustHold(t)

}

+// convertedMoveTargetStopped converts a move (convertedMove: the source,

+// box 0, is terminated before the flip) and stops the move's own target,

+// the one participant the conversion left, before it acknowledges; it

+// returns that box. Stopped is not terminated: nothing fences it, and

+// it never acknowledges the converted operation.

+func (w *world) convertedMoveTargetStopped(t *testing.T) *box {

+ w.convertedMove(t, nil)

+ c := w.claim

+ if len(c.Op.Parts) != 1 || len(c.Op.Acks) != 0 || c.Op.Tgt >= 0 {

+ t.Fatalf("not a converted move whose one participant is the move's target: %s", w.state())

+ }

+ mt := w.boxByID(c.Op.Parts[0])

+ if mt == nil || mt.Region == c.Op.SrcRegion {

+ t.Fatalf("the converted move's participant %d is not the move's target in another region: %s", c.Op.Parts[0], w.state())

+ }

+ w.stop(mt)

+ return mt

// TestConvertedMoveDropsTheMoveTargetFromTheBarrier

// (reloc-name-drops-move-target; final review Important 1, 1b-next

// 151261fe): the move's source is terminated before the flip, and the

diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go

index 92840e779..2d325bb8f 100644

--- a/internal/sim/hostlife/regionha_test.go

+++ b/internal/sim/hostlife/regionha_test.go

@@ -828,7 +828,7 @@ func (w *world) relocPinning(b *box, c *claim) {

// which only a converted move leaves there. The mutation keeps it, and

// the barrier waits for a box that may never acknowledge: a stopped move

// target holds the relocation at pinning with no deadline and no stuck

-// (INV-3; TestConvertedMoveDropsTheMoveTargetFromTheBarrier).

+// (a liveness guard: TestConvertedMoveDropsTheMoveTargetFromTheBarrier).

func (w *world) relocNameTarget(c *claim) {

op := c.Op

to := w.chooseBoxExcept(op.SrcRegion, c.Holder.App, relocExcept(op)...)

diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go

index 9124cbb92..15b0c012e 100644

--- a/internal/sim/hostlife/regionha_witness_test.go

+++ b/internal/sim/hostlife/regionha_witness_test.go

@@ -966,40 +966,6 @@ func wPushKeepsLiveFiles(t *testing.T, w *world) {

w.finish(t)

}

-// convertedMoveTargetStopped converts a move (convertedMove: the source,

-// box 0, is terminated before the flip) and stops the move's own target,

-// the one participant the conversion left, before it acknowledges; it

-// returns that box. Stopped is not terminated: nothing fences it, and

-// it never acknowledges the converted operation.

-func (w *world) convertedMoveTargetStopped(t *testing.T) *box {

- w.convertedMove(t, nil)

- c := w.claim

- if len(c.Op.Parts) != 1 || len(c.Op.Acks) != 0 || c.Op.Tgt >= 0 {

- t.Fatalf("not a converted move whose one participant is the move's target: %s", w.state())

- }

- mt := w.boxByID(c.Op.Parts[0])

- if mt == nil || mt.Region == c.Op.SrcRegion {

- t.Fatalf("the converted move's participant %d is not the move's target in another region: %s", c.Op.Parts[0], w.state())

- }

- w.stop(mt)

- return mt

-// wConvertedMoveTargetStopped (reloc-name-drops-move-target; final

-// review Important 1, 1b-next 151261fe): a move's source is terminated

-// before the flip, the move converts to a relocation at pinning, and the

-// move's target in region 1 is stopped before it acknowledges. Naming

-// the region's other box takes the move's target off the barrier in the

-// same CAS, and the host serves on the named box; without the rule the

-// barrier waits for the stopped box, with no deadline and no stuck, and

-// nothing moves (INV-3).

-func wConvertedMoveTargetStopped(t *testing.T, w *world) {

- w.twoBox()

- w.convertedMoveTargetStopped(t)

- w.servingOn(t, nil)

- w.finish(t)

// wParkEvidenceEveryBox (park-evidence-every-box; final review Important

// 2, the shape of two-box seed 819): the host serves on box 0 with an

// acknowledged write its replicator has not shipped, and a delete

diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go

index bfe2660e6..d1c5f5b8c 100644

--- a/internal/sim/hostlife/rules_test.go

+++ b/internal/sim/hostlife/rules_test.go

@@ -204,6 +204,6 @@ var allRules = []string{

"reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin)

"reloc-failover-start-guard", // rev 7 (Astra round 4 finding 3; 1b-next rev 19 Worker.Start, StartRelocation): a serving executor's failover starts only with an eligible target, the app admitting the registration (and its recheck) and RelocationStartGuard with the source fenced; the mutation starts at once (TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica)

"reloc-failover-ack-before-pin", // rev 5 and 6 (Astra rounds 2 and 3; 1b-next rev 19 PinFailover): an initial failover (op.PinFailover, the model's starting) selects its pin only after the target is named and every participant acknowledged; converted moves, nested failovers and replays pin first, as Worker.pinning does; the mutation pins first, and a manifest that lands while the target's controller is unavailable is left out (a loss bound: TestFailoverPinWaitsForTheAcknowledgement)

- "reloc-name-drops-move-target", // final review Important 1 (1b-next 151261fe, NameTarget; moves §7.10, region HA §5.8): naming a converted move's same-region target takes the move's own target (move_target_box, in the other region) off the participants in the same CAS; the mutation keeps it on the barrier, and a stopped move target holds the relocation at pinning for ever (INV-3; TestConvertedMoveDropsTheMoveTargetFromTheBarrier, witness)

+ "reloc-name-drops-move-target", // final review Important 1 (1b-next 151261fe, NameTarget; moves §7.10, region HA §5.8): naming a converted move's same-region target takes the move's own target (move_target_box, in the other region) off the participants in the same CAS; the mutation keeps it on the barrier, and a stopped move target holds the relocation at pinning for ever (liveness, expected miss; TestConvertedMoveDropsTheMoveTargetFromTheBarrier)

"park-evidence-every-box", // final review Important 2 (cf566b41; hostops RetirementEvidence.VerifyObligation, collectEvidence over the inventory; claim §6.2a): in a two-box region a park-replica or park-superseded run by a box that is not the executor waits for every live box of the region not on lost to publish its stop evidence for the operation; the mutation parks on the owner's evidence alone, and the sibling writer's replicator ships into the parked region (INV-10, seed 819; witness)

}

diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go

index b8edfad44..4cb78f896 100644

--- a/internal/sim/hostlife/witness_test.go

+++ b/internal/sim/hostlife/witness_test.go

@@ -261,8 +261,6 @@ var witnesses = []witness{

// the final review's fixes

{"park-evidence-every-box", "park-evidence-every-box", "freed with residue",

"two-box seed 819: a delete's regional park-replica is run by the writer's sibling while the writer's replicator still runs; with the rule it waits for the writer's own stop evidence, without it the region is parked and the writer's next shipment is residue when the host is freed (INV-10)", wParkEvidenceEveryBox},

- {"reloc-name-drops-move-target", "reloc-name-drops-move-target", "INV-3",

- "1b-next 151261fe: a move converts to a relocation when its source is terminated before the flip, and the move's target in the other region is stopped before it acknowledges; naming the region's other box takes the move's target off the barrier and the host serves there, without the rule the barrier waits for the stopped box for ever", wConvertedMoveTargetStopped},

}

// TestWitnesses is the deterministic half of the mutation evidence.