diff --git a/Makefile b/Makefile index ffd22ef6f..36a45e54f 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..bf708f655 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 @@ -270,6 +271,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 ;; 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/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/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/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/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)