Skip to content
Merged
Show file tree
Hide file tree
Changes from 44 commits
Commits
Show all changes
54 commits
Select commit Hold shift + click to select a range
7963b2c
updated oob columns and renaming shorthands
lorenzogentile404 Oct 23, 2025
7709439
updated shorthands
lorenzogentile404 Oct 27, 2025
e17e943
added specialized computation
lorenzogentile404 Oct 27, 2025
8378037
added osaka ecdata
lorenzogentile404 Oct 27, 2025
9b6b54d
updated ec_data columns
lorenzogentile404 Oct 27, 2025
20a4a75
updated ec_data generalities
lorenzogentile404 Oct 27, 2025
3951185
added utils
lorenzogentile404 Oct 27, 2025
e0b9a0f
added specialized computation
lorenzogentile404 Oct 28, 2025
01fa2e7
added circuit selector
lorenzogentile404 Oct 28, 2025
9f31979
used ISZERO instead of LT for ECRECOVER and P256_VERIFY
lorenzogentile404 Nov 3, 2025
d7d6016
fixed callToR1MembershipEXT
lorenzogentile404 Nov 4, 2025
84f2793
fixed address_sum
lorenzogentile404 Nov 4, 2025
c2390e4
used computed columns for circuit selectors
lorenzogentile404 Nov 4, 2025
beb70c8
partially updated osaka hub with P256_VERIFY
lorenzogentile404 Nov 5, 2025
e2684e2
fixed precompile success case
lorenzogentile404 Nov 5, 2025
d76b2ed
fixed naming
lorenzogentile404 Nov 5, 2025
26d2f17
fixed formatting
lorenzogentile404 Nov 5, 2025
730f961
EIP-7823: Set upper bounds for `MODEXP` --- `OOB` side (#813)
OlivierBBB Nov 7, 2025
07c0230
EIP-7823: Set upper bounds for `MODEXP` --- `BLAKE_MODEXP` side (#812)
OlivierBBB Nov 7, 2025
5090d90
EIP-7823: Set upper bounds for `MODEXP` --- `MMU` side (#814)
OlivierBBB Nov 7, 2025
9d313e4
Automatic vanishing constraints of `misc/XXX_?` columns when `misc/XX…
OlivierBBB Nov 7, 2025
28a83b3
EIP-7823: Set upper bounds for `MODEXP` --- `HUB` side (#815)
OlivierBBB Nov 7, 2025
3fb426c
Replace `R@C` in ROFF constant name with `RAC` (#822)
OlivierBBB Nov 7, 2025
6969e68
removed deprecated comments
lorenzogentile404 Nov 9, 2025
7b4e3fb
added TODOs
lorenzogentile404 Nov 10, 2025
a0f12c1
feat: precompile processing justifying success and FKTR update for pv…
amkCha Nov 12, 2025
a313559
feat: update nsr and flag sums + rm TODOs
amkCha Nov 12, 2025
dd4771d
feat: update defproperty sanity check for p256-verfy
amkCha Nov 17, 2025
7598eaa
fixed index max data for p256_verify precompile
lorenzogentile404 Nov 19, 2025
fa257d7
Merge branch 'master' into 780-eip-7951-precompile-for-secp256r1-curv…
lorenzogentile404 Nov 20, 2025
9bbaa63
set result rows for P256_VERIFY precompile
lorenzogentile404 Nov 20, 2025
e23ed8e
update oob osaka shorthands
lorenzogentile404 Nov 21, 2025
76f952a
updated oob wrt p256_verify
lorenzogentile404 Nov 21, 2025
bb7da45
fix: wrong flag sums for BLS ... ?!
OlivierBBB Nov 21, 2025
2694b49
ras: formatting
OlivierBBB Nov 21, 2025
861a000
fix: cursor comment
OlivierBBB Nov 21, 2025
dc5122e
ras: renaming + formatting
OlivierBBB Nov 21, 2025
aeb7677
ras: splitting justifying HUB preditions constraint
OlivierBBB Nov 21, 2025
4d0de63
ras: formatting + constraints splitting
OlivierBBB Nov 21, 2025
f6d2790
ras: formatting
OlivierBBB Nov 21, 2025
b69ba54
ras: formatting
OlivierBBB Nov 21, 2025
2348a08
feat: new scenario/PRC_xxx shorthands
OlivierBBB Nov 21, 2025
027a754
ras: splitting OOB/shorthands file as in spec
OlivierBBB Nov 21, 2025
52ff6ac
ras
OlivierBBB Nov 21, 2025
008b715
feat: P256_VERIFY constraints HUB-side
OlivierBBB Nov 21, 2025
77b8727
ras: make it compile
OlivierBBB Nov 21, 2025
1365116
feat: remove P256 from EC_ADD/MUL/PAIRING/BLS precompile processing
OlivierBBB Nov 21, 2025
301f9c1
fix: add preconditions to defproperty's
OlivierBBB Nov 21, 2025
1dba760
fix: typo
OlivierBBB Nov 21, 2025
890493a
feat: appropriate guards on various defproperty's for common precompiles
OlivierBBB Nov 21, 2025
7547f21
Merge branch 'master' into 780-eip-7951-precompile-for-secp256r1-curv…
OlivierBBB Nov 21, 2025
1814df8
typo
OlivierBBB Nov 21, 2025
9558f61
ras: formatting
OlivierBBB Nov 21, 2025
3c4fc31
ras
OlivierBBB Nov 21, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ CONSTANTS_PRAGUE := constants/prague/constants.zkasm
CONSTANTS_OSAKA := constants/osaka/constants.zkasm

EC_DATA_LONDON := ecdata/london

EC_DATA_OSAKA := ecdata/osaka

EUC := euc/euc.zkasm
Expand Down
6 changes: 6 additions & 0 deletions constants/constants.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,7 @@
GAS_CONST_BLS_MAP_FP2_TO_G2 23800
GAS_CONST_BLS_PAIRING_CHECK 37700
GAS_CONST_BLS_PAIRING_CHECK_PAIR 32600
GAS_CONST_P256_VERIFY 6900
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM MISC ;;
Expand Down Expand Up @@ -328,6 +329,7 @@
PRECOMPILE_CALL_DATA_UNIT_SIZE___BLS_PAIRING_CHECK 384
PRECOMPILE_CALL_DATA_SIZE___FP_TO_G1 64
PRECOMPILE_CALL_DATA_SIZE___FP2_TO_G2 128
PRECOMPILE_CALL_DATA_SIZE___P256_VERIFY 160

PRC_ECPAIRING_SIZE (* 6 WORD_SIZE)
PRECOMPILE_CALL_DATA_SIZE___BLAKE2F 213
Expand All @@ -342,6 +344,7 @@
PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK 32
PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1 128
PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2 256
PRECOMPILE_RETURN_DATA_SIZE___P256_VERIFY 32

PRC_BLS_G1_MSM_MAX_DISCOUNT 519
PRC_BLS_G2_MSM_MAX_DISCOUNT 524
Expand Down Expand Up @@ -405,6 +408,8 @@
PHASE_ECMUL_RESULT 0x070B
PHASE_ECPAIRING_DATA 0x080A
PHASE_ECPAIRING_RESULT 0x080B
PHASE_P256_VERIFY_DATA 0x100A
PHASE_P256_VERIFY_RESULT 0x100B
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; BLS DATA MODULE ;;
Expand Down Expand Up @@ -523,6 +528,7 @@
OOB_INST_BLS_PAIRING_CHECK 0xFF0F
OOB_INST_BLS_MAP_FP_TO_G1 0xFF10
OOB_INST_BLS_MAP_FP2_TO_G2 0xFF11
OOB_INST_P256_VERIFY 0xF100
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; RLP* MODULE ;;
Expand Down
6 changes: 0 additions & 6 deletions ecdata/london/columns.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -36,12 +36,6 @@
(G2_MEMBERSHIP_TEST_REQUIRED :binary@prove)
(ACCEPTABLE_PAIR_OF_POINTS_FOR_PAIRING_CIRCUIT :binary@prove)

(CIRCUIT_SELECTOR_ECRECOVER :binary@prove)
(CIRCUIT_SELECTOR_ECADD :binary@prove)
(CIRCUIT_SELECTOR_ECMUL :binary@prove)
(CIRCUIT_SELECTOR_ECPAIRING :binary@prove)
(CIRCUIT_SELECTOR_G2_MEMBERSHIP :binary@prove)

(WCP_FLAG :binary@prove)
(WCP_ARG1_HI :i128)
(WCP_ARG1_LO :i128)
Expand Down
35 changes: 14 additions & 21 deletions ecdata/london/constraints.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -478,7 +478,6 @@
(eq! P_is_point_at_infinity 1)
(vanishes! P_is_point_at_infinity))))))

;; Note: in the specs for simplicity we omit the last four arguments
(defun (callToC1MembershipWCP k
_P_x_hi
_P_x_lo
Expand All @@ -492,7 +491,6 @@
(callToLT (+ k 1) _P_y_hi _P_y_lo P_BN_HI P_BN_LO)
(callToEQ (+ k 2) _P_y_square_hi _P_y_square_lo _P_x_cube_plus_three_hi _P_x_cube_plus_three_lo)))

;; Note: in the specs for simplicity we omit the last four arguments
(defun (callToC1MembershipEXT k
_P_x_hi
_P_x_lo
Expand Down Expand Up @@ -568,17 +566,17 @@
(s_hi (shift LIMB 6))
(s_lo (shift LIMB 7)))
(begin (callToLT 0 r_hi r_lo SECP256K1N_HI SECP256K1N_LO)
(callToLT 1 0 0 r_hi r_lo)
(callToISZERO 1 r_hi r_lo)
(callToLT 2 s_hi s_lo SECP256K1N_HI SECP256K1N_LO)
(callToLT 3 0 0 s_hi s_lo)
(callToISZERO 3 s_hi s_lo)
(callToEQ 4 v_hi v_lo 0 27)
(callToEQ 5 v_hi v_lo 0 28))))

(defconstraint justify-success-bit-ecrecover (:guard (ecrecover-hypothesis))
(let ((r_is_in_range WCP_RES)
(r_is_positive (next WCP_RES))
(r_is_positive (- 1 (next WCP_RES)))
(s_is_in_range (shift WCP_RES 2))
(s_is_positive (shift WCP_RES 3))
(s_is_positive (- 1 (shift WCP_RES 3)))
(v_is_27 (shift WCP_RES 4))
(v_is_28 (shift WCP_RES 5))
(internal_checks_passed (shift HURDLE INDEX_MAX_ECRECOVER_DATA)))
Expand Down Expand Up @@ -729,25 +727,20 @@
;; 3.7.3 Interface for ;;
;; Gnark ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint ecrecover-circuit-selector ()
(eq! CS_ECRECOVER (* ICP (is_ecrecover))))
(defcomputedcolumn (CIRCUIT_SELECTOR_ECRECOVER :binary@prove)
(* ICP (is_ecrecover)))

(defconstraint ecadd-circuit-selector ()
(eq! CS_ECADD (* ICP (is_ecadd))))
(defcomputedcolumn (CIRCUIT_SELECTOR_ECADD :binary@prove)
(* ICP (is_ecadd)))

(defconstraint ecmul-circuit-selector ()
(eq! CS_ECMUL (* ICP (is_ecmul))))
(defcomputedcolumn (CIRCUIT_SELECTOR_ECMUL :binary@prove)
(* ICP (is_ecmul)))

(defconstraint ecpairing-circuit-selector ()
(begin
(if-not-zero IS_ECPAIRING_DATA (eq! CS_ECPAIRING ACCPC))
(if-not-zero IS_ECPAIRING_RESULT (eq! CS_ECPAIRING (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING))))
(if-zero (is_ecpairing) (vanishes! CS_ECPAIRING))
)
)
(defcomputedcolumn (CIRCUIT_SELECTOR_ECPAIRING :binary@prove)
(+ (* IS_ECPAIRING_DATA ACCPC) (* IS_ECPAIRING_RESULT (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING)))))

(defconstraint g2-membership-circuit-selector ()
(eq! CS_G2_MEMBERSHIP G2MTR))
(defcomputedcolumn (CIRCUIT_SELECTOR_G2_MEMBERSHIP :binary@prove)
G2MTR)

(defconstraint circuit-selectors-sum-binary ()
(debug (is-binary (+ CS_ECRECOVER CS_ECADD CS_ECMUL CS_ECPAIRING CS_G2_MEMBERSHIP))))
Expand Down
25 changes: 11 additions & 14 deletions ecdata/osaka/columns.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -10,14 +10,16 @@
(INDEX_MAX :i16)
(SUCCESS_BIT :binary@prove)

(IS_ECRECOVER_DATA :binary@prove)
(IS_ECRECOVER_RESULT :binary@prove)
(IS_ECADD_DATA :binary@prove)
(IS_ECADD_RESULT :binary@prove)
(IS_ECMUL_DATA :binary@prove)
(IS_ECMUL_RESULT :binary@prove)
(IS_ECPAIRING_DATA :binary@prove)
(IS_ECPAIRING_RESULT :binary@prove)
(IS_ECRECOVER_DATA :binary@prove)
(IS_ECRECOVER_RESULT :binary@prove)
(IS_ECADD_DATA :binary@prove)
(IS_ECADD_RESULT :binary@prove)
(IS_ECMUL_DATA :binary@prove)
(IS_ECMUL_RESULT :binary@prove)
(IS_ECPAIRING_DATA :binary@prove)
(IS_ECPAIRING_RESULT :binary@prove)
(IS_P256_VERIFY_DATA :binary@prove)
(IS_P256_VERIFY_RESULT :binary@prove)

(TOTAL_PAIRINGS :i16)
(ACC_PAIRINGS :i16)
Expand All @@ -36,12 +38,6 @@
(G2_MEMBERSHIP_TEST_REQUIRED :binary@prove)
(ACCEPTABLE_PAIR_OF_POINTS_FOR_PAIRING_CIRCUIT :binary@prove)

(CIRCUIT_SELECTOR_ECRECOVER :binary@prove)
(CIRCUIT_SELECTOR_ECADD :binary@prove)
(CIRCUIT_SELECTOR_ECMUL :binary@prove)
(CIRCUIT_SELECTOR_ECPAIRING :binary@prove)
(CIRCUIT_SELECTOR_G2_MEMBERSHIP :binary@prove)

(WCP_FLAG :binary@prove)
(WCP_ARG1_HI :i128)
(WCP_ARG1_LO :i128)
Expand Down Expand Up @@ -71,6 +67,7 @@
CS_ECADD CIRCUIT_SELECTOR_ECADD
CS_ECMUL CIRCUIT_SELECTOR_ECMUL
CS_ECPAIRING CIRCUIT_SELECTOR_ECPAIRING
CS_P256_VERIFY CIRCUIT_SELECTOR_P256_VERIFY
CS_G2_MEMBERSHIP CIRCUIT_SELECTOR_G2_MEMBERSHIP)


13 changes: 13 additions & 0 deletions ecdata/osaka/constants.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,21 @@
P_BN_LO 0x97816a916871ca8d3c208c16d87cfd47
SECP256K1N_HI 0xffffffffffffffffffffffffffffffff
SECP256K1N_LO 0xfffffffffffffffffffffffefffffc2f
P_R1_HI 0xffffffff000000010000000000000000
P_R1_LO 0x00000000ffffffffffffffffffffffff
SECP256R1N_HI 0xffffffff00000000ffffffffffffffff
SECP256R1N_LO 0xbce6faada7179e84f3b9cac2fc632551
A_COEFF_R1_HI 0xffffffff000000010000000000000000
A_COEFF_R1_LO 0x00000000fffffffffffffffffffffffc
B_COEFF_R1_HI 0x5ac635d8aa3a93e7b3ebbd55769886bc
B_COEFF_R1_LO 0x651d06b0cc53b0f63bce3c3e27d2604b
MULMOD 0x09
ADDMOD 0x08
ECRECOVER 0x01
ECADD 0x06
ECMUL 0x07
ECPAIRING 0x08
P256_VERIFY 0x100
INDEX_MAX_ECRECOVER_DATA 7
INDEX_MAX_ECADD_DATA 7
INDEX_MAX_ECMUL_DATA 5
Expand All @@ -19,6 +28,8 @@
INDEX_MAX_ECADD_RESULT 3
INDEX_MAX_ECMUL_RESULT 3
INDEX_MAX_ECPAIRING_RESULT 1
INDEX_MAX_P256_VERIFY_DATA 9
INDEX_MAX_P256_VERIFY_RESULT 1
TOTAL_SIZE_ECRECOVER_DATA 128
TOTAL_SIZE_ECADD_DATA 128
TOTAL_SIZE_ECMUL_DATA 96
Expand All @@ -27,6 +38,8 @@
TOTAL_SIZE_ECADD_RESULT 64
TOTAL_SIZE_ECMUL_RESULT 64
TOTAL_SIZE_ECPAIRING_RESULT 32
TOTAL_SIZE_P256_VERIFY_DATA 160
TOTAL_SIZE_P256_VERIFY_RESULT 32
CT_MAX_SMALL_POINT 3
CT_MAX_LARGE_POINT 7)

Expand Down
Loading
Loading