Miden VM constraints#527
Conversation
…d MIR translation
Al-Kindi-0
added
MidenVM constraints
no changelog
| # Enforce that when absorbing the next set of elements into the state during linear hash | ||
| # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to | ||
| # the next row. | ||
| enf f_abp * (h' - h) = 0 for h in h; |
There was a problem hiding this comment.
According to the doc (https://0xmiden.github.io/miden-vm/design/chiplets/hasher.html#hasher-state-constraints) and the comment, shouldn't this be only for the first 4 elements in h?
There was a problem hiding this comment.
Indeed, this is an example of some stale constraints that need updating.
I am compiling a list now and will fix soon.
Al-Kindi-0
force-pushed
the
vm-constraints-new
branch
from
8874614 to
341ad89
Compare
Leo-Besancon
left a comment
Leo-Besancon
left a comment
There was a problem hiding this comment.
Hi! Working my way through the PRs in the order outlined in #537, left a few small comments but I'm not sure they need to be addressed (or if maybe followup PRs address some of them)
| let op_square = op^2; | ||
|
|
||
| enf op_square * (linear_op_0 - non_linear_op_0) + non_linear_op_0 = v0_0; | ||
| enf op_square * (linear_op_1 - non_linear_op_1) + non_linear_op_1 = v0_1; |
There was a problem hiding this comment.
Maybe use select(op_square, linear_op_0, non_linear_op_0) here
| let a_and_b = compute_limb_and(a_limb, b_limb); | ||
| let a_xor_b = compute_limb_xor(a_limb, b_limb); | ||
|
|
||
| enf z = zp * 16 + op_flag * (a_xor_b - a_and_b) + a_and_b; |
There was a problem hiding this comment.
Maybe use select too
| # enf match { | ||
| # !b & f_absorb_node: is_unchanged(h[j + 4]) for j in 0..4, | ||
| # b & f_absorb_node: h[j + 8]' = h[j + 4] for j in 0..4 | ||
| # } |
There was a problem hiding this comment.
should be able to uncomment this
| enf f_scw' * (v0' - v0) + binary_not(f_scw') * v0' = 0 when is_constrained_value[0]; | ||
| enf f_scw' * (v1' - v1) + binary_not(f_scw') * v1' = 0 when is_constrained_value[1]; | ||
| enf f_scw' * (v2' - v2) + binary_not(f_scw') * v2' = 0 when is_constrained_value[2]; | ||
| enf f_scw' * (v3' - v3) + binary_not(f_scw') * v3' = 0 when is_constrained_value[3]; |
2 participants
Describe your changes
Checklist before requesting a review
nextaccording to naming convention.CHANGELOG.md