diff --git a/Makefile b/Makefile index c9355bf91..5e3880e18 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,8 @@ ALU := alu/add/add.zkasm alu/ext alu/mod alu/mul BIN := bin/bin.zkasm -BLAKE2f_MODEXP_DATA := blake2fmodexpdata +BLAKE2f_MODEXP_DATA_LONDON := blake2fmodexpdata/london +BLAKE2f_MODEXP_DATA_OSAKA := blake2fmodexpdata/osaka # constraints used in prod for LINEA, with linea block gas limit BLOCKDATA_LONDON := blockdata/london @@ -53,7 +54,8 @@ LOG_DATA := logdata LOG_INFO_LONDON := loginfo/london LOG_INFO_CANCUN := loginfo/cancun -MMU := mmu +MMU_LONDON := mmu/london +MMU_OSAKA := mmu/osaka MMIO_LONDON := mmio/london MMIO_CANCUN := mmio/cancun @@ -118,7 +120,6 @@ endef ZKEVM_MODULES_COMMON := ${CONSTANTS} \ ${ALU} \ ${BIN} \ - ${BLAKE2f_MODEXP_DATA} \ ${BLOCKHASH} \ ${EUC} \ ${EXP} \ @@ -136,6 +137,7 @@ ZKEVM_MODULES_COMMON := ${CONSTANTS} \ ZKEVM_MODULES_LONDON := ${ZKEVM_MODULES_COMMON} \ ${CONSTANTS_LONDON} \ ${TABLES_LONDON} \ + ${BLAKE2f_MODEXP_DATA_LONDON} \ ${BLOCKDATA_LONDON} \ ${EC_DATA_LONDON} \ ${HUB_LONDON} \ @@ -155,6 +157,7 @@ ZKEVM_MODULES_LONDON := ${ZKEVM_MODULES_COMMON} \ ZKEVM_MODULES_SHANGHAI := ${ZKEVM_MODULES_COMMON} \ ${CONSTANTS_LONDON} \ ${TABLES_LONDON} \ + ${BLAKE2f_MODEXP_DATA_LONDON} \ ${BLOCKDATA_PARIS} \ ${EC_DATA_LONDON} \ ${HUB_SHANGHAI} \ @@ -169,8 +172,9 @@ ZKEVM_MODULES_SHANGHAI := ${ZKEVM_MODULES_COMMON} \ ${TXN_DATA_SHANGHAI} ZKEVM_MODULES_CANCUN := ${ZKEVM_MODULES_COMMON} \ - ${CONSTANTS_CANCUN} \ + ${CONSTANTS_CANCUN} \ ${TABLES_CANCUN} \ + ${BLAKE2f_MODEXP_DATA_LONDON} \ ${BLOCKDATA_CANCUN} \ ${BLS_CANCUN} \ ${EC_DATA_LONDON} \ @@ -189,6 +193,7 @@ ZKEVM_MODULES_CANCUN := ${ZKEVM_MODULES_COMMON} \ ZKEVM_MODULES_PRAGUE := ${ZKEVM_MODULES_COMMON} \ ${CONSTANTS_PRAGUE} \ ${TABLES_PRAGUE} \ + ${BLAKE2f_MODEXP_DATA_LONDON} \ ${BLOCKDATA_CANCUN} \ ${BLS_PRAGUE} \ ${EC_DATA_LONDON} \ @@ -207,6 +212,7 @@ ZKEVM_MODULES_PRAGUE := ${ZKEVM_MODULES_COMMON} \ ZKEVM_MODULES_OSAKA := ${ZKEVM_MODULES_COMMON} \ ${CONSTANTS_OSAKA} \ ${TABLES_PRAGUE} \ + ${BLAKE2f_MODEXP_DATA_OSAKA} \ ${BLOCKDATA_CANCUN} \ ${BLS_PRAGUE} \ ${EC_DATA_OSAKA} \ diff --git a/blake2fmodexpdata/columns.lisp b/blake2fmodexpdata/london/columns.lisp similarity index 100% rename from blake2fmodexpdata/columns.lisp rename to blake2fmodexpdata/london/columns.lisp diff --git a/blake2fmodexpdata/constants.lisp b/blake2fmodexpdata/london/constants.lisp similarity index 100% rename from blake2fmodexpdata/constants.lisp rename to blake2fmodexpdata/london/constants.lisp diff --git a/blake2fmodexpdata/constraints.lisp b/blake2fmodexpdata/london/constraints.lisp similarity index 100% rename from blake2fmodexpdata/constraints.lisp rename to blake2fmodexpdata/london/constraints.lisp diff --git a/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp b/blake2fmodexpdata/london/lookups/blakemodexp_into_wcp.lisp similarity index 100% rename from blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp rename to blake2fmodexpdata/london/lookups/blakemodexp_into_wcp.lisp diff --git a/blake2fmodexpdata/osaka/columns.lisp b/blake2fmodexpdata/osaka/columns.lisp new file mode 100644 index 000000000..6432c3faa --- /dev/null +++ b/blake2fmodexpdata/osaka/columns.lisp @@ -0,0 +1,18 @@ +(module blake2fmodexpdata) + +(defcolumns + (STAMP :i16) + (ID :i32) + (PHASE :byte) + (INDEX :byte :display :dec) + (INDEX_MAX :byte :display :dec) + (LIMB :i128 :display :bytes) + (IS_MODEXP_BASE :binary@prove) + (IS_MODEXP_EXPONENT :binary@prove) + (IS_MODEXP_MODULUS :binary@prove) + (IS_MODEXP_RESULT :binary@prove) + (IS_BLAKE_DATA :binary@prove) + (IS_BLAKE_PARAMS :binary@prove) + (IS_BLAKE_RESULT :binary@prove) + ) + diff --git a/blake2fmodexpdata/osaka/constants.lisp b/blake2fmodexpdata/osaka/constants.lisp new file mode 100644 index 000000000..079bc4079 --- /dev/null +++ b/blake2fmodexpdata/osaka/constants.lisp @@ -0,0 +1,13 @@ +(module blake2fmodexpdata) + +(defconst + INDEX_MAX_MODEXP 63 + INDEX_MAX_MODEXP_BASE INDEX_MAX_MODEXP + INDEX_MAX_MODEXP_EXPONENT INDEX_MAX_MODEXP + INDEX_MAX_MODEXP_MODULUS INDEX_MAX_MODEXP + INDEX_MAX_MODEXP_RESULT INDEX_MAX_MODEXP + INDEX_MAX_BLAKE_DATA 12 + INDEX_MAX_BLAKE_PARAMS 1 + INDEX_MAX_BLAKE_RESULT 3) + + diff --git a/blake2fmodexpdata/osaka/constraints.lisp b/blake2fmodexpdata/osaka/constraints.lisp new file mode 100644 index 000000000..843d4d3e9 --- /dev/null +++ b/blake2fmodexpdata/osaka/constraints.lisp @@ -0,0 +1,76 @@ +(module blake2fmodexpdata) + +(defun (flag-sum) + (+ IS_MODEXP_BASE + IS_MODEXP_EXPONENT + IS_MODEXP_MODULUS + IS_MODEXP_RESULT + IS_BLAKE_DATA + IS_BLAKE_PARAMS + IS_BLAKE_RESULT)) + +(defun (phase-sum) + (+ (* PHASE_MODEXP_BASE IS_MODEXP_BASE) + (* PHASE_MODEXP_EXPONENT IS_MODEXP_EXPONENT) + (* PHASE_MODEXP_MODULUS IS_MODEXP_MODULUS) + (* PHASE_MODEXP_RESULT IS_MODEXP_RESULT) + (* PHASE_BLAKE_DATA IS_BLAKE_DATA) + (* PHASE_BLAKE_PARAMS IS_BLAKE_PARAMS) + (* PHASE_BLAKE_RESULT IS_BLAKE_RESULT))) + +(defun (index-max-sum) + (+ (* INDEX_MAX_MODEXP_BASE IS_MODEXP_BASE) + (* INDEX_MAX_MODEXP_EXPONENT IS_MODEXP_EXPONENT) + (* INDEX_MAX_MODEXP_MODULUS IS_MODEXP_MODULUS) + (* INDEX_MAX_MODEXP_RESULT IS_MODEXP_RESULT) + (* INDEX_MAX_BLAKE_DATA IS_BLAKE_DATA) + (* INDEX_MAX_BLAKE_PARAMS IS_BLAKE_PARAMS) + (* INDEX_MAX_BLAKE_RESULT IS_BLAKE_RESULT))) + +(defconstraint no-stamp-no-flag () + (if-zero STAMP + (vanishes! (flag-sum)) + (eq! (flag-sum) 1))) + +(defconstraint set-phase-and-index () + (begin (eq! PHASE (phase-sum)) + (eq! INDEX_MAX (index-max-sum)))) + +(defconstraint stamp-constancies () + (stamp-constancy STAMP ID)) + +(defconstraint index-constancies (:guard INDEX) + (remained-constant! (phase-sum))) + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint no-stamp-nothing () + (if-zero STAMP + (begin (vanishes! ID) + (vanishes! (next INDEX))))) + +(defun (stamp-increment) + (force-bin (+ (* (- 1 IS_MODEXP_BASE) (next IS_MODEXP_BASE)) + (* (- 1 IS_BLAKE_DATA) (next IS_BLAKE_DATA))))) + +(defconstraint stamp-increases () + (will-inc! STAMP (stamp-increment))) + +(defun (transition-bit) + (force-bin (+ (* IS_MODEXP_BASE (next IS_MODEXP_EXPONENT)) + (* IS_MODEXP_EXPONENT (next IS_MODEXP_MODULUS)) + (* IS_MODEXP_MODULUS (next IS_MODEXP_RESULT)) + (* IS_MODEXP_RESULT + (+ (next IS_MODEXP_BASE) (next IS_BLAKE_DATA))) + (* IS_BLAKE_DATA (next IS_BLAKE_PARAMS)) + (* IS_BLAKE_PARAMS (next IS_BLAKE_RESULT)) + (* IS_BLAKE_RESULT + (+ (next IS_MODEXP_BASE) (next IS_BLAKE_DATA)))))) + +(defconstraint heartbeat (:guard STAMP) + (if-zero (- INDEX_MAX INDEX) + (eq! (transition-bit) 1) + (will-inc! INDEX 1))) + + diff --git a/blake2fmodexpdata/osaka/lookups/blakemodexp_into_wcp.lisp b/blake2fmodexpdata/osaka/lookups/blakemodexp_into_wcp.lisp new file mode 100644 index 000000000..056b83e33 --- /dev/null +++ b/blake2fmodexpdata/osaka/lookups/blakemodexp_into_wcp.lisp @@ -0,0 +1,28 @@ +(defun (blake2fmodexpdata-into-wcp-oob-into-wcp-activation-flag) + (force-bin (* (~ blake2fmodexpdata.STAMP) + (- blake2fmodexpdata.STAMP (prev blake2fmodexpdata.STAMP))))) + +(defclookup + blake2fmodexpdata-into-wcp + ;; target colums (in WCP) + ( + wcp.ARG_1_HI + wcp.ARG_1_LO + wcp.ARG_2_HI + wcp.ARG_2_LO + wcp.RES + wcp.INST + ) + ;; source selector + (blake2fmodexpdata-into-wcp-oob-into-wcp-activation-flag) + ;; source columns + ( + 0 + (prev blake2fmodexpdata.ID) + 0 + blake2fmodexpdata.ID + 1 + EVM_INST_LT + )) + + diff --git a/constants/constants.lisp b/constants/constants.lisp index bebab8b76..f93b1ad91 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -228,6 +228,7 @@ GAS_CONST_IDENTITY 15 GAS_CONST_IDENTITY_WORD 3 GAS_CONST_MODEXP 200 + GAS_CONST_MODEXP_EIP_7823 500 GAS_CONST_ECADD 150 GAS_CONST_ECMUL 6000 GAS_CONST_ECPAIRING 45000 @@ -244,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 ;; @@ -270,6 +272,7 @@ HISTORY_STORAGE_ADDRESS_HI 0x0000f908 HISTORY_STORAGE_ADDRESS_LO 0x27f1c53a10cb7a02335b175320002935 EIP_7825_TRANSACTION_GAS_LIMIT_CAP 0x1000000 ;; 2^24 == 16777216 appears in OSAKA + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1024 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; LINEA MISC ;; @@ -326,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 @@ -340,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 @@ -403,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 ;; @@ -521,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 ;; diff --git a/ecdata/london/columns.lisp b/ecdata/london/columns.lisp index 672d87450..ab86b2d03 100644 --- a/ecdata/london/columns.lisp +++ b/ecdata/london/columns.lisp @@ -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) diff --git a/ecdata/london/constraints.lisp b/ecdata/london/constraints.lisp index f91e1eecb..82d91ead8 100644 --- a/ecdata/london/constraints.lisp +++ b/ecdata/london/constraints.lisp @@ -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 @@ -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 @@ -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))) @@ -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)))) diff --git a/ecdata/osaka/columns.lisp b/ecdata/osaka/columns.lisp index 672d87450..d61eceec4 100644 --- a/ecdata/osaka/columns.lisp +++ b/ecdata/osaka/columns.lisp @@ -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) @@ -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) @@ -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) diff --git a/ecdata/osaka/constants.lisp b/ecdata/osaka/constants.lisp index 0a7ef9cdf..6e9932630 100644 --- a/ecdata/osaka/constants.lisp +++ b/ecdata/osaka/constants.lisp @@ -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 @@ -19,6 +28,8 @@ INDEX_MAX_ECADD_RESULT 3 INDEX_MAX_ECMUL_RESULT 3 INDEX_MAX_ECPAIRING_RESULT 1 + INDEX_MAX_P256_VERIFY_DATA 10 + INDEX_MAX_P256_VERIFY_RESULT 1 TOTAL_SIZE_ECRECOVER_DATA 128 TOTAL_SIZE_ECADD_DATA 128 TOTAL_SIZE_ECMUL_DATA 96 @@ -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) diff --git a/ecdata/osaka/constraints.lisp b/ecdata/osaka/constraints.lisp index f91e1eecb..beed1bb6c 100644 --- a/ecdata/osaka/constraints.lisp +++ b/ecdata/osaka/constraints.lisp @@ -30,14 +30,20 @@ (defun (is_ecpairing) (force-bin (+ IS_ECPAIRING_DATA IS_ECPAIRING_RESULT))) +(defun (is_p256_verify) + (force-bin (+ IS_P256_VERIFY_DATA IS_P256_VERIFY_RESULT))) + (defun (flag_sum) - (force-bin (+ (is_ecrecover) (is_ecadd) (is_ecmul) (is_ecpairing)))) + (force-bin (+ (is_ecrecover) (is_ecadd) (is_ecmul) (is_ecpairing) (is_p256_verify)))) (defun (address_sum) (+ (* ECRECOVER (is_ecrecover)) (* ECADD (is_ecadd)) (* ECMUL (is_ecmul)) - (* ECPAIRING (is_ecpairing)))) + (* ECPAIRING (is_ecpairing)) + (* P256_VERIFY (is_p256_verify)))) + +;; TODO: rename constants (defun (phase_sum) (+ (* PHASE_ECRECOVER_DATA IS_ECRECOVER_DATA) @@ -47,13 +53,15 @@ (* PHASE_ECMUL_DATA IS_ECMUL_DATA) (* PHASE_ECMUL_RESULT IS_ECMUL_RESULT) (* PHASE_ECPAIRING_DATA IS_ECPAIRING_DATA) - (* PHASE_ECPAIRING_RESULT IS_ECPAIRING_RESULT))) + (* PHASE_ECPAIRING_RESULT IS_ECPAIRING_RESULT) + (* PHASE_P256_VERIFY_DATA IS_P256_VERIFY_DATA) + (* PHASE_P256_VERIFY_RESULT IS_P256_VERIFY_RESULT))) (defun (is_data) - (force-bin (+ IS_ECRECOVER_DATA IS_ECADD_DATA IS_ECMUL_DATA IS_ECPAIRING_DATA))) + (force-bin (+ IS_ECRECOVER_DATA IS_ECADD_DATA IS_ECMUL_DATA IS_ECPAIRING_DATA IS_P256_VERIFY_DATA))) (defun (is_result) - (force-bin (+ IS_ECRECOVER_RESULT IS_ECADD_RESULT IS_ECMUL_RESULT IS_ECPAIRING_RESULT))) + (force-bin (+ IS_ECRECOVER_RESULT IS_ECADD_RESULT IS_ECMUL_RESULT IS_ECPAIRING_RESULT IS_P256_VERIFY_RESULT))) (defun (transition_to_data) (force-bin (* (- 1 (is_data)) (next (is_data))))) @@ -110,11 +118,13 @@ (+ (* INDEX_MAX_ECRECOVER_DATA IS_ECRECOVER_DATA) (* INDEX_MAX_ECADD_DATA IS_ECADD_DATA) (* INDEX_MAX_ECMUL_DATA IS_ECMUL_DATA) + (* INDEX_MAX_P256_VERIFY_DATA IS_P256_VERIFY_DATA) ;; (* INDEX_MAX_ECRECOVER_RESULT IS_ECRECOVER_RESULT) (* INDEX_MAX_ECADD_RESULT IS_ECADD_RESULT) (* INDEX_MAX_ECMUL_RESULT IS_ECMUL_RESULT) - (* INDEX_MAX_ECPAIRING_RESULT IS_ECPAIRING_RESULT))) + (* INDEX_MAX_ECPAIRING_RESULT IS_ECPAIRING_RESULT) + (* INDEX_MAX_P256_VERIFY_RESULT IS_P256_VERIFY_RESULT))) (defconstraint set-index-max () (eq! (* 16 INDEX_MAX) @@ -132,10 +142,12 @@ (* IS_ECADD_DATA TOTAL_SIZE_ECADD_DATA) (* IS_ECMUL_DATA TOTAL_SIZE_ECMUL_DATA) (* IS_ECPAIRING_DATA TOTAL_SIZE_ECPAIRING_DATA_MIN TOTAL_PAIRINGS) + (* IS_P256_VERIFY_DATA TOTAL_SIZE_P256_VERIFY_DATA) (* IS_ECRECOVER_RESULT TOTAL_SIZE_ECRECOVER_RESULT SUCCESS_BIT) (* IS_ECADD_RESULT TOTAL_SIZE_ECADD_RESULT SUCCESS_BIT) (* IS_ECMUL_RESULT TOTAL_SIZE_ECMUL_RESULT SUCCESS_BIT) - (* IS_ECPAIRING_RESULT TOTAL_SIZE_ECPAIRING_RESULT SUCCESS_BIT)))) + (* IS_ECPAIRING_RESULT TOTAL_SIZE_ECPAIRING_RESULT SUCCESS_BIT) + (* IS_P256_VERIFY_RESULT TOTAL_SIZE_P256_VERIFY_RESULT SUCCESS_BIT)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -301,10 +313,12 @@ (* IS_ECADD_DATA (next (is_ecadd))) (* IS_ECMUL_DATA (next (is_ecmul))) (* IS_ECPAIRING_DATA (next (is_ecpairing))) + (* IS_P256_VERIFY_DATA (next (is_p256_verify))) (* IS_ECRECOVER_RESULT (next IS_ECRECOVER_RESULT)) (* IS_ECADD_RESULT (next IS_ECADD_RESULT)) (* IS_ECMUL_RESULT (next IS_ECMUL_RESULT)) (* IS_ECPAIRING_RESULT (next IS_ECPAIRING_RESULT)) + (* IS_P256_VERIFY_RESULT (next IS_P256_VERIFY_RESULT)) (transition_to_data)) 1))) @@ -478,7 +492,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 @@ -492,7 +505,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 @@ -507,6 +519,95 @@ (callToMULMOD (+ k 2) _P_x_square_hi _P_x_square_lo _P_x_hi _P_x_lo P_BN_HI P_BN_LO) (callToADDMOD (+ k 3) _P_x_cube_hi _P_x_cube_lo 0 3 P_BN_HI P_BN_LO))) +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.4.5 R1 membership ;; +;; utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (callToR1Membership k P_x_hi P_x_lo P_y_hi P_y_lo) + (let ((P_x_is_in_range (shift WCP_RES k)) + (P_y_is_in_range (shift WCP_RES (+ k 1))) + (P_satisfies_cubic (shift WCP_RES (+ k 2))) + (P_y_square_hi (shift EXT_RES_HI k)) + (P_y_square_lo (shift EXT_RES_LO k)) + (P_x_square_hi (shift EXT_RES_HI (+ k 1))) + (P_x_square_lo (shift EXT_RES_LO (+ k 1))) + (P_x_cube_hi (shift EXT_RES_HI (+ k 2))) + (P_x_cube_lo (shift EXT_RES_LO (+ k 2))) + (a_times_P_x_hi (shift EXT_RES_HI (+ k 3))) + (a_times_P_x_lo (shift EXT_RES_LO (+ k 3))) + (P_x_cube_plus_a_times_P_x_hi (shift EXT_RES_HI (+ k 4))) + (P_x_cube_plus_a_times_P_x_lo (shift EXT_RES_LO (+ k 4))) + (P_x_cube_plus_a_times_P_x_plus_b_hi (shift EXT_RES_HI (+ k 5))) + (P_x_cube_plus_a_times_P_x_plus_b_lo (shift EXT_RES_LO (+ k 5))) + (P_is_in_range (shift HURDLE (+ k 1))) + (R1_membership (shift HURDLE k)) + (large_sum (+ P_x_hi P_x_lo P_y_hi P_y_lo)) + (P_is_point_at_infinity (shift IS_INFINITY k))) + (begin (callToR1MembershipWCP k + P_x_hi + P_x_lo + P_y_hi + P_y_lo + P_y_square_hi + P_y_square_lo + P_x_cube_plus_a_times_P_x_plus_b_hi + P_x_cube_plus_a_times_P_x_plus_b_lo) + (callToR1MembershipEXT k + P_x_hi + P_x_lo + P_y_hi + P_y_lo + P_x_square_hi + P_x_square_lo + P_x_cube_hi + P_x_cube_lo + a_times_P_x_hi + a_times_P_x_lo + P_x_cube_plus_a_times_P_x_hi + P_x_cube_plus_a_times_P_x_lo) + (eq! P_is_in_range (* P_x_is_in_range P_y_is_in_range)) + (eq! R1_membership + (* P_is_in_range (- 1 P_is_point_at_infinity) P_satisfies_cubic)) + (if-zero P_is_in_range + (vanishes! P_is_point_at_infinity) + (if-zero large_sum + (eq! P_is_point_at_infinity 1) + (vanishes! P_is_point_at_infinity)))))) + +(defun (callToR1MembershipWCP k + P_x_hi + P_x_lo + P_y_hi + P_y_lo + P_y_square_hi + P_y_square_lo + P_x_cube_plus_a_times_P_x_plus_b_hi + P_x_cube_plus_a_times_P_x_plus_b_lo) + (begin (callToLT k P_x_hi P_x_lo P_R1_HI P_R1_LO) + (callToLT (+ k 1) P_y_hi P_y_lo P_R1_HI P_R1_LO) + (callToEQ (+ k 2) P_y_square_hi P_y_square_lo P_x_cube_plus_a_times_P_x_plus_b_hi P_x_cube_plus_a_times_P_x_plus_b_lo))) + +(defun (callToR1MembershipEXT k + P_x_hi + P_x_lo + P_y_hi + P_y_lo + P_x_square_hi + P_x_square_lo + P_x_cube_hi + P_x_cube_lo + a_times_P_x_hi + a_times_P_x_lo + P_x_cube_plus_a_times_P_x_hi + P_x_cube_plus_a_times_P_x_lo) + (begin (callToMULMOD k P_y_hi P_y_lo P_y_hi P_y_lo P_R1_HI P_R1_LO) + (callToMULMOD (+ k 1) P_x_hi P_x_lo P_x_hi P_x_lo P_R1_HI P_R1_LO) + (callToMULMOD (+ k 2) P_x_square_hi P_x_square_lo P_x_hi P_x_lo P_R1_HI P_R1_LO) + (callToMULMOD (+ k 3) A_COEFF_R1_HI A_COEFF_R1_LO P_x_hi P_x_lo P_R1_HI P_R1_LO) + (callToADDMOD (+ k 4) P_x_cube_hi P_x_cube_lo a_times_P_x_hi a_times_P_x_lo P_R1_HI P_R1_LO) + (callToADDMOD (+ k 5) P_x_cube_plus_a_times_P_x_hi P_x_cube_plus_a_times_P_x_lo B_COEFF_R1_HI B_COEFF_R1_LO P_R1_HI P_R1_LO))) + ;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 3.4.4 Well formed ;; @@ -568,17 +669,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))) @@ -692,6 +793,48 @@ (vanishes! SUCCESS_BIT) (eq! SUCCESS_BIT (- 1 NOT_ON_G2_ACC_MAX)))) +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.6.5 The P256_VERIFY ;; +;; case ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (p256-verify-hypothesis) + (* IS_P256_VERIFY_DATA + (~ (- ID (prev ID))))) + +(defconstraint internal-checks-256-verify (:guard (p256-verify-hypothesis)) + (let ((h_hi LIMB) + (h_lo (next LIMB)) + (r_hi (shift LIMB 2)) + (r_lo (shift LIMB 3)) + (s_hi (shift LIMB 4)) + (s_lo (shift LIMB 5)) + (Q_x_hi (shift LIMB 6)) + (Q_x_lo (shift LIMB 7)) + (Q_y_hi (shift LIMB 8)) + (Q_y_lo (shift LIMB 9))) + (begin (callToLT 0 r_hi r_lo SECP256R1N_HI SECP256R1N_LO) + (callToISZERO 1 r_hi r_lo) + (callToLT 2 s_hi s_lo SECP256R1N_HI SECP256R1N_LO) + (callToISZERO 3 s_hi s_lo) + (callToR1Membership 4 Q_x_hi Q_x_lo Q_y_hi Q_y_lo)))) + +(defconstraint justify-success-bit-256-verify (:guard (p256-verify-hypothesis)) + (let ((r_is_in_range WCP_RES) + (r_is_positive (- 1 (next WCP_RES))) + (s_is_in_range (shift WCP_RES 2)) + (s_is_positive (- 1 (shift WCP_RES 3))) + (R1_membership (shift HURDLE 4)) + (internal_checks_passed (shift HURDLE INDEX_MAX_P256_VERIFY_DATA))) + (begin (eq! HURDLE (* r_is_in_range r_is_positive)) + (eq! (next HURDLE) (* s_is_in_range s_is_positive)) + (eq! (shift HURDLE 2) + (* HURDLE (next HURDLE))) + (eq! internal_checks_passed + (* R1_membership (shift HURDLE 2))) + (if-zero internal_checks_passed + (vanishes! SUCCESS_BIT))))) + ;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 3.7 Elliptic curve ;; @@ -729,25 +872,23 @@ ;; 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))) + +(defcomputedcolumn (CIRCUIT_SELECTOR_ECADD :binary@prove) + (* ICP (is_ecadd))) -(defconstraint ecadd-circuit-selector () - (eq! CS_ECADD (* ICP (is_ecadd)))) +(defcomputedcolumn (CIRCUIT_SELECTOR_ECMUL :binary@prove) + (* ICP (is_ecmul))) -(defconstraint ecmul-circuit-selector () - (eq! CS_ECMUL (* ICP (is_ecmul)))) +(defcomputedcolumn (CIRCUIT_SELECTOR_ECPAIRING :binary@prove) + (+ (* IS_ECPAIRING_DATA ACCPC) (* IS_ECPAIRING_RESULT (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING))))) -(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_P256_VERIFY :binary@prove) + (* ICP (is_p256_verify))) -(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)))) diff --git a/hub/osaka/columns/miscellaneous.lisp b/hub/osaka/columns/miscellaneous.lisp index 4203edb63..afad48f69 100644 --- a/hub/osaka/columns/miscellaneous.lisp +++ b/hub/osaka/columns/miscellaneous.lisp @@ -14,7 +14,7 @@ ;; EXP columns (DONE) ( EXP_INST :i16 ) - ( EXP_DATA :array [5] :i128 ) + ( EXP_DATA :array [5] :i128 ) ;;"" ;; MMU columns (DONE) ( MMU_INST :i16 :display :hex) @@ -52,7 +52,7 @@ ;; OOB columns (OOB_INST :i16 ) - (OOB_DATA :array[1:10] :i128 ) + (OOB_DATA :array[1:10] :i128 ) ;;"" ;; STP columns ( STP_INSTRUCTION :byte ) diff --git a/hub/osaka/columns/scenario.lisp b/hub/osaka/columns/scenario.lisp index b9a4cdc68..73124410c 100644 --- a/hub/osaka/columns/scenario.lisp +++ b/hub/osaka/columns/scenario.lisp @@ -66,6 +66,8 @@ (PRC_BLS_PAIRING_CHECK :binary@prove) (PRC_BLS_MAP_FP_TO_G1 :binary@prove) (PRC_BLS_MAP_FP2_TO_G2 :binary@prove) + ;; Osaka precompiles + (PRC_P256_VERIFY :binary@prove) ;; execution paths (PRC_SUCCESS_CALLER_WILL_REVERT :binary@prove) (PRC_SUCCESS_CALLER_WONT_REVERT :binary@prove) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_I.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_I.lisp index c5f79d2d9..29fe889b1 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_I.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_I.lisp @@ -20,8 +20,7 @@ (* CALL___first_half_nsr___prc_success_will_revert scenario/PRC_SUCCESS_CALLER_WILL_REVERT) (* CALL___first_half_nsr___prc_success_wont_revert scenario/PRC_SUCCESS_CALLER_WONT_REVERT) )) - - + (defun (precompile-processing---2nd-half-NSR) (+ (* (precompile-processing---2nd-half-NSR-for-ECRECOVER) scenario/PRC_ECRECOVER) @@ -34,6 +33,7 @@ (* (precompile-processing---2nd-half-NSR-for-ECPAIRING) scenario/PRC_ECPAIRING) (* (precompile-processing---2nd-half-NSR-for-BLAKE2f) scenario/PRC_BLAKE2f) (* (precompile-processing---2nd-half-NSR-for-all-BLS-precompiles) (scenario-shorthand---PRC---common-BLS-address-bit-sum)) + (* (precompile-processing---2nd-half-NSR-for-P256-VERIFY) scenario/PRC_P256_VERIFY) )) (defun (precompile-processing---2nd-half-flag-sum) @@ -48,6 +48,7 @@ (* (precompile-processing---2nd-half-flag-sum-for-ECPAIRING) scenario/PRC_ECPAIRING) (* (precompile-processing---2nd-half-flag-sum-for-BLAKE2f) scenario/PRC_BLAKE2f) (* (precompile-processing---2nd-half-flag-sum-for-all-BLS-precompiles) (scenario-shorthand---PRC---common-BLS-address-bit-sum)) + (* (precompile-processing---2nd-half-flag-sum-for-P256-VERIFY) scenario/PRC_P256_VERIFY) )) ;; Stand failure / success shorthands diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_II.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_II.lisp index 01fa79a78..2d322d670 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_II.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_II.lisp @@ -357,3 +357,30 @@ (defun (precompile-processing---flag-sum-all-BLS-FKTH) (precompile-processing---flag-sum-standard-failure)) (defun (precompile-processing---flag-sum-all-BLS-FKTR) (precompile-processing---flag-sum-standard-failure)) (defun (precompile-processing---flag-sum-all-BLS-success) (precompile-processing---flag-sum-standard-success)) + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; P256_VERIFY ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + +;; P256_VERIFY flag sum +(defun (precompile-processing---2nd-half-flag-sum-for-P256-VERIFY) + (+ (* scenario/PRC_FAILURE_KNOWN_TO_HUB) + (* (precompile-processing---flag-sum-P256-VERIFY-FKTR) scenario/PRC_FAILURE_KNOWN_TO_RAM) + (* (precompile-processing---flag-sum-P256-VERIFY-success) (scenario-shorthand---PRC---success)) + )) +;; P256_VERIFY non stack rows +(defun (precompile-processing---2nd-half-NSR-for-P256-VERIFY) + (+ (* (precompile-processing---nsr-P256-VERIFY-FKTH) scenario/PRC_FAILURE_KNOWN_TO_HUB) + (* (precompile-processing---nsr-P256-VERIFY-FKTR) scenario/PRC_FAILURE_KNOWN_TO_RAM) + (* (precompile-processing---nsr-P256-VERIFY-success) (scenario-shorthand---PRC---success)) + )) +;; P256_VERIFY non stack rows shorthands +(defun (precompile-processing---nsr-P256-VERIFY-FKTH) precompile-processing---nsr-standard-failure) +(defun (precompile-processing---nsr-P256-VERIFY-FKTR) precompile-processing---nsr-standard-failure) +(defun (precompile-processing---nsr-P256-VERIFY-success) precompile-processing---nsr-standard-success) ;; "" +;; P256_VERIFY flag sum shorthands +(defun (precompile-processing---flag-sum-P256-VERIFY-FKTH) (precompile-processing---flag-sum-standard-failure)) +(defun (precompile-processing---flag-sum-P256-VERIFY-FKTR) (precompile-processing---flag-sum-standard-failure)) +(defun (precompile-processing---flag-sum-P256-VERIFY-success) (precompile-processing---flag-sum-standard-success)) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/common/generalities.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/common/generalities.lisp index f9652effc..ada0bc42d 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/common/generalities.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/common/generalities.lisp @@ -55,6 +55,7 @@ (* OOB_INST_BLS_PAIRING_CHECK scenario/PRC_BLS_PAIRING_CHECK ) (* OOB_INST_BLS_MAP_FP_TO_G1 scenario/PRC_BLS_MAP_FP_TO_G1 ) (* OOB_INST_BLS_MAP_FP2_TO_G2 scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* OOB_INST_P256_VERIFY scenario/PRC_P256_VERIFY ) )) @@ -131,6 +132,7 @@ (* 96 scenario/PRC_ECMUL ) (* (precompile-processing---dup-cds) scenario/PRC_ECPAIRING ) (* (precompile-processing---dup-cds) (scenario-shorthand---PRC---common-BLS-address-bit-sum) ) + (* 160 scenario/PRC_P256_VERIFY ) )) (defun (precompile-processing---common---MMU-exo-sum) @@ -141,6 +143,7 @@ (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECMUL ) (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECPAIRING ) (* EXO_SUM_WEIGHT_BLSDATA (scenario-shorthand---PRC---common-BLS-address-bit-sum) ) + (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_P256_VERIFY ) )) (defun (precompile-processing---common---MMU-phase) @@ -158,6 +161,7 @@ (* PHASE_BLS_PAIRING_CHECK_DATA scenario/PRC_BLS_PAIRING_CHECK ) (* PHASE_BLS_MAP_FP_TO_G1_DATA scenario/PRC_BLS_MAP_FP_TO_G1 ) (* PHASE_BLS_MAP_FP2_TO_G2_DATA scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* PHASE_P256_VERIFY_DATA scenario/PRC_P256_VERIFY ) )) ;; ECRECOVER related shorthands @@ -194,6 +198,7 @@ scenario/PRC_ECMUL scenario/PRC_ECPAIRING (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY )) ))) @@ -208,6 +213,7 @@ scenario/PRC_ECMUL scenario/PRC_ECPAIRING (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY )))) (defconstraint precompile-processing---common---justifying-return-gas-prediction (:guard (precompile-processing---common---precondition)) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/constants.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/constants.lisp deleted file mode 100644 index 376472702..000000000 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/constants.lisp +++ /dev/null @@ -1,17 +0,0 @@ -(module hub) - -;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;; -;;;; ;;;; -;;;; X.Y CALL ;;;; -;;;; ;;;; -;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconst - ;; - precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---full-return-data-transfer 2 - precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---partial-return-data-copy 3 - precompile-processing---ECADD_MUL_PAIRING_and_BLS---context-row-offset---updating-caller-context 4 - ) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/FKTR.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/FKTR.lisp similarity index 61% rename from hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/FKTR.lisp rename to hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/FKTR.lisp index 919ad10bf..034dc36d4 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/FKTR.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/FKTR.lisp @@ -20,16 +20,17 @@ ;; Shorthands ;; ;;;;;;;;;;;;;;;; -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---FKTR-case) (* PEEK_AT_SCENARIO - (+ scenario/PRC_ECADD - scenario/PRC_ECMUL - scenario/PRC_ECPAIRING - (scenario-shorthand---PRC---common-BLS-address-bit-sum) - ) - scenario/PRC_FAILURE_KNOWN_TO_RAM)) - -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---FKTR-requires-extracting-non-empty-call-data - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---FKTR-case)) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---FKTR-case) (* PEEK_AT_SCENARIO + (+ scenario/PRC_ECADD + scenario/PRC_ECMUL + scenario/PRC_ECPAIRING + (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY + ) + scenario/PRC_FAILURE_KNOWN_TO_RAM)) + +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---FKTR-requires-extracting-non-empty-call-data + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---FKTR-case)) (eq! (precompile-processing---common---OOB-extract-call-data) 1)) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/constants.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/constants.lisp new file mode 100644 index 000000000..4c3b3d951 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/constants.lisp @@ -0,0 +1,17 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconst + ;; + precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---full-return-data-transfer 2 + precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---partial-return-data-copy 3 + precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---context-row-offset---updating-caller-context 4 + ) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/success_case.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/success_case.lisp similarity index 51% rename from hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/success_case.lisp rename to hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/success_case.lisp index d2a95a3d4..4d77de232 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls/success_case.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/ec_add_mul_pairing_bls_and_p256_verify/success_case.lisp @@ -20,25 +20,27 @@ ;; Shorthands ;; ;;;;;;;;;;;;;;;; -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case) (* PEEK_AT_SCENARIO - (+ scenario/PRC_ECADD - scenario/PRC_ECMUL - scenario/PRC_ECPAIRING - (scenario-shorthand---PRC---common-BLS-address-bit-sum) - ) - (scenario-shorthand---PRC---success) - )) - -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECADD) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECADD)) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECMUL) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECMUL)) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECPAIRING) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECPAIRING)) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---trivial-ECPAIRING) (* (precompile-processing---common---OOB-empty-call-data) scenario/PRC_ECPAIRING)) - -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-cases) (+ (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECADD) - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECMUL) - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECPAIRING) - (scenario-shorthand---PRC---common-BLS-address-bit-sum) - )) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case) (* PEEK_AT_SCENARIO + (+ scenario/PRC_ECADD + scenario/PRC_ECMUL + scenario/PRC_ECPAIRING + (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY + ) + (scenario-shorthand---PRC---success) + )) + +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECADD) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECADD)) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECMUL) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECMUL)) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECPAIRING) (* (precompile-processing---common---OOB-extract-call-data) scenario/PRC_ECPAIRING)) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---trivial-ECPAIRING) (* (precompile-processing---common---OOB-empty-call-data) scenario/PRC_ECPAIRING)) + +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-cases) (+ (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECADD) + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECMUL) + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECPAIRING) + (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY + )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -46,22 +48,23 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---second-misc-row-peeking-flags - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (eq! (weighted-MISC-flag-sum precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---full-return-data-transfer) - (* MISC_WEIGHT_MMU (precompile-processing---ECADD_MUL_PAIRING_and_BLS---trigger_MMU)))) +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---second-misc-row-peeking-flags + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (eq! (weighted-MISC-flag-sum precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---full-return-data-transfer) + (* MISC_WEIGHT_MMU (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---trigger_MMU)))) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---trigger_MMU) (+ (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECADD) - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECMUL) - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECPAIRING) - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---trivial-ECPAIRING) - (scenario-shorthand---PRC---common-BLS-address-bit-sum) - )) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---trigger_MMU) (+ (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECADD) + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECMUL) + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECPAIRING) + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---trivial-ECPAIRING) + (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY + )) -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---setting-MMU-instruction---full-return-data-transfer---trivial-case - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (if-not-zero (precompile-processing---ECADD_MUL_PAIRING_and_BLS---trivial-ECPAIRING) - (set-MMU-instruction---mstore precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---full-return-data-transfer ;; offset +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---setting-MMU-instruction---full-return-data-transfer---trivial-case + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (if-not-zero (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---trivial-ECPAIRING) + (set-MMU-instruction---mstore precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---full-return-data-transfer ;; offset ;; src_id ;; source ID (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID @@ -78,58 +81,61 @@ ;; phase ;; phase ))) -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---setting-MMU-instruction---full-return-data-transfer---nontrivial-cases - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (if-not-zero (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-cases) - (set-MMU-instruction---exo-to-ram-transplants precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---full-return-data-transfer ;; offset +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---setting-MMU-instruction---full-return-data-transfer---nontrivial-cases + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (if-not-zero (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-cases) + (set-MMU-instruction---exo-to-ram-transplants precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---full-return-data-transfer ;; offset (+ 1 HUB_STAMP) ;; source ID (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high ;; src_offset_lo ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-size) ;; size + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-size) ;; size ;; ref_offset ;; reference offset ;; ref_size ;; reference size ;; success_bit ;; success bit ;; limb_1 ;; limb 1 ;; limb_2 ;; limb 2 - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---exo-sum) ;; weighted exogenous module flag sum - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-phase) ;; phase + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---exo-sum) ;; weighted exogenous module flag sum + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-phase) ;; phase ))) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-size) (+ (* PRECOMPILE_RETURN_DATA_SIZE___ECADD (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECADD) ) - (* PRECOMPILE_RETURN_DATA_SIZE___ECMUL (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECMUL) ) - (* PRECOMPILE_RETURN_DATA_SIZE___ECPAIRING (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECPAIRING) ) - (* PRECOMPILE_RETURN_DATA_SIZE___POINT_EVALUATION scenario/PRC_POINT_EVALUATION ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_ADD scenario/PRC_BLS_G1_ADD ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_MSM scenario/PRC_BLS_G1_MSM ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_ADD scenario/PRC_BLS_G2_ADD ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_MSM scenario/PRC_BLS_G2_MSM ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK scenario/PRC_BLS_PAIRING_CHECK ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1 scenario/PRC_BLS_MAP_FP_TO_G1 ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2 scenario/PRC_BLS_MAP_FP2_TO_G2 ) - )) - -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-phase) (+ (* PHASE_ECADD_RESULT (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECADD) ) - (* PHASE_ECMUL_RESULT (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECMUL) ) - (* PHASE_ECPAIRING_RESULT (precompile-processing---ECADD_MUL_PAIRING_and_BLS---nontrivial-ECPAIRING) ) - (* PHASE_POINT_EVALUATION_RESULT scenario/PRC_POINT_EVALUATION ) - (* PHASE_BLS_G1_ADD_RESULT scenario/PRC_BLS_G1_ADD ) - (* PHASE_BLS_G1_MSM_RESULT scenario/PRC_BLS_G1_MSM ) - (* PHASE_BLS_G2_ADD_RESULT scenario/PRC_BLS_G2_ADD ) - (* PHASE_BLS_G2_MSM_RESULT scenario/PRC_BLS_G2_MSM ) - (* PHASE_BLS_PAIRING_CHECK_RESULT scenario/PRC_BLS_PAIRING_CHECK ) - (* PHASE_BLS_MAP_FP_TO_G1_RESULT scenario/PRC_BLS_MAP_FP_TO_G1 ) - (* PHASE_BLS_MAP_FP2_TO_G2_RESULT scenario/PRC_BLS_MAP_FP2_TO_G2 ) - )) - - -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---exo-sum) (+ (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECADD ) - (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECMUL ) - (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECPAIRING ) - (* EXO_SUM_WEIGHT_BLSDATA (scenario-shorthand---PRC---common-BLS-address-bit-sum) ) - )) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-size) (+ (* PRECOMPILE_RETURN_DATA_SIZE___ECADD (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECADD) ) + (* PRECOMPILE_RETURN_DATA_SIZE___ECMUL (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECMUL) ) + (* PRECOMPILE_RETURN_DATA_SIZE___ECPAIRING (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECPAIRING) ) + (* PRECOMPILE_RETURN_DATA_SIZE___POINT_EVALUATION scenario/PRC_POINT_EVALUATION ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_ADD scenario/PRC_BLS_G1_ADD ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_MSM scenario/PRC_BLS_G1_MSM ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_ADD scenario/PRC_BLS_G2_ADD ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_MSM scenario/PRC_BLS_G2_MSM ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK scenario/PRC_BLS_PAIRING_CHECK ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1 scenario/PRC_BLS_MAP_FP_TO_G1 ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2 scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* PRECOMPILE_RETURN_DATA_SIZE___P256_VERIFY scenario/PRC_P256_VERIFY ) + )) + +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-phase) (+ (* PHASE_ECADD_RESULT (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECADD) ) + (* PHASE_ECMUL_RESULT (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECMUL) ) + (* PHASE_ECPAIRING_RESULT (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---nontrivial-ECPAIRING) ) + (* PHASE_POINT_EVALUATION_RESULT scenario/PRC_POINT_EVALUATION ) + (* PHASE_BLS_G1_ADD_RESULT scenario/PRC_BLS_G1_ADD ) + (* PHASE_BLS_G1_MSM_RESULT scenario/PRC_BLS_G1_MSM ) + (* PHASE_BLS_G2_ADD_RESULT scenario/PRC_BLS_G2_ADD ) + (* PHASE_BLS_G2_MSM_RESULT scenario/PRC_BLS_G2_MSM ) + (* PHASE_BLS_PAIRING_CHECK_RESULT scenario/PRC_BLS_PAIRING_CHECK ) + (* PHASE_BLS_MAP_FP_TO_G1_RESULT scenario/PRC_BLS_MAP_FP_TO_G1 ) + (* PHASE_BLS_MAP_FP2_TO_G2_RESULT scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* PHASE_P256_VERIFY_RESULT scenario/PRC_P256_VERIFY ) + )) + + +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---exo-sum) (+ (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECADD ) + (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECMUL ) + (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECPAIRING ) + (* EXO_SUM_WEIGHT_BLSDATA (scenario-shorthand---PRC---common-BLS-address-bit-sum)) + (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_P256_VERIFY ) + )) @@ -140,24 +146,24 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---third-misc-row-peeking-flags - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (eq! (weighted-MISC-flag-sum precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---partial-return-data-copy) +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---third-misc-row-peeking-flags + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (eq! (weighted-MISC-flag-sum precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---partial-return-data-copy) (* MISC_WEIGHT_MMU (precompile-processing---common---OOB-r@c-nonzero)))) -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---setting-the-MMU-instruction---partial-return-data-copy - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---partial-return-data-copy) - (set-MMU-instruction---ram-to-ram-sans-padding precompile-processing---ECADD_MUL_PAIRING_and_BLS---misc-row-offset---partial-return-data-copy ;; offset +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---setting-the-MMU-instruction---partial-return-data-copy + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (if-not-zero (shift misc/MMU_FLAG precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---partial-return-data-copy) + (set-MMU-instruction---ram-to-ram-sans-padding precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---misc-row-offset---partial-return-data-copy ;; offset (+ 1 HUB_STAMP) ;; source ID CONTEXT_NUMBER ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high 0 ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-reference-size) ;; size + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-reference-size) ;; size (precompile-processing---dup-r@o) ;; reference offset (precompile-processing---dup-r@c) ;; reference size ;; success_bit ;; success bit @@ -167,18 +173,19 @@ ;; phase ;; phase ))) -(defun (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-reference-size) (+ (* PRECOMPILE_RETURN_DATA_SIZE___ECADD scenario/PRC_ECADD ) - (* PRECOMPILE_RETURN_DATA_SIZE___ECMUL scenario/PRC_ECMUL ) - (* PRECOMPILE_RETURN_DATA_SIZE___ECPAIRING scenario/PRC_ECPAIRING ) - (* PRECOMPILE_RETURN_DATA_SIZE___POINT_EVALUATION scenario/PRC_POINT_EVALUATION ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_ADD scenario/PRC_BLS_G1_ADD ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_MSM scenario/PRC_BLS_G1_MSM ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_ADD scenario/PRC_BLS_G2_ADD ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_MSM scenario/PRC_BLS_G2_MSM ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK scenario/PRC_BLS_PAIRING_CHECK ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1 scenario/PRC_BLS_MAP_FP_TO_G1 ) - (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2 scenario/PRC_BLS_MAP_FP2_TO_G2 ) - )) +(defun (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-reference-size) (+ (* PRECOMPILE_RETURN_DATA_SIZE___ECADD scenario/PRC_ECADD ) + (* PRECOMPILE_RETURN_DATA_SIZE___ECMUL scenario/PRC_ECMUL ) + (* PRECOMPILE_RETURN_DATA_SIZE___ECPAIRING scenario/PRC_ECPAIRING ) + (* PRECOMPILE_RETURN_DATA_SIZE___POINT_EVALUATION scenario/PRC_POINT_EVALUATION ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_ADD scenario/PRC_BLS_G1_ADD ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G1_MSM scenario/PRC_BLS_G1_MSM ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_ADD scenario/PRC_BLS_G2_ADD ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_G2_MSM scenario/PRC_BLS_G2_MSM ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK scenario/PRC_BLS_PAIRING_CHECK ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1 scenario/PRC_BLS_MAP_FP_TO_G1 ) + (* PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2 scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* PRECOMPILE_RETURN_DATA_SIZE___P256_VERIFY scenario/PRC_P256_VERIFY ) + )) ;;;;;;;;;;;;;;;;;;;;;;; @@ -186,11 +193,11 @@ ;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---ECADD_MUL_PAIRING_and_BLS---updating-caller-context-with-precompile-return-data - (:guard (precompile-processing---ECADD_MUL_PAIRING_and_BLS---success-case)) - (provide-return-data precompile-processing---ECADD_MUL_PAIRING_and_BLS---context-row-offset---updating-caller-context ;; row offset +(defconstraint precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---updating-caller-context-with-precompile-return-data + (:guard (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---success-case)) + (provide-return-data precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---context-row-offset---updating-caller-context ;; row offset CONTEXT_NUMBER ;; receiver context (+ 1 HUB_STAMP) ;; provider context 0 ;; rdo - (precompile-processing---ECADD_MUL_PAIRING_and_BLS---return-data-reference-size) ;; rds + (precompile-processing---ECADD_MUL_PAIRING_BLS_and_P256_VERIFY---return-data-reference-size) ;; rds )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp deleted file mode 100644 index f8b58381a..000000000 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp +++ /dev/null @@ -1,280 +0,0 @@ -(module hub) - -;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;; -;;;; ;;;; -;;;; X.Y CALL ;;;; -;;;; ;;;; -;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;; - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; X.Y.Z.4 MODEXP common processing ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defun (precompile-processing---MODEXP---standard-precondition) (* PEEK_AT_SCENARIO scenario/PRC_MODEXP)) - -(defconstraint precompile-processing---MODEXP---excluding-execution-scenarios (:guard (precompile-processing---MODEXP---standard-precondition)) - (vanishes! scenario/PRC_FAILURE_KNOWN_TO_HUB)) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) - MISC_WEIGHT_OOB)) - -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset - (precompile-processing---dup-cds))) ;; call data size - -(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) -(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) -(defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-analysis) - (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) - MISC_WEIGHT_OOB) - )) - -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset - CONTEXT_NUMBER ;; source ID - ;; tgt_id ;; target ID - ;; aux_id ;; auxiliary ID - ;; src_offset_hi ;; source offset high - 0 ;; source offset low - ;; tgt_offset_lo ;; target offset low - ;; size ;; size - (precompile-processing---dup-cdo) ;; reference offset - (precompile-processing---dup-cds) ;; reference size - ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE - ;; exo_sum ;; weighted exogenous module flag sum - ;; phase ;; phase - ))) - -(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) -(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) - -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset - (precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs - (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs - 0 ;; low part of some {b,e,m}bs - 0 ;; bit indicating whether to compute max(xbs, ybs) or not - )) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-analysis) - (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) - MISC_WEIGHT_OOB) - )) - -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset - CONTEXT_NUMBER ;; source ID - ;; tgt_id ;; target ID - ;; aux_id ;; auxiliary ID - ;; src_offset_hi ;; source offset high - 32 ;; source offset low - ;; tgt_offset_lo ;; target offset low - ;; size ;; size - (precompile-processing---dup-cdo) ;; reference offset - (precompile-processing---dup-cds) ;; reference size - ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE - ;; exo_sum ;; weighted exogenous module flag sum - ;; phase ;; phase - ))) - -(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) -(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) - -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset - (precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs - (precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs - 0 ;; low part of some {b,e,m}bs - 0 ;; bit indicating whether to compute max(xbs, ybs) or not - )) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; mbs extraction and analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-analysis) - (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) - MISC_WEIGHT_OOB) - )) - -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset - CONTEXT_NUMBER ;; source ID - ;; tgt_id ;; target ID - ;; aux_id ;; auxiliary ID - ;; src_offset_hi ;; source offset high - 64 ;; source offset low - ;; tgt_offset_lo ;; target offset low - ;; size ;; size - (precompile-processing---dup-cdo) ;; reference offset - (precompile-processing---dup-cds) ;; reference size - ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE - ;; exo_sum ;; weighted exogenous module flag sum - ;; phase ;; phase - ))) - -(defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) -(defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) - -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset - (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs - (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs - (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs - 1 ;; bit indicating whether to compute max(xbs, ybs) or not - )) - - -(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) -(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) - (+ (* MISC_WEIGHT_EXP (precompile-processing---MODEXP---load-lead)) - (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---load-lead)) - MISC_WEIGHT_OOB) - )) - -(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset - (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) - (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) - )) - -(defun (precompile-processing---MODEXP---load-lead) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" - - -(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) - (set-MMU-instruction---mload precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset - CONTEXT_NUMBER ;; source ID - ;; tgt_id ;; target ID - ;; aux_id ;; auxiliary ID - ;; src_offset_hi ;; source offset high - (+ (precompile-processing---dup-cdo) - 96 - (precompile-processing---MODEXP---bbs-lo)) ;; source offset low - ;; tgt_offset_lo ;; target offset low - ;; size ;; size - ;; ref_offset ;; reference offset - ;; ref_size ;; reference size - ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE - ;; exo_sum ;; weighted exogenous module flag sum - ;; phase ;; phase - ))) - -(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---load-lead) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---load-lead) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) - - -(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) - (set-EXP-instruction-MODEXP-lead-log - precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset - (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part - (precompile-processing---MODEXP---raw-lead-lo) ;; raw leading word where exponent starts, low part - (precompile-processing---MODEXP---cds-cutoff) ;; min{max{cds - 96 - bbs, 0}, 32} - (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} - ))) - -(defun (precompile-processing---MODEXP---lead-log) (* (precompile-processing---MODEXP---load-lead) (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) (* 8 (precompile-processing---MODEXP---sub-ebs-32)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; pricing analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing) - MISC_WEIGHT_OOB - )) - -(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset - (precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile - (precompile-processing---dup-r@c) ;; return at capacity - (precompile-processing---MODEXP---modexp-full-log) ;; leading (≤) word log of exponent - (precompile-processing---MODEXP---max-mbs-bbs) ;; call data size - )) - -(defun (precompile-processing---MODEXP---ram-success) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---pricing)) -(defun (precompile-processing---MODEXP---return-gas) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---pricing)) -(defun (precompile-processing---MODEXP---r@c-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---pricing)) ;; "" - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Justifying precompile success / failure scenarios ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint precompile-processing---MODEXP---justifying-success-failure-scenarios (:guard (precompile-processing---MODEXP---standard-precondition)) - (begin - (eq! (scenario-shorthand---PRC---success) (precompile-processing---MODEXP---ram-success)) - (eq! (precompile-processing---prd-return-gas) (precompile-processing---MODEXP---return-gas)) - )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp new file mode 100644 index 000000000..d1f219a69 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp @@ -0,0 +1,43 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) + MISC_WEIGHT_OOB)) + + +(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset + (precompile-processing---dup-cds))) ;; call data size + + +(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" +(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" +(defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp new file mode 100644 index 000000000..f7a27ad12 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp @@ -0,0 +1,74 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) + MISC_WEIGHT_OOB) + )) + + +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 0 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis))) + + +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset + (precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs + 0 ;; low part of some {b,e,m}bs + 0 ;; bit indicating whether to compute max(xbs, ybs) or not + )) + + +(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---bbs-normalized) (* (precompile-processing---MODEXP---bbs-lo) + (precompile-processing---MODEXP---bbs-within-bounds))) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp new file mode 100644 index 000000000..147cb611b --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp @@ -0,0 +1,75 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) + MISC_WEIGHT_OOB) + )) + + +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 32 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + + +(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))) + + +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset + (precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs + 0 ;; low part of some {b,e,m}bs + 0 ;; bit indicating whether to compute max(xbs, ybs) or not + )) + + +(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) +(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---ebs-normalized) (* (precompile-processing---MODEXP---ebs-lo) + (precompile-processing---MODEXP---ebs-within-bounds))) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp new file mode 100644 index 000000000..32f48eebb --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp @@ -0,0 +1,82 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; mbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) + MISC_WEIGHT_OOB) + )) + + +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 64 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + + +(defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis))) + + +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis ;; offset + (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-normalized) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-within-bounds) ;; bit indicating whether to compute max(xbs, ybs) or not + )) + + +(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-normalized) (* (precompile-processing---MODEXP---mbs-lo) + (precompile-processing---MODEXP---mbs-within-bounds))) + +(defun (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) (* (precompile-processing---MODEXP---bbs-within-bounds) + (precompile-processing---MODEXP---ebs-within-bounds) + (precompile-processing---MODEXP---mbs-within-bounds) + )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp new file mode 100644 index 000000000..50318fcae --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp @@ -0,0 +1,100 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-OOB-on-leading-word-row) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) + + +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (precompile-processing---MODEXP---extract-leading-word) ) + (eq! (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (precompile-processing---MODEXP---extract-leading-word) ) + (eq! (precompile-processing---MODEXP---call-OOB-on-leading-word-row) 1 ) + (eq! (+ (shift misc/MXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) + (shift misc/STP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) + 0) + )) + + +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) + (precompile-processing---dup-cds) ;; call data size + (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) + )) + +(defun (precompile-processing---MODEXP---extract-leading-word) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---cds-cutoff) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---ebs-cutoff) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---sub-ebs-32) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" + + +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) + (set-MMU-instruction---mload precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + (+ (precompile-processing---dup-cdo) + 96 + (precompile-processing---MODEXP---bbs-normalized)) ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + ;; ref_offset ;; reference offset + ;; ref_size ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) + + +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) + (set-EXP-instruction-MODEXP-lead-log precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset + (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part + (precompile-processing---MODEXP---raw-lead-lo) ;; raw leading word where exponent starts, low part + (precompile-processing---MODEXP---cds-cutoff) ;; min{max{cds - 96 - bbs, 0}, 32} + (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} + ))) + +(defun (precompile-processing---MODEXP---lead-log) (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) (* 16 (precompile-processing---MODEXP---sub-ebs-32)))) + +;; @OLIVIER: on reprend ici; pas sûr que modexp-full-log soit bien défini (filtres différents) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp new file mode 100644 index 000000000..2faa93e97 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp @@ -0,0 +1,46 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; pricing analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing) + MISC_WEIGHT_OOB + )) + + +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset + (precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile + (precompile-processing---dup-r@c) ;; return at capacity + (precompile-processing---MODEXP---modexp-full-log) ;; leading (≤) word log of exponent + (precompile-processing---MODEXP---max-mbs-bbs) ;; call data size + )) + +(defun (precompile-processing---MODEXP---ram-success) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---pricing)) +(defun (precompile-processing---MODEXP---return-gas) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---pricing)) +(defun (precompile-processing---MODEXP---r@c-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---pricing)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp new file mode 100644 index 000000000..41d70f7bf --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (precompile-processing---MODEXP---standard-precondition) (* PEEK_AT_SCENARIO scenario/PRC_MODEXP)) + +(defconstraint precompile-processing---MODEXP---excluding-execution-scenarios + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! scenario/PRC_FAILURE_KNOWN_TO_HUB)) + diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp new file mode 100644 index 000000000..6733a8c90 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -0,0 +1,32 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Justifying precompile success / failure scenarios ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---justifying-success-failure-scenarios + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (scenario-shorthand---PRC---success) (* (precompile-processing---MODEXP---ram-success) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) ) + (eq! (precompile-processing---prd-return-gas) (* (precompile-processing---MODEXP---return-gas) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) ) + )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp index f9b7545f0..1ef0064d2 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp @@ -11,9 +11,9 @@ (defconst precompile-processing---MODEXP---misc-row-offset---cds-analysis 1 - precompile-processing---MODEXP---misc-row-offset---bbs-analysis 2 - precompile-processing---MODEXP---misc-row-offset---ebs-analysis 3 - precompile-processing---MODEXP---misc-row-offset---mbs-analysis 4 + precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis 2 + precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis 3 + precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis 4 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis 5 precompile-processing---MODEXP---misc-row-offset---pricing 6 precompile-processing---MODEXP---misc-row-offset---base-extraction 7 diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp index e8339c966..eb01e306b 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp @@ -44,9 +44,9 @@ (defconstraint precompile-processing---MODEXP---success-case---base-extraction-row---setting-the-OOB-instruction-which-decides-which-actual-parameters-to-extract (:guard (precompile-processing---MODEXP---success-case)) (set-OOB-instruction---modexp-extract precompile-processing---MODEXP---misc-row-offset---base-extraction ;; offset (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) - (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) - (precompile-processing---MODEXP---mbs-lo) ;; low part of mbs (modulus byte size) + (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) + (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) + (precompile-processing---MODEXP---mbs-normalized) ;; low part of mbs (modulus byte size) )) ;; Note: we deduce some shorthands AT THE END OF THE FILE. @@ -79,7 +79,7 @@ ;; src_offset_hi ;; source offset high 96 ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---bbs-lo) ;; size + (precompile-processing---MODEXP---bbs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -127,9 +127,9 @@ (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (+ 96 (precompile-processing---MODEXP---bbs-lo)) ;; source offset low + (+ 96 (precompile-processing---MODEXP---bbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---ebs-lo) ;; size + (precompile-processing---MODEXP---ebs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -157,12 +157,14 @@ ;; extract_modulus == 1 case: (set-MMU-instruction---modexp-data precompile-processing---MODEXP---misc-row-offset---modulus-extraction ;; offset CONTEXT_NUMBER ;; source ID - (+ 1 HUB_STAMP) ;; target ID + (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (+ 96 (precompile-processing---MODEXP---bbs-lo) (precompile-processing---MODEXP---ebs-lo)) ;; source offset low + (+ 96 + (precompile-processing---MODEXP---bbs-normalized) + (precompile-processing---MODEXP---ebs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---mbs-lo) ;; size + (precompile-processing---MODEXP---mbs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -194,7 +196,7 @@ ;; src_offset_hi ;; source offset high ;; src_offset_lo ;; source offset low ;; tgt_offset_lo ;; target offset low - 512 ;; size + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND ;; size ;; ref_offset ;; reference offset ;; ref_size ;; reference size ;; success_bit ;; success bit @@ -225,9 +227,10 @@ CONTEXT_NUMBER ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (- 512 (precompile-processing---MODEXP---mbs-lo)) ;; source offset low + (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND + (precompile-processing---MODEXP---mbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---mbs-lo) ;; size + (precompile-processing---MODEXP---mbs-normalized) ;; size (precompile-processing---dup-r@o) ;; reference offset (precompile-processing---dup-r@c) ;; reference size ;; success_bit ;; success bit @@ -248,8 +251,9 @@ (provide-return-data precompile-processing---MODEXP---context-row-offset---success ;; row offset CONTEXT_NUMBER ;; receiver context (+ 1 HUB_STAMP) ;; provider context - (- 512 (precompile-processing---MODEXP---mbs-lo)) ;; rdo - (precompile-processing---MODEXP---mbs-lo) ;; rds + (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND + (precompile-processing---MODEXP---mbs-normalized)) ;; rdo + (precompile-processing---MODEXP---mbs-normalized) ;; rds )) diff --git a/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/exp.lisp b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/exp.lisp new file mode 100644 index 000000000..684924032 --- /dev/null +++ b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/exp.lisp @@ -0,0 +1,19 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X Miscellaneous-rows ;; +;; X.Y Automatic vanishing constraints ;; +;; X.Y.Z EXP sub-perspective ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint misc-rows---automatic-vanishing-of-columns-in-inactive-sub-perspectives---EXP-sub-perspective + (:guard PEEK_AT_MISCELLANEOUS) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero misc/EXP_FLAG + (begin + (vanishes! misc/EXP_INST ) + (for k [5] (vanishes! [ misc/EXP_DATA k ] )) ;; "" + ))) diff --git a/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mmu.lisp b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mmu.lisp new file mode 100644 index 000000000..57bfd6946 --- /dev/null +++ b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mmu.lisp @@ -0,0 +1,32 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X Miscellaneous-rows ;; +;; X.Y Automatic vanishing constraints ;; +;; X.Y.Z MMU sub-perspective ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint misc-rows---automatic-vanishing-of-columns-in-inactive-sub-perspectives---MMU-sub-perspective + (:guard PEEK_AT_MISCELLANEOUS) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero misc/MMU_FLAG + (begin + (vanishes! misc/MMU_INST ) + (vanishes! misc/MMU_SRC_ID ) + (vanishes! misc/MMU_TGT_ID ) + (vanishes! misc/MMU_AUX_ID ) + (vanishes! misc/MMU_SRC_OFFSET_LO ) + (vanishes! misc/MMU_SRC_OFFSET_HI ) + (vanishes! misc/MMU_TGT_OFFSET_LO ) + (vanishes! misc/MMU_SIZE ) + (vanishes! misc/MMU_REF_OFFSET ) + (vanishes! misc/MMU_REF_SIZE ) + (vanishes! misc/MMU_SUCCESS_BIT ) + (vanishes! misc/MMU_LIMB_1 ) + (vanishes! misc/MMU_LIMB_2 ) + (vanishes! misc/MMU_PHASE ) + (vanishes! misc/MMU_EXO_SUM ) + ))) diff --git a/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mxp.lisp b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mxp.lisp new file mode 100644 index 000000000..97997f2b3 --- /dev/null +++ b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/mxp.lisp @@ -0,0 +1,33 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X Miscellaneous-rows ;; +;; X.Y Automatic vanishing constraints ;; +;; X.Y.Z MXP sub-perspective ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint misc-rows---automatic-vanishing-of-columns-in-inactive-sub-perspectives---MXP-sub-perspective + (:guard PEEK_AT_MISCELLANEOUS) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero misc/MXP_FLAG + (begin + (vanishes! misc/MXP_INST ) + (vanishes! misc/MXP_MXPX ) + (vanishes! misc/MXP_DEPLOYS ) + (vanishes! misc/MXP_OFFSET_1_HI ) + (vanishes! misc/MXP_OFFSET_1_LO ) + (vanishes! misc/MXP_OFFSET_2_HI ) + (vanishes! misc/MXP_OFFSET_2_LO ) + (vanishes! misc/MXP_SIZE_1_HI ) + (vanishes! misc/MXP_SIZE_1_LO ) + (vanishes! misc/MXP_SIZE_2_HI ) + (vanishes! misc/MXP_SIZE_2_LO ) + (vanishes! misc/MXP_WORDS ) + (vanishes! misc/MXP_GAS_MXP ) + (vanishes! misc/MXP_SIZE_1_NONZERO_NO_MXPX ) + (vanishes! misc/MXP_SIZE_2_NONZERO_NO_MXPX ) + ))) + diff --git a/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/oob.lisp b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/oob.lisp new file mode 100644 index 000000000..bc0ec37d9 --- /dev/null +++ b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/oob.lisp @@ -0,0 +1,19 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X Miscellaneous-rows ;; +;; X.Y Automatic vanishing constraints ;; +;; X.Y.Z OOB sub-perspective ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint misc-rows---automatic-vanishing-of-columns-in-inactive-sub-perspectives---OOB-sub-perspective + (:guard PEEK_AT_MISCELLANEOUS) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero misc/OOB_FLAG + (begin + (vanishes! misc/OOB_INST ) + (for k [1:10] (vanishes! [ misc/OOB_DATA k ] )) ;; "" + ))) diff --git a/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/stp.lisp b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/stp.lisp new file mode 100644 index 000000000..a11d656e8 --- /dev/null +++ b/hub/osaka/constraints/miscellaneous-rows/automatic-vanishing/stp.lisp @@ -0,0 +1,29 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X Miscellaneous-rows ;; +;; X.Y Automatic vanishing constraints ;; +;; X.Y.Z STP sub-perspective ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint misc-rows---automatic-vanishing-of-columns-in-inactive-sub-perspectives---STP-sub-perspective + (:guard PEEK_AT_MISCELLANEOUS) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero misc/STP_FLAG + (begin + (vanishes! misc/STP_INSTRUCTION ) + (vanishes! misc/STP_GAS_HI ) + (vanishes! misc/STP_GAS_LO ) + (vanishes! misc/STP_VALUE_HI ) + (vanishes! misc/STP_VALUE_LO ) + (vanishes! misc/STP_EXISTS ) + (vanishes! misc/STP_WARMTH ) + (vanishes! misc/STP_OOGX ) + (vanishes! misc/STP_GAS_MXP ) + (vanishes! misc/STP_GAS_UPFRONT_GAS_COST ) + (vanishes! misc/STP_GAS_PAID_OUT_OF_POCKET ) + (vanishes! misc/STP_GAS_STIPEND ) + ))) diff --git a/hub/osaka/constraints/scenario-rows/shorthands/precompile.lisp b/hub/osaka/constraints/scenario-rows/shorthands/precompile.lisp index bd9f0e141..e6ff274d1 100644 --- a/hub/osaka/constraints/scenario-rows/shorthands/precompile.lisp +++ b/hub/osaka/constraints/scenario-rows/shorthands/precompile.lisp @@ -30,6 +30,7 @@ ;; scenario/PRC_BLS_MAP_FP_TO_G1 ;; scenario/PRC_BLS_MAP_FP2_TO_G2 (scenario-shorthand---PRC---common-BLS-address-bit-sum) + scenario/PRC_P256_VERIFY ))) @@ -126,6 +127,7 @@ (* 15 scenario/PRC_BLS_PAIRING_CHECK ) (* 16 scenario/PRC_BLS_MAP_FP_TO_G1 ) (* 17 scenario/PRC_BLS_MAP_FP2_TO_G2 ) + (* 256 scenario/PRC_P256_VERIFY ) ;; scenario/PRC_SUCCESS_CALLER_WILL_REVERT ;; scenario/PRC_SUCCESS_CALLER_WONT_REVERT ;; scenario/PRC_FAILURE_KNOWN_TO_HUB diff --git a/mmu/osaka/constants.lisp b/mmu/osaka/constants.lisp index e4886e2e8..fef81d25d 100644 --- a/mmu/osaka/constants.lisp +++ b/mmu/osaka/constants.lisp @@ -53,8 +53,8 @@ ;;NB_MICRO_ROWS_TOT_RAM_TO_RAM_SANS_PADDING variable ;;NB_MICRO_ROWS_TOT_ANY_TO_RAM_WITH_PADDING_PURE_PADDING variable ;;NB_MICRO_ROWS_TOT_ANY_TO_RAM_WITH_PADDING_SOME_DATA variable - NB_MICRO_ROWS_TOT_MODEXP_ZERO 32 - NB_MICRO_ROWS_TOT_MODEXP_DATA 32 + NB_MICRO_ROWS_TOT_MODEXP_ZERO 64 + NB_MICRO_ROWS_TOT_MODEXP_DATA 64 NB_MICRO_ROWS_TOT_BLAKE 2) diff --git a/mmu/osaka/instructions/modexp_data.lisp b/mmu/osaka/instructions/modexp_data.lisp index 8029feb98..7c80658b8 100644 --- a/mmu/osaka/instructions/modexp_data.lisp +++ b/mmu/osaka/instructions/modexp_data.lisp @@ -30,9 +30,9 @@ (defun (modexp-data---exo-sum) macro/EXO_SUM) (defun (modexp-data---phase) macro/PHASE) (defun (modexp-data---param-byte-size) (modexp-data---size)) -(defun (modexp-data---param-offset) (+ (modexp-data---cdo) (modexp-data---src-offset))) -(defun (modexp-data---leftover-data-size) (- (modexp-data---cds) (modexp-data---src-offset))) -(defun (modexp-data---num-left-padding-bytes) (- 512 (modexp-data---param-byte-size))) +(defun (modexp-data---param-offset) (+ (modexp-data---cdo) (modexp-data---src-offset))) +(defun (modexp-data---leftover-data-size) (- (modexp-data---cds) (modexp-data---src-offset))) +(defun (modexp-data---num-left-padding-bytes) (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND (modexp-data---param-byte-size))) (defun (modexp-data---data-runs-out) (shift prprc/WCP_RES 2)) (defun (modexp-data---num-right-padding-bytes) (* (- (modexp-data---param-byte-size) (modexp-data---leftover-data-size)) (modexp-data---data-runs-out))) (defun (modexp-data---right-padding-remainder) (shift prprc/EUC_REM 2)) @@ -40,9 +40,10 @@ (defun (modexp-data---middle-sbo) (shift prprc/EUC_REM 6)) ;; "" -(defconstraint modexp-data---setting-TOT (:guard (* MACRO IS_MODEXP_DATA)) - ;; Setting total number of mmio inst - (eq! TOT NB_MICRO_ROWS_TOT_MODEXP_DATA)) +(defconstraint modexp-data---number-of-preprocessing-rows-ie-setting-TOT (:guard (* MACRO IS_MODEXP_DATA)) + ;; Setting total number of mmio inst + (eq! TOT + NB_MICRO_ROWS_TOT_MODEXP_DATA)) (defconstraint modexp-data---1st-preprocessing-row (:guard (* MACRO IS_MODEXP_DATA)) (begin @@ -64,7 +65,8 @@ (modexp-data---num-right-padding-bytes) LLARGE) (eq! TOTRZ (shift prprc/EUC_QUOT 2)) - (debug (eq! TOTNT (- 32 (+ TOTLZ TOTRZ)))))) + (debug (eq! TOTNT (- NB_MICRO_ROWS_TOT_MODEXP_DATA + (+ TOTLZ TOTRZ)))))) (defconstraint modexp-data---3rd-preprocessing-row (:guard (* MACRO IS_MODEXP_DATA)) (begin diff --git a/mmu/osaka/instructions/modexp_zero.lisp b/mmu/osaka/instructions/modexp_zero.lisp index dec3c0c96..3232782ce 100644 --- a/mmu/osaka/instructions/modexp_zero.lisp +++ b/mmu/osaka/instructions/modexp_zero.lisp @@ -16,7 +16,7 @@ (defconstraint modexp-zero---setting-the-TOTs (:guard (* MACRO IS_MODEXP_ZERO)) (begin (vanishes! TOTLZ) - (eq! TOTNT NB_MICRO_ROWS_TOT_MODEXP_ZERO) + (eq! TOTNT NB_MICRO_ROWS_TOT_MODEXP_ZERO) (vanishes! TOTRZ))) (defconstraint modexp-zero---setting-micro-instruction-constant-values (:guard (* MACRO IS_MODEXP_ZERO)) diff --git a/oob/cancun/precompiles/modexp/xbs.lisp b/oob/cancun/precompiles/modexp/xbs.lisp index fbaaf481a..fda951eca 100644 --- a/oob/cancun/precompiles/modexp/xbs.lisp +++ b/oob/cancun/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (defun (prc-modexp-xbs---compute-max) [DATA 4]) (defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) (defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO) (defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) (defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) @@ -28,7 +28,7 @@ (defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) + (eq! (prc-modexp-xbs---comparison-to-512) 1))) (defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (if-zero (prc-modexp-xbs---compute-max) diff --git a/oob/london/precompiles/modexp/xbs.lisp b/oob/london/precompiles/modexp/xbs.lisp index fbaaf481a..fda951eca 100644 --- a/oob/london/precompiles/modexp/xbs.lisp +++ b/oob/london/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (defun (prc-modexp-xbs---compute-max) [DATA 4]) (defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) (defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO) (defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) (defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) @@ -28,7 +28,7 @@ (defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) + (eq! (prc-modexp-xbs---comparison-to-512) 1))) (defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (if-zero (prc-modexp-xbs---compute-max) diff --git a/oob/osaka/columns.lisp b/oob/osaka/columns.lisp index 8036a4102..fc5b5e2e4 100644 --- a/oob/osaka/columns.lisp +++ b/oob/osaka/columns.lisp @@ -38,6 +38,7 @@ (IS_BLS_PAIRING_CHECK :binary@prove) (IS_BLS_MAP_FP_TO_G1 :binary@prove) (IS_BLS_MAP_FP2_TO_G2 :binary@prove) + (IS_P256_VERIFY :binary@prove) (WCP_FLAG :binary@prove) (ADD_FLAG :binary@prove) (MOD_FLAG :binary@prove) diff --git a/oob/osaka/constants.lisp b/oob/osaka/constants.lisp index 0566d1243..bfdc94b84 100644 --- a/oob/osaka/constants.lisp +++ b/oob/osaka/constants.lisp @@ -33,6 +33,7 @@ CT_MAX_BLS_PAIRING_CHECK 4 CT_MAX_BLS_MAP_FP_TO_G1 3 CT_MAX_BLS_MAP_FP2_TO_G2 3 + CT_MAX_P256_VERIFY 3 G_QUADDIVISOR 3) diff --git a/oob/osaka/heartbeat.lisp b/oob/osaka/heartbeat.lisp index 585d60b37..61096f4de 100644 --- a/oob/osaka/heartbeat.lisp +++ b/oob/osaka/heartbeat.lisp @@ -23,7 +23,7 @@ (vanishes! CT))) (defconstraint ct-max () - (eq! CT_MAX (maxct-sum))) + (eq! CT_MAX (ct-max-sum))) (defconstraint non-trivial-instruction-counter-cycle () (if-not-zero STAMP diff --git a/oob/osaka/precompiles/common/bls/bls_msm.lisp b/oob/osaka/precompiles/common/post_cancun/bls_msm.lisp similarity index 100% rename from oob/osaka/precompiles/common/bls/bls_msm.lisp rename to oob/osaka/precompiles/common/post_cancun/bls_msm.lisp diff --git a/oob/osaka/precompiles/common/bls/bls_pairing_check.lisp b/oob/osaka/precompiles/common/post_cancun/bls_pairing_check.lisp similarity index 100% rename from oob/osaka/precompiles/common/bls/bls_pairing_check.lisp rename to oob/osaka/precompiles/common/post_cancun/bls_pairing_check.lisp diff --git a/oob/osaka/precompiles/common/bls/point_evaluation_bls_adds_bls_maps.lisp b/oob/osaka/precompiles/common/post_cancun/point_evaluation_bls_adds_bls_maps.lisp similarity index 89% rename from oob/osaka/precompiles/common/bls/point_evaluation_bls_adds_bls_maps.lisp rename to oob/osaka/precompiles/common/post_cancun/point_evaluation_bls_adds_bls_maps.lisp index 77e5de530..48bf40312 100644 --- a/oob/osaka/precompiles/common/bls/point_evaluation_bls_adds_bls_maps.lisp +++ b/oob/osaka/precompiles/common/post_cancun/point_evaluation_bls_adds_bls_maps.lisp @@ -12,19 +12,23 @@ IS_BLS_G1_ADD IS_BLS_G2_ADD IS_BLS_MAP_FP_TO_G1 - IS_BLS_MAP_FP2_TO_G2)) + IS_BLS_MAP_FP2_TO_G2 + IS_P256_VERIFY)) (defun (fixed-cds) (+ (* PRECOMPILE_CALL_DATA_SIZE___POINT_EVALUATION IS_POINT_EVALUATION) (* PRECOMPILE_CALL_DATA_SIZE___G1_ADD IS_BLS_G1_ADD) (* PRECOMPILE_CALL_DATA_SIZE___G2_ADD IS_BLS_G2_ADD) (* PRECOMPILE_CALL_DATA_SIZE___FP_TO_G1 IS_BLS_MAP_FP_TO_G1) - (* PRECOMPILE_CALL_DATA_SIZE___FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2))) + (* PRECOMPILE_CALL_DATA_SIZE___FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2) + (* PRECOMPILE_CALL_DATA_SIZE___P256_VERIFY IS_P256_VERIFY))) (defun (fixed-gast-cost) (+ (* GAS_CONST_POINT_EVALUATION IS_POINT_EVALUATION) (* GAS_CONST_BLS_G1_ADD IS_BLS_G1_ADD) (* GAS_CONST_BLS_G2_ADD IS_BLS_G2_ADD) (* GAS_CONST_BLS_MAP_FP_TO_G1 IS_BLS_MAP_FP_TO_G1) - (* GAS_CONST_BLS_MAP_FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2))) + (* GAS_CONST_BLS_MAP_FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2) + (* GAS_CONST_P256_VERIFY IS_P256_VERIFY))) + (defun (prc-pointevaluation-prc-blsg1add-prc-blsg2add-prc-blsmapfptog1-prc-blsmapfp2tog2---precompile-cost) (fixed-gast-cost)) (defun (prc-pointevaluation-prc-blsg1add-prc-blsg2add-prc-blsmapfptog1-prc-blsmapfp2tog2---valid-cds) (shift OUTGOING_RES_LO 2)) (defun (prc-pointevaluation-prc-blsg1add-prc-blsg2add-prc-blsmapfptog1-prc-blsmapfp2tog2---sufficient-gas) (- 1 (shift OUTGOING_RES_LO 3))) diff --git a/oob/osaka/precompiles/modexp/lead.lisp b/oob/osaka/precompiles/modexp/lead.lisp index d02040e00..3ea070382 100644 --- a/oob/osaka/precompiles/modexp/lead.lisp +++ b/oob/osaka/precompiles/modexp/lead.lisp @@ -10,14 +10,16 @@ (defun (prc-modexp-lead---standard-precondition) IS_MODEXP_LEAD) (defun (prc-modexp-lead---bbs) [DATA 1]) (defun (prc-modexp-lead---ebs) [DATA 3]) -(defun (prc-modexp-lead---load-lead) [DATA 4]) +(defun (prc-modexp-lead---extract-leading-word) [DATA 4]) (defun (prc-modexp-lead---cds-cutoff) [DATA 6]) (defun (prc-modexp-lead---ebs-cutoff) [DATA 7]) (defun (prc-modexp-lead---sub-ebs_32) [DATA 8]) (defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO) (defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO)) (defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2)) -(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3)) +(defun (prc-modexp-lead---result-of-comparison) (shift OUTGOING_RES_LO 3)) + +;; "" (defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) (call-to-ISZERO 0 0 (prc-modexp-lead---ebs))) @@ -37,12 +39,12 @@ 32))) (defconstraint prc-modexp-lead---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (begin (eq! (prc-modexp-lead---load-lead) + (begin (eq! (prc-modexp-lead---extract-leading-word) (* (prc-modexp-lead---call-data-contains-exponent-bytes) (- 1 (prc-modexp-lead---ebs-is-zero)))) (if-zero (prc-modexp-lead---call-data-contains-exponent-bytes) (vanishes! (prc-modexp-lead---cds-cutoff)) - (if-zero (prc-modexp-lead---comp) + (if-zero (prc-modexp-lead---result-of-comparison) (eq! (prc-modexp-lead---cds-cutoff) 32) (eq! (prc-modexp-lead---cds-cutoff) (- (prc---cds) (+ 96 (prc-modexp-lead---bbs)))))) diff --git a/oob/osaka/precompiles/modexp/pricing.lisp b/oob/osaka/precompiles/modexp/pricing.lisp index 6efc25567..5ab1da55d 100644 --- a/oob/osaka/precompiles/modexp/pricing.lisp +++ b/oob/osaka/precompiles/modexp/pricing.lisp @@ -7,47 +7,188 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING) + +(defconst + ROFF___MODEXP_PRICING___RAC_ISZERO_CHECK 0 + ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK 1 + ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 2 + ROFF___MODEXP_PRICING___MAX_VS_32 3 + ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST 4 + ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST 5 + ) + + +(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) IS_MODEXP_PRICING)) (defun (prc-modexp-pricing---exponent-log) [DATA 6]) -(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO)) -(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2))) -(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3)) -(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4)) -(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero) - (* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log)) - (prc-modexp-pricing---f-of-max))) -(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) - (prc-modexp-pricing---big-quotient) - GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 0 0 (prc---r@c))) - -(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log))) - -(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 2 - 0 - (+ (prc-modexp-pricing---max-xbs-ybs) 7) - 0 - 8)) - -(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR)) - -(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost))) - -(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (begin (eq! (prc---ram-success) - (- 1 (shift OUTGOING_RES_LO 5))) - (if-zero (prc---ram-success) - (vanishes! (prc---return-gas)) - (eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost)))) - (eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO)))) +(defun (prc-modexp-pricing---max-mbs-bbs) [DATA 7]) +;; "" + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 0: r@c.isZero() check ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint prc-modexp-pricing---r@c-iszero-check + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_PRICING___RAC_ISZERO_CHECK + 0 + (prc---r@c) + )) + +(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___RAC_ISZERO_CHECK)) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 1: exponentLog.isZero() check ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-pricing---check-exponent-log-is-zero + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK + 0 + (prc-modexp-pricing---exponent-log) + )) + +(defun (prc-modexp-pricing---exponent-log-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 2: ⌈ max(mbs, bbs) / 8 ⌉ compututation ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---computing-ceiling-of-max-mbs-bbs-over-8 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-DIV ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 + 0 + (+ (prc-modexp-pricing---max-mbs-bbs) 7) + 0 + 8 + )) + +(defun (prc-modexp-pricing---ceiling-of-max-over-8) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 3: comparing max(mbs, bbs) and 32 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-pricing---max-mbs-bbs-vs-32 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___MAX_VS_32 + 0 + WORD_SIZE + 0 + (prc-modexp-pricing---max-mbs-bbs) + )) + +(defun (prc-modexp-pricing---word-cost-dominates) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___MAX_VS_32)) +(defun (prc-modexp-pricing---f-of-max) (* (prc-modexp-pricing---ceiling-of-max-over-8) + (prc-modexp-pricing---ceiling-of-max-over-8))) +(defun (prc-modexp-pricing---multiplication-complexity) (if-zero (force-bin (prc-modexp-pricing---word-cost-dominates)) + 16 + (* 2 (prc-modexp-pricing---f-of-max)))) +(defun (prc-modexp-pricing---iteration-count-or-1) (if-zero (force-bin (prc-modexp-pricing---exponent-log-is-zero)) + (prc-modexp-pricing---exponent-log) + 1)) +(defun (prc-modexp-pricing---raw-cost) (* (prc-modexp-pricing---multiplication-complexity) + (prc-modexp-pricing---iteration-count-or-1))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 4: comparing raw_price to 500 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---compare-raw-cost-against-GAS_CONST_MODEXP-of-EIP-7823 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST + 0 + (prc-modexp-pricing---raw-cost) + 0 + GAS_CONST_MODEXP_EIP_7823 + )) + +(defun (prc-modexp-pricing---raw-cost-LT-min-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST))) +(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---raw-cost-LT-min-cost) + ;; raw_cost_LT_min_cost ≡ faux + (prc-modexp-pricing---raw-cost) + ;; raw_cost_LT_min_cost ≡ true + GAS_CONST_MODEXP_EIP_7823)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 5: comparing callee_gas to precopile_cost ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST + 0 + (prc---callee-gas) + 0 + (prc-modexp-pricing---precompile-cost) + )) + +(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; justifying HUB predictions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint prc-modexp-pricing---justify-hub-predictions---ram-success + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (prc---ram-success) + (- 1 (prc-modexp-pricing---callee-gas-LT-precompile-cost)) + )) + +(defconstraint prc-modexp-pricing---justify-hub-predictions---return-gas + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero (force-bin (prc---ram-success)) + ;; ram_success ≡ faux + (vanishes! (prc---return-gas)) + ;; ram_success ≡ true + (eq! (prc---return-gas) + (- (prc---callee-gas) + (prc-modexp-pricing---precompile-cost))) + )) + +(defconstraint prc-modexp-pricing---justify-hub-predictions---r@c-nonzero + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (prc---r@c-nonzero) + (- 1 (prc-modex-pricing---r@c-is-zero)) + )) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index fbaaf481a..a204106b7 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -7,35 +7,128 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) -(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) -(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) -(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) -(defun (prc-modexp-xbs---compute-max) [DATA 4]) -(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) -(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) - -(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 0 (prc-modexp-xbs---xbs-hi) (prc-modexp-xbs---xbs-lo) 0 513)) - -(defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) - -(defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) - -(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) - -(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (if-zero (prc-modexp-xbs---compute-max) - (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - (vanishes! (prc-modexp-xbs---xbs-nonzero))) - (begin (eq! (prc-modexp-xbs---xbs-nonzero) - (- 1 (shift OUTGOING_RES_LO 2))) - (if-zero (prc-modexp-xbs---comp) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo)) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo)))))) + +(defconst + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE (+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1) + + ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND 0 + ROFF___MODEXP_XBS___XBS_VS_YBS 1 + ROFF___MODEXP_XBS___XBS_ISZERO_CHECK 2 + ) + + +(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) +(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) +(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) +(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) +(defun (prc-modexp-xbs---compute-max) (force-bin [DATA 4])) +(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) +(defun (prc-modexp-xbs---xbs-nonzero) (force-bin [DATA 8])) +(defun (prc-modexp-xbs---xbs-within-bounds) (force-bin [DATA 9])) +(defun (prc-modexp-xbs---xbs-out-of-bounds) (force-bin [DATA 10])) +;; "" + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 0: comparing xbs against 1024 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---comparing-xbs-against-EIP-7823-upper-bound + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND + (prc-modexp-xbs---xbs-hi) + (prc-modexp-xbs---xbs-lo) + 0 + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE + )) + +(defun (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND )) +(defun (prc-modexp-xbs---xbs-is-GT-the-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 1: comparing xbs against ybs ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---comparing-xbs-against-ybs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_XBS___XBS_VS_YBS + 0 + (prc-modexp-xbs---xbs-lo) + 0 + (prc-modexp-xbs---ybs-lo) + )) + +(defun (prc-modexp-xbs---xbs-is-LT-ybs) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_YBS )) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 2: zeroness check for xbs ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---is-zero-check-for-xbs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK + 0 + (prc-modexp-xbs---xbs-lo) + )) + +(defun (prc-modexp-xbs---xbs-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK )) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; justifying HUB predictions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---binarity-sanity-check + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (is-binary (prc-modexp-xbs---compute-max))) + + +(defconstraint prc-modexp-xbs---justifying-hub-predictions---various-prediction-bits + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin (eq! (prc-modexp-xbs---xbs-nonzero) (- 1 (prc-modexp-xbs---xbs-is-zero)) ) + (eq! (prc-modexp-xbs---xbs-within-bounds) (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) ) + (eq! (prc-modexp-xbs---xbs-out-of-bounds) (prc-modexp-xbs---xbs-is-GT-the-EIP-7823-upper-bound) ) + )) + + +(defconstraint prc-modexp-xbs---justifying-hub-predictions---setting-the-value-of-max-xbs-ybs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero (prc-modexp-xbs---compute-max) + ;; comupte_max = false + (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + ;; comupte_max = false + (if-zero (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) + ;; false case + (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + ;; true case + (if-zero (prc-modexp-xbs---xbs-is-LT-ybs) + ;; false case + (eq! (prc-modexp-xbs---max-xbs-ybs) + (prc-modexp-xbs---xbs-lo)) + ;; true case + (eq! (prc-modexp-xbs---max-xbs-ybs) + (prc-modexp-xbs---ybs-lo)) + )))) diff --git a/oob/osaka/shorthands.lisp b/oob/osaka/shorthands.lisp index fe5b3d10f..7cf5b2551 100644 --- a/oob/osaka/shorthands.lisp +++ b/oob/osaka/shorthands.lisp @@ -18,7 +18,8 @@ IS_ECADD IS_ECMUL IS_ECPAIRING - (flag-sum-prc-bls))) + (flag-sum-prc-bls) + (flag-sum-osaka-precompile))) (defun (flag-sum-prc-blake) (+ IS_BLAKE2F_CDS IS_BLAKE2F_PARAMS)) @@ -29,9 +30,9 @@ IS_MODEXP_PRICING IS_MODEXP_EXTRACT)) -(defun (flag-sum-eip-blob-transactions) IS_POINT_EVALUATION) +(defun (flag-sum-cancun-precompiles) IS_POINT_EVALUATION) -(defun (flag-sum-eip-bls12-precompiles) (+ IS_BLS_G1_ADD +(defun (flag-sum-prague-precompiles) (+ IS_BLS_G1_ADD IS_BLS_G1_MSM IS_BLS_G2_ADD IS_BLS_G2_MSM @@ -39,8 +40,10 @@ IS_BLS_MAP_FP_TO_G1 IS_BLS_MAP_FP2_TO_G2)) -(defun (flag-sum-prc-bls) (+ (flag-sum-eip-blob-transactions) - (flag-sum-eip-bls12-precompiles))) +(defun (flag-sum-prc-bls) (+ (flag-sum-cancun-precompiles) + (flag-sum-prague-precompiles))) + +(defun (flag-sum-osaka-precompile) IS_P256_VERIFY) (defun (flag-sum-prc) (+ (flag-sum-prc-common) (flag-sum-prc-blake) @@ -67,7 +70,8 @@ (* OOB_INST_ECADD IS_ECADD) (* OOB_INST_ECMUL IS_ECMUL) (* OOB_INST_ECPAIRING IS_ECPAIRING) - (wght-sum-prc-bls))) + (wght-sum-prc-bls) + (wght-sum-prc-osaka-precompiles))) (defun (wght-sum-prc-blake) (+ (* OOB_INST_BLAKE_CDS IS_BLAKE2F_CDS) (* OOB_INST_BLAKE_PARAMS IS_BLAKE2F_PARAMS))) @@ -78,9 +82,9 @@ (* OOB_INST_MODEXP_PRICING IS_MODEXP_PRICING) (* OOB_INST_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) -(defun (wght-sum-prc-eip-blob-transactions) (+ (* OOB_INST_POINT_EVALUATION IS_POINT_EVALUATION))) +(defun (wght-sum-prc-cancun-precompiles) (+ (* OOB_INST_POINT_EVALUATION IS_POINT_EVALUATION))) -(defun (wght-sum-prc-eip-bls12-precompiles) (+ (* OOB_INST_BLS_G1_ADD IS_BLS_G1_ADD) +(defun (wght-sum-prc-prague-precompiles) (+ (* OOB_INST_BLS_G1_ADD IS_BLS_G1_ADD) (* OOB_INST_BLS_G1_MSM IS_BLS_G1_MSM) (* OOB_INST_BLS_G2_ADD IS_BLS_G2_ADD) (* OOB_INST_BLS_G2_MSM IS_BLS_G2_MSM) @@ -88,8 +92,10 @@ (* OOB_INST_BLS_MAP_FP_TO_G1 IS_BLS_MAP_FP_TO_G1) (* OOB_INST_BLS_MAP_FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2))) -(defun (wght-sum-prc-bls) (+ (wght-sum-prc-eip-blob-transactions) - (wght-sum-prc-eip-bls12-precompiles))) +(defun (wght-sum-prc-osaka-precompiles) (+ (* OOB_INST_P256_VERIFY IS_P256_VERIFY))) + +(defun (wght-sum-prc-bls) (+ (wght-sum-prc-cancun-precompiles) + (wght-sum-prc-prague-precompiles))) (defun (wght-sum-prc) (+ (wght-sum-prc-common) (wght-sum-prc-blake) @@ -98,7 +104,7 @@ (defun (wght-sum) (+ (wght-sum-inst) (wght-sum-prc))) -(defun (maxct-sum-inst) (+ (* CT_MAX_JUMP IS_JUMP) +(defun (ct-max-sum-inst) (+ (* CT_MAX_JUMP IS_JUMP) (* CT_MAX_JUMPI IS_JUMPI) (* CT_MAX_RDC IS_RDC) (* CT_MAX_CDL IS_CDL) @@ -109,27 +115,28 @@ (* CT_MAX_SSTORE IS_SSTORE) (* CT_MAX_DEPLOYMENT IS_DEPLOYMENT))) -(defun (maxct-sum-prc-common) (+ (* CT_MAX_ECRECOVER IS_ECRECOVER) +(defun (ct-max-sum-prc-common) (+ (* CT_MAX_ECRECOVER IS_ECRECOVER) (* CT_MAX_SHA2 IS_SHA2) (* CT_MAX_RIPEMD IS_RIPEMD) (* CT_MAX_IDENTITY IS_IDENTITY) (* CT_MAX_ECADD IS_ECADD) (* CT_MAX_ECMUL IS_ECMUL) (* CT_MAX_ECPAIRING IS_ECPAIRING) - (maxct-sum-prc-bls))) + (ct-max-sum-prc-bls) + (ct-max-sum-prc-osaka-precompiles))) -(defun (maxct-sum-prc-blake) (+ (* CT_MAX_BLAKE2F_CDS IS_BLAKE2F_CDS) +(defun (ct-max-sum-prc-blake) (+ (* CT_MAX_BLAKE2F_CDS IS_BLAKE2F_CDS) (* CT_MAX_BLAKE2F_PARAMS IS_BLAKE2F_PARAMS))) -(defun (maxct-sum-prc-modexp) (+ (* CT_MAX_MODEXP_CDS IS_MODEXP_CDS) +(defun (ct-max-sum-prc-modexp) (+ (* CT_MAX_MODEXP_CDS IS_MODEXP_CDS) (* CT_MAX_MODEXP_XBS IS_MODEXP_XBS) (* CT_MAX_MODEXP_LEAD IS_MODEXP_LEAD) (* CT_MAX_MODEXP_PRICING IS_MODEXP_PRICING) (* CT_MAX_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) -(defun (maxct-sum-prc-eip-blob-transactions)(+ (* CT_MAX_POINT_EVALUATION IS_POINT_EVALUATION))) +(defun (ct-max-sum-prc-cancun-precompiles)(+ (* CT_MAX_POINT_EVALUATION IS_POINT_EVALUATION))) -(defun (maxct-sum-prc-eip-bls12-precompiles)(+ (* CT_MAX_BLS_G1_ADD IS_BLS_G1_ADD) +(defun (ct-max-sum-prc-prague-precompiles)(+ (* CT_MAX_BLS_G1_ADD IS_BLS_G1_ADD) (* CT_MAX_BLS_G1_MSM IS_BLS_G1_MSM) (* CT_MAX_BLS_G2_ADD IS_BLS_G2_ADD) (* CT_MAX_BLS_G2_MSM IS_BLS_G2_MSM) @@ -137,15 +144,17 @@ (* CT_MAX_BLS_MAP_FP_TO_G1 IS_BLS_MAP_FP_TO_G1) (* CT_MAX_BLS_MAP_FP2_TO_G2 IS_BLS_MAP_FP2_TO_G2))) -(defun (maxct-sum-prc-bls) (+ (maxct-sum-prc-eip-blob-transactions) - (maxct-sum-prc-eip-bls12-precompiles))) +(defun (ct-max-sum-prc-osaka-precompiles) (* CT_MAX_P256_VERIFY IS_P256_VERIFY)) + +(defun (ct-max-sum-prc-bls) (+ (ct-max-sum-prc-cancun-precompiles) + (ct-max-sum-prc-prague-precompiles))) -(defun (maxct-sum-prc) (+ (maxct-sum-prc-common) - (maxct-sum-prc-blake) - (maxct-sum-prc-modexp))) +(defun (ct-max-sum-prc) (+ (ct-max-sum-prc-common) + (ct-max-sum-prc-blake) + (ct-max-sum-prc-modexp))) -(defun (maxct-sum) (+ (maxct-sum-inst) - (maxct-sum-prc))) +(defun (ct-max-sum) (+ (ct-max-sum-inst) + (ct-max-sum-prc))) (defun (lookup-sum k) (+ (shift ADD_FLAG k) (shift MOD_FLAG k) @@ -159,4 +168,3 @@ (defun (assumption---fresh-new-stamp) (- STAMP (prev STAMP))) -;; TODO: change maxct ot ct-max diff --git a/oob/prague/precompiles/modexp/xbs.lisp b/oob/prague/precompiles/modexp/xbs.lisp index fbaaf481a..fda951eca 100644 --- a/oob/prague/precompiles/modexp/xbs.lisp +++ b/oob/prague/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (defun (prc-modexp-xbs---compute-max) [DATA 4]) (defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) (defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO) (defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) (defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) @@ -28,7 +28,7 @@ (defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) + (eq! (prc-modexp-xbs---comparison-to-512) 1))) (defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (if-zero (prc-modexp-xbs---compute-max) diff --git a/oob/shanghai/precompiles/modexp/xbs.lisp b/oob/shanghai/precompiles/modexp/xbs.lisp index fbaaf481a..fda951eca 100644 --- a/oob/shanghai/precompiles/modexp/xbs.lisp +++ b/oob/shanghai/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (defun (prc-modexp-xbs---compute-max) [DATA 4]) (defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) (defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO) (defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) (defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) @@ -28,7 +28,7 @@ (defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) + (eq! (prc-modexp-xbs---comparison-to-512) 1))) (defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) (if-zero (prc-modexp-xbs---compute-max)