TEST ONLY (do not merge): #890 gate mutation — prove CI goes RED - #895
Closed
avrabe wants to merge 5 commits into
Closed
TEST ONLY (do not merge): #890 gate mutation — prove CI goes RED#895avrabe wants to merge 5 commits into
avrabe wants to merge 5 commits into
Conversation
…(step 1/5) Adds scripts/oracle_wiring_check.py: every scripts/repro/*.py|*.sh must carry exactly one `# ci-status:` declaration (wired | manual (<category>) — reason | unwired — reason), and a `wired` declaration is VERIFIED against .github/workflows/*.yml so a green board can never sit on top of an inert gate. Step 1 declares the 82 scripts a workflow already references. The remaining 70 are UNDECLARED and the gate is red on them by construction — classified next. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ns (step 2/5)
Read and classified the 70 scripts no workflow referenced. 63 of them run green
against a freshly built synth right now (verified locally, one at a time) and
are wired in the next step; 7 are genuinely manual and say WHY, in a closed
category vocabulary (measurement / scratch / external-input) rather than free
text.
Three enabling fixes fall out of the audit:
* base_cse / leaf_dead_frame / load_store_big_offset_382 / uxth_fold hardcoded
./target/{debug,release}/synth; they now honour $SYNTH (same literal default)
so CI can point them at its own build.
* sret_decide_differential printed "MISMATCH <-- BUG" and still exited 0 —
wiring it as-is would have added a gate that CANNOT fail. The verdict is now
the exit status (proved: mutating the -35 expectation to -34 gives rc=1).
The gate is deliberately still red: 63 files declare `wired` while no workflow
references them. That is the exact defect being fixed, and it is now MACHINE
VISIBLE instead of requiring a 150-file read.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… 3/5) Four new sweep jobs (selector / memory / rv32 / wcet) plus one step in the existing fact-spec job run the 63 differentials that were sitting in scripts/repro/ with nothing executing them. Every one was verified green locally against a freshly built synth before being wired — the compile line comes from each harness's own documented Run: block. Highlights of what was NOT being gated: the six mem757_* red-first reconstructions of gale's wrong-segment miscompile (#757); every RV32 oracle for a regression gale found on real silicon (#220/#226/#232/#317/#343); all four WCET soundness cross-checks — the only thing that EXECUTES the fixtures and checks bound_cycles >= executed_instructions, i.e. the evidence behind the "sound WCET bound" claim; and the #494 rem_u identity differential behind the beat-clang headline. The gate itself is wired IN THE SAME COMMIT, as a step in claim-check — an ALREADY-REQUIRED context on main. A brand-new job would not be required, so it could sit red for weeks without blocking anything: the exact failure mode. It uses `set -o pipefail` and re-reads its own JSON summary to assert a non-zero wired count over a non-empty script set, so a run that measured nothing fails instead of greening on exit 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
claims.yaml SYNTH-ORACLE-WIRING-890 pins the totals the header comments cannot express: wired >= 145 (a FLOOR — the oracle surface must not be emptied by deleting harnesses instead of fixing them), manual <= 7 (a ceiling on the legitimate escape hatch), unwired <= 0 (a ceiling of ZERO — a new un-wired oracle is a red build, not a backlog entry). Proved by mutation: flipping one wired script to manual fails BOTH the floor and the ceiling legs. This generalizes SYNTH-GPIO-846-ORACLE-CI-WIRED, which hand-pins exactly one script's CI wiring — the instance-at-a-time shape #890 exists to replace. Also hardens the gate after a mutation found a real defect in it: `pipefail` without `-e` let the INERT-GATE mutation green the CI step, because the shell's status is its last command's. The step now sets `-euo pipefail` explicitly and the summary carries `wired_unreferenced` + `failures` so the verdict is reachable from the summary alone, never from exit 0. scripts/repro/ORACLE_WIRING.md documents the mechanism, argues header-over- manifest, itemizes the manual seven, and carries the four-mutation transcript (each run executes the step extracted VERBATIM from ci.yml, so there is no drift between what was proved and what CI runs). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… it goes RED in CI
Two mutations, both of which the gate must catch:
A. mem757_ptr_base_copy_differential.py — ci-status header REMOVED (undeclared).
B. wake_path_differential.py — declared `wired` while no workflow references
it (the INERT-GATE case: a green board sitting on top of a gate nothing
runs, which is the exact defect #890 exists to kill).
Expected: the `Claim Check` job fails at the "Oracle wiring gate" step. This
branch exists only to produce that CI red as evidence on PR #894; it is never
merged.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Contributor
Author
|
Evidence captured — the Run: https://github.com/pulseengine/synth/actions/runs/30545009045/job/90878830002 — linked from #894. Closing; never merged. |
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
A gate that has never been seen to fire is indistinguishable from one that cannot — which is the #890 thesis applied to #890 itself. So both required mutations were run through GitHub, not just locally: a throwaway branch carrying only the two mutations turned the real `Claim Check` job red at the Oracle wiring gate step (PR #895, closed unmerged, branch deleted). oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED FAIL ... mem757_ptr_base_copy_differential.py: UNDECLARED ... FAIL ... wake_path_differential.py: declares `wired` but NO workflow references it — the gate is INERT ... ##[error]Process completed with exit code 1. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
A gate that has never been seen to fire is indistinguishable from one that cannot — which is the #890 thesis applied to #890 itself. So both required mutations were run through GitHub, not just locally: a throwaway branch carrying only the two mutations turned the real `Claim Check` job red at the Oracle wiring gate step (PR #895, closed unmerged, branch deleted). oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED FAIL ... mem757_ptr_base_copy_differential.py: UNDECLARED ... FAIL ... wake_path_differential.py: declares `wired` but NO workflow references it — the gate is INERT ... ##[error]Process completed with exit code 1. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…nual / 0 undeclared (#894) * feat(#890): oracle-wiring gate — declared ci-status per repro script (step 1/5) Adds scripts/oracle_wiring_check.py: every scripts/repro/*.py|*.sh must carry exactly one `# ci-status:` declaration (wired | manual (<category>) — reason | unwired — reason), and a `wired` declaration is VERIFIED against .github/workflows/*.yml so a green board can never sit on top of an inert gate. Step 1 declares the 82 scripts a workflow already references. The remaining 70 are UNDECLARED and the gate is red on them by construction — classified next. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): classify all 152 repro scripts — 7 manual with real reasons (step 2/5) Read and classified the 70 scripts no workflow referenced. 63 of them run green against a freshly built synth right now (verified locally, one at a time) and are wired in the next step; 7 are genuinely manual and say WHY, in a closed category vocabulary (measurement / scratch / external-input) rather than free text. Three enabling fixes fall out of the audit: * base_cse / leaf_dead_frame / load_store_big_offset_382 / uxth_fold hardcoded ./target/{debug,release}/synth; they now honour $SYNTH (same literal default) so CI can point them at its own build. * sret_decide_differential printed "MISMATCH <-- BUG" and still exited 0 — wiring it as-is would have added a gate that CANNOT fail. The verdict is now the exit status (proved: mutating the -35 expectation to -34 gives rc=1). The gate is deliberately still red: 63 files declare `wired` while no workflow references them. That is the exact defect being fixed, and it is now MACHINE VISIBLE instead of requiring a 150-file read. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): wire 63 forgotten oracles + CI-wire the gate itself (step 3/5) Four new sweep jobs (selector / memory / rv32 / wcet) plus one step in the existing fact-spec job run the 63 differentials that were sitting in scripts/repro/ with nothing executing them. Every one was verified green locally against a freshly built synth before being wired — the compile line comes from each harness's own documented Run: block. Highlights of what was NOT being gated: the six mem757_* red-first reconstructions of gale's wrong-segment miscompile (#757); every RV32 oracle for a regression gale found on real silicon (#220/#226/#232/#317/#343); all four WCET soundness cross-checks — the only thing that EXECUTES the fixtures and checks bound_cycles >= executed_instructions, i.e. the evidence behind the "sound WCET bound" claim; and the #494 rem_u identity differential behind the beat-clang headline. The gate itself is wired IN THE SAME COMMIT, as a step in claim-check — an ALREADY-REQUIRED context on main. A brand-new job would not be required, so it could sit red for weeks without blocking anything: the exact failure mode. It uses `set -o pipefail` and re-reads its own JSON summary to assert a non-zero wired count over a non-empty script set, so a run that measured nothing fails instead of greening on exit 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): ratchet the manual/unwired budgets + policy doc (step 4/5) claims.yaml SYNTH-ORACLE-WIRING-890 pins the totals the header comments cannot express: wired >= 145 (a FLOOR — the oracle surface must not be emptied by deleting harnesses instead of fixing them), manual <= 7 (a ceiling on the legitimate escape hatch), unwired <= 0 (a ceiling of ZERO — a new un-wired oracle is a red build, not a backlog entry). Proved by mutation: flipping one wired script to manual fails BOTH the floor and the ceiling legs. This generalizes SYNTH-GPIO-846-ORACLE-CI-WIRED, which hand-pins exactly one script's CI wiring — the instance-at-a-time shape #890 exists to replace. Also hardens the gate after a mutation found a real defect in it: `pipefail` without `-e` let the INERT-GATE mutation green the CI step, because the shell's status is its last command's. The step now sets `-euo pipefail` explicitly and the summary carries `wired_unreferenced` + `failures` so the verdict is reachable from the summary alone, never from exit 0. scripts/repro/ORACLE_WIRING.md documents the mechanism, argues header-over- manifest, itemizes the manual seven, and carries the four-mutation transcript (each run executes the step extracted VERBATIM from ci.yml, so there is no drift between what was proved and what CI runs). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#890): a COMMENT mention must not count as wired (step 5/5) The gate derived "referenced by a workflow" from a raw grep of the .yml, so a mention in a COMMENT satisfied it — a gate satisfiable by prose, which is the exact failure shape #890 exists to reject. References now come from the PARSED workflow: each step's `run:` body plus its `with:`/`env:` values. A workflow that will not parse is a hard error, never a silent pass. No script changed status (verified before the change: zero of the 145 wired were wired by a comment alone), so this is pure future-proofing — but the diagnostic now says WHY: "It IS mentioned in ci.yml, but only in a COMMENT — prose does not run an oracle." Mutation matrix against the final gate, each run executing the step extracted VERBATIM from ci.yml (no drift between what was proved and what CI runs): baseline EXIT 0 M1 un-declare a script EXIT 1 UNDECLARED M2 declare wired, no reference at all EXIT 1 the gate is INERT M3 delete a wired oracle's CI step EXIT 1 the gate is INERT M4 gate's glob matches nothing EXIT 1 VACUOUS ['total<100'] M5 reference demoted to a comment EXIT 1 only in a COMMENT M6 manual reason replaced with "TODO" EXIT 1 needs a REAL reason restored EXIT 0 Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(#890): record the REAL CI-red evidence for the oracle-wiring gate A gate that has never been seen to fire is indistinguishable from one that cannot — which is the #890 thesis applied to #890 itself. So both required mutations were run through GitHub, not just locally: a throwaway branch carrying only the two mutations turned the real `Claim Check` job red at the Oracle wiring gate step (PR #895, closed unmerged, branch deleted). oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED FAIL ... mem757_ptr_base_copy_differential.py: UNDECLARED ... FAIL ... wake_path_differential.py: declares `wired` but NO workflow references it — the gate is INERT ... ##[error]Process completed with exit code 1. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(#890): the gate docstring says PARSED-workflow, matching the implementation Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#890): scope the dangling-reference check to the executable surface The reverse check (a workflow step running a repro script that no longer exists) scanned the RAW .yml, so a stale mention in a COMMENT would have been reported as a "dangling CI step" — a false red, and the wrong diagnosis: untidy prose is not a broken gate. It now scans the same executable surface the forward check uses. Proved still live by mutation: adding a step that runs a nonexistent script fails with the dangling-step message (EXIT 1). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * ci(#890): install wabt in the four repro sweeps; restore the lane CHANGELOG after rebase Two fixes on top of the rebase onto main (which now carries L4 #896 and the bare-pipefail hardening #900). 1. **wat2wasm was missing.** Both failing sweeps died with `FileNotFoundError: 'wat2wasm'`. That is the gate DOING ITS JOB: these 63 oracles had never run in CI, so their host dependencies had never been discovered — exactly the class that made the #881 VFP oracle fail on the runner while passing locally (#850). Several fixtures build their .wasm from .wat at test time. wabt installed in all four sweep jobs. 2. **Restored this lane's CHANGELOG entries.** My conflict resolution kept the `# ci-status:` header lines plus main's side, which is correct for the repro scripts and WRONG for an additive CHANGELOG — it silently dropped all four of the lane's bullets. Recovered verbatim from the pre-rebase branch and merged with the existing entry. Caught by counting bullets after the rebase rather than trusting that a clean `rebase --continue` meant a clean result. Rebase conflict in vcr_dec_001_join_alloc_execution_differential.py resolved keeping BOTH sides: L4's updated "increments 2+3" docstring and this lane's ci-status header. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Evidence branch for #894. Two mutations of the oracle-wiring gate; the
Claim Checkjob must fail at the Oracle wiring gate step.mem757_ptr_base_copy_differential.pyhas its# ci-status:header removed →UNDECLARED.wake_path_differential.pydeclareswiredwhile no workflow references it →the gate is INERT.Closed once the red run is captured. Never merged.