Null pointer optimization

Ix/Aiur/Compiler/Check.lean

@@ -408,17 +408,18 @@ def zonkTyp (t : Typ) : CheckM Typ := do
   zonkTypBound (s.nextMVar + 1) {} t
 
 /-- Fixed signature of `unconstrainedBigUintDivMod`: the inputs are lists
-of U64 limbs — a pointer to a list datatype instantiated at `[U8; 8]`
-(e.g. `KLimbs = List‹U64›`) — and each result is the SAME list datatype
-instantiated at `[G; 8]`. The result limbs are UNCONSTRAINED prover
-advice, so they must not type as range-checked bytes; consumers rebuild
-`u8` limbs via `u8_range_check` (see `glimbs_to_klimbs` in the IxVM
-kernel). The list's constructor shape is not verified here; the runtime
-BigUint::div_rem faults on a malformed chain. Takes the ZONKED input
-type. -/
+of U64 limbs — a null-pointer-niche list datatype instantiated at
+`[U8; 8]` (e.g. `KLimbs = List‹U64›`, one field element wide: 0 = Nil,
+otherwise a pointer to the `(limb, tail)` cell) — and each result is the
+SAME list datatype instantiated at `[G; 8]`. The result limbs are
+UNCONSTRAINED prover advice, so they must not type as range-checked
+bytes; consumers rebuild `u8` limbs via `u8_range_check` (see
+`glimbs_to_klimbs` in the IxVM kernel). The list's constructor shape is
+not verified here; the runtime BigUint::div_rem faults on a malformed
+chain. Takes the ZONKED input type. -/
 def bigUintDivModResultTyp : Typ → CheckM Typ
