amadan

carlos / platform Public

moves: the recovery's generation lineage rests on the claim's admission invariant (Task 3 fix 4)

Checked against the claim code: during a restoring or reverting op no
writer is admitted except through the recovery owners, and never a warm
one. The holder's session changes only in AdmitWriter's CAS, whose only
production callers are hostbox.Writer's paths; Writer.Admit refuses every
warm or certified admission; only the executor admits; and every cold
admission's evidence is ClaimOwnerDispatch's, which hands the op's kinds
to the recovery owners, whose evidence journals the link. So a chain of
generations is a chain of the recovery's sessions, and no session binding
is added. The invariant is written at lineage() with citations;
TestRecoveryOpAdmitsNoOutsideWriter pins the refusals (a warm admission,
an outside owner's shapes, another box) and that any cold admission the
op takes is in the lineage.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude c51bdc7467bc41c66ca7b647ba71858755f78102 parent e0f4d1f
2 files changed, +120 −0
  • internal/host/movesrecoveryowners.go +33 −0
  • internal/host/movesrecoveryowners_test.go +87 −0
diff --git a/internal/host/movesrecoveryowners.go b/internal/host/movesrecoveryowners.go
index d16ce6cd2..2c80f6c7b 100644
--- a/internal/host/movesrecoveryowners.go
+++ b/internal/host/movesrecoveryowners.go
@@ -899,6 +899,39 @@ func (r movesRecoveryOwners) recordLineage(host string, v recoveryProbe, g strin
// admitted by this recovery over the one before. Any other writer admitted
// in between breaks the chain (its generation was never journalled here):
// the ownership interval is unproven and refused.
+//
+// The links bind generations, not sessions, and that is complete because
+// the claim admits no writer during a restoring or reverting op except
+// through these owners, and never a warm one (fix round 4; checked against
+// the claim code at e0f4d1f7):
+//
+// - the holder's session, generation and writer box change only in
+// AdmitWriter's CAS (hostclaim/generation.go:166-170); ReturnToSource
+// sets the generation and stamp only from released to claimed, before
+// any recovery admission (hostclaim/move.go:1025-1046);
+// - AdmitWriter's only production callers are hostbox.Writer's three
+// paths (hostbox/writer.go:63; writer_loss.go:58 through
+// hostclaim/lost.go:218; writer_loss.go:79 through
+// hostclaim/move_fence_admission.go:44);
+// - Writer.Admit refuses every warm or certified admission before any
+// path (hostbox/writer.go:34-36), so no admission keeps a generation
+// while advancing the session: the counterexample's intervening warm
+// admission cannot be written;
+// - only the op's executor admits (hostbox/writer.go:37,
+// hostclaim/generation.go:40-42), under the observed op and phase
+// (hostclaim/generation.go:43-45);
+// - every cold admission's evidence, on every path, is
+// ClaimOwnerDispatch.AdmissionEvidence (host/claimassembly.go:181,
+// host/claimconstruction.go:267), which hands restoring and reverting
+// only to the moves owners (host/claimowners.go:220-224), which hand them
+// to these recovery owners (movesprobeowners.go, recoveryKind); their
+// AdmissionEvidence journals the link before it returns nil. Without
+// the moves owners bound, the serving owners' evidence refuses any move
+// kind (host/claimowners.go:328).
+//
+// So every session after the root is a cold admission evidenced here, and
+// a chain of generations is a chain of this recovery's sessions.
+// TestRecoveryOpAdmitsNoOutsideWriter pins the refusals.
func (r movesRecoveryOwners) lineage(host string, v recoveryProbe) error {
m := r.m
h := v.holder
diff --git a/internal/host/movesrecoveryowners_test.go b/internal/host/movesrecoveryowners_test.go
index 18f78573a..0226f3e8c 100644
--- a/internal/host/movesrecoveryowners_test.go
+++ b/internal/host/movesrecoveryowners_test.go
@@ -960,3 +960,90 @@ func (f *rcFixture) admitThroughWriter(o hostclaim.Observed, in ClaimLaunchInput
}
return admitted
}
+
+// Fix round 4: the invariant lineage relies on (see its comment). While the
+// op is restoring or reverting, the claim admits no writer outside the
+// recovery owners: the writer refuses any warm admission (the reviewer's
+// counterexample keeps G under an outside session); only the executor may
+// admit; and the dispatch hands every cold admission of the op to the
+// recovery owners' evidence, which refuses one they would not select (an
+// outside owner's shape) and journals the link of any it accepts, so even a
+// hand-built admission that passes is in the recovery's lineage.
+func TestRecoveryOpAdmitsNoOutsideWriter(t *testing.T) {
+ for _, kind := range []string{rcClean, rcRevert} {
+ t.Run(kind, func(t *testing.T) {
+ f := newRCFixture(t, kind)
+ ctx := t.Context()
+ o := f.read()
+ in := f.selectAdmission(o)
+ admitted := f.admitThroughWriter(o, in)
+ outside := 0
+ serving := ClaimKindOwners{Inputs: f.owners, PublicationEvidence: func(context.Context, hostclaim.Observed) error { return nil },
+ AdmissionEvidence: func(context.Context, hostclaim.Observed, hostclaim.Admission, *genselect.Plan) error {
+ outside++
+ return nil
+ }}
+ moves := f.owners.MovesOwners(&movesProbeAttempts{}).ClaimKindOwners
+ dispatch := ClaimOwnerDispatch{Serving: serving, Moves: &moves}
+ w := hostbox.Writer{Claims: f.claims, Data: f.bucket, Bucket: "data", Region: "ie", Box: "ie-box", AdmissionEvidence: dispatch.AdmissionEvidence}
+ h := admitted.Claim.Holder
+ plan, err := genselect.Select(ctx, f.bucket, f.owners.request(poHost, h))
+ if err != nil {
+ t.Fatal(err)
+ }
+ restart := hostclaim.Admission{ObservedOpID: poOp, ObservedPhase: hostclaim.PhaseProbing, ObservedSession: h.Session, ObservedGeneration: h.Generation,
+ Box: "ie-box", Region: "ie", PredecessorRegion: "ie", Mode: "cold", NewGeneration: "outside1", RemoteMaxTXID: plan.MaxTXID}
+ unmoved := func() {
+ t.Helper()
+ now := f.read().Claim.Holder
+ if now.Session != h.Session || now.Generation != h.Generation || now.WriterBox != h.WriterBox || len(now.Admissions) != len(h.Admissions) {
+ t.Fatalf("the holder moved: %+v", now)
+ }
+ }
+
+ // The counterexample's outside warm admission keeping G.
+ warm := restart
+ warm.Mode, warm.NewGeneration, warm.PredecessorCertified = "warm", "", true
+ if _, err := w.Admit(ctx, admitted, warm, nil); !errors.Is(err, hostbox.ErrUnsupported) {
+ t.Fatalf("a warm admission: %v", err)
+ }
+ // An outside owner's shape (serving's: no op, no phase), and one
+ // claiming coverage the recovery's restart never claims.
+ for name, mutate := range map[string]func(*hostclaim.Admission){
+ "serving's shape": func(a *hostclaim.Admission) { a.ObservedOpID, a.ObservedPhase = "", "" },
+ "claimed coverage": func(a *hostclaim.Admission) { a.Coverage = "clean-return" },
+ "a kept stamp": func(a *hostclaim.Admission) { a.KeepStamp = true },
+ } {
+ a := restart
+ mutate(&a)
+ if _, err := w.Admit(ctx, admitted, a, plan); err == nil {
+ t.Fatalf("%s was admitted", name)
+ }
+ }
+ if outside != 0 {
+ t.Fatalf("the dispatch reached another owner's evidence %d times", outside)
+ }
+ // Another box is never the executor.
+ other := restart
+ other.Box = "uk-box"
+ if _, err := hostclaim.Update(ctx, f.claims, admitted, hostclaim.AdmitWriter(other)); !errors.Is(err, hostclaim.ErrWrongState) {
+ t.Fatalf("another box: %v", err)
+ }
+ unmoved()
+
+ // Any cold admission the op does take passed the recovery's
+ // evidence, which journalled its link: it is in the lineage.
+ taken, err := w.Admit(ctx, admitted, restart, plan)
+ if err != nil {
+ t.Fatal(err)
+ }
+ v, err := f.owners.recovery().recovery(ctx, taken)
+ if err != nil {
+ t.Fatal(err)
+ }
+ if err := f.owners.recovery().lineage(poHost, v); err != nil {
+ t.Fatalf("an admission the evidence passed: %v", err)
+ }
+ })
+ }
+}