Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix nightly tests #2115

Merged
merged 3 commits into from
Nov 20, 2024
Merged

fix nightly tests #2115

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ea52379
fix some tests
leonardoalt Nov 19, 2024
21aa384
review
leonardoalt Nov 20, 2024
78b15cc
Merge remote-tracking branch 'origin/main' into fix-nightly
leonardoalt Nov 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 19 additions & 21 deletions linker/src/lib.rs
View file
Open in desktop
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);
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

these were caused by changing the asm test

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🃏

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
View file
Open in desktop
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();
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this function is called for both Composite and Mono proofs, and it assumed all degrees were unique ranges before. This now takes the max of all max degrees for the halo2 setup

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
View file
Open in desktop
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
View file
Open in desktop
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);
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

unfortunately Halo2 has a bug somewhere and we can't do this.
This is testes in other places (including RISCV tests) with witgen

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is it possible to disable halo2 for the test instead?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we still want to run halo2 proofs for these tests to test permutations between machines

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But do we test the previous functionality somewhere else?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

language/compiler/witgen wise yes, the RISCV machine has this stuff and more


// 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
View file
Open in desktop
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);
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here re halo2


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
View file
Open in desktop
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)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here and below re halo2

{
}

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