// in is uint8_t*: zero-extend
int32_t x = (int32_t)in[idx] - INPUT_ZP;

// BUG: as if in were int8_t*: sign-extend
int32_t x = (int32_t)(int8_t)in[idx] - INPUT_ZP;

What it is

A compiler for one very small neural network: a single 3×3 convolution from one channel to four, a ReLU, and a 2×2 max pool, over an 8×8 uint8 image. That is about 200 bytes of activations end to end. The model is deliberately that small, because at that size one person can build every stage a real compiler has — a spec, an IR, a memory planner, a code generator, a formal proof, and an optimization pass — and then check each one instead of trusting it. The output is C that compiles with the Pico SDK and runs on a Raspberry Pi Pico.

How it works

Six phases, each producing an artifact the next one reads.

• Spec. A quantized PyTorch model is exported to qparams.json, and a pure numpy reference reproduces it exactly. This reference, not PyTorch, is what everything downstream is checked against.
• IR. A small SSA graph with two kinds of tensors. Activations get live ranges and go in the SRAM arena; weights and biases are constants and go in flash, so they never compete for the arena.
• Planning. Alias analysis, then a greedy first-fit allocator, tried under two sort orders and the smaller result kept.
• Codegen. The IR plus the memory plan become model.c and model.h: one static uint8_t arena[], and every tensor addressed at its planned offset.
• Proof. Z3 compares two independently written transliterations of the innermost kernel — one from the spec, one from the emitted C.
• Optimization. Packed weight loads and loop unrolling, measured on the ARM disassembly rather than estimated, and then re-proved.

How it was verified

Three layers, each of which can fail in a way the others cannot catch.

First, the numpy spec is checked against the real quantized PyTorch model on 2,000 random inputs, bit for bit. That is what makes the spec trustworthy enough to be a spec at all. Second, the generated C is compiled on the host and checked against that spec on 500 vectors, again bit for bit. Third — and this is the part tests cannot do — Z3 is asked whether any input exists on which the C and the spec disagree. It answers UNSAT.

The difference matters. 500 passing vectors is 500 points out of a domain of roughly 2¹⁴⁴: nine uint8 activations and nine int8 weights, with the bias left symbolic so the result holds for every int32 bias too. A sampled test cannot distinguish a kernel that is correct from one that is correct on everything you happened to try. The proof can. The whole-network claim is inductive: this exact kernel runs 4 × 6 × 6 = 144 times with different concrete values, and proving it for all symbolic values covers every one of those as a special case.

The proof is also checked for the ability to fail. Reintroducing the sign-extension bug from Phase 0 flips the query to SAT, and Z3 returns a concrete disagreeing input — the “Break it” panel above shows the one it found.

Results

The planner’s alias analysis lets ReLU write into the convolution’s output buffer, and the pool output then reuses the lots the input has vacated. That is the whole 46% saving: no cleverness beyond noticing which tensors are dead.

On the optimized kernel, checking the disassembly first turned out to matter. The generated code was reloading the same weight bytes on every iteration; packing them into 32-bit words and unrolling the multiply-accumulate cut the inner loop from 137 dynamic instructions per output pixel to 45. The proof was then re-run against the optimized code and still returns UNSAT.

What didn’t work

Symmetric int8 activations were the original plan, and qnnpack rejected them: the backend wanted unsigned quint8 with a real, non-zero zero point. Every later phase carries that decision — it is why the spec zero-extends the activation and sign-extends the weight, and why getting that one distinction wrong is a realistic enough bug to be worth proving against.

The Z3 proof on the optimized kernel timed out at first. Asking the solver to reason about packing, unpacking, the multiply-accumulate, and floating-point requantization in one query was too much. Decomposing it worked: prove the packed accumulator is bit-identical to the naive one over all inputs (pure bit-vector, no floating point), then compose with the already-proven equivalence, since requantization is a deterministic function of the accumulator.

MaxPool is not aliased. It changes shape, and the planner cannot prove that reuse safe in general, so it does not do it here either. A 36-byte saving is not worth an unsound rule.

Next

Applying the compiler to a robotics workload on the RP2040.

GenAI statement, from the repository: generative AI was used in the creation of this project to (1) teach me the concepts behind the project, (2) proofread code, and (3) assist in debugging.