verified: bound GEMM memory, certify the multiply LUT, test the shipped paths

LUTBackend.gemm and NeuralBackend.gemm materialized the full (m,n,k) product block before reducing, making peak memory cubic in layer width -- 2.4 GB for one layer's forward at the SpikeWhale panel's maximum settings. Both now block the m axis; the contraction axis k is untouched, so results are bit-identical (512x768x768: 2426.9 MB -> 77.2 MB; neural 64x96x96: 519.2 MB -> 57.5 MB).

The two backends need different block accounting: a LUT product costs 8 bytes, a neural product ~880 (four nibble pairs through a 128-wide net).

build_luts() returned its tables unchecked while the docs described a self-certify gate. The table is the complete finite domain, so certifying it IS the exhaustive verification: LUTBackend now checks all 65536 entries against signed integer multiply at construction and raises on mismatch (0.5 ms).

Exhaustive verification covered the scalar entry points; production runs the batched paths and the LUTs built from them, which are different code. test_verified_units.py checks every shipped path against golden integer arithmetic over its full domain (24 checks, all passing).

gemm_int8 enforces the int32 accumulator bound (K <= 131071) rather than asserting it in a comment. instrument.require() fails on under-invocation and refuses to report while counting is disabled.

README.md

@@ -363,6 +363,7 @@ docker/                      Dockerfile, dashboard image, compose (demo cluster)
 scripts/setup.bat / setup.sh interactive setup helpers
 config/                      nodes + cluster env examples
 examples/my_task_template.py starting point for your own model
+test_verified_units.py       full-domain checks of every shipped verified path (24)
 docs/                        QUICKSTART, LIMITS, CUSTOM_TASK, TAILSCALE
 daisychain/spikewhale_task.py   trains the real SpikeWhale on streamed HF datasets
 daisychain/spikewhale_panel.py  slider control panel (localhost:8899)
