diff --git a/.github/workflows/emit-bitexact-gate.yml b/.github/workflows/emit-bitexact-gate.yml index 88fd39e404..3777c35965 100644 --- a/.github/workflows/emit-bitexact-gate.yml +++ b/.github/workflows/emit-bitexact-gate.yml @@ -18,6 +18,7 @@ on: - "tools/verify_emit_bitexact.py" - "tools/verify_multitarget.py" - "tools/verify_trainer_c.py" + - "tools/fuzz_trainer.py" - "specs/ternary/gft_smul.t27" - "specs/ternary/gft_sadd.t27" - ".github/workflows/emit-bitexact-gate.yml" @@ -52,3 +53,6 @@ jobs: - name: Prove the WHOLE trainer bit-exact in C (== model == Verilog) run: python3 tools/verify_trainer_c.py + + - name: Differential-fuzz the trainer (random topologies, edge inputs) + run: python3 tools/fuzz_trainer.py 40 diff --git a/docs/NOW.md b/docs/NOW.md index 36fa4c0e4f..fa0ca8fa01 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,14 @@ -# NOW — feat: WHOLE trainer bit-exact in C (== model == Verilog) (2026-08-07) +# NOW — feat: differential fuzzer for the trainer (random topologies + edge inputs) (2026-08-07) Last updated: 2026-08-07 +## feat: fuzz C-trainer == GF-T model over random topologies with edge values (Refs #1764) + +- The whole-trainer cross-target proof (verify_trainer_c) checked a few CHOSEN nets on a fixed 80-step sequence. `tools/fuzz_trainer.py` widens it to a RANDOMIZED space: random topology (1-3 inputs, 1-3 hidden layers of width 1-5, 1-3 outputs) x random training inputs with EDGE VALUES injected (offset-saturation-large 1e5, tiny 1e-9, exact 0/+-1/+-2/+-0.5), cross-checking the C trainer against the Python GF-T model per step +- **Local deep run: 250 random topologies x 16 steps = 4000 step-comparisons, edge values injected -- NO divergence.** CI runs a 40-topology fuzz (~24s). A single mismatch prints a reproducible counterexample (sizes, init, seq) +- Refactored verify_trainer_c into reusable `run_model` / `run_c` (one shared C emission, no drift between the gate and the fuzzer). Verified the fuzzer catches a real divergence (corrupted relu' modf) +- => cross-target bit-exactness of the whole trainer is now proven over a fuzzed space, not just chosen examples -- hardening the "one spec -> any target" claim against rare arithmetic edge cases (saturation, cancellation, underflow). Tool+CI only; Refs #1764 + ## feat: the entire training loop is bit-exact across C and Verilog, not just primitives (Refs #1764) - Last cycle proved the GF-T PRIMITIVES (smul/sadd) bit-exact across targets. This extends it to the WHOLE TRAINER. `tools/verify_trainer_c.py` emits the microsequencer as a C program -- the C GF-T primitives (t27c gen-c) + a microcode interpreter + the operand-modifier `modf` -- runs a full 80-step training run (forward+backprop+update) and checks every output per step against the independent Python GF-T model diff --git a/tools/fuzz_trainer.py b/tools/fuzz_trainer.py new file mode 100644 index 0000000000..bf5cc959b2 --- /dev/null +++ b/tools/fuzz_trainer.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Differential fuzzer: C trainer vs the Python GF-T model over RANDOM topologies +and RANDOM training inputs, with edge values injected (offset-saturation-large, +tiny, exact 0/+-1/+-2/+-0.5). Where the fixed-sequence gate (verify_trainer_c) +proves bit-exactness on a few chosen nets, this widens it to a randomized space -- +a single divergence is a reproducible counterexample of a spec-vs-model edge bug. + +Reuses run_model / run_c from verify_trainer_c (one shared C emission, no drift). +CI-friendly: SKIPs (exit 0) if t27c / cc is missing; any mismatch exits 1. + python3 tools/fuzz_trainer.py [rounds] # default 40; try 500 locally +""" +import os, sys, shutil, tempfile, random, importlib.util + +ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +vt_spec = importlib.util.spec_from_file_location( + "vt", os.path.join(ROOT, "tools/verify_trainer_c.py")) +vt = importlib.util.module_from_spec(vt_spec); vt_spec.loader.exec_module(vt) + +ROUNDS = int(sys.argv[1]) if len(sys.argv) > 1 else 40 +STEPS = 16 +EDGES = [0.0, 1.0, -1.0, 2.0, -2.0, 0.5, -0.5, 0.25, -0.25] + + +def rnd_val(r): + p = r.random() + if p < 0.15: return r.choice(EDGES) # exact GF-T-representable + if p < 0.25: return r.uniform(-1e5, 1e5) # large -> offset saturation + if p < 0.30: return r.choice([1e-6, -1e-6, 1e-9]) # tiny -> underflow edge + return round(r.uniform(-4, 4), 3) + + +def rnd_sizes(r): + n_in = r.randint(1, 3) + depth = r.randint(1, 3) # hidden layers + sizes = [n_in] + [r.randint(1, 5) for _ in range(depth)] + [r.randint(1, 3)] + return sizes + + +def main(): + t27c = vt.find_t27c() + if not t27c: + vt.skip("t27c binary not found") + if not shutil.which("cc"): + vt.skip("no C compiler (cc) on PATH") + g = vt.load_gen() + r = random.Random(20260807) + total_steps = 0 + with tempfile.TemporaryDirectory() as wd: + for rd in range(ROUNDS): + sizes = rnd_sizes(r) + reg, steps = g.gen_deep(sizes) + n_in, n_out = sizes[0], sizes[-1] + # random init over every weight (W..) / bias (b..) register; scratch and + # activation regs stay 0 (as the RTL zero-inits them) + init = [(idx, g.enc(rnd_val(r))) for name, idx in reg.items() + if name.startswith("W") or name.startswith("b")] + # random training sequence with edge-injected inputs/targets + seq = [([rnd_val(r) for _ in range(n_in)], [rnd_val(r) for _ in range(n_out)]) + for _ in range(STEPS)] + py = vt.run_model(g, reg, steps, init, n_in, n_out, seq) + cy = vt.run_c(g, reg, steps, init, n_in, n_out, seq, t27c, wd) + if cy is None: + print(f"FAIL round {rd} sizes={sizes}: C trainer failed to build/run"); sys.exit(1) + if len(cy) != len(py): + print(f"FAIL round {rd} sizes={sizes}: C {len(cy)} vs model {len(py)} steps"); sys.exit(1) + for i, (p, c) in enumerate(zip(py, cy)): + if p != c: + print(f"COUNTEREXAMPLE round {rd} sizes={sizes} step {i}: model={p} C={c}") + print(f" init={init}") + print(f" seq={seq}") + sys.exit(1) + total_steps += len(py) + print(f"FUZZ OK: C trainer == model over {ROUNDS} random topologies x {STEPS} steps " + f"({total_steps} step-comparisons), edge values injected -- no divergence") + sys.exit(0) + + +if __name__ == "__main__": + main() diff --git a/tools/verify_trainer_c.py b/tools/verify_trainer_c.py index 03035a894f..7088fc8b9e 100644 --- a/tools/verify_trainer_c.py +++ b/tools/verify_trainer_c.py @@ -71,40 +71,41 @@ def build_seq(n_in, n_out): return seq -def check(g, arch, t27c, wd): - v, reg, steps, n_in, n_out = emit_and_gen(g, arch) - init = [(int(i), int(val)) for i, val in re.findall(r"rf\[(\d+)\]<=32'd(\d+);", v)] +def run_model(g, reg, steps, init_pairs, n_in, n_out, seq): + """Run the training sequence through the Python GF-T model. init_pairs = list of + (reg_index, u32); seq = list of (xs_floats, ts_floats). Returns per-step output + tuples (yout u32 for each of n_out).""" rf = [0] * len(reg) - for i, val in init: + for i, val in init_pairs: rf[i] = val - seq = build_seq(n_in, n_out) - # python model reference - py = [] + out = [] for xs, ts in seq: for k in range(n_in): rf[reg[f"x{k}"]] = g.enc(xs[k]) for o in range(n_out): rf[reg[f"t{o}"]] = g.enc(ts[o]) g.run(steps, rf) - py.append(tuple(rf[reg[f"y{o}"]] & 0xFFFFFFFF for o in range(n_out))) - # emit the C trainer + out.append(tuple(rf[reg[f"y{o}"]] & 0xFFFFFFFF for o in range(n_out))) + return out + + +def run_c(g, reg, steps, init_pairs, n_in, n_out, seq, t27c, wd): + """Emit the trainer as a C program (t27c gen-c primitives + microcode interpreter + + modf), compile, run the same sequence. Returns per-step output tuples, or None + on a build failure. gftmod.h is (re)written into wd.""" hdr = subprocess.run([t27c, "gen-c", "specs/ternary/gft_smul.t27"], capture_output=True, text=True, cwd=ROOT).stdout if "GFTSMUL_H" not in hdr: - skip("t27c gen-c failed") + return None open(os.path.join(wd, "gftmod.h"), "w").write(hdr) op = ",".join("2" if o == "MOV" else ("1" if o == "ADD" else "0") for o, *_ in steps) ai = ",".join(str(s[1]) for s in steps); am = ",".join(str(s[2]) for s in steps) bi = ",".join(str(s[3]) for s in steps); bm = ",".join(str(s[4]) for s in steps) di = ",".join(str(s[5]) for s in steps) - initc = "".join(f"rf[{i}]={val}u;" for i, val in init) + initc = "".join(f"rf[{i}]={val}u;" for i, val in init_pairs) xidx = [reg[f"x{k}"] for k in range(n_in)]; tidx = [reg[f"t{o}"] for o in range(n_out)] yidx = [reg[f"y{o}"] for o in range(n_out)] - rows = [] - for xs, ts in seq: - vals = [g.enc(x) for x in xs] + [g.enc(t) for t in ts] - rows.append(",".join(str(x) for x in vals)) - samples = "{" + "},{".join(rows) + "}" - ncol = n_in + n_out - # build the C main + rows = ["{" + ",".join(str(x) for x in ([g.enc(x) for x in xs] + [g.enc(t) for t in ts])) + "}" + for xs, ts in seq] + samples = ",".join(rows) main = f"""#define assert_eq(a,b) ((void)0) #include "gftmod.h" #include @@ -118,7 +119,7 @@ def check(g, arch, t27c, wd): rf[DI[pc]] = OP[pc]==2 ? a : (OP[pc] ? sadd(a,b) : smul(a,b)); }} }} -static const uint32_t SAMP[{len(seq)}][{ncol}]={{{samples}}}; +static const uint32_t SAMP[{len(seq)}][{n_in + n_out}]={{{samples}}}; static const int XIDX[]={{{",".join(map(str,xidx))}}}, TIDX[]={{{",".join(map(str,tidx))}}}, YIDX[]={{{",".join(map(str,yidx))}}}; int main(void){{ int s,k; @@ -136,9 +137,19 @@ def check(g, arch, t27c, wd): b = os.path.join(wd, "tbin") r = subprocess.run(["cc", "-O2", "-o", b, cf], cwd=wd, capture_output=True, text=True) if r.returncode != 0: - print(f"FAIL {arch}: C trainer failed to compile\n{r.stderr[-800:]}"); return False + return None out = subprocess.run([b], capture_output=True, text=True).stdout - cy = [tuple(map(int, ln.split())) for ln in out.strip().splitlines()] + return [tuple(map(int, ln.split())) for ln in out.strip().splitlines()] + + +def check(g, arch, t27c, wd): + v, reg, steps, n_in, n_out = emit_and_gen(g, arch) + init = [(int(i), int(val)) for i, val in re.findall(r"rf\[(\d+)\]<=32'd(\d+);", v)] + seq = build_seq(n_in, n_out) + py = run_model(g, reg, steps, init, n_in, n_out, seq) + cy = run_c(g, reg, steps, init, n_in, n_out, seq, t27c, wd) + if cy is None: + print(f"FAIL {arch}: C trainer failed to build/run"); return False if len(cy) != len(py): print(f"FAIL {arch}: C produced {len(cy)} of {len(py)} steps"); return False mism = [(i, p, c) for i, (p, c) in enumerate(zip(py, cy)) if p != c]