feat(acir static analysis): MSM constraints#20540
feat(acir static analysis): MSM constraints#20540defkit wants to merge 19 commits intosn/acir_ec_add_constraints_partial_checkfrom
Conversation
Flakey Tests🤖 says: This CI run detected 1 tests that failed, but were tolerated due to a .test_patterns.yml entry. |
| auto y2 = (*real_input2).y; | ||
| auto inf2 = (*real_input2).is_infinite; | ||
|
|
||
| // If both points are constant, operator+ is computed natively without gates |
There was a problem hiding this comment.
Same check twice, we checked is_point_const above
| // Range constraint consists of variable index and num bits to be constrained. | ||
| // num bits == 1 => bool gate | ||
| // num bits <= 14 => arithmetic gate + create_new_range_constraint <=> arithmetic gate + list[tag] | ||
| // num bits > 14 => decompose_into_default_range => decompose chain with additional range constrains for sublimbs | ||
| // | ||
| const auto& variable_gates = analyzer.get_variable_gates(analyzer.to_real(witness)); |
There was a problem hiding this comment.
@DanielKotov FYI, moved to helpers/range_helpers.hpp
| * tba = conditional_assign(predicate, input_result, result) | ||
| * result.assert_equal(tba) | ||
| * | ||
| * Tracing batch_mul internals is impractical (complex multi-point multiplication), so the |
There was a problem hiding this comment.
PLease add a TODO to implement the proper tracing (maybe by using fuzzy hashes) in the future
| return std::nullopt; | ||
| } | ||
|
|
||
| return get_field_from_w_o<FF>(builder, filtered[0]); |
There was a problem hiding this comment.
What happens if several are found?
There was a problem hiding this comment.
That's actually a bug in all helpers
All helpers assume that the first match is the correct one, which is not true
e.g. in cases when the points shares the same is_infinite witness, to_grumpkin_point will create different variables for conditional_assign result and that will break validation
ii have to refactor all helpers to iterate through all possible gates...
There was a problem hiding this comment.
With the latest change we assume that the first occurrence of non-consumed normalization gate is the correct one.
It still can be an issue in really strange cases if we encounter the same witness being used in previous constraints, processed by Daniel's functions, but it will be easy to fix in future
| * @details mirrors bool_t::assert_bool | ||
| */ | ||
| template <typename FF, typename CircuitBuilder> | ||
| bool is_boolean_gate_exists(StaticAnalyzer_<FF, CircuitBuilder>& analyzer, |
| bool condition = true; | ||
|
|
||
| // 1. Verify on-curve check for all input points | ||
| for (size_t i = 0; i < constraint->points.size(); i += 3) { |
There was a problem hiding this comment.
What if it's not a multiple of 3?
There was a problem hiding this comment.
It is asserted by create_multi_scalar_mul_constraint
| using namespace bb; | ||
| using namespace acir_format; | ||
| using namespace cdg; | ||
|
|
There was a problem hiding this comment.
I think we need more extensive tests with longer MSMs and various combinations
| uint32_t witness_idx) | ||
| { | ||
| auto filter_helper = FilterFunctionBuilder<CircuitBuilder, FF>(builder) | ||
| .set_w_l(witness_idx) |
There was a problem hiding this comment.
Doesn't check w_r is the same
|
In the latest commit I've refactored filtering logic; introduced "consumed" gates mechanism. It is needed for special cases, when the same witness is reused in similar ACIR constraints, (e.g #20540 (comment) ) I still think that taking the first non-consumed gate, which matches the condition is good enough, because variable_gates are populated sequentially, keeping the same order as in constraints. I cannot see the case, when the first matching gate is incorrect one |
3 participants
Checks that
We skip tracing batch_mul, because it is way too complex