carlos / platform Public

hostlife model: rev 7.16, joint round 15 and claim rev 6.23

Every remote chore carries claim rev 6.23's park scope from its queuing
CAS: location in the grammar's form (instances/<host>,
instances/<host>/<incarnation>, moves/<host>/<op id>, moves/<host>; no
trailing slash; INV-23), the archive incarnation (a free host's sweep
uses the newest retired one), and evidence_at as the ORIGINAL evidence
or fencing bound: the cut's stop for the commit's source park, the
release or the declaration for the target's, the seal bound (seal plus
the staging lease) for a staging lane, the listing for a sweep, the
publication for a generation chore. One deadline for every scope,
staging included: a listing later than evidence_at + H (R15-1; rev 7.15
bound staging at cleanup and kept the seal's quiet time instead).
Witness wStagingScopeDeadline: sealed, deadline seal + lease + H, the
cleanup first runs 40 steps past it under a restarted agent and must
acknowledge at once. wParkScopeSurvivesRestart takes its deadline from
the persisted scope. Witnesses: 72.

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

claude 2 weeks ago 6bfae1530d5d7500e89ada30ead43829da8083c9 parent 63fc6a7

5 files changed, +176 −47

internal/sim/hostlife/console_test.go +6 −3
internal/sim/hostlife/moves_test.go +13 −11
internal/sim/hostlife/protocol_test.go +65 −23
internal/sim/hostlife/witness_test.go +72 −4
internal/sim/hostlife/world_test.go +20 −6

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

index 603e2f145..48aeea4bc 100644

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

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

@@ -1235,12 +1235,15 @@ func (w *world) operator() {

if owesReturn && n.Op.RollbackID != "" && on("lost-return-park") {

// a return the lost target had begun: park its lane in the

// source's region, after the lane's staging horizon (model 27)

- n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", w.now+stagingTTL+horizonH))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", w.now+stagingTTL+horizonH), w.now+stagingTTL, c.Holder.Inc))

}

if owesEvidence { // a box that released already queued these

+ // the lost target's parks cite the declaration's fencing bound

+ // (claim rev 6.23 §2: a lost-box source uses the persisted

+ // fenced_at), the staging lane its seal bound

n.Obl = append(n.Obl,

- w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH),

- w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))

+ w.scoped(w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH), w.now, c.Holder.Inc),

+ w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet), stagingBound(op.SealQuiet), c.Holder.Inc))

// the lost target's region is parked whole: the records whose

// predecessors are there (a restarted probe's, whose dead

// writer never published) are covered in this CAS (claim rev

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

index 754779310..c21e361ba 100644

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

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

@@ -543,7 +543,7 @@ func (w *world) abortMove(c *claim, by *box) {

}

n.Op.Phase = "aborting"

if on("abort-target-owner") {

- n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH), w.now+stagingTTL, c.Holder.Inc))

}

return true

})

@@ -565,7 +565,7 @@ func (w *world) startRevert(c *claim) {

} else {

n.Op.RevPhase = "verify"

}

- n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH), w.now+stagingTTL, c.Holder.Inc))

return true

})

}

@@ -868,9 +868,9 @@ func (w *world) followRecord(c *claim) bool {

q = 0

}

n.Obl = append(n.Obl,

- w.newObl(n, "park-superseded", op.SrcRegion, -1, c.Holder.Location, "", q),

+ w.scoped(w.newObl(n, "park-superseded", op.SrcRegion, -1, c.Holder.Location, "", q), op.StopAt, c.Holder.Inc),

w.newObl(n, "park-local", -1, op.Src, "", "", 0),

- w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))

+ w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet), stagingBound(op.SealQuiet), c.Holder.Inc))

if q > n.Quiet[op.SrcRegion] {

n.Quiet[op.SrcRegion] = q

}

@@ -1275,10 +1275,10 @@ func (w *world) releaseTarget(b *box, c *claim) {

n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.TgtStopAt = -1, true, dirty, "released", w.now

q := w.now + horizonH

if on("target-park") {

- n.Obl = append(n.Obl, w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", q))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", q), w.now, c.Holder.Inc))

w.coverRegionPredecessors(n, op.TgtRegion, "rollback") // the target region's whole location is parked (claim rev 6.14 item 6)

}

- n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet), stagingBound(op.SealQuiet), c.Holder.Inc))

if !dirty {

n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, b.ID, "", "", 0))

}

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

// admission (claim rev 6.9); the return lane's park is owed

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

n.Op.ReturnParked = true

