carlos / platform Public

sim: a delete or purge over a completion box whose termination fence verifies passes the barrier (ruling 86), and the operator's declare-lost crutch is gone

1b-next ca282378: StartGuard's fencedCompletion. verifiedCompletionFence
is ProductionAuthority.completionFence: the unmarked completion's box is
enrolled, its box-fences record exists and it is terminated; the delete
and purge start CASes pass it to completionBarrier, as a failover passes
its fenced source. Rule reloc-completion-fenced-exempt, witness
wPurgeOverAFencedCompletionBox (seed 2224's schedule; INV-3 under the
mutation). TestTerminatedCompletionBoxBlocksAPurge now shows the purge
refused before the fence record and started after it, with no
declare-lost.

declareDeadCompletionBox is removed: the unmutated 3,000-seed two-box
run converges without it (0 failed; seed 2224 takes the exemption). The
model leaves one case to an operator: with region HA off no worker writes
a fence record, so a completion box terminated before its discharge
blocks a delete or purge until its fence is recorded or it is declared
lost; the sweep never reaches it.

One-box COUNTERS and traces unchanged.

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

Paul Campbell pushed by claude 1 week ago ded69314897a3cfd5e7ec24404097786b9bebbd1 parent d2e97bf

5 files changed, +72 −57

internal/sim/hostlife/console_test.go +4 −7
internal/sim/hostlife/regionha_completion_test.go +18 −28
internal/sim/hostlife/regionha_completion_witness_test.go +47 −22
internal/sim/hostlife/rules_test.go +1 −0
internal/sim/hostlife/witness_test.go +2 −0

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	336.477s
?   	github.com/carlosframework/platform/cmd/changelog	[no test files]
ok  	github.com/carlosframework/platform/cmd/console	3.196s
ok  	github.com/carlosframework/platform/cmd/moveprobe	93.273s
ok  	github.com/carlosframework/platform/internal/activator	210.417s
ok  	github.com/carlosframework/platform/internal/agentsock	0.028s
ok  	github.com/carlosframework/platform/internal/alerting	0.009s
ok  	github.com/carlosframework/platform/internal/analytics	0.034s
ok  	github.com/carlosframework/platform/internal/appconfig	2.327s
ok  	github.com/carlosframework/platform/internal/apperr	0.106s
ok  	github.com/carlosframework/platform/internal/applog	0.160s
ok  	github.com/carlosframework/platform/internal/awsinv	0.010s
ok  	github.com/carlosframework/platform/internal/boxchoice	0.011s
ok  	github.com/carlosframework/platform/internal/boxid	0.470s
?   	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.014s
ok  	github.com/carlosframework/platform/internal/caps	0.018s
ok  	github.com/carlosframework/platform/internal/certwarm	0.008s
ok  	github.com/carlosframework/platform/internal/cgroup	0.199s
ok  	github.com/carlosframework/platform/internal/changelog	0.257s
ok  	github.com/carlosframework/platform/internal/clamd	0.060s
?   	github.com/carlosframework/platform/internal/cliflag	[no test files]
ok  	github.com/carlosframework/platform/internal/console	356.684s
?   	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.047s
ok  	github.com/carlosframework/platform/internal/dbdoor/dbdoortest	0.013s
ok  	github.com/carlosframework/platform/internal/dbverify	0.007s
ok  	github.com/carlosframework/platform/internal/dnsrec	0.007s
ok  	github.com/carlosframework/platform/internal/docsite	0.007s
ok  	github.com/carlosframework/platform/internal/domains	2.022s
ok  	github.com/carlosframework/platform/internal/doorkey	0.007s
ok  	github.com/carlosframework/platform/internal/economics	0.007s
ok  	github.com/carlosframework/platform/internal/edge	25.987s
?   	github.com/carlosframework/platform/internal/edgeproof	[no test files]
ok  	github.com/carlosframework/platform/internal/edgesfile	0.007s
ok  	github.com/carlosframework/platform/internal/fleetapi	0.138s
ok  	github.com/carlosframework/platform/internal/gate	1.655s
ok  	github.com/carlosframework/platform/internal/genselect	0.017s
ok  	github.com/carlosframework/platform/internal/geo	0.012s
ok  	github.com/carlosframework/platform/internal/geoip	0.031s
ok  	github.com/carlosframework/platform/internal/host	56.762s
ok  	github.com/carlosframework/platform/internal/hostactors	0.317s
ok  	github.com/carlosframework/platform/internal/hostbox	1.271s
ok  	github.com/carlosframework/platform/internal/hostclaim	0.257s
ok  	github.com/carlosframework/platform/internal/hostevidence	0.012s
ok  	github.com/carlosframework/platform/internal/hostexec	0.299s
ok  	github.com/carlosframework/platform/internal/hostfence	0.049s
ok  	github.com/carlosframework/platform/internal/hostfiles	4.136s
ok  	github.com/carlosframework/platform/internal/hostfloor	0.016s
ok  	github.com/carlosframework/platform/internal/hostguard	0.140s
ok  	github.com/carlosframework/platform/internal/hostops	1.400s
?   	github.com/carlosframework/platform/internal/hostops/fencerelease	[no test files]
ok  	github.com/carlosframework/platform/internal/hostops/internal/fencerelease	0.002s
ok  	github.com/carlosframework/platform/internal/hostquarantine	0.002s
ok  	github.com/carlosframework/platform/internal/hostresolve	0.145s
ok  	github.com/carlosframework/platform/internal/hostwrite	0.002s
ok  	github.com/carlosframework/platform/internal/infraview	0.002s
ok  	github.com/carlosframework/platform/internal/instancectl	1.708s
ok  	github.com/carlosframework/platform/internal/instanceexec	2.696s
ok  	github.com/carlosframework/platform/internal/instancefs	0.003s
ok  	github.com/carlosframework/platform/internal/instancekey	0.003s
ok  	github.com/carlosframework/platform/internal/instanceupdates	0.009s
ok  	github.com/carlosframework/platform/internal/layout	1.360s
ok  	github.com/carlosframework/platform/internal/lease	9.449s
ok  	github.com/carlosframework/platform/internal/lease/leasetest	0.006s
ok  	github.com/carlosframework/platform/internal/ledger	0.013s
ok  	github.com/carlosframework/platform/internal/mail	0.166s
ok  	github.com/carlosframework/platform/internal/maintenance	0.079s
ok  	github.com/carlosframework/platform/internal/maintenanceexec	5.532s
ok  	github.com/carlosframework/platform/internal/maintenanceguard	0.093s
ok  	github.com/carlosframework/platform/internal/metrics	0.005s
ok  	github.com/carlosframework/platform/internal/moves	21.229s
ok  	github.com/carlosframework/platform/internal/moves/archive	0.766s
ok  	github.com/carlosframework/platform/internal/objstore	0.163s
ok  	github.com/carlosframework/platform/internal/ops	0.156s
ok  	github.com/carlosframework/platform/internal/park	0.196s
ok  	github.com/carlosframework/platform/internal/privatefile	0.004s
ok  	github.com/carlosframework/platform/internal/provision	3.217s
ok  	github.com/carlosframework/platform/internal/publicrelease	0.007s
?   	github.com/carlosframework/platform/internal/regionname	[no test files]
ok  	github.com/carlosframework/platform/internal/registry	3.716s
ok  	github.com/carlosframework/platform/internal/relay	7.226s
ok  	github.com/carlosframework/platform/internal/release	17.979s
ok  	github.com/carlosframework/platform/internal/rollout	3.270s
ok  	github.com/carlosframework/platform/internal/rolloutwords	0.003s
ok  	github.com/carlosframework/platform/internal/rootaws	0.006s
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.239s
ok  	github.com/carlosframework/platform/internal/sim/hostlife	8.506s
ok  	github.com/carlosframework/platform/internal/sim/litestreamfacts	4.560s
ok  	github.com/carlosframework/platform/internal/status	0.038s
ok  	github.com/carlosframework/platform/internal/steering	0.006s
ok  	github.com/carlosframework/platform/internal/stopevidence	0.132s
ok  	github.com/carlosframework/platform/internal/svcrole	0.002s
ok  	github.com/carlosframework/platform/internal/telemetry	0.004s
ok  	github.com/carlosframework/platform/internal/termfence	0.004s
ok  	github.com/carlosframework/platform/internal/tunnelclient	0.004s
ok  	github.com/carlosframework/platform/internal/unixdial	0.003s
ok  	github.com/carlosframework/platform/internal/updatewords	0.002s
ok  	github.com/carlosframework/platform/internal/usage	0.004s
ok  	github.com/carlosframework/platform/internal/version	0.002s
ok  	github.com/carlosframework/platform/internal/vet	1.562s
=== 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: downloading https://github.com/minio/minio/releases/download/RELEASE.2025-09-07T16-13-09Z/minio.linux-arm64.RELEASE.2025-09-07T16-13-09Z
  minio: downloaded, digest verified
  mc: downloading https://github.com/minio/mc/releases/download/RELEASE.2025-08-13T08-35-41Z/mc.linux-arm64.RELEASE.2025-08-13T08-35-41Z
  mc: downloaded, 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:23:18 moves: T4: STORE: list: operation error S3: ListObjectsV2, https response error StatusCode: 403, RequestID: 18DDD8120D3B7E61, 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/console_test.go b/internal/sim/hostlife/console_test.go

