From 936883afdc21770641e9631929d8872f7f729b11 Mon Sep 17 00:00:00 2001
From: Vasilev Dmitrii <raoffonom@icloud.com>
Date: Fri, 7 Aug 2026 21:21:28 +0700
Subject: [PATCH] feat: prove GF-T primitives bit-exact across C + Rust +
 Verilog + model

Strengthens the one-spec-any-target thesis from Verilog-only to four targets.
verify_multitarget.py emits smul/sadd (the exact functions the trainer's shared
datapath uses) via t27c gen-c and gen-rust, compiles both (cc/rustc), and
cross-checks against the independent Python GF-T model over 600 random operand
pairs each: C == model and Rust == model bit-exact for both. Combined with
Verilog == model (verify_emit_bitexact), all of {Verilog, C, Rust, model} agree
bit-for-bit. Wired into emit-bitexact-gate (SKIPs if cc/rustc/t27c absent).

gen-c emits the spec's test blocks as assert_eq() calls undeclared in C; stubbed
as a no-op macro before include since we call the functions directly.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/emit-bitexact-gate.yml |   4 +
 docs/NOW.md                              |  10 +-
 tools/verify_multitarget.py              | 121 +++++++++++++++++++++++
 3 files changed, 134 insertions(+), 1 deletion(-)
 create mode 100644 tools/verify_multitarget.py

diff --git a/.github/workflows/emit-bitexact-gate.yml b/.github/workflows/emit-bitexact-gate.yml
index 75583131b8..e276b9304f 100644
--- a/.github/workflows/emit-bitexact-gate.yml
+++ b/.github/workflows/emit-bitexact-gate.yml
@@ -16,6 +16,7 @@ on:
     paths:
       - "tools/gft_backprop_microcode.py"
       - "tools/verify_emit_bitexact.py"
+      - "tools/verify_multitarget.py"
       - "specs/ternary/gft_smul.t27"
       - "specs/ternary/gft_sadd.t27"
       - ".github/workflows/emit-bitexact-gate.yml"
@@ -44,3 +45,6 @@ jobs:
 
       - name: Prove generated RTL == GF-T model (bit-exact) + synthesizes
         run: python3 tools/verify_emit_bitexact.py
+
+      - name: Prove GF-T primitives bit-exact across C + Rust + model
+        run: python3 tools/verify_multitarget.py
diff --git a/docs/NOW.md b/docs/NOW.md
index 6b0363a2a1..596d8345cf 100644
--- a/docs/NOW.md
+++ b/docs/NOW.md
@@ -1,7 +1,15 @@
-# NOW — docs: whitepaper updated for the programmable/deep/CI-enforced trainer (2026-08-07)
+# NOW — feat: cross-target bit-exactness (C + Rust + Verilog + model) (2026-08-07)
 
 Last updated: 2026-08-07
 
