-
Notifications
You must be signed in to change notification settings - Fork 73
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
Implement Basic Bus #1566
base: main
Are you sure you want to change the base?
Implement Basic Bus #1566
Conversation
let<T: Add + Mul + FromLiteral> fingerprint_with_id: T, T[], Fp2<T> -> Fp2<T> = |id, expr_array, alpha| fold( | ||
expr_array, | ||
from_base(id), | ||
|sum_acc, el| add_ext(mul_ext(alpha, sum_acc), from_base(el)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
let<T: Add + Mul + FromLiteral> fingerprint_with_id: T, T[], Fp2<T> -> Fp2<T> = |id, expr_array, alpha| fold( | |
expr_array, | |
from_base(id), | |
|sum_acc, el| add_ext(mul_ext(alpha, sum_acc), from_base(el)) | |
let<T: Add + Mul + FromLiteral> fingerprint_with_id: T, T[], Fp2<T> -> Fp2<T> = |id, expr_array, alpha| fingerprint([id] + expr_array, alpha); |
This should work and be equivalent, no?
let (acc_1, acc_2) = unpack_ext(acc_ext); | ||
let (expr_1, expr_2) = unpack_ext(update_expr); | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
let (acc_1, acc_2) = unpack_ext(acc_ext); | |
let (expr_1, expr_2) = unpack_ext(update_expr); | |
Doesn't seem to be used.
let compute_next_z_receive: expr, expr, expr[], expr, Fp2<expr>, Fp2<expr>, Fp2<expr> -> fe[] = query |is_first, id, tuple, multiplicity, acc, alpha, beta| { | ||
// Implemented as: folded = (beta - fingerprint(id, tuple...)); | ||
// `multiplicity / (beta - fingerprint(id, tuple...))` to `acc` | ||
let folded = sub_ext(beta, fingerprint_with_id(id, tuple, alpha)); | ||
let folded_next = next_ext(folded); | ||
|
||
let m_ext = from_base(multiplicity); | ||
let m_ext_next = next_ext(m_ext); | ||
|
||
let is_first_next = from_base(is_first'); | ||
|
||
// acc' = acc * (1 - is_first') - multiplicity / fingerprint_with_id(id, (a1', a2')) | ||
let res = sub_ext( | ||
mul_ext(eval_ext(acc), eval_ext(sub_ext(from_base(1), is_first_next))), | ||
mul_ext(eval_ext(m_ext_next), inv_ext(eval_ext(folded_next))) | ||
); | ||
|
||
match res { | ||
Fp2::Fp2(a0_fe, a1_fe) => [a0_fe, a1_fe] | ||
} | ||
}; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
let compute_next_z_receive: expr, expr, expr[], expr, Fp2<expr>, Fp2<expr>, Fp2<expr> -> fe[] = query |is_first, id, tuple, multiplicity, acc, alpha, beta| { | |
// Implemented as: folded = (beta - fingerprint(id, tuple...)); | |
// `multiplicity / (beta - fingerprint(id, tuple...))` to `acc` | |
let folded = sub_ext(beta, fingerprint_with_id(id, tuple, alpha)); | |
let folded_next = next_ext(folded); | |
let m_ext = from_base(multiplicity); | |
let m_ext_next = next_ext(m_ext); | |
let is_first_next = from_base(is_first'); | |
// acc' = acc * (1 - is_first') - multiplicity / fingerprint_with_id(id, (a1', a2')) | |
let res = sub_ext( | |
mul_ext(eval_ext(acc), eval_ext(sub_ext(from_base(1), is_first_next))), | |
mul_ext(eval_ext(m_ext_next), inv_ext(eval_ext(folded_next))) | |
); | |
match res { | |
Fp2::Fp2(a0_fe, a1_fe) => [a0_fe, a1_fe] | |
} | |
}; | |
let compute_next_z_receive: expr, expr, expr[], expr, Fp2<expr>, Fp2<expr>, Fp2<expr> -> fe[] = query |is_first, id, tuple, multiplicity, acc, alpha, beta| compute_next_z_send(is_first, id, tuple, -multiplicity, acc, alpha, beta); |
Right?
let is_first_next = from_base(is_first'); | ||
|
||
// acc' = acc * (1 - is_first') + multiplicity / fingerprint_with_id(id, (a1', a2')) | ||
let res = add_ext( | ||
mul_ext(eval_ext(acc), eval_ext(sub_ext(from_base(1), is_first_next))), | ||
mul_ext(eval_ext(m_ext_next), inv_ext(eval_ext(folded_next))) | ||
); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
let is_first_next = from_base(is_first'); | |
// acc' = acc * (1 - is_first') + multiplicity / fingerprint_with_id(id, (a1', a2')) | |
let res = add_ext( | |
mul_ext(eval_ext(acc), eval_ext(sub_ext(from_base(1), is_first_next))), | |
mul_ext(eval_ext(m_ext_next), inv_ext(eval_ext(folded_next))) | |
); | |
let is_first_next = eval(is_first'); | |
let current_acc = if is_first_next == 1 { from_base(0) } else { eval_ext(acc) }; | |
// acc' = current_acc + multiplicity / fingerprint_with_id(id, (a1', a2')) | |
let res = add_ext( | |
current_acc, | |
mul_ext(eval_ext(m_ext_next), inv_ext(eval_ext(folded_next))) | |
); |
This fixes the extension test! Previously, the hint was never executed, because the argument acc
was never known. What happens now is this:
- The hint is run on the last row. Because
is_first'
evaluates to1
,current_acc == from_base(0)
andacc
(which is unknown) never needs to be evaluated. - This sets
z_next
in the last row, which setsz
in the the first row. - When evaluating the hint on the first row,
is_first'
evaluates to0
, soacc
(a.k.az
) needs to be evaluated. But we've just set it, so it works.
In your previous code, you would have evaluated acc
in step 1 and then multiply by 0
. That is correct, but witgen is not smart enough to know that the when multiplying by 0 it doesn't need to evaluate the other factor.
Also, this code should be more efficient ;)
Related to the issue of implementing basic bus (#1497), I have implemented basic bus together with an example (
permutation_via_bus.asm
) as specified inside the issue.Currently,
test_data/std/bus_permutation_via_challenges.asm
works as intended (To make it sound, stage(1) witness columns need to be exposed publicly and verifier needs to check such asout_z1 + out_z2 = 0
) We can now check using RUST_LOG=trace and adding the final z1 and z2 is equal to 0.However,
test_data/std/bus_permutation_via_challenges_ext.asm
is not working correctly as intended. This will be fixed with the following commits.