carlos / platform Public

sim: the probe stop stops the writers, flushes and records the positions before root's stop (ruling 87), so the cold first serving wake loses nothing the probe session acknowledged

1b-next 6a4eadde. relocStopProbe now runs flushStopped's steps first:
the writers stopped, the database flushed (the session's own replicator)
and the files published as one manifest, the positions recorded
(probeRecord, durable); only then the owned activator fence and root's
receipt. With another owner's fence it refuses after the flush, root not
asked and the fence untouched (ruling 75 as ruling 87 amends it). A
restart before the record has no replicator, so the stop refuses until
ruling 67's deadline makes the op stuck, as a release does.

Rule reloc-probe-stop-flush, oracle INV-34 (the first serving wake's
writes_lost names no write the stopped probe session acknowledged),
witness wProbeStopFlushes. TestFirstServingWakeIsCold now shows the
probe session's write in the new generation and nothing declared lost;
TestProbeStopRefusedAfterARestartBeforeTheRecord and the amended
TestProbeStopRefusesAnotherFence are new or updated.
TestL18CrashDuringInstallation's probing case may now crash after the
probe passed and before the record: it serves wherever the operator's
resolve puts it.

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 372f7a4b43912e407b02732a0cf08a4e93cc3d6c parent 86294cb

7 files changed, +196 −40

internal/sim/hostlife/protocol_test.go +6 −0
internal/sim/hostlife/regionha_cases_test.go +9 −1
internal/sim/hostlife/regionha_completion_test.go +84 −9
internal/sim/hostlife/regionha_completion_witness_test.go +86 −25
internal/sim/hostlife/rules_test.go +1 −0
internal/sim/hostlife/witness_test.go +2 −0
internal/sim/hostlife/world_test.go +8 −5

CI passed — run details

CI log

=== gate ===
cd launchctx && go vet ./... && go test ./... -count=1
ok  	amadan.net/carlos/platform.git/launchctx	0.012s
?   	amadan.net/carlos/platform.git/launchctx/controlname	[no test files]
?   	amadan.net/carlos/platform.git/launchctx/wireid	[no test files]
go vet ./...
gofmt -l .: clean
go test ./... -count=1 -timeout 30m
ok  	github.com/carlosframework/platform	337.104s
?   	github.com/carlosframework/platform/cmd/changelog	[no test files]
ok  	github.com/carlosframework/platform/cmd/console	3.243s
ok  	github.com/carlosframework/platform/cmd/moveprobe	93.273s
ok  	github.com/carlosframework/platform/internal/activator	209.942s
ok  	github.com/carlosframework/platform/internal/agentsock	0.018s
ok  	github.com/carlosframework/platform/internal/alerting	0.003s
ok  	github.com/carlosframework/platform/internal/analytics	0.018s
ok  	github.com/carlosframework/platform/internal/appconfig	2.312s
ok  	github.com/carlosframework/platform/internal/apperr	0.077s
ok  	github.com/carlosframework/platform/internal/applog	0.132s
ok  	github.com/carlosframework/platform/internal/awsinv	0.003s
ok  	github.com/carlosframework/platform/internal/boxchoice	0.004s
ok  	github.com/carlosframework/platform/internal/boxid	0.892s
?   	github.com/carlosframework/platform/internal/boxid/boxidtest	[no test files]
?   	github.com/carlosframework/platform/internal/boxid/internal/signtest	[no test files]
ok  	github.com/carlosframework/platform/internal/boxvolumes	0.008s
ok  	github.com/carlosframework/platform/internal/caps	0.012s
ok  	github.com/carlosframework/platform/internal/certwarm	0.002s
ok  	github.com/carlosframework/platform/internal/cgroup	0.192s
ok  	github.com/carlosframework/platform/internal/changelog	0.250s
ok  	github.com/carlosframework/platform/internal/clamd	0.054s
?   	github.com/carlosframework/platform/internal/cliflag	[no test files]
ok  	github.com/carlosframework/platform/internal/console	356.515s
?   	github.com/carlosframework/platform/internal/controlname	[no test files]
?   	github.com/carlosframework/platform/internal/controlsock	[no test files]
ok  	github.com/carlosframework/platform/internal/dbdoor	6.195s
ok  	github.com/carlosframework/platform/internal/dbdoor/dbdoortest	0.011s
ok  	github.com/carlosframework/platform/internal/dbverify	0.005s
ok  	github.com/carlosframework/platform/internal/dnsrec	0.005s
ok  	github.com/carlosframework/platform/internal/docsite	0.005s
ok  	github.com/carlosframework/platform/internal/domains	2.027s
ok  	github.com/carlosframework/platform/internal/doorkey	0.006s
ok  	github.com/carlosframework/platform/internal/economics	0.004s
ok  	github.com/carlosframework/platform/internal/edge	26.012s
?   	github.com/carlosframework/platform/internal/edgeproof	[no test files]
ok  	github.com/carlosframework/platform/internal/edgesfile	0.010s
ok  	github.com/carlosframework/platform/internal/fleetapi	0.137s
ok  	github.com/carlosframework/platform/internal/gate	1.654s
ok  	github.com/carlosframework/platform/internal/genselect	0.015s
ok  	github.com/carlosframework/platform/internal/geo	0.023s
ok  	github.com/carlosframework/platform/internal/geoip	0.034s
ok  	github.com/carlosframework/platform/internal/host	56.514s
ok  	github.com/carlosframework/platform/internal/hostactors	0.636s
ok  	github.com/carlosframework/platform/internal/hostbox	1.292s
ok  	github.com/carlosframework/platform/internal/hostclaim	0.272s
ok  	github.com/carlosframework/platform/internal/hostevidence	0.013s
ok  	github.com/carlosframework/platform/internal/hostexec	0.312s
ok  	github.com/carlosframework/platform/internal/hostfence	0.039s
ok  	github.com/carlosframework/platform/internal/hostfiles	4.123s
ok  	github.com/carlosframework/platform/internal/hostfloor	0.013s
ok  	github.com/carlosframework/platform/internal/hostguard	0.134s
ok  	github.com/carlosframework/platform/internal/hostops	1.434s
?   	github.com/carlosframework/platform/internal/hostops/fencerelease	[no test files]
ok  	github.com/carlosframework/platform/internal/hostops/internal/fencerelease	0.013s
ok  	github.com/carlosframework/platform/internal/hostquarantine	0.013s
ok  	github.com/carlosframework/platform/internal/hostresolve	0.132s
ok  	github.com/carlosframework/platform/internal/hostwrite	0.013s
ok  	github.com/carlosframework/platform/internal/infraview	0.014s
ok  	github.com/carlosframework/platform/internal/instancectl	1.713s
ok  	github.com/carlosframework/platform/internal/instanceexec	2.727s
ok  	github.com/carlosframework/platform/internal/instancefs	0.018s
ok  	github.com/carlosframework/platform/internal/instancekey	0.017s
ok  	github.com/carlosframework/platform/internal/instanceupdates	0.009s
ok  	github.com/carlosframework/platform/internal/layout	1.400s
ok  	github.com/carlosframework/platform/internal/lease	9.442s
ok  	github.com/carlosframework/platform/internal/lease/leasetest	0.005s
ok  	github.com/carlosframework/platform/internal/ledger	0.011s
ok  	github.com/carlosframework/platform/internal/mail	0.161s
ok  	github.com/carlosframework/platform/internal/maintenance	0.077s
ok  	github.com/carlosframework/platform/internal/maintenanceexec	5.509s
ok  	github.com/carlosframework/platform/internal/maintenanceguard	0.076s
ok  	github.com/carlosframework/platform/internal/metrics	0.005s
ok  	github.com/carlosframework/platform/internal/moves	21.216s
ok  	github.com/carlosframework/platform/internal/moves/archive	0.772s
ok  	github.com/carlosframework/platform/internal/objstore	0.179s
ok  	github.com/carlosframework/platform/internal/ops	0.159s
ok  	github.com/carlosframework/platform/internal/park	0.196s
ok  	github.com/carlosframework/platform/internal/privatefile	0.003s
ok  	github.com/carlosframework/platform/internal/provision	3.256s
ok  	github.com/carlosframework/platform/internal/publicrelease	0.006s
?   	github.com/carlosframework/platform/internal/regionname	[no test files]
ok  	github.com/carlosframework/platform/internal/registry	3.766s
ok  	github.com/carlosframework/platform/internal/relay	7.222s
ok  	github.com/carlosframework/platform/internal/release	17.869s
ok  	github.com/carlosframework/platform/internal/rollout	3.288s
ok  	github.com/carlosframework/platform/internal/rolloutwords	0.005s
ok  	github.com/carlosframework/platform/internal/rootaws	0.007s
ok  	github.com/carlosframework/platform/internal/s3compat	0.005s
ok  	github.com/carlosframework/platform/internal/safefile	0.004s
ok  	github.com/carlosframework/platform/internal/schedule	2.251s
ok  	github.com/carlosframework/platform/internal/sim/hostlife	8.778s
ok  	github.com/carlosframework/platform/internal/sim/litestreamfacts	3.895s
ok  	github.com/carlosframework/platform/internal/status	0.037s
ok  	github.com/carlosframework/platform/internal/steering	0.006s
ok  	github.com/carlosframework/platform/internal/stopevidence	0.116s
ok  	github.com/carlosframework/platform/internal/svcrole	0.002s
ok  	github.com/carlosframework/platform/internal/telemetry	0.006s
ok  	github.com/carlosframework/platform/internal/termfence	0.007s
ok  	github.com/carlosframework/platform/internal/tunnelclient	0.005s
ok  	github.com/carlosframework/platform/internal/unixdial	0.003s
ok  	github.com/carlosframework/platform/internal/updatewords	0.003s
ok  	github.com/carlosframework/platform/internal/usage	0.008s
ok  	github.com/carlosframework/platform/internal/version	0.002s
ok  	github.com/carlosframework/platform/internal/vet	1.556s
=== cross ===
--- shard 0 of 5 ---
cross-compiling darwin/arm64
--- shard 1 of 5 ---
cross-compiling darwin/amd64
--- shard 2 of 5 ---
cross-compiling linux/arm64
--- shard 3 of 5 ---
cross-compiling windows/amd64
--- shard 4 of 5 ---
cross-compiling windows/arm64
=== minio-contract ===
minio contract: arm64, minio RELEASE.2025-09-07T16-13-09Z, mc RELEASE.2025-08-13T08-35-41Z
  minio: cached, digest verified
  mc: cached, digest verified
  minio healthy on 127.0.0.1:20999
Added `local` successfully.
Bucket created successfully `local/contract-bucket`.
Bucket created successfully `local/denied-bucket`.
Created policy `contract-only` successfully.
Added user `scopeduser` successfully.
Attached Policies: [contract-only]
To User: scopeduser
  buckets and scoped user ready
=== RUN   TestDeliveredContractMinio
=== RUN   TestDeliveredContractMinio/put
=== RUN   TestDeliveredContractMinio/get_round-trips_the_body
=== RUN   TestDeliveredContractMinio/list_shows_the_key
=== RUN   TestDeliveredContractMinio/head_and_list_agree_on_the_version
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_its_own_object
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_its_own_object/not_by_PutObjectTagging
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_its_own_object/and_not_by_x-amz-tagging_on_upload
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/not_by_CreateMultipartUpload
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/not_by_CopyObject_with_a_REPLACE_tagging_directive
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/but_multipart_itself_is_allowed
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/and_copy_itself_is_allowed
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/a_POST-policy_forged_tag_with_a_matching_version_is_still_not_a_verdict
=== RUN   TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/and_an_ordinary_tagged-with-something-else_upload_is_allowed
=== RUN   TestDeliveredContractMinio/delete_removes_it
=== RUN   TestDeliveredContractMinio/cross-bucket_denial
--- PASS: TestDeliveredContractMinio (0.02s)
    --- PASS: TestDeliveredContractMinio/put (0.00s)
    --- PASS: TestDeliveredContractMinio/get_round-trips_the_body (0.00s)
    --- PASS: TestDeliveredContractMinio/list_shows_the_key (0.00s)
    --- PASS: TestDeliveredContractMinio/head_and_list_agree_on_the_version (0.00s)
    --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_its_own_object (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_its_own_object/not_by_PutObjectTagging (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_its_own_object/and_not_by_x-amz-tagging_on_upload (0.00s)
    --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route (0.01s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/not_by_CreateMultipartUpload (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/not_by_CopyObject_with_a_REPLACE_tagging_directive (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/but_multipart_itself_is_allowed (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/and_copy_itself_is_allowed (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/a_POST-policy_forged_tag_with_a_matching_version_is_still_not_a_verdict (0.00s)
        --- PASS: TestDeliveredContractMinio/the_app_cannot_tag_by_any_other_route/and_an_ordinary_tagged-with-something-else_upload_is_allowed (0.00s)
    --- PASS: TestDeliveredContractMinio/delete_removes_it (0.00s)
    --- PASS: TestDeliveredContractMinio/cross-bucket_denial (0.00s)
PASS
ok  	github.com/carlosframework/platform/internal/objstore	0.025s
=== RUN   TestT4StorageProbeMinio
2026/10/12 17:47:55 moves: T4: STORE: list: operation error S3: ListObjectsV2, https response error StatusCode: 403, RequestID: 18DDD969C570AC1F, HostID: 7c420053e0fbcd7f41653fdd92ffa2802c903d05303b1aa15adc2e8bb65d183f, api error SignatureDoesNotMatch: The request signature we calculated does not match the signature you provided. Check your key and signing method.
--- PASS: TestT4StorageProbeMinio (0.01s)
PASS
ok  	github.com/carlosframework/platform/internal/host	0.022s
minio contract: PASS

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

index 750baf8fd..f5d15a2dd 100644

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

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

@@ -1980,6 +1980,12 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {

n := w.exemptDeclared(b, lost, h, a.NewGeneration, true)

w.stats["writes_lost declared"]++

w.stats["writes declared lost"] += n

+ if d := c.Op.Completed; n > 0 && c.Op.Kind == "serving" && d != nil && d.Box == b.ID && lost.Session == d.Session && lost.Box == d.Box {

+ // INV-34 (ruling 87): the probe stop flushed every write its

+ // session acknowledged, so the first serving wake's writes_lost,

+ // bounded by the remote's last shipped transaction, names none

+ w.violate("INV-34: box %d's first serving wake after relocation %s declared %d writes the stopped probe session %d acknowledged lost (ruling 87: the probe stop flushes first)", b.ID, d.Op, n, d.Session)

+ }

w.lostAlert++

w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes", b.ID, lost.Box, lost.Gen, lost.Session, lost.RemoteMaxTXID, n)

}

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

index b1e297d2b..639406bcd 100644

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

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

@@ -280,7 +280,15 @@ func TestL18CrashDuringInstallation(t *testing.T) {

to := w.boxByID(w.claim.Op.Tgt)

w.drive(2, never, w.act(to)) // a step into the phase: a PUT issued, a files directory extracted

w.crash(to)

- w.servingOn(t, to)

+ if c := w.claim; c.Op.Kind == "relocating" && c.Op.Phase == "probed" && c.Op.ProbeStop == nil && to.probeRecord == nil {

+ // the probe passed and the crash came before the probe

+ // stop recorded its flush (ruling 87): no replicator, so

+ // the stop refuses until the deadline, and the operator's

+ // resolve serves the host elsewhere

+ w.servingOn(t, nil)

+ } else {

+ w.servingOn(t, to)

+ }

w.finish(t)

w.mustHold(t)

})

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

index 1dc6d77bd..98603dce7 100644

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

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

@@ -68,6 +68,27 @@ func (w *world) relocStopProbe(b *box, c *claim) {

if h == nil || h.WriterBox != b.ID || op.Exec != b.ID {

return

}

+ // ruling 87 (1b-next 6a4eadde, EndProbe): the release's own steps first

+ // (flushStopped): the writers stopped, the database and the files

+ // flushed, the positions recorded; only then the activator's fence

+ // and root's stop. A restart before the record leaves no replicator,

+ // so the flush refuses until ruling 67's deadline makes the op stuck,

+ // as a release does. The mutation of reloc-probe-stop-flush stops at

+ // once with nothing flushed (joint round 2's model)

+ if !w.evidence(b, "probe-writers:"+op.ID) {

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

+ return

+ }

+ if on("reloc-probe-stop-flush") {

+ if r := b.probeRecord; r == nil || r.Op != op.ID || r.Session != h.Session {

+ tx, seq, ok := w.flushProbe(b, c)

+ if !ok {

+ return

+ }

+ b.probeRecord = &probeRecordEntry{Op: op.ID, Session: h.Session, TX: tx, Seq: seq}

+ w.stats["probe stop: flushed and recorded"]++

+ }

owner := probeOwner(op.ID, h.Session)

if strings.HasPrefix(b.probeFence, probeKey(op.ID)+"/") && b.probeFence != owner {

w.stats["probe stop: the persisted fence owner names another session"]++

@@ -76,24 +97,21 @@ func (w *world) relocStopProbe(b *box, c *claim) {

b.probeFence = owner // probe-fence.json, persisted before anything is asked of the activator

if b.actFence != "" && b.actFence != owner {

if on("reloc-probe-fence-owner") {

- // ErrFenceHeld: nothing stopped, nothing asked of root

- w.stats["probe stop: another owner's fence, nothing stopped"]++

- w.logf("relocation %s: box %d's probe stop meets %s's fence; nothing is stopped", op.ID, b.ID, b.actFence)

+ // ErrFenceHeld (ruling 75 as ruling 87 amends it): the writers

+ // are stopped and flushed, root is not asked, and the other

+ // owner's fence is left as it is

+ w.stats["probe stop: another owner's fence, root not asked"]++

+ w.logf("relocation %s: box %d's probe stop meets %s's fence; flushed, root not asked", op.ID, b.ID, b.actFence)

return

}

w.stats["probe stop: another owner's fence replaced (mutation)"]++

}

b.actFence = owner

+ // root's writer-session stop and its receipt

if !w.evidence(b, probeKey(op.ID)) {

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

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 {

@@ -451,3 +469,60 @@ func (w *world) closeLaunches(b *box, op string, session int) {

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

}

+// probeRecordEntry is the probe stop's recorded positions (ruling 87,

+// ReleasePositions under the probe's own stop request): durable, so a

+// restart after the record stops without flushing again.

+type probeRecordEntry struct {

+ Op string

+ Session, TX int

+ Seq int

+// flushProbe is flushStopped's database and files steps for the probe

+// session (ruling 87, the release's FlushDB and FlushFiles): they need

+// the session's own replicator and the box's own files directory; with

+// either gone (a restart before the record) the flush refuses. The

+// pending writes ship and the listing must reach the stopped database's

+// position; the files and wake state are published as one manifest of the

+// generation, acknowledged. It reports the positions once both landed.

+func (w *world) flushProbe(b *box, c *claim) (tx, seq int, ok bool) {

+ h := c.Holder

+ db := b.DB

+ if db == nil || db.Inc != h.Inc || db.Gen != h.Gen || db.Epoch != b.Epoch || db.Session != h.Session || b.Files == nil || b.Files.Inc != h.Inc {

+ w.stats["probe stop: no replicator or files directory and no record, refused"]++

+ return 0, 0, false

+ }

+ if len(db.Pending) > 0 {

+ bl := w.deltaOf(db, db.Inc)

+ db.FirstFull = false

+ db.Queue = append(db.Queue, bl)

+ db.Pos, db.Pending = bl.Max, nil

+ }

+ w.ship(b)

+ if len(db.Queue) > 0 || db.InFlight != nil || w.remoteMax(w.buckets[b.Region], dataKey(h.Location, h.Gen, "")) < db.Pos {

+ w.stats["probe stop: waits for the flush"]++

+ return 0, 0, false

+ }

+ files := b.Files.clone()

+ if b.pubGen != h.Gen {

+ b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0

+ }

+ if !w.ensureObject(b, h, files) {

+ w.stats["probe stop: waits for its files object"]++

+ return 0, 0, false

+ }

+ if b.releaseSeq == 0 {

+ b.pubSeq++

+ b.releaseSeq = b.pubSeq

+ }

+ w.issued++

+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.releaseSeq, Files: files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}

+ if !w.ackedPut(b, manifestKey(h.Location, h.Gen, b.releaseSeq), bl, true) {

+ w.stats["probe stop: waits for its manifest"]++

+ return 0, 0, false

+ }

+ seq, b.releaseSeq = b.releaseSeq, 0

+ b.published = filesState(b.Timers, files)

+ return db.Pos, seq, true

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

index 464ff2cc3..0d2b2d8d6 100644

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

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

@@ -252,42 +252,97 @@ func (w *world) hasFilesAnywhere(g string) bool {

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()

+// probeWriteThenServe drains box 0 to box 3; once the probe passed, the

+// probe session acknowledges a write its replicator has not shipped; then

+// the relocation completes and the first serving wake on box 3 runs. It

+// returns the write, the completion and the P and stamp it completed with.

+func (w *world) probeWriteThenServe(t *testing.T) (wr int, d completedEntry, p string, stamp int, ok bool) {

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) })

+ if !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) {

+ return 0, d, "", 0, false

+ }

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

+ if !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) {

+ return 0, d, "", 0, false

+ }

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

+ ok = 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 wr, d, p, stamp, ok

+// wProbeStopFlushes (reloc-probe-stop-flush, ruling 87): the probe

+// session acknowledges a write the replicator has not shipped; the probe

+// stop flushes it before root's stop, so the first serving wake, cold,

+// declares a writes_lost that names none of the probe session's writes.

+// Stopped with nothing flushed, that wake declares the write lost

+// (INV-34).

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

+ if _, _, _, _, ok := w.probeWriteThenServe(t); !ok {

+ return

+ }

+ w.finish(t)

+// TestFirstServingWakeIsCold (L18 joint round 2 finding 1, ruling 87):

+// the first serving wake after the completion is cold (a fresh

+// generation, a new stamp, a writes_lost for the stopped probe session),

+// and since the probe stop flushed, the write the probe session

+// acknowledged is in the new generation and no write is declared lost.

+func TestFirstServingWakeIsCold(t *testing.T) {

+ w := newWitness()

+ wr, d, p, stamp, ok := w.probeWriteThenServe(t)

+ if !ok {

+ w.mustHold(t)

+ }

w.mustHold(t)

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

- declared := false

+ to := w.boxByID(d.Box)

for _, a := range w.acks {

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

- declared = true

+ t.Fatalf("the probe session's write %d was declared lost: %s", wr, w.state())

}

- 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())

+ if to.DB == nil || !contains(to.DB.Log, wr) || w.stats["writes declared lost"] != 0 {

+ t.Fatalf("the probe session's write %d is not in the first serving wake's database (%d writes declared lost): %s", wr, w.stats["writes declared lost"], 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)

}

+// TestProbeStopRefusedAfterARestartBeforeTheRecord (reloc-probe-stop-flush,

+// ruling 87): the probe passed, its flush is held, and the target's agent

+// restarts before the positions are recorded. The new agent has no

+// replicator for the probe session, so the probe stop refuses; nothing is

+// journaled, and ruling 67's deadline makes the relocation stuck, as a

+// release would be. The mutation stops at once, and this test fails.

+func TestProbeStopRefusedAfterARestartBeforeTheRecord(t *testing.T) {

+ w := twoBoxWitness()

+ 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)

+ w.appWrite(to)

+ loc := w.claim.Holder.Location

+ w.holdKey(loc)

+ w.drive(3, never, w.act(from, to))

+ if to.probeRecord != nil || w.claim.Op.ProbeStop != nil {

+ t.Fatalf("the probe stop recorded or journaled with its flush held: %s", w.state())

+ }

+ w.crash(to)

+ w.hold = nil

+ w.completeHeld(loc)

+ w.reach(t, 3*releaseDeadline, "stuck at the probe stop's deadline", func() bool { return w.claim.Op.Stuck != "" }, w.act(from, to), w.recoveryPass)

+ w.mustHold(t)

+ if c := w.claim; c.Op.Phase != "probed" || c.Op.ProbeStop != nil || to.probeRecord != nil || w.stats["probe stop: no replicator or files directory and no record, refused"] == 0 {

+ t.Fatalf("the probe stop did not refuse until the deadline: %s", w.state())

+ }

// 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

@@ -544,9 +599,11 @@ func TestCompletionBarrierExemptions(t *testing.T) {

w.mustHold(t)

}

-// TestProbeStopRefusesAnotherFence (reloc-probe-fence-owner, the

-// refusal's detail): the refused probe stop stops nothing, journals no

-// stop and leaves the other owner's fence in place.

+// TestProbeStopRefusesAnotherFence (reloc-probe-fence-owner as ruling 87

+// amends ruling 75): with another owner's fence on the host, the probe

+// stop stops the writers and flushes and records the positions, then

+// refuses: root is not asked (no receipt), no stop is journaled, and the

+// other owner's fence is left as it is.

func TestProbeStopRefusesAnotherFence(t *testing.T) {

w := twoBoxWitness()

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

@@ -557,8 +614,12 @@ func TestProbeStopRefusesAnotherFence(t *testing.T) {

to.actFence = "op-elsewhere"

w.drive(20, never, w.act(from, to))

w.mustHold(t)

- if c := w.claim; c.Op.ProbeStop != nil || !hasMain(to) || to.actFence != "op-elsewhere" || to.StopEvidence[probeKey(c.Op.ID)] {

- t.Fatalf("the refused probe stop changed something (stop %+v, running %v, fence %q): %s", c.Op.ProbeStop, hasMain(to), to.actFence, w.state())

+ c := w.claim

+ if c.Op.ProbeStop != nil || to.actFence != "op-elsewhere" || to.StopEvidence[probeKey(c.Op.ID)] {

+ t.Fatalf("the refused probe stop asked root or touched the fence (stop %+v, fence %q): %s", c.Op.ProbeStop, to.actFence, w.state())

+ }

+ if hasMain(to) || to.probeRecord == nil || to.probeRecord.Op != c.Op.ID {

+ t.Fatalf("the probe's writers were not stopped and flushed before the refusal (running %v, record %+v)", hasMain(to), to.probeRecord)

}

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

index 6057daa60..134ffae25 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-probe-stop-flush", // ruling 87 (1b-next 6a4eadde, EndProbe through flushStopped): the probe stop stops the writers, flushes the database and files and records the positions before the activator's fence and root's stop, and with another owner's fence it refuses after the flush; a restart before the record has no replicator, so it refuses until ruling 67's deadline; the mutation stops with nothing flushed, and the first serving wake declares writes the probe session acknowledged (INV-34; wProbeStopFlushes)

"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 ae4cc16d2..33c36dc7f 100644

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

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

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

"N6: the first serving wake after the completion 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", wServingWakeHandsOver},

{"reloc-completed-catchup-hold", "reloc-completed-catchup-hold", "INV-33",

"finding 3, ruling 85: the source releases, its reconcile is delayed until the target completed, and its next reconcile holds its row for the completed op until its park-local retires it; without the catch-up hold the row its release left ready stays ready", wDelayedSourceHoldsItsRow},

+ {"reloc-probe-stop-flush", "reloc-probe-stop-flush", "INV-34",

+ "ruling 87: the probe session acknowledges a write its replicator has not shipped; the probe stop flushes it before root's stop, so the first serving wake, cold, declares nothing the probe session acknowledged; stopped with nothing flushed, that wake declares the write lost", wProbeStopFlushes},

{"reloc-completion-fenced-exempt", "reloc-completion-fenced-exempt", "INV-3",

"ruling 86, seed 2224: a purge closes the app's admission and the completion box is terminated before its discharge; once its fence record exists the purge verifies it, starts over the unmarked completion and frees the host; without the exemption the barrier refuses the purge and the closed admission the failover, for ever", wPurgeOverAFencedCompletionBox},

}

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

index 2e7b6be3a..aeaecd178 100644

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

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

@@ -417,11 +417,14 @@ type box struct {

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

launchClosedOp string

launchClosedSession int

- owedDischarge string

- foreignFence string

- dischargeFails bool

- markFails bool

- crashAfter string

+ // probeRecord is the probe stop's recorded positions (ruling 87),

+ // durable: a restart after it stops the session without a new flush

+ probeRecord *probeRecordEntry

+ owedDischarge string

+ foreignFence string

+ dischargeFails bool

+ markFails bool

+ crashAfter string

Row *row

DB *localDB