From 6c48b61455f296492fd138c633d7d957a7d1be51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?St=C3=A9phane=20ROBERT?= Date: Mon, 21 Sep 2026 08:25:00 +0200 Subject: [PATCH] fix(ci): the nightly runtime proof asks the emulator what it verified MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `runtime` job ran the four dataplane suites, the leftovers doorstep, and nothing else of guard.sh. Both local reproductions of those same suites call `guard.sh verification` before the emulator stops — leg.sh and day2.sh — so a claim the emulator itself published as broken reddened a workstation and never a night. `runtime-proof` is the gate #736 wanted a green night from before tagging, and a green there did not say the claims held. Measured before arming it, because a gate that starts red teaches people to ignore it and #731 is about exactly that: on 2026-09-15, after #741 closed the one claim breaking under OVN, the incus-ovn leg answers `held=58 broken=0 unreadable=0 repaired=0`. The step is `if: always()` and runs before the emulator stops, because the counters and the claims die with the process (#670). **What the falsification taught, and it is the better half of this change.** The test was written as three `strings.Contains` over the workflow text, and both mutations went straight through it: - commenting the step out keeps every name in the file, so a grep-shaped test stays green while the night asks nothing. The test now drops whole-line YAML comments before reading, so it reads steps rather than text; - `if: always() == false` CONTAINS `if: always()`. The test now compares the step's `if:` as a whole line, so a longer expression that merely starts the same way cannot satisfy it. Neither defect was visible from reading the test. Both mutations bite now. Closes #740 Assisted-by: Claude Code (claude-opus-5) --- .github/workflows/runtime-proof.yml | 21 +++ tools/ci/runtime_verification_test.go | 129 ++++++++++++++++++ .../the-night-asks-what-was-verified.json | 21 +++ 3 files changed, 171 insertions(+) create mode 100644 tools/ci/runtime_verification_test.go create mode 100644 tools/falsify/specs/the-night-asks-what-was-verified.json diff --git a/.github/workflows/runtime-proof.yml b/.github/workflows/runtime-proof.yml index 6c084e9..22ee274 100644 --- a/.github/workflows/runtime-proof.yml +++ b/.github/workflows/runtime-proof.yml @@ -424,6 +424,27 @@ jobs: if: always() run: sudo tools/conformance/score.sh http://127.0.0.1:4599 + # What the emulator read back against every machine's plan, asked before + # it stops because the counters and the claims die with it (#670). + # + # This job ran the four dataplane suites and never asked (#740). The two + # local reproductions of those same suites do — leg.sh and day2.sh both + # call it — so a claim the emulator itself published as broken reddened a + # workstation and never a night. `runtime-proof` is the gate #736 wanted a + # green night from before tagging, and a green here did not say the claims + # held. + # + # Measured before arming it, because a gate that starts red teaches people + # to ignore it and #731 is about exactly that: on 2026-09-15, after #741 + # closed the one claim that was breaking under OVN, the incus-ovn leg + # answers `held=58 broken=0 unreadable=0 repaired=0`. + # + # `if: always()` so a suite that already failed still gets its claims + # reported rather than hiding them behind the first red. + - name: What the emulator verified against every plan + if: always() + run: sudo tools/conformance/guard.sh verification http://127.0.0.1:4599 + # On failure only: what the emulator saw, and what the runtime holds — # the two views whose disagreement is usually the diagnosis. - name: The emulator's log and the runtime's state diff --git a/tools/ci/runtime_verification_test.go b/tools/ci/runtime_verification_test.go new file mode 100644 index 0000000..289ec03 --- /dev/null +++ b/tools/ci/runtime_verification_test.go @@ -0,0 +1,129 @@ +package ci + +import ( + "os" + "path/filepath" + "strings" + "testing" +) + +// The nightly runtime proof asks the emulator what it verified, and gates on +// the answer. +// +// It did not, for as long as the gate existed (#740). The `runtime` job ran the +// four dataplane suites and the leftovers doorstep and nothing else of +// guard.sh, while both local reproductions of those same suites — +// tools/conformance/leg.sh and tools/conformance/day2.sh — call +// `guard.sh verification` before the emulator stops. So a claim the emulator +// itself published as broken reddened a workstation and never a night, and +// `runtime-proof` is the gate #736 wanted a green night from before tagging: a +// green there did not say the claims held. +// +// Three properties, and the first alone would be a comment: +// +// 1. the step exists in the job that boots machines; +// 2. it runs BEFORE the emulator is stopped, because the counters and the +// claims die with the process (#670); +// 3. it is `if: always()`, so a suite that already failed still gets its +// claims reported rather than hiding them behind the first red. +func TestTheRuntimeProofAsksWhatTheEmulatorVerified(t *testing.T) { + workflow := readWorkflow(t, "runtime-proof.yml") + + const step = "tools/conformance/guard.sh verification" + if !strings.Contains(workflow, step) { + t.Fatalf("runtime-proof.yml never runs %q: the four dataplane suites pass, the "+ + "emulator publishes a broken claim on /_feint/health, and the night says green", step) + } + + verifyAt := strings.Index(workflow, step) + stopAt := strings.Index(workflow, "feint stop --addr 127.0.0.1:4599") + if stopAt < 0 { + t.Fatal("runtime-proof.yml no longer stops its emulator; this test's ordering check has lost its subject") + } + if verifyAt > stopAt { + t.Error("the verification step runs after the emulator is stopped: the claims and the " + + "counters die with the process, so it would ask a dead endpoint and pass on nothing") + } + + // The `if:` of the step itself, read from the block that declares it rather + // than from anywhere in the file: a distant `if: always()` would satisfy a + // naive Contains and prove nothing about this step. + // + // And compared as a whole LINE, not as a substring. `if: always() == false` + // contains `if: always()`, so a substring check calls a step that can never + // run correctly armed — the falsification for this spec is that exact + // mutation, and it stayed green until this read the line. + block := stepBlock(workflow, "What the emulator verified against every plan") + if block == "" { + t.Fatal("no step named `What the emulator verified against every plan`: the name is what a " + + "reader of a job log looks for, and what night-report.yml quotes when it fails") + } + if got := conditionOf(block); got != "always()" { + t.Errorf("the verification step is `if: %s`, want `if: always()`: a suite failing earlier "+ + "would skip it, and the claims of the very run that went wrong are the ones worth reading", got) + } + if !strings.Contains(block, step) { + t.Errorf("the step named for the verification does not run it:\n%s", block) + } +} + +// stepBlock returns the lines of one `- name:` step, up to the next step at the +// same indentation. Returns "" when no step carries that name. +func stepBlock(workflow, name string) string { + start := strings.Index(workflow, "- name: "+name) + if start < 0 { + return "" + } + rest := workflow[start+1:] + if next := strings.Index(rest, "\n - name: "); next >= 0 { + return workflow[start : start+1+next] + } + return workflow[start:] +} + +// conditionOf answers a step's `if:` expression, or "" when it declares none. +// +// The whole line, so a check on it cannot be satisfied by a longer expression +// that merely starts the same way. +func conditionOf(block string) string { + for _, line := range strings.Split(block, "\n") { + trimmed := strings.TrimSpace(line) + if after, found := strings.CutPrefix(trimmed, "if:"); found { + return strings.TrimSpace(after) + } + } + return "" +} + +func readWorkflow(t *testing.T, name string) string { + t.Helper() + body, err := os.ReadFile(filepath.Join("..", "..", ".github", "workflows", name)) + if err != nil { + t.Fatalf("read %s: %v", name, err) + } + return withoutComments(string(body)) +} + +// withoutComments drops every whole-line YAML comment. +// +// Without it this test reads text rather than steps, and a step commented out +// still satisfies every `strings.Contains` below — which is the difference +// between checking a form and checking a behaviour. The falsification for this +// change is exactly that mutation: comment the step out, keeping every name in +// the file, and the night stops asking what the emulator verified while a +// grep-shaped test stays green. +// +// Whole-line only, on purpose. A `#` inside a value is part of the value, and a +// blanket strip would cut `127.0.0.1:4599 # the emulator` down to something this +// test's ordering check could no longer find. +func withoutComments(workflow string) string { + lines := strings.Split(workflow, "\n") + kept := lines[:0] + for _, line := range lines { + if strings.HasPrefix(strings.TrimSpace(line), "#") { + continue + } + kept = append(kept, line) + } + return strings.Join(kept, "\n") +} diff --git a/tools/falsify/specs/the-night-asks-what-was-verified.json b/tools/falsify/specs/the-night-asks-what-was-verified.json new file mode 100644 index 0000000..01ecb27 --- /dev/null +++ b/tools/falsify/specs/the-night-asks-what-was-verified.json @@ -0,0 +1,21 @@ +{ + "package": "./tools/ci/", + "mutations": [ + { + "label": "the night stops asking what the emulator verified: the step is commented out rather than deleted, so every name in the file survives and only a test that reads STEPS rather than TEXT can notice (#740)", + "file": ".github/workflows/runtime-proof.yml", + "package": "./tools/ci/", + "find": " - name: What the emulator verified against every plan\n if: always()\n run: sudo tools/conformance/guard.sh verification http://127.0.0.1:4599", + "replace": " # - name: What the emulator verified against every plan\n # if: always()\n # run: sudo tools/conformance/guard.sh verification http://127.0.0.1:4599", + "test": "TestTheRuntimeProofAsksWhatTheEmulatorVerified" + }, + { + "label": "the step stops being `if: always()`, so a suite that already failed hides the claims of the very run that went wrong", + "file": ".github/workflows/runtime-proof.yml", + "package": "./tools/ci/", + "find": " - name: What the emulator verified against every plan\n if: always()\n", + "replace": " - name: What the emulator verified against every plan\n if: always() == false\n", + "test": "TestTheRuntimeProofAsksWhatTheEmulatorVerified" + } + ] +}