|
478 | 478 | (eq! P_is_point_at_infinity 1) |
479 | 479 | (vanishes! P_is_point_at_infinity)))))) |
480 | 480 |
|
481 | | -;; Note: in the specs for simplicity we omit the last four arguments |
482 | 481 | (defun (callToC1MembershipWCP k |
483 | 482 | _P_x_hi |
484 | 483 | _P_x_lo |
|
492 | 491 | (callToLT (+ k 1) _P_y_hi _P_y_lo P_BN_HI P_BN_LO) |
493 | 492 | (callToEQ (+ k 2) _P_y_square_hi _P_y_square_lo _P_x_cube_plus_three_hi _P_x_cube_plus_three_lo))) |
494 | 493 |
|
495 | | -;; Note: in the specs for simplicity we omit the last four arguments |
496 | 494 | (defun (callToC1MembershipEXT k |
497 | 495 | _P_x_hi |
498 | 496 | _P_x_lo |
|
568 | 566 | (s_hi (shift LIMB 6)) |
569 | 567 | (s_lo (shift LIMB 7))) |
570 | 568 | (begin (callToLT 0 r_hi r_lo SECP256K1N_HI SECP256K1N_LO) |
571 | | - (callToLT 1 0 0 r_hi r_lo) |
| 569 | + (callToISZERO 1 r_hi r_lo) |
572 | 570 | (callToLT 2 s_hi s_lo SECP256K1N_HI SECP256K1N_LO) |
573 | | - (callToLT 3 0 0 s_hi s_lo) |
| 571 | + (callToISZERO 3 s_hi s_lo) |
574 | 572 | (callToEQ 4 v_hi v_lo 0 27) |
575 | 573 | (callToEQ 5 v_hi v_lo 0 28)))) |
576 | 574 |
|
577 | 575 | (defconstraint justify-success-bit-ecrecover (:guard (ecrecover-hypothesis)) |
578 | 576 | (let ((r_is_in_range WCP_RES) |
579 | | - (r_is_positive (next WCP_RES)) |
| 577 | + (r_is_positive (- 1 (next WCP_RES))) |
580 | 578 | (s_is_in_range (shift WCP_RES 2)) |
581 | | - (s_is_positive (shift WCP_RES 3)) |
| 579 | + (s_is_positive (- 1 (shift WCP_RES 3))) |
582 | 580 | (v_is_27 (shift WCP_RES 4)) |
583 | 581 | (v_is_28 (shift WCP_RES 5)) |
584 | 582 | (internal_checks_passed (shift HURDLE INDEX_MAX_ECRECOVER_DATA))) |
|
729 | 727 | ;; 3.7.3 Interface for ;; |
730 | 728 | ;; Gnark ;; |
731 | 729 | ;;;;;;;;;;;;;;;;;;;;;;;;; |
732 | | -(defconstraint ecrecover-circuit-selector () |
733 | | - (eq! CS_ECRECOVER (* ICP (is_ecrecover)))) |
| 730 | +(defcomputedcolumn (CIRCUIT_SELECTOR_ECRECOVER :binary@prove) |
| 731 | + (* ICP (is_ecrecover))) |
734 | 732 |
|
735 | | -(defconstraint ecadd-circuit-selector () |
736 | | - (eq! CS_ECADD (* ICP (is_ecadd)))) |
| 733 | +(defcomputedcolumn (CIRCUIT_SELECTOR_ECADD :binary@prove) |
| 734 | + (* ICP (is_ecadd))) |
737 | 735 |
|
738 | | -(defconstraint ecmul-circuit-selector () |
739 | | - (eq! CS_ECMUL (* ICP (is_ecmul)))) |
| 736 | +(defcomputedcolumn (CIRCUIT_SELECTOR_ECMUL :binary@prove) |
| 737 | + (* ICP (is_ecmul))) |
740 | 738 |
|
741 | | -(defconstraint ecpairing-circuit-selector () |
742 | | - (begin |
743 | | - (if-not-zero IS_ECPAIRING_DATA (eq! CS_ECPAIRING ACCPC)) |
744 | | - (if-not-zero IS_ECPAIRING_RESULT (eq! CS_ECPAIRING (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING)))) |
745 | | - (if-zero (is_ecpairing) (vanishes! CS_ECPAIRING)) |
746 | | - ) |
747 | | -) |
| 739 | +(defcomputedcolumn (CIRCUIT_SELECTOR_ECPAIRING :binary@prove) |
| 740 | + (+ (* IS_ECPAIRING_DATA ACCPC) (* IS_ECPAIRING_RESULT (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING))))) |
748 | 741 |
|
749 | | -(defconstraint g2-membership-circuit-selector () |
750 | | - (eq! CS_G2_MEMBERSHIP G2MTR)) |
| 742 | +(defcomputedcolumn (CIRCUIT_SELECTOR_G2_MEMBERSHIP :binary@prove) |
| 743 | + G2MTR) |
751 | 744 |
|
752 | 745 | (defconstraint circuit-selectors-sum-binary () |
753 | 746 | (debug (is-binary (+ CS_ECRECOVER CS_ECADD CS_ECMUL CS_ECPAIRING CS_G2_MEMBERSHIP)))) |
|
0 commit comments