Add the third opinion: an independent model, exhaustive, on 33.7M inputs

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

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

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