diff --git a/Benchmarks/Blake3.lean b/Benchmarks/Blake3.lean
index c48fc387..5610e521 100644
--- a/Benchmarks/Blake3.lean
+++ b/Benchmarks/Blake3.lean
@@ -26,7 +26,9 @@ def blake3Bench : IO $ Array BenchReport := do
     | throw (IO.userError "Aiur function not found")
   let .ok decls := toplevel.checkAndSimplify
     | throw (IO.userError "Simplification failed")
-  let aiurSystem := Aiur.AiurSystem.build decls.compile commitmentParameters
+  let .ok bytecode := decls.compile
+    | throw (IO.userError "Compilation failed")
+  let aiurSystem := Aiur.AiurSystem.build bytecode commitmentParameters
 
   let mut benches := Array.emptyWithCapacity $ dataSizes.size * numHashesPerProof.size
   for dataSize in dataSizes do
diff --git a/Benchmarks/Sha256.lean b/Benchmarks/Sha256.lean
index 751a7e46..c619d767 100644
--- a/Benchmarks/Sha256.lean
+++ b/Benchmarks/Sha256.lean
@@ -26,7 +26,9 @@ def sha256Bench : IO $ Array BenchReport := do
     | throw (IO.userError "Aiur function not found")
   let .ok decls := toplevel.checkAndSimplify
     | throw (IO.userError "Simplification failed")
-  let aiurSystem := Aiur.AiurSystem.build decls.compile commitmentParameters
+  let .ok bytecode := decls.compile
+    | throw (IO.userError "Compilation failed")
+  let aiurSystem := Aiur.AiurSystem.build bytecode commitmentParameters
 
   let mut benches := Array.emptyWithCapacity $ dataSizes.size * numHashesPerProof.size
   for dataSize in dataSizes do
diff --git a/Ix/Aiur/Compile.lean b/Ix/Aiur/Compile.lean
index ef1469f5..3d6d5f5b 100644
--- a/Ix/Aiur/Compile.lean
+++ b/Ix/Aiur/Compile.lean
@@ -193,41 +193,49 @@ inductive Layout
 
 abbrev LayoutMap := Std.HashMap Global Layout
 
-def TypedDecls.layoutMap (decls : TypedDecls) : LayoutMap :=
-  let pass := fun (layoutMap, funcIdx, gadgetIdx) (_, v) => match v with
+def TypedDecls.layoutMap (decls : TypedDecls) : Except String LayoutMap := do
+  let pass := fun (layoutMap, funcIdx, gadgetIdx) (_, v) => do match v with
     | .dataType dataType =>
-      let dataTypeSize := dataType.size decls
+      let dataTypeSize ← dataType.size decls
       let layoutMap := layoutMap.insert dataType.name (.dataType { size := dataTypeSize })
