diff --git a/.github/workflows/emit-bitexact-gate.yml b/.github/workflows/emit-bitexact-gate.yml index c5201c414..8f620b29a 100644 --- a/.github/workflows/emit-bitexact-gate.yml +++ b/.github/workflows/emit-bitexact-gate.yml @@ -14,6 +14,12 @@ on: pull_request: branches: [master] paths: + # The four backends this gate proves equivalent all live in ONE file, + # bootstrap/src/compiler.rs -- gen_zig:3437, gen_verilog:6741, gen_c:10522, + # gen_rust:14382, in 31,077 lines. Without bootstrap/** here, a PR that + # rewrites the C emitter merges with the cross-target proof never running. + - "bootstrap/**" + - "cli/**" - "tools/gft_backprop_microcode.py" - "tools/verify_emit_bitexact.py" - "tools/verify_multitarget.py" @@ -52,7 +58,7 @@ jobs: run: python3 tools/verify_emit_bitexact.py - name: Prove GF-T primitives bit-exact across C + Rust + model - run: python3 tools/verify_multitarget.py + run: python3 tools/verify_multitarget.py --require - name: Prove the WHOLE trainer bit-exact in C (== model == Verilog) run: python3 tools/verify_trainer_c.py diff --git a/docs/NOW.md b/docs/NOW.md index b489966d2..552d43126 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,14 @@ +# NOW -- the bit-exactness gate could not see the compiler (2026-08-18) + +Last updated: 2026-08-18 + +## ci: let the cross-target gate see bootstrap/, and make its skip loud (Closes #2183) + +- **The gate that proves "one spec, four targets, bit-exact" was blind to the compiler.** `emit-bitexact-gate.yml` listed 11 paths and `bootstrap/**` was not one of them, while all four backends live in a single file: `bootstrap/src/compiler.rs`, `gen_zig:3437`, `gen_verilog:6741`, `gen_c:10522`, `gen_rust:14382`, 31,077 lines. A PR rewriting the C emitter merged with the proof never running +- **Green did not mean proved.** `tools/verify_multitarget.py` exits 0 when `t27c`, `cc` or `rustc` is missing. The job builds `t27c` itself and the runner ships the other two, so a skip there means the environment broke -- and exit 0 makes *proved* indistinguishable from *never ran* +- `--require` turns every skip into a failure and is now what CI passes; without it the script stays tolerant, so a contributor without `rustc` is not blocked. Verified both ways: tolerant exits 0, `--require` exits 1 with the reason +- The path filter carries a negative control in this commit's own verification: `bootstrap/src/compiler.rs`, `cli/tri/src/main.rs` and `tools/verify_multitarget.py` all match; `docs/README.md` does not. A filter that matches everything is as useless as one that matches nothing + # NOW -- the withdrawal gate was green because it was blind (2026-08-18) Last updated: 2026-08-18 diff --git a/tools/verify_multitarget.py b/tools/verify_multitarget.py index c37a80b9c..8ad64174f 100644 --- a/tools/verify_multitarget.py +++ b/tools/verify_multitarget.py @@ -7,9 +7,15 @@ C == model and Rust == model on the same random operands -- closing the "one spec -> any target, bit-exact" claim across {Verilog, C, Rust, model}. -Self-contained + CI-friendly: SKIPs (exit 0) if t27c / a C compiler / rustc is -missing; a real cross-target divergence exits 1. Run: - python3 tools/verify_multitarget.py +Self-contained. Locally it SKIPs (exit 0) when t27c, a C compiler or rustc is +absent, because a contributor without rustc should not be blocked. In CI that +tolerance is wrong: the workflow builds t27c itself and the runner ships cc and +rustc, so a skip there means the environment broke, and exit 0 makes "proved" +indistinguishable from "never ran". Pass --require to turn every skip into a +failure. A real cross-target divergence exits 1 in both modes. + + python3 tools/verify_multitarget.py # local, tolerant + python3 tools/verify_multitarget.py --require # CI, asserts it actually ran """ import os, sys, shutil, subprocess, tempfile, importlib.util, random @@ -18,7 +24,16 @@ N = 600 +REQUIRE = "--require" in sys.argv + + def skip(msg): + if REQUIRE: + print(f"FAIL verify_multitarget: {msg}") + print(" --require was given, so a missing prerequisite is a failure, not a skip.") + print(" The CI job builds t27c and the runner ships cc and rustc; if one is") + print(" absent the environment is broken and this check did not run.") + sys.exit(1) print(f"SKIP verify_multitarget: {msg}") sys.exit(0)