From bd72f9a3d439afe3cda0f1226817fbd179b090fc Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 21:12:41 +0700 Subject: [PATCH] verify: add the third opinion, exhaustive over 33.7M inputs #2199 shipped exhaustive cross-target checking and printed a limitation on every run: C against Rust only, so a fault shared by both backends -- a spec bug or shared front-end lowering -- was invisible. 'The backends agree' and 'the backends both match the specification' are different claims, and the first is easy to mistake for the second. tools/ternary_model.py is an independent transcription of the primitives, read from specs/ternary/ternary_ripple_adder.t27 and re-expressed in Python. It was NOT derived from the generated C or Rust; had it been, it would agree by construction and prove nothing. Transcribed faithfully, including what looks wrong: pack2 does not mask its arguments to two bits, so a value above 3 spills into the neighbouring trit lane. A model that 'fixed' that would report a divergence which is really the model disagreeing with the specification it exists to encode. full_adder(u8,u8,u8) 16,777,216 inputs model == C == Rust maj3(u8,u8,u8) 16,777,216 inputs model == C == Rust tmul(u8,u8) 65,536 inputs model == C == Rust pack2(u8,u8) 65,536 inputs model == C == Rust negate(u8) 256 inputs model == C == Rust 33.7 million inputs, three independent implementations, about eight seconds. Two negative controls, because the model arm needed its own. Perturbing C proves the C/Rust comparison has resolution; it says nothing about whether a model disagreeing with BOTH backends would be noticed, which is the entire reason the model exists. one-input perturbation of C 91a68892 -> b7b51485 one-input perturbation of MODEL 91a68892 -> cea51633, backends 91a68892 Measured rather than guessed: pure Python did not finish full_adder's 16.7M inputs in 600s -- nine dot27 calls per input, 27 lanes each, ~4e9 operations. Memoising dot27, a pure function whose semantics are untouched by it, took the rate from 179k calls/s to 2.2M/s. Targets added to TARGETS without a model entry stay two-way and are labelled [2-way: no model entry], so the weaker case cannot pass itself off as the stronger. Closes #2200 Refs #2198 Co-Authored-By: Claude Opus 5 --- docs/NOW.md | 13 ++++++ tools/ternary_model.py | 93 ++++++++++++++++++++++++++++++++++++++ tools/verify_exhaustive.py | 91 ++++++++++++++++++++++++++++++------- 3 files changed, 180 insertions(+), 17 deletions(-) create mode 100644 tools/ternary_model.py diff --git a/docs/NOW.md b/docs/NOW.md index 591ad9da1..5e777e1cc 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,16 @@ +# NOW -- the third opinion, exhaustive (2026-08-18) + +Last updated: 2026-08-18 + +## verify: an independent model closes the two-way gap on 33.7M inputs (Closes #2200) + +- **#2199 printed its own limitation on every run:** C against Rust only, so a fault shared by both backends -- a spec bug, or shared lowering -- was invisible. "The backends agree" and "both match the specification" are different claims +- **`tools/ternary_model.py` is transcribed from the SPEC text**, not from generated code. Had it been derived from the backends it would agree by construction and prove nothing. Transcribed faithfully including what looks wrong: `pack2` does not mask its arguments to two bits, so values above 3 spill into the next trit lane -- a model that "fixed" that would report the model disagreeing with the spec it encodes +- **model == C == Rust, exhaustively:** `full_adder` and `maj3` at 16,777,216 inputs each, `tmul` and `pack2` at 65,536, `negate` at 256. **33.7 million inputs, three implementations, ~8 seconds** +- **Two negative controls, because the model arm needed its own.** Perturbing C proves the C/Rust comparison has resolution and says nothing about whether a model disagreeing with *both* backends would be seen -- which is the reason the model exists +- **Measured, not guessed:** pure Python did not finish `full_adder` in 600 s (nine `dot27` calls per input, 27 lanes each, ~4e9 operations). Memoising `dot27` -- pure, so semantics untouched -- took it from 179k calls/s to 2.2M/s +- Targets without a model entry stay two-way and are **labelled** as such, so the weaker case cannot pass for the stronger + # NOW -- exhaust the input space wherever it is small (2026-08-18) Last updated: 2026-08-18 diff --git a/tools/ternary_model.py b/tools/ternary_model.py new file mode 100644 index 000000000..8aa55234a --- /dev/null +++ b/tools/ternary_model.py @@ -0,0 +1,93 @@ +"""An independent Python model of the ternary primitives, transcribed from the SPEC. + +Independence is the whole point, so it matters how this was written: each function +below was read from `specs/ternary/ternary_ripple_adder.t27` and re-expressed here. +None of it was derived from the generated C or Rust. If it had been, it would agree +with them by construction and prove nothing. + +Transcribed faithfully, including the parts that look wrong. `pack2` does not mask its +arguments to two bits, so a value above 3 spills into the neighbouring trit position. +That is what the spec says; a model that "fixed" it would report a divergence that is +really the model disagreeing with the specification it is supposed to encode. + +Widths are emulated where the spec names them: `dot27` accumulates in i16 and `tmul` +returns i8. With 27 terms of magnitude 1 no wrap occurs, but the wrap is applied anyway +rather than assumed away. +""" + + +def _i16(v): + return ((v + (1 << 15)) & 0xFFFF) - (1 << 15) + + +def _i8(v): + return ((v + (1 << 7)) & 0xFF) - (1 << 7) + + +def tmul(ta, tb): + """if ta == 1 -> 0; if tb == 1 -> 0; if ta == tb -> 1; else -1.""" + if ta == 1: + return 0 + if tb == 1: + return 0 + if ta == tb: + return 1 + return _i8(-1) + + +def dot27(a, b): + """Sum of tmul over 27 trit lanes, two bits each, accumulated in i16.""" + acc = 0 + for i in range(27): + ta = (a >> (i << 1)) & 3 + tb = (b >> (i << 1)) & 3 + acc = _i16(acc + tmul(ta, tb)) + return acc + + +def sign0(v): + """v > 0 -> 2; v < 0 -> 0; else 1.""" + return 2 if v > 0 else (0 if v < 0 else 1) + + +def negate(t): + """2 -> 0; 0 -> 2; anything else -> 1.""" + return 0 if t == 2 else (2 if t == 0 else 1) + + +_Z = 6004799503160661 + + +def pack2(t0, t1): + """Note: t0 and t1 are NOT masked to two bits. Spec behaviour, reproduced.""" + cleared = _Z & 18446744073709551600 + return (cleared | (t0 & 0xFFFFFFFFFFFFFFFF) | ((t1 & 0xFFFFFFFFFFFFFFFF) << 2)) \ + & 0xFFFFFFFFFFFFFFFF + + +def pack3(t0, t1, t2): + cleared = _Z & 18446744073709551552 + return (cleared | t0 | (t1 << 2) | (t2 << 4)) & 0xFFFFFFFFFFFFFFFF + + +def bneuron(x, w, bias): + return sign0(_i16(dot27(x, w) + bias)) + + +def xor2(a, b): + x = pack2(a, b) + w = pack2(2, 2) + h1 = bneuron(x, w, -1) + h2 = bneuron(x, w, 1) + return bneuron(pack2(h2, negate(h1)), w, -1) + + +def maj3(a, b, c): + return sign0(dot27(pack3(a, b, c), 12009599006321322)) + + +def full_adder(a, b, cin): + """Sum trit in bits[1:0], carry trit in bits[3:2].""" + s = xor2(xor2(a, b), cin) + carry = maj3(a, b, cin) + return ((carry << 2) | s) & 0xFF diff --git a/tools/verify_exhaustive.py b/tools/verify_exhaustive.py index c0c311b81..5b0f04f18 100755 --- a/tools/verify_exhaustive.py +++ b/tools/verify_exhaustive.py @@ -9,13 +9,17 @@ can enumerate does not need a prover or a sample. A ternary full adder takes three trits-in-a-byte and has 16,777,216 possible inputs. That is seconds of CPU. -What this checks and what it does NOT. It compares the C backend against the Rust -backend on every input. If both are wrong in the same way -- a bug in the spec, or in -shared front-end lowering -- this will not see it. That is a weaker statement than -`verify_igla_race.py` makes for `ternary_mul`, where an independent Python model is the -third opinion. The distinction is printed with every result, because "C == Rust on all -inputs" and "C == Rust == independent model on all inputs" are different claims and the -first is easy to mistake for the second. +What this checks. C, Rust and an independent model, on every input. The model lives in +`tools/ternary_model.py` and was transcribed from the SPEC text, not from the generated +code -- that is what makes it a third opinion rather than a restatement. A fault shared +by both backends, whether from the spec or from shared front-end lowering, shows up as +the model disagreeing with both. + +An earlier version of this file compared only C against Rust and said so on every run, +because "the backends agree" and "the backends both match the specification" are +different claims and the first is easy to mistake for the second. The model closes that +gap for the primitives listed below; anything added to TARGETS without a model entry is +reported as two-way and labelled as such. Coverage before this file: four specs (`ternary_mac`, `systolic_ternary`, `gft_smul`, `gft_sadd`). `ternary_ripple_adder.t27` generates 167 lines of C and had no cross-target @@ -35,6 +39,14 @@ import tempfile import time +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import functools # noqa: E402 +import ternary_model as MODEL # noqa: E402 + +# dot27 is pure, so memoising it changes nothing about what the model computes and +# takes full_adder over its 16,777,216 inputs from minutes to under a minute. +MODEL.dot27 = functools.lru_cache(maxsize=None)(MODEL.dot27) + ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) # (spec, function, [(c_type, rust_type, lo, hi)]) -- the full domain of each argument. @@ -130,6 +142,27 @@ def build_and_run(src, path, cmd, wd, what): return r.stdout.strip() +def model_digest(fn, args): + """The same FNV-1a fold, over the same domain, computed by the independent model.""" + f = getattr(MODEL, fn, None) + if f is None: + return None + h = 2166136261 + + def rec(i, acc): + nonlocal h + if i == len(args): + v = f(*acc) & 0xFFFFFFFF + h = ((h ^ v) * 16777619) & 0xFFFFFFFF + return + _, _, lo, hi = args[i] + for x in range(lo, hi + 1): + rec(i + 1, acc + [x]) + + rec(0, []) + return f"{h:08x}" + + def check(spec, fn, args, wd): space = 1 for _, _, lo, hi in args: @@ -151,7 +184,17 @@ def check(spec, fn, args, wd): print(f"FAIL {fn}: C digest {cd} != Rust digest {rd} -- the backends disagree on at " f"least one of the {space:,} possible inputs") return False - print(f"OK {fn:<12} C == Rust on ALL {space:>12,} inputs digest {cd} {dt:.1f}s") + md = model_digest(fn, args) + if md is None: + print(f"OK {fn:<12} C == Rust on ALL {space:>12,} inputs digest {cd} {dt:.1f}s" + f" [2-way: no model entry in ternary_model.py]") + return True + if md != cd: + print(f"FAIL {fn}: backends agree on {cd} but the independent model says {md} -- both " + f"backends differ from the specification on at least one of the {space:,} inputs, " + f"which two-way agreement could never have shown") + return False + print(f"OK {fn:<12} model == C == Rust on ALL {space:>12,} inputs digest {cd} {dt:.1f}s") return True @@ -171,10 +214,25 @@ def self_check(wd): bad_c = build_and_run(bad_src, os.path.join(wd, "sb.c"), ["cc", "-O2", "-o", os.path.join(wd, "sb"), os.path.join(wd, "sb.c")], wd, "self-check C perturbed") - ok = good_c is not None and bad_c is not None and good_c != bad_c - print(f" self-check: one-input perturbation changes the digest = {ok}" - + (f" ({good_c} -> {bad_c})" if ok else "")) - return 0 if ok else 1 + ok_c = good_c is not None and bad_c is not None and good_c != bad_c + print(f" self-check: one-input perturbation of C changes the digest = {ok_c}" + + (f" ({good_c} -> {bad_c})" if ok_c else "")) + + # The model arm needs its own control. Perturbing C proves the C/Rust comparison + # has resolution; it says nothing about whether a model that disagreed with BOTH + # backends would be noticed -- which is the whole reason the model was added. + real = MODEL.tmul + try: + MODEL.tmul = lambda a, b, _r=real: (_r(a, b) + 1) if (a == 7 and b == 3) else _r(a, b) + perturbed = model_digest("tmul", args) + finally: + MODEL.tmul = real + clean = model_digest("tmul", args) + ok_m = perturbed is not None and clean is not None and perturbed != clean and clean == good_c + print(f" self-check: one-input perturbation of the MODEL is visible = {ok_m}" + + (f" ({clean} -> {perturbed}, backends {good_c})" if ok_m else "")) + + return 0 if (ok_c and ok_m) else 1 def main(): @@ -183,10 +241,9 @@ def main(): if "--self-check" in sys.argv: return self_check(wd) print("Cross-target agreement over the ENTIRE input space.\n") - print(" This compares C against Rust. It does NOT include an independent model, so a") - print(" fault shared by both backends -- a spec bug, or shared front-end lowering --") - print(" is invisible here. verify_igla_race.py carries the stronger form for") - print(" ternary_mul, where a Python model is the third opinion.\n") + print(" Three opinions: the C backend, the Rust backend, and tools/ternary_model.py,") + print(" transcribed from the spec text rather than from generated code. A fault shared") + print(" by both backends shows up as the model disagreeing with both.\n") results = [] for spec, fn, args in TARGETS: if only and fn not in only: @@ -200,7 +257,7 @@ def main(): if bad: print(f"FAIL: {len(bad)} of {len(results)} targets did not agree or did not run") return 1 - print(f"ALL {len(results)} PRIMITIVES: C == Rust EXHAUSTIVELY (no sampling, no model)") + print(f"ALL {len(results)} PRIMITIVES: model == C == Rust EXHAUSTIVELY (no sampling)") return 0