carlos / platform Public

hostlife model: rev 7.18, joint round 17 (R17-1)

INV-23's second half checks every reference a scoped park archives or
deletes, in the manifest it builds and in a persisted manifest it
replays, whatever rules are on; an out-of-scope reference is a
violation and is never acted on. The operations' own parks (a landing's
install park, a dirty return's, a push's) run under a scope of
holder.location and are confined to it. TestForeignManifestReplayRefused:
a persisted manifest naming another incarnation's key, replayed under a
valid scope, is refused and the key is not deleted. No rule change.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

claude 2 weeks ago 9c417aaa6e58ac53f08b78d945358922468ba92a parent 39904c8

3 files changed, +105 −18

internal/sim/hostlife/moves_test.go +3 −3
internal/sim/hostlife/protocol_test.go +53 −15
internal/sim/hostlife/witness_test.go +49 −0

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

index ed2a73a8e..e9531b677 100644

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

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

@@ -942,7 +942,7 @@ func (w *world) landTarget(b *box, c *claim) {

w.violate("INV-9: the cut of %s waits on quiet_after[%d] until %d", op.ID, b.Region, c.Quiet[b.Region])

}

// an earlier stay of this incarnation, in its location here

- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], nil) {

+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), confine(loc)) {

w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

}

case "install-copy":

@@ -1418,7 +1418,7 @@ func (w *world) recoverSource(b *box, c *claim) {

if !w.evidence(b, op.RollbackID) {

return

}

- if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, nil) {

+ if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), confine(c.Holder.Location)) {

w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

}

case "install-copy":

@@ -1550,7 +1550,7 @@ func (w *world) pushStep(b *box, c *claim) {

return true

})

case "park":

- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, nil) {

+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), confine(loc)) {

w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) })

}

case "install":

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

index b7986dd7d..e0c6a387f 100644

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

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

