carlos / platform Public

hostlife: files-home-move-phases text names the commit boundary and both witnesses (joint round 3 P3)

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

Paul Campbell pushed by claude 2 weeks ago cef63683cb4cecf9376be1a050314ad950acb61b parent 54c0b63

1 file changed, +1 −1

internal/sim/hostlife/rules_test.go +1 −1

CI passed — run details

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

index 439cf4cbc..37de7b4d1 100644

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

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

@@ -208,5 +208,5 @@ var allRules = []string{

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

// Astra's joint round 1 on the two-box model

"files-live-region", // joint round 1 finding 1, claim §6.2a (the live set is {authoritative region, location, generation}; region HA §5.6, L13): the files live set is region-qualified: holder.generation's manifests, the pin's, P's, the chain's newest and the objects they or a box's files directory name are live only in the files home (filesHome: the authoritative region, and while a relocation runs its source region holds the whole files live set), and the newest manifest is read only in the key's own region; the mutation reads every region, so a manifest PUT landing in the former region after a move's cleanup protects itself and the object it names, and the sweep never retires them (INV-10; witness)

- "files-home-move-phases", // joint round 1 review I1, claim §6.2a and moves §5.1's authoritative-region table: the files home also holds the source region while moving (op.exec none from stopped on), while landing until the target's probe is admitted, and while restoring (released included); the mutation keeps op.exec's region and a relocation's source only, so a park-generation queued during the move archives the live manifest in stopped and the converted failover pins no keyed manifest (INV-3; witness)

+ "files-home-move-phases", // joint round 1 review I1, claim §6.2a and moves §5.1's authoritative-region table: the files home also holds the source region while moving (op.exec none from stopped on), while landing until the move commits (op.Committed: admission does not rule out a clean rollback, joint round 2), and while restoring (released included); the mutation keeps op.exec's region and a relocation's source only, so a park-generation queued during the move archives the live manifest in stopped, or after the target's admission before a clean rollback, and the source-region failover pins no keyed manifest (INV-30, INV-3 with INV-30 off; wMoveStoppedKeepsLiveFiles, wRollbackKeepsSourceFiles)

}