-      let pass := fun (acc, index) constructor =>
-        let offsets := constructor.argTypes.foldl (init := #[0])
-          fun offsets typ => offsets.push (offsets[offsets.size - 1]! + typ.size decls)
+      let pass := fun (acc, index) constructor => do
+        let offsets ← constructor.argTypes.foldlM (init := #[0]) fun offsets typ => do
+          let typSyze ← typ.size decls
+          pure $ offsets.push (offsets[offsets.size - 1]! + typSyze)
         let decl := .constructor { size := dataTypeSize, offsets, index }
         let name := dataType.name.pushNamespace constructor.nameHead
-        (acc.insert name decl, index + 1)
-      let (layoutMap, _) := dataType.constructors.foldl (init := (layoutMap, 0)) pass
-      (layoutMap, funcIdx, gadgetIdx)
+        pure (acc.insert name decl, index + 1)
+      let (layoutMap, _) ← dataType.constructors.foldlM pass (layoutMap, 0)
+      pure (layoutMap, funcIdx, gadgetIdx)
     | .function function =>
-      let inputSize := function.inputs.foldl (init := 0) fun acc (_, typ) => acc + typ.size decls
-      let outputSize := function.output.size decls
-      let offsets := function.inputs.foldl (init := #[0])
-        fun offsets (_, typ) => offsets.push (offsets[offsets.size - 1]! + typ.size decls)
+      let inputSize ← function.inputs.foldlM (init := 0) fun acc (_, typ) => do
+        let typSize ← typ.size decls
+        pure $ acc + typSize
+      let outputSize ← function.output.size decls
+      let offsets ← function.inputs.foldlM (init := #[0]) fun offsets (_, typ) => do
+        let typSyze ← typ.size decls
+        pure $ offsets.push (offsets[offsets.size - 1]! + typSyze)
       let layoutMap := layoutMap.insert function.name $
         .function { index := funcIdx, inputSize, outputSize, offsets }
-      (layoutMap, funcIdx + 1, gadgetIdx)
-    | .constructor .. => (layoutMap, funcIdx, gadgetIdx)
-  let (layoutMap, _) := decls.foldl pass ({}, 0, 0)
-  layoutMap
-
-def typSize (layoutMap : LayoutMap) : Typ → Nat
-| .unit => 0
-| .field .. => 1
-| .pointer .. => 1
-| .function .. => 1
-| .tuple ts => ts.foldl (fun acc t => acc + typSize layoutMap t) 0
-| .array typ n => n * typSize layoutMap typ
+      pure (layoutMap, funcIdx + 1, gadgetIdx)
+    | .constructor .. => pure (layoutMap, funcIdx, gadgetIdx)
+  let (layoutMap, _) ← decls.foldlM pass ({}, 0, 0)
+  pure layoutMap
+
+def typSize (layoutMap : LayoutMap) : Typ → Except String Nat
+| .unit => pure 0
+| .field .. => pure 1
+| .pointer .. => pure 1
+| .function .. => pure 1
+| .tuple ts => ts.foldlM (init := 0) fun acc t => do
+  let tSize ← typSize layoutMap t
+  pure $ acc + tSize
+| .array typ n => do
+  let size ← typSize layoutMap typ
+  pure $ n * size
 | .dataType g => match layoutMap[g]? with
-  | some (.dataType layout) => layout.size
-  | _ => unreachable!
+  | some (.dataType layout) => pure layout.size
+  | _ => throw "Impossible case"
 
 structure CompilerState where
   valIdx : Bytecode.ValIdx
@@ -235,28 +243,30 @@ structure CompilerState where
   selIdx : Bytecode.SelIdx
   deriving Inhabited
 
-def pushOp (op : Bytecode.Op) (size : Nat := 1) : StateM CompilerState (Array Bytecode.ValIdx) :=
+abbrev CompileM := EStateM String CompilerState
+
+def pushOp (op : Bytecode.Op) (size : Nat := 1) : CompileM (Array Bytecode.ValIdx) :=
   modifyGet (fun s =>
     let valIdx := s.valIdx
     let ops := s.ops
     (Array.range' valIdx size, { s with valIdx := valIdx + size, ops := ops.push op}))
 
-def extractOps : StateM CompilerState (Array Bytecode.Op) :=
+def extractOps : CompileM (Array Bytecode.Op) :=
   modifyGet fun s => (s.ops, {s with ops := #[]})
 
 partial def toIndex
  (layoutMap : LayoutMap)
  (bindings : Std.HashMap Local (Array Bytecode.ValIdx))
- (term : TypedTerm) : StateM CompilerState (Array Bytecode.ValIdx) :=
+ (term : TypedTerm) : CompileM (Array Bytecode.ValIdx) :=
   match term.inner with
   -- | .unsafeCast inner castTyp =>
   --   if typSize layoutMap castTyp != typSize layoutMap term.typ then
-  --     panic! "Impossible cast"
+  --     throw "Impossible cast"
   --   else
   --     toIndex layoutMap bindings (.mk term.typ inner)
   | .unit => pure #[]
-  | .ret .. => panic! "Should not happen after typechecking"
-  | .match .. => panic! "Non-tail `match` not yet implemented"
+  | .ret .. => throw "Should not happen after typechecking"
+  | .match .. => throw "Non-tail `match` not yet implemented"
   | .var name => pure bindings[name]!
   | .ref name => match layoutMap[name]! with
     | .function layout => do
@@ -270,7 +280,7 @@ partial def toIndex
         pure $ index ++ Array.replicate (size - index.size) padding
       else
         pure index
-    | _ => panic! "Should not happen after typechecking"
+    | _ => throw "Should not happen after typechecking"
   | .data (.field g) => pushOp (Bytecode.Op.const g)
   | .data (.tuple terms) | .data (.array terms) =>
       terms.foldlM (init := #[]) fun acc arg => do
@@ -278,7 +288,7 @@ partial def toIndex
   | .let (.var var) val bod => do
     let val ← toIndex layoutMap bindings val
     toIndex layoutMap (bindings.insert var val) bod
-  | .let .. => panic! "Should not happen after simplifying"
+  | .let .. => throw "Should not happen after simplifying"
   | .add a b => do
     let a ← expectIdx a
     let b ← expectIdx b
@@ -296,7 +306,7 @@ partial def toIndex
     pushOp (.eqZero a)
   | .app name@(⟨.str .anonymous unqualifiedName⟩) args =>
     match bindings.get? (.str unqualifiedName) with
-    | some _ => panic! "Dynamic calls not yet implemented"
+    | some _ => throw "Dynamic calls not yet implemented"
     | none => match layoutMap[name]! with
       | .function layout => do
         let args ← buildArgs args
@@ -310,7 +320,7 @@ partial def toIndex
           pure $ index ++ Array.replicate (size - index.size) padding
         else
           pure index
-      | _ => panic! "Should not happen after typechecking"
+      | _ => throw "Should not happen after typechecking"
   | .app name args => match layoutMap[name]! with
     | .function layout => do
       let args ← buildArgs args
@@ -324,49 +334,60 @@ partial def toIndex
         pure $ index ++ Array.replicate (size - index.size) padding
       else
         pure index
-    | _ => panic! "Should not happen after typechecking"
+    | _ => throw "Should not happen after typechecking"
   -- | .preimg name@(⟨.str .anonymous unqualifiedName⟩) out =>
   --   match bindings.get? (.str unqualifiedName) with
-  --   | some _ => panic! "dynamic preimage not yet implemented"
+  --   | some _ => throw "dynamic preimage not yet implemented"
   --   | none => match layoutMap.get' name with
   --     | .function layout => do
   --       let out ← toIndex layoutMap bindings out
   --       pushOp (Bytecode.Op.preimg layout.index out layout.inputSize) layout.inputSize
-  --     | _ => panic! "should not happen after typechecking"
+  --     | _ => throw "should not happen after typechecking"
   -- | .preimg name out => match layoutMap.get' name with
   --   | .function layout => do
   --     let out ← toIndex layoutMap bindings out
   --     pushOp (Bytecode.Op.preimg layout.index out layout.inputSize) layout.inputSize
-  --   | _ => panic! "should not happen after typechecking"
+  --   | _ => throw "should not happen after typechecking"
   | .proj arg i => do
-    let typs := match (arg.typ, arg.escapes) with
-      | (.tuple typs, false) => typs
-      | _ => panic! "Should not happen after typechecking"
-    let offset := (typs.extract 0 i).foldl (init := 0)
-      fun acc typ => typSize layoutMap typ + acc
+    let typs ← match (arg.typ, arg.escapes) with
+      | (.tuple typs, false) => pure typs
+      | _ => throw "Should not happen after typechecking"
+    let offset ← (typs.extract 0 i).foldlM (init := 0) fun acc typ => do
+      let typLen ← match typSize layoutMap typ with
+        | .error e => throw e
+        | .ok len => pure len
+      pure $ typLen + acc
     let arg ← toIndex layoutMap bindings arg
-    let length := typSize layoutMap typs[i]!
-    pure $ arg.extract offset (offset + length)
+    let iLen ← match typSize layoutMap typs[i]! with
+      | .error e => throw e
+      | .ok len => pure len
+    pure $ arg.extract offset (offset + iLen)
   | .get arr i => do
-    let eltTyp := match (arr.typ, arr.escapes) with
-      | (.array typ _, false) => typ
-      | _ => panic! "Should not happen after typechecking"
-    let eltSize := typSize layoutMap eltTyp
+    let eltTyp ← match (arr.typ, arr.escapes) with
+      | (.array typ _, false) => pure typ
+      | _ => throw "Should not happen after typechecking"
+    let eltSize ← match typSize layoutMap eltTyp with
+      | .error e => throw e
+      | .ok len => pure len
     let offset := i * eltSize
     let arr ← toIndex layoutMap bindings arr
     pure $ arr.extract offset (offset + eltSize)
   | .slice arr i j => do
-    let eltTyp := match (arr.typ, arr.escapes) with
-      | (.array typ _, false) => typ
-      | _ => panic! "Should not happen after typechecking"
-    let eltSize := typSize layoutMap eltTyp
+    let eltTyp ← match (arr.typ, arr.escapes) with
+      | (.array typ _, false) => pure typ
+      | _ => throw "Should not happen after typechecking"
+    let eltSize ← match typSize layoutMap eltTyp with
+      | .error e => throw e
+      | .ok len => pure len
     let arr ← toIndex layoutMap bindings arr
     pure $ arr.extract (i * eltSize) (j * eltSize)
   | .set arr i val => do
-    let eltTyp := match (arr.typ, arr.escapes) with
-      | (.array typ _, false) => typ
-      | _ => panic! "Should not happen after typechecking"
-    let eltSize := typSize layoutMap eltTyp
+    let eltTyp ← match (arr.typ, arr.escapes) with
+      | (.array typ _, false) => pure typ
+      | _ => throw "Should not happen after typechecking"
+    let eltSize ← match typSize layoutMap eltTyp with
+      | .error e => throw e
+      | .ok len => pure len
     let arr ← toIndex layoutMap bindings arr
     let left := arr.extract 0 (i * eltSize)
     let val ← toIndex layoutMap bindings val
@@ -376,9 +397,11 @@ partial def toIndex
     let args ← toIndex layoutMap bindings arg
     pushOp (.store args)
   | .load ptr => do
-    let size := match (ptr.typ, ptr.escapes) with
-    | (.pointer typ, false) => typSize layoutMap typ
-    | _ => unreachable!
+    let size ← match (ptr.typ, ptr.escapes) with
+    | (.pointer typ, false) => match typSize layoutMap typ with
+      | .error e => throw e
+      | .ok len => pure len
+    | _ => throw "Impossible case"
     let ptr ← expectIdx ptr
     pushOp (.load size ptr) size
   | .ptrVal ptr => toIndex layoutMap bindings ptr
@@ -455,7 +478,7 @@ partial def toIndex
       if h : idxs.size = 1 then
         have : 0 < idxs.size := by simp only [h, Nat.lt_add_one]
         pure idxs[0]
-      else panic! "Term is not of size 1"
+      else throw "Term is not of size 1"
 
 mutual
 
@@ -464,11 +487,11 @@ partial def TypedTerm.compile
  (returnTyp : Typ)
  (layoutMap : LayoutMap)
  (bindings : Std.HashMap Local (Array Bytecode.ValIdx))
-: StateM CompilerState Bytecode.Block := match term.inner with
+: CompileM Bytecode.Block := match term.inner with
   | .let (.var var) val bod => do
     let val ← toIndex layoutMap bindings val
     bod.compile returnTyp layoutMap (bindings.insert var val)
-  | .let .. => panic! "Should not happen after simplifying"
+  | .let .. => throw "Should not happen after simplifying"
   | .debug label term ret => do
     let term ← term.mapM (toIndex layoutMap bindings)
     modify fun stt => { stt with ops := stt.ops.push (.debug label term) }
@@ -478,34 +501,38 @@ partial def TypedTerm.compile
     -- Also do this for tuple-like and array-like (one constructor only) datatypes
     | .tuple typs => match cases with
       | [(.tuple vars, branch)] => do
-        let bindArgs bindings pats typs idxs :=
-          let (bindings, _) := (pats.zip typs).foldl (init := (bindings, 0))
+        let bindArgs bindings pats typs idxs := do
+          let (bindings, _) ← (pats.zip typs).foldlM (init := (bindings, 0))
             fun (bindings, offset) (pat, typ) => match pat with
-              | .var var =>
-                let len := typSize layoutMap typ
+              | .var var => do
+                let len ← match typSize layoutMap typ with
+                  | .error e => throw e
+                  | .ok len => pure len
                 let newOffset := offset + len
-                (bindings.insert var (idxs.extract offset newOffset), newOffset)
-              | _ => panic! "Should not happen after simplification"
-          bindings
+                pure (bindings.insert var (idxs.extract offset newOffset), newOffset)
+              | _ => throw "Should not happen after simplification"
+          pure bindings
         let idxs ← toIndex layoutMap bindings term
-        let bindings := bindArgs bindings vars typs idxs
+        let bindings ← bindArgs bindings vars typs idxs
         branch.compile returnTyp layoutMap bindings
-      | _ => unreachable!
+      | _ => throw "Impossible case"
     | .array typ _ => match cases with
       | [(.array vars, branch)] => do
-        let bindArgs bindings pats idxs :=
-          let len := typSize layoutMap typ
-          let (bindings, _) := pats.foldl (init := (bindings, 0))
+        let bindArgs bindings pats idxs := do
+          let len ← match typSize layoutMap typ with
+            | .error e => throw e
+            | .ok len => pure len
+          let (bindings, _) ← pats.foldlM (init := (bindings, 0))
             fun (bindings, offset) pat => match pat with
               | .var var =>
                 let newOffset := offset + len
-                (bindings.insert var (idxs.extract offset newOffset), newOffset)
-              | _ => panic! "Should not happen after simplification"
-          bindings
+                pure (bindings.insert var (idxs.extract offset newOffset), newOffset)
+              | _ => throw "Should not happen after simplification"
+          pure bindings
         let idxs ← toIndex layoutMap bindings term
-        let bindings := bindArgs bindings vars idxs
+        let bindings ← bindArgs bindings vars idxs
         branch.compile returnTyp layoutMap bindings
-      | _ => unreachable!
+      | _ => throw "Impossible case"
     | _ => do
       let idxs ← toIndex layoutMap bindings term
       let ops ← extractOps
@@ -539,7 +566,7 @@ partial def addCase
   (idxs : Array Bytecode.ValIdx)
 : (Array (G × Bytecode.Block) × Option Bytecode.Block) →
   (Pattern × TypedTerm) →
-  StateM CompilerState (Array (G × Bytecode.Block) × Option Bytecode.Block) := fun (cases, default) (pat, term) =>
+  CompileM (Array (G × Bytecode.Block) × Option Bytecode.Block) := fun (cases, default) (pat, term) =>
   -- If simplified, only one default will exist, and it will appear at the end of the match
   assert! default.isNone
   match pat with
@@ -551,24 +578,24 @@ partial def addCase
     pure (cases', default)
   | .ref global pats => do
     let layout := layoutMap[global]!
-    let (index, offsets) := match layout with
-    | .function layout => (layout.index, layout.offsets)
-    | .constructor layout => (layout.index, layout.offsets)
+    let (index, offsets) ← match layout with
+    | .function layout => pure (layout.index, layout.offsets)
+    | .constructor layout => pure (layout.index, layout.offsets)
     | .dataType _
-    | .gadget _ => panic! "Impossible after typechecking"
-    let bindArgs bindings pats offsets idxs :=
+    | .gadget _ => throw "Impossible after typechecking"
+    let bindArgs bindings pats offsets idxs := do
       let n := pats.length
-      let bindings := (List.range n).foldl (init := bindings) fun bindings i =>
+      let bindings ← (List.range n).foldlM (init := bindings) fun bindings i =>
         let pat := pats[i]!
         -- the `+ 1` is to account for the tag
         let offset := offsets[i]! + 1
         let next_offset := offsets[(i + 1)]! + 1
         match pat with
         | .var var =>
-          bindings.insert var (idxs.extract offset next_offset)
-        | _ => panic! "Should not happen after simplification"
-      bindings
-    let bindings := bindArgs bindings pats offsets idxs
+          pure $ bindings.insert var (idxs.extract offset next_offset)
+        | _ => throw "Should not happen after simplification"
+      pure bindings
+    let bindings ← bindArgs bindings pats offsets idxs
     let initState ← get
     let term ← term.compile returnTyp layoutMap bindings
     set { initState with selIdx := (← get).selIdx }
@@ -579,36 +606,40 @@ partial def addCase
     let term ← term.compile returnTyp layoutMap bindings
     set { initState with selIdx := (← get).selIdx }
     pure (cases, .some term)
-  | _ => unreachable!
+  | _ => throw "Impossible case"
 
 end
 
 def TypedFunction.compile (decls : TypedDecls) (layoutMap : LayoutMap) (f : TypedFunction) :
-    Bytecode.Block × Bytecode.LayoutMState :=
-  let (inputSize, _outputSize) := match layoutMap[f.name]? with
-    | some (.function layout) => (layout.inputSize, layout.outputSize)
-    | _ => panic! s!"`{f.name}` should be a function"
-  let (valIdx, bindings) := f.inputs.foldl (init := (0, default))
-    fun (valIdx, bindings) (arg, typ) =>
-      let len := typSize layoutMap typ
+    Except String (Bytecode.Block × Bytecode.LayoutMState) := do
+  let (inputSize, _outputSize) ← match layoutMap[f.name]? with
+    | some (.function layout) => pure (layout.inputSize, layout.outputSize)
+    | _ => throw s!"`{f.name}` should be a function"
+  let (valIdx, bindings) ← f.inputs.foldlM (init := (0, default))
+    fun (valIdx, bindings) (arg, typ) => do
+      let len ← match typSize layoutMap typ with
+        | .error e => throw e
+        | .ok len => pure len
       let indices := Array.range' valIdx len
-      (valIdx + len, bindings.insert arg indices)
+      pure (valIdx + len, bindings.insert arg indices)
   let state := { valIdx, selIdx := 0, ops := #[] }
-  let body := f.body.compile f.output layoutMap bindings |>.run' state
-  let (_, layoutMState) := Bytecode.blockLayout body |>.run decls (.new inputSize)
-  (body, layoutMState)
-
-def TypedDecls.compile (decls : TypedDecls) : Bytecode.Toplevel :=
-  let layout := decls.layoutMap
+  match f.body.compile f.output layoutMap bindings |>.run state with
+  | .error e _ => throw e
+  | .ok body _ =>
+    let (_, layoutMState) := Bytecode.blockLayout body |>.run decls (.new inputSize)
+    pure (body, layoutMState)
+
+def TypedDecls.compile (decls : TypedDecls) : Except String Bytecode.Toplevel := do
+  let layout ← decls.layoutMap
   let initMemSizes : Bytecode.MemSizes := .empty
-  let (functions, memSizes) := decls.foldl (init := (#[], initMemSizes))
+  let (functions, memSizes) ← decls.foldlM (init := (#[], initMemSizes))
     fun acc@(functions, memSizes) (_, decl) => match decl with
-      | .function function =>
-        let (body, layoutMState) := function.compile decls layout
+      | .function function => do
+        let (body, layoutMState) ← function.compile decls layout
         let function := ⟨body, layoutMState.functionLayout, function.unconstrained⟩
         let memSizes := layoutMState.memSizes.fold (·.insert ·) memSizes
-        (functions.push function, memSizes)
-      | _ => acc
-  ⟨functions, memSizes.toArray⟩
+        pure (functions.push function, memSizes)
+      | _ => pure acc
+  pure ⟨functions, memSizes.toArray⟩
 
 end Aiur
diff --git a/Ix/Aiur/Term.lean b/Ix/Aiur/Term.lean
index 71061824..d3ca942a 100644
--- a/Ix/Aiur/Term.lean
+++ b/Ix/Aiur/Term.lean
@@ -238,28 +238,37 @@ mutual
 
 open Std (HashSet)
 
-partial def Typ.size (decls : TypedDecls) (visited : HashSet Global := {}) : Typ → Nat
-  | .unit => 0
-  | .field .. => 1
-  | .pointer .. => 1
-  | .function .. => 1
-  | .tuple ts => ts.foldl (init := 0) fun acc t => acc + t.size decls visited
-  | .array t n => n * t.size decls visited
+partial def Typ.size (decls : TypedDecls) (visited : HashSet Global := {}) :
+    Typ → Except String Nat
+  | .unit => pure 0
+  | .field .. => pure 1
+  | .pointer .. => pure 1
+  | .function .. => pure 1
+  | .tuple ts => ts.foldlM (init := 0) fun acc t => do
+    let tSize ← t.size decls visited
+    pure $ acc + tSize
+  | .array t n => do
+    let tSize ← t.size decls visited
+    pure $ n * tSize
   | .dataType g => match decls.getByKey g with
     | some (.dataType data) => data.size decls visited
-    | _ => panic! "impossible case"
+    | _ => throw s!"Datatype not found: `{g}`"
 
-partial def Constructor.size (decls : TypedDecls) (visited : HashSet Global := {}) (c : Constructor) : Nat :=
-  c.argTypes.foldl (fun acc t => acc + t.size decls visited) 0
+partial def Constructor.size (decls : TypedDecls) (visited : HashSet Global := {})
+    (c : Constructor) : Except String Nat :=
+  c.argTypes.foldlM (init := 0) fun acc t => do
+    let tSize ← t.size decls visited
+    pure $ acc + tSize
 
-partial def DataType.size (dt : DataType) (decls : TypedDecls) (visited : HashSet Global := {}) : Nat :=
+partial def DataType.size (dt : DataType) (decls : TypedDecls)
+    (visited : HashSet Global := {}) : Except String Nat :=
   if visited.contains dt.name then
-    panic! s!"cycle detected at datatype `{dt.name}`"
-  else
+    throw s!"Cycle detected at datatype `{dt.name}`"
+  else do
     let visited := visited.insert dt.name
-    let ctorSizes := dt.constructors.map (Constructor.size decls visited)
+    let ctorSizes ← dt.constructors.mapM (Constructor.size decls visited)
     let maxFields := ctorSizes.foldl max 0
-    maxFields + 1
+    pure $ maxFields + 1
 end
 
 end Aiur
diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index 319c8b1e..e568ba6c 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -3,6 +3,7 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixon := ⟦
+  -- Expression type
   enum Expr {
     Srt([G; 8]),
     Var([G; 8]),
@@ -17,6 +18,147 @@ def ixon := ⟦
     Let([G; 8], &Expr, &Expr, &Expr),
     Share([G; 8])
   }
+
+  -- Universe levels
+  enum Univ {
+    Zero,
+    Succ(&Univ),
+    Max(&Univ, &Univ),
+    IMax(&Univ, &Univ),
+    Var([G; 8])
+  }
+
+  enum ExprList {
+    Cons(&Expr, &ExprList),
+    Nil
+  }
+
+  enum UnivList {
+    Cons(&Univ, &UnivList),
+    Nil
+  }
+
+  enum AddressList {
+    Cons([G; 32], &AddressList),
+    Nil
+  }
+
+  -- Definition kind
+  enum DefKind {
+    Definition,
+    Opaque,
+    Theorem
+  }
+
+  -- Definition safety
+  enum DefinitionSafety {
+    Unsafe,
+    Safe,
+    Partial
+  }
+
+  -- Quotient kind
+  enum QuotKind {
+    Typ,
+    Ctor,
+    Lift,
+    Ind
+  }
+
+  -- Definition: (kind, safety, lvls, typ, value)
+  enum Definition {
+    Mk(DefKind, DefinitionSafety, [G; 8], &Expr, &Expr)
+  }
+
+  -- RecursorRule: (fields, rhs)
+  enum RecursorRule {
+    Mk([G; 8], &Expr)
+  }
+
+  enum RecursorRuleList {
+    Cons(RecursorRule, &RecursorRuleList),
+    Nil
+  }
+
+  -- Recursor: (k, is_unsafe, lvls, params, indices, motives, minors, typ, rules)
+  enum Recursor {
+    Mk(G, G, [G; 8], [G; 8], [G; 8], [G; 8], [G; 8], &Expr, &RecursorRuleList)
+  }
+
+  -- Axiom: (is_unsafe, lvls, typ)
+  enum Axiom {
+    Mk(G, [G; 8], &Expr)
+  }
+
+  -- Quotient: (kind, lvls, typ)
+  enum Quotient {
+    Mk(QuotKind, [G; 8], &Expr)
+  }
+
+  -- Constructor: (is_unsafe, lvls, cidx, params, fields, typ)
+  enum Constructor {
+    Mk(G, [G; 8], [G; 8], [G; 8], [G; 8], &Expr)
+  }
+
+  enum ConstructorList {
+    Cons(Constructor, &ConstructorList),
+    Nil
+  }
+
+  -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
+  enum Inductive {
+    Mk(G, G, G, [G; 8], [G; 8], [G; 8], [G; 8], &Expr, &ConstructorList)
+  }
+
+  -- InductiveProj: (idx, block_address)
+  enum InductiveProj {
+    Mk([G; 8], [G; 32])
+  }
+
+  -- ConstructorProj: (idx, cidx, block_address)
+  enum ConstructorProj {
+    Mk([G; 8], [G; 8], [G; 32])
+  }
+
+  -- RecursorProj: (idx, block_address)
+  enum RecursorProj {
+    Mk([G; 8], [G; 32])
+  }
+
+  -- DefinitionProj: (idx, block_address)
+  enum DefinitionProj {
+    Mk([G; 8], [G; 32])
+  }
+
+  -- MutConst: constants within a mutual block
+  enum MutConst {
+    Defn(Definition),
+    Indc(Inductive),
+    Recr(Recursor)
+  }
+
+  enum MutConstList {
+    Cons(MutConst, &MutConstList),
+    Nil
+  }
+
+  -- ConstantInfo: the variant/payload of a constant
+  enum ConstantInfo {
+    Defn(Definition),
+    Recr(Recursor),
+    Axio(Axiom),
+    Quot(Quotient),
+    CPrj(ConstructorProj),
+    RPrj(RecursorProj),
+    IPrj(InductiveProj),
+    DPrj(DefinitionProj),
+    Muts(&MutConstList)
+  }
+
+  -- Constant: (info, sharing, refs, univs)
+  enum Constant {
+    Mk(ConstantInfo, &ExprList, &AddressList, &UnivList)
+  }
 ⟧
 
 end IxVM
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index e2fda205..fa605824 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -3,127 +3,99 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixonSerialize := ⟦
-  fn put_expr(expr: Expr) -> ByteStream {
+  fn put_expr(expr: Expr, rest: ByteStream) -> ByteStream {
     match expr {
       -- Srt: Tag4(0x0, univ_idx)
-      Expr.Srt(univ_idx) => put_tag4(0x0, univ_idx),
+      Expr.Srt(univ_idx) => put_tag4(0x0, univ_idx, rest),
 
       -- Var: Tag4(0x1, idx)
-      Expr.Var(idx) => put_tag4(0x1, idx),
+      Expr.Var(idx) => put_tag4(0x1, idx, rest),
 
       -- Ref: Tag4(0x2, len) + Tag0(ref_idx) + univ_list
       Expr.Ref(ref_idx, &univ_list) =>
         let len = u64_list_length(univ_list);
-        let tag = put_tag4(0x2, len);
-        let ref_bytes = put_tag0(ref_idx);
-        let univ_bytes = put_u64_list(univ_list);
-        byte_stream_concat(tag, byte_stream_concat(ref_bytes, univ_bytes)),
+        put_tag4(0x2, len, put_tag0(ref_idx, put_u64_list(univ_list, rest))),
 
       -- Rec: Tag4(0x3, len) + Tag0(rec_idx) + univ_list
       Expr.Rec(rec_idx, &univ_list) =>
         let len = u64_list_length(univ_list);
-        let tag = put_tag4(0x3, len);
-        let rec_bytes = put_tag0(rec_idx);
-        let univ_bytes = put_u64_list(univ_list);
-        byte_stream_concat(tag, byte_stream_concat(rec_bytes, univ_bytes)),
+        put_tag4(0x3, len, put_tag0(rec_idx, put_u64_list(univ_list, rest))),
 
       -- Prj: Tag4(0x4, field_idx) + Tag0(type_ref_idx) + put_expr(val)
       Expr.Prj(type_ref_idx, field_idx, &val) =>
-        let tag = put_tag4(0x4, field_idx);
-        let type_bytes = put_tag0(type_ref_idx);
-        let val_bytes = put_expr(val);
-        byte_stream_concat(tag, byte_stream_concat(type_bytes, val_bytes)),
+        put_tag4(0x4, field_idx, put_tag0(type_ref_idx, put_expr(val, rest))),
 
       -- Str: Tag4(0x5, ref_idx)
-      Expr.Str(ref_idx) => put_tag4(0x5, ref_idx),
+      Expr.Str(ref_idx) => put_tag4(0x5, ref_idx, rest),
 
       -- Nat: Tag4(0x6, ref_idx)
-      Expr.Nat(ref_idx) => put_tag4(0x6, ref_idx),
+      Expr.Nat(ref_idx) => put_tag4(0x6, ref_idx, rest),
 
       -- App: Tag4(0x7, count) + telescope
       Expr.App(_, _) =>
         let count = app_telescope_count(expr);
-        let tag = put_tag4(0x7, count);
-        let telescope = put_app_telescope(expr);
-        byte_stream_concat(tag, telescope),
+        put_tag4(0x7, count, put_app_telescope(expr, rest)),
 
       -- Lam: Tag4(0x8, count) + telescope
       Expr.Lam(_, _) =>
         let count = lam_telescope_count(expr);
-        let tag = put_tag4(0x8, count);
-        let telescope = put_lam_telescope(expr);
-        byte_stream_concat(tag, telescope),
+        put_tag4(0x8, count, put_lam_telescope(expr, rest)),
 
       -- All: Tag4(0x9, count) + telescope
       Expr.All(_, _) =>
         let count = all_telescope_count(expr);
-        let tag = put_tag4(0x9, count);
-        let telescope = put_all_telescope(expr);
-        byte_stream_concat(tag, telescope),
+        put_tag4(0x9, count, put_all_telescope(expr, rest)),
 
       -- Let: Tag4(0xA, non_dep) + put_expr(ty) + put_expr(val) + put_expr(body)
       -- non_dep: 0 for dependent, 1 for non-dependent
       Expr.Let(non_dep, &ty, &val, &body) =>
-        let tag = put_tag4(0xA, non_dep);
-        let ty_bytes = put_expr(ty);
-        let val_bytes = put_expr(val);
-        let body_bytes = put_expr(body);
-        byte_stream_concat(
-          tag,
-          byte_stream_concat(
-            ty_bytes,
-            byte_stream_concat(val_bytes, body_bytes)
-          )
-        ),
+        put_tag4(0xA, non_dep, put_expr(ty, put_expr(val, put_expr(body, rest)))),
 
       -- Share: Tag4(0xB, idx)
-      Expr.Share(idx) => put_tag4(0xB, idx),
+      Expr.Share(idx) => put_tag4(0xB, idx, rest),
     }
   }
 
-  fn put_u64_le(bs: [G; 8], num_bytes: G) -> ByteStream {
+  fn put_u64_le(bs: [G; 8], num_bytes: G, rest: ByteStream) -> ByteStream {
     match num_bytes {
-      0 => ByteStream.Nil,
+      0 => rest,
       _ =>
         let [b1, b2, b3, b4, b5, b6, b7, b8] = bs;
-        let rest = [b2, b3, b4, b5, b6, b7, b8, 0];
-        ByteStream.Cons(b1, store(put_u64_le(rest, num_bytes - 1))),
+        let rest_shifted = [b2, b3, b4, b5, b6, b7, b8, 0];
+        ByteStream.Cons(b1, store(put_u64_le(rest_shifted, num_bytes - 1, rest))),
     }
   }
 
-  fn put_tag0(bs: [G; 8]) -> ByteStream {
+  fn put_tag0(bs: [G; 8], rest: ByteStream) -> ByteStream {
     let byte_count = u64_byte_count(bs);
     let small = u8_less_than(bs[0], 128);
     match (byte_count, small) {
-      (1, 1) => ByteStream.Cons(bs[0], store(ByteStream.Nil)),
+      (1, 1) => ByteStream.Cons(bs[0], store(rest)),
       _ =>
         let head = 128 + (byte_count - 1);
-        ByteStream.Cons(head, store(put_u64_le(bs, byte_count))),
+        ByteStream.Cons(head, store(put_u64_le(bs, byte_count, rest))),
     }
   }
 
-  fn put_tag4(flag: G, bs: [G; 8]) -> ByteStream {
+  fn put_tag4(flag: G, bs: [G; 8], rest: ByteStream) -> ByteStream {
     let byte_count = u64_byte_count(bs);
     let small = u8_less_than(bs[0], 8);
     match (byte_count, small) {
       (1, 1) =>
         let head = flag * 16 + bs[0];
-        ByteStream.Cons(head, store(ByteStream.Nil)),
+        ByteStream.Cons(head, store(rest)),
       _ =>
         let head = flag * 16 + 8 + (byte_count - 1);
-        let bs_bytes = put_u64_le(bs, byte_count);
-        ByteStream.Cons(head, store(bs_bytes)),
+        ByteStream.Cons(head, store(put_u64_le(bs, byte_count, rest))),
     }
   }
 
   -- Serialize field list (each element as Tag0)
-  fn put_u64_list(list: U64List) -> ByteStream {
+  fn put_u64_list(list: U64List, rest: ByteStream) -> ByteStream {
     match list {
-      U64List.Nil => ByteStream.Nil,
-      U64List.Cons(idx, rest) =>
-        let idx_bytes = put_tag0(idx);
-        let rest_bytes = put_u64_list(load(rest));
-        byte_stream_concat(idx_bytes, rest_bytes),
+      U64List.Nil => rest,
+      U64List.Cons(idx, rest_list) =>
+        put_tag0(idx, put_u64_list(load(rest_list), rest)),
     }
   }
 
@@ -152,35 +124,434 @@ def ixonSerialize := ⟦
   }
 
   -- Serialize App telescope body (function, then all args in order)
-  fn put_app_telescope(expr: Expr) -> ByteStream {
+  fn put_app_telescope(expr: Expr, rest: ByteStream) -> ByteStream {
     match expr {
       Expr.App(&func, &arg) =>
-        let func_bytes = put_app_telescope(func);
-        let arg_bytes = put_expr(arg);
-        byte_stream_concat(func_bytes, arg_bytes),
-      _ => put_expr(expr),
+        put_app_telescope(func, put_expr(arg, rest)),
+      _ => put_expr(expr, rest),
     }
   }
 
   -- Serialize Lam telescope body (all types, then body)
-  fn put_lam_telescope(expr: Expr) -> ByteStream {
+  fn put_lam_telescope(expr: Expr, rest: ByteStream) -> ByteStream {
     match expr {
       Expr.Lam(&ty, &body) =>
-        let ty_bytes = put_expr(ty);
-        let rest_bytes = put_lam_telescope(body);
-        byte_stream_concat(ty_bytes, rest_bytes),
-      _ => put_expr(expr),
+        put_expr(ty, put_lam_telescope(body, rest)),
+      _ => put_expr(expr, rest),
     }
   }
 
   -- Serialize All telescope body (all types, then body)
-  fn put_all_telescope(expr: Expr) -> ByteStream {
+  fn put_all_telescope(expr: Expr, rest: ByteStream) -> ByteStream {
     match expr {
       Expr.All(&ty, &body) =>
-        let ty_bytes = put_expr(ty);
-        let rest_bytes = put_all_telescope(body);
-        byte_stream_concat(ty_bytes, rest_bytes),
-      _ => put_expr(expr),
+        put_expr(ty, put_all_telescope(body, rest)),
+      _ => put_expr(expr, rest),
+    }
+  }
+
+  -- Write a 32-byte address
+  fn put_address(a: [G; 32], rest: ByteStream) -> ByteStream {
+    let list31 = ByteStream.Cons(a[31], store(rest));
+    let list30 = ByteStream.Cons(a[30], store(list31));
+    let list29 = ByteStream.Cons(a[29], store(list30));
+    let list28 = ByteStream.Cons(a[28], store(list29));
+    let list27 = ByteStream.Cons(a[27], store(list28));
+    let list26 = ByteStream.Cons(a[26], store(list27));
+    let list25 = ByteStream.Cons(a[25], store(list26));
+    let list24 = ByteStream.Cons(a[24], store(list25));
+    let list23 = ByteStream.Cons(a[23], store(list24));
+    let list22 = ByteStream.Cons(a[22], store(list23));
+    let list21 = ByteStream.Cons(a[21], store(list22));
+    let list20 = ByteStream.Cons(a[20], store(list21));
+    let list19 = ByteStream.Cons(a[19], store(list20));
+    let list18 = ByteStream.Cons(a[18], store(list19));
+    let list17 = ByteStream.Cons(a[17], store(list18));
+    let list16 = ByteStream.Cons(a[16], store(list17));
+    let list15 = ByteStream.Cons(a[15], store(list16));
+    let list14 = ByteStream.Cons(a[14], store(list15));
+    let list13 = ByteStream.Cons(a[13], store(list14));
+    let list12 = ByteStream.Cons(a[12], store(list13));
+    let list11 = ByteStream.Cons(a[11], store(list12));
+    let list10 = ByteStream.Cons(a[10], store(list11));
+    let list9 = ByteStream.Cons(a[9], store(list10));
+    let list8 = ByteStream.Cons(a[8], store(list9));
+    let list7 = ByteStream.Cons(a[7], store(list8));
+    let list6 = ByteStream.Cons(a[6], store(list7));
+    let list5 = ByteStream.Cons(a[5], store(list6));
+    let list4 = ByteStream.Cons(a[4], store(list5));
+    let list3 = ByteStream.Cons(a[3], store(list4));
+    let list2 = ByteStream.Cons(a[2], store(list3));
+    let list1 = ByteStream.Cons(a[1], store(list2));
+    ByteStream.Cons(a[0], store(list1))
+  }
+
+  -- Pack DefKind (2 bits) and DefinitionSafety (2 bits) into a single byte
+  fn pack_def_kind_safety(kind: DefKind, safety: DefinitionSafety) -> G {
+    let kind_bits = match kind {
+      DefKind.Definition => 0,
+      DefKind.Opaque => 1,
+      DefKind.Theorem => 2,
+    };
+    let safety_bits = match safety {
+      DefinitionSafety.Unsafe => 0,
+      DefinitionSafety.Safe => 1,
+      DefinitionSafety.Partial => 2,
+    };
+    kind_bits * 4 + safety_bits
+  }
+
+  -- ============================================================================
+  -- Universe serialization
+  -- ============================================================================
+
+  -- Count nested Succ universes for telescope compression
+  fn univ_succ_count(u: Univ) -> [G; 8] {
+    match u {
+      Univ.Succ(&inner) => relaxed_u64_succ(univ_succ_count(inner)),
+      _ => [0; 8],
+    }
+  }
+
+  -- Get the base (non-Succ) universe
+  fn univ_succ_base(u: Univ) -> Univ {
+    match u {
+      Univ.Succ(&inner) => univ_succ_base(inner),
+      _ => u,
+    }
+  }
+
+  fn put_univ(u: Univ, rest: ByteStream) -> ByteStream {
+    match u {
+      Univ.Zero =>
+        -- Tag2(FLAG_ZERO_SUCC=0, size=0)
+        ByteStream.Cons(0, store(rest)),
+
+      Univ.Succ(_) =>
+        -- Count nested Succs for telescope compression
+        let count = univ_succ_count(u);
+        -- Find the base (non-Succ) universe
+        let base = univ_succ_base(u);
+        -- Tag2(FLAG_ZERO_SUCC=0, size=count) + base
+        put_tag2(0, count, put_univ(base, rest)),
+
+      Univ.Max(&a, &b) =>
+        -- Tag2(FLAG_MAX=1, size=0)
+        put_tag2(1, [0; 8], put_univ(a, put_univ(b, rest))),
+
+      Univ.IMax(&a, &b) =>
+        -- Tag2(FLAG_IMAX=2, size=0)
+        put_tag2(2, [0; 8], put_univ(a, put_univ(b, rest))),
+
+      Univ.Var(idx) =>
+        -- Tag2(FLAG_VAR=3, size=idx)
+        put_tag2(3, idx, rest),
+    }
+  }
+
+  -- Tag2: 2-bit flag, variable size
+  -- Format: [flag:2][large:1][size:5] or [flag:2][large:1][size_bytes...]
+  fn put_tag2(flag: G, size: [G; 8], rest: ByteStream) -> ByteStream {
+    let byte_count = u64_byte_count(size);
+    let small = u8_less_than(size[0], 32);
+    match (byte_count, small) {
+      (1, 1) =>
+        -- Single byte: flag in bits 6-7, size in bits 0-4
+        let head = flag * 64 + size[0];
+        ByteStream.Cons(head, store(rest)),
+      _ =>
+        -- Multi-byte: flag in bits 6-7, large=1 in bit 5, size_bytes-1 in bits 0-4
+        let head = flag * 64 + 32 + (byte_count - 1);
+        ByteStream.Cons(head, store(put_u64_le(size, byte_count, rest))),
+    }
+  }
+
+  -- ============================================================================
+  -- List serialization
+  -- ============================================================================
+
+  fn put_expr_list(list: ExprList, rest: ByteStream) -> ByteStream {
+    match list {
+      ExprList.Nil => rest,
+      ExprList.Cons(&expr, &rest_list) =>
+        put_expr(expr, put_expr_list(rest_list, rest)),
+    }
+  }
+
+  fn put_univ_list(list: UnivList, rest: ByteStream) -> ByteStream {
+    match list {
+      UnivList.Nil => rest,
+      UnivList.Cons(&u, &rest_list) =>
+        put_univ(u, put_univ_list(rest_list, rest)),
+    }
+  }
+
+  fn put_address_list(list: AddressList, rest: ByteStream) -> ByteStream {
+    match list {
+      AddressList.Nil => rest,
+      AddressList.Cons(addr, &rest_list) =>
+        put_address(addr, put_address_list(rest_list, rest)),
+    }
+  }
+
+  fn expr_list_length(list: ExprList) -> [G; 8] {
+    match list {
+      ExprList.Nil => [0; 8],
+      ExprList.Cons(_, &rest) => relaxed_u64_succ(expr_list_length(rest)),
+    }
+  }
+
+  fn univ_list_length(list: UnivList) -> [G; 8] {
+    match list {
+      UnivList.Nil => [0; 8],
+      UnivList.Cons(_, &rest) => relaxed_u64_succ(univ_list_length(rest)),
+    }
+  }
+
+  fn address_list_length(list: AddressList) -> [G; 8] {
+    match list {
+      AddressList.Nil => [0; 8],
+      AddressList.Cons(_, &rest) => relaxed_u64_succ(address_list_length(rest)),
+    }
+  }
+
+  fn recursor_rule_list_length(list: RecursorRuleList) -> [G; 8] {
+    match list {
+      RecursorRuleList.Nil => [0; 8],
+      RecursorRuleList.Cons(_, &rest) => relaxed_u64_succ(recursor_rule_list_length(rest)),
+    }
+  }
+
+  fn constructor_list_length(list: ConstructorList) -> [G; 8] {
+    match list {
+      ConstructorList.Nil => [0; 8],
+      ConstructorList.Cons(_, &rest) => relaxed_u64_succ(constructor_list_length(rest)),
+    }
+  }
+
+  fn mut_const_list_length(list: MutConstList) -> [G; 8] {
+    match list {
+      MutConstList.Nil => [0; 8],
+      MutConstList.Cons(_, &rest) => relaxed_u64_succ(mut_const_list_length(rest)),
+    }
+  }
+
+  -- ============================================================================
+  -- Constant serialization
+  -- ============================================================================
+
+  fn put_quot_kind(kind: QuotKind, rest: ByteStream) -> ByteStream {
+    let tag = match kind {
+      QuotKind.Typ => 0,
+      QuotKind.Ctor => 1,
+      QuotKind.Lift => 2,
+      QuotKind.Ind => 3,
+    };
+    ByteStream.Cons(tag, store(rest))
+  }
+
+  fn put_definition(defn: Definition, rest: ByteStream) -> ByteStream {
+    match defn {
+      Definition.Mk(kind, safety, lvls, &typ, &value) =>
+        let packed = pack_def_kind_safety(kind, safety);
+        ByteStream.Cons(packed, store(put_tag0(lvls, put_expr(typ, put_expr(value, rest))))),
+    }
+  }
+
+  fn put_recursor_rule(rule: RecursorRule, rest: ByteStream) -> ByteStream {
+    match rule {
+      RecursorRule.Mk(fields, &rhs) =>
+        put_tag0(fields, put_expr(rhs, rest)),
+    }
+  }
+
+  fn put_recursor_rule_list(list: RecursorRuleList, rest: ByteStream) -> ByteStream {
+    match list {
+      RecursorRuleList.Nil => rest,
+      RecursorRuleList.Cons(rule, &rest_list) =>
+        put_recursor_rule(rule, put_recursor_rule_list(rest_list, rest)),
+    }
+  }
+
+  fn put_recursor(recr: Recursor, rest: ByteStream) -> ByteStream {
+    match recr {
+      Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, &typ, &rules) =>
+        let bools = k + 2 * is_unsafe;
+        let rules_len = recursor_rule_list_length(rules);
+        ByteStream.Cons(bools, store(
+          put_tag0(lvls,
+            put_tag0(params,
+              put_tag0(indices,
+                put_tag0(motives,
+                  put_tag0(minors,
+                    put_expr(typ,
+                      put_tag0(rules_len,
+                        put_recursor_rule_list(rules, rest)))))))))),
+    }
+  }
+
+  fn put_axiom(axim: Axiom, rest: ByteStream) -> ByteStream {
+    match axim {
+      Axiom.Mk(is_unsafe, lvls, &typ) =>
+        ByteStream.Cons(is_unsafe, store(put_tag0(lvls, put_expr(typ, rest)))),
+    }
+  }
+
+  fn put_quotient(quot: Quotient, rest: ByteStream) -> ByteStream {
+    match quot {
+      Quotient.Mk(kind, lvls, &typ) =>
+        put_quot_kind(kind, put_tag0(lvls, put_expr(typ, rest))),
+    }
+  }
+
+  fn put_constructor(ctor: Constructor, rest: ByteStream) -> ByteStream {
+    match ctor {
+      Constructor.Mk(is_unsafe, lvls, cidx, params, fields, &typ) =>
+        ByteStream.Cons(is_unsafe, store(
+          put_tag0(lvls,
+            put_tag0(cidx,
+              put_tag0(params,
+                put_tag0(fields,
+                  put_expr(typ, rest))))))),
+    }
+  }
+
+  fn put_constructor_list(list: ConstructorList, rest: ByteStream) -> ByteStream {
+    match list {
+      ConstructorList.Nil => rest,
+      ConstructorList.Cons(ctor, &rest_list) =>
+        put_constructor(ctor, put_constructor_list(rest_list, rest)),
+    }
+  }
+
+  fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
+    match indc {
+      Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, &ctors) =>
+        let bools = recr + 2 * refl + 4 * is_unsafe;
+        let ctors_len = constructor_list_length(ctors);
+        ByteStream.Cons(bools, store(
+          put_tag0(lvls,
+            put_tag0(params,
+              put_tag0(indices,
+                put_tag0(nested,
+                  put_expr(typ,
+                    put_tag0(ctors_len,
+                      put_constructor_list(ctors, rest))))))))),
+    }
+  }
+
+  fn put_inductive_proj(prj: InductiveProj, rest: ByteStream) -> ByteStream {
+    match prj {
+      InductiveProj.Mk(idx, block) =>
+        put_tag0(idx, put_address(block, rest)),
+    }
+  }
+
+  fn put_constructor_proj(prj: ConstructorProj, rest: ByteStream) -> ByteStream {
+    match prj {
+      ConstructorProj.Mk(idx, cidx, block) =>
+        put_tag0(idx, put_tag0(cidx, put_address(block, rest))),
+    }
+  }
+
+  fn put_recursor_proj(prj: RecursorProj, rest: ByteStream) -> ByteStream {
+    match prj {
+      RecursorProj.Mk(idx, block) =>
+        put_tag0(idx, put_address(block, rest)),
+    }
+  }
+
+  fn put_definition_proj(prj: DefinitionProj, rest: ByteStream) -> ByteStream {
+    match prj {
+      DefinitionProj.Mk(idx, block) =>
+        put_tag0(idx, put_address(block, rest)),
+    }
+  }
+
+  fn put_mut_const(mc: MutConst, rest: ByteStream) -> ByteStream {
+    match mc {
+      MutConst.Defn(defn) =>
+        ByteStream.Cons(0, store(put_definition(defn, rest))),
+      MutConst.Indc(indc) =>
+        ByteStream.Cons(1, store(put_inductive(indc, rest))),
+      MutConst.Recr(recr) =>
+        ByteStream.Cons(2, store(put_recursor(recr, rest))),
+    }
+  }
+
+  fn put_mut_const_list(list: MutConstList, rest: ByteStream) -> ByteStream {
+    match list {
+      MutConstList.Nil => rest,
+      MutConstList.Cons(mc, &rest_list) =>
+        put_mut_const(mc, put_mut_const_list(rest_list, rest)),
+    }
+  }
+
+  fn put_constant_info(info: ConstantInfo, rest: ByteStream) -> ByteStream {
+    match info {
+      ConstantInfo.Defn(defn) => put_definition(defn, rest),
+      ConstantInfo.Recr(recr) => put_recursor(recr, rest),
+      ConstantInfo.Axio(axim) => put_axiom(axim, rest),
+      ConstantInfo.Quot(quot) => put_quotient(quot, rest),
+      ConstantInfo.CPrj(prj) => put_constructor_proj(prj, rest),
+      ConstantInfo.RPrj(prj) => put_recursor_proj(prj, rest),
+      ConstantInfo.IPrj(prj) => put_inductive_proj(prj, rest),
+      ConstantInfo.DPrj(prj) => put_definition_proj(prj, rest),
+      -- Muts is never called here - handled separately in put_constant
+      ConstantInfo.Muts(_) => rest,
+    }
+  }
+
+  fn constant_info_variant(info: ConstantInfo) -> [G; 8] {
+    match info {
+      ConstantInfo.Defn(_) => [0; 8],  -- CONST_DEFN
+      ConstantInfo.Recr(_) => [1; 8],  -- CONST_RECR
+      ConstantInfo.Axio(_) => [2; 8],  -- CONST_AXIO
+      ConstantInfo.Quot(_) => [3; 8],  -- CONST_QUOT
+      ConstantInfo.CPrj(_) => [4; 8],  -- CONST_CPRJ
+      ConstantInfo.RPrj(_) => [5; 8],  -- CONST_RPRJ
+      ConstantInfo.IPrj(_) => [6; 8],  -- CONST_IPRJ
+      ConstantInfo.DPrj(_) => [7; 8],  -- CONST_DPRJ
+      ConstantInfo.Muts(_) => [0; 8],  -- Not used (handled separately)
+    }
+  }
+
+  fn put_sharing(list: ExprList, rest: ByteStream) -> ByteStream {
+    let len = expr_list_length(list);
+    put_tag0(len, put_expr_list(list, rest))
+  }
+
+  fn put_refs(list: AddressList, rest: ByteStream) -> ByteStream {
+    let len = address_list_length(list);
+    put_tag0(len, put_address_list(list, rest))
+  }
+
+  fn put_univs(list: UnivList, rest: ByteStream) -> ByteStream {
+    let len = univ_list_length(list);
+    put_tag0(len, put_univ_list(list, rest))
+  }
+
+  fn put_constant(cnst: Constant, rest: ByteStream) -> ByteStream {
+    match cnst {
+      Constant.Mk(info, &sharing, &refs, &univs) =>
+        match info {
+          ConstantInfo.Muts(&mutuals) =>
+            -- Use FLAG_MUTS (0xC) with entry count in size field
+            let count = mut_const_list_length(mutuals);
+            put_tag4(0xC, count,
+              put_mut_const_list(mutuals,
+                put_sharing(sharing,
+                  put_refs(refs,
+                    put_univs(univs, rest))))),
+          _ =>
+            -- Use FLAG (0xD) with variant in size field
+            let variant = constant_info_variant(info);
+            put_tag4(0xD, variant,
+              put_constant_info(info,
+                put_sharing(sharing,
+                  put_refs(refs,
+                    put_univs(univs, rest))))),
+        },
     }
   }
 ⟧
diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean
index 05c3cb25..61e66609 100644
--- a/Tests/Aiur/Common.lean
+++ b/Tests/Aiur/Common.lean
@@ -38,8 +38,8 @@ def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Toplevel) :
     Except String AiurTestEnv := do
   let toplevel ← toplevelFn.mapError toString
   let decls ← toplevel.checkAndSimplify.mapError toString
-  let bytecodeToplevel := decls.compile
-  let aiurSystem := Aiur.AiurSystem.build bytecodeToplevel commitmentParameters
+  let bytecode ← decls.compile
+  let aiurSystem := Aiur.AiurSystem.build bytecode commitmentParameters
   return ⟨toplevel, aiurSystem⟩
 
 def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : TestSeq :=
@@ -60,8 +60,8 @@ def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel)
     (cases : List AiurTestCase) : TestSeq :=
   withExceptOk "Toplevel merging succeeds" toplevelFn fun toplevel =>
     withExceptOk "Check and simplification succeed" toplevel.checkAndSimplify fun decls =>
-      let bytecodeToplevel := decls.compile
-      let aiurSystem := Aiur.AiurSystem.build bytecodeToplevel commitmentParameters
+      withExceptOk "Compilation succeeds" decls.compile fun bytecode =>
+      let aiurSystem := Aiur.AiurSystem.build bytecode commitmentParameters
       let env : AiurTestEnv := ⟨toplevel, aiurSystem⟩
       cases.foldl (init := .done) fun tSeq testCase =>
         tSeq ++ env.runTestCase testCase