- n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", op.ReturnQuiet))

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", op.ReturnQuiet), stagingBound(op.ReturnQuiet), c.Holder.Inc))

return sameOp(n.Op.ID, op.ID)

})

return

@@ -1707,12 +1707,14 @@ func (w *world) sweep(b *box, c *claim) {

inc := 0

if n.Holder != nil {

inc = n.Holder.Inc

+ } else if len(n.Retired) > 0 {

+ inc = n.Retired[len(n.Retired)-1] // a free host's sweep archives under the newest retired incarnation (claim rev 6.23 §2)

}

for _, p := range prefixes {

- // the scope is persisted at the queuing CAS (claim rev 6.15 §2):

- // the sweeping box's complete listing is the evidence, taken now

- n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: op, Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep",

- Scope: &parkScope{Location: p, Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH}})

+ // the scope is persisted at the queuing CAS (claim rev 6.23 §2):

+ // the sweeping box's complete listing is the evidence, taken now;

+ // the location instances/<host> or moves/<host>

+ n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op, Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}, w.now, inc))

}

// CoverParkedPredecessors at the queuing CAS (claim rev 6.21 item 6):

// the predecessors with a sweepable object, no others

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

index 1d5127371..f811d108b 100644

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

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

@@ -2,6 +2,7 @@ package hostlife

import (

"fmt"

+ "regexp"

"strings"

)

@@ -1054,8 +1055,7 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase

}

// the chore's scope (claim rev 6.15 §2, R14-5): the publication is

// the evidence that the predecessor is dead, taken now

- n.Obl = append(n.Obl, obligation{ID: oid, Op: id, Kind: "park-generation", Region: chore, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH,

- Scope: &parkScope{Location: n.Holder.Location, Inc: n.Holder.Inc, EvidenceAt: w.now, RequestLimit: requestLimitH}})

+ n.Obl = append(n.Obl, w.scoped(obligation{ID: oid, Op: id, Kind: "park-generation", Region: chore, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, n.Holder.Inc))

}

// retention is E's (claim rev 6.14 item 8, R12-6): covered entries

// are dropped from the front only while more than eight entries

@@ -1859,8 +1859,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {

if ret == "" {

ret = "@root"

}

- n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH,

- Scope: &parkScope{Location: n.Holder.Location, Inc: n.Holder.Inc, EvidenceAt: w.now, RequestLimit: requestLimitH}})

+ n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, n.Holder.Inc))

}

n.Holder.Admissions = append(n.Holder.Admissions, e)

@@ -2167,10 +2166,15 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

}

default:

quiet := o.Quiet

+ if o.Scope != nil && !scopeLocationRe.MatchString(o.Scope.Location) {

+ // INV-23 (claim rev 6.23 §2, R15-1): a scope's location is exactly

+ // one of the grammar's four forms

+ w.violate("INV-23: chore %s (%s) carries a scope location %q outside the claim's grammar", o.ID, o.Kind, o.Scope.Location)

+ }

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

// host, when it is not the current executor (a whole-location

- // park; a staging park's quiet time is the seal's own)

+ // park; a staging lane's bound is its seal's, persisted)