+## feat: GF-T primitives proven bit-exact across ALL t27 backends (Refs #1764)
+
+- Strengthens the core "one spec -> any target, bit-exact" thesis from Verilog-only to FOUR targets. `tools/verify_multitarget.py` emits the GF-T primitives `smul`/`sadd` (the exact functions the trainer's shared datapath uses) via t27c gen-c and gen-rust, compiles both (cc / rustc), and cross-checks against the independent Python GF-T model over 600 random operand pairs each
+- Result: **C == model and Rust == model BIT-EXACT** for smul and sadd; combined with Verilog == model (already proven by verify_emit_bitexact), all of {Verilog, C, Rust, model} agree bit-for-bit. Wired into the emit-bitexact-gate workflow (SKIPs cleanly if cc/rustc/t27c absent)
+- (Found + handled: gen-c emits the spec's `test` blocks as `assert_eq(...)` calls undeclared in C -> stub as a no-op macro before include, since we call the functions directly)
+- This cycle was "все три" (A/G/H): **A** (flash to silicon) remains blocked on the physical JTAG re-connect; **G** (nextpnr-xilinx P&R for real Fmax) needs the xilinx nextpnr variant + chipdb (not installed; too heavy for CI) -- deferred, not faked; **H** delivered here
+- Tool+CI only; Refs #1764
+
 ## docs: GFT_WHITEPAPER reflects cycles 71-74 (no structural limits, CI-enforced) (Refs #1764)
 
 - The whitepaper undersold the product: it described a 2-layer-only trainer with multi-output/depth pending. Updated section 4 to the current reality: (b) one-shared-multiplier microsequencer; (c) FULLY PROGRAMMABLE trainer -- any feed-forward topology, free input/output/hidden width AND arbitrary depth (2/3/4-layer), trainable biases, learning real tasks (noisy nonlinear ~97% 2-layer / 98% 3-layer, multi-class one-hot 93%); (d) correctness as a CI-ENFORCED invariant -- bit-exact spec->RTL over a full training run + synthesizability + one-shared-multiplier datapath invariant, on every PR
diff --git a/tools/verify_multitarget.py b/tools/verify_multitarget.py
new file mode 100644
index 0000000000..c37a80b9cc
--- /dev/null
+++ b/tools/verify_multitarget.py
@@ -0,0 +1,121 @@
+#!/usr/bin/env python3
+"""Cross-target bit-exactness for the GF-T primitives the trainer is built on.
+
+`smul` and `sadd` (the exact functions the microsequencer's shared datapath uses)
+must compute IDENTICALLY across t27's backends. verify_emit_bitexact already proves
+Verilog == the independent Python GF-T model over a full training run; this proves
+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
+"""
+import os, sys, shutil, subprocess, tempfile, importlib.util, random
+
+ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
+SPECS = {"gft_smul": "smul", "gft_sadd": "sadd"}   # spec file -> top function
+N = 600
+
+
+def skip(msg):
+    print(f"SKIP verify_multitarget: {msg}")
+    sys.exit(0)
+
+
+def find_t27c():
+    for p in ("target/debug/t27c", "target/release/t27c"):
+        cand = os.path.join(ROOT, p)
+        if os.path.exists(cand):
+            return cand
+    return shutil.which("t27c")
+
+
+def load_gen():
+    spec = importlib.util.spec_from_file_location(
+        "gbm", os.path.join(ROOT, "tools/gft_backprop_microcode.py"))
+    m = importlib.util.module_from_spec(spec); spec.loader.exec_module(m)
+    return m
+
+
+def gen_pairs(g):
+    random.seed(202)
+    vals = [g.enc(round(random.uniform(-4, 4), 3)) for _ in range(48)]
+    vals += [g.enc(0.0), g.enc(1.0), g.enc(-1.0), g.enc(2.0), g.enc(0.5), g.enc(-2.0), g.enc(0.25)]
+    return [(random.choice(vals), random.choice(vals)) for _ in range(N)]
+
+
+def py_ref(g, fn, pairs):
+    f = getattr(g, fn)
+    return [f(a, b) & 0xFFFFFFFF for a, b in pairs]
+
+
+def run_c(t27c, spec, fn, pairs, wd):
+    hdr = subprocess.run([t27c, "gen-c", f"specs/ternary/{spec}.t27"],
+                         capture_output=True, text=True, cwd=ROOT).stdout
+    if "GFTSMUL_H" not in hdr and "GFTSADD_H" not in hdr:
+        return None
+    open(os.path.join(wd, "mod.h"), "w").write(hdr)
+    a = ",".join(str(x) for x, _ in pairs); b = ",".join(str(y) for _, y in pairs)
+    # the spec's `test` blocks emit `assert_eq(...)` calls (undeclared in C); we
+    # call the functions directly, so stub it out before including the module
+    main = (f'#define assert_eq(x,y) ((void)0)\n#include "mod.h"\n#include <stdio.h>\nint main(){{'
+            f'uint32_t A[]={{{a}}},B[]={{{b}}};int n={len(pairs)};'
+            f'for(int i=0;i<n;i++)printf("%u\\n",(unsigned){fn}(A[i],B[i]));return 0;}}')
+    open(os.path.join(wd, "main.c"), "w").write(main)
+    if subprocess.run(["cc", "-O2", "-o", os.path.join(wd, "cbin"), os.path.join(wd, "main.c")],
+                      cwd=wd, capture_output=True, text=True).returncode != 0:
+        return None
+    out = subprocess.run([os.path.join(wd, "cbin")], capture_output=True, text=True).stdout
+    return [int(x) for x in out.split()]
+
+
+def run_rust(t27c, spec, fn, pairs, wd):
+    src = subprocess.run([t27c, "gen-rust", f"specs/ternary/{spec}.t27"],
+                         capture_output=True, text=True, cwd=ROOT).stdout
+    if "fn " not in src:
+        return None
+    a = ",".join(str(x) for x, _ in pairs); b = ",".join(str(y) for _, y in pairs)
+    src += (f'\nfn main(){{let a:[u32;{len(pairs)}]=[{a}];let b:[u32;{len(pairs)}]=[{b}];'
+            f'for i in 0..a.len(){{println!("{{}}",{fn}(a[i],b[i]) as u32);}}}}\n')
+    rs = os.path.join(wd, "m.rs"); open(rs, "w").write(src)
+    if subprocess.run(["rustc", "-A", "warnings", "-O", "-o", os.path.join(wd, "rbin"), rs],
+                      cwd=wd, capture_output=True, text=True).returncode != 0:
+        return None
+    out = subprocess.run([os.path.join(wd, "rbin")], capture_output=True, text=True).stdout
+    return [int(x) for x in out.split()]
+
+
+def main():
+    t27c = find_t27c()
+    if not t27c:
+        skip("t27c binary not found")
+    if not shutil.which("cc"):
+        skip("no C compiler (cc) on PATH")
+    if not shutil.which("rustc"):
+        skip("rustc not on PATH")
+    g = load_gen()
+    ok = True
+    with tempfile.TemporaryDirectory() as wd:
+        for spec, fn in SPECS.items():
+            pairs = gen_pairs(g)
+            ref = py_ref(g, fn, pairs)
+            for tgt, runner in (("C", run_c), ("Rust", run_rust)):
+                got = runner(t27c, spec, fn, pairs, wd)
+                if got is None:
+                    print(f"FAIL {spec}.{fn}: {tgt} backend failed to build/run"); ok = False; continue
+                if len(got) != len(ref):
+                    print(f"FAIL {spec}.{fn}: {tgt} produced {len(got)} of {len(ref)} outputs"); ok = False; continue
+                mism = [(i, r, x) for i, (r, x) in enumerate(zip(ref, got)) if r != x]
+                if mism:
+                    i, r, x = mism[0]
+                    print(f"FAIL {spec}.{fn}: {tgt} != model in {len(mism)}/{len(ref)}; "
+                          f"first pair {pairs[i]} model={r} {tgt}={x}"); ok = False
+                else:
+                    print(f"OK {spec}.{fn}: {tgt} == Python model BIT-EXACT over {len(ref)} operand pairs")
+    print("ALL TARGETS BIT-EXACT (Verilog[via emit gate] + C + Rust + model agree)" if ok else "CROSS-TARGET MISMATCH")
+    sys.exit(0 if ok else 1)
+
+
+if __name__ == "__main__":
+    main()