chore: audit ECCVM msm relation #16532
Conversation
| std::get<21>(accumulator) += round_transition * (-q_double_shift + 1) * (-q_skew_shift + 1) * scaling_factor; | ||
|
|
||
| // if double, next double != 1 | ||
| std::get<22>(accumulator) += q_double * q_double_shift * scaling_factor; |
There was a problem hiding this comment.
this is superfluous, as q_double == 1 forces q_add_shift == 1, but q_add, q_double, and q_skew are all mutually exclusive.
| // if msm_transition = 0 and round_transition = 0, count_shift = count + add1 + add2 + add3 + add4 | ||
| // todo: we need this? | ||
| // if we are changing the "round" (i.e. starting to process a new wNAF digit), the count_shift must be 0. | ||
| std::get<23>(accumulator) += round_delta * count_shift * scaling_factor; |
There was a problem hiding this comment.
when we start a new "round" (i.e., when we start processing a new wNAF digit), we reset the count to 0. (this was underconstrained before)
There was a problem hiding this comment.
this also ensures that round is correctly range constrained, periodic, etc., which is also required to prove that the set relation correctly constrains everything.
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
…. this will require a new column.
notnotraju
force-pushed
the
rk/eccvm-audit-msm-relation
branch
from
6a95cd7 to
31a1502
Compare
…k/eccvm-audit-msm-relation
…ew descriptions of some of the columns.
| // if msm_transition = 1, count_shift = 0 | ||
| std::get<26>(accumulator) += is_not_first_row * msm_transition_shift * count_shift * scaling_factor; | ||
| // if msm_transition = 1, then round = 0. | ||
| std::get<26>(accumulator) += msm_transition * round * scaling_factor; |
There was a problem hiding this comment.
reset the round to be zero at an MSM transition
| std::get<20>(accumulator) += round_transition * (q_skew_shift + q_double_shift - 1) * scaling_factor; | ||
|
|
||
| // if no double or no skew, round_delta = 0 | ||
| std::get<35>(accumulator) += (-round_delta + 1) * q_double_shift * scaling_factor; |
There was a problem hiding this comment.
this seems necessary: round increments by 1 if next is a double. the corresponding logic with skew is explained the comments.
NOTE: this is important to prove that the set_relation correctly constrains everything.
| std::get<33>(accumulator) += (-msm_transition_shift + 1) * q_skew * (-q_skew_shift + 1) * scaling_factor; | ||
| // if q_skew == 1, then round == 32. This is almost certainly redundant but psychologically useful to "constrain | ||
| // both ends". | ||
| std::get<34>(accumulator) += q_skew * (-round + 32) * scaling_factor; |
There was a problem hiding this comment.
if skew == 1, then round == 32. This is likely redundant, but we have to be careful about the q_add logic, so I thought constraining "both ends" is better. It also makes me more sure that round is correctly range-constrained.
notnotraju
added
the
bberg-int-audit
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
| // == 1.) | ||
| // this means that the first row with `round == 32` has q_skew == 1. then all subsequent q_skew entries must be 1, | ||
| // _until_ we start our new MSM. | ||
| std::get<33>(accumulator) += (-msm_transition_shift + 1) * q_skew * (-q_skew_shift + 1) * scaling_factor; |
There was a problem hiding this comment.
this says: once q_skew is 1, the subsequent values of q_skew will be 1 until we hit an MSM transition. we have already forced q_skew to be 1 at the first row where round == 32 (bc of round_transition logic). this in particular obviates the need to add an extra column that I earlier thought was necessary. win for inductive logic, I guess!
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp
Outdated
Show resolved
Hide resolved
…k/eccvm-audit-msm-relation
Audit of the MSM relation.
There were a couple of columns that I think were underconstrained (see discussion below). I hopefully have made the MSM relations more robust/clear as to why they are correct.
Aside from a few changes to the relations, this PR mostly involves a lot of documentation. The most important part of this is re: the multiset equality check. The description of why this suffices to correctly constrain the q_add columns is more transparent now.