Null pointer optimization - #555
Closed
gabriel-barrett wants to merge 6 commits into
Closed
Conversation
Memory pointers now start at 1: the executor, the codegen template, the trace builder, both Lean evaluators, the --interp interpreter and the BigUint limb-chain builders all mint insertion-index + 1 and dereference ptr - 1 (0 never binds). The memory circuit enforces it with a new constraint, IsFirstRow * is_real * (ptr - 1): together with the existing increment chain, real-row pointers are exactly 1..height, so 0 becomes the IMPOSSIBLE pointer. This reserves the value 0 as a null-pointer niche for enum layouts (a pointer-typed field can never legitimately hold 0), which the follow-up null-pointer optimization builds on. Codegen regenerated. Kernel FFT pins drift microscopically (~+0.001%: the kernel byte-decomposes some pointer values, and every pointer shifted by one) - all 71 pins and the shard aggregate re-measured. aiur (cargo + prove suite incl. interpreter parity), ixvm, multi-stark and recursive-verifier suites pass; fmt, clippy, deny clean.
A datatype with exactly two constructors, one nullary and the other carrying a top-level pointer field, drops its tag slot: pointers are 1-based (0 is pinned impossible by the memory circuit), so the pointer field doubles as the discriminant. The nullary constructor is the all-zero vector; the payload constructor is its bare fields. Nat-likes shrink 2 -> 1, list nodes lose a column everywhere (ListNode<U64> 10 -> 9, ByteStream cons 3 -> 2, RBTreeMap nodes, ...). Matches on niche types dispatch on the pointer slot: the nullary arm is case 0, the payload arm is the DEFAULT arm - its inequality witness against 0 exists precisely because real pointers are nonzero - and a wildcard or explicit default covers whichever constructor is not listed (case 0 with a payload arm present; dead and NOT compiled when both are). The not-compiled part matters: a compiled-but-discarded arm still consumes a selector index, desynchronizing stored selector ids from the layout's selector count (caught by rbtree_map_balance_fix, whose fallthrough patterns hit exactly that as a ColumnOutOfRange at system build). Implemented in the layout pass (hasPointerNiche + niche slot on ConstructorLayout), lowering (construction, match dispatch, match-level arm classification via NicheMatchCtx), the Source flatten/unflatten mirrors (also fixing latent tagless mis-unflatten), and the flat-level BigUint limb-chain builders on both the Rust and Lean sides (memory[10] -> memory[9], Nil = zeros, walk ends at next_ptr == 0). Value-level evaluators are layout-transparent and unchanged. Codegen regenerated (kernel shrinks ~5%); all 71 kernel FFT pins and the shard aggregate re-measured (0-1.2% cheaper). aiur (cargo + prove suite incl. divmod hints and parity), ixvm, multi-stark and recursive-verifier suites pass; fmt, clippy, deny clean.
A niche match listing the payload constructor with no nullary arm and no default would otherwise route the nullary value (niche slot 0) into the payload default arm and execute it with garbage bindings — partial matches are legal (there is no exhaustiveness check; tagged layouts surface MatchNoCase at runtime). Such matches now get a synthesized case-0 arm asserting 0 = 1: a runtime error mirroring MatchNoCase, and an unsatisfiable arm in-circuit. Codegen regenerated; kernel FFT pins re-measured (+0.01..+1.4% from the extra arms on partial matches in the kernel/verifier sources).
Prove-suite cases for the niche layout: construction of both variants, both match directions, the wildcard-covers-nullary form (compiles to case 0), non-tail matchContinue dispatch, a pointer field at nonzero offset (NichePair, niche slot 1), and Nil-crossing recursion on the width-1 extreme (PNat: the value IS the bare pointer).
gabriel-barrett
force-pushed
the
null-pointer-optimization
branch
from
August 12, 2026 21:57
ab615ca to
0ec1526
Compare
The list VALUE is now one field element: 0 IS Nil (the impossible pointer), anything else points at the (head, tail) cell. No tag slot, no stored Nil node, and every traversal's base case is a plain field match instead of a memory load — across the kernel and the recursive verifier, list emptiness checks no longer touch the memory channel. Sweep of ~1,400 sites across 28 files: store(ListNode.Nil) -> List.Nil (now free), store(ListNode.Cons(x, r)) -> List.Cons(store((x, r))), match load(l) -> match l with the load moved into the Cons arm, and the deref-let uncons idiom updated. The unconstrainedBigUintDivMod contract follows: the typing rule takes the niche list datatype by value (no longer a pointer), and the flat-level builders on both sides (read/build/find_klimbs_u64, BytecodeEval's limb chains) plus the value-level mirrors (SourceEval, Interpret — Cons/Nil now identified by shape, not declaration order) build 0-terminated chains with (limb, tail) cells and no Nil row. The test toplevel's BNode migrates to the same shape. Codegen regenerated; all 71 kernel FFT pins and the shard aggregate re-measured (all down 0.0-0.3% — the proxy is blake3-dominated; the structural win is the removed per-traversal load and the deleted Nil rows per memory width). aiur (cargo + prove suite incl. divmod hints and parity), ixvm, multi-stark and recursive-verifier suites pass; fmt, clippy, deny clean.
gabriel-barrett
force-pushed
the
null-pointer-optimization
branch
from
August 12, 2026 22:13
0ec1526 to
40596b4
Compare
Same treatment as List: a Layer value is ONE field element — 0 is Nil, anything else points at the (previous layer, digest) cell. No stored Nil node, the layer parameters of the blake3 chunk folds (blake3_compress_chunks/_block/_finish, b3_io_chunks, b3_lane_chunks, b3_rows_chunks) pass the bare value, and the per-layer dereference in blake3_compress_layer / blake3_next_layer moves into the Push arm. Codegen regenerated; all 71 kernel FFT pins and the shard aggregate re-measured (all down 0.0-0.13%). aiur-prove, ixvm (pins + parity), multi-stark and recursive-verifier suites pass; fmt, clippy, deny clean.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements niche optimization. Memory pointers now start at 1 and are never 0.
Lists are now a bit more efficient:
is a single number, 0 being
Nil.