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.

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

Propagate known. #2325

Open
wants to merge 35 commits into
base: main
Choose a base branch
from
Open

Propagate known. #2325

wants to merge 35 commits into from

Conversation

chriseth
Copy link
Member

No description provided.

Copy link

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite Current: a3dc813 Previous: b961239 Ratio
jit-witgen-benchmark/jit_witgen_benchmark 51511629019 ns/iter (± 46751484) 32073282431 ns/iter (± 76394754) 1.61
executor-benchmark/keccak 437809691309 ns/iter (± 3274197576) 16140744556 ns/iter (± 112427593) 27.12

This comment was automatically generated by workflow using github-action-benchmark.

@chriseth chriseth changed the base branch from main to provide_completed_identities January 14, 2025 10:49
@chriseth chriseth marked this pull request as ready for review January 14, 2025 14:24
@chriseth
Copy link
Member Author

chriseth commented Jan 14, 2025

Error solving equality constraint:
  (main_arith::is_affine + main_arith::is_ec_add + main_arith::is_ec_double)
* (
  main_arith::do_mstore
    - (main_arith::CLK32[0] + main_arith::CLK32[1] + main_arith::CLK32[2] + main_arith::CLK32[3]
    + main_arith::CLK32[4] + main_arith::CLK32[5] + main_arith::CLK32[6] + main_arith::CLK32[7]
    + (main_arith::CLK32[8] + main_arith::CLK32[9] + main_arith::CLK32[10] + main_arith::CLK32[11]
    + main_arith::CLK32[12] + main_arith::CLK32[13] + main_arith::CLK32[14] + main_arith::CLK32[15]
    )))= 0
    on row 8:
    Linear constraint is not satisfiable: -(1 + main_arith::is_ec_double[8]) != 0

In the last line, the fact that it did not replace main_arith::is_ec_double[8] by an actual value means that it is known (i.e. the code contains a way to assign it) but only symbolically, and there are range constraints known on it such that the range constraint +1 excludes zero.

It probably also means that is_affine and is_ec_add are both known at compile time, one of them is zero, the other one is 1.

It also branched, but not sure if those are still active:

[DEBUG powdr_executor::witgen::jit::processor] Branching on variable main_arith::is_affine[0] with range [0, 1] & 0x1 at depth 0
[DEBUG powdr_executor::witgen::jit::processor] Branching on variable main_arith::is_mod[0] with range [0, 1] & 0x1 at depth 1

Base automatically changed from provide_completed_identities to main January 15, 2025 20:00
});
let mut progress = false;
for (id, row_offset) in &self.identities {
if witgen.process_identity(can_process.clone(), id, *row_offset)? {
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 need to use a for loop here because of the ? operator.

@@ -237,7 +233,7 @@ if (VM::instr_add[0] == 1) {
col fixed INSTR_ADD = [0, 1] + [0]*;
col fixed INSTR_MUL = [1, 0] + [1]*;
pc' = pc + 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.

This change was needed because otherwise, the system is not solvable. Do a case analysis of the allowed values for pc and pc' and you will see why.

@@ -186,7 +186,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
row_offset,
rhs: VariableOrValue::Value(value),
});
self.process_assignments();
self.process_assignments().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 should not lead to a conflict. If that happens, we can propagate the error, but this function is called in some places where it is difficult to propagate the error.

@@ -203,24 +203,71 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
row_offset,
rhs: VariableOrValue::Variable(variable),
});
self.process_assignments();
self.process_assignments().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.

Same here.

@@ -255,11 +302,6 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
let Some(new_range_constraints) =
can_process_call.can_process_call_fully(lookup_id, &known, &range_constraints)
else {
log::trace!(
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 was very noisy and not really helpful.

@@ -363,7 +406,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
}
}
if progress {
self.process_assignments();
self.process_assignments().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.

Again, too lazy to propagate the error here. Let's see if it happens.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant