amadan
sim: the region-wide stop-evidence wait before a two-box park-replica or park-superseded is the named rule park-evidence-every-box, with a witness of seed 819's shape that violates INV-10 under its mutation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
4 files changed,
+45
−2
internal/sim/hostlife/protocol_test.go+5 −2internal/sim/hostlife/regionha_witness_test.go+37 −0internal/sim/hostlife/rules_test.go+1 −0internal/sim/hostlife/witness_test.go+2 −0
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 3efe4951e..f01ff161e 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -2285,10 +2285,13 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if !w.evidence(b, o.Op) { |
| return |
| } |
| - if w.perRegion > 1 { |
| + if w.perRegion > 1 && on("park-evidence-every-box") { |
| // every box of the region publishes its own stop evidence |
| // (hostops collectEvidence over the inventory); the owner's |
| - // alone proves nothing about its sibling |
| + // alone proves nothing about its sibling. The mutation |
| + // parks on the owner's evidence alone, and a sibling |
| + // writer's replicator ships into the parked region |
| + // (seed 819; wParkEvidenceEveryBox) |
| for _, x := range w.regionBoxes(b.Region) { |
| if x != b && !contains(c.Lost, x.ID) && !x.StopEvidence[o.Op] { |
| return |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index 4195f2778..9124cbb92 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -999,3 +999,40 @@ func wConvertedMoveTargetStopped(t *testing.T, w *world) { |
| 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 |
| +// begins. Region 0's park-replica is a regional chore, and box 3, the |
| +// sibling, runs it while box 0's agent does nothing (its replicator, a |
| +// process of its own, still runs). With the rule box 3 waits for box 0's |
| +// stop evidence, which comes only when box 0's agent acts, and the park |
| +// covers the write; without it box 3 parks region 0 on its own evidence, |
| +// box 0's replicator then ships the write into the parked region, and the |
| +// host is freed with it as residue (INV-10). |
| +func wParkEvidenceEveryBox(t *testing.T, w *world) { |
| + w.twoBox() |
| + writer, sib := w.boxes[0], w.boxes[3] |
| + w.serve(writer, 1, app0) |
| + w.running(t, writer) |
| + w.appWrite(writer) |
| + w.userDelete() |
| + if w.claim.Op.Kind != "deleting" { |
| + t.Fatalf("witness: the delete did not begin: %s", w.state()) |
| + } |
| + owed := func() bool { |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-replica" && o.Region == writer.Region && o.Prefix == w.claim.Holder.Location { |
| + return true |
| + } |
| + } |
| + return false |
| + } |
| + if !w.reach(t, 50, "region 0's park-replica queued", owed, w.runConsole) { |
| + return |
| + } |
| + w.drive(6*horizonH, func() bool { return !owed() }, w.runConsole, w.act(sib), w.recoveryPass) |
| + w.logf("witness: box 0's replicator ships its queue") |
| + w.replicate(writer) |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 892fdf82a..baa39e93d 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -205,4 +205,5 @@ var allRules = []string{ |
| "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) |
| + "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 96d461349..b8edfad44 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -259,6 +259,8 @@ var witnesses = []witness{ |
| {"reloc-dead-target-bound", "reloc-dead-target-bound", "INV-3", |
| "rev 18 finding 2: the target dies at installing and no spare is launched; with the bound the fence is consumed into stuck and the operator's replay serves on the source, without it nothing moves", wDeadTargetBound}, |
| // 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}, |
| } |