Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion .github/workflows/emit-bitexact-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
11 changes: 11 additions & 0 deletions docs/NOW.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
21 changes: 18 additions & 3 deletions tools/verify_multitarget.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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)

Expand Down
Loading