41 const AllEntities& in,
43 const FF& scaling_factor)
46 using View =
typename Accumulator::View;
48 static const auto offset_generator = [&]() {
52 static const FF qx = result.x;
53 static const FF qy = result.y;
54 static const Accumulator ox(qx);
55 static const Accumulator oy(qy);
58 const auto z1 = View(in.transcript_z1);
59 const auto z2 = View(in.transcript_z2);
60 const auto z1_zero = View(in.transcript_z1zero);
61 const auto z2_zero = View(in.transcript_z2zero);
62 const auto op = View(in.transcript_op);
63 const auto q_add = View(in.transcript_add);
64 const auto q_mul = View(in.transcript_mul);
65 const auto q_mul_shift = View(in.transcript_mul_shift);
66 const auto q_eq = View(in.transcript_eq);
67 const auto msm_transition = View(in.transcript_msm_transition);
68 const auto msm_count = View(in.transcript_msm_count);
69 const auto msm_count_shift = View(in.transcript_msm_count_shift);
70 const auto pc = View(in.transcript_pc);
71 const auto pc_shift = View(in.transcript_pc_shift);
72 const auto transcript_accumulator_x_shift = View(in.transcript_accumulator_x_shift);
73 const auto transcript_accumulator_y_shift = View(in.transcript_accumulator_y_shift);
74 const auto transcript_accumulator_x = View(in.transcript_accumulator_x);
75 const auto transcript_accumulator_y = View(in.transcript_accumulator_y);
76 const auto msm_count_zero_at_transition = View(in.transcript_msm_count_zero_at_transition);
77 const auto msm_count_at_transition_inverse = View(in.transcript_msm_count_at_transition_inverse);
78 const auto transcript_msm_x = View(in.transcript_msm_intermediate_x);
79 const auto transcript_msm_y = View(in.transcript_msm_intermediate_y);
80 const auto transcript_Px = View(in.transcript_Px);
81 const auto transcript_Py = View(in.transcript_Py);
82 const auto is_accumulator_empty = -View(in.transcript_accumulator_not_empty) + 1;
83 const auto lagrange_first = View(in.lagrange_first);
84 const auto lagrange_last = View(in.lagrange_last);
85 const auto is_accumulator_empty_shift = -View(in.transcript_accumulator_not_empty_shift) + 1;
86 const auto q_reset_accumulator = View(in.transcript_reset_accumulator);
87 const auto lagrange_second = View(in.lagrange_second);
88 const auto lagrange_third = View(in.lagrange_third);
89 const auto transcript_Pinfinity = View(in.transcript_base_infinity);
90 const auto transcript_Px_inverse = View(in.transcript_base_x_inverse);
91 const auto transcript_Py_inverse = View(in.transcript_base_y_inverse);
92 const auto transcript_add_x_equal = View(in.transcript_add_x_equal);
93 const auto transcript_add_y_equal = View(in.transcript_add_y_equal);
94 const auto transcript_add_lambda = View(in.transcript_add_lambda);
95 const auto transcript_msm_infinity = View(in.transcript_msm_infinity);
97 const auto is_not_first_row = (-lagrange_first + 1);
98 const auto is_not_last_row = (-lagrange_last + 1);
99 const auto is_not_first_or_last_row = (-lagrange_first + -lagrange_last + 1);
100 const auto is_not_infinity = (-transcript_Pinfinity + 1);
102 const auto is_not_hiding_row = (-lagrange_second + 1);
122 auto tmp = q_add + q_add;
127 tmp += q_reset_accumulator;
137 Accumulator pc_delta = pc - pc_shift;
138 auto num_muls_in_row = ((-z1_zero + 1) + (-z2_zero + 1)) * (-transcript_Pinfinity + 1);
142 is_not_first_row * (pc_delta - q_mul * num_muls_in_row) * scaling_factor;
163 auto msm_transition_check = q_mul * (-q_mul_shift + 1);
164 auto msm_count_total = msm_count + num_muls_in_row;
170 auto msm_count_zero_at_transition_check = msm_count_zero_at_transition * msm_count_total;
171 msm_count_zero_at_transition_check +=
172 (msm_count_total * msm_count_at_transition_inverse - 1) * (-msm_count_zero_at_transition + 1);
178 msm_transition_check * msm_count_zero_at_transition_check * scaling_factor;
188 (msm_transition - msm_transition_check * (-msm_count_zero_at_transition + 1)) * scaling_factor;
205 auto msm_count_delta = msm_count_shift - msm_count;
207 (msm_count_delta - q_mul * num_muls_in_row) *
216 auto opcode_exclusion_relation = q_mul * (q_add + q_eq + q_reset_accumulator);
217 opcode_exclusion_relation += q_add * (q_mul + q_eq + q_reset_accumulator);
227 auto both_infinity = transcript_Pinfinity * is_accumulator_empty;
228 auto both_not_infinity = (-transcript_Pinfinity + 1) * (-is_accumulator_empty + 1);
229 auto infinity_exclusion_check =
230 transcript_Pinfinity + is_accumulator_empty - both_infinity - both_infinity;
231 auto eq_x_diff = transcript_Px - transcript_accumulator_x;
232 auto eq_y_diff = transcript_Py - transcript_accumulator_y;
234 auto eq_x_diff_relation =
235 q_eq * (eq_x_diff * both_not_infinity + infinity_exclusion_check) * is_not_hiding_row;
236 auto eq_y_diff_relation =
237 q_eq * (eq_y_diff * both_not_infinity + infinity_exclusion_check) * is_not_hiding_row;
252 lagrange_third * (-is_accumulator_empty + 1) * scaling_factor;
254 (lagrange_third * msm_count + lagrange_last * pc) * scaling_factor;
263 const auto validate_on_curve = q_add + q_mul + q_eq;
264 const auto on_curve_check =
265 transcript_Py * transcript_Py - transcript_Px * transcript_Px * transcript_Px - get_curve_b();
268 validate_on_curve * on_curve_check * is_not_infinity * is_not_hiding_row * scaling_factor;
277 Accumulator transcript_lambda_relation(0);
278 auto is_double = transcript_add_x_equal * transcript_add_y_equal;
281 auto is_add = -transcript_add_x_equal + 1;
282 auto rhs_x = transcript_accumulator_x;
283 auto rhs_y = transcript_accumulator_y;
284 auto out_x = transcript_accumulator_x_shift;
285 auto out_y = transcript_accumulator_y_shift;
286 auto lambda = transcript_add_lambda;
290 auto lhs_x = transcript_Px * q_add + transcript_msm_x * msm_transition;
291 auto lhs_y = transcript_Py * q_add + transcript_msm_y * msm_transition;
293 auto lhs_infinity = transcript_Pinfinity * q_add + transcript_msm_infinity * msm_transition;
294 auto rhs_infinity = is_accumulator_empty;
297 auto result_is_lhs = rhs_infinity * (-lhs_infinity + 1);
298 auto result_is_rhs = (-rhs_infinity + 1) * lhs_infinity;
301 auto result_infinity_from_inputs = lhs_infinity * rhs_infinity;
304 auto result_infinity_from_operation = transcript_add_x_equal * (-transcript_add_y_equal + 1);
308 auto result_is_infinity = result_infinity_from_inputs + result_infinity_from_operation;
309 auto any_add_is_active = q_add + msm_transition;
313 Accumulator transcript_msm_lambda_relation(0);
314 auto msm_x = transcript_msm_x;
315 auto msm_y = transcript_msm_y;
318 auto lambda_denominator = (rhs_x - msm_x);
319 auto lambda_numerator = (rhs_y - msm_y);
320 auto lambda_relation = lambda * lambda_denominator - lambda_numerator;
321 transcript_msm_lambda_relation += lambda_relation * is_add;
325 auto lambda_denominator = msm_y + msm_y;
326 auto lambda_numerator = msm_x * msm_x * 3;
327 auto lambda_relation = lambda * lambda_denominator - lambda_numerator;
328 transcript_msm_lambda_relation += lambda_relation * is_double;
330 auto transcript_add_or_dbl_from_msm_output_is_valid =
331 (-transcript_msm_infinity + 1) * (-is_accumulator_empty + 1);
335 transcript_msm_lambda_relation *= transcript_add_or_dbl_from_msm_output_is_valid;
340 auto lambda_relation_invalid =
341 (transcript_msm_infinity + is_accumulator_empty + result_infinity_from_operation);
342 auto lambda_relation = lambda * lambda_relation_invalid;
343 transcript_msm_lambda_relation += lambda_relation;
346 transcript_lambda_relation = transcript_msm_lambda_relation * msm_transition;
351 Accumulator transcript_add_lambda_relation(0);
352 auto add_x = transcript_Px;
353 auto add_y = transcript_Py;
356 auto lambda_denominator = (rhs_x - add_x);
357 auto lambda_numerator = (rhs_y - add_y);
358 auto lambda_relation = lambda * lambda_denominator - lambda_numerator;
359 transcript_add_lambda_relation += lambda_relation * is_add;
363 auto lambda_denominator = add_y + add_y;
364 auto lambda_numerator = add_x * add_x * 3;
365 auto lambda_relation = lambda * lambda_denominator - lambda_numerator;
366 transcript_add_lambda_relation += lambda_relation * is_double;
368 auto transcript_add_or_dbl_from_add_output_is_valid =
369 (-transcript_Pinfinity + 1) * (-is_accumulator_empty + 1);
370 transcript_add_lambda_relation *= transcript_add_or_dbl_from_add_output_is_valid;
375 auto lambda_relation_invalid =
376 (transcript_Pinfinity + is_accumulator_empty + result_infinity_from_operation);
377 auto lambda_relation = lambda * lambda_relation_invalid;
378 transcript_add_lambda_relation += lambda_relation;
381 transcript_lambda_relation += transcript_add_lambda_relation * q_add;
398 auto propagate_transcript_accumulator =
399 (q_mul) * (-msm_transition + 1) + (q_eq * (-q_reset_accumulator + 1));
401 auto lambda_sqr = lambda * lambda;
406 auto x3 = lambda_sqr - lhs_x - rhs_x;
407 auto y3 = lambda * (lhs_x - x3) - lhs_y;
408 x3 += result_is_lhs * (rhs_x + lhs_x + lhs_x);
409 x3 += result_is_rhs * (lhs_x + rhs_x + rhs_x);
410 x3 += result_is_infinity * (lhs_x + rhs_x);
411 y3 += result_is_lhs * (lhs_y + lhs_y);
412 y3 += result_is_rhs * (lhs_y + rhs_y);
413 y3 += result_is_infinity * lhs_y;
417 auto add_point_x_relation = (x3 - out_x) * any_add_is_active;
418 add_point_x_relation +=
419 propagate_transcript_accumulator * is_not_last_row * (out_x - transcript_accumulator_x);
421 add_point_x_relation += (out_x * q_reset_accumulator);
422 auto add_point_y_relation = (y3 - out_y) * any_add_is_active;
423 add_point_y_relation +=
424 propagate_transcript_accumulator * is_not_last_row * (out_y - transcript_accumulator_y);
426 add_point_y_relation += (out_y * q_reset_accumulator);
427 auto opcode_is_zero =
428 (is_not_first_row) * (-q_add + 1) * (-q_mul + 1) * (-q_reset_accumulator + 1) * (-q_eq + 1);
429 add_point_x_relation += (out_x * opcode_is_zero);
430 add_point_y_relation += (out_y * opcode_is_zero);
441 const auto offset = offset_generator();
442 const auto x1 =
offset[0];
443 const auto y1 = -
offset[1];
444 const auto x2 = View(in.transcript_msm_x);
445 const auto y2 = View(in.transcript_msm_y);
446 const auto x3 = View(in.transcript_msm_intermediate_x);
447 const auto y3 = View(in.transcript_msm_intermediate_y);
448 const auto transcript_msm_infinity = View(in.transcript_msm_infinity);
452 const auto x_term = (x3 + x2 + x1) * (x2 - x1) * (x2 - x1) - (y2 - y1) * (y2 - y1);
453 const auto y_term = (x1 - x3) * (y2 - y1) - (x2 - x1) * (y1 + y3);
460 const auto transcript_offset_generator_subtract_x =
461 x_term * (-transcript_msm_infinity + 1) + transcript_msm_infinity * x3;
462 const auto transcript_offset_generator_subtract_y =
463 y_term * (-transcript_msm_infinity + 1) + transcript_msm_infinity * y3;
465 msm_transition * transcript_offset_generator_subtract_x * scaling_factor;
467 msm_transition * transcript_offset_generator_subtract_y * scaling_factor;
472 const auto x_diff = x2 - x1;
473 const auto y_sum = y2 + y1;
475 msm_transition * transcript_msm_infinity * x_diff * scaling_factor;
477 msm_transition * transcript_msm_infinity * y_sum * scaling_factor;
479 const auto transcript_msm_x_inverse = View(in.transcript_msm_x_inverse);
480 const auto inverse_term = (-transcript_msm_infinity + 1) * (x_diff * transcript_msm_x_inverse - 1);
500 auto accumulator_infinity_preserve_flag = propagate_transcript_accumulator;
501 auto accumulator_infinity_preserve = accumulator_infinity_preserve_flag *
502 (is_accumulator_empty - is_accumulator_empty_shift) *
503 is_not_first_or_last_row;
504 auto accumulator_infinity_q_reset = q_reset_accumulator * (-is_accumulator_empty_shift + 1);
505 auto accumulator_infinity_from_add =
506 any_add_is_active * (result_is_infinity - is_accumulator_empty_shift);
512 auto opcode_is_zero =
513 (is_not_first_row) * (-q_add + 1) * (-q_mul + 1) * (-q_reset_accumulator + 1) * (-q_eq + 1);
514 auto accumulator_infinity_from_noop = opcode_is_zero * (-is_accumulator_empty_shift + 1);
515 auto accumulator_infinity_relation =
516 accumulator_infinity_preserve +
517 (accumulator_infinity_q_reset + accumulator_infinity_from_add) * is_not_first_row +
518 accumulator_infinity_from_noop;
526 auto x_diff = lhs_x - rhs_x;
528 auto x_product = transcript_Px_inverse * (-transcript_add_x_equal + 1) + transcript_add_x_equal;
529 auto x_constant = transcript_add_x_equal - 1;
530 auto transcript_add_x_equal_check_relation = (x_diff * x_product + x_constant) * any_add_is_active;
538 auto y_diff = lhs_y - rhs_y;
539 auto y_product = transcript_Py_inverse * (-transcript_add_y_equal + 1) + transcript_add_y_equal;
540 auto y_constant = transcript_add_y_equal - 1;
541 auto transcript_add_y_equal_check_relation = (y_diff * y_product + y_constant) * any_add_is_active;
553 lagrange_second * (-q_reset_accumulator + 1) * scaling_factor;
566 is_accumulator_empty * transcript_accumulator_x * scaling_factor;
568 is_accumulator_empty * transcript_accumulator_y * scaling_factor;
577 lagrange_first * View(in.transcript_accumulator_not_empty) * scaling_factor;