amadan

carlos / platform Public

sim: plan 1b-next rev 19's fixes for the model's findings: a nonempty database pins only files that carry instance.key (the L21 window fails safe), probe-failed and a dead target with no spare go stuck after the deadline with the fence consumed, and every unopened P is recorded on every path and parked at completion

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude b652b8ff0863eb45ecfe4f923a9aa53a650f186b parent 3cb7f53
7 files changed, +247 −64
  • internal/sim/hostlife/console_test.go +1 −0
  • internal/sim/hostlife/regionha_cases_test.go +76 −43
  • internal/sim/hostlife/regionha_test.go +83 −17
  • internal/sim/hostlife/regionha_witness_test.go +71 −0
  • internal/sim/hostlife/rules_test.go +5 −0
  • internal/sim/hostlife/witness_test.go +9 −2
  • internal/sim/hostlife/world_test.go +2 −2
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index cf98bfc3a..88980b190 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1272,6 +1272,7 @@ func (w *world) operator() {
n.Op.Stuck, n.Op.Phase, n.Op.FailedAt, n.Op.Release = "", "probe-failed", w.now, nil
what = "sent its live target to probe-failed"
default:
+ w.abandonPrepared(n)
n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true
n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1
n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go
index 9a52eea4b..6086dcba6 100644
--- a/internal/sim/hostlife/regionha_cases_test.go
+++ b/internal/sim/hostlife/regionha_cases_test.go
@@ -620,14 +620,16 @@ func TestOnlyTheExecutorInstalls(t *testing.T) {
}
}
-// ---------- findings: hazards the model shows in 1b-next rev 16 ----------
-
-// TestFailoverBeforeTheFirstManifest (finding F2): a host none of whose
-// files manifests has landed is terminated; 1b-next pins its files as
-// empty (StorePinner: "Empty for a host that never published files"), so
-// the install mints a fresh instance.key over data sealed with the old
-// one. The model reproduces it (INV-4); the sweep never terminates such
-// an executor (model ruling 17).
+// ---------- findings F1 to F3, closed by 1b-next rev 17 to 19 ----------
+
+// TestFailoverBeforeTheFirstManifest (finding F2, closed by 1b-next
+// ruling 25 as rev 18 amended it): a host none of whose files manifests
+// has landed is terminated. The pin refuses files that carry no
+// instance.key for a nonempty database, the operation is stuck, and
+// nothing is installed: no fresh key over sealed data. The database is
+// unrecoverable by relocation (L21); the operator's replay never accepts
+// the keyless pin. Under the mutation of files-pin-needs-key the install
+// mints a fresh key (INV-4) and this test fails.
func TestFailoverBeforeTheFirstManifest(t *testing.T) {
w := twoBoxWitness()
from := w.boxes[0]
@@ -637,21 +639,24 @@ func TestFailoverBeforeTheFirstManifest(t *testing.T) {
w.running(t, from)
w.hold = nil
w.terminate(from)
- w.drive(400, func() bool {
- return len(w.violations) > 0 || w.claim.Op.Kind == "serving" && w.claim.Op.Exec != from.ID
- }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec)
- if len(w.violations) == 0 || !contains([]int{4}, invNumber(w.violations[0])) {
- t.Fatalf("finding F2 no longer reproduces (want INV-4): %v", w.violations)
+ w.drive(400, func() bool { return len(w.violations) > 0 }, w.actAll(), w.recoveryPass, w.wakeExec)
+ w.mustHold(t)
+ c := w.claim
+ if c.Op.Kind != "relocating" || c.Op.Stuck == "" || c.Op.Pin != nil || c.Op.Prepared != "" {
+ t.Fatalf("the failover did not stop at an unevidenced files pin: %s", w.state())
+ }
+ if w.stats["pin: files unevidenced, no instance.key"] == 0 {
+ t.Fatalf("the pin never refused: %v", w.stats)
}
}
-// TestProbeFailedInATwoBoxRegion (finding F1): a drain's target cannot
-// run the app; its probe fails and it releases. 1b-next's worker looks
-// for a spare with no bound (Worker.Step: "no eligible box yet: a later
-// pass may find one"), and replaceTargetSlot refuses the source, so in a
-// two-box region the host serves nowhere until an operator acts. The
-// model marks it stuck after the release deadline (model ruling 14) and
-// the operator's resolve returns it to the source (model ruling 13).
+// TestProbeFailedInATwoBoxRegion (finding F1, closed by 1b-next ruling
+// 26): a drain's target cannot run the app; its probe fails and it
+// releases. With no spare the worker waits, and ReleaseDeadline after
+// probe_failed_since the operation is stuck; nothing names the source
+// automatically. The operator's resolve returns the host to the source
+// (plan ruling 13). Under the mutation of reloc-no-spare-bound the
+// operation waits for ever (INV-3) and this test fails.
func TestProbeFailedInATwoBoxRegion(t *testing.T) {
w := twoBoxWitness()
from, to := w.boxes[0], w.boxes[3]
@@ -659,38 +664,66 @@ func TestProbeFailedInATwoBoxRegion(t *testing.T) {
w.serve(from, 1, app0)
w.running(t, from)
w.drainTo(t, to)
+ w.reach(t, 1500, "probe-failed with the target released", func() bool {
+ c := w.claim
+ return c.Op.Phase == "probe-failed" && c.Op.Release != nil && c.Op.Release.Box == to.ID
+ }, w.actAll(), w.recoveryPass)
+ w.drive(releaseDeadline/2, never, w.actAll(), w.recoveryPass)
+ if c := w.claim; c.Op.Stuck != "" || c.Op.Tgt == from.ID {
+ t.Fatalf("before the deadline the operation is stuck or names the source: %s", w.state())
+ }
w.reach(t, 1500, "stuck with no spare", func() bool { return w.claim.Op.Stuck == "no eligible box for the nested relocation" }, w.actAll(), w.recoveryPass)
w.servingOn(t, from)
w.finish(t)
w.mustHold(t)
}
-// TestAbandonedPreparedGenerationParked (finding F3): a target replaced
-// at installing leaves its partial build of P behind (the replacement
-// builds a fresh P'); 1b-next's CompleteRelocation queues park-local
-// chores only. The model parks every unopened P in the serving CAS
-// (model ruling 16); without it INV-10 finds P's objects at the release.
+// TestAbandonedPreparedGenerationParked (finding F3, closed by 1b-next
+// ruling 27 and rev 18 finding 3): an unopened P is recorded on every
+// path that drops it and parked at completion. installing: the target
+// is replaced at installing and the replacement builds P'. probe-failed:
+// the probe deadline passes before any admission, the target is then
+// terminated, and the replacement table's nested branch drops P. Under
+// the mutation of reloc-abandoned-prepared INV-10 finds P's objects.
func TestAbandonedPreparedGenerationParked(t *testing.T) {
- w := twoBoxWitness()
- from, to := w.boxes[0], w.boxes[3]
- w.serve(from, 1, app0)
- w.running(t, from)
- w.published(t, from)
- w.drainTo(t, to)
- third := w.extraBox(0, 30)
- w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass)
- p := w.claim.Op.Prepared
- w.terminate(to)
- w.reach(t, 100, "replaced", func() bool { return w.claim.Op.Exec == third.ID }, w.act(third))
- if w.claim.Op.Prepared == p {
- t.Fatalf("the replacement at installing kept P")
+ for _, path := range []string{"installing", "probe-failed"} {
+ t.Run(path, func(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.drainTo(t, to)
+ third := w.extraBox(0, 30)
+ w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass)
+ p := w.claim.Op.Prepared
+ if path == "probe-failed" {
+ w.dropPBeforeAdmission(t, from, to)
+ } else {
+ w.terminate(to)
+ }
+ w.reach(t, 300, "P dropped", func() bool { return w.claim.Op.Prepared != p }, w.actAll(), w.recoveryPass)
+ w.servingOn(t, third)
+ if w.stats["relocation: abandoned prepared generation parked"] == 0 {
+ t.Fatalf("the abandoned P %q was not parked at serving", p)
+ }
+ w.finish(t)
+ w.mustHold(t)
+ })
}
- w.servingOn(t, third)
- if w.stats["relocation: abandoned prepared generation parked"] == 0 {
- t.Fatalf("the abandoned P %q was not parked at serving", p)
+}
+
+// dropPBeforeAdmission is rev 18 finding 3's trace: the target freezes
+// in probing until the probe deadline passes with P unopened, the worker
+// moves it to probe-failed, and it is terminated there.
+func (w *world) dropPBeforeAdmission(t *testing.T, from, to *box) {
+ w.reach(t, 1500, "probing", func() bool { return w.claim.Op.Phase == "probing" }, w.act(from, to), w.recoveryPass)
+ to.Frozen = true
+ w.reach(t, 3*probeDeadline, "probe-failed before any admission", func() bool { return w.claim.Op.Phase == "probe-failed" }, w.act(from), w.recoveryPass)
+ if preparedOpened(w.claim) {
+ t.Fatalf("P was opened")
}
- w.finish(t)
- w.mustHold(t)
+ w.terminate(to)
}
// invNumber is the n of the first "INV-n" in a violation, 0 if none.
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 47effbedf..9d8e987af 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -243,9 +243,38 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry {
}
pin.ManKey, pin.ManVer, pin.ManSeq, pin.ManGen = mk, mv, ms, mg
}
+ // 1b-next ruling 25 as rev 18 amended it (finding F2; rule
+ // files-pin-needs-key): when a writer was admitted and the pinned
+ // database is nonempty, the pinned manifest must carry a live
+ // instance.key, or the operation is stuck; no operator replay accepts
+ // it, since a database is never installed without its key. The L21
+ // window (the app mints the key after it starts, and its first
+ // manifest with the key has not landed) ends here. The mutation pins
+ // what it found, rev 16's behaviour. Only the two-box shape has a
+ // files publisher (ruling 11)
+ if w.perRegion > 1 && on("files-pin-needs-key") && h.Session != 0 && n > 0 && !manifestHasKey(w.pinnedManifestOf(b.Region, pin)) {
+ w.stats["pin: files unevidenced, no instance.key"]++
+ w.markStuck(c, fmt.Sprintf("the pinned files carry no instance.key for a nonempty database (TXID %d)", n))
+ return nil
+ }
return pin
}
+// pinnedManifestOf is the manifest pin names, read by version.
+func (w *world) pinnedManifestOf(r int, pin *pinEntry) *blob {
+ if pin.ManKey == "" {
+ return nil
+ }
+ if v := w.buckets[r].byID(pin.ManKey, pin.ManVer); v != nil && !v.Marker {
+ return v.B
+ }
+ return nil
+}
+
+// manifestHasKey: the manifest carries a live instance.key (InstanceKeyPath,
+// liveEntry): its files directory names one.
+func manifestHasKey(m *blob) bool { return m != nil && m.Files != nil && m.Files.Key != 0 }
+
// restoreUpTo restores generation gen of region r from its current
// listing, capped at TXID upto: the newest current snapshot at or below
// upto as the root, then the planner's rule (ltx.IsContiguous, highest
@@ -406,13 +435,13 @@ func (w *world) markStuck(c *claim, why string) {
// source, when it is alive and its fence did not discharge it, and every
// other box this operation handed op.exec to.
func (w *world) relocationLeftovers(n *claim, op opState) {
- // every prepared generation this operation built and no writer ever
- // opened is a dead generation of holder.location: its remote build is
- // retired by a park-generation queued here (model ruling 16; 1b-next's
- // CompleteRelocation queues park-local chores only, and nothing else
- // retires an abandoned P's objects before the at-rest sweep)
+ // every prepared generation the operation abandoned unopened
+ // (abandoned_prepared) is a dead generation of holder.location: its
+ // remote build is retired by a park-generation queued here, beside the
+ // park-local chores (1b-next ruling 27, CompleteRelocation; plan ruling
+ // 16). An opened P is part of the writer lineage and never listed
if h := n.Holder; h != nil {
- for _, g := range op.Built {
+ for _, g := range op.Abandoned {
if g == h.Gen || w.ancestorGen(h.Location, h.Gen, g) {
continue
}
@@ -581,12 +610,30 @@ func (w *world) relocPinning(b *box, c *claim) {
}
}
+// abandonPrepared is abandonPrepared(c) in hostclaim (1b-next ruling
+// 27, rev 18 finding 3): before an unopened P is replaced or dropped, it
+// is journaled in abandoned_prepared, so the serving CAS parks it. Every
+// path that replaces or drops P calls it: install, the replacement
+// table's nested branch, the nested relocation after probe-failed and the
+// operator's replay. The mutation of reloc-abandoned-prepared records
+// nothing, which reopens finding F3.
+func (w *world) abandonPrepared(n *claim) {
+ p := n.Op.Prepared
+ if p == "" || preparedOpened(n) || hasStr(n.Op.Abandoned, p) || !on("reloc-abandoned-prepared") {
+ return
+ }
+ n.Op.Abandoned = append(n.Op.Abandoned, p)
+}
+
// handExec is install() in hostclaim: op.exec to box at phase with
// prepared generation P, a new stamp (this CAS's), journaled as
// install_stamp, no receipt, the probe attempts reset for the new
// executor (BeginProbeAttempt counts per box), and the box noted as owing
// a park-local should it be abandoned.
func (w *world) handExec(n *claim, box int, phase, prepared string) {
+ if prepared != n.Op.Prepared {
+ w.abandonPrepared(n) // install replaces an unopened P (1b-next ruling 27)
+ }
n.Op.Exec, n.Op.Phase, n.Op.Prepared = box, phase, prepared
n.Holder.Stamp = w.issueStamp(n, box)
n.Op.InstallStamp = n.Holder.Stamp
@@ -594,9 +641,6 @@ func (w *world) handExec(n *claim, box int, phase, prepared string) {
n.Op.Receipt = nil
}
n.Op.Attempts = 0
- if prepared != "" && !hasStr(n.Op.Built, prepared) {
- n.Op.Built = append(n.Op.Built, prepared)
- }
n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box)
n.Boxes = addUniq(n.Boxes, box)
}
@@ -989,7 +1033,11 @@ func (w *world) relocProbeFailed(b *box, c *claim) {
}
next := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op, op.Exec)...)
if next == nil {
- if w.now > op.FailedAt+releaseDeadline {
+ // 1b-next ruling 26 (rev 17, finding F1; rule reloc-no-spare-bound):
+ // with no spare ReleaseDeadline after probe_failed_since, stuck;
+ // never the source, which the operator's resolve alone may name.
+ // The mutation waits for a spare for ever, rev 16's behaviour
+ if on("reloc-no-spare-bound") && w.now > op.FailedAt+releaseDeadline {
w.markStuck(c, "no eligible box for the nested relocation")
}
return
@@ -1001,6 +1049,7 @@ func (w *world) relocProbeFailed(b *box, c *claim) {
if !w.nameReplacement(n, next.ID, "pinning") {
return n.Op.Stuck != "" // stuck: the CAS records it
}
+ w.abandonPrepared(n)
n.Op.Exec = -1
n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
@@ -1181,13 +1230,15 @@ func (w *world) regionHAOwnsLoss(b *box) bool {
switch c.Op.Kind {
case "serving", "relocating":
if c.Op.Exec == b.ID && w.perRegion > 1 {
- // finding F2 (model ruling 17): an executor none of whose files
- // manifests has landed (an adopted legacy host before its first
- // publication, a new host before its first manifest lands) would
- // fail over to a fresh instance.key; the sweep leaves it alone,
- // and TestFailoverBeforeTheFirstManifest shows the loss
+ // the L21 window (plan ruling 17): an executor whose newest
+ // landed manifest carries no instance.key (none landed yet, or
+ // only the pre-start copy) is unrecoverable by any relocation:
+ // its failover is stuck by design (1b-next ruling 25) and never
+ // converges, so the sweep leaves it alone; the witness for
+ // files-pin-needs-key and TestFailoverBeforeTheFirstManifest
+ // show it fail safe
_, _, _, _, m := w.newestManifest(b.Region, c.Holder.Location, c.Holder.Gen)
- return m != nil
+ return manifestHasKey(m)
}
return true
}
@@ -1470,6 +1521,14 @@ func (w *world) replaceTarget(n *claim, x *box) bool {
}
next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...)
if next == nil {
+ if on("reloc-dead-target-bound") && w.now > x.TerminatedAt+releaseDeadline {
+ // FenceTargetWithoutSpare (1b-next rev 18 finding 2): the fence
+ // is consumed ReleaseDeadline after its observed_at and the
+ // operation is stuck; the mutation waits for a spare for ever
+ w.stats["relocation: dead target with no spare fenced"]++
+ w.fenceTargetStuck(n, x, fmt.Sprintf("box %d terminated and no spare in %d steps", x.ID, releaseDeadline))
+ return true
+ }
w.stats["relocation: target lost, no spare yet"]++
return false
}
@@ -1486,6 +1545,7 @@ func (w *world) replaceTarget(n *claim, x *box) bool {
case !late || !on("reloc-replacement-table"):
w.handExec(n, next.ID, "installed", n.Op.Prepared) // P was never opened: to' makes its own local install and opens it
default:
+ w.abandonPrepared(n)
n.Op.Exec, n.Op.Phase = -1, "pinning"
n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil
n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
@@ -1509,8 +1569,14 @@ func (w *world) replaceTarget(n *claim, x *box) bool {
// mutation is rev 8's: always op.exec none at pinning, which revokes a
// live source without its stop evidence.
func (w *world) fenceExhaustedTarget(n *claim, x *box) {
- why := fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements)
w.stats["relocation: exhausted target fenced"]++
+ w.fenceTargetStuck(n, x, fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements))
+}
+
+// fenceTargetStuck is 1b-next's fenceTargetStuck, the body
+// FenceExhaustedTarget and FenceTargetWithoutSpare share (rev 18): phase
+// sensitive as above; an unopened P is kept for the operator.
+func (w *world) fenceTargetStuck(n *claim, x *box, why string) {
if on("reloc-exhausted-fence") && n.Op.Exec >= 0 && n.Op.Exec != x.ID {
n.Op.Stuck = why
return
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 2b9079246..2523a7f01 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -751,3 +751,74 @@ func wRelocPinEvidencedEmpty(t *testing.T, w *world) {
w.servingOn(t, nil)
w.finish(t)
}
+
+// rev 3: 1b-next rev 17 to 19's fixes for findings F1 to F3, and L21
+
+// wL21Window (files-pin-needs-key): the L21 window, explicit. The cold
+// admission's pre-start manifest copy has landed without instance.key
+// (§5.6 copies the manifest before the app starts); the app minted the
+// key after it started, wrote rows sealed with it and replicated them;
+// the publisher's manifest carrying the key has not landed when the box
+// is terminated. Recovery fails safe: the pin refuses, the operation is
+// stuck, and no database is installed without its key. Without the rule
+// the keyless manifest is pinned and the install mints a fresh key over
+// the sealed rows (INV-4).
+func wL21Window(t *testing.T, w *world) {
+ w.twoBox()
+ from := w.boxes[0]
+ w.serve(from, 1, app0)
+ h := w.claim.Holder
+ w.issued++
+ pre := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: 1, Base: w.issued} // the pre-start copy: no files, no key
+ k := manifestKey(h.Location, h.Gen, 1)
+ w.buckets[0].objs[k] = []*version{{ID: w.newVer(), B: pre}}
+ from.pubGen, from.pubSeq = h.Gen, 1
+ w.holdKey(h.Location + "files/") // the manifest with the key never lands
+ w.running(t, from)
+ w.appWrite(from)
+ w.replicate(from)
+ w.drive(30, never, w.act(from)) // the rows' uploads land; the manifest stays held
+ w.terminate(from)
+ w.drive(400, func() bool { return len(w.violations) > 0 || w.claim.Op.Stuck != "" }, w.actAll(), w.recoveryPass, w.wakeExec)
+ if len(w.violations) == 0 {
+ if c := w.claim; c.Op.Stuck == "" || c.Op.Prepared != "" {
+ w.violate("INV-3 (witness): the L21 failover neither stopped nor installed: %s", w.state())
+ }
+ }
+}
+
+// wNoSpareBound (reloc-no-spare-bound, F1): a drain's target fails its
+// probe in a two-box region; with the bound the operation is stuck and
+// the operator returns the host to the source; without it, it waits.
+func wNoSpareBound(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ to.FailApp = true
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, from)
+ w.finish(t)
+}
+
+// wDeadTargetBound (reloc-dead-target-bound, rev 18 finding 2): the
+// drain's target is terminated at installing and the group launches no
+// replacement (region 0 kept at one box: a capacity shortage), so no
+// spare exists. With the bound the fence is consumed ReleaseDeadline
+// later, the operation is stuck, and the operator's replay serves the
+// host on the source; without it nothing moves.
+func wDeadTargetBound(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.drainTo(t, to)
+ w.oneBoxRegion[0] = true
+ if !w.relocPhase(t, "installing", w.act(from, to), w.recoveryPass) {
+ return
+ }
+ w.terminate(to)
+ w.servingOn(t, from)
+ w.finish(t)
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index ac25284a9..7af7a8064 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -181,4 +181,9 @@ var allRules = []string{
"files-pin-exact", // region HA §5.8 the pinned recovery set, B2-4 (RecoveryPin.FilesManifest, StorePinner, ruling 21's retained copy): the local install applies the manifest version the pin names; the mutation reads the newest at install time. A determinism rule: a later PUT adds a version nothing reads (expected miss)
"files-live-set", // region HA §5.6, L13, claim §6.2a (the classifier's files live set, 1b-next rev 12 finding 1's referenced origins): a park-generation never archives the live manifest of the chain, holder.generation's, P's or the pinned one; the mutation archives them with their dead generation
"files-prepared-seq-zero", // claim rev 6.30 R18-1, moves rev 7.22 §7.6, 1b-next rev 15 finding 1 (CopyPinnedManifest, PreparedAuthority.FilesSeq 0): P's prepared manifest is at sequence 0 and the session publisher starts at 1; the mutation keeps the source's sequence, so a later pin takes the stale prepared manifest over the session's (INV-28)
+ // plan 1b-next rev 17 to 19's fixes for the model's findings F1 to F3 (rev 3 of this plan)
+ "reloc-no-spare-bound", // 1b-next ruling 26 (rev 17, F1): probe-failed with no eligible spare is stuck ReleaseDeadline after probe_failed_since, never sent to the source; the mutation waits for ever (INV-3)
+ "reloc-dead-target-bound", // 1b-next rev 18 finding 2 (FenceTargetWithoutSpare): a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at; the mutation waits for ever (INV-3)
+ "reloc-abandoned-prepared", // 1b-next ruling 27, rev 18 finding 3 (abandonPrepared, abandoned_prepared): every unopened P that is replaced or dropped, on every path, is parked at completion; the mutation records none (INV-10)
+ "files-pin-needs-key", // 1b-next ruling 25 as rev 18 amended it (F2, L21): a nonempty database with an admitted writer pins only a manifest carrying instance.key, else stuck; the mutation pins it keyless and the install mints a fresh key (INV-4)
}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 34544e7ba..5b7fa7720 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -218,8 +218,8 @@ var witnesses = []witness{
"the executor registers a timer whose manifest never lands and is terminated; the fence drops the timer silently", wFenceDeclaresTimers},
{"reloc-enrolled-only", "reloc-enrolled-only", "INV-27",
"the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly},
- {"files-live-set", "files-live-set", "INV-4",
- "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover's install starts over data sealed with a key no manifest carries", wFilesLiveSet},
+ {"files-live-set", "files-live-set", "INV-3",
+ "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover finds no manifest carrying instance.key: stuck, never served (rev 3: 1b-next ruling 25 makes the loss fail safe; with files-pin-needs-key also gone it is INV-4)", wFilesLiveSet},
{"reloc-pin-claim-gen", "reloc-pin-claim-gen", "INV-3",
"a pinner observed the first round after the source's release and stalled; after the target wrote into P and died, its stale selection of generation_from is journaled for the nested pinning, and the build waits forever for objects generation_from's own park retired", wRelocPinClaimGen},
{"reloc-release-deadline", "reloc-release-deadline", "INV-3",
@@ -240,6 +240,13 @@ var witnesses = []witness{
"a failover whose listing finds nothing although the writes are durable: with the rule the operation is stuck until an operator resolves it on a listing that shows them; without it the pin is empty and the install loses the durable writes", wRelocPinEvidencedEmpty},
{"files-prepared-seq-zero", "files-prepared-seq-zero", "INV-28",
"the source's manifests reach sequence 3; P's prepared manifest keeps 3, the probe session publishes its timer at 1, and the nested failover pins and declares from the stale prepared manifest", wFilesPreparedSeqZero},
+ // rev 3: 1b-next rev 17 to 19's fixes for the model's findings, and the L21 window
+ {"files-pin-needs-key", "files-pin-needs-key", "INV-4",
+ "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window},
+ {"reloc-no-spare-bound", "reloc-no-spare-bound", "INV-3",
+ "F1: a drain's target fails its probe in a two-box region with no spare; with the bound the operation is stuck and the operator's resolve returns the host to the source, without it it waits for ever", wNoSpareBound},
+ {"reloc-dead-target-bound", "reloc-dead-target-bound", "INV-3",
+ "rev 18 finding 2: the target dies at installing and no spare is launched; with the bound the fence is consumed into stuck and the operator's replay serves on the source, without it nothing moves", wDeadTargetBound},
}
// TestWitnesses is the deterministic half of the mutation evidence.
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index 19ce89d71..cfb51f788 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -826,7 +826,7 @@ type opState struct {
Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1)
Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
- Built []string // every prepared generation this operation built: one no writer opened is parked at serving (model ruling 16)
+ Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27)
// journal
ReportAt int
@@ -1221,7 +1221,7 @@ func (c *claim) clone() *claim {
n.Op.Excluded = append([]int(nil), c.Op.Excluded...)
n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)
n.Op.Discharged = append([]int(nil), c.Op.Discharged...)
- n.Op.Built = append([]string(nil), c.Op.Built...)
+ n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...)
if r := c.Op.Release; r != nil {
cp := *r
cp.Files = r.Files.clone()