carlos / platform Public

sim: the first serving wake after a completion is cold, and a release closes the session's launches at the stop and admission only at Collect

L18 joint round 2 (Astra, model ded69314 against 1b-next b9092a0c).

Finding 1 (P2): the probe stop no longer closes the session cleanly. As
in relocationStopProbe, main's writer-session stop drains the producers
and ends the session with no FlushDB and no certificate. The completed
prior's serving wake refuses PredecessorCertified (claimServingOwners.
Select is always cold), so it admits into a fresh generation at a new
stamp and records the stopped probe session's writes_lost; P is retired by
the park-generation that follows. The N6 witness now asserts all of that.
TestFirstServingWakeIsCold shows a write the probe session acknowledged,
and the replicator had not shipped, declared lost (alerted, every
invariant holding): the built probe stop does not flush, unlike a release.
The drain tests now allow the first serving wake's one declaration, still
of zero writes. reloc-row-cases is back on its original INV-6: the target's
cold first wake activates the stamp the released source's admission
issued.

Finding 3 (P3): StopWriters closes the session's launch journal at the
stop (closeLaunches: the stopped session is never relaunched, an admitted
start abandoned); root's admission fence (relFence) comes only with
Collect, after the flush and the recorded positions. The new rule
reloc-admits-probe-only mirrors relocatingAdmission: a relocating claim
admits only op.exec's cold probe in probing, so no wake admits a writer
between the two, before or after a restart
(TestNoAdmissionBetweenStopAndFence, which fails under the mutation).
reloc-stuck-refuses-admission is now redundant alone:
TestStuckSourceRefusesAdmission fails only with both mutations.

One-box COUNTERS and traces unchanged; unmutated 3,000 two-box seeds,
0 failed.

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

Paul Campbell pushed by claude 1 week ago 917771bbf4a449aa93a5b5a8e6b15bce92baaeb6 parent ded6931

10 files changed, +205 −40

internal/sim/hostlife/ltx_test.go +1 −2
internal/sim/hostlife/protocol_test.go +15 −0
internal/sim/hostlife/regionha_cases_test.go +2 −2
internal/sim/hostlife/regionha_completion_test.go +29 −13
internal/sim/hostlife/regionha_completion_witness_test.go +121 −3
internal/sim/hostlife/regionha_test.go +13 −5
internal/sim/hostlife/regionha_witness_test.go +5 −3
internal/sim/hostlife/rules_test.go +1 −0
internal/sim/hostlife/witness_test.go +2 −2
internal/sim/hostlife/world_test.go +16 −10

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

index cd2e01a8f..0bd85c0f1 100644

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

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

@@ -410,8 +410,7 @@ func (w *world) closeStep(b *box) {

// rollback's source was admitted cold at every wake and the rollback

// never released)

c := w.claim

- inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "moving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting" ||

- c.Op.Kind == "relocating" && c.Op.Phase == "probed") // a relocation's probe stop drains its session (L18 finding 2)

+ inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "moving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting")

if c == nil || c.Holder == nil || !inside || c.Op.Exec != b.ID || c.Holder.Inc != db.Inc || db.Gen != c.Holder.Gen {

// a push, a move's cut, a delete or a purge is taking this writer

// over: its generation is being replaced or parked, and a

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

index c8a803f37..750baf8fd 100644

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

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

@@ -1631,6 +1631,14 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp

w.stats["admission refused: relocation stuck"]++

return a, false

}

+ if c.Op.Kind == "relocating" && !(probe && c.Op.Phase == "probing") && on("reloc-admits-probe-only") {

+ // relocatingAdmission (1b-next generation.go): a relocating claim

+ // admits only op.exec's cold probe in probing; the source in

+ // starting or releasing keeps the session it has and admits no new

+ // one (L18 joint round 2 finding 3)

+ w.stats["admission refused: relocating admits only the probe"]++

+ return a, false

+ }

a.KeepStamp = h.Stamp > h.Session

