Ixon Expr serialization

.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
 

.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:

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 -/
 ⟧

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)),

Ix/IxVM/ByteStream.lean

@@ -8,10 +8,18 @@ def byteStream := ⟦
     Nil
   }
 
+  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(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)),
     }
   }
 
@@ -34,6 +42,27 @@ def byteStream := ⟦
     }
   }
 
+  -- 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;
@@ -151,6 +180,18 @@ def byteStream := ⟦
 
     [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

Ix/IxVM/Ixon.lean

@@ -3,72 +3,19 @@ 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
+  enum Expr {
+    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),
+    Lam(&Expr, &Expr),
+    All(&Expr, &Expr),
+    Let([G; 8], &Expr, &Expr, &Expr),
+    Share([G; 8])
   }
 ⟧