From 6d64c826ef52c67de7d4c29a417f0bde45d59c57 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 16 Jul 2024 09:52:44 +0200 Subject: [PATCH 1/2] Turn machine statements into block statements. --- linker/src/lib.rs | 2 +- std/machines/binary.asm | 24 +++++++++---------- std/machines/hash/poseidon_bn254.asm | 8 +++---- std/machines/hash/poseidon_gl.asm | 2 +- std/machines/hash/poseidon_gl_memory.asm | 2 +- std/machines/shift.asm | 2 +- test_data/asm/block_machine_cache_miss.asm | 2 +- test_data/asm/book/instructions.asm | 2 +- test_data/asm/book/instructions2.asm | 2 +- test_data/asm/dynamic_vadcop.asm | 2 +- test_data/asm/multiple_signatures.asm | 2 +- test_data/asm/permutations/link_merging.asm | 2 +- .../vm_to_block_multiple_links.asm | 2 +- test_data/asm/side_effects.asm | 2 +- test_data/asm/vm_instr_param_mapping.asm | 2 +- test_data/asm/vm_to_block_array.asm | 2 +- .../asm/vm_to_block_multiple_interfaces.asm | 2 +- test_data/asm/vm_to_block_to_block.asm | 4 ++-- .../asm/vm_to_block_unique_interface.asm | 4 ++-- test_data/asm/vm_to_vm_to_block.asm | 2 +- 20 files changed, 36 insertions(+), 36 deletions(-) diff --git a/linker/src/lib.rs b/linker/src/lib.rs index a1173a2d3..4747225de 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -638,7 +638,7 @@ machine NegativeForUnsigned { machine SubVM with latch: latch, operation_id: operation_id, min_degree: 64, max_degree: 128 { operation add5<0> x -> y; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; diff --git a/std/machines/binary.asm b/std/machines/binary.asm index 370e393e4..9871d8f73 100644 --- a/std/machines/binary.asm +++ b/std/machines/binary.asm @@ -10,8 +10,8 @@ machine ByteBinary with { operation run<0> P_operation, P_A, P_B -> P_C; - col fixed latch = [1]*; - col fixed operation_id = [0]*; + let latch: col = |i| 1; + let operation_id: col = |i| 0; let bit_counts = [256, 256, 3]; let min_degree = std::array::product(bit_counts); @@ -24,7 +24,7 @@ machine ByteBinary with let P_A: col = a; let P_B: col = b; let P_operation: col = op; - col fixed P_C(i) { + let P_C: col = |i| { match op(i) { 0 => a(i) & b(i), 1 => a(i) | b(i), @@ -45,19 +45,19 @@ machine Binary(byte_binary: ByteBinary) with operation xor<2> A, B -> C; - col witness operation_id; + let operation_id; unchanged_until(operation_id, latch); - col fixed latch(i) { if (i % 4) == 3 { 1 } else { 0 } }; - col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) }; + let latch: col = |i| { if (i % 4) == 3 { 1 } else { 0 } }; + let FACTOR: col = |i| { 1 << (((i + 1) % 4) * 8) }; - col witness A_byte; - col witness B_byte; - col witness C_byte; + let A_byte; + let B_byte; + let C_byte; - col witness A; - col witness B; - col witness C; + let A; + let B; + let C; A' = A * (1 - latch) + A_byte * FACTOR; B' = B * (1 - latch) + B_byte * FACTOR; diff --git a/std/machines/hash/poseidon_bn254.asm b/std/machines/hash/poseidon_bn254.asm index 3c5c54961..e417a3c6e 100644 --- a/std/machines/hash/poseidon_bn254.asm +++ b/std/machines/hash/poseidon_bn254.asm @@ -16,7 +16,7 @@ machine PoseidonBN254 with // hash functions. operation poseidon_permutation<0> state[0], state[1], state[2] -> output[0]; - col witness operation_id; + let operation_id; // Using parameters from https://eprint.iacr.org/2019/458.pdf // See https://extgit.iaik.tugraz.at/krypto/hadeshash/-/blob/master/code/poseidonperm_x5_254_3.sage @@ -34,9 +34,9 @@ machine PoseidonBN254 with let PARTIAL_ROUNDS = 57; let ROWS_PER_HASH = FULL_ROUNDS + PARTIAL_ROUNDS + 1; - pol constant L0 = [1] + [0]*; - pol constant FIRSTBLOCK(i) { if i % ROWS_PER_HASH == 0 { 1 } else { 0 } }; - pol constant LASTBLOCK(i) { if i % ROWS_PER_HASH == ROWS_PER_HASH - 1 { 1 } else { 0 } }; + let L0: col = |i| if i == 0 { 1 } else { 0 }; + let FIRSTBLOCK: col = |i| { if i % ROWS_PER_HASH == 0 { 1 } else { 0 } }; + let LASTBLOCK: col = |i| { if i % ROWS_PER_HASH == ROWS_PER_HASH - 1 { 1 } else { 0 } }; // Like LASTBLOCK, but also 1 in the last row of the table // Specified this way because we can't access the degree in the match statement pol constant LAST = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]* + [1]; diff --git a/std/machines/hash/poseidon_gl.asm b/std/machines/hash/poseidon_gl.asm index c082b1d51..dff512121 100644 --- a/std/machines/hash/poseidon_gl.asm +++ b/std/machines/hash/poseidon_gl.asm @@ -16,7 +16,7 @@ machine PoseidonGL with // hash functions. operation poseidon_permutation<0> state[0], state[1], state[2], state[3], state[4], state[5], state[6], state[7], state[8], state[9], state[10], state[11] -> output[0], output[1], output[2], output[3]; - col witness operation_id; + let operation_id; // Ported from: // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil diff --git a/std/machines/hash/poseidon_gl_memory.asm b/std/machines/hash/poseidon_gl_memory.asm index 9d945d090..290b82595 100644 --- a/std/machines/hash/poseidon_gl_memory.asm +++ b/std/machines/hash/poseidon_gl_memory.asm @@ -42,7 +42,7 @@ machine PoseidonGLMemory(mem: Memory, split_gl: SplitGL) with // Reads happen at the provided time step; writes happen at the next time step. operation poseidon_permutation<0> input_addr, output_addr, time_step ->; - col witness operation_id; + let operation_id; // Ported from: // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil diff --git a/std/machines/shift.asm b/std/machines/shift.asm index e498763b2..591da1533 100644 --- a/std/machines/shift.asm +++ b/std/machines/shift.asm @@ -44,7 +44,7 @@ machine Shift(byte_shift: ByteShift) with operation shr<1> A, B -> C; - col witness operation_id; + let operation_id; unchanged_until(operation_id, latch); col fixed latch(i) { if (i % 4) == 3 { 1 } else { 0 } }; diff --git a/test_data/asm/block_machine_cache_miss.asm b/test_data/asm/block_machine_cache_miss.asm index cf25bcc1d..4650f1e99 100644 --- a/test_data/asm/block_machine_cache_miss.asm +++ b/test_data/asm/block_machine_cache_miss.asm @@ -6,7 +6,7 @@ machine Arith with operation double<0> x -> y; operation square<1> x -> y; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col fixed X(i) {i}; col fixed DOUBLE(i) {2*i}; diff --git a/test_data/asm/book/instructions.asm b/test_data/asm/book/instructions.asm index babdc3936..9f9de5763 100644 --- a/test_data/asm/book/instructions.asm +++ b/test_data/asm/book/instructions.asm @@ -15,7 +15,7 @@ machine SubMachine with latch: latch, operation_id: operation_id { - col witness operation_id; + let operation_id; col fixed latch = [1]*; operation add<0> x, y -> z; diff --git a/test_data/asm/book/instructions2.asm b/test_data/asm/book/instructions2.asm index 73f16614e..e2f2dee80 100644 --- a/test_data/asm/book/instructions2.asm +++ b/test_data/asm/book/instructions2.asm @@ -3,7 +3,7 @@ machine SubMachine with latch: latch, operation_id: operation_id { - col witness operation_id; + let operation_id; col fixed latch = [1]*; operation add<0> x, y -> z; diff --git a/test_data/asm/dynamic_vadcop.asm b/test_data/asm/dynamic_vadcop.asm index 01f637ced..78076ea85 100644 --- a/test_data/asm/dynamic_vadcop.asm +++ b/test_data/asm/dynamic_vadcop.asm @@ -56,7 +56,7 @@ machine Arith with operation mul<1> x[0], x[1] -> y; col fixed latch = [1]*; - col witness operation_id; + let operation_id; col witness x[2]; col witness y; diff --git a/test_data/asm/multiple_signatures.asm b/test_data/asm/multiple_signatures.asm index 594998972..04e75de8d 100644 --- a/test_data/asm/multiple_signatures.asm +++ b/test_data/asm/multiple_signatures.asm @@ -9,7 +9,7 @@ machine Add with // The compiler enforces that there is an operation ID if there are // multiple operations, even though we want the constraints to be // the same in both cases... - col witness operation_id; + let operation_id; let latch = 1; // A and B provided => C will be the sum. diff --git a/test_data/asm/permutations/link_merging.asm b/test_data/asm/permutations/link_merging.asm index a0a77174b..f206d4152 100644 --- a/test_data/asm/permutations/link_merging.asm +++ b/test_data/asm/permutations/link_merging.asm @@ -2,7 +2,7 @@ machine SubMachine with latch: latch, operation_id: operation_id { - col witness operation_id; + let operation_id; col fixed latch = [1]*; operation add<0> x, y -> z; diff --git a/test_data/asm/permutations/vm_to_block_multiple_links.asm b/test_data/asm/permutations/vm_to_block_multiple_links.asm index 7bed5317a..d9dbdb825 100644 --- a/test_data/asm/permutations/vm_to_block_multiple_links.asm +++ b/test_data/asm/permutations/vm_to_block_multiple_links.asm @@ -54,7 +54,7 @@ machine Arith with operation sub<1> z, x -> y; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; diff --git a/test_data/asm/side_effects.asm b/test_data/asm/side_effects.asm index 1542a15c3..2348c679e 100644 --- a/test_data/asm/side_effects.asm +++ b/test_data/asm/side_effects.asm @@ -18,7 +18,7 @@ machine MemoryProxy with { operation mstore<0> addr, step, value ->; - col witness operation_id; + let operation_id; col fixed latch = [1]*; Byte2 byte2; diff --git a/test_data/asm/vm_instr_param_mapping.asm b/test_data/asm/vm_instr_param_mapping.asm index 9e9f717f6..be9bf5be2 100644 --- a/test_data/asm/vm_instr_param_mapping.asm +++ b/test_data/asm/vm_instr_param_mapping.asm @@ -23,7 +23,7 @@ machine AddVM with { operation add<0> x,y -> z; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; diff --git a/test_data/asm/vm_to_block_array.asm b/test_data/asm/vm_to_block_array.asm index 2ed39be39..18eecfdbd 100644 --- a/test_data/asm/vm_to_block_array.asm +++ b/test_data/asm/vm_to_block_array.asm @@ -28,7 +28,7 @@ machine Arith with operation mul<1> x[0], x[1] -> y; col fixed latch = [1]*; - col witness operation_id; + let operation_id; col witness x[2]; col witness y; diff --git a/test_data/asm/vm_to_block_multiple_interfaces.asm b/test_data/asm/vm_to_block_multiple_interfaces.asm index beaacb74d..38a48b184 100644 --- a/test_data/asm/vm_to_block_multiple_interfaces.asm +++ b/test_data/asm/vm_to_block_multiple_interfaces.asm @@ -9,7 +9,7 @@ machine Arith with operation sub<1> z, x -> y; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; diff --git a/test_data/asm/vm_to_block_to_block.asm b/test_data/asm/vm_to_block_to_block.asm index e04217618..6c0f68221 100644 --- a/test_data/asm/vm_to_block_to_block.asm +++ b/test_data/asm/vm_to_block_to_block.asm @@ -5,7 +5,7 @@ machine Inc with { operation inc<0> x -> y; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; @@ -24,7 +24,7 @@ machine Assert1 with // Increment x by calling into inc machine link => y = inc.inc(x); - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; diff --git a/test_data/asm/vm_to_block_unique_interface.asm b/test_data/asm/vm_to_block_unique_interface.asm index c2592336c..59b879229 100644 --- a/test_data/asm/vm_to_block_unique_interface.asm +++ b/test_data/asm/vm_to_block_unique_interface.asm @@ -7,7 +7,7 @@ machine Binary with operation or<1> x, y -> z; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; @@ -28,7 +28,7 @@ machine Arith with operation sub<1> x, y -> z; - col witness operation_id; + let operation_id; col fixed latch = [1]*; col witness x; col witness y; diff --git a/test_data/asm/vm_to_vm_to_block.asm b/test_data/asm/vm_to_vm_to_block.asm index df5fd9b19..c2db9ac48 100644 --- a/test_data/asm/vm_to_vm_to_block.asm +++ b/test_data/asm/vm_to_vm_to_block.asm @@ -59,7 +59,7 @@ machine Arith with operation mul<1> x1, x2 -> y; col fixed latch = [1]*; - col witness operation_id; + let operation_id; col witness x1; col witness x2; col witness y; From 93c7601f70b0dfa36f19ec9453f12972ebe8e5ce Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Sep 2024 14:07:05 +0000 Subject: [PATCH 2/2] fix tests --- linker/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/linker/src/lib.rs b/linker/src/lib.rs index 4747225de..7265ac700 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -705,7 +705,7 @@ namespace main__rom(4); pol constant operation_id = [0]*; pol constant latch = [1]*; namespace main_vm(64..128); - pol commit operation_id; + let operation_id; pol constant latch = [1]*; pol commit x; pol commit y; @@ -982,7 +982,7 @@ namespace main__rom(32); pol constant operation_id = [0]*; pol constant latch = [1]*; namespace main_submachine(32); - pol commit operation_id; + let operation_id; pol constant latch = [1]*; pol commit x; pol commit y;