Skip to content

Commit

Permalink
fix nightly tests (#2115)
Browse files Browse the repository at this point in the history
  • Loading branch information
leonardoalt authored Nov 20, 2024
1 parent 8b38138 commit 82798c8
Show file tree
Hide file tree
Showing 6 changed files with 26 additions and 57 deletions.
40 changes: 19 additions & 21 deletions linker/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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]*;
Expand All @@ -963,14 +960,15 @@ 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]*;
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) };
Expand All @@ -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";
Expand Down
7 changes: 6 additions & 1 deletion pipeline/src/test_util.rs
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,12 @@ pub fn gen_halo2_proof(pipeline: Pipeline<Bn254Field>, 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::<Bn254Field>()
Expand Down
1 change: 1 addition & 0 deletions test_data/asm/permutations/binary4.asm
Original file line number Diff line number Diff line change
Expand Up @@ -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) };

Expand Down
7 changes: 0 additions & 7 deletions test_data/asm/permutations/block_to_block.asm
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down
7 changes: 0 additions & 7 deletions test_data/asm/permutations/vm_to_block.asm
Original file line number Diff line number Diff line change
Expand Up @@ -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 }

Expand All @@ -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;
}
}
21 changes: 0 additions & 21 deletions test_data/asm/permutations/vm_to_block_multiple_links.asm
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down

0 comments on commit 82798c8

Please sign in to comment.