web/docs/VERIFICATION.md

Verification — why you can trust the numbers

DaisyChain-Web's core claim is strong: every device — any GPU, any driver, or plain CPU — computes bit-identical results, so replicas can be compared by hashing raw bytes. This document explains the layers that make that claim checked by things that run, not argued. Full current results: TEST_RESULTS.md.

The verified INT8 units

All model multiplies run through one primitive: a block-scaled int8 GEMM.

1. Inputs are quantized per row / per column: scale = max(|row|)/127 (floored at 1e-8), values to int8.
2. Products come from mul_lut — a 65536-entry table of exact int8 products — accumulated in int32 (exact; no overflow at these sizes).
3. The float epilogue is fixed to a bit-exact rounding schedule: epi(s,a,b) = f32(f32(f32(s)·a)·b) — round to f32 after the int→float conversion and after each multiply.

Steps 1–2 are integer-exact everywhere by construction. Step 3 is where "bit-identical across devices" is usually lost — so it is pinned to WGSL's guarantees (add/multiply are correctly rounded; division is not, so no division ever runs on the GPU — scales are derived in JS f64, which is exactly rounded and device-identical).

Layer 1: exact init gates (every device, every boot)

No kernel computes a single training value before passing its gate: run the kernel and the JS mirror on a sweep of shapes (ragged ones included) and compare — int32 accumulators exactly, f32 outputs at the bit level. Any mismatch demotes the device to the CPU mirror. Bit-level matters: JS !== treats -0 === 0, but real ISAs have non-IEEE modes that flush −0 to +0, and the replica hash would see that. The gates compare exactly what the hash sees.

Gates re-run at every init because floating-point behavior is runtime state on real hardware (rounding mode and denorm flushing are per-wave MODE registers on RDNA2, set by the driver) — a device model can't be trusted across boots; a fresh gate can.

Some gates additionally gate the gate: the B2B chain gate hunts for an input where the old and new quantize specs actually disagree and requires the GPU to match the new one — so a pass is something the old spec would fail, not a vacuous agreement.

Layer 2: continuous audit (every run, live shapes)

Init gates use test shapes; the audit samples random output cells of the live GEMMs during training and recomputes them through the units. A kernel that is correct at gate shapes but wrong at live shapes (stride bugs, padding bugs) is caught while it trains.

Layer 3: the kernel probe (every step, cross-device)

The weight hash cannot catch a device whose kernel is wrong — weights only depend on the gradient bytes everyone receives. So each step every device also publishes a probe hash: the same seeded int8 GEMM through its live kernel. Same math ⇒ same hash, on every honest device, any backend.

Layer 4: the referee — an IEEE-754 oracle

Who checks the JS mirror? test_ieee.js builds a binary32 oracle from the IEEE-754 definition in exact BigInt arithmetic — no Math.fround anywhere in it, round-to-nearest-even, subnormals, signed zero. The mirror's epilogue agrees with the oracle on 500k+ checks, including a tie-to-even ladder around 2²⁴ — and the oracle rejects the older round-once mirror on 34% of inputs, which is what makes the agreement meaningful.

Layer 5: properties and mutation scores

test_metamorphic.js holds correctness properties that need no reference implementation: relations (permuting rows permutes outputs; a zero row yields zeros; batches decompose; single-cell sensitivity) plus two definitional absolutes — fused-ReLU output can never be negative, and at unit scales the output must equal the exact integer dot product. The split is principled: if out satisfies every relation, so does 2·out — relations are provably blind to value bugs, absolutes are not.

test_corpus.js then mutation-scores the checkers themselves against an externally authored bug taxonomy (dipankarsarkar/gpuemu-corpus): each ported bug must be caught (4/4 properties, 4/4 differential), and a control run must stay clean. A checker that has never rejected anything is decoration; these have a scoreboard.

Hardware ground truth (RDNA2 ISA audit)

Reading a real GPU ISA against the assumptions confirmed on silicon: V_DOT4_I32_I8 is an exact packed int8 dot (the DP4A path is exact by ISA guarantee); f32 add/mul are 0.5 ULP; reciprocal is 1 ULP (division stays off the GPU). It also produced two hardenings: the bit-level gate comparisons above, and a proof that FMA contraction of the quantize's x·inv + 0.5 (one rounding instead of two — a choice WGSL leaves to the compiler) is floor-invisible by construction: last-ulp anomalies occur at binade edges, but RNE tie parity keeps both rounding schedules on the same side of every integer, so the quantized int8 is identical either way. Since no gate can forbid a compiler an fma, that one had to be a theorem, not a check — test_b2b.js asserts both halves (anomalies exist; zero survive floor).

What this does NOT protect against

A malicious peer that runs the correct math but lies — sends a crafted gradient — is not caught by any of this; there is no gradient authentication. The verification stack proves the computation is right on every honest device. Trust in the participants is still yours to establish.