if !on("admit-everywhere") && c.Op.Kind != "serving" {

a.Mode, a.NewGeneration = "unguarded", want // the mutation: writer sessions for ordinary wakes only (rev 7.8)

@@ -1642,6 +1650,13 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp

bk := w.buckets[b.Region]

a.RemoteMaxTXID = w.remoteMax(bk, dataKey(h.Location, h.Gen, ""))

a.PredecessorCertified = w.certificate(b, c) != nil

+ if w.completedPrior(b, c) {

+ // the first serving wake after a completion (N6) is claimServingOwners'

+ // Select: always cold into a fresh generation, PredecessorCertified

+ // refused, the predecessor's writes_lost recorded; the probe's stop

+ // receipt serves the handover alone (L18 joint round 2 finding 1)

+ a.PredecessorCertified = false

+ }

if want == "" || want == h.Gen || w.ancestorGen(h.Location, h.Gen, want) {

// holder.generation, or an operation's prepared generation that a

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

index e41ba1b01..b1e297d2b 100644

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

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

@@ -97,8 +97,8 @@ func TestL18RelocationByDrain(t *testing.T) {

t.Fatalf("the drain did not start: %s", w.state())

}

w.servingOn(t, to)

- if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] != 0 {

- t.Errorf("released coverage: %d released, %d writes_lost (want 1 and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"])

+ if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] > 1 || w.stats["writes declared lost"] != 0 {

+ t.Errorf("released coverage: %d released, %d writes_lost covering %d writes (want 1, at most the first serving wake's, and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"], w.stats["writes declared lost"])

}

w.finish(t)