@@ -2015,15 +2015,30 @@ func (w *world) probeAccepted(b *box, c *claim) {

// parkStep advances one park of `prefix` in b's own bucket into dest. It

// returns true when the location is verified empty after the quiet time.

// keep, when set, names keys the park must leave alone.

-func (w *world) parkStep(b *box, prefix, dest string, quiet int, keep func(string) bool) bool {

- return w.parkDepth(b, prefix, dest, quiet, keep, 0)

+func (w *world) parkStep(b *box, prefix, dest string, quiet int, scope *parkScope, keep func(string) bool) bool {

+ return w.parkDepth(b, prefix, dest, quiet, keep, scope, 0)

+// member is INV-23's second half (claim rev 6.24 §2; R16-2, R17-1): every

+// reference a scoped park archives or deletes, in a manifest it builds

+// and in a persisted manifest it replays, must be within the scope. It

+// is checked for every reference, whatever rules are on: the listing's

+// confinement (rule scope-membership) is the implementation, this is the

+// oracle. An out-of-scope reference is a violation and is not acted on.

+func (w *world) member(scope *parkScope, id, what string, r ref) bool {

+ if scope == nil || inScope(r.Key, scope.Location) {

+ return true

+ }

+ w.violate("INV-23: chore %s (scope %s, incarnation %d) would %s %s@%d, outside its scope", id, scope.Location, scope.Inc, what, r.Key, r.Ver)

+ return false

}

-func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(string) bool, depth int) bool {

+func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(string) bool, scope *parkScope, depth int) bool {

if depth > 8 {

return false // a park that cannot finish: reported as non-convergence

}

bk := w.buckets[b.Region]

+ id := dest

skip := func(k string) bool {

return (strings.HasSuffix(k, "lock.json") && on("park-skip-lock")) || (keep != nil && keep(k))

}

@@ -2055,9 +2070,13 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(stri

if !on("park-all-versions") && !current {

continue

}

- dels = append(dels, ref{Region: b.Region, Key: k, Ver: v.ID})

+ r := ref{Region: b.Region, Key: k, Ver: v.ID}

+ if !w.member(scope, id, "delete", r) {

+ continue // out of scope: never deleted, never archived

+ }

+ dels = append(dels, r)

if !v.Marker {

- archive = append(archive, ref{Region: b.Region, Key: k, Ver: v.ID})

+ archive = append(archive, r)

}

@@ -2079,10 +2098,16 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(stri

w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manKey, b: &blob{Kind: "manifest", Refs: archive, Dels: dels}})

return false

}

- // replay the manifest's deletion set, by version id, in one batch per visit

+ // replay the manifest's deletion set, by version id, in one batch per

+ // visit; a persisted manifest's references are checked against the

+ // scope as the fresh set was (R17-1: a manifest naming another

+ // incarnation's keys under a valid scope is refused, not replayed)

issued := false

+ for _, r := range man.B.Refs {

+ w.member(scope, id, "archive", r)

+ }

for _, r := range man.B.Dels {

- if bk.byID(r.Key, r.Ver) == nil {

+ if !w.member(scope, id, "delete", r) || bk.byID(r.Key, r.Ver) == nil {

continue

}

if on("park-by-version") {

@@ -2106,7 +2131,7 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(stri

}

for _, v := range bk.objs[k] {

if !v.Marker {

- return w.parkDepth(b, prefix, dest+"s/", quiet, keep, depth+1)

+ return w.parkDepth(b, prefix, dest+"s/", quiet, keep, scope, depth+1)

}

@@ -2202,12 +2227,6 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

if o.Scope != nil && o.Kind != "park-local" {

loc := o.Scope.Location

member = func(k string) bool { return inScope(k, loc) }

- for _, k := range w.buckets[b.Region].keys(o.Prefix) {

- if !member(k) && hasNonMarker(w.buckets[b.Region].objs[k]) && (o.Kind != "park-sweep" || w.sweepable(w.claim, b.Region, k)) && !on("scope-membership") {

- w.violate("INV-23: chore %s (%s, scope %s, incarnation %d) would archive %s, outside its scope", o.ID, o.Kind, loc, o.Scope.Inc, k)

- break

- }

}

if o.Kind == "park-replica" || o.Kind == "park-superseded" || o.Kind == "park-staging" {

// the owner first proves the region's box runs nothing for the

@@ -2308,7 +2327,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

inner := keep

keep = func(k string) bool { return genOf(o.Prefix, k) != retire || inner != nil && inner(k) }

}

- if !w.parkStep(b, o.Prefix, o.Dest(), quiet, keep) {

+ if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.Scope, keep) {

return

}

@@ -2399,6 +2418,25 @@ func (w *world) scoped(o obligation, evidenceAt, inc int) obligation {

// scopeLocation is the scope grammar's form of a park prefix.

func scopeLocation(prefix string) string { return strings.TrimSuffix(prefix, "/") }

+// opScope is the scope an operation's own park runs under (a landing's

+// install park of the target region's earlier stay, a dirty return's and

+// a push's park of what their install supersedes): holder.location, the

+// holder's incarnation, the operation's own evidence time (R16-1, R17-1).

+func (w *world) opScope(c *claim, prefix string) *parkScope {

+ inc := 0

+ if c.Holder != nil {

+ inc = c.Holder.Inc

+ }

+ return &parkScope{Location: scopeLocation(prefix), Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH}

+// confine is the keep function that confines a park's listing to its

+// scope: a legacy instances/<host> scope excludes child incarnations.

+func confine(prefix string) func(string) bool {

+ loc := scopeLocation(prefix)

+ return func(k string) bool { return !inScope(k, loc) }

// scopeOf is the scope location a key belongs to (claim rev 6.24 §2): a

// staging key's is moves/<host> (or its own lane, moves/<host>/<op id>,

// which inScope tests by prefix); an instance key's is its incarnation

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

index 3ff197598..7154794b8 100644

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

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

@@ -2692,6 +2692,55 @@ func TestLegacyLostTargetReturn(t *testing.T) {

}

+// TestForeignManifestReplayRefused (R17-1): a persisted manifest naming

+// another incarnation's keys, replayed under a valid scope, is refused by

+// INV-23 and nothing it names is deleted. The state is constructed: no

+// schedule of the model produces such a manifest.

+func TestForeignManifestReplayRefused(t *testing.T) {

+ w := newWitness()

+ defer func() {

+ if t.Failed() {

+ dump(t, w)

+ }

+ }()

+ b0 := w.boxes[0]

+ w.serve(b0, 1, app0)

+ w.wake(b0)

+ w.appWrite(b0)

+ w.recreated(t, b0.Region)

+ if len(w.violations) > 0 || w.claim.Holder == nil || w.claim.Holder.Inc != 2 {

+ t.Fatalf("incarnation 2 does not serve: %s", w.state())

+ }

+ // a late object of incarnation 1, and a sweep chore of incarnation 2's

+ // own location whose persisted manifest wrongly names it

+ foreign := ltxKey(locationFor(1, false), "old", 0, 3, 3)

+ w.buckets[b0.Region].objs[foreign] = append(w.buckets[b0.Region].objs[foreign], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 3, Max: 3, Inc: 1, Pages: map[string]int{}}})

+ fv := w.buckets[b0.Region].current(foreign).ID

+ o := obligation{ID: "obx", Op: fmt.Sprintf("session:%d", w.claim.Holder.Session), Kind: "park-sweep", Region: b0.Region, Box: -1, Prefix: locationFor(2, false), Ret: "sweep",

+ Scope: &parkScope{Location: scopeLocation(locationFor(2, false)), Inc: 2, EvidenceAt: w.now - horizonH, RequestLimit: requestLimitH}}

+ man := &blob{Kind: "manifest", Refs: []ref{{Region: b0.Region, Key: foreign, Ver: fv}}, Dels: []ref{{Region: b0.Region, Key: foreign, Ver: fv}}}

+ w.buckets[b0.Region].objs[o.Dest()+"manifest"] = []*version{{ID: w.newVer(), B: man}}

+ w.cas(w.claim, func(n *claim) bool { n.Obl = append(n.Obl, o); return true })

+ // one step of the chore: the replay of its persisted manifest (a later

+ // at-rest sweep may park the object legitimately under incarnation 1's

+ // own scope, which is not in question here)

+ w.tick(func() { w.obligationRunner(b0) })

+ found := false

+ for _, v := range w.violations {

+ if strings.Contains(v, "INV-23") && strings.Contains(v, foreign) {

+ found = true

+ }

+ if !found {

+ t.Fatalf("the replayed foreign manifest was not refused by INV-23: %v", w.violations)

+ }

+ w.completeDue(true)

+ if w.buckets[b0.Region].byID(foreign, fv) == nil {

+ t.Fatalf("the foreign object %s@%d was deleted by the replay", foreign, fv)

+ }

+ t.Logf("refused: %s", w.violations[0])

// TestStagingSurvivesLegacyPark (claim rev 6.24 §2, R16-1): a legacy host's

// earlier stay in the target region is parked by the landing's install

// phase while the move's sealed staging sits beside it under moves/; the