@@ -370,6 +371,56 @@ web/                         DaisyChain-Web: P2P browser training (WebRTC + WebG
 export_luts_web.py           regenerates web/public LUTs from the trained units
 ```
 
+## Recent updates (August 2026) — verified compute path
+
+Three changes to `daisychain/verified/`, each measured rather than asserted.
+`python test_verified_units.py` (24 checks) reproduces all of it.
+
+**Bounded GEMM memory.** `LUTBackend.gemm` and `NeuralBackend.gemm` materialized
+the whole `(m, n, k)` product block before reducing it, so peak memory was cubic
+in layer width. At the SpikeWhale panel's maximum (hidden 768, sequence 512) a
+single layer's forward allocated **2.4 GB** — on the spare hardware this project
+exists to use. Both now block the `m` axis. The contraction axis `k` is untouched,
+so the sum and its order are unchanged and results stay bit-identical:
+
+| GEMM | before | after |
+| --- | --- | --- |
+| 64x64x64 | 2.3 MB | 2.3 MB (unchanged path) |
+| 256x256x256 | 135.8 MB | 68.9 MB |
+| 512x768x768 (panel max) | 2426.9 MB | **77.2 MB** |
+| neural backend, 64x96x96 | 519.2 MB | **57.5 MB** |
+
+Caps are class attributes (`LUTBackend.max_block_bytes`,
+`NeuralBackend.max_products`), tunable per instance. Below the cap the LUT path
+takes the original single-block branch unchanged.
+
+The two backends need *different* accounting, which is worth knowing before tuning
+them: a LUT product costs 8 bytes, but a neural product is split into four nibble
+pairs through a 128-wide net and costs ~880 bytes. Applying the LUT's byte budget
+to the neural path computes a block 110x too large and never splits at all.
+
+**The multiply LUT is certified, not trusted.** `build_luts()` returned its tables
+unchecked while the docs described a self-certify gate. Because the table *is* the
+complete finite domain, certifying it **is** the exhaustive verification:
+`LUTBackend.__init__` now checks all 65536 entries against signed integer multiply
+and raises on mismatch. Cost: **0.5 ms**.
+
+**Full-domain tests for the paths that ship.** The units' exhaustive verification
+covers the scalar entry points (`NeuralMul8.verify()` walks `mul()`); production
+runs the batched ones — `mul_array`, `relu_array`, `requant_array` — and the LUTs
+built from them, which are different code. `test_verified_units.py` checks every
+shipped path against golden integer arithmetic over its complete domain. All pass
+today; nothing would have caught a regression before.
+
+**Two guards against silent no-ops.** `gemm_int8` enforces the int32 accumulator
+bound (`MAX_INT32_K = 131071`) instead of asserting it in a comment, since layer
+width is user-selectable and an overflow would produce wrong numbers rather than
+raise. `instrument.require(**minimums)` fails when a verified unit was
+under-invoked, and refuses to report at all while counting is disabled — a zero
+from a probe that was switched off is not evidence that the units did not run.
+
+---
+
 ## Install
 ```bash
 pip install torch numpy psutil

daisychain/verified/backends.py

@@ -42,16 +42,38 @@ class NeuralBackend:
     def available(self) -> bool:
         return hasattr(self.mul, "mul_array")
 
+    #: Cap on PRODUCTS (m*n*k entries) handed to one batched multiply.
+    #:
+    #: Counted in products, not bytes, because bytes-per-product here is not the
+    #: 8 of an int64 table lookup: `reshape(-1)` materializes the broadcast pair
+    #: arrays, `mul_array` then splits each product into FOUR nibble pairs, and
+    #: each pair goes through a 128-wide net whose activations dominate everything
+    #: else. Measured on the numpy side alone: ~880 bytes per product (589,824
+    #: products -> 519 MB peak), and torch's own allocations sit on top of that.
+    #:
+    #: Applying LUTBackend's m*n*k*8 accounting here -- which the first version of
+    #: this patch did -- computes a block 110x too large and never splits at all.
+    #: The contraction axis k is untouched either way, so blocking cannot change
+    #: the sum or its order: the result stays bit-identical.
+    max_products = 1 << 16
+
     def gemm(self, A: np.ndarray, B: np.ndarray) -> np.ndarray:
         A = np.asarray(A).astype(np.int64)
         B = np.asarray(B).astype(np.int64)
         m, k = A.shape
         _, n = B.shape
-        # all (A[i,t], B[t,j]) pairs -> one batched neural multiply -> sum over k
-        Ai = np.broadcast_to(A[:, None, :], (m, n, k))          # (m,n,k)
-        Bj = np.broadcast_to(B.T[None, :, :], (m, n, k))        # (m,n,k)
-        prod = self.mul.mul_array(Ai.reshape(-1), Bj.reshape(-1)).reshape(m, n, k)
-        return prod.sum(axis=2).astype(np.int64)
+        Bt = B.T[None, :, :]
+        out = np.empty((m, n), dtype=np.int64)
+        rows = max(1, int(self.max_products // max(1, n * k)))
+        for i in range(0, m, rows):
+            r = A[i:i + rows]
+            rn = r.shape[0]
+            # all (A[i,t], B[t,j]) pairs in this block -> one batched neural multiply
+            Ai = np.broadcast_to(r[:, None, :], (rn, n, k))
+            Bj = np.broadcast_to(Bt, (rn, n, k))
+            prod = self.mul.mul_array(Ai.reshape(-1), Bj.reshape(-1)).reshape(rn, n, k)
+            out[i:i + rows] = prod.sum(axis=2)
+        return out.astype(np.int64)
 
 
 def pick_backend(neural=None):

daisychain/verified/instrument.py

@@ -32,3 +32,42 @@ def bump(key: str, n: int = 1):
 
 def report() -> dict:
     return dict(COUNTS)
+
+
+def enabled() -> bool:
+    """Whether counting is on.
+
+    Callers need this to tell "the units did not run" apart from "nobody was
+    counting". A zero count from a disabled instrument is not evidence about the
+    units; reporting it as one is how a silent no-op passes for a result.
+    """
+    return _ENABLED
+
+
+def require(**minimums: int) -> dict:
+    """Assert each counter reached a minimum, and return the counts.
+
+    The counters are the evidence that compute went THROUGH the verified units
+    rather than around them -- but nothing forces anyone to look. A run where the
+    units never fired otherwise produces the same silence as a run where they
+    fired and the result was unremarkable.
+
+        instrument.enable()
+        ... train ...
+        instrument.require(**{"NeuralMul4.forward_calls": 1})
+
+    Raises RuntimeError if counting is disabled (a zero here would be an artifact
+    of the probe, not a fact about the run) or if any counter fell short.
+    """
+    if not _ENABLED:
+        raise RuntimeError(
+            "instrument.require() called while counting is disabled -- enable() "
+            "first, or the zero counts say nothing about whether the units ran")
+    short = {k: (COUNTS.get(k, 0), n) for k, n in minimums.items()
+             if COUNTS.get(k, 0) < n}
+    if short:
+        raise AssertionError(
+            "verified units under-invoked: "
+            + ", ".join("%s=%d (want >=%d)" % (k, got, want)
+                        for k, (got, want) in sorted(short.items())))
+    return dict(COUNTS)

daisychain/verified/kernel.py

@@ -11,11 +11,24 @@ from __future__ import annotations
 import numpy as np
 
 
+#: Largest contraction length an int32 accumulator can take without overflow.
+#: |a*b| <= 128*128 = 16384 for int8 operands, so K*16384 must stay inside int32.
+#: The bound is real headroom (131071), but layer width is user-selectable from the
+#: SpikeWhale panel, so it is checked rather than asserted in a comment -- an
+#: overflow here would silently produce wrong numbers, not raise.
+MAX_INT32_K = (2 ** 31 - 1) // (128 * 128)
+
+
 def gemm_int8(A: np.ndarray, B: np.ndarray) -> np.ndarray:
     """Signed INT8 GEMM with exact int32 accumulation (tensor-core semantics)."""
+    k = A.shape[-1]
+    if k > MAX_INT32_K:
+        raise ValueError(
+            "contraction length %d exceeds int32 accumulator headroom %d; "
+            "accumulate in int64 for this size" % (k, MAX_INT32_K))
     a = A.astype(np.int32)
     b = B.astype(np.int32)
-    return a @ b            # exact integer matmul, no overflow for our sizes
+    return a @ b            # exact integer matmul within the checked bound
 
 
 def random_int8(shape, rng) -> np.ndarray:

daisychain/verified/lut.py

@@ -34,12 +34,43 @@ def build_relu8_lut(relu) -> np.ndarray:
     return relu.relu_array(np.arange(256)).astype(np.int64)
 
 
+def certify_mul8_lut(lut: np.ndarray) -> tuple[int, int]:
+    """Check the materialized multiply table against signed integer multiply.
+
+    The table IS the entire finite domain, so certifying it is the exhaustive
+    verification -- not a sample of it. Costs ~0.5 ms, which is why there is no
+    reason to take the guarantee on trust at runtime.
+    """
+    a = np.arange(256)
+    au, bu = np.repeat(a, 256), np.tile(a, 256)
+    sa = np.where(au >= 128, au - 256, au)
+    sb = np.where(bu >= 128, bu - 256, bu)
+    got = lut[au, bu].ravel()
+    return int((got == sa * sb).sum()), got.size
+
+
 class LUTBackend:
     """GEMM via the materialized (verified) multiply table + integer accumulate."""
     name = "lut"
 
-    def __init__(self, mul):
+    #: Cap on the (rows, n, k) product block held at once, in bytes. The block is
+    #: an int64 temporary of m*n*k entries, so an unchunked GEMM allocates
+    #: m*n*k*8 -- cubic in layer width. At the panel's maximum settings
+    #: (hidden 768, seqlen 512) that is 2.4 GB for ONE layer's forward, on
+    #: machines this project targets precisely because they are small. Blocking
+    #: the m axis bounds it; the contraction axis k is untouched, so the sum and
+    #: its order are unchanged and the result is bit-identical.
+    max_block_bytes = 64 << 20
+
+    def __init__(self, mul, certify: bool = True):
         self.mul_lut = build_mul8_lut(mul)
+        if certify:
+            ok, tot = certify_mul8_lut(self.mul_lut)
+            if ok != tot:
+                raise ValueError(
+                    "verified multiply LUT is not bit-exact: %d/%d entries match "
+                    "signed integer multiply" % (ok, tot))
+            self.certified = (ok, tot)
 
     def available(self):
         return True
@@ -47,9 +78,17 @@ class LUTBackend:
     def gemm(self, A: np.ndarray, B: np.ndarray) -> np.ndarray:
         au = (A.astype(np.int64) & 0xFF)
         bu = (B.astype(np.int64) & 0xFF)
-        # products via table lookup, then sum over the contraction axis
-        prod = self.mul_lut[au[:, None, :], bu.T[None, :, :]]   # (m, n, k)
+        m, k = au.shape
+        n = bu.shape[1]
         from . import instrument
         instrument.bump("VerifiedMul(LUT).gemms", 1)
-        instrument.bump("VerifiedMul(LUT).products", prod.size)
-        return prod.sum(axis=2)
+        instrument.bump("VerifiedMul(LUT).products", m * n * k)
+        # products via table lookup, then sum over the contraction axis
+        bt = bu.T[None, :, :]
+        rows = max(1, int(self.max_block_bytes // max(1, n * k * 8)))
+        if rows >= m:                                   # small layer: one block
+            return self.mul_lut[au[:, None, :], bt].sum(axis=2)
+        out = np.empty((m, n), dtype=np.int64)
+        for i in range(0, m, rows):
+            out[i:i + rows] = self.mul_lut[au[i:i + rows, None, :], bt].sum(axis=2)
+        return out

test_verified_units.py

@@ -0,0 +1,169 @@
+"""Full-domain regression tests for the paths that actually ship.
+
+The units already carry exhaustive verification of their SCALAR entry points
+(`NeuralMul8.verify()` walks all 65536 signed pairs against `a*b`). Production
+does not call those. It calls the BATCHED paths -- `mul_array`, `relu_array`,
+`requant_array` -- and the lookup tables built from them. Those are different
+code: nibble concatenation, one batched forward, vectorized sign correction.
+
+A guarantee that covers a path nobody runs is not the guarantee anyone wanted,
+so every check here goes against a golden reference (Python integer arithmetic),
+over the complete finite domain, on the path that ships.
+
+Run:  python test_verified_units.py
+"""
+from __future__ import annotations
+
+import sys
+
+import numpy as np
+
+from daisychain.verified.qat import load_units, build_luts
+from daisychain.verified import instrument
+from daisychain.verified.kernel import gemm_int8, MAX_INT32_K
+from daisychain.verified.backends import NeuralBackend
+from daisychain.verified.lut import certify_mul8_lut
+
+FAILURES = []
+
+
+def ck(name, cond, detail=""):
+    print("  %-4s %s%s" % ("ok" if cond else "FAIL", name,
+                           "" if cond else "  <- " + str(detail)))
+    if not cond:
+        FAILURES.append(name)
+
+
+def signed_domain():
+    """Every ordered pair of signed bytes, and their true products."""
+    a = np.repeat(np.arange(-128, 128), 256)
+    b = np.tile(np.arange(-128, 128), 256)
+    return a, b, a.astype(np.int64) * b.astype(np.int64)
+
+
+def main():
+    units = load_units()
+    mul, requant, relu_unit = units
+    luts = build_luts(*units)
+    backend = luts["backend"]
+
+    print("multiply -- the SHIPPED batched path, full domain")
+    a, b, gold = signed_domain()
+    got = mul.mul_array(a.astype(np.int8), b.astype(np.int8))
+    ck("mul_array == a*b over all 65536 signed pairs", np.array_equal(got, gold))
+
+    print("multiply -- the materialized table")
+    ok, tot = certify_mul8_lut(backend.mul_lut)
+    ck("mul LUT == a*b over all 65536 entries", ok == tot, "%d/%d" % (ok, tot))
+    ck("LUTBackend self-certified at construction",
+       getattr(backend, "certified", None) == (65536, 65536))
+
+    print("requantize -- sat_int8(x >> 8), full int16 domain")
+    x = np.arange(65536)
+    xs = np.where(x >= 32768, x - 65536, x)
+    rq_gold = np.clip(xs >> requant.shift, -128, 127)
+    ck("requant_array == sat_int8(x >> shift) over all 65536",
+       np.array_equal(requant.requant_array(x), rq_gold))
+    ck("requant LUT == golden over all 65536",
+       np.array_equal(luts["requant"][x & 0xFFFF], rq_gold))
+
+    print("relu -- max(0, x), full int8 domain")
+    r = np.arange(256)
+    rs = np.where(r >= 128, r - 256, r)
+    relu_gold = np.maximum(0, rs)
+    ck("relu_array == max(0,x) over all 256",
+       np.array_equal(relu_unit.relu_array(rs.astype(np.int8)), relu_gold))
+    ck("relu LUT == golden over all 256",
+       np.array_equal(luts["relu"][r & 0xFF], relu_gold))
+
+    print("GEMM -- blocked paths must be bit-identical to golden integer matmul")
+    rng = np.random.default_rng(11)
+    for (m, k, n) in [(1, 1, 1), (3, 5, 7), (64, 64, 64), (96, 128, 96), (129, 257, 65)]:
+        A = rng.integers(-128, 128, size=(m, k), dtype=np.int16).astype(np.int8)
+        B = rng.integers(-128, 128, size=(k, n), dtype=np.int16).astype(np.int8)
+        g = A.astype(np.int64) @ B.astype(np.int64)
+        ck("LUT gemm %dx%dx%d == int64 matmul" % (m, k, n),
+           np.array_equal(backend.gemm(A, B), g))
+
+    # The neural backend is the slow functional path; check it on a small shape
+    # AND across a block boundary, since blocking is what this change introduced.
+    # The block count is ASSERTED rather than assumed: mul_array bumps
+    # NeuralMul4.forward_calls once per call, i.e. once per block, so the counter
+    # is direct evidence the split actually happened. A test that says
+    # "forced multi-block" while silently running one block proves nothing.
+    nb = NeuralBackend(mul)
+    nb.max_products = 16                          # force many blocks on a tiny GEMM
+    A = rng.integers(-128, 128, size=(17, 9), dtype=np.int16).astype(np.int8)
+    B = rng.integers(-128, 128, size=(9, 11), dtype=np.int16).astype(np.int8)
+    instrument.enable()
+    instrument.reset()
+    got_nb = nb.gemm(A, B)
+    blocks = instrument.report().get("NeuralMul4.forward_calls", 0)
+    instrument.disable()
+    ck("neural gemm actually split into >1 block", blocks > 1, "blocks=%d" % blocks)
+    ck("neural gemm == int64 matmul (multi-block)",
+       np.array_equal(got_nb, A.astype(np.int64) @ B.astype(np.int64)))
+
+    print("GEMM -- blocking must not change results as the block size varies")
+    A = rng.integers(-128, 128, size=(40, 24), dtype=np.int16).astype(np.int8)
+    B = rng.integers(-128, 128, size=(24, 32), dtype=np.int16).astype(np.int8)
+    ref = backend.gemm(A, B)
+    same = True
+    for cap in (1 << 10, 1 << 14, 1 << 18, 1 << 26):
+        backend.max_block_bytes = cap
+        same &= bool(np.array_equal(backend.gemm(A, B), ref))
+    backend.max_block_bytes = 64 << 20
+    ck("identical across block sizes 1 KB .. 64 MB", same)
+
+    print("int32 accumulator bound is enforced, not assumed")
+    ck("MAX_INT32_K == 131071", MAX_INT32_K == 131071, MAX_INT32_K)
+    small = np.zeros((1, 4), dtype=np.int8)
+    ck("gemm_int8 accepts K within bound",
+       gemm_int8(small, np.zeros((4, 1), dtype=np.int8)).shape == (1, 1))
+    try:
+        gemm_int8(np.zeros((1, MAX_INT32_K + 1), dtype=np.int8),
+                  np.zeros((MAX_INT32_K + 1, 1), dtype=np.int8))
+        ck("gemm_int8 rejects K past the bound", False, "no error raised")
+    except ValueError:
+        ck("gemm_int8 rejects K past the bound", True)
+    except MemoryError:
+        ck("gemm_int8 rejects K past the bound", False,
+           "allocated before checking -- bound must be checked first")
+
+    print("instrument -- a zero must not be able to masquerade as evidence")
+    instrument.disable()
+    instrument.reset()
+    ck("enabled() reports the probe state", instrument.enabled() is False)
+    try:
+        instrument.require(**{"NeuralMul4.forward_calls": 1})
+        ck("require() refuses to report while disabled", False, "returned instead")
+    except RuntimeError:
+        ck("require() refuses to report while disabled", True)
+
+    instrument.enable()
+    instrument.reset()
+    backend.gemm(np.ones((2, 2), dtype=np.int8), np.ones((2, 2), dtype=np.int8))
+    try:
+        instrument.require(**{"VerifiedMul(LUT).gemms": 1})
+        ck("require() passes when the unit actually ran", True)
+    except AssertionError as e:
+        ck("require() passes when the unit actually ran", False, e)
+    try:
+        instrument.require(**{"VerifiedMul(LUT).gemms": 10 ** 9})
+        ck("require() fails when a unit is under-invoked", False, "did not raise")
+    except AssertionError:
+        ck("require() fails when a unit is under-invoked", True)
+    instrument.disable()
+
+    print()
+    if FAILURES:
+        print("FAILED: %d" % len(FAILURES))
+        for f in FAILURES:
+            print("   - %s" % f)
+        return 1
+    print("all checks passed")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())