amadan
settings-4: the scripted disagreement gates M9 again
Ruling R-M9-SCRIPTED: a scripted sub-test builds the state directly (box0's
consumed file {R1, b1}, the build state {R1, b3}, unpinned and manual),
reachable from a pre-fence binary's racing write or a copy stale for one
reconcile. Root's rule 2 must install b3 and the wake must complete R1, so
resolvedFor's order is gated in the simulation again.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+53
−0
internal/release/updatesim_test.go+53 −0
diff --git a/internal/release/updatesim_test.go b/internal/release/updatesim_test.go| index 5dddd3947..2a4de8a41 100644 |
| --- a/internal/release/updatesim_test.go |
| +++ b/internal/release/updatesim_test.go |
| @@ -103,6 +103,7 @@ import ( |
| func TestUpdateRequestLifecycleSimulation(t *testing.T) { |
| t.Run("seed 531 shape, unpinned", testUpdateSimSeed531Unpinned) |
| t.Run("carry fence, a failed completion racing a cut", testUpdateSimCarryFence) |
| + t.Run("a file and the build state disagree on R1", testUpdateSimDisagreement) |
| seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200) |
| par := updateSimEnv(t, "UPDATESIM_PAR", 1) |
| first := 0 |
| @@ -249,6 +250,58 @@ func runScriptedSim(t *testing.T, name string, w *simWorld, steps []func() strin |
| return true |
| } |
| +// testUpdateSimDisagreement gates resolvedFor's order (ruling |
| +// R-RESOLUTION-STATE-WINS; ruling R-M9-SCRIPTED) on a state built directly: |
| +// box 0's consumed file resolves the pending R1 to b1 while the build state |
| +// resolves the same R1 to b3, unpinned and manual. Under the carry fence no |
| +// graceful path in this model leaves that state behind any more. It is still |
| +// reachable in production from a box running a pre-fence binary (a racing |
| +// root pass wrote its record after the cut's carry), or from a registry copy |
| +// that stays stale for one reconcile without a read error (root resolves R1 |
| +// again from a copy that lacks the state's resolution). Root's rule 2 must |
| +// install the build state's b3 (through the production Target and |
| +// NextConsumed), and the wake that runs it must complete R1 (DecideHeldWake, |
| +// HeldExecStale and NextBuildState). Following the file would run b1, which |
| +// never completes R1. |
| +func testUpdateSimDisagreement(t *testing.T) { |
| + w := newUpdateSimWorld(0, false) |
| + w.scripted = true |
| + 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 = "b3" |
| + for _, b := range w.boxes { |
| + b.eligible["b1"], b.eligible["b2"], b.eligible["b3"] = true, true, true |
| + } |
| + w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b2", Resolved: &ResolvedRequest{ID: 1, Target: "b3"}} |
| + w.lastRan, w.replica = "b2", true |
| + w.at = 0 |
| + b0 := w.boxes[0] |
| + b0.live, b0.staged["b2"] = "b2", true |
| + b0.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)} |
| + b0.consumed = &Consumed{Schema: 1, Host: updateSimHost, Resolved: &ResolvedRequest{ID: 1, Target: "b1"}} |
| + w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1} |
| + // R1's resolution as the world records it: the build state's |
| + // (R-RESOLUTION-STATE-WINS), so invariant 6 judges installs against b3. |
| + w.syncResolutions() |
| + steps := []func() string{ |
| + func() string { return w.rootPass(b0, true) }, |
| + func() string { return w.wake(b0) }, |
| + } |
| + const name = "the scripted disagreement (file {R1, b1}, build state {R1, b3})" |
| + // The outcome is asserted even when an invariant stopped the steps early. |
| + runScriptedSim(t, name, w, steps) |
| + if st := w.state; b0.live != "b3" || st == nil || st.LastExecuted != "b3" || st.Completed != 1 || st.CompletedFailed { |
| + t.Errorf("%s: live %q, build state %+v; want rule 2 to install the build state's b3 and its wake to complete R1\ntrace:\n%s", |
| + name, b0.live, st, strings.Join(w.trace, "\n")) |
| + } |
| + t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n")) |
| +} |
| + |
| // testUpdateSimCarryFence is Astra round 2 finding 2's shape (ruling |
| // R-CARRY-FENCE), scripted both ways. Box 0 resolves R1 to b2 and installs |
| // it; b2 then fails on box 0, so root's next pass there records R1 |