tools/infer: a deterministic inference engine, and the gates that check it

[zemo-g]

Twelve commits building a transformer inference engine where the same
request produces the same bytes, on three different Apple GPUs, checked by
tests that demand exact equality rather than closeness. Written in Rail,
running on Metal, no CUDA, no PyTorch, no Python in the inference path.

Full README with the claims and their limits: tools/infer/README.md.

The claims, each with a gate

1. Incremental decode is bit-identical to a full forward pass.
   kv138_gate.rail requires max |full - incremental| == 0.0 across all
   98,304 hidden values and the full 16,384-wide logit row.
2. A chunk of K tokens equals K sequential steps, caches included. The
   keystone. ng0_keystone_gate.rail: 48 tokens both ways, independent
   buffer sets, divergent comparisons: 0 (of 34).
3. Therefore speculative decoding cannot change the output.
   ng0_spec.rail does n-gram draft-and-verify with no draft model and no
   second set of weights: 2.0x fewer forward passes, byte-equal output.
4. It holds across three chips and three OS versions, M4 Pro / M1 Ultra
   / base M1, each compiling its own dylib and kernels, same hash.

The gates can fail

An outside review found they could not. Max-difference alone is blind: an
all-NaN run leaves every running max at 0.0 because IEEE says every
comparison with NaN is false, and an all-zero run agrees perfectly while
proving nothing. Every parity gate now counts finite nonzero values first
and fails if the tensor is mostly dead. Verified by deleting the weights
file: the gate that used to report max diff 0.0, PASS now reports
hidden 0/98304 live and fails.

The roofline changed the plan

rl0_gate.rail measures the memory ceiling with a coalesced streaming
kernel rather than quoting a spec sheet. Batch-1 decode reads 0.45 GB of
weights per token and should be memory-bound. It reached 6% of measured
bandwidth. So the gate measured the other term: 288 empty dispatches cost
24-34ms against a 36ms decode step, because every tgl_* call built its own
command buffer, committed, and waited.

tgl_batch_begin/tgl_batch_end encode the step into one command buffer.
Kernels, arguments and order are untouched, so only the moment the CPU stops
to listen changes.

	ms/token	tok/s	% of measured bandwidth
one command buffer per dispatch	36.1	27.6	5.7%
one command buffer per token	7.5	132.9	27.1%

4.8x, decode checksum bit-identical, all three gates unchanged. That is
what the gates are for.

The gate also failed its own repeatability check twice (16.7%, then 20.6%
spread between identical bandwidth runs) and was fixed by improving the
estimator rather than relaxing the threshold: best-of-N, since contention
only ever slows a run, and interleaved comparison batches, since this
machine runs a GPU beacon at ~9fps and sequential batches turn drift in load
into fake disagreement. Spread is now 0.7-2.2%.

The ids become language

tok0.rail is the byte-level BPE the 240M base run was trained with: 173
base bytes, 15,404 merges, vocab 15,577. Encoding is deliberately the slow
obvious algorithm because that is what produced these ids; a faster encoder
giving different ids would feed the model tokens it never saw.

tok0_gate.sh checks it two independent ways, because each is blind where
the other sees. It compares against bpe_replica.py over seven cases picked
for what breaks byte-level BPE, and skipping one merge is caught by four of
seven. But that check cannot see its own input: truncating the merges file
by 100 lines left all seven reporting ok. So it also verifies the merges
against the run's recorded tokenizer.sha256 and pins the alphabet hash,
which that recording never covered even though the alphabet is half the
tokenizer.

Being precise about the size of this

Replayability, not verifiability. Verification costs what generation
cost: a checker needs the weights, matching hardware, and the same time.
That makes it a fraud-proof primitive, not a succinct proof to a stranger.
zkML and TEE attestation give a verifier an asymptotic advantage; this does
not.

Batch-1 is a choice, not a requirement. The keystone gate is in fact a
batch-invariance proof; this engine has not spent it on throughput yet.

Greedy only, and prior art exists and is good (LLM-42 runs the same
argument in the opposite direction). The honest contribution is the
numerical half: making chunk-equals-sequential true bitwise on commodity
hardware.

Verification

190/190 tests, tokenizer gate 9/9, all three parity gates pass, leak guard
clean. Start with kv0_gate.rail and rsqrt_probe.rail, which need no
weights and no downloads.