From d51f6faa49a83e3aa5fb1a7607d1f8459b42e834 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Fri, 13 Feb 2026 10:59:26 -0300
Subject: [PATCH 1/7] nuked old serializer

---
 Ix/IxVM/Ixon.lean            |  70 ----
 Ix/IxVM/IxonDeserialize.lean | 602 -----------------------------------
 Ix/IxVM/IxonSerialize.lean   | 426 -------------------------
 3 files changed, 1098 deletions(-)

diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index c920e22d..7907ab55 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -2,74 +2,4 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
-def ixon := ⟦
-  enum Address {
-    Bytes([[G; 4]; 8])
-  }
-
-  enum Nat {
-    Bytes(ByteStream)
-  }
-
-  enum Tag4 {
-    Mk(G, [G; 8])
-  }
-
-  enum DefKind {
-    Definition,
-    Opaque,
-    Theorem
-  }
-
-  enum BuiltIn {
-    Obj,
-    Neutral,
-    Unreachable
-  }
-
-  enum DefinitionSafety {
-    Unsafe,
-    Safe,
-    Partial
-  }
-
-  enum Ixon {
-    NAnon,                                 -- 0x00, anonymous name
-    NStr(Address, Address),                -- 0x01, string name
-    NNum(Address, Address),                -- 0x02, number name
-    UZero,                                 -- 0x03, universe zero
-    USucc(Address),                        -- 0x04, universe successor
-    UMax(Address, Address),                -- 0x05, universe max
-    UIMax(Address, Address),               -- 0x06, universe impredicative max
-    UVar(Nat),                             -- 0x1X, universe variable
-    EVar(Nat),                             -- 0x2X, expression variable
-    -- ERef(Address, Vec<Address>),           -- 0x3X, expression reference
-    -- ERec(Nat, Vec<Address>),               -- 0x4X, expression recursion
-    -- EPrj(Address, Nat, Address),           -- 0x5X, expression projection
-    ESort(Address),                        -- 0x80, expression sort
-    EStr(Address),                         -- 0x81, expression string
-    ENat(Address),                         -- 0x82, expression natural
-    EApp(Address, Address),                -- 0x83, expression application
-    ELam(Address, Address),                -- 0x84, expression lambda
-    EAll(Address, Address),                -- 0x85, expression forall
-    ELet(G, Address, Address, Address),    -- 0x86, 0x87, expression let. TODO: change the first argument to a Bool
-    Blob(ByteStream),                      -- 0x9X, tagged bytes
-    -- Defn(Definition),                      -- 0xA0, definition constant
-    -- Recr(Recursor),                        -- 0xA1, recursor constant
-    -- Axio(Axiom),                           -- 0xA2, axiom constant
-    -- Quot(Quotient),                        -- 0xA3, quotient constant
-    -- CPrj(ConstructorProj),                 -- 0xA4, constructor projection
-    -- RPrj(RecursorProj),                    -- 0xA5, recursor projection
-    -- IPrj(InductiveProj),                   -- 0xA6, inductive projection
-    -- DPrj(DefinitionProj),
-    -- 0xA7, definition projection
-    -- Muts(Vec<MutConst>),                   -- 0xBX, mutual constants
-    -- 0xE0: Env (environment), 0xE1: CheckProof, 0xE2: EvalProof
-    Chck(Address, Address, Address),             -- 0xE3, typechecking claim
-    Eval(Address, Address, Address, Address),    -- 0xE4, evaluation claim
-    Comm(Address, Address),                      -- 0xE5, cryptographic commitment
-    Prim(BuiltIn)                                -- 0xE6, compiler built-ins
-  }
-⟧
-
 end IxVM