if (o.Kind == "park-replica" || o.Kind == "park-superseded") && (c.Op.Exec != b.ID || c.Holder == nil) {

if !w.evidence(b, o.Op) {

return

@@ -2188,7 +2192,10 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

if c.Holder != nil {

inc = c.Holder.Inc

}

- scope := &parkScope{Location: o.Prefix, Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH}

+ // the chore was queued unscoped (a delete's or adoption's

+ // park-replica): the evidence is the stop evidence first in

+ // hand, now; a staging lane never comes here under the rule

+ scope := &parkScope{Location: scopeLocation(o.Prefix), Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH}

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

for i := range n.Obl {

if n.Obl[i].ID == o.ID && n.Obl[i].Scope == nil {

@@ -2209,20 +2216,25 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

}

// the horizon after the evidence is H, the signature-age

// allowance plus the request bound (R14-3): the scope persists the

- // request bound, never the whole horizon

- evidAt, horizon := b.evidAt[o.ID], horizonH

+ // request bound, never the whole horizon. One deadline for every

+ // scope, a staging lane's included (claim rev 6.23 §2, R15-1): a

+ // listing later than evidence_at + H, the evidence being the

+ // persisted original bound, never the cleanup's start; rev 7.15

+ // bound a staging park at cleanup and then ignored the bound for

+ // the seal's quiet time

+ deadline := b.evidAt[o.ID] + horizonH

if o.Scope != nil {

- evidAt, horizon = o.Scope.EvidenceAt, sigAgeH+o.Scope.RequestLimit

+ deadline = o.Scope.deadline()

}

- if on("quiet-before-ack") && o.Kind != "park-staging" && evidAt+horizon > quiet {

- quiet = evidAt + horizon // a staging park keeps the seal's quiet time (SealQuiet), bound by its own lease

+ if (on("quiet-before-ack") || o.Kind == "park-staging") && deadline > quiet {

+ quiet = deadline

}

if o.Kind == "park-generation" && o.Scope != nil && on("quiet-before-ack") {

// a dead generation's chore under its scope (R14-5): the

// publication's evidence time plus H, never less than the

// queued quiet time

- if q := o.Scope.EvidenceAt + sigAgeH + o.Scope.RequestLimit; q > quiet {

+ if q := o.Scope.deadline(); q > quiet {

quiet = q

}

@@ -2236,12 +2248,12 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

keep = func(k string) bool { return !w.sweepable(w.claim, b.Region, k) }

quiet = 0

if o.Scope != nil && on("quiet-before-ack") {

- // the sweep's scope (claim rev 6.15 §6.2a; platform-1e's answer

- // to rev 7.14 note 2): a park-sweep is a retirement event, parked

- // at once and acknowledged only after a verification listing

- // later than evidence_at + H, H the signature-age allowance plus

- // the request bound; the straggler pass is that listing

- quiet = o.Scope.EvidenceAt + sigAgeH + o.Scope.RequestLimit

+ // the sweep's scope (claim rev 6.23 §6.2a): a park-sweep is a

+ // retirement event, parked at once and acknowledged only after a

+ // verification listing later than evidence_at + H, H the

+ // signature-age allowance plus the request bound; the straggler

+ // pass is that listing; every sweep acknowledgement waits it

+ quiet = o.Scope.deadline()

}

if o.Kind == "park-generation" {

@@ -2257,18 +2269,18 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

return

}

- evid, horizon := 0, horizonH

+ deadline := horizonH

if b.evidAt != nil {

- evid = b.evidAt[o.ID]

+ deadline = b.evidAt[o.ID] + horizonH

}

if o.Scope != nil {

- evid, horizon = o.Scope.EvidenceAt, sigAgeH+o.Scope.RequestLimit

+ deadline = o.Scope.deadline()

}

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

for i, x := range n.Obl {

if x.ID == o.ID {

- if (o.Kind == "park-replica" || o.Kind == "park-superseded") && on("quiet-before-ack") && o.Region >= 0 && evid+horizon > n.Quiet[o.Region] {

- n.Quiet[o.Region] = evid + horizon // quiet_after survives free

+ if (o.Kind == "park-replica" || o.Kind == "park-superseded") && on("quiet-before-ack") && o.Region >= 0 && deadline > n.Quiet[o.Region] {

+ n.Quiet[o.Region] = deadline // quiet_after survives free

}

if o.Kind == "park-superseded" && n.Holder != nil && o.Prefix == n.Holder.Location {

// INV-17 (rev 7.13, R12-3): the whole location in this region

@@ -2322,6 +2334,36 @@ func (w *world) newObl(c *claim, kind string, region, boxID int, prefix, ret str

return obligation{ID: w.newID("ob"), Op: c.Op.ID, Kind: kind, Region: region, Box: boxID, Prefix: prefix, Ret: ret, Quiet: quiet}

}

+// scoped attaches a chore's persisted park scope at its queuing CAS (claim

+// rev 6.23 §2): the location is the park prefix without its trailing "/",

+// evidenceAt the original evidence or fencing bound the caller cites, inc

+// the archive incarnation. Under the mutation of persisted-park-scope the

+// chore is queued unscoped and the runner binds the cleanup's own clock,

+// as rev 7.13 did.

+func (w *world) scoped(o obligation, evidenceAt, inc int) obligation {

+ if !on("persisted-park-scope") {

+ return o

+ }

+ o.Scope = &parkScope{Location: scopeLocation(o.Prefix), Inc: inc, EvidenceAt: evidenceAt, RequestLimit: requestLimitH}

+ return o

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

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

+// scopeLocationRe is claim rev 6.23's grammar for a scope's location

+// (the model's incarnation ids are decimal, the claim's 64 hex): exactly

+// instances/<host>, instances/<host>/<incarnation>, moves/<host>/<op id>

+// or moves/<host>, nothing else, no trailing "/".

+var scopeLocationRe = regexp.MustCompile(`^(instances/` + host + `(/[0-9]+)?|moves/` + host + `(/[A-Za-z0-9-]+)?)$`)

+// stagingBound is a staging lane's evidence_at: the seal bound, the time

+// after which no staging writer, its lease holder included, can still

+// write; the lane's quiet time is that bound plus H, so the bound is the

+// quiet time less H (the staging-quiet mutation's quiet time of "now"

+// gives a bound already past).

+func stagingBound(quiet int) int { return quiet - horizonH }

func (c *claim) oblFor(op string) int {

n := 0

for _, o := range c.Obl {

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

index 9bca1789d..b6773cbae 100644

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

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

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

"the commit's CAS is followed again by another reader: the replay is refused, the park is queued once and the coverage stands (R12-3, replay)", wCommitReplayed},

{"persisted-park-scope", "persisted-park-scope", "INV-9",

"a committed move's source-region park binds its scope, the original evidence time, in the claim; the region's agent restarts mid-park; with the box-local evidence map (rev 7.13) the horizon starts again from the restart and the acknowledgement comes late (claim rev 6.15 §2, R13-4)", wParkScopeSurvivesRestart},

+ {"persisted-park-scope", "persisted-park-scope", "INV-9",

+ "a committed move's staging lane sealed at the cut: its persisted bound is the seal's, deadline seal + lease + H; the target region's cleanup first runs 40 steps after that deadline and its agent restarts as it begins; the acknowledgement must follow at once, since the persisted deadline has passed; bound at cleanup's own clock (rev 7.15) the chore waits a fresh horizon (claim rev 6.23 §2, R15-1)", wStagingScopeDeadline},

{"holderless-park", "holderless-park", "INV-20",

"a deleted host's region keeps late residue; the free host's sweep runs as a holderless parking op and a create requested meanwhile waits for FreeAfterPark; with bare chores on the free claim (rev 7.13) the create claims the host over the outstanding park (claim rev 6.15 §6.2a, R13-4)", wFreeSweepVsCreate},

{"covered-baseline-refused", "covered-baseline-refused", "INV-2",

@@ -2454,31 +2456,97 @@ func wParkScopeSurvivesRestart(t *testing.T, w *world) {

}

t0 := w.now

var id string

+ deadline := w.claim.Op.StopAt + horizonH // the cut's stop evidence plus H (claim rev 6.23: the persisted original bound)

for _, o := range w.claim.Obl {

if o.Kind == "park-superseded" && o.Region == src.Region {

id = o.ID

+ if o.Scope != nil {

+ deadline = o.Scope.deadline()

+ }

}

if id == "" {

t.Fatalf("witness: no park-superseded for the source region after the commit: %s", w.state())

}

// the park runs for a while, then the source region's agent restarts

- for i := 0; i < 45; i++ {

+ // before the deadline

+ restart := deadline - 20

+ if restart < t0+5 {

+ restart = t0 + 5

+ }

+ for w.now < restart {

w.tick(w.act(src, tgt), w.runConsole, w.recoveryPass)

if len(w.violations) > 0 {

return

}

if !hasObl(w.claim.Obl, id) {

- t.Fatalf("witness: the park %s acknowledged before the restart, at %d (commit at %d): the horizon did not hold", id, w.now, t0)

+ t.Fatalf("witness: the park %s acknowledged before the restart, at %d (commit at %d, deadline %d): the horizon did not hold", id, w.now, t0, deadline)

}

w.crash(src) // a new agent process: the box-local evidence map is gone

w.reach(t, 400, "the source region's park acknowledged", func() bool { return !hasObl(w.claim.Obl, id) }, w.act(src, tgt), w.runConsole, w.recoveryPass)

if len(w.violations) > 0 {

return

}

- if deadline := t0 + horizonH + 40; w.now > deadline {

- w.violate("INV-9 (witness): the park %s was acknowledged at %d, after %d, the commit's evidence plus the horizon and slack: the restart at %d started the horizon again", id, w.now, deadline, t0+45)

+ if w.now > deadline+30 {

+ w.violate("INV-9 (witness): the park %s was acknowledged at %d, after its persisted deadline %d and slack: the restart at %d started the horizon again from the restart's clock", id, w.now, deadline, restart)

+ return

+ }

+ w.finish(t)

+// wStagingScopeDeadline (claim rev 6.23 §2, R15-1): a staging lane's scope

+// persists the seal bound, and its deadline is that bound plus H; a

+// cleanup that first runs after the deadline, through an agent restart,

+// acknowledges at once rather than waiting a fresh horizon from its own

+// clock (the round's example: sealed at 100, deadline 560, cleanup at 600

+// must not wait until 660).

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

+ src, tgt := w.boxes[0], w.boxes[1]

+ w.serve(src, 1, app0)

+ w.wake(src)

+ w.appWrite(src)

+ w.commitLanding(t, src, tgt)

+ if len(w.violations) > 0 {

+ return

+ }

+ var id string

+ deadline := w.claim.Op.SealQuiet

+ for _, o := range w.claim.Obl {

+ if o.Kind == "park-staging" && o.Region == tgt.Region {

+ id = o.ID

+ if o.Scope != nil {

+ deadline = o.Scope.deadline()

+ }

+ if id == "" {

+ t.Fatalf("witness: no staging park for the target region after the commit: %s", w.state())

+ }

+ // the target region's cleanup is delayed: its obligation runner does

+ // not run until 40 steps past the deadline (the target's worker and

+ // the source run as usual)

+ for w.now < deadline+40 {

+ w.tick(func() { w.worker(src); w.obligationRunner(src); w.worker(tgt) }, w.runConsole, w.recoveryPass)

+ if len(w.violations) > 0 {

+ return

+ }

+ if !hasObl(w.claim.Obl, id) {

+ t.Fatalf("witness: the staging park %s was acknowledged before its cleanup ran: %s", id, w.state())

+ }

+ w.crash(tgt) // the cleanup begins under a new agent process

+ start := w.now

+ w.reach(t, 200, "the staging lane parked", func() bool { return !hasObl(w.claim.Obl, id) }, w.act(src, tgt), w.runConsole, w.recoveryPass)

+ if len(w.violations) > 0 {

+ return

+ }

+ if w.now < deadline {

+ w.violate("INV-9 (witness): the staging park %s was acknowledged at %d, before its persisted deadline %d", id, w.now, deadline)

+ return

+ }

+ if w.now > start+20 {

+ w.violate("INV-9 (witness): the staging park %s was acknowledged at %d; its persisted deadline %d had passed when the cleanup began at %d, yet it waited a fresh horizon (bound at the cleanup's clock, until %d)", id, w.now, deadline, start, start+horizonH)

return

}

w.finish(t)

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

index 2f762fe31..574134d38 100644

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

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

@@ -649,18 +649,32 @@ type obligation struct {

Scope *parkScope // the persisted park scope of a remote chore (claim rev 6.15 §2), bound before its first step runs

}

-// parkScope is claim rev 6.15's park scope {location, incarnation,

-// evidence_at, request_limit_ns}, persisted in the chore when it is queued

-// or bound before its first step, so every retry, an agent restart's

-// included, uses the same location, archive incarnation and original

-// evidence time: a retry's own clock is never evidence (R13-4).

+// parkScope is claim rev 6.23's park scope {location, incarnation,

+// evidence_at, request_limit_ns} (§2), persisted in the chore when it is

+// queued or bound before its first step, so every retry, an agent

+// restart's included, uses the same location, archive incarnation and

+// original evidence time: a retry's own clock is never evidence (R13-4,

+// R15-1). Location is exactly one of instances/<host>,

+// instances/<host>/<incarnation>, moves/<host>/<op id> (a move's staging

+// or a rollback's return lane) or moves/<host> (the staging sweep), with

+// no trailing "/". EvidenceAt is always the original evidence or fencing

+// bound: the stop evidence a whole-location park cites, the seal bound of

+// a staging lane (the time after which no staging writer, its lease

+// holder included, can still write), the sweeping box's listing, the

+// publication that supersedes a generation; never cleanup's start time.

+// Every scope has the one deadline: acknowledge only after a listing

+// later than EvidenceAt + H, H = sigAgeH + RequestLimit.

type parkScope struct {

Location string

Inc int

EvidenceAt int

- RequestLimit int // request_limit_ns: the longest request, which H adds to the signature age; the acknowledgement waits EvidenceAt + sigAgeH + RequestLimit

+ RequestLimit int // request_limit_ns: the longest request, which H adds to the signature age

}

+// deadline is the scope's acknowledgement bound: a listing later than

+// evidence_at + H (claim rev 6.23 §2, §6.2a).

+func (s *parkScope) deadline() int { return s.EvidenceAt + sigAgeH + s.RequestLimit }

// admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it

// produced, the box and generation it admitted, the stamp, the mode (warm

// or cold), whether the writer has opened, and the predecessor it observed.