diff --git a/linker/src/lib.rs b/linker/src/lib.rs index 9999fa042..362dac016 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -879,7 +879,7 @@ namespace main_vm(64..128); fn permutation_instructions() { let expected = r#"namespace main(128); let _operation_id; - query |__i| std::prover::provide_if_unknown(_operation_id, __i, || 13); + query |__i| std::prover::provide_if_unknown(_operation_id, __i, || 9); pol constant _block_enforcer_last_step = [0]* + [1]; let _operation_id_no_change = (1 - _block_enforcer_last_step) * (1 - instr_return); _operation_id_no_change * (_operation_id' - _operation_id) = 0; @@ -896,7 +896,6 @@ namespace main_vm(64..128); pol commit reg_write_Z_B; pol commit B; pol commit instr_or; - pol commit instr_or_into_B; pol commit instr_assert_eq; std::constraints::make_conditional(X = Y, instr_assert_eq); pol commit instr__jump_to_operation; @@ -923,35 +922,33 @@ namespace main_vm(64..128); Z = read_Z_A * A + read_Z_B * B + read_Z_pc * pc + Z_const + Z_read_free * Z_free_value; pol constant first_step = [1] + [0]*; A' = reg_write_X_A * X + reg_write_Y_A * Y + reg_write_Z_A * Z + instr__reset * 0 + (1 - (reg_write_X_A + reg_write_Y_A + reg_write_Z_A + instr__reset)) * A; - B' = reg_write_X_B * X + reg_write_Y_B * Y + reg_write_Z_B * Z + instr_or_into_B * B' + instr__reset * 0 + (1 - (reg_write_X_B + reg_write_Y_B + reg_write_Z_B + instr_or_into_B + instr__reset)) * B; + B' = reg_write_X_B * X + reg_write_Y_B * Y + reg_write_Z_B * Z + instr__reset * 0 + (1 - (reg_write_X_B + reg_write_Y_B + reg_write_Z_B + instr__reset)) * B; pol commit pc_update; pc_update = instr__jump_to_operation * _operation_id + instr__loop * pc + instr_return * 0 + (1 - (instr__jump_to_operation + instr__loop + instr_return)) * (pc + 1); pc' = (1 - first_step') * pc_update; pol commit X_free_value; pol commit Y_free_value; pol commit Z_free_value; - instr_or_into_B $ [0, X, Y, B'] is main_bin::latch * main_bin::sel[0] $ [main_bin::operation_id, main_bin::A, main_bin::B, main_bin::C]; - 1 $ [0, pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, instr_or, instr_or_into_B, instr_assert_eq, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_B, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_pc] in main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_Y_A, main__rom::p_reg_write_Z_A, main__rom::p_reg_write_X_B, main__rom::p_reg_write_Y_B, main__rom::p_reg_write_Z_B, main__rom::p_instr_or, main__rom::p_instr_or_into_B, main__rom::p_instr_assert_eq, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_B, main__rom::p_read_X_pc, main__rom::p_Y_const, main__rom::p_Y_read_free, main__rom::p_read_Y_A, main__rom::p_read_Y_B, main__rom::p_read_Y_pc, main__rom::p_Z_const, main__rom::p_Z_read_free, main__rom::p_read_Z_A, main__rom::p_read_Z_B, main__rom::p_read_Z_pc]; - instr_or $ [0, X, Y, Z] is main_bin::latch * main_bin::sel[1] $ [main_bin::operation_id, main_bin::A, main_bin::B, main_bin::C]; + 1 $ [0, pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, instr_or, instr_assert_eq, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_B, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_pc] in main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_Y_A, main__rom::p_reg_write_Z_A, main__rom::p_reg_write_X_B, main__rom::p_reg_write_Y_B, main__rom::p_reg_write_Z_B, main__rom::p_instr_or, main__rom::p_instr_assert_eq, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_B, main__rom::p_read_X_pc, main__rom::p_Y_const, main__rom::p_Y_read_free, main__rom::p_read_Y_A, main__rom::p_read_Y_B, main__rom::p_read_Y_pc, main__rom::p_Z_const, main__rom::p_Z_read_free, main__rom::p_read_Z_A, main__rom::p_read_Z_B, main__rom::p_read_Z_pc]; + instr_or $ [0, X, Y, Z] is main_bin::latch * main_bin::sel[0] $ [main_bin::operation_id, main_bin::A, main_bin::B, main_bin::C]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(128); - pol constant p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] + [13]*; - pol constant p_X_const = [0, 0, 2, 0, 1, 0, 3, 0, 2, 0, 1, 0, 0, 0] + [0]*; + pol constant p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] + [9]*; + pol constant p_X_const = [0, 0, 2, 0, 1, 0, 3, 0, 0, 0] + [0]*; pol constant p_X_read_free = [0]*; - pol constant p_Y_const = [0, 0, 3, 3, 2, 3, 4, 7, 3, 3, 2, 3, 0, 0] + [0]*; + pol constant p_Y_const = [0, 0, 3, 3, 2, 3, 4, 7, 0, 0] + [0]*; pol constant p_Y_read_free = [0]*; pol constant p_Z_const = [0]*; - pol constant p_Z_read_free = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; - pol constant p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; - pol constant p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; - pol constant p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; - pol constant p_instr_assert_eq = [0, 0, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 0] + [0]*; - pol constant p_instr_or = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; - pol constant p_instr_or_into_B = [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0] + [0]*; - pol constant p_instr_return = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; - pol constant p_read_X_A = [0, 0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0] + [0]*; - pol constant p_read_X_B = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0] + [0]*; + pol constant p_Z_read_free = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0] + [0]*; + pol constant p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; + pol constant p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; + pol constant p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; + pol constant p_instr_assert_eq = [0, 0, 0, 1, 0, 1, 0, 1, 0, 0] + [0]*; + pol constant p_instr_or = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0] + [0]*; + pol constant p_instr_return = [0, 0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; + pol constant p_read_X_A = [0, 0, 0, 1, 0, 1, 0, 1, 0, 0] + [0]*; + pol constant p_read_X_B = [0]*; pol constant p_read_X_pc = [0]*; pol constant p_read_Y_A = [0]*; pol constant p_read_Y_B = [0]*; @@ -963,7 +960,7 @@ namespace main__rom(128); pol constant p_reg_write_X_B = [0]*; pol constant p_reg_write_Y_A = [0]*; pol constant p_reg_write_Y_B = [0]*; - pol constant p_reg_write_Z_A = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; + pol constant p_reg_write_Z_A = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0] + [0]*; pol constant p_reg_write_Z_B = [0]*; pol constant operation_id = [0]*; pol constant latch = [1]*; @@ -971,6 +968,7 @@ namespace main_bin(128); pol commit operation_id; pol constant latch(i) { if i % 8 == 7 { 1 } else { 0 } }; let sum_sel = std::array::sum(sel); + std::utils::force_bool(sum_sel); pol constant FACTOR(i) { 1 << (i + 1) % 8 * 4 }; let a = |i| i % 16; pol constant P_A(i) { a(i) }; @@ -987,7 +985,7 @@ namespace main_bin(128); B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; - pol commit sel[2]; + pol commit sel[1]; std::array::map(sel, std::utils::force_bool); "#; let file_name = "../test_data/asm/permutations/vm_to_block.asm"; diff --git a/pipeline/src/test_util.rs b/pipeline/src/test_util.rs index f274155f2..d66c6b0a3 100644 --- a/pipeline/src/test_util.rs +++ b/pipeline/src/test_util.rs @@ -267,7 +267,12 @@ pub fn gen_halo2_proof(pipeline: Pipeline, backend: BackendVariant) // Setup let output_dir = pipeline.output_dir().clone().unwrap(); let setup_file_path = output_dir.join("params.bin"); - let max_degree = pil.degrees().into_iter().max().unwrap(); + let max_degree = pil + .degree_ranges() + .into_iter() + .map(|range| range.max) + .max() + .unwrap(); buffered_write_file(&setup_file_path, |writer| { powdr_backend::BackendType::Halo2 .factory::() diff --git a/test_data/asm/permutations/binary4.asm b/test_data/asm/permutations/binary4.asm index e4d2588e7..ac1826b42 100644 --- a/test_data/asm/permutations/binary4.asm +++ b/test_data/asm/permutations/binary4.asm @@ -13,6 +13,7 @@ machine Binary4 with // check that we can reference the call_selectors let sum_sel = std::array::sum(sel); + std::utils::force_bool(sum_sel); col fixed FACTOR(i) { 1 << (((i + 1) % 8) * 4) }; diff --git a/test_data/asm/permutations/block_to_block.asm b/test_data/asm/permutations/block_to_block.asm index 0573713ba..0db0598a4 100644 --- a/test_data/asm/permutations/block_to_block.asm +++ b/test_data/asm/permutations/block_to_block.asm @@ -43,9 +43,7 @@ machine Main with degree: 256 { Binary4 bin; Binary4x bin4; - // two permutations to machine bin instr or X, Y -> Z link ~> Z = bin.or(X, Y); - instr or_into_B X, Y link ~> B' = bin.or(X, Y); // permutation to machine bin4 instr or4 X, Y, Z, W -> R link ~> R = bin4.or4(X, Y, Z, W); @@ -58,11 +56,6 @@ machine Main with degree: 256 { A <== or(1,2); assert_eq A, 3; - or_into_B 2,3; - assert_eq B, 3; - or_into_B 1,2; - assert_eq B, 3; - A <== or4(1,2,4,8); assert_eq A, 15; A <== or4(15,16,32,64); diff --git a/test_data/asm/permutations/vm_to_block.asm b/test_data/asm/permutations/vm_to_block.asm index f300e4a52..236b54e1b 100644 --- a/test_data/asm/permutations/vm_to_block.asm +++ b/test_data/asm/permutations/vm_to_block.asm @@ -11,9 +11,7 @@ machine Main with degree: 128 { Binary4 bin; - // two permutations to machine bin instr or X, Y -> Z link ~> Z = bin.or(X, Y); - instr or_into_B X, Y link ~> B' = bin.or(X, Y); instr assert_eq X, Y { X = Y } @@ -25,11 +23,6 @@ machine Main with degree: 128 { A <== or(3,4); assert_eq A, 7; - or_into_B 2,3; - assert_eq B, 3; - or_into_B 1,2; - assert_eq B, 3; - return; } } 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..268a00420 100644 --- a/test_data/asm/permutations/vm_to_block_multiple_links.asm +++ b/test_data/asm/permutations/vm_to_block_multiple_links.asm @@ -14,32 +14,11 @@ machine Main with degree: 32 { instr sub X, Y -> Z link ~> Z = arith.sub(X, Y); instr assert_eq X, Y { X = Y } - // instructions activating multiple permutations - instr add_one X -> Y - link ~> B = arith.add(X, 2) - link ~> Y = arith.sub(B, 1) - { - } - - // multiple links with flags - instr add_or_sub X, Y -> Z - link if ADD ~> Z = arith.add(X, Y) - link if (1 - ADD) ~> Z = arith.sub(X, Y); - function main { A <== add(1, 1); A <== add(A, 1); A <== sub(A, 1); assert_eq A, 2; - A <== add_one(A); - assert_eq A, 3; - - ADD <=X= 1; - A <== add_or_sub(2,5); - assert_eq A, 7; - ADD <=X= 0; - A <== add_or_sub(A,5); - assert_eq A, 2; return; }