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/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..fec0658b 100644 --- a/Ix/IxVM/ByteStream.lean +++ b/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 diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean index c920e22d..319c8b1e 100644 --- a/Ix/IxVM/Ixon.lean +++ b/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
), -- 0x3X, expression reference - -- ERec(Nat, Vec
), -- 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), -- 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]) } ⟧ diff --git a/Ix/IxVM/IxonDeserialize.lean b/Ix/IxVM/IxonDeserialize.lean index 583c3f33..c71f1a79 100644 --- a/Ix/IxVM/IxonDeserialize.lean +++ b/Ix/IxVM/IxonDeserialize.lean @@ -2,606 +2,7 @@ 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..e2fda205 100644 --- a/Ix/IxVM/IxonSerialize.lean +++ b/Ix/IxVM/IxonSerialize.lean @@ -2,428 +2,185 @@ 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 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, + _ => + 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)), + } + } + + -- 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), } } - 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))))), + -- 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), } } - 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, + -- 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), } } ⟧ 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