-  | .pointer (.app g #[.array .u8 8]) =>
-    pure (.pointer (.app g #[.array .field 8]))
+  | .app g #[.array .u8 8] =>
+    pure (.app g #[.array .field 8])
   | τ => throw $ .unconstrainedBigUintDivModType τ
 
 def instantiateParams (params : List String) : CheckM (Array Typ × (Global → Option Typ)) := do

Ix/Aiur/Compiler/Layout.lean

@@ -29,6 +29,21 @@ the remaining recursion depth. The outer interfaces use `decls.size + 1`
 as bound — the monotonic visited set makes this bound unreachable on
 well-formed inputs. -/
 
+/-- Null-pointer niche (the Aiur analogue of Rust's niche optimization):
+a two-constructor datatype where one constructor is nullary and the other
+carries at least one top-level pointer field. Memory pointers are 1-based
+(0 is the impossible pointer, pinned by the memory circuit), so the
+pointer field doubles as the discriminant — 0 IS the nullary variant —
+and the tag slot is dropped. The nullary variant is represented as the
+all-zero vector; matches dispatch on the pointer slot against 0. -/
+def DataType.hasPointerNiche (dt : DataType) : Bool :=
+  let isPtr : Typ → Bool := fun | .pointer _ => true | _ => false
+  match dt.constructors with
+  | [a, b] =>
+    (a.argTypes.isEmpty && b.argTypes.any isPtr) ||
+    (b.argTypes.isEmpty && a.argTypes.any isPtr)
+  | _ => false
+
 mutual
 
 /-- See `Typ.size` for the outer interface. -/
@@ -70,8 +85,10 @@ def DataType.sizeBound (decls : Decls) : Nat → Std.HashSet Global → DataType
         (Concrete.Constructor.sizeBound decls bound visited)
       let maxFields := ctorSizes.foldl max 0
       -- Single-variant enums need no tag slot: the layout matches a plain
-      -- tuple of the sole constructor's fields.
-      if dt.constructors.length == 1 then pure maxFields
+      -- tuple of the sole constructor's fields. Null-pointer-niche enums
+      -- (see `DataType.hasPointerNiche`) drop the tag as well: the pointer
+      -- field doubles as the discriminant.
+      if dt.constructors.length == 1 || dt.hasPointerNiche then pure maxFields
       else pure (maxFields + 1)
 end
 

Ix/Aiur/Interpret.lean

@@ -65,7 +65,7 @@ partial def Value.ppDeref (store : Store) (depth : Nat) : Value → String
   | .pointer _ n =>
       if depth == 0 then "..."
       else
-        match store.getByIdx n with
+        match (if n == 0 then none else store.getByIdx (n - 1)) with
         | some (vs, _) =>
             -- Stored value is `Array Value`; for tagged enums it's
             -- typically `[ctor]` or `[tag, fields...]`. Recurse on each.
@@ -92,7 +92,7 @@ private def matchPattern (store : Store) :
   | .or p1 p2,    v           =>
       matchPattern store p1 v <|> matchPattern store p2 v
   | .pointer p,   .pointer _ n =>
-      match store.getByIdx n with
+      match (if n == 0 then none else store.getByIdx (n - 1)) with
       | some (vs, _) => vs[0]?.bind (matchPattern store p ·)
       | none         => none
   | _,            _           => none
@@ -204,40 +204,41 @@ private def callSite (g : Global) (args : List Value) (m : InterpM Value) : Inte
 
 Value-level mirror of `read_klimbs_u64` / `build_klimbs_u64` in
 `crates/aiur/src/execute.rs`; see `Ix/Aiur/Semantics/SourceEval.lean` for
-the reference-evaluator twin. Constructor 0 = Cons(limb, rest),
-constructor 1 = Nil; limb bytes little-endian, limbs head-first. -/
+the reference-evaluator twin. The list is the niche enum
+`{ Nil, Cons(&(limb, tail)) }`: Nil is a bare value (nothing stored), Cons
+carries a pointer to the `(limb, tail)` cell. Limb bytes little-endian,
+limbs head-first. -/
 
 /-- Store a value content-deduped, returning its pointer (the `.store`
 semantics, callable from the divmod chain builder). -/
 private def storeValueI (v : Value) : InterpM Value := do
   let store ← getStore
   if let some idx := store.getIdxOf #[v] then
-    return .pointer 0 idx
+    return .pointer 0 (idx + 1)
   let idx := store.size
   modify fun s => { s with store := s.store.insert #[v] () }
-  return .pointer 0 idx
+  return .pointer 0 (idx + 1)
 
 /-- Walk a limb-chain pointer, returning the node datatype and the limbs
 head-first. `steps` bounds the walk so a malformed cycle terminates. -/
 private def readLimbChainI (decls : Decls) :
     Nat → Value → InterpM (DataType × List (Array G))
   | 0, _ => throwErr "unconstrainedBigUintDivMod: cyclic limb list"
-  | steps+1, ptrVal => do
-    match ptrVal with
-    | .pointer _ n =>
-      let store ← getStore
-      match store.getByIdx n with
-      | none => throwErr s!"unconstrainedBigUintDivMod: invalid pointer {n}"
-      | some (vs, _) =>
-        match (vs[0]? : Option Value) with
-        | some (.ctor g args) =>
-          match decls.getByKey g with
-          | some (.constructor dt ctor) =>
-            let tag := dt.constructors.findIdx? (· == ctor) |>.getD 0
-            if tag == 1 then pure (dt, [])
-            else if tag == 0 then
-              match args with
-              | #[.array byteVals, rest] =>
+  | steps+1, listVal => do
+    match listVal with
+    | .ctor g args =>
+      match decls.getByKey g with
+      | some (.constructor dt _) =>
+        if args.isEmpty then pure (dt, [])  -- Nil: no cell exists
+        else
+          match args with
+          | #[.pointer _ n] =>
+            let store ← getStore
+            match (if n == 0 then none else store.getByIdx (n - 1)) with
+            | none => throwErr s!"unconstrainedBigUintDivMod: invalid pointer {n}"
+            | some (vs, _) =>
+              match (vs[0]? : Option Value) with
+              | some (.tuple #[.array byteVals, rest]) =>
                 let bytes ← byteVals.mapM fun bv =>
                   match bv with
                   | .field b =>
@@ -250,21 +251,20 @@ private def readLimbChainI (decls : Decls) :
                   let (_, restLimbs) ← readLimbChainI decls steps rest
                   pure (dt, bytes :: restLimbs)
                 else throwErr "unconstrainedBigUintDivMod: limb is not [U8; 8]"
-              | _ => throwErr "unconstrainedBigUintDivMod: malformed Cons node"
-            else
-              throwErr "unconstrainedBigUintDivMod: unexpected constructor tag"
-          | _ => throwErr s!"unconstrainedBigUintDivMod: unbound ctor {g}"
-        | _ => throwErr "unconstrainedBigUintDivMod: node is not a constructor"
-    | _ => throwErr "unconstrainedBigUintDivMod: input is not a pointer"
+              | _ => throwErr "unconstrainedBigUintDivMod: malformed Cons cell"
+          | _ => throwErr "unconstrainedBigUintDivMod: malformed Cons value"
+      | _ => throwErr s!"unconstrainedBigUintDivMod: unbound ctor {g}"
+    | _ => throwErr "unconstrainedBigUintDivMod: input is not a list value"
 
 /-- Build a limb chain from head-first `limbs` (Nil first, limbs in
 reverse — same allocation order as the Rust builder). -/
 private def buildLimbChainI (consG nilG : Global) :
     List (Array G) → InterpM Value
-  | [] => storeValueI (.ctor nilG #[])
+  | [] => pure (.ctor nilG #[])  -- Nil IS the value; nothing is stored
   | limb :: rest => do
-    let restPtr ← buildLimbChainI consG nilG rest
-    storeValueI (.ctor consG #[.array (limb.map .field), restPtr])
+    let restVal ← buildLimbChainI consG nilG rest
+    let cellPtr ← storeValueI (.tuple #[.array (limb.map .field), restVal])
+    pure (.ctor consG #[cellPtr])
 
 mutual
 
@@ -368,15 +368,15 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       let v ← interp decls bindings t
       let store ← getStore
       if let some idx := store.getIdxOf #[v] then
-        return .pointer 0 idx
+        return .pointer 0 (idx + 1)
       let idx := store.size
       modify fun s => { s with store := s.store.insert #[v] () }
-      return .pointer 0 idx
+      return .pointer 0 (idx + 1)
   | .load t => do
       match ← interp decls bindings t with
       | .pointer _ n =>
           let store ← getStore
-          match store.getByIdx n with
+          match (if n == 0 then none else store.getByIdx (n - 1)) with
           | some (vs, _) => return vs[0]!
           | none         => throwErr s!"load: invalid pointer {n}"
       | _ => throwErr "load: expected pointer"
@@ -481,7 +481,9 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       let bound := (← getStore).size + 1
       let (dt, aLimbs) ← readLimbChainI decls bound aPtr
       let (_, bLimbs) ← readLimbChainI decls bound bPtr
-      match dt.constructors[0]?, dt.constructors[1]? with
+      -- Identify Cons/Nil by shape (nullary = Nil), not declaration order.
+      match dt.constructors.find? (!·.argTypes.isEmpty),
+            dt.constructors.find? (·.argTypes.isEmpty) with
       | some cons, some nil =>
         let consG := dt.name.pushNamespace cons.nameHead
         let nilG := dt.name.pushNamespace nil.nameHead

Ix/Aiur/Semantics/BytecodeEval.lean

@@ -82,64 +82,68 @@ def readIdxs (st : EvalState) (vs : Array ValIdx) : Except BytecodeError (Array
 
 /-! ## Memory ops -/
 
-/-- Insert/retrieve at a specific width bucket; returns the insertion index. -/
+/-- Insert/retrieve at a specific width bucket; returns the 1-BASED pointer
+(insertion index + 1). Pointer 0 is reserved as the impossible (null)
+pointer — the memory circuit pins the first row's pointer to 1, so no
+valid store ever answers to 0 (mirrors `execute.rs`). -/
 def memStore (st : EvalState) (vals : Array G) : EvalState × Nat :=
   let width := vals.size
   let bucket := st.memory.getByKey width |>.getD default
   if let some idx := bucket.getIdxOf vals then
-    (st, idx)
+    (st, idx + 1)
   else
     let idx := bucket.size
     let newBucket := bucket.insert vals ()
     let newMem := st.memory.insert width newBucket
-    ({ st with memory := newMem }, idx)
+    ({ st with memory := newMem }, idx + 1)
 
-/-- Load from the width-`size` bucket at index `ptr`. -/
+/-- Load from the width-`size` bucket at 1-based pointer `ptr`; 0 is the
+reserved null pointer and never binds. -/
 def memLoad (st : EvalState) (size : Nat) (ptr : Nat) :
     Except BytecodeError (Array G) :=
-  match st.memory.getByKey size with
-  | none        => .error (.invalidPointer size ptr)
-  | some bucket =>
-    match bucket.getByIdx ptr with
+  match st.memory.getByKey size, ptr with
+  | none, _ | _, 0 => .error (.invalidPointer size ptr)
+  | some bucket, idx + 1 =>
+    match bucket.getByIdx idx with
     | some (vs, _) => .ok vs
     | none         => .error (.invalidPointer size ptr)
 
 /-! ## `List<U64>` limb chains (`unconstrainedBigUintDivMod`)
 
 Mirrors `read_klimbs_u64` / `build_klimbs_u64` in `crates/aiur/src/execute.rs`:
-nodes live in the width-10 memory bucket with the standard tagged-enum
-layout `[tag, byte0..byte7, next_ptr]` — tag 0 = Cons, tag 1 = Nil, bytes
-little-endian within the u64 limb. -/
+`List<U64>` is the niche enum `{ Nil, Cons(&(U64, List<U64>)) }` — the list
+value is one field element, 0 = Nil (no node stored), otherwise a pointer
+to the `(limb, tail)` cell in the width-9 bucket, `[byte0..byte7, tail]`.
+Bytes are little-endian within the u64 limb. -/
 
 /-- Walk a limb chain from `ptr`, returning the limbs head-first. `steps`
-bounds the walk: a chain longer than the width-10 bucket must revisit a
+bounds the walk: a chain longer than the width-9 bucket must revisit a
 pointer, i.e. a malformed cycle. -/
 def readLimbChain (st : EvalState) : Nat → Nat →
     Except BytecodeError (List (Array G))
   | 0, _ => .error .unconstrainedBigUintDivModFailed
   | steps+1, ptr => do
-    let vs ← memLoad st 10 ptr
-    match vs[0]?, vs[9]? with
-    | some tag, some next =>
-      if tag == 1 then pure []
-      else if tag == 0 then
-        let bytes := vs.extract 1 9
+    if ptr == 0 then pure []  -- Nil IS the zero list value; no node exists
+    else
+      let vs ← memLoad st 9 ptr
+      match vs[8]? with
+      | some next =>
+        let bytes := vs.extract 0 8
         if bytes.size == 8 && bytes.all (·.val < 256) then do
           let rest ← readLimbChain st steps next.val.toNat
           pure (bytes :: rest)
         else .error .unconstrainedBigUintDivModFailed
-      else .error .unconstrainedBigUintDivModFailed
-    | _, _ => .error .unconstrainedBigUintDivModFailed
+      | _ => .error .unconstrainedBigUintDivModFailed
 
 /-- Build a limb chain from head-first `limbs`, returning the head pointer.
 Same insertion order as the Rust builder (Nil first, then limbs in reverse),
 so freshly-created pointer indices agree; `memStore` content-dedups like
 `QueryMap` does. -/
 def buildLimbChain (st : EvalState) : List (Array G) → EvalState × Nat
-  | [] => memStore st (#[1] ++ Array.replicate 9 0)
+  | [] => (st, 0)  -- Nil IS the zero list value; nothing is stored
   | limb :: rest =>
     let (st', restPtr) := buildLimbChain st rest
-    memStore st' (#[0] ++ limb ++ #[.ofNat restPtr])
+    memStore st' (limb ++ #[.ofNat restPtr])
 
 def pushMap (st : EvalState) (g : G) : EvalState :=
   { st with map := st.map.push g }
@@ -350,7 +354,7 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
   | .unconstrainedBigUintDivMod a b => do
     let aPtr ← readIdx st a
     let bPtr ← readIdx st b
-    -- Walk bound: the width-10 bucket size plus one (see `readLimbChain`).
+    -- Walk bound: the width-9 bucket size plus one (see `readLimbChain`).
     let bound := (st.memory.getByKey 10 |>.map (·.size) |>.getD 0) + 1
     let aLimbs ← readLimbChain st bound aPtr.val.toNat
     let bLimbs ← readLimbChain st bound bPtr.val.toNat