diff --git a/Ix/IxVM/IxonDeserialize.lean b/Ix/IxVM/IxonDeserialize.lean
index 583c3f33..7907ab55 100644
--- a/Ix/IxVM/IxonDeserialize.lean
+++ b/Ix/IxVM/IxonDeserialize.lean
@@ -2,606 +2,4 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
-set_option maxHeartbeats 2000000 in
-def ixonDeserialize := ⟦
-  #[unconstrained]
-  fn deserialize(stream: ByteStream) -> Ixon {
-    match stream {
-      ByteStream.Cons(0x00, _) => Ixon.NAnon,
-      ByteStream.Cons(0x01, tail_ptr) =>
-        let tail = load(tail_ptr);
-        -- let (addr1, tail) = fold(0..8, ([[0; 4]; 8], tail), |acc, @i|
-        --   fold(0..4, acc, |(acc_addr, acc_stream), @j|
-        --     let ByteStream.Cons(byte, acc_stream_tail_ptr) = acc_stream;
-        --     (set(acc_addr, @i, set(acc_addr[@i], @j, byte)), load(acc_stream_tail_ptr))));
-        -- let (addr2, _tail) = fold(0..8, ([[0; 4]; 8], tail), |acc, @i|
-        --   fold(0..4, acc, |(acc_addr, acc_stream), @j|
-        --     let ByteStream.Cons(byte, acc_stream_tail_ptr) = acc_stream;
-        --     (set(acc_addr, @i, set(acc_addr[@i], @j, byte)), load(acc_stream_tail_ptr))));
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.NStr(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x02, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.NNum(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x03, _) => Ixon.UZero,
-      ByteStream.Cons(0x04, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.USucc(Address.Bytes(addr)),
-      ByteStream.Cons(0x05, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.UMax(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x06, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.UIMax(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x80, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.ESort(Address.Bytes(addr)),
-      ByteStream.Cons(0x81, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.EStr(Address.Bytes(addr)),
-      ByteStream.Cons(0x82, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.ENat(Address.Bytes(addr)),
-      ByteStream.Cons(0x83, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.EApp(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x84, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.ELam(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x85, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.EAll(Address.Bytes(addr1), Address.Bytes(addr2)),
-      ByteStream.Cons(0x86, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr3, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.ELet(1, Address.Bytes(addr1), Address.Bytes(addr2), Address.Bytes(addr3)),
-      ByteStream.Cons(0x87, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr3, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.ELet(0, Address.Bytes(addr1), Address.Bytes(addr2), Address.Bytes(addr3)),
-      ByteStream.Cons(0xE3, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr3, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.Chck(Address.Bytes(addr1), Address.Bytes(addr2), Address.Bytes(addr3)),
-      ByteStream.Cons(0xE4, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr3, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr4, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.Eval(
-          Address.Bytes(addr1), Address.Bytes(addr2),
-          Address.Bytes(addr3), Address.Bytes(addr4)
-        ),
-      ByteStream.Cons(0xE5, tail_ptr) =>
-        let tail = load(tail_ptr);
-        let (addr1, tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        let (addr2, _tail) = deserialize_addr(tail, [[0; 4]; 8], 0);
-        Ixon.Comm(Address.Bytes(addr1), Address.Bytes(addr2)),
-      _ => -- Variable sizes
-        let (tag, stream) = deserialize_tag(stream);
-        match tag {
-          Tag4.Mk(1, size) =>
-            let (bytes, _) = deserialize_byte_stream(stream, [0; 8], size);
-            Ixon.UVar(Nat.Bytes(bytes)),
-          Tag4.Mk(2, size) =>
-            let (bytes, _) = deserialize_byte_stream(stream, [0; 8], size);
-            Ixon.EVar(Nat.Bytes(bytes)),
-          Tag4.Mk(9, size) =>
-            let (bytes, _) = deserialize_byte_stream(stream, [0; 8], size);
-            Ixon.Blob(bytes),
-        },
-    }
-  }
-
-  #[unconstrained]
-  fn deserialize_tag(stream: ByteStream) -> (Tag4, ByteStream) {
-    match stream {
-      ByteStream.Cons(head, tail_ptr) =>
-        let (flag, large, small) = decode_tag_head(head);
-        match large {
-          0 => (Tag4.Mk(flag, [small, 0, 0, 0, 0, 0, 0, 0]), load(tail_ptr)),
-          1 =>
-            let (u64, tail) = u64_get_trimmed_le(small + 1, load(tail_ptr));
-            (Tag4.Mk(flag, u64), tail),
-        },
-    }
-  }
-
-  #[unconstrained]
-  fn deserialize_byte_stream(stream: ByteStream, count: [G; 8], size: [G; 8]) -> (ByteStream, ByteStream) {
-    match (size[0]-count[0], size[1]-count[1], size[2]-count[2], size[3]-count[3],
-           size[4]-count[4], size[5]-count[5], size[6]-count[6], size[7]-count[7]) {
-      (0, 0, 0, 0, 0, 0, 0, 0) => (ByteStream.Nil, stream),
-      _ => match stream {
-        ByteStream.Cons(byte, tail_ptr) =>
-          let (tail_de, remaining) = deserialize_byte_stream(
-            load(tail_ptr),
-            relaxed_u64_succ(count),
-            size
-          );
-          (ByteStream.Cons(byte, store(tail_de)), remaining),
-      },
-    }
-  }
-
-  -- TODO: remove this function
-  #[unconstrained]
-  fn deserialize_addr(stream: ByteStream, addr: [[G; 4]; 8], i: G) -> ([[G; 4]; 8], ByteStream) {
-    match stream {
-      ByteStream.Cons(byte, tail_ptr) =>
-        match i {
-          0 =>
-            let addr = set(addr, 0, set(addr[0], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 1),
-          1 =>
-            let addr = set(addr, 0, set(addr[0], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 2),
-          2 =>
-            let addr = set(addr, 0, set(addr[0], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 3),
-          3 =>
-            let addr = set(addr, 0, set(addr[0], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 4),
-          4 =>
-            let addr = set(addr, 1, set(addr[1], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 5),
-          5 =>
-            let addr = set(addr, 1, set(addr[1], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 6),
-          6 =>
-            let addr = set(addr, 1, set(addr[1], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 7),
-          7 =>
-            let addr = set(addr, 1, set(addr[1], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 8),
-          8 =>
-            let addr = set(addr, 2, set(addr[2], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 9),
-          9 =>
-            let addr = set(addr, 2, set(addr[2], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 10),
-          10 =>
-            let addr = set(addr, 2, set(addr[2], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 11),
-          11 =>
-            let addr = set(addr, 2, set(addr[2], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 12),
-          12 =>
-            let addr = set(addr, 3, set(addr[3], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 13),
-          13 =>
-            let addr = set(addr, 3, set(addr[3], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 14),
-          14 =>
-            let addr = set(addr, 3, set(addr[3], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 15),
-          15 =>
-            let addr = set(addr, 3, set(addr[3], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 16),
-          16 =>
-            let addr = set(addr, 4, set(addr[4], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 17),
-          17 =>
-            let addr = set(addr, 4, set(addr[4], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 18),
-          18 =>
-            let addr = set(addr, 4, set(addr[4], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 19),
-          19 =>
-            let addr = set(addr, 4, set(addr[4], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 20),
-          20 =>
-            let addr = set(addr, 5, set(addr[5], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 21),
-          21 =>
-            let addr = set(addr, 5, set(addr[5], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 22),
-          22 =>
-            let addr = set(addr, 5, set(addr[5], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 23),
-          23 =>
-            let addr = set(addr, 5, set(addr[5], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 24),
-          24 =>
-            let addr = set(addr, 6, set(addr[6], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 25),
-          25 =>
-            let addr = set(addr, 6, set(addr[6], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 26),
-          26 =>
-            let addr = set(addr, 6, set(addr[6], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 27),
-          27 =>
-            let addr = set(addr, 6, set(addr[6], 3, byte));
-            deserialize_addr(load(tail_ptr), addr, 28),
-          28 =>
-            let addr = set(addr, 7, set(addr[7], 0, byte));
-            deserialize_addr(load(tail_ptr), addr, 29),
-          29 =>
-            let addr = set(addr, 7, set(addr[7], 1, byte));
-            deserialize_addr(load(tail_ptr), addr, 30),
-          30 =>
-            let addr = set(addr, 7, set(addr[7], 2, byte));
-            deserialize_addr(load(tail_ptr), addr, 31),
-          31 =>
-            let addr = set(addr, 7, set(addr[7], 3, byte));
-            (addr, load(tail_ptr)),
-        },
-    }
-  }
-
-  #[unconstrained]
-  fn decode_tag_head(head: G) -> (G, G, G) {
-    match head {
-      0b00000000 => (0b0000, 0b0, 0b000),
-      0b00000001 => (0b0000, 0b0, 0b001),
-      0b00000010 => (0b0000, 0b0, 0b010),
-      0b00000011 => (0b0000, 0b0, 0b011),
-      0b00000100 => (0b0000, 0b0, 0b100),
-      0b00000101 => (0b0000, 0b0, 0b101),
-      0b00000110 => (0b0000, 0b0, 0b110),
-      0b00000111 => (0b0000, 0b0, 0b111),
-      0b00001000 => (0b0000, 0b1, 0b000),
-      0b00001001 => (0b0000, 0b1, 0b001),
-      0b00001010 => (0b0000, 0b1, 0b010),
-      0b00001011 => (0b0000, 0b1, 0b011),
-      0b00001100 => (0b0000, 0b1, 0b100),
-      0b00001101 => (0b0000, 0b1, 0b101),
-      0b00001110 => (0b0000, 0b1, 0b110),
-      0b00001111 => (0b0000, 0b1, 0b111),
-      0b00010000 => (0b0001, 0b0, 0b000),
-      0b00010001 => (0b0001, 0b0, 0b001),
-      0b00010010 => (0b0001, 0b0, 0b010),
-      0b00010011 => (0b0001, 0b0, 0b011),
-      0b00010100 => (0b0001, 0b0, 0b100),
-      0b00010101 => (0b0001, 0b0, 0b101),
-      0b00010110 => (0b0001, 0b0, 0b110),
-      0b00010111 => (0b0001, 0b0, 0b111),
-      0b00011000 => (0b0001, 0b1, 0b000),
-      0b00011001 => (0b0001, 0b1, 0b001),
-      0b00011010 => (0b0001, 0b1, 0b010),
-      0b00011011 => (0b0001, 0b1, 0b011),
-      0b00011100 => (0b0001, 0b1, 0b100),
-      0b00011101 => (0b0001, 0b1, 0b101),
-      0b00011110 => (0b0001, 0b1, 0b110),
-      0b00011111 => (0b0001, 0b1, 0b111),
-      0b00100000 => (0b0010, 0b0, 0b000),
-      0b00100001 => (0b0010, 0b0, 0b001),
-      0b00100010 => (0b0010, 0b0, 0b010),
-      0b00100011 => (0b0010, 0b0, 0b011),
-      0b00100100 => (0b0010, 0b0, 0b100),
-      0b00100101 => (0b0010, 0b0, 0b101),
-      0b00100110 => (0b0010, 0b0, 0b110),
-      0b00100111 => (0b0010, 0b0, 0b111),
-      0b00101000 => (0b0010, 0b1, 0b000),
-      0b00101001 => (0b0010, 0b1, 0b001),
-      0b00101010 => (0b0010, 0b1, 0b010),
-      0b00101011 => (0b0010, 0b1, 0b011),
-      0b00101100 => (0b0010, 0b1, 0b100),
-      0b00101101 => (0b0010, 0b1, 0b101),
-      0b00101110 => (0b0010, 0b1, 0b110),
-      0b00101111 => (0b0010, 0b1, 0b111),
-      0b00110000 => (0b0011, 0b0, 0b000),
-      0b00110001 => (0b0011, 0b0, 0b001),
-      0b00110010 => (0b0011, 0b0, 0b010),
-      0b00110011 => (0b0011, 0b0, 0b011),
-      0b00110100 => (0b0011, 0b0, 0b100),
-      0b00110101 => (0b0011, 0b0, 0b101),
-      0b00110110 => (0b0011, 0b0, 0b110),
-      0b00110111 => (0b0011, 0b0, 0b111),
-      0b00111000 => (0b0011, 0b1, 0b000),
-      0b00111001 => (0b0011, 0b1, 0b001),
-      0b00111010 => (0b0011, 0b1, 0b010),
-      0b00111011 => (0b0011, 0b1, 0b011),
-      0b00111100 => (0b0011, 0b1, 0b100),
-      0b00111101 => (0b0011, 0b1, 0b101),
-      0b00111110 => (0b0011, 0b1, 0b110),
-      0b00111111 => (0b0011, 0b1, 0b111),
-      0b01000000 => (0b0100, 0b0, 0b000),
-      0b01000001 => (0b0100, 0b0, 0b001),
-      0b01000010 => (0b0100, 0b0, 0b010),
-      0b01000011 => (0b0100, 0b0, 0b011),
-      0b01000100 => (0b0100, 0b0, 0b100),
-      0b01000101 => (0b0100, 0b0, 0b101),
-      0b01000110 => (0b0100, 0b0, 0b110),
-      0b01000111 => (0b0100, 0b0, 0b111),
-      0b01001000 => (0b0100, 0b1, 0b000),
-      0b01001001 => (0b0100, 0b1, 0b001),
-      0b01001010 => (0b0100, 0b1, 0b010),
-      0b01001011 => (0b0100, 0b1, 0b011),
-      0b01001100 => (0b0100, 0b1, 0b100),
-      0b01001101 => (0b0100, 0b1, 0b101),
-      0b01001110 => (0b0100, 0b1, 0b110),
-      0b01001111 => (0b0100, 0b1, 0b111),
-      0b01010000 => (0b0101, 0b0, 0b000),
-      0b01010001 => (0b0101, 0b0, 0b001),
-      0b01010010 => (0b0101, 0b0, 0b010),
-      0b01010011 => (0b0101, 0b0, 0b011),
-      0b01010100 => (0b0101, 0b0, 0b100),
-      0b01010101 => (0b0101, 0b0, 0b101),
-      0b01010110 => (0b0101, 0b0, 0b110),
-      0b01010111 => (0b0101, 0b0, 0b111),
-      0b01011000 => (0b0101, 0b1, 0b000),
-      0b01011001 => (0b0101, 0b1, 0b001),
-      0b01011010 => (0b0101, 0b1, 0b010),
-      0b01011011 => (0b0101, 0b1, 0b011),
-      0b01011100 => (0b0101, 0b1, 0b100),
-      0b01011101 => (0b0101, 0b1, 0b101),
-      0b01011110 => (0b0101, 0b1, 0b110),
-      0b01011111 => (0b0101, 0b1, 0b111),
-      0b01100000 => (0b0110, 0b0, 0b000),
-      0b01100001 => (0b0110, 0b0, 0b001),
-      0b01100010 => (0b0110, 0b0, 0b010),
-      0b01100011 => (0b0110, 0b0, 0b011),
-      0b01100100 => (0b0110, 0b0, 0b100),
-      0b01100101 => (0b0110, 0b0, 0b101),
-      0b01100110 => (0b0110, 0b0, 0b110),
-      0b01100111 => (0b0110, 0b0, 0b111),
-      0b01101000 => (0b0110, 0b1, 0b000),
-      0b01101001 => (0b0110, 0b1, 0b001),
-      0b01101010 => (0b0110, 0b1, 0b010),
-      0b01101011 => (0b0110, 0b1, 0b011),
-      0b01101100 => (0b0110, 0b1, 0b100),
-      0b01101101 => (0b0110, 0b1, 0b101),
-      0b01101110 => (0b0110, 0b1, 0b110),
-      0b01101111 => (0b0110, 0b1, 0b111),
-      0b01110000 => (0b0111, 0b0, 0b000),
-      0b01110001 => (0b0111, 0b0, 0b001),
-      0b01110010 => (0b0111, 0b0, 0b010),
-      0b01110011 => (0b0111, 0b0, 0b011),
-      0b01110100 => (0b0111, 0b0, 0b100),
-      0b01110101 => (0b0111, 0b0, 0b101),
-      0b01110110 => (0b0111, 0b0, 0b110),
-      0b01110111 => (0b0111, 0b0, 0b111),
-      0b01111000 => (0b0111, 0b1, 0b000),
-      0b01111001 => (0b0111, 0b1, 0b001),
-      0b01111010 => (0b0111, 0b1, 0b010),
-      0b01111011 => (0b0111, 0b1, 0b011),
-      0b01111100 => (0b0111, 0b1, 0b100),
-      0b01111101 => (0b0111, 0b1, 0b101),
-      0b01111110 => (0b0111, 0b1, 0b110),
-      0b01111111 => (0b0111, 0b1, 0b111),
-      0b10000000 => (0b1000, 0b0, 0b000),
-      0b10000001 => (0b1000, 0b0, 0b001),
-      0b10000010 => (0b1000, 0b0, 0b010),
-      0b10000011 => (0b1000, 0b0, 0b011),
-      0b10000100 => (0b1000, 0b0, 0b100),
-      0b10000101 => (0b1000, 0b0, 0b101),
-      0b10000110 => (0b1000, 0b0, 0b110),
-      0b10000111 => (0b1000, 0b0, 0b111),
-      0b10001000 => (0b1000, 0b1, 0b000),
-      0b10001001 => (0b1000, 0b1, 0b001),
-      0b10001010 => (0b1000, 0b1, 0b010),
-      0b10001011 => (0b1000, 0b1, 0b011),
-      0b10001100 => (0b1000, 0b1, 0b100),
-      0b10001101 => (0b1000, 0b1, 0b101),
-      0b10001110 => (0b1000, 0b1, 0b110),
-      0b10001111 => (0b1000, 0b1, 0b111),
-      0b10010000 => (0b1001, 0b0, 0b000),
-      0b10010001 => (0b1001, 0b0, 0b001),
-      0b10010010 => (0b1001, 0b0, 0b010),
-      0b10010011 => (0b1001, 0b0, 0b011),
-      0b10010100 => (0b1001, 0b0, 0b100),
-      0b10010101 => (0b1001, 0b0, 0b101),
-      0b10010110 => (0b1001, 0b0, 0b110),
-      0b10010111 => (0b1001, 0b0, 0b111),
-      0b10011000 => (0b1001, 0b1, 0b000),
-      0b10011001 => (0b1001, 0b1, 0b001),
-      0b10011010 => (0b1001, 0b1, 0b010),
-      0b10011011 => (0b1001, 0b1, 0b011),
-      0b10011100 => (0b1001, 0b1, 0b100),
-      0b10011101 => (0b1001, 0b1, 0b101),
-      0b10011110 => (0b1001, 0b1, 0b110),
-      0b10011111 => (0b1001, 0b1, 0b111),
-      0b10100000 => (0b1010, 0b0, 0b000),
-      0b10100001 => (0b1010, 0b0, 0b001),
-      0b10100010 => (0b1010, 0b0, 0b010),
-      0b10100011 => (0b1010, 0b0, 0b011),
-      0b10100100 => (0b1010, 0b0, 0b100),
-      0b10100101 => (0b1010, 0b0, 0b101),
-      0b10100110 => (0b1010, 0b0, 0b110),
-      0b10100111 => (0b1010, 0b0, 0b111),
-      0b10101000 => (0b1010, 0b1, 0b000),
-      0b10101001 => (0b1010, 0b1, 0b001),
-      0b10101010 => (0b1010, 0b1, 0b010),
-      0b10101011 => (0b1010, 0b1, 0b011),
-      0b10101100 => (0b1010, 0b1, 0b100),
-      0b10101101 => (0b1010, 0b1, 0b101),
-      0b10101110 => (0b1010, 0b1, 0b110),
-      0b10101111 => (0b1010, 0b1, 0b111),
-      0b10110000 => (0b1011, 0b0, 0b000),
-      0b10110001 => (0b1011, 0b0, 0b001),
-      0b10110010 => (0b1011, 0b0, 0b010),
-      0b10110011 => (0b1011, 0b0, 0b011),
-      0b10110100 => (0b1011, 0b0, 0b100),
-      0b10110101 => (0b1011, 0b0, 0b101),
-      0b10110110 => (0b1011, 0b0, 0b110),
-      0b10110111 => (0b1011, 0b0, 0b111),
-      0b10111000 => (0b1011, 0b1, 0b000),
-      0b10111001 => (0b1011, 0b1, 0b001),
-      0b10111010 => (0b1011, 0b1, 0b010),
-      0b10111011 => (0b1011, 0b1, 0b011),
-      0b10111100 => (0b1011, 0b1, 0b100),
-      0b10111101 => (0b1011, 0b1, 0b101),
-      0b10111110 => (0b1011, 0b1, 0b110),
-      0b10111111 => (0b1011, 0b1, 0b111),
-      0b11000000 => (0b1100, 0b0, 0b000),
-      0b11000001 => (0b1100, 0b0, 0b001),
-      0b11000010 => (0b1100, 0b0, 0b010),
-      0b11000011 => (0b1100, 0b0, 0b011),
-      0b11000100 => (0b1100, 0b0, 0b100),
-      0b11000101 => (0b1100, 0b0, 0b101),
-      0b11000110 => (0b1100, 0b0, 0b110),
-      0b11000111 => (0b1100, 0b0, 0b111),
-      0b11001000 => (0b1100, 0b1, 0b000),
-      0b11001001 => (0b1100, 0b1, 0b001),
-      0b11001010 => (0b1100, 0b1, 0b010),
-      0b11001011 => (0b1100, 0b1, 0b011),
-      0b11001100 => (0b1100, 0b1, 0b100),
-      0b11001101 => (0b1100, 0b1, 0b101),
-      0b11001110 => (0b1100, 0b1, 0b110),
-      0b11001111 => (0b1100, 0b1, 0b111),
-      0b11010000 => (0b1101, 0b0, 0b000),
-      0b11010001 => (0b1101, 0b0, 0b001),
-      0b11010010 => (0b1101, 0b0, 0b010),
-      0b11010011 => (0b1101, 0b0, 0b011),
-      0b11010100 => (0b1101, 0b0, 0b100),
-      0b11010101 => (0b1101, 0b0, 0b101),
-      0b11010110 => (0b1101, 0b0, 0b110),
-      0b11010111 => (0b1101, 0b0, 0b111),
-      0b11011000 => (0b1101, 0b1, 0b000),
-      0b11011001 => (0b1101, 0b1, 0b001),
-      0b11011010 => (0b1101, 0b1, 0b010),
-      0b11011011 => (0b1101, 0b1, 0b011),
-      0b11011100 => (0b1101, 0b1, 0b100),
-      0b11011101 => (0b1101, 0b1, 0b101),
-      0b11011110 => (0b1101, 0b1, 0b110),
-      0b11011111 => (0b1101, 0b1, 0b111),
-      0b11100000 => (0b1110, 0b0, 0b000),
-      0b11100001 => (0b1110, 0b0, 0b001),
-      0b11100010 => (0b1110, 0b0, 0b010),
-      0b11100011 => (0b1110, 0b0, 0b011),
-      0b11100100 => (0b1110, 0b0, 0b100),
-      0b11100101 => (0b1110, 0b0, 0b101),
-      0b11100110 => (0b1110, 0b0, 0b110),
-      0b11100111 => (0b1110, 0b0, 0b111),
-      0b11101000 => (0b1110, 0b1, 0b000),
-      0b11101001 => (0b1110, 0b1, 0b001),
-      0b11101010 => (0b1110, 0b1, 0b010),
-      0b11101011 => (0b1110, 0b1, 0b011),
-      0b11101100 => (0b1110, 0b1, 0b100),
-      0b11101101 => (0b1110, 0b1, 0b101),
-      0b11101110 => (0b1110, 0b1, 0b110),
-      0b11101111 => (0b1110, 0b1, 0b111),
-      0b11110000 => (0b1111, 0b0, 0b000),
-      0b11110001 => (0b1111, 0b0, 0b001),
-      0b11110010 => (0b1111, 0b0, 0b010),
-      0b11110011 => (0b1111, 0b0, 0b011),
-      0b11110100 => (0b1111, 0b0, 0b100),
-      0b11110101 => (0b1111, 0b0, 0b101),
-      0b11110110 => (0b1111, 0b0, 0b110),
-      0b11110111 => (0b1111, 0b0, 0b111),
-      0b11111000 => (0b1111, 0b1, 0b000),
-      0b11111001 => (0b1111, 0b1, 0b001),
-      0b11111010 => (0b1111, 0b1, 0b010),
-      0b11111011 => (0b1111, 0b1, 0b011),
-      0b11111100 => (0b1111, 0b1, 0b100),
-      0b11111101 => (0b1111, 0b1, 0b101),
-      0b11111110 => (0b1111, 0b1, 0b110),
-      0b11111111 => (0b1111, 0b1, 0b111),
-    }
-  }
-
-  #[unconstrained]
-  fn u64_get_trimmed_le(len: G, stream: ByteStream) -> ([G; 8], ByteStream) {
-    let u64 = [0; 8];
-    match len {
-      1 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        (set(u64, 0, b0), load(tail_ptr)),
-      2 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        (set(u64, 1, b1), load(tail_ptr)),
-      3 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        (set(u64, 2, b2), load(tail_ptr)),
-      4 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b3, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        let u64 = set(u64, 2, b2);
-        (set(u64, 3, b3), load(tail_ptr)),
-      5 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b3, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b4, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        let u64 = set(u64, 2, b2);
-        let u64 = set(u64, 3, b3);
-        (set(u64, 4, b4), load(tail_ptr)),
-      6 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b3, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b4, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b5, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        let u64 = set(u64, 2, b2);
-        let u64 = set(u64, 3, b3);
-        let u64 = set(u64, 4, b4);
-        (set(u64, 5, b5), load(tail_ptr)),
-      7 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b3, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b4, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b5, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b6, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        let u64 = set(u64, 2, b2);
-        let u64 = set(u64, 3, b3);
-        let u64 = set(u64, 4, b4);
-        let u64 = set(u64, 5, b5);
-        (set(u64, 6, b6), load(tail_ptr)),
-      8 =>
-        let ByteStream.Cons(b0, tail_ptr) = stream;
-        let ByteStream.Cons(b1, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b2, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b3, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b4, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b5, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b6, tail_ptr) = load(tail_ptr);
-        let ByteStream.Cons(b7, tail_ptr) = load(tail_ptr);
-        let u64 = set(u64, 0, b0);
-        let u64 = set(u64, 1, b1);
-        let u64 = set(u64, 2, b2);
-        let u64 = set(u64, 3, b3);
-        let u64 = set(u64, 4, b4);
-        let u64 = set(u64, 5, b5);
-        let u64 = set(u64, 6, b6);
-        (set(u64, 7, b7), load(tail_ptr)),
-    }
-  }
-⟧
-
 end IxVM
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index a3a1f1f0..7907ab55 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -2,430 +2,4 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
-set_option maxHeartbeats 2000000 in
-def ixonSerialize := ⟦
-  fn serialize(ixon: Ixon) -> ByteStream {
-    let stream = ByteStream.Nil;
-    match ixon {
-      Ixon.NAnon => ByteStream.Cons(0x00, store(stream)),
-      Ixon.NStr(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x01;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.NNum(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x02;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.UZero => ByteStream.Cons(0x03, store(stream)),
-      Ixon.USucc(Address.Bytes(n)) =>
-        let tag = 0x04;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.UMax(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x05;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.UIMax(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x06;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.ESort(Address.Bytes(n)) =>
-        let tag = 0x80;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.EStr(Address.Bytes(n)) =>
-        let tag = 0x81;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.ENat(Address.Bytes(n)) =>
-        let tag = 0x82;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.EApp(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x83;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.ELam(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x84;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.EAll(Address.Bytes(n), Address.Bytes(s)) =>
-        let tag = 0x85;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.ELet(b, Address.Bytes(n), Address.Bytes(s), Address.Bytes(t)) =>
-        let tag = 0x87 - b;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(n[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(s[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(t[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.Chck(Address.Bytes(a), Address.Bytes(b), Address.Bytes(c)) =>
-        let tag = 0xE3;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(a[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(b[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(c[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.Eval(Address.Bytes(a), Address.Bytes(b), Address.Bytes(c), Address.Bytes(d)) =>
-        let tag = 0xE4;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(a[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(b[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(c[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(d[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.Comm(Address.Bytes(a), Address.Bytes(b)) =>
-        let tag = 0xE5;
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(a[@i][@j], store(stream))));
-        let stream = fold(8..0, stream, |stream, @i|
-          fold(4..0, stream, |stream, @j| ByteStream.Cons(b[@i][@j], store(stream))));
-        ByteStream.Cons(tag, store(stream)),
-      Ixon.Blob(bytes) =>
-        let len: [G; 8] = byte_stream_length(bytes);
-        let flag = 0x9;
-        serialize_cons_head(flag, len, bytes),
-      Ixon.UVar(Nat.Bytes(bytes)) =>
-        let len: [G; 8] = byte_stream_length(bytes);
-        let flag = 0x1;
-        serialize_cons_head(flag, len, bytes),
-      Ixon.EVar(Nat.Bytes(bytes)) =>
-        let len: [G; 8] = byte_stream_length(bytes);
-        let flag = 0x2;
-        serialize_cons_head(flag, len, bytes),
-    }
-  }
-
-  fn serialize_cons_head(flag: G, len: [G; 8], stream: ByteStream) -> ByteStream {
-    match len {
-      [b1, 0, 0, 0, 0, 0, 0, 0] =>
-        -- 248 is minus 8 in u8
-        let (_, large) = u8_add(b1, 248);
-        match large {
-          0 =>
-            let tag = encode_tag_head(flag, 0, b1);
-            ByteStream.Cons(tag, store(stream)),
-          1 =>
-            let tag = encode_tag_head(flag, 1, 0);
-            ByteStream.Cons(tag, store(ByteStream.Cons(b1, store(stream)))),
-        },
-      [_, _, 0, 0, 0, 0, 0, 0] =>
-        let tag = encode_tag_head(flag, 1, 1);
-        ByteStream.Cons(tag, store(fold(2..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, 0, 0, 0, 0, 0] =>
-        let tag = encode_tag_head(flag, 1, 2);
-        ByteStream.Cons(tag, store(fold(3..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, _, 0, 0, 0, 0] =>
-        let tag = encode_tag_head(flag, 1, 3);
-        ByteStream.Cons(tag, store(fold(4..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, _, _, 0, 0, 0] =>
-        let tag = encode_tag_head(flag, 1, 4);
-        ByteStream.Cons(tag, store(fold(5..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, _, _, _, 0, 0] =>
-        let tag = encode_tag_head(flag, 1, 5);
-        ByteStream.Cons(tag, store(fold(6..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, _, _, _, _, 0] =>
-        let tag = encode_tag_head(flag, 1, 6);
-        ByteStream.Cons(tag, store(fold(7..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-      [_, _, _, _, _, _, _, _] =>
-        let tag = encode_tag_head(flag, 1, 7);
-        ByteStream.Cons(tag, store(fold(8..0, stream, |stream, @i| ByteStream.Cons(len[@i], store(stream))))),
-    }
-  }
-
-  fn encode_tag_head(x: G, y: G, z: G) -> G {
-    match (x, y, z) {
-      (0b0000, 0b0, 0b000) => 0b00000000,
-      (0b0000, 0b0, 0b001) => 0b00000001,
-      (0b0000, 0b0, 0b010) => 0b00000010,
-      (0b0000, 0b0, 0b011) => 0b00000011,
-      (0b0000, 0b0, 0b100) => 0b00000100,
-      (0b0000, 0b0, 0b101) => 0b00000101,
-      (0b0000, 0b0, 0b110) => 0b00000110,
-      (0b0000, 0b0, 0b111) => 0b00000111,
-      (0b0000, 0b1, 0b000) => 0b00001000,
-      (0b0000, 0b1, 0b001) => 0b00001001,
-      (0b0000, 0b1, 0b010) => 0b00001010,
-      (0b0000, 0b1, 0b011) => 0b00001011,
-      (0b0000, 0b1, 0b100) => 0b00001100,
-      (0b0000, 0b1, 0b101) => 0b00001101,
-      (0b0000, 0b1, 0b110) => 0b00001110,
-      (0b0000, 0b1, 0b111) => 0b00001111,
-      (0b0001, 0b0, 0b000) => 0b00010000,
-      (0b0001, 0b0, 0b001) => 0b00010001,
-      (0b0001, 0b0, 0b010) => 0b00010010,
-      (0b0001, 0b0, 0b011) => 0b00010011,
-      (0b0001, 0b0, 0b100) => 0b00010100,
-      (0b0001, 0b0, 0b101) => 0b00010101,
-      (0b0001, 0b0, 0b110) => 0b00010110,
-      (0b0001, 0b0, 0b111) => 0b00010111,
-      (0b0001, 0b1, 0b000) => 0b00011000,
-      (0b0001, 0b1, 0b001) => 0b00011001,
-      (0b0001, 0b1, 0b010) => 0b00011010,
-      (0b0001, 0b1, 0b011) => 0b00011011,
-      (0b0001, 0b1, 0b100) => 0b00011100,
-      (0b0001, 0b1, 0b101) => 0b00011101,
-      (0b0001, 0b1, 0b110) => 0b00011110,
-      (0b0001, 0b1, 0b111) => 0b00011111,
-      (0b0010, 0b0, 0b000) => 0b00100000,
-      (0b0010, 0b0, 0b001) => 0b00100001,
-      (0b0010, 0b0, 0b010) => 0b00100010,
-      (0b0010, 0b0, 0b011) => 0b00100011,
-      (0b0010, 0b0, 0b100) => 0b00100100,
-      (0b0010, 0b0, 0b101) => 0b00100101,
-      (0b0010, 0b0, 0b110) => 0b00100110,
-      (0b0010, 0b0, 0b111) => 0b00100111,
-      (0b0010, 0b1, 0b000) => 0b00101000,
-      (0b0010, 0b1, 0b001) => 0b00101001,
-      (0b0010, 0b1, 0b010) => 0b00101010,
-      (0b0010, 0b1, 0b011) => 0b00101011,
-      (0b0010, 0b1, 0b100) => 0b00101100,
-      (0b0010, 0b1, 0b101) => 0b00101101,
-      (0b0010, 0b1, 0b110) => 0b00101110,
-      (0b0010, 0b1, 0b111) => 0b00101111,
-      (0b0011, 0b0, 0b000) => 0b00110000,
-      (0b0011, 0b0, 0b001) => 0b00110001,
-      (0b0011, 0b0, 0b010) => 0b00110010,
-      (0b0011, 0b0, 0b011) => 0b00110011,
-      (0b0011, 0b0, 0b100) => 0b00110100,
-      (0b0011, 0b0, 0b101) => 0b00110101,
-      (0b0011, 0b0, 0b110) => 0b00110110,
-      (0b0011, 0b0, 0b111) => 0b00110111,
-      (0b0011, 0b1, 0b000) => 0b00111000,
-      (0b0011, 0b1, 0b001) => 0b00111001,
-      (0b0011, 0b1, 0b010) => 0b00111010,
-      (0b0011, 0b1, 0b011) => 0b00111011,
-      (0b0011, 0b1, 0b100) => 0b00111100,
-      (0b0011, 0b1, 0b101) => 0b00111101,
-      (0b0011, 0b1, 0b110) => 0b00111110,
-      (0b0011, 0b1, 0b111) => 0b00111111,
-      (0b0100, 0b0, 0b000) => 0b01000000,
-      (0b0100, 0b0, 0b001) => 0b01000001,
-      (0b0100, 0b0, 0b010) => 0b01000010,
-      (0b0100, 0b0, 0b011) => 0b01000011,
-      (0b0100, 0b0, 0b100) => 0b01000100,
-      (0b0100, 0b0, 0b101) => 0b01000101,
-      (0b0100, 0b0, 0b110) => 0b01000110,
-      (0b0100, 0b0, 0b111) => 0b01000111,
-      (0b0100, 0b1, 0b000) => 0b01001000,
-      (0b0100, 0b1, 0b001) => 0b01001001,
-      (0b0100, 0b1, 0b010) => 0b01001010,
-      (0b0100, 0b1, 0b011) => 0b01001011,
-      (0b0100, 0b1, 0b100) => 0b01001100,
-      (0b0100, 0b1, 0b101) => 0b01001101,
-      (0b0100, 0b1, 0b110) => 0b01001110,
-      (0b0100, 0b1, 0b111) => 0b01001111,
-      (0b0101, 0b0, 0b000) => 0b01010000,
-      (0b0101, 0b0, 0b001) => 0b01010001,
-      (0b0101, 0b0, 0b010) => 0b01010010,
-      (0b0101, 0b0, 0b011) => 0b01010011,
-      (0b0101, 0b0, 0b100) => 0b01010100,
-      (0b0101, 0b0, 0b101) => 0b01010101,
-      (0b0101, 0b0, 0b110) => 0b01010110,
-      (0b0101, 0b0, 0b111) => 0b01010111,
-      (0b0101, 0b1, 0b000) => 0b01011000,
-      (0b0101, 0b1, 0b001) => 0b01011001,
-      (0b0101, 0b1, 0b010) => 0b01011010,
-      (0b0101, 0b1, 0b011) => 0b01011011,
-      (0b0101, 0b1, 0b100) => 0b01011100,
-      (0b0101, 0b1, 0b101) => 0b01011101,
-      (0b0101, 0b1, 0b110) => 0b01011110,
-      (0b0101, 0b1, 0b111) => 0b01011111,
-      (0b0110, 0b0, 0b000) => 0b01100000,
-      (0b0110, 0b0, 0b001) => 0b01100001,
-      (0b0110, 0b0, 0b010) => 0b01100010,
-      (0b0110, 0b0, 0b011) => 0b01100011,
-      (0b0110, 0b0, 0b100) => 0b01100100,
-      (0b0110, 0b0, 0b101) => 0b01100101,
-      (0b0110, 0b0, 0b110) => 0b01100110,
-      (0b0110, 0b0, 0b111) => 0b01100111,
-      (0b0110, 0b1, 0b000) => 0b01101000,
-      (0b0110, 0b1, 0b001) => 0b01101001,
-      (0b0110, 0b1, 0b010) => 0b01101010,
-      (0b0110, 0b1, 0b011) => 0b01101011,
-      (0b0110, 0b1, 0b100) => 0b01101100,
-      (0b0110, 0b1, 0b101) => 0b01101101,
-      (0b0110, 0b1, 0b110) => 0b01101110,
-      (0b0110, 0b1, 0b111) => 0b01101111,
-      (0b0111, 0b0, 0b000) => 0b01110000,
-      (0b0111, 0b0, 0b001) => 0b01110001,
-      (0b0111, 0b0, 0b010) => 0b01110010,
-      (0b0111, 0b0, 0b011) => 0b01110011,
-      (0b0111, 0b0, 0b100) => 0b01110100,
-      (0b0111, 0b0, 0b101) => 0b01110101,
-      (0b0111, 0b0, 0b110) => 0b01110110,
-      (0b0111, 0b0, 0b111) => 0b01110111,
-      (0b0111, 0b1, 0b000) => 0b01111000,
-      (0b0111, 0b1, 0b001) => 0b01111001,
-      (0b0111, 0b1, 0b010) => 0b01111010,
-      (0b0111, 0b1, 0b011) => 0b01111011,
-      (0b0111, 0b1, 0b100) => 0b01111100,
-      (0b0111, 0b1, 0b101) => 0b01111101,
-      (0b0111, 0b1, 0b110) => 0b01111110,
-      (0b0111, 0b1, 0b111) => 0b01111111,
-      (0b1000, 0b0, 0b000) => 0b10000000,
-      (0b1000, 0b0, 0b001) => 0b10000001,
-      (0b1000, 0b0, 0b010) => 0b10000010,
-      (0b1000, 0b0, 0b011) => 0b10000011,
-      (0b1000, 0b0, 0b100) => 0b10000100,
-      (0b1000, 0b0, 0b101) => 0b10000101,
-      (0b1000, 0b0, 0b110) => 0b10000110,
-      (0b1000, 0b0, 0b111) => 0b10000111,
-      (0b1000, 0b1, 0b000) => 0b10001000,
-      (0b1000, 0b1, 0b001) => 0b10001001,
-      (0b1000, 0b1, 0b010) => 0b10001010,
-      (0b1000, 0b1, 0b011) => 0b10001011,
-      (0b1000, 0b1, 0b100) => 0b10001100,
-      (0b1000, 0b1, 0b101) => 0b10001101,
-      (0b1000, 0b1, 0b110) => 0b10001110,
-      (0b1000, 0b1, 0b111) => 0b10001111,
-      (0b1001, 0b0, 0b000) => 0b10010000,
-      (0b1001, 0b0, 0b001) => 0b10010001,
-      (0b1001, 0b0, 0b010) => 0b10010010,
-      (0b1001, 0b0, 0b011) => 0b10010011,
-      (0b1001, 0b0, 0b100) => 0b10010100,
-      (0b1001, 0b0, 0b101) => 0b10010101,
-      (0b1001, 0b0, 0b110) => 0b10010110,
-      (0b1001, 0b0, 0b111) => 0b10010111,
-      (0b1001, 0b1, 0b000) => 0b10011000,
-      (0b1001, 0b1, 0b001) => 0b10011001,
-      (0b1001, 0b1, 0b010) => 0b10011010,
-      (0b1001, 0b1, 0b011) => 0b10011011,
-      (0b1001, 0b1, 0b100) => 0b10011100,
-      (0b1001, 0b1, 0b101) => 0b10011101,
-      (0b1001, 0b1, 0b110) => 0b10011110,
-      (0b1001, 0b1, 0b111) => 0b10011111,
-      (0b1010, 0b0, 0b000) => 0b10100000,
-      (0b1010, 0b0, 0b001) => 0b10100001,
-      (0b1010, 0b0, 0b010) => 0b10100010,
-      (0b1010, 0b0, 0b011) => 0b10100011,
-      (0b1010, 0b0, 0b100) => 0b10100100,
-      (0b1010, 0b0, 0b101) => 0b10100101,
-      (0b1010, 0b0, 0b110) => 0b10100110,
-      (0b1010, 0b0, 0b111) => 0b10100111,
-      (0b1010, 0b1, 0b000) => 0b10101000,
-      (0b1010, 0b1, 0b001) => 0b10101001,
-      (0b1010, 0b1, 0b010) => 0b10101010,
-      (0b1010, 0b1, 0b011) => 0b10101011,
-      (0b1010, 0b1, 0b100) => 0b10101100,
-      (0b1010, 0b1, 0b101) => 0b10101101,
-      (0b1010, 0b1, 0b110) => 0b10101110,
-      (0b1010, 0b1, 0b111) => 0b10101111,
-      (0b1011, 0b0, 0b000) => 0b10110000,
-      (0b1011, 0b0, 0b001) => 0b10110001,
-      (0b1011, 0b0, 0b010) => 0b10110010,
-      (0b1011, 0b0, 0b011) => 0b10110011,
-      (0b1011, 0b0, 0b100) => 0b10110100,
-      (0b1011, 0b0, 0b101) => 0b10110101,
-      (0b1011, 0b0, 0b110) => 0b10110110,
-      (0b1011, 0b0, 0b111) => 0b10110111,
-      (0b1011, 0b1, 0b000) => 0b10111000,
-      (0b1011, 0b1, 0b001) => 0b10111001,
-      (0b1011, 0b1, 0b010) => 0b10111010,
-      (0b1011, 0b1, 0b011) => 0b10111011,
-      (0b1011, 0b1, 0b100) => 0b10111100,
-      (0b1011, 0b1, 0b101) => 0b10111101,
-      (0b1011, 0b1, 0b110) => 0b10111110,
-      (0b1011, 0b1, 0b111) => 0b10111111,
-      (0b1100, 0b0, 0b000) => 0b11000000,
-      (0b1100, 0b0, 0b001) => 0b11000001,
-      (0b1100, 0b0, 0b010) => 0b11000010,
-      (0b1100, 0b0, 0b011) => 0b11000011,
-      (0b1100, 0b0, 0b100) => 0b11000100,
-      (0b1100, 0b0, 0b101) => 0b11000101,
-      (0b1100, 0b0, 0b110) => 0b11000110,
-      (0b1100, 0b0, 0b111) => 0b11000111,
-      (0b1100, 0b1, 0b000) => 0b11001000,
-      (0b1100, 0b1, 0b001) => 0b11001001,
-      (0b1100, 0b1, 0b010) => 0b11001010,
-      (0b1100, 0b1, 0b011) => 0b11001011,
-      (0b1100, 0b1, 0b100) => 0b11001100,
-      (0b1100, 0b1, 0b101) => 0b11001101,
-      (0b1100, 0b1, 0b110) => 0b11001110,
-      (0b1100, 0b1, 0b111) => 0b11001111,
-      (0b1101, 0b0, 0b000) => 0b11010000,
-      (0b1101, 0b0, 0b001) => 0b11010001,
-      (0b1101, 0b0, 0b010) => 0b11010010,
-      (0b1101, 0b0, 0b011) => 0b11010011,
-      (0b1101, 0b0, 0b100) => 0b11010100,
-      (0b1101, 0b0, 0b101) => 0b11010101,
-      (0b1101, 0b0, 0b110) => 0b11010110,
-      (0b1101, 0b0, 0b111) => 0b11010111,
-      (0b1101, 0b1, 0b000) => 0b11011000,
-      (0b1101, 0b1, 0b001) => 0b11011001,
-      (0b1101, 0b1, 0b010) => 0b11011010,
-      (0b1101, 0b1, 0b011) => 0b11011011,
-      (0b1101, 0b1, 0b100) => 0b11011100,
-      (0b1101, 0b1, 0b101) => 0b11011101,
-      (0b1101, 0b1, 0b110) => 0b11011110,
-      (0b1101, 0b1, 0b111) => 0b11011111,
-      (0b1110, 0b0, 0b000) => 0b11100000,
-      (0b1110, 0b0, 0b001) => 0b11100001,
-      (0b1110, 0b0, 0b010) => 0b11100010,
-      (0b1110, 0b0, 0b011) => 0b11100011,
-      (0b1110, 0b0, 0b100) => 0b11100100,
-      (0b1110, 0b0, 0b101) => 0b11100101,
-      (0b1110, 0b0, 0b110) => 0b11100110,
-      (0b1110, 0b0, 0b111) => 0b11100111,
-      (0b1110, 0b1, 0b000) => 0b11101000,
-      (0b1110, 0b1, 0b001) => 0b11101001,
-      (0b1110, 0b1, 0b010) => 0b11101010,
-      (0b1110, 0b1, 0b011) => 0b11101011,
-      (0b1110, 0b1, 0b100) => 0b11101100,
-      (0b1110, 0b1, 0b101) => 0b11101101,
-      (0b1110, 0b1, 0b110) => 0b11101110,
-      (0b1110, 0b1, 0b111) => 0b11101111,
-      (0b1111, 0b0, 0b000) => 0b11110000,
-      (0b1111, 0b0, 0b001) => 0b11110001,
-      (0b1111, 0b0, 0b010) => 0b11110010,
-      (0b1111, 0b0, 0b011) => 0b11110011,
-      (0b1111, 0b0, 0b100) => 0b11110100,
-      (0b1111, 0b0, 0b101) => 0b11110101,
-      (0b1111, 0b0, 0b110) => 0b11110110,
-      (0b1111, 0b0, 0b111) => 0b11110111,
-      (0b1111, 0b1, 0b000) => 0b11111000,
-      (0b1111, 0b1, 0b001) => 0b11111001,
-      (0b1111, 0b1, 0b010) => 0b11111010,
-      (0b1111, 0b1, 0b011) => 0b11111011,
-      (0b1111, 0b1, 0b100) => 0b11111100,
-      (0b1111, 0b1, 0b101) => 0b11111101,
-      (0b1111, 0b1, 0b110) => 0b11111110,
-      (0b1111, 0b1, 0b111) => 0b11111111,
-    }
-  }
-⟧
-
 end IxVM

From e310ff7e8444e3785fedebbbc94f648c5f258950 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Fri, 13 Feb 2026 11:43:36 -0300
Subject: [PATCH 2/7] ixon exprs

---
 Ix/IxVM/Ixon.lean | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index 7907ab55..03fe341e 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -2,4 +2,45 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
+def ixon := ⟦
+  -- Universe list for variable-length universe arguments
+  enum UnivList {
+    Cons(G, &UnivList),
+    Nil
+  }
+
+  -- Ixon expression type (alpha-invariant Lean expressions)
+  -- Names are stripped, binder info is in metadata
+  enum Expr {
+    -- Sort/Type at a universe level (index into Constant.univs table)
+    Srt(G),
+    -- De Bruijn variable
+    Var(G),
+    -- Reference to top-level constant with universe arguments
+    -- First G is index into Constant.refs, UnivList are indices into Constant.univs
+    Ref(G, &UnivList),
+    -- Mutual recursion reference (index within block) with universe arguments
+    -- First G is rec index, UnivList are indices into Constant.univs
+    Rec(G, &UnivList),
+    -- Projection: (struct_type_ref_idx, field_index, struct_value)
+    -- First G is index into Constant.refs table for the struct type
+    Prj(G, G, &Expr),
+    -- String literal - index into Constant.refs table (address points to blob)
+    Str(G),
+    -- Natural number literal - index into Constant.refs table (address points to blob)
+    Nat(G),
+    -- Application: (function, argument)
+    App(&Expr, &Expr),
+    -- Lambda: (binder_type, body)
+    Lam(&Expr, &Expr),
+    -- Forall/Pi: (binder_type, body)
+    All(&Expr, &Expr),
+    -- Let: (non_dep, type, value, body)
+    -- non_dep is 0 for dep, 1 for non_dep
+    Let(G, &Expr, &Expr, &Expr),
+    -- Reference to shared subexpression in MutualBlock.sharing[idx]
+    Share(G)
+  }
+⟧
+
 end IxVM

From 931132abec7a0ce37dbcabddad690035ff0500dd Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sat, 14 Feb 2026 10:06:51 -0300
Subject: [PATCH 3/7] U64

---
 Ix/IxVM.lean                 |   2 +
 Ix/IxVM/Blake3.lean          |  13 +---
 Ix/IxVM/ByteStream.lean      | 126 +++------------------------------
 Ix/IxVM/Ixon.lean            |  41 +++--------
 Ix/IxVM/IxonDeserialize.lean |   3 +
 Ix/IxVM/IxonSerialize.lean   |   2 +
 Ix/IxVM/U64.lean             | 132 +++++++++++++++++++++++++++++++++++
 7 files changed, 161 insertions(+), 158 deletions(-)
 create mode 100644 Ix/IxVM/U64.lean

diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean
index b8ffb9cc..8d10f97a 100644
--- a/Ix/IxVM.lean
+++ b/Ix/IxVM.lean
@@ -4,6 +4,7 @@ import Ix.IxVM.Blake3
 import Ix.IxVM.Ixon
 import Ix.IxVM.IxonSerialize
 import Ix.IxVM.IxonDeserialize
+import Ix.IxVM.U64
 
 namespace IxVM
 
@@ -37,6 +38,7 @@ def ixVM : Except Aiur.Global Aiur.Toplevel := do
   let vm ← vm.merge ixon
   let vm ← vm.merge ixonSerialize
   let vm ← vm.merge ixonDeserialize
+  let vm ← vm.merge u64
   vm.merge entrypoints
 
 end IxVM
diff --git a/Ix/IxVM/Blake3.lean b/Ix/IxVM/Blake3.lean
index bf6945b3..219d0560 100644
--- a/Ix/IxVM/Blake3.lean
+++ b/Ix/IxVM/Blake3.lean
@@ -108,12 +108,12 @@ def blake3 := ⟦
       (ByteStream.Nil, 0, _) => Layer.Push(store(layer), block_digest),
 
       (ByteStream.Nil, _, _) =>
-        let flags = CHUNK_END + chunk_count_is_zero(chunk_count) * ROOT + eq_zero(chunk_index - block_index) * CHUNK_START;
+        let flags = CHUNK_END + u64_is_zero(chunk_count) * ROOT + eq_zero(chunk_index - block_index) * CHUNK_START;
         Layer.Push(store(layer), blake3_compress(block_digest, block_buffer, chunk_count, block_index, flags)),
 
       (ByteStream.Cons(head, input_ptr), 63, 1023) =>
         let input = load(input_ptr);
-        let flags = ROOT * byte_stream_is_empty(input) * chunk_count_is_zero(chunk_count) + CHUNK_END;
+        let flags = ROOT * byte_stream_is_empty(input) * u64_is_zero(chunk_count) + CHUNK_END;
         let block_buffer = assign_block_value(block_buffer, block_index, head);
         let IV = [[103, 230, 9, 106], [133, 174, 103, 187], [114, 243, 110, 60], [58, 245, 79, 165], [127, 82, 14, 81], [140, 104, 5, 155], [171, 217, 131, 31], [25, 205, 224, 91]];
         let empty_buffer = [[0; 4]; 16];
@@ -124,7 +124,7 @@ def blake3 := ⟦
         let input = load(input_ptr);
         let block_buffer = assign_block_value(block_buffer, block_index, head);
         let chunk_end_flag = byte_stream_is_empty(input) * CHUNK_END;
-        let root_flag = byte_stream_is_empty(input) * chunk_count_is_zero(chunk_count) * ROOT;
+        let root_flag = byte_stream_is_empty(input) * u64_is_zero(chunk_count) * ROOT;
         let chunk_start_flag = eq_zero(chunk_index - block_index) * CHUNK_START;
         let flags = chunk_end_flag + root_flag + chunk_start_flag;
         let block_digest = blake3_compress(
@@ -368,13 +368,6 @@ def blake3 := ⟦
     ]
   }
 
-  fn chunk_count_is_zero(chunk_count: [G; 8]) -> G {
-    match chunk_count {
-      [0, 0, 0, 0, 0, 0, 0, 0] => 1,
-      _ => 0,
-    }
-  }
-
   fn assign_block_value(block: [[G; 4]; 16], idx: G, val: G) -> [[G; 4]; 16] {
     match idx {
       0 => set(block, 0, set(block[0], 0, val)),
diff --git a/Ix/IxVM/ByteStream.lean b/Ix/IxVM/ByteStream.lean
index 768ddbc0..3c00bd36 100644
--- a/Ix/IxVM/ByteStream.lean
+++ b/Ix/IxVM/ByteStream.lean
@@ -8,6 +8,14 @@ def byteStream := ⟦
     Nil
   }
 
+  fn byte_streams_concat(a: ByteStream, b: ByteStream) -> ByteStream {
+    match a {
+      ByteStream.Nil => b,
+      ByteStream.Cons(byte, rest) =>
+        ByteStream.Cons(byte, store(concat_byte_streams(load(rest), b))),
+    }
+  }
+
   fn byte_stream_length(bytes: ByteStream) -> [G; 8] {
     match bytes {
       ByteStream.Nil => [0; 8],
@@ -33,124 +41,6 @@ def byteStream := ⟦
       ByteStream.Nil => 1,
     }
   }
-
-  -- Reconstructs a byte from its bits in little-endian.
-  fn u8_recompose(bits: [G; 8]) -> G {
-    let [b0, b1, b2, b3, b4, b5, b6, b7] = bits;
-    b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6 + 128 * b7
-  }
-
-  fn u32_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let [a0, a1, a2, a3] = a;
-    let [b0, b1, b2, b3] = b;
-
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(a0, b0);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(a1, b1);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Byte 2
-    let (sum2, overflow2) = u8_add(a2, b2);
-    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
-    let carry3 = u8_xor(overflow2, carry2a);
-
-    -- Byte 3
-    let (sum3, _x) = u8_add(a3, b3);
-    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
-
-    [sum0, sum1_with_carry, sum2_with_carry, sum3_with_carry]
-  }
-
-  fn u32_xor(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let c0 = u8_xor(a[0], b[0]);
-    let c1 = u8_xor(a[1], b[1]);
-    let c2 = u8_xor(a[2], b[2]);
-    let c3 = u8_xor(a[3], b[3]);
-    [c0, c1, c2, c3]
-  }
-
-  fn u32_and(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let c0 = u8_and(a[0], b[0]);
-    let c1 = u8_and(a[1], b[1]);
-    let c2 = u8_and(a[2], b[2]);
-    let c3 = u8_and(a[3], b[3]);
-    [c0, c1, c2, c3]
-  }
-
-  -- Computes the successor of an `u64` assumed to be properly represented in
-  -- little-endian bytes. If that's not the case, this implementation has UB.
-  fn relaxed_u64_succ(bytes: [G; 8]) -> [G; 8] {
-    let [b0, b1, b2, b3, b4, b5, b6, b7] = bytes;
-    match b0 {
-      255 => match b1 {
-        255 => match b2 {
-          255 => match b3 {
-            255 => match b4 {
-              255 => match b5 {
-                255 => match b6 {
-                  255 => match b7 {
-                    255 => [0, 0, 0, 0, 0, 0, 0, 0],
-                    _ => [0, 0, 0, 0, 0, 0, 0, b7 + 1],
-                  },
-                  _ => [0, 0, 0, 0, 0, 0, b6 + 1, b7],
-                },
-                _ => [0, 0, 0, 0, 0, b5 + 1, b6, b7],
-              },
-              _ => [0, 0, 0, 0, b4 + 1, b5, b6, b7],
-            },
-            _ => [0, 0, 0, b3 + 1, b4, b5, b6, b7],
-          },
-          _ => [0, 0, b2 + 1, b3, b4, b5, b6, b7],
-        },
-        _ => [0, b1 + 1, b2, b3, b4, b5, b6, b7],
-      },
-      _ => [b0 + 1, b1, b2, b3, b4, b5, b6, b7],
-    }
-  }
-
-  fn relaxed_u64_be_add_2_bytes(u64: [G; 8], bs: [G; 2]) -> [G; 8] {
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(u64[7], bs[1]);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(u64[6], bs[0]);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Other bytes
-    let (sum2, carry3) = u8_add(u64[5], carry2);
-    let (sum3, carry4) = u8_add(u64[4], carry3);
-    let (sum4, carry5) = u8_add(u64[3], carry4);
-    let (sum5, carry6) = u8_add(u64[2], carry5);
-    let (sum6, carry7) = u8_add(u64[1], carry6);
-    let (sum7, _carry8) = u8_add(u64[0], carry7);
-
-    [sum7, sum6, sum5, sum4, sum3, sum2, sum1, sum0]
-  }
-
-  fn u32_be_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(a[3], b[3]);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(a[2], b[2]);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Byte 2
-    let (sum2, overflow2) = u8_add(a[1], b[1]);
-    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
-    let carry3 = u8_xor(overflow2, carry2a);
-
-    -- Byte 3
-    let (sum3, _x) = u8_add(a[0], b[0]);
-    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
-
-    [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
-  }
 ⟧
 
 end IxVM
diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index 03fe341e..a9a4cbfe 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -3,43 +3,24 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixon := ⟦
-  -- Universe list for variable-length universe arguments
-  enum UnivList {
-    Cons(G, &UnivList),
+  enum U64List {
+    Cons([G; 8], &U64List),
     Nil
   }
 
-  -- Ixon expression type (alpha-invariant Lean expressions)
-  -- Names are stripped, binder info is in metadata
   enum Expr {
-    -- Sort/Type at a universe level (index into Constant.univs table)
-    Srt(G),
-    -- De Bruijn variable
-    Var(G),
-    -- Reference to top-level constant with universe arguments
-    -- First G is index into Constant.refs, UnivList are indices into Constant.univs
-    Ref(G, &UnivList),
-    -- Mutual recursion reference (index within block) with universe arguments
-    -- First G is rec index, UnivList are indices into Constant.univs
-    Rec(G, &UnivList),
-    -- Projection: (struct_type_ref_idx, field_index, struct_value)
-    -- First G is index into Constant.refs table for the struct type
-    Prj(G, G, &Expr),
-    -- String literal - index into Constant.refs table (address points to blob)
-    Str(G),
-    -- Natural number literal - index into Constant.refs table (address points to blob)
-    Nat(G),
-    -- Application: (function, argument)
+    Srt([G; 8]),
+    Var([G; 8]),
+    Ref([G; 8], &U64List),
+    Rec([G; 8], &U64List),
+    Prj([G; 8], [G; 8], &Expr),
+    Str([G; 8]),
+    Nat([G; 8]),
     App(&Expr, &Expr),
-    -- Lambda: (binder_type, body)
     Lam(&Expr, &Expr),
-    -- Forall/Pi: (binder_type, body)
     All(&Expr, &Expr),
-    -- Let: (non_dep, type, value, body)
-    -- non_dep is 0 for dep, 1 for non_dep
-    Let(G, &Expr, &Expr, &Expr),
-    -- Reference to shared subexpression in MutualBlock.sharing[idx]
-    Share(G)
+    Let([G; 8], &Expr, &Expr, &Expr),
+    Share([G; 8])
   }
 ⟧
 
diff --git a/Ix/IxVM/IxonDeserialize.lean b/Ix/IxVM/IxonDeserialize.lean
index 7907ab55..c71f1a79 100644
--- a/Ix/IxVM/IxonDeserialize.lean
+++ b/Ix/IxVM/IxonDeserialize.lean
@@ -2,4 +2,7 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
+def ixonDeserialize := ⟦
+⟧
+
 end IxVM
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index 7907ab55..16de9d15 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -2,4 +2,6 @@ import Ix.Aiur.Meta
 
 namespace IxVM
 
+def ixonSerialize := ⟦
+⟧
 end IxVM
diff --git a/Ix/IxVM/U64.lean b/Ix/IxVM/U64.lean
new file mode 100644
index 00000000..63ffc363
--- /dev/null
+++ b/Ix/IxVM/U64.lean
@@ -0,0 +1,132 @@
+import Ix.Aiur.Meta
+
+namespace IxVM
+
+def u64 := ⟦
+  fn u64_is_zero(x: [G; 8]) -> G {
+    match x {
+      [0, 0, 0, 0, 0, 0, 0, 0] => 1,
+      _ => 0,
+    }
+  }
+
+  -- Reconstructs a byte from its bits in little-endian.
+  fn u8_recompose(bits: [G; 8]) -> G {
+    let [b0, b1, b2, b3, b4, b5, b6, b7] = bits;
+    b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6 + 128 * b7
+  }
+
+  fn u32_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let [a0, a1, a2, a3] = a;
+    let [b0, b1, b2, b3] = b;
+
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(a0, b0);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(a1, b1);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Byte 2
+    let (sum2, overflow2) = u8_add(a2, b2);
+    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
+    let carry3 = u8_xor(overflow2, carry2a);
+
+    -- Byte 3
+    let (sum3, _x) = u8_add(a3, b3);
+    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
+
+    [sum0, sum1_with_carry, sum2_with_carry, sum3_with_carry]
+  }
+
+  fn u32_xor(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let c0 = u8_xor(a[0], b[0]);
+    let c1 = u8_xor(a[1], b[1]);
+    let c2 = u8_xor(a[2], b[2]);
+    let c3 = u8_xor(a[3], b[3]);
+    [c0, c1, c2, c3]
+  }
+
+  fn u32_and(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let c0 = u8_and(a[0], b[0]);
+    let c1 = u8_and(a[1], b[1]);
+    let c2 = u8_and(a[2], b[2]);
+    let c3 = u8_and(a[3], b[3]);
+    [c0, c1, c2, c3]
+  }
+
+  -- Computes the successor of an `u64` assumed to be properly represented in
+  -- little-endian bytes. If that's not the case, this implementation has UB.
+  fn relaxed_u64_succ(bytes: [G; 8]) -> [G; 8] {
+    let [b0, b1, b2, b3, b4, b5, b6, b7] = bytes;
+    match b0 {
+      255 => match b1 {
+        255 => match b2 {
+          255 => match b3 {
+            255 => match b4 {
+              255 => match b5 {
+                255 => match b6 {
+                  255 => match b7 {
+                    255 => [0, 0, 0, 0, 0, 0, 0, 0],
+                    _ => [0, 0, 0, 0, 0, 0, 0, b7 + 1],
+                  },
+                  _ => [0, 0, 0, 0, 0, 0, b6 + 1, b7],
+                },
+                _ => [0, 0, 0, 0, 0, b5 + 1, b6, b7],
+              },
+              _ => [0, 0, 0, 0, b4 + 1, b5, b6, b7],
+            },
+            _ => [0, 0, 0, b3 + 1, b4, b5, b6, b7],
+          },
+          _ => [0, 0, b2 + 1, b3, b4, b5, b6, b7],
+        },
+        _ => [0, b1 + 1, b2, b3, b4, b5, b6, b7],
+      },
+      _ => [b0 + 1, b1, b2, b3, b4, b5, b6, b7],
+    }
+  }
+
+  fn relaxed_u64_be_add_2_bytes(u64: [G; 8], bs: [G; 2]) -> [G; 8] {
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(u64[7], bs[1]);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(u64[6], bs[0]);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Other bytes
+    let (sum2, carry3) = u8_add(u64[5], carry2);
+    let (sum3, carry4) = u8_add(u64[4], carry3);
+    let (sum4, carry5) = u8_add(u64[3], carry4);
+    let (sum5, carry6) = u8_add(u64[2], carry5);
+    let (sum6, carry7) = u8_add(u64[1], carry6);
+    let (sum7, _carry8) = u8_add(u64[0], carry7);
+
+    [sum7, sum6, sum5, sum4, sum3, sum2, sum1, sum0]
+  }
+
+  fn u32_be_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(a[3], b[3]);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(a[2], b[2]);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Byte 2
+    let (sum2, overflow2) = u8_add(a[1], b[1]);
+    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
+    let carry3 = u8_xor(overflow2, carry2a);
+
+    -- Byte 3
+    let (sum3, _x) = u8_add(a[0], b[0]);
+    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
+
+    [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
+  }
+⟧
+
+end IxVM

From 204bc99e9ae78207eb1ac1bc373bd5ff38174456 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sun, 15 Feb 2026 18:34:46 -0300
Subject: [PATCH 4/7] `put_tag0` and `put_u64_le`

---
 Ix/IxVM/ByteStream.lean    |  4 ++--
 Ix/IxVM/IxonSerialize.lean | 34 ++++++++++++++++++++++++++++++++++
 Ix/IxVM/U64.lean           | 15 ++++++++++++++-
 3 files changed, 50 insertions(+), 3 deletions(-)

diff --git a/Ix/IxVM/ByteStream.lean b/Ix/IxVM/ByteStream.lean
index 3c00bd36..501fe954 100644
--- a/Ix/IxVM/ByteStream.lean
+++ b/Ix/IxVM/ByteStream.lean
@@ -8,11 +8,11 @@ def byteStream := ⟦
     Nil
   }
 
-  fn byte_streams_concat(a: ByteStream, b: ByteStream) -> ByteStream {
+  fn byte_stream_concat(a: ByteStream, b: ByteStream) -> ByteStream {
     match a {
       ByteStream.Nil => b,
       ByteStream.Cons(byte, rest) =>
-        ByteStream.Cons(byte, store(concat_byte_streams(load(rest), b))),
+        ByteStream.Cons(byte, store(byte_stream_concat(load(rest), b))),
     }
   }
 
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index 16de9d15..a7e0d1ff 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -3,5 +3,39 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixonSerialize := ⟦
+  fn put_u64_le(bs: [G; 8], num_bytes: G) -> ByteStream {
+    match num_bytes {
+      0 => ByteStream.Nil,
+      _ =>
+        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))),
+    }
+  }
+
+  fn put_tag0(bs: [G; 8]) -> 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)),
+      _ =>
+        let head = 128 + (byte_count - 1);
+        ByteStream.Cons(head, store(put_u64_le(bs, byte_count))),
+    }
+  }
+
+  fn put_tag4(flag: G, bs: [G; 8]) -> 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)),
+      _ =>
+        let head = flag * 16 + 8 + (byte_count - 1);
+        let bs_bytes = put_u64_le(bs, byte_count);
+        ByteStream.Cons(head, store(bs_bytes)),
+    }
+  }
 ⟧
 end IxVM
diff --git a/Ix/IxVM/U64.lean b/Ix/IxVM/U64.lean
index 63ffc363..f0b00ae3 100644
--- a/Ix/IxVM/U64.lean
+++ b/Ix/IxVM/U64.lean
@@ -3,6 +3,20 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def u64 := ⟦
+  -- Count bytes needed to represent a u64 (0-8)
+  fn u64_byte_count(x: [G; 8]) -> G {
+    match x {
+      [_, 0, 0, 0, 0, 0, 0, 0] => 1,
+      [_, _, 0, 0, 0, 0, 0, 0] => 2,
+      [_, _, _, 0, 0, 0, 0, 0] => 3,
+      [_, _, _, _, 0, 0, 0, 0] => 4,
+      [_, _, _, _, _, 0, 0, 0] => 5,
+      [_, _, _, _, _, _, 0, 0] => 6,
+      [_, _, _, _, _, _, _, 0] => 7,
+      _ => 8,
+    }
+  }
+
   fn u64_is_zero(x: [G; 8]) -> G {
     match x {
       [0, 0, 0, 0, 0, 0, 0, 0] => 1,
@@ -126,7 +140,6 @@ def u64 := ⟦
     let (sum3_with_carry, _x) = u8_add(sum3, carry3);
 
     [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
-  }
 ⟧
 
 end IxVM

From 1180ec37cadf775ed58053ac954ba51712486671 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Feb 2026 17:56:31 -0300
Subject: [PATCH 5/7] `put_expr`

---
 Ix/IxVM/ByteStream.lean    |   6 +-
 Ix/IxVM/Ixon.lean          |   5 --
 Ix/IxVM/IxonSerialize.lean | 147 +++++++++++++++++++++++++++++++++++++
 Ix/IxVM/U64.lean           |  12 +++
 4 files changed, 162 insertions(+), 8 deletions(-)

diff --git a/Ix/IxVM/ByteStream.lean b/Ix/IxVM/ByteStream.lean
index 501fe954..a7bf1693 100644
--- a/Ix/IxVM/ByteStream.lean
+++ b/Ix/IxVM/ByteStream.lean
@@ -11,15 +11,15 @@ def byteStream := ⟦
   fn byte_stream_concat(a: ByteStream, b: ByteStream) -> ByteStream {
     match a {
       ByteStream.Nil => b,
-      ByteStream.Cons(byte, rest) =>
-        ByteStream.Cons(byte, store(byte_stream_concat(load(rest), b))),
+      ByteStream.Cons(byte, &rest) =>
+        ByteStream.Cons(byte, store(byte_stream_concat(rest, b))),
     }
   }
 
   fn byte_stream_length(bytes: ByteStream) -> [G; 8] {
     match bytes {
       ByteStream.Nil => [0; 8],
-      ByteStream.Cons(_, rest) => relaxed_u64_succ(byte_stream_length(load(rest))),
+      ByteStream.Cons(_, &rest) => relaxed_u64_succ(byte_stream_length(rest)),
     }
   }
 
diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index a9a4cbfe..319c8b1e 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -3,11 +3,6 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixon := ⟦
-  enum U64List {
-    Cons([G; 8], &U64List),
-    Nil
-  }
-
   enum Expr {
     Srt([G; 8]),
     Var([G; 8]),
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index a7e0d1ff..e2fda205 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -3,6 +3,84 @@ import Ix.Aiur.Meta
 namespace IxVM
 
 def ixonSerialize := ⟦
+  fn put_expr(expr: Expr) -> ByteStream {
+    match expr {
+      -- Srt: Tag4(0x0, univ_idx)
+      Expr.Srt(univ_idx) => put_tag4(0x0, univ_idx),
+
+      -- Var: Tag4(0x1, idx)
+      Expr.Var(idx) => put_tag4(0x1, idx),
+
+      -- 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)),
+
+      -- 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)),
+
+      -- 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)),
+
+      -- Str: Tag4(0x5, ref_idx)
+      Expr.Str(ref_idx) => put_tag4(0x5, ref_idx),
+
+      -- Nat: Tag4(0x6, ref_idx)
+      Expr.Nat(ref_idx) => put_tag4(0x6, ref_idx),
+
+      -- 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),
+
+      -- 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),
+
+      -- 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),
+
+      -- 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)
+          )
+        ),
+
+      -- Share: Tag4(0xB, idx)
+      Expr.Share(idx) => put_tag4(0xB, idx),
+    }
+  }
+
   fn put_u64_le(bs: [G; 8], num_bytes: G) -> ByteStream {
     match num_bytes {
       0 => ByteStream.Nil,
@@ -37,5 +115,74 @@ def ixonSerialize := ⟦
         ByteStream.Cons(head, store(bs_bytes)),
     }
   }
+
+  -- Serialize field list (each element as Tag0)
+  fn put_u64_list(list: U64List) -> 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),
+    }
+  }
+
+  -- Count nested App expressions
+  fn app_telescope_count(expr: Expr) -> [G; 8] {
+    match expr {
+      Expr.App(&func, _) => relaxed_u64_succ(app_telescope_count(func)),
+      _ => [0; 8],
+    }
+  }
+
+  -- Count nested Lam expressions
+  fn lam_telescope_count(expr: Expr) -> [G; 8] {
+    match expr {
+      Expr.Lam(_, &body) => relaxed_u64_succ(lam_telescope_count(body)),
+      _ => [0; 8],
+    }
+  }
+
+  -- Count nested All expressions
+  fn all_telescope_count(expr: Expr) -> [G; 8] {
+    match expr {
+      Expr.All(_, &body) => relaxed_u64_succ(all_telescope_count(body)),
+      _ => [0; 8],
+    }
+  }
+
+  -- Serialize App telescope body (function, then all args in order)
+  fn put_app_telescope(expr: Expr) -> 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),
+    }
+  }
+
+  -- Serialize Lam telescope body (all types, then body)
+  fn put_lam_telescope(expr: Expr) -> 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),
+    }
+  }
+
+  -- Serialize All telescope body (all types, then body)
+  fn put_all_telescope(expr: Expr) -> 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),
+    }
+  }
 ⟧
+
 end IxVM
diff --git a/Ix/IxVM/U64.lean b/Ix/IxVM/U64.lean
index f0b00ae3..212d44a0 100644
--- a/Ix/IxVM/U64.lean
+++ b/Ix/IxVM/U64.lean
@@ -140,6 +140,18 @@ def u64 := ⟦
     let (sum3_with_carry, _x) = u8_add(sum3, carry3);
 
     [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
+
+  enum U64List {
+    Cons([G; 8], &U64List),
+    Nil
+  }
+
+  fn u64_list_length(xs: U64List) -> [G; 8] {
+    match xs {
+      U64List.Nil => [0; 8],
+      U64List.Cons(_, rest) => relaxed_u64_succ(u64_list_length(load(rest))),
+    }
+  }
 ⟧
 
 end IxVM

From 273385b648559384ba4c2dd313bd735edaa55358 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Feb 2026 18:12:46 -0300
Subject: [PATCH 6/7] removed U64 file

---
 Ix/IxVM.lean            |   2 -
 Ix/IxVM/ByteStream.lean | 151 ++++++++++++++++++++++++++++++++++++++
 Ix/IxVM/U64.lean        | 157 ----------------------------------------
 3 files changed, 151 insertions(+), 159 deletions(-)
 delete mode 100644 Ix/IxVM/U64.lean

diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean
index 8d10f97a..b8ffb9cc 100644
--- a/Ix/IxVM.lean
+++ b/Ix/IxVM.lean
@@ -4,7 +4,6 @@ import Ix.IxVM.Blake3
 import Ix.IxVM.Ixon
 import Ix.IxVM.IxonSerialize
 import Ix.IxVM.IxonDeserialize
-import Ix.IxVM.U64
 
 namespace IxVM
 
@@ -38,7 +37,6 @@ def ixVM : Except Aiur.Global Aiur.Toplevel := do
   let vm ← vm.merge ixon
   let vm ← vm.merge ixonSerialize
   let vm ← vm.merge ixonDeserialize
-  let vm ← vm.merge u64
   vm.merge entrypoints
 
 end IxVM
diff --git a/Ix/IxVM/ByteStream.lean b/Ix/IxVM/ByteStream.lean
index a7bf1693..fec0658b 100644
--- a/Ix/IxVM/ByteStream.lean
+++ b/Ix/IxVM/ByteStream.lean
@@ -41,6 +41,157 @@ def byteStream := ⟦
       ByteStream.Nil => 1,
     }
   }
+
+  -- Count bytes needed to represent a u64 (0-8)
+  fn u64_byte_count(x: [G; 8]) -> G {
+    match x {
+      [_, 0, 0, 0, 0, 0, 0, 0] => 1,
+      [_, _, 0, 0, 0, 0, 0, 0] => 2,
+      [_, _, _, 0, 0, 0, 0, 0] => 3,
+      [_, _, _, _, 0, 0, 0, 0] => 4,
+      [_, _, _, _, _, 0, 0, 0] => 5,
+      [_, _, _, _, _, _, 0, 0] => 6,
+      [_, _, _, _, _, _, _, 0] => 7,
+      _ => 8,
+    }
+  }
+
+  fn u64_is_zero(x: [G; 8]) -> G {
+    match x {
+      [0, 0, 0, 0, 0, 0, 0, 0] => 1,
+      _ => 0,
+    }
+  }
+
+  -- Reconstructs a byte from its bits in little-endian.
+  fn u8_recompose(bits: [G; 8]) -> G {
+    let [b0, b1, b2, b3, b4, b5, b6, b7] = bits;
+    b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6 + 128 * b7
+  }
+
+  fn u32_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let [a0, a1, a2, a3] = a;
+    let [b0, b1, b2, b3] = b;
+
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(a0, b0);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(a1, b1);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Byte 2
+    let (sum2, overflow2) = u8_add(a2, b2);
+    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
+    let carry3 = u8_xor(overflow2, carry2a);
+
+    -- Byte 3
+    let (sum3, _x) = u8_add(a3, b3);
+    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
+
+    [sum0, sum1_with_carry, sum2_with_carry, sum3_with_carry]
+  }
+
+  fn u32_xor(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let c0 = u8_xor(a[0], b[0]);
+    let c1 = u8_xor(a[1], b[1]);
+    let c2 = u8_xor(a[2], b[2]);
+    let c3 = u8_xor(a[3], b[3]);
+    [c0, c1, c2, c3]
+  }
+
+  fn u32_and(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    let c0 = u8_and(a[0], b[0]);
+    let c1 = u8_and(a[1], b[1]);
+    let c2 = u8_and(a[2], b[2]);
+    let c3 = u8_and(a[3], b[3]);
+    [c0, c1, c2, c3]
+  }
+
+  -- Computes the successor of an `u64` assumed to be properly represented in
+  -- little-endian bytes. If that's not the case, this implementation has UB.
+  fn relaxed_u64_succ(bytes: [G; 8]) -> [G; 8] {
+    let [b0, b1, b2, b3, b4, b5, b6, b7] = bytes;
+    match b0 {
+      255 => match b1 {
+        255 => match b2 {
+          255 => match b3 {
+            255 => match b4 {
+              255 => match b5 {
+                255 => match b6 {
+                  255 => match b7 {
+                    255 => [0, 0, 0, 0, 0, 0, 0, 0],
+                    _ => [0, 0, 0, 0, 0, 0, 0, b7 + 1],
+                  },
+                  _ => [0, 0, 0, 0, 0, 0, b6 + 1, b7],
+                },
+                _ => [0, 0, 0, 0, 0, b5 + 1, b6, b7],
+              },
+              _ => [0, 0, 0, 0, b4 + 1, b5, b6, b7],
+            },
+            _ => [0, 0, 0, b3 + 1, b4, b5, b6, b7],
+          },
+          _ => [0, 0, b2 + 1, b3, b4, b5, b6, b7],
+        },
+        _ => [0, b1 + 1, b2, b3, b4, b5, b6, b7],
+      },
+      _ => [b0 + 1, b1, b2, b3, b4, b5, b6, b7],
+    }
+  }
+
+  fn relaxed_u64_be_add_2_bytes(u64: [G; 8], bs: [G; 2]) -> [G; 8] {
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(u64[7], bs[1]);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(u64[6], bs[0]);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Other bytes
+    let (sum2, carry3) = u8_add(u64[5], carry2);
+    let (sum3, carry4) = u8_add(u64[4], carry3);
+    let (sum4, carry5) = u8_add(u64[3], carry4);
+    let (sum5, carry6) = u8_add(u64[2], carry5);
+    let (sum6, carry7) = u8_add(u64[1], carry6);
+    let (sum7, _carry8) = u8_add(u64[0], carry7);
+
+    [sum7, sum6, sum5, sum4, sum3, sum2, sum1, sum0]
+  }
+
+  fn u32_be_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
+    -- Byte 0, no initial carry
+    let (sum0, carry1) = u8_add(a[3], b[3]);
+
+    -- Byte 1
+    let (sum1, overflow1) = u8_add(a[2], b[2]);
+    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
+    let carry2 = u8_xor(overflow1, carry1a);
+
+    -- Byte 2
+    let (sum2, overflow2) = u8_add(a[1], b[1]);
+    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
+    let carry3 = u8_xor(overflow2, carry2a);
+
+    -- Byte 3
+    let (sum3, _x) = u8_add(a[0], b[0]);
+    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
+
+    [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
+  }
+
+  enum U64List {
+    Cons([G; 8], &U64List),
+    Nil
+  }
+
+  fn u64_list_length(xs: U64List) -> [G; 8] {
+    match xs {
+      U64List.Nil => [0; 8],
+      U64List.Cons(_, rest) => relaxed_u64_succ(u64_list_length(load(rest))),
+    }
+  }
 ⟧
 
 end IxVM
diff --git a/Ix/IxVM/U64.lean b/Ix/IxVM/U64.lean
deleted file mode 100644
index 212d44a0..00000000
--- a/Ix/IxVM/U64.lean
+++ /dev/null
@@ -1,157 +0,0 @@
-import Ix.Aiur.Meta
-
-namespace IxVM
-
-def u64 := ⟦
-  -- Count bytes needed to represent a u64 (0-8)
-  fn u64_byte_count(x: [G; 8]) -> G {
-    match x {
-      [_, 0, 0, 0, 0, 0, 0, 0] => 1,
-      [_, _, 0, 0, 0, 0, 0, 0] => 2,
-      [_, _, _, 0, 0, 0, 0, 0] => 3,
-      [_, _, _, _, 0, 0, 0, 0] => 4,
-      [_, _, _, _, _, 0, 0, 0] => 5,
-      [_, _, _, _, _, _, 0, 0] => 6,
-      [_, _, _, _, _, _, _, 0] => 7,
-      _ => 8,
-    }
-  }
-
-  fn u64_is_zero(x: [G; 8]) -> G {
-    match x {
-      [0, 0, 0, 0, 0, 0, 0, 0] => 1,
-      _ => 0,
-    }
-  }
-
-  -- Reconstructs a byte from its bits in little-endian.
-  fn u8_recompose(bits: [G; 8]) -> G {
-    let [b0, b1, b2, b3, b4, b5, b6, b7] = bits;
-    b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6 + 128 * b7
-  }
-
-  fn u32_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let [a0, a1, a2, a3] = a;
-    let [b0, b1, b2, b3] = b;
-
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(a0, b0);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(a1, b1);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Byte 2
-    let (sum2, overflow2) = u8_add(a2, b2);
-    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
-    let carry3 = u8_xor(overflow2, carry2a);
-
-    -- Byte 3
-    let (sum3, _x) = u8_add(a3, b3);
-    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
-
-    [sum0, sum1_with_carry, sum2_with_carry, sum3_with_carry]
-  }
-
-  fn u32_xor(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let c0 = u8_xor(a[0], b[0]);
-    let c1 = u8_xor(a[1], b[1]);
-    let c2 = u8_xor(a[2], b[2]);
-    let c3 = u8_xor(a[3], b[3]);
-    [c0, c1, c2, c3]
-  }
-
-  fn u32_and(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    let c0 = u8_and(a[0], b[0]);
-    let c1 = u8_and(a[1], b[1]);
-    let c2 = u8_and(a[2], b[2]);
-    let c3 = u8_and(a[3], b[3]);
-    [c0, c1, c2, c3]
-  }
-
-  -- Computes the successor of an `u64` assumed to be properly represented in
-  -- little-endian bytes. If that's not the case, this implementation has UB.
-  fn relaxed_u64_succ(bytes: [G; 8]) -> [G; 8] {
-    let [b0, b1, b2, b3, b4, b5, b6, b7] = bytes;
-    match b0 {
-      255 => match b1 {
-        255 => match b2 {
-          255 => match b3 {
-            255 => match b4 {
-              255 => match b5 {
-                255 => match b6 {
-                  255 => match b7 {
-                    255 => [0, 0, 0, 0, 0, 0, 0, 0],
-                    _ => [0, 0, 0, 0, 0, 0, 0, b7 + 1],
-                  },
-                  _ => [0, 0, 0, 0, 0, 0, b6 + 1, b7],
-                },
-                _ => [0, 0, 0, 0, 0, b5 + 1, b6, b7],
-              },
-              _ => [0, 0, 0, 0, b4 + 1, b5, b6, b7],
-            },
-            _ => [0, 0, 0, b3 + 1, b4, b5, b6, b7],
-          },
-          _ => [0, 0, b2 + 1, b3, b4, b5, b6, b7],
-        },
-        _ => [0, b1 + 1, b2, b3, b4, b5, b6, b7],
-      },
-      _ => [b0 + 1, b1, b2, b3, b4, b5, b6, b7],
-    }
-  }
-
-  fn relaxed_u64_be_add_2_bytes(u64: [G; 8], bs: [G; 2]) -> [G; 8] {
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(u64[7], bs[1]);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(u64[6], bs[0]);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Other bytes
-    let (sum2, carry3) = u8_add(u64[5], carry2);
-    let (sum3, carry4) = u8_add(u64[4], carry3);
-    let (sum4, carry5) = u8_add(u64[3], carry4);
-    let (sum5, carry6) = u8_add(u64[2], carry5);
-    let (sum6, carry7) = u8_add(u64[1], carry6);
-    let (sum7, _carry8) = u8_add(u64[0], carry7);
-
-    [sum7, sum6, sum5, sum4, sum3, sum2, sum1, sum0]
-  }
-
-  fn u32_be_add(a: [G; 4], b: [G; 4]) -> [G; 4] {
-    -- Byte 0, no initial carry
-    let (sum0, carry1) = u8_add(a[3], b[3]);
-
-    -- Byte 1
-    let (sum1, overflow1) = u8_add(a[2], b[2]);
-    let (sum1_with_carry, carry1a) = u8_add(sum1, carry1);
-    let carry2 = u8_xor(overflow1, carry1a);
-
-    -- Byte 2
-    let (sum2, overflow2) = u8_add(a[1], b[1]);
-    let (sum2_with_carry, carry2a) = u8_add(sum2, carry2);
-    let carry3 = u8_xor(overflow2, carry2a);
-
-    -- Byte 3
-    let (sum3, _x) = u8_add(a[0], b[0]);
-    let (sum3_with_carry, _x) = u8_add(sum3, carry3);
-
-    [sum3_with_carry, sum2_with_carry, sum1_with_carry, sum0]
-
-  enum U64List {
-    Cons([G; 8], &U64List),
-    Nil
-  }
-
-  fn u64_list_length(xs: U64List) -> [G; 8] {
-    match xs {
-      U64List.Nil => [0; 8],
-      U64List.Cons(_, rest) => relaxed_u64_succ(u64_list_length(load(rest))),
-    }
-  }
-⟧
-
-end IxVM

From 44530b735bb76bb66bebbb46431ac78631daa2b1 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Fri, 20 Feb 2026 12:17:10 -0300
Subject: [PATCH 7/7] tests for the IxVM with `lake exe test-ixvm`

---
 .github/workflows/ci.yml  |  1 +
 .github/workflows/nix.yml |  1 +
 Ix/IxVM.lean              | 36 ++++++++++++++++++------------------
 README.md                 |  3 ++-
 Tests/AiurHashes.lean     |  2 --
 Tests/IxVM.lean           |  6 ++++++
 Tests/IxVMMain.lean       |  4 ++++
 Tests/Main.lean           |  2 ++
 flake.nix                 |  2 ++
 lakefile.lean             |  3 +++
 10 files changed, 39 insertions(+), 21 deletions(-)
 create mode 100644 Tests/IxVM.lean
 create mode 100644 Tests/IxVMMain.lean

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d0f506b1..0ef1861e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -42,6 +42,7 @@ jobs:
           lake test -- cli
       - run: lake exe test-aiur
       - run: lake exe test-aiur-hashes
+      - run: lake exe test-ixvm
       - name: Check lean.h.hash
         run: lake run check-lean-h-hash
 
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index c8e0bb42..2f87c928 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -36,6 +36,7 @@ jobs:
       # Expensive tests are only built in Nix to save time
       - run: nix build .#test-aiur --accept-flake-config
       - run: nix build .#test-aiur-hashes --accept-flake-config
+      - run: nix build .#test-ixvm --accept-flake-config
 
   # Tests Nix devShell support on Ubuntu
   nix-devshell:
diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean
index b8ffb9cc..8cab2964 100644
--- a/Ix/IxVM.lean
+++ b/Ix/IxVM.lean
@@ -10,24 +10,24 @@ namespace IxVM
 def entrypoints := ⟦
   /- # Test entrypoints -/
 
-  fn ixon_blake3_test(h: [[G; 4]; 8]) {
-    let key = [
-      h[0][0], h[0][1], h[0][2], h[0][3],
-      h[1][0], h[1][1], h[1][2], h[1][3],
-      h[2][0], h[2][1], h[2][2], h[2][3],
-      h[3][0], h[3][1], h[3][2], h[3][3],
-      h[4][0], h[4][1], h[4][2], h[4][3],
-      h[5][0], h[5][1], h[5][2], h[5][3],
-      h[6][0], h[6][1], h[6][2], h[6][3],
-      h[7][0], h[7][1], h[7][2], h[7][3]
-    ];
-    let (idx, len) = io_get_info(key);
-    let bytes_unconstrained = read_byte_stream(idx, len);
-    let ixon_unconstrained = deserialize(bytes_unconstrained);
-    let bytes = serialize(ixon_unconstrained);
-    let bytes_hash = blake3(bytes);
-    assert_eq!(h, bytes_hash);
-  }
+  -- fn ixon_blake3_test(h: [[G; 4]; 8]) {
+  --   let key = [
+  --     h[0][0], h[0][1], h[0][2], h[0][3],
+  --     h[1][0], h[1][1], h[1][2], h[1][3],
+  --     h[2][0], h[2][1], h[2][2], h[2][3],
+  --     h[3][0], h[3][1], h[3][2], h[3][3],
+  --     h[4][0], h[4][1], h[4][2], h[4][3],
+  --     h[5][0], h[5][1], h[5][2], h[5][3],
+  --     h[6][0], h[6][1], h[6][2], h[6][3],
+  --     h[7][0], h[7][1], h[7][2], h[7][3]
+  --   ];
+  --   let (idx, len) = io_get_info(key);
+  --   let bytes_unconstrained = read_byte_stream(idx, len);
+  --   let ixon_unconstrained = deserialize(bytes_unconstrained);
+  --   let bytes = serialize(ixon_unconstrained);
+  --   let bytes_hash = blake3(bytes);
+  --   assert_eq!(h, bytes_hash);
+  -- }
 
   /- # Benchmark entrypoints -/
 ⟧
diff --git a/README.md b/README.md
index dc82bf87..23b3a498 100644
--- a/README.md
+++ b/README.md
@@ -190,10 +190,11 @@ Compiler performance benchmarks are tracked at https://bencher.dev/console/proje
 - `lake test -- cli` runs CLI integration tests
 - `lake test -- rust-compile` runs the Rust cross-compilation diagnostic
 
-To run the Aiur and Aiur-Hashes tests, which are slower, run:
+To run tests that involve zk proofs, which are slower, run:
 
 - `lake exe test-aiur`
 - `lake exe test-aiur-hashes`
+- `lake exe test-ixvm`
 
 **Rust tests:** `cargo test`
 
diff --git a/Tests/AiurHashes.lean b/Tests/AiurHashes.lean
index 69259370..d7df00bc 100644
--- a/Tests/AiurHashes.lean
+++ b/Tests/AiurHashes.lean
@@ -2,8 +2,6 @@ import Tests.Common
 import Ix.IxVM.ByteStream
 import Ix.IxVM.Blake3
 import Ix.IxVM.Sha256
-import Ix.Aiur.Simple
-import Ix.Aiur.Compile
 import Blake3
 
 @[extern "rs_sha256"]
diff --git a/Tests/IxVM.lean b/Tests/IxVM.lean
new file mode 100644
index 00000000..4d38aa8d
--- /dev/null
+++ b/Tests/IxVM.lean
@@ -0,0 +1,6 @@
+import Tests.Common
+import Ix.IxVM
+
+def Tests.IxVM.suite := [
+  mkAiurTests IxVM.ixVM []
+]
diff --git a/Tests/IxVMMain.lean b/Tests/IxVMMain.lean
new file mode 100644
index 00000000..5af85eed
--- /dev/null
+++ b/Tests/IxVMMain.lean
@@ -0,0 +1,4 @@
+import Tests.IxVM
+
+def main (args : List String) : IO UInt32 := do
+  LSpec.lspecIO (.ofList [("ixvm", Tests.IxVM.suite)]) args
diff --git a/Tests/Main.lean b/Tests/Main.lean
index 9329dc96..4b2d4e52 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -1,5 +1,6 @@
 import Tests.Aiur
 import Tests.AiurHashes
+import Tests.IxVM
 import Tests.ByteArray
 import Tests.Ix.Ixon
 import Tests.Ix.Claim
@@ -26,6 +27,7 @@ opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize
 def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
   ("aiur", Tests.Aiur.suite),
   ("aiur-hashes", Tests.AiurHashes.suite),
+  ("ixvm", Tests.IxVM.suite),
   ("ffi", Tests.FFI.suite),
   ("byte-array", Tests.ByteArray.suite),
   ("ixon", Tests.Ixon.suite),
diff --git a/flake.nix b/flake.nix
index efcabe8c..a51fc428 100644
--- a/flake.nix
+++ b/flake.nix
@@ -125,6 +125,7 @@
         ixTest = lake2nix.mkPackage (lakeBinArgs // {name = "IxTests";});
         testAiur = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur";});
         testAiurHashes = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur-hashes";});
+        testIxVM = lake2nix.mkPackage (lakeBinArgs // {name = "test-ixvm";});
         benchAiur = lake2nix.mkPackage (lakeBinArgs // {name = "bench-aiur";});
         benchBlake3 = lake2nix.mkPackage (lakeBinArgs // {name = "bench-blake3";});
         benchShardMap = lake2nix.mkPackage (lakeBinArgs // {name = "bench-shardmap";});
@@ -141,6 +142,7 @@
           test = ixTest;
           test-aiur = testAiur;
           test-aiur-hashes = testAiurHashes;
+          test-ixvm = testIxVM;
           # Ix benches
           bench-aiur = benchAiur;
           bench-blake3 = benchBlake3;
diff --git a/lakefile.lean b/lakefile.lean
index 0da72927..ada02900 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -38,6 +38,9 @@ lean_exe «test-aiur» where
 lean_exe «test-aiur-hashes» where
   root := `Tests.AiurHashesMain
 
+lean_exe «test-ixvm» where
+  root := `Tests.IxVMMain
+
 end Tests
 
 section IxApplications