amadan
settings-4 task 11: fix round 1: the mirror matches production; the resolution order is gated
- The failure book goes to Target only for routes with settings, as
settingsTarget's !plain does (ruling R-T6-BOOK-2). Invariant 4 is scoped
to settings routes, and its comment is corrected.
- A scripted sub-test replays the seed-531 shape through the model's
actions, and so through the production Target, NextConsumed and
NextBuildState: a resolution left on box0, a re-resolution on box1 under
a pin, a return, then an unpin. It asserts that rule 2 installs the build
state's T and that the wake completes R1. Every invariant is checked at
each step.
- Invariant 3 also checks the decision: only the head rests on the
pointer, and only the head bakes. The repoint half is documented as
holding by construction of the mirror.
- boxView reads the build state before the file (R-RESOLUTION-STATE-WINS).
Sweep: UPDATESIM_SEEDS=3000 UPDATESIM_PAR=2 nice -n 19 go test -p 1:
PASS, ok 0.308s.
Mutants: each ran in a fresh mktemp copy of 72d23724 plus this file, at
200 seeds, and the copy was deleted after the run:
- M1: INVARIANT 1, 56/200 (seed 4: box1 resolved R4 again).
- M2: INVARIANT 5, 20/200 (seed 6: held, R3 behind baking b5, live b5);
also 6.
- M3: INVARIANT 1, 60/200 (seed 1: wake records R7 newly completed);
also 5, including the scripted sub-test at step 1.
- M4: INVARIANT 4, 72/200 (seed 3: box2 repointed onto failed b5).
- M5: INVARIANT 5, 47/200 (seed 2: held instance repointed onto b5).
- M6: INVARIANT 6, 86/200 (seed 1: R3 pending and eligible under pin
b1, not resolved); also the scripted sub-test at step 5.
- M7: INVARIANT 1, 10/200 (seed 87: rule 2 selected completed R1); also
5, 6.
- M8': INVARIANT 1, 10/200 (seed 87); INVARIANT 6, 77/200 (seed 1: box0
resolved R1 to b1, no first eligible).
- M9 (only resolvedFor's order reverted): killed by the scripted
sub-test's invariant line, "INVARIANT 6 ... in the scripted seed-531
shape at step 9 (root@box0 {request "b2"}: up to date): rule 2 installs
b2 for R1; first eligible "b3"". The random seeds alone do not kill it
at 200.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+113
−16
internal/release/updatesim_test.go+113 −16
diff --git a/internal/release/updatesim_test.go b/internal/release/updatesim_test.go| index 6a367d92c..6f2adb290 100644 |
| --- a/internal/release/updatesim_test.go |
| +++ b/internal/release/updatesim_test.go |
| @@ -38,12 +38,17 @@ import ( |
| // the pass. UPDATESIM_STRICT=1 reads every box's consumed file at once |
| // instead; that is documentation of a known gap, not the gate (below). |
| // 2. The build state names the build that last touched the database. |
| -// 3. No install lacks evidence: every repoint is the head, a build with a |
| -// promotion record, or the box's own staged copy. |
| -// 4. Failure records outrank: no repoint a Target decision makes lands on a |
| -// build the box holds as failed (the model never sets GoodVersion, so no |
| -// instance has served a failed build; default routes with no consumed |
| -// file keep today's adoption, which never read the book: R-T6-BOOK). |
| +// 3. No install lacks evidence. At the decision: Target names pointer |
| +// evidence only for the head, and asks for bake only on the head. At |
| +// the repoint: the build is the head, has a promotion record, or is the |
| +// box's own staged copy; that half holds by construction of the |
| +// adoptHost mirror (its evidence switch), and is kept as a tripwire. |
| +// 4. Failure records outrank: no repoint a Target decision makes for a |
| +// route with settings lands on a build the box holds as failed (the |
| +// model never sets GoodVersion, so no instance has served a failed |
| +// build). A route with default settings keeps today's adoption, which |
| +// never reads the book, consumed file or not (rulings R-T6-BOOK, |
| +// R-T6-BOOK-2; adopt.go settingsTarget's !plain), so it is out of scope. |
| // 5. Unresolved requests block nothing: a held instance with an unresolved |
| // request whose head is baking recovers onto last_executed; and a held |
| // instance (no pin) never repoints anywhere but last_executed, a T its |
| @@ -76,6 +81,7 @@ import ( |
| // replays seed n alone. A failure prints the seed, the step and the trace, |
| // and a line "INVARIANT <n> ..." per invariant any seed violated. |
| func TestUpdateRequestLifecycleSimulation(t *testing.T) { |
| + t.Run("seed 531 shape, unpinned", testUpdateSimSeed531Unpinned) |
| seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200) |
| par := updateSimEnv(t, "UPDATESIM_PAR", 1) |
| first := 0 |
| @@ -143,6 +149,69 @@ func TestUpdateRequestLifecycleSimulation(t *testing.T) { |
| } |
| } |
| +// testUpdateSimSeed531Unpinned replays the shape seed 531 found, through |
| +// the model's own actions (so every invariant is checked at every step) and |
| +// so through the production Target, NextConsumed and NextBuildState. Box 0 |
| +// resolves R1 to b2 and the instance moves before any wake; box 1 resolves |
| +// R1 again, to b3, under a pin set after the request, and its wake (running |
| +// the pin) carries {R1, b3} into the build state; the instance returns to |
| +// box 0, whose file still says {R1, b2}, and the pin is cleared. Rule 2 must |
| +// then install the build state's b3 (R-RESOLUTION-STATE-WINS), and the wake |
| +// that runs it must complete R1. The random schedule reaches the |
| +// disagreement only under a pin, and rarely clears it in time, so this |
| +// guards resolvedFor's order by itself. |
| +func testUpdateSimSeed531Unpinned(t *testing.T) { |
| + w := newUpdateSimWorld(0, false) |
| + for i := range w.boxes { |
| + w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i)) |
| + } |
| + w.builds = []string{"b1", "b2", "b3"} |
| + for i, b := range w.builds { |
| + w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true |
| + } |
| + w.head = "b2" |
| + for _, b := range w.boxes[:2] { |
| + b.eligible["b1"], b.eligible["b2"] = true, true |
| + } |
| + w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"} |
| + w.lastRan, w.replica = "b1", true |
| + w.at = 0 |
| + w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true |
| + w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)} |
| + w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1} |
| + |
| + steps := []func() string{ |
| + func() string { return w.rootPass(w.boxes[0], true) }, |
| + func() string { w.settings.Pin = "b1"; return "pin b1 (after the request)" }, |
| + func() string { return w.moveTo(1, true) }, |
| + func() string { w.head = "b3"; w.boxes[1].eligible["b3"] = true; return "promote b3, baked on box1" }, |
| + func() string { return w.rootPass(w.boxes[1], true) }, |
| + func() string { return w.wake(w.boxes[1]) }, |
| + func() string { return w.moveTo(0, true) }, |
| + func() string { w.settings.Pin = ""; return "unpin" }, |
| + func() string { return w.rootPass(w.boxes[0], true) }, |
| + func() string { return w.wake(w.boxes[0]) }, |
| + } |
| + for i, step := range steps { |
| + w.viols = nil |
| + action := step() |
| + w.trace = append(w.trace, fmt.Sprintf("%3d %s %s", i+1, action, w.summary())) |
| + w.check() |
| + for _, v := range w.viols { |
| + t.Errorf("INVARIANT %d (%s) violated in the scripted seed-531 shape at step %d (%s): %s\ntrace:\n%s", |
| + v.inv, updateSimInvariants[v.inv], i+1, action, v.msg, strings.Join(w.trace, "\n")) |
| + } |
| + if len(w.viols) > 0 { |
| + return |
| + } |
| + } |
| + if st := w.state; st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[0].live != "b3" { |
| + t.Errorf("scripted seed-531 shape: after the unpinned pass and wake on box0, live %q, build state %+v; want b3 live and R1 completed by it\ntrace:\n%s", |
| + w.boxes[0].live, w.state, strings.Join(w.trace, "\n")) |
| + } |
| + t.Logf("trace:\n%s", strings.Join(w.trace, "\n")) |
| +} |
| + |
| const ( |
| updateSimHost = "blog.example.com" |
| updateSimSteps = 80 |
| @@ -433,13 +502,18 @@ func (w *simWorld) refresh() string { |
| // source's column (registry coldhandover copies build_state). A box the |
| // instance returns to still has its old consumed file and live link. |
| func (w *simWorld) move() string { |
| - src := w.cur() |
| j := w.rng.Intn(len(w.boxes) - 1) |
| if j >= w.at { |
| j++ |
| } |
| + return w.moveTo(j, w.rng.Intn(100) < 50) |
| +} |
| + |
| +// moveTo moves the instance to box j; carried is whether the destination's |
| +// registry row carries the source's build-state copy. |
| +func (w *simWorld) moveTo(j int, carried bool) string { |
| + src := w.cur() |
| dst := w.boxes[j] |
| - carried := w.rng.Intn(100) < 50 |
| if carried { |
| dst.copy = cloneSimCopy(src.copy) |
| } else { |
| @@ -625,7 +699,8 @@ func (w *simWorld) watermarkAnywhere() uint64 { |
| } |
| // boxView is what a pass on b can see of request r: pending (above both |
| -// sources' completed ids) and the T either source resolved it to. |
| +// sources' completed ids) and the T either source resolved it to, the build |
| +// state's first (R-RESOLUTION-STATE-WINS). |
| func boxView(c *Consumed, st *BuildState, r uint64) (pending bool, t string) { |
| var m uint64 |
| if c != nil { |
| @@ -637,12 +712,12 @@ func boxView(c *Consumed, st *BuildState, r uint64) (pending bool, t string) { |
| if r == 0 || r <= m { |
| return false, "" |
| } |
| - if c != nil && c.Resolved != nil && c.Resolved.ID == r { |
| - return true, c.Resolved.Target |
| - } |
| if st != nil && st.Resolved != nil && st.Resolved.ID == r { |
| return true, st.Resolved.Target |
| } |
| + if c != nil && c.Resolved != nil && c.Resolved.ID == r { |
| + return true, c.Resolved.Target |
| + } |
| return true, "" |
| } |
| @@ -679,9 +754,15 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| if !b.eligible[head] { |
| in.HeadHeld = "in its supply-chain bake window" |
| } |
| - failed := b.failed |
| - in.Failed = func(v string) bool { return failed[v] } |
| + // settingsTarget gives Target the failure book only for a route |
| + // with settings (!plain); default settings keep today's adoption, |
| + // which never read it, even with a consumed file (R-T6-BOOK-2). |
| + if !u.Default() { |
| + failed := b.failed |
| + in.Failed = func(v string) bool { return failed[v] } |
| + } |
| dec = Target(in) |
| + w.checkEvidence(dec, head) |
| w.checkDecision(b, in, dec, resolve, wmBefore, held) |
| if resolve { |
| next := NextConsumed(in, dec) |
| @@ -742,11 +823,12 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| return desc + ": no evidence" |
| } |
| - // The repoint. |
| + // The repoint. Invariant 3's repoint half holds by construction of the |
| + // evidence switch above; it stays as a tripwire for the mirror. |
| if !(ver == head || w.promoted[ver] || stagedBefore) { |
| w.fail(3, "repointed onto %s: not the head %s, no promotion record, not staged on %s", ver, head, b.name) |
| } |
| - if viaTarget && b.failed[ver] { |
| + if viaTarget && !u.Default() && b.failed[ver] { |
| w.fail(4, "%s repointed onto %s, which it holds as failed (%s)", b.name, ver, simDec(dec)) |
| } |
| if viaTarget && held && u.Pin == "" { |
| @@ -773,6 +855,21 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| return fmt.Sprintf("%s: repoint %q->%s", desc, prev, ver) |
| } |
| +// checkEvidence is invariant 3 at the decision: only the head rests on the |
| +// signed pointer, and only the head bakes (§4.1, §4.3: a pin, a resolved T |
| +// and a recovery waive bake and need a record or a staged copy). |
| +func (w *simWorld) checkEvidence(dec TargetDecision, head string) { |
| + if dec.Version == "" || dec.Version == head { |
| + return |
| + } |
| + if dec.Evidence == EvidencePointer { |
| + w.fail(3, "decision %s rests on the pointer for %s, not the head %s", simDec(dec), dec.Version, head) |
| + } |
| + if dec.Bake { |
| + w.fail(3, "decision %s bakes %s, not the head %s", simDec(dec), dec.Version, head) |
| + } |
| +} |
| + |
| // checkDecision checks invariants 1 and 6 on one Target decision, before |
| // root writes it. |
| func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, resolve bool, wmBefore uint64, held bool) { |