if !contains(to.DB.Log, wr) || !contains(to.Timers, id) && !w.delivered[id] {

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

index d081e0ec2..1dc6d77bd 100644

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

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

@@ -88,19 +88,12 @@ func (w *world) relocStopProbe(b *box, c *claim) {

w.stats["probe stop: a process survives"]++

return

}

- // main's writer-session stop drains the producers: the session's own

- // replicator closes cleanly (claim §6.4a), so the next serving wake

- // continues the generation; a replicator that died with its agent

- // certifies nothing, and that wake is cold and declares

- if db := b.DB; db != nil && db.Inc == h.Inc && db.Gen == h.Gen && db.Epoch == b.Epoch && db.Session == h.Session && !b.mem["close:"+owner] {

- b.mem["close:"+owner] = true

- db.Closing = true

- }

- w.closeStep(b)

- if b.DB != nil && b.DB.Closing {

- w.stats["probe stop: waits for the clean close"]++

- return

- }

+ // main's writer-session stop (Wake.Stop, collectCapturedStop) drains

+ // the producers and ends the session; nothing flushes the database

+ // first (the release's FlushDB has no counterpart here) and nothing

+ // certifies it, so writes the probe session acknowledged and the

+ // replicator had not shipped stay local (L18 joint round 2 finding 1:

+ // the first serving wake is cold and declares them)

if w.cas(c, func(n *claim) bool {

ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probed" && n.Op.Exec == b.ID && n.Holder.Session == h.Session && n.Op.ProbeStop == nil

if ok {

@@ -435,3 +428,26 @@ func (w *world) verifiedCompletionFence(c *claim) int {

w.stats["start: the completion box's termination fence verified"]++

return x.ID

}

+// completedPrior is relocationCompletedHandover.completedPrior: the claim

+// serves on b with a completion recorded on b, and the holder is still the

+// stopped probe session.

+func (w *world) completedPrior(b *box, c *claim) bool {

+ d := c.Op.Completed

+ return c.Op.Kind == "serving" && d != nil && d.Box == b.ID && c.Holder != nil && c.Holder.Session == d.Session && c.Holder.WriterBox == b.ID

+// closeLaunches is StopWriters' first step: the current attempt's and

+// session's launch journal is closed, so the stopped session is never

+// relaunched (an admitted start still in progress is abandoned). It is

+// not root's admission fence, which Collect writes later (relFence).

+func (w *world) closeLaunches(b *box, op string, session int) {

+ if b.launchClosedOp != op || b.launchClosedSession != session {

+ b.launchClosedOp, b.launchClosedSession = op, session

+ w.logf("box %d: relocation %s closed session %d's launch journal", b.ID, op, session)

+ }

+ if b.open != nil && b.open.Session == session {

+ b.open = nil

+ w.stats["release: a start in progress abandoned with its session"]++

+ }

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

index 5e20d9d34..464ff2cc3 100644

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

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

@@ -202,15 +202,133 @@ func wCompletionWithRegionHAOff(t *testing.T, w *world) {

// wServingWakeHandsOver (reloc-completed-handover, N6): after the

// completion the first serving wake on box 3 hands over from the probe's

-// receipt and the host runs. Routed to main's stop, its serving-shaped

-// fence replaces the probe's and the handover refuses for good (INV-3).

+// receipt and is cold, as claimServingOwners.Select makes every serving

+// wake (L18 joint round 2 finding 1): a fresh generation, a new

+// installation stamp, a writes_lost record for the stopped probe session,

+// and P retired by the park-generation that follows. Routed to main's

+// stop, its serving-shaped fence replaces the probe's and the handover

+// refuses for good (INV-3).

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

_, to, ok := w.completedDrain(t, nil)

if !ok {

return

}

- w.reach(t, 200, "the host runs on box 3", func() bool { return hasMain(to) }, w.actAll(), w.recoveryPass, func() { w.wake(to) })

+ d, p, stamp := *w.claim.Op.Completed, w.claim.Holder.Gen, w.claim.Holder.Stamp

+ if !w.reach(t, 200, "the host runs on box 3", func() bool { return hasMain(to) && to.open == nil }, w.actAll(), w.recoveryPass, func() { w.wake(to) }) {

+ return

+ }

+ w.checkFirstWakeCold(t, d, p, stamp)

+ w.reach(t, 600, "P retired by its park-generation", func() bool { return !w.hasFilesAnywhere(p) && len(w.claim.Obl) == 0 }, w.actAll(), w.recoveryPass)

+ w.finish(t)

+// checkFirstWakeCold asserts the first serving wake after completion d of

+// prepared generation p at stamp: cold, into a fresh generation, at a new

+// stamp, declaring the stopped probe session's writes_lost.

+func (w *world) checkFirstWakeCold(t *testing.T, d completedEntry, p string, stamp int) {

+ t.Helper()

+ h := w.claim.Holder

+ l := lastAdmission(h)

+ switch {

+ case h.Gen == p || h.Gen == "":

+ t.Errorf("the first serving wake continued P %q (generation %q)", p, h.Gen)

+ case h.Stamp == stamp:

+ t.Errorf("the first serving wake kept the installation stamp %d", stamp)

+ case l == nil || l.Mode != "cold" || l.Box != d.Box || l.Gen != h.Gen:

+ t.Errorf("the first serving wake was not a cold admission on box %d: %+v", d.Box, l)

+ case l.Lost == nil || l.Lost.Session != d.Session || l.Lost.Box != d.Box || l.Lost.Gen != p:

+ t.Errorf("the first serving wake did not declare the stopped probe session %d's writes_lost: %+v", d.Session, l.Lost)

+ }

+// hasFilesAnywhere: some region's bucket holds an object of generation g

+// of the holder's location.

+func (w *world) hasFilesAnywhere(g string) bool {

+ for _, b := range w.boxes {

+ if w.hasFiles(b, w.claim.Holder.Location, g) {

+ return true

+ }

+ return false

+// TestFirstServingWakeIsCold (L18 joint round 2 finding 1; data safety):

+// the probe session acknowledges a write that its replicator has not yet

+// shipped when the probe passes. The probe stop drains the producers and

+// ends the session without flushing the database, and the first serving

+// wake is cold from what the remote holds: the write is not in the new

+// generation, and it is declared lost (writes_lost, alerted), never lost

+// silently. Every invariant holds; the loss is the built code's (no flush

+// precedes the probe stop, as FlushDB precedes a release's).

+func TestFirstServingWakeIsCold(t *testing.T) {

+ w := newWitness()

+ w.twoBox()

+ from, to := w.boxes[0], w.boxes[3]

+ w.serve(from, 1, app0)

+ w.running(t, from)

+ w.drainTo(t, to)

+ w.reach(t, 1500, "the probe passed", func() bool { c := w.claim; return c.Op.Phase == "probed" && c.Op.ProbeStop == nil && hasMain(to) }, w.act(from, to), w.recoveryPass)

+ wr := w.appWrite(to) // acknowledged by the probe session, not yet replicated

+ w.reach(t, 200, "serving on box 3", func() bool { return w.claim.Op.Kind == "serving" && w.claim.Op.Completed != nil }, w.act(from, to), w.recoveryPass)

+ d, p, stamp := *w.claim.Op.Completed, w.claim.Holder.Gen, w.claim.Holder.Stamp

+ w.reach(t, 200, "the host runs on box 3", func() bool { return hasMain(to) && to.open == nil }, w.actAll(), w.recoveryPass, func() { w.wake(to) })

+ w.mustHold(t)

+ w.checkFirstWakeCold(t, d, p, stamp)

+ declared := false

+ for _, a := range w.acks {

+ if a.W == wr && a.Exempt {

+ declared = true

+ }

+ if !declared || to.DB == nil || contains(to.DB.Log, wr) {

+ t.Fatalf("the probe session's unreplicated write %d is not declared lost by the cold wake (declared %v): %s", wr, declared, w.state())

+ }

+ t.Logf("the probe session's acknowledged write %d is declared lost by the first serving wake (%d writes_lost, %d writes)", wr, w.stats["writes_lost declared"], w.stats["writes declared lost"])

w.finish(t)

+ w.mustHold(t)

+// TestNoAdmissionBetweenStopAndFence (reloc-admits-probe-only, L18 joint

+// round 2 finding 3): the source's release stops its writers and closes

+// the session's launch journal, and its flush is held, so root's

+// admission fence (Collect) has not come. A request reaches the source,

+// then its agent restarts and another request reaches it: no writer is

+// admitted in the interval, because relocatingAdmission admits only the

+// probe. The mutation admits the source's wake, and this test fails.

+func TestNoAdmissionBetweenStopAndFence(t *testing.T) {

+ w := twoBoxWitness()

+ from, to := w.boxes[0], w.boxes[3]

+ w.serve(from, 1, app0)

+ w.running(t, from)

+ w.appWrite(from)

+ loc := w.claim.Holder.Location

+ w.holdKey(loc) // the flush is held: no positions, no Collect

+ w.drainTo(t, to)

+ w.reach(t, 200, "the source stopped, its launch journal closed", func() bool {

+ return w.claim.Op.Phase == "releasing" && from.launchClosedOp == w.claim.Op.ID && !hasMain(from)

+ }, w.act(from, to), w.recoveryPass)

+ session, op := w.claim.Holder.Session, w.claim.Op.ID

+ for _, restart := range []bool{false, true} {

+ if restart {

+ w.crash(from)

+ }

+ w.drive(5, never, func() { w.wake(from) }, w.act(from, to))

+ if from.relFence == op {

+ t.Fatalf("root's admission fence came before the flush")

+ }

+ if hasMain(from) || w.claim.Holder.Session != session || from.open != nil {

+ t.Fatalf("a wake admitted a writer between the stop and the fence (restart %v): %s", restart, w.state())

+ }

+ if w.stats["admission refused: relocating admits only the probe"] == 0 {

+ t.Fatalf("no wake reached the admission: %v", w.stats)

+ }

+ w.mustHold(t)

+ w.hold = nil

+ w.completeHeld(loc)

+ w.servingOn(t, nil)

+ w.finish(t)

+ w.mustHold(t)

}

// wDelayedSourceHoldsItsRow (reloc-completed-catchup-hold, finding 3):

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

index f53016f5a..89f175ae6 100644

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

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

@@ -151,11 +151,14 @@ func relocExcept(op opState, extra ...int) []int {

// reloc-release-needs-receipt, rev 11).

func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

h := c.Holder

- // root's admission fence for this release (ruling 28 puts it at the

- // release's end; the model closes admission at the stop, which is

- // earlier, and the row hold is reconcile's alone: reloc-row-cases while

- // relocating, the catch-up hold after a completion, finding 3)

- b.relFence = c.Op.ID

+ // StopWriters (L18 joint round 2 finding 3): the current attempt's and

+ // session's launch journal closes first, so the stopped session is never

+ // relaunched; root's durable admission fence (relFence) comes only with

+ // Collect, after the flush and the recorded positions (ruling 28). In

+ // between, no wake admits a writer: AdmitWriter's relocatingAdmission

+ // admits nobody in starting or releasing (rule reloc-admits-probe-only).

+ // The row hold is reconcile's alone (reloc-row-cases, the catch-up hold)

+ w.closeLaunches(b, c.Op.ID, h.Session)

if !w.evidence(b, c.Op.ID) {

w.stats["release: a process survives the stop"]++

return nil

@@ -179,10 +182,12 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

case r.Ctl == b.Epoch:

r.Receipt = true // the producers drain; root persists the receipt

w.stats["release: receipt persisted"]++

+ b.relFence = c.Op.ID // Collect: root's durable admission fence, after the flush and the positions

default:

w.stats["release: recorded positions without a receipt, refused"]++

return nil

}

+ b.relFence = c.Op.ID // root's fence stands with the receipt (Collect)

e := r.E

e.Files, e.Timers = r.E.Files.clone(), append([]int(nil), r.E.Timers...)

return &e

@@ -269,6 +274,9 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

return nil

}

+ if b.relFence != c.Op.ID {

+ b.relFence = c.Op.ID // Collect, on the mutations' paths that skip the record or the receipt

+ }

return e

}

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

index d84a6028b..5b089d40d 100644

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

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

@@ -19,7 +19,9 @@ func twoBoxWitness() *world {

// region 0 through every phase of §5.8's table; the host serves on box 3

// with every acknowledged write and timer, box 0's installation is

// retired by its park-local, and the first probe admission's coverage is

-// released (no writes_lost declared, L9).

+// released (L9): no write is declared lost; the first serving wake on box

+// 3 is cold and records a writes_lost for the stopped probe session, which

+// acknowledged nothing here (L18 joint round 2 finding 1).

func TestDrainEndToEnd(t *testing.T) {

w := twoBoxWitness()

from, to := w.boxes[0], w.boxes[3]

@@ -43,8 +45,8 @@ func TestDrainEndToEnd(t *testing.T) {

t.Errorf("phase %s never observed", p)

}

- if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] != 0 {

- t.Errorf("released coverage: %d released, %d writes_lost (want 1 and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"])

+ if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] > 1 || w.stats["writes declared lost"] != 0 {

}

w.finish(t)

if len(w.violations) > 0 {

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

index 01594fe33..6057daa60 100644

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

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

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

"reloc-completed-handover", // finding 2, N6 (wireCompletedHandover, relocationCompletedHandover): the first serving wake after a completion hands over from the probe's receipt and stops nothing; the mutation routes it to main's stop, whose serving-shaped fence replaces the probe's, and the handover refuses for good (INV-3; wServingWakeHandsOver)

"reloc-completed-catchup-hold", // finding 3, ruling 85 (hostbox completedHold, 1b-next a092ddc2): a source whose reconcile runs only after the target completed holds its row for the completed op until its park-local retires it; the mutation leaves the row its release left ready (INV-33; wDelayedSourceHoldsItsRow)

"reloc-completion-fenced-exempt", // ruling 86 (1b-next ca282378: StartGuard's fencedCompletion, ProductionAuthority.completionFence): a delete or purge whose caller verified the completion box's termination fence passes the barrier, as a failover with its fenced source does; the mutation verifies nothing, and a completion box terminated before its discharge while a purge holds admission closed blocks both the purge and the failover for ever (INV-3; wPurgeOverAFencedCompletionBox)

+ "reloc-admits-probe-only", // L18 joint round 2 finding 3 (hostclaim relocatingAdmission): a relocating claim admits only op.exec's cold probe in probing, so between StopWriters' launch-journal closure and Collect's admission fence no wake of the source admits a writer; the mutation admits the source's wake in starting and releasing, as the model did before (TestNoAdmissionBetweenStopAndFence)

"reloc-c1-failed-release-refused", // finding 4, claim ask C1 open (QueueRelocationRelease requires the source in releasing): a live failed target cannot release in probe-failed and reaches stuck at the release deadline, and the operator's resolve stops it; the mutation releases as if C1 had landed (a fidelity guard: TestFailedTargetCannotReleaseWithoutC1)

"reloc-c11-later-attempt-refused", // finding 4, claim ask C11 open (Preflight's ErrLaterAttemptUnlaunchable, ruling 58): after P's opening a later cold probe attempt is refused before it is counted, which is probe-failed; the mutation counts and makes it as if C11 had landed (a fidelity guard: TestLaterAttemptRefusedWithoutC11)

}

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

index bebdd038e..ae4cc16d2 100644

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

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

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

"a failover: the executor is terminated with an acknowledged write whose upload is still in flight; the first admission of P takes released coverage and the write is neither restored nor declared", wRelocReleasedCoverage},

{"reloc-source-loss", "reloc-source-loss", "INV-2",

"a drain whose source is terminated in releasing before its release is journaled, with an unuploaded write; taken as released at what the remote holds, the write goes undeclared", wRelocSourceLoss},

- {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-31",

- "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer; since L18 finding 2 no relocating phase admits a non-probe writer, so the admission lands just after the completion, before the target discharged its participation (INV-31; rev 4 to 11 saw INV-6 at the removed opened phase)", wRelocRowCases},

+ {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-6",

+ "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer, and the stamp its admission issued is activated under the target (INV-6). Since L18 finding 2 no relocating phase admits a non-probe writer, so the admission lands just after the completion, and the target's cold first serving wake activates it (joint round 2 finding 1)", wRelocRowCases},

{"fence-discharge-qualified", "fence-discharge-qualified", "INV-26",

"a terminated box with a volume that was not DeleteOnTermination has its park-local chores discharged automatically", wFenceDischargeQualified},

{"fence-declares-timers", "fence-declares-timers", "acknowledged timer",

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

index a0ac5c504..2e7b6be3a 100644

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

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

@@ -401,21 +401,27 @@ type box struct {

// in the agent's memory, so a restart empties it; probeFence is the

// persisted owner a probe stop installs under (probe-fence.json),

// kept until the completion is marked; relFence is root's admission

- // fence of a release (the op it closed admission for), which ruling

- // 28 puts at the release's end instead of a row hold; owedDischarge

+ // fence of a release (the op it closed admission for), written with

+ // Collect after the flush and the positions (ruling 28), never a row

+ // hold; owedDischarge

// is ground truth, the completed relocation whose participation this

// box has not yet discharged (C10). foreignFence is a witness's

// stand-in for another operation's fence that its owner never lifted

// (INV-32's ground truth). dischargeFails, markFails and crashAfter

// are witness knobs on the completion pass

- actFence string

- probeFence string

- relFence string

- owedDischarge string

- foreignFence string

- dischargeFails bool

- markFails bool

- crashAfter string

+ actFence string

+ probeFence string

+ relFence string

+ // launchClosedOp and launchClosedSession: the session whose launch

+ // journal a release's StopWriters closed (durable; L18 joint round 2

+ // finding 3): it is never relaunched, an admitted start included

+ launchClosedOp string

+ launchClosedSession int

+ owedDischarge string

+ foreignFence string

+ dischargeFails bool

+ markFails bool

+ crashAfter string

Row *row

DB *localDB