index 1e70a7126..a10a3aa8f 100644

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

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

@@ -375,8 +375,8 @@ func (w *world) userDelete() {

recVer = w.rec.Ver

}

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

- if w.completionBarrier(n, -1) {

- return false // StartGuard's completion barrier (ruling 77)

+ if w.completionBarrier(n, w.verifiedCompletionFence(n)) {

+ return false // StartGuard's completion barrier (ruling 77), a verified fence exempt (ruling 86)

}

n.Op = opState{Kind: "deleting", ID: id, Exec: -1, ReqAt: w.now, RecVer: recVer} // intent: the record's ETag (claim §5.2 step 1)

return true

@@ -740,8 +740,8 @@ func (w *world) purgeSteps(p *consolePlan) bool {

}

id := w.newID("pg")

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

- if n.Op.Kind != "serving" || w.completionBarrier(n, -1) {

- return false

+ if n.Op.Kind != "serving" || w.completionBarrier(n, w.verifiedCompletionFence(n)) {

+ return false // ruling 86: a completion box whose termination fence verifies is exempt

}

n.Op = opState{Kind: "purging", ID: id, Exec: -1, ReqAt: w.now}

return true

@@ -1248,9 +1248,6 @@ func (w *world) operator() {

return

}

- if w.declareDeadCompletionBox(c) {

- return

- }

// a stuck relocation (§5.8): carlos ops host resolve (model ruling 13;

// the spec names the command and leaves its effect open). Nothing

// moves away from a live box without its stop evidence:

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

index d8d629ccd..d081e0ec2 100644

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

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

@@ -412,36 +412,26 @@ func (w *world) c1Fallback() bool { return !w.claimC1 && on("reloc-c1-failed-rel

// mutation counts and makes it as if C11 had landed).

func (w *world) c11Fallback() bool { return !w.claimC11 && on("reloc-c11-later-attempt-refused") }

-// declareDeadCompletionBox is the operator's declare-lost (claim D2) of a

-// completion box terminated before its discharge, while a purge holds the

-// app's admission closed: the gap the model found in the built code (seed

-// 2224 / 3,000, two boxes). completionBarrier refuses the purge's

-// StartGuard, because the box is not on lost; the failover that would

-// cite its fence is refused by Admission.Register, because the purge

-// closed admission; so neither starts and nothing finishes the

-// completion. 1b-next has no automatic way out, so the model's operator

-// declares the box lost (the barrier's lost exemption), counted, and the

-// purge proceeds. It acts only in that shape.

-func (w *world) declareDeadCompletionBox(c *claim) bool {

+// verifiedCompletionFence is ProductionAuthority.completionFence (ruling

+// 86, 1b-next ca282378): a delete or a purge passes StartGuard the

+// completion box whose termination fence it verified, as a failover

+// passes its fenced source, or -1. Verified means the box is in the

+// roster (enrolled), its box-fences record exists (a regional worker

+// observed the termination: FenceObservedAt) and the cloud says it is

+// terminated (VerifyFenceForBox); never inferred from a missing fence.

+// The mutation of reloc-completion-fenced-exempt verifies nothing, as

+// before ruling 86: a completion box terminated before its discharge

+// while a purge holds admission closed blocks the purge, and the purge's

+// closed admission blocks the failover (seed 2224 / 3,000, two boxes).

+func (w *world) verifiedCompletionFence(c *claim) int {

d := c.Op.Completed

- if c.Holder == nil || c.Op.Kind != "serving" || d == nil || d.Discharged || contains(c.Lost, d.Box) {

- return false

+ if c.Op.Kind != "serving" || d == nil || d.Discharged || contains(c.Lost, d.Box) || !on("reloc-completion-fenced-exempt") {

+ return -1

}

x := w.boxByID(d.Box)

- ad := w.admit[c.Holder.App]

- if x == nil || !x.Terminated || ad == nil || !ad.Closed {

- return false

+ if x == nil || !x.Enrolled || !x.Terminated || x.FenceObservedAt == 0 {

+ return -1

}

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

- if n.Op.Completed == nil || n.Op.Completed.Op != d.Op || n.Op.Completed.Discharged || contains(n.Lost, d.Box) {

- return false

- }

- n.Lost = addUniq(n.Lost, d.Box)

- return true

- }) {

- w.stats["operator declared a terminated completion box lost (purge and failover both refused)"]++

- w.logf("operator declared box %d lost: its completion of %s blocks the purge, and the purge's closed admission blocks the failover", d.Box, d.Op)

- return true

- }

- return false

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

+ return x.ID

}

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

index 1a5f25f8f..5e20d9d34 100644

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

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

@@ -444,34 +444,59 @@ func TestProbeStopRefusesAnotherFence(t *testing.T) {

}

-// TestTerminatedCompletionBoxBlocksAPurge records a gap in the built code

-// (seed 2224 / 3,000, two boxes): the completion box is terminated

-// before its discharge while a purge has closed the app's admission. The

-// purge's StartGuard is refused by the completion barrier (the box is not

-// on lost), and the failover that would cite the box's fence is refused

-// by the closed admission, so without an operator nothing moves. The

-// operator's declare-lost (declareDeadCompletionBox) puts the box on

-// lost, the barrier's exemption, and the purge proceeds.

-func TestTerminatedCompletionBoxBlocksAPurge(t *testing.T) {

- w := newWitness()

- _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })

+// purgeOverATerminatedCompletionBox is seed 2224's schedule (3,000, two

+// boxes): the completion's discharge fails, a purge closes the app's

+// admission, and the completion box is terminated before its discharge.

+// The failover that would cite its fence is refused by the closed

+// admission (Admission.Register), so only the purge can move.

+func (w *world) purgeOverATerminatedCompletionBox(t *testing.T) (to *box, ok bool) {

+ _, to, ok = w.completedDrain(t, func(to *box) { to.dischargeFails = true })

if !ok {

- w.mustHold(t)

+ return to, false

}

w.userPurge()

- w.reach(t, 100, "the purge closed the app's admission", func() bool { return w.admit[app0].Closed }, w.runConsole)

+ if !w.reach(t, 100, "the purge closed the app's admission", func() bool { return w.admit[app0].Closed }, w.runConsole) {

+ return to, false

+ }

w.terminate(to)

- w.drive(400, never, w.actAll(), w.runConsole, w.recoveryPass)

- w.mustHold(t)

- if c := w.claim; c == nil || c.Op.Kind != "serving" || contains(c.Lost, to.ID) {

- t.Fatalf("something moved without the operator: %s", w.state())

+ return to, true

+// wPurgeOverAFencedCompletionBox (reloc-completion-fenced-exempt, ruling

+// 86): once a worker has written the dead completion box's fence record,

+// the purge verifies it and starts over the unmarked completion, and the

+// host is freed with no operator. Without the exemption the purge is

+// refused by the barrier and the failover by the purge's closed

+// admission, for ever (INV-3).

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

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

+ return

}

- if w.stats["start refused: a completed relocation is not discharged"] == 0 || w.stats["failover start: app admission closed"] == 0 {

- t.Fatalf("not the deadlock: barrier %d, failover %d", w.stats["start refused: a completed relocation is not discharged"], w.stats["failover start: app admission closed"])

+ w.reach(t, 2000, "the purge freed the host", func() bool { c := w.claim; return c == nil || c.Holder == nil }, w.actAll(), w.runConsole, w.recoveryPass)

+ w.finish(t)

+// TestTerminatedCompletionBoxBlocksAPurge was the gap the model found at

+// seed 2224, closed by ruling 86 (1b-next ca282378): the purge refused by

+// the barrier while the completion box's fence is not yet recorded, then

+// started over it once the fence verifies, and the host freed with no

+// operator's declare-lost (the model's operator has none since).

+func TestTerminatedCompletionBoxBlocksAPurge(t *testing.T) {

+ w := newWitness()

+ to, ok := w.purgeOverATerminatedCompletionBox(t)

+ if !ok {

+ w.mustHold(t)

}

- w.reach(t, 2000, "the purge freed the host after the operator's declare-lost", func() bool { c := w.claim; return c == nil || c.Holder == nil }, w.actAll(), w.runConsole, w.recoveryPass, w.operator)

+ w.drive(60, never, w.runConsole) // the purge's start, before any worker observed the termination

+ if c := w.claim; c.Op.Kind != "serving" || to.FenceObservedAt != 0 || w.stats["start refused: a completed relocation is not discharged"] == 0 {

+ t.Fatalf("the purge was not refused before the fence record: fence observed at %d, %s", to.FenceObservedAt, w.state())

+ }

+ w.reach(t, 2000, "the purge freed the host", func() bool { c := w.claim; return c == nil || c.Holder == nil }, w.actAll(), w.runConsole, w.recoveryPass)

w.mustHold(t)

- if w.stats["operator declared a terminated completion box lost (purge and failover both refused)"] != 1 {

- t.Fatalf("the operator's declare-lost did not run once: %v", w.stats)

+ if to.FenceObservedAt == 0 || w.stats["start: the completion box's termination fence verified"] == 0 || w.stats["failover start: app admission closed"] == 0 {

+ t.Fatalf("not ruling 86's path: fence observed at %d, %v", to.FenceObservedAt, w.stats)

+ }

+ if contains(w.claim.Lost, to.ID) && w.claim.Holder != nil {

+ t.Fatalf("the box was declared lost: %s", w.state())

}

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

index d2bd81f6d..01594fe33 100644

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

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

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

"reloc-completion-claim-mode", // finding 2, ruling 82 (newCompletionRuntime): the completion pass runs whenever claim mode is on, region HA on or off; the mutation runs it with region HA on only, and a completion pending when region HA is turned off never finishes (INV-3; wCompletionWithRegionHAOff)

"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-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 303d359ab..bebdd038e 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-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},

}

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