diff --git a/Makefile b/Makefile index 4996826e4..779629c93 100644 --- a/Makefile +++ b/Makefile @@ -25,9 +25,9 @@ BLS_CANCUN := blsdata/cancun BLS_PRAGUE := blsdata/prague CONSTANTS := constants/constants.lisp -CONSTANTS_LONDON := constants/london/constants.lisp -CONSTANTS_CANCUN := constants/cancun/constants.lisp -CONSTANTS_PRAGUE := constants/prague/constants.lisp +CONSTANTS_LONDON := constants/london/constants.zkasm +CONSTANTS_CANCUN := constants/cancun/constants.zkasm +CONSTANTS_PRAGUE := constants/prague/constants.zkasm EC_DATA := ecdata @@ -87,7 +87,7 @@ TABLES_LONDON := reftables/*.lisp reftables/london/*.lisp TABLES_CANCUN := reftables/*.lisp reftables/cancun/*.lisp TABLES_PRAGUE := reftables/*.lisp reftables/prague/*.lisp -TRM := trm +TRM := trm/trm.zkasm TXN_DATA_LONDON := txndata/london TXN_DATA_SHANGHAI := txndata/shanghai diff --git a/constants/cancun/constants.lisp b/constants/cancun/constants.lisp deleted file mode 100644 index 6948c190e..000000000 --- a/constants/cancun/constants.lisp +++ /dev/null @@ -1,8 +0,0 @@ - (defconst - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; PRECOMPILES ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - MAX_PRC_ADDRESS 0x0a - ) \ No newline at end of file diff --git a/constants/cancun/constants.zkasm b/constants/cancun/constants.zkasm new file mode 100644 index 000000000..ffbec505e --- /dev/null +++ b/constants/cancun/constants.zkasm @@ -0,0 +1 @@ +const MAX_PRC_ADDRESS = 0x0a \ No newline at end of file diff --git a/constants/london/constants.lisp b/constants/london/constants.lisp deleted file mode 100644 index a8361f3e4..000000000 --- a/constants/london/constants.lisp +++ /dev/null @@ -1,8 +0,0 @@ - (defconst - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; PRECOMPILES ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - MAX_PRC_ADDRESS 0x09 - ) \ No newline at end of file diff --git a/constants/london/constants.zkasm b/constants/london/constants.zkasm new file mode 100644 index 000000000..941dcc354 --- /dev/null +++ b/constants/london/constants.zkasm @@ -0,0 +1 @@ +const MAX_PRC_ADDRESS = 0x09 \ No newline at end of file diff --git a/constants/prague/constants.lisp b/constants/prague/constants.lisp deleted file mode 100644 index 8228a0678..000000000 --- a/constants/prague/constants.lisp +++ /dev/null @@ -1,8 +0,0 @@ - (defconst - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; PRECOMPILES ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - MAX_PRC_ADDRESS 0x11 - ) \ No newline at end of file diff --git a/constants/prague/constants.zkasm b/constants/prague/constants.zkasm new file mode 100644 index 000000000..a71365a32 --- /dev/null +++ b/constants/prague/constants.zkasm @@ -0,0 +1 @@ +const MAX_PRC_ADDRESS = 0x11 diff --git a/hub/cancun/lookups/hub_into_trm.lisp b/hub/cancun/lookups/hub_into_trm.lisp index 3a21730c6..abc1470ef 100644 --- a/hub/cancun/lookups/hub_into_trm.lisp +++ b/hub/cancun/lookups/hub_into_trm.lisp @@ -5,18 +5,16 @@ (defclookup hub-into-trm ;; target columns ( - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI trm.IS_PRECOMPILE ) ;; source selector (hub-into-trm-trigger) ;; source columns ( + (:: hub.account/TRM_RAW_ADDRESS_HI hub.account/ADDRESS_LO) hub.account/ADDRESS_HI - hub.account/TRM_RAW_ADDRESS_HI - hub.account/ADDRESS_LO hub.account/IS_PRECOMPILE ) ) diff --git a/hub/london/lookups/hub_into_trm.lisp b/hub/london/lookups/hub_into_trm.lisp index 3a21730c6..abc1470ef 100644 --- a/hub/london/lookups/hub_into_trm.lisp +++ b/hub/london/lookups/hub_into_trm.lisp @@ -5,18 +5,16 @@ (defclookup hub-into-trm ;; target columns ( - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI trm.IS_PRECOMPILE ) ;; source selector (hub-into-trm-trigger) ;; source columns ( + (:: hub.account/TRM_RAW_ADDRESS_HI hub.account/ADDRESS_LO) hub.account/ADDRESS_HI - hub.account/TRM_RAW_ADDRESS_HI - hub.account/ADDRESS_LO hub.account/IS_PRECOMPILE ) ) diff --git a/hub/prague/lookups/hub_into_trm.lisp b/hub/prague/lookups/hub_into_trm.lisp index 3a21730c6..abc1470ef 100644 --- a/hub/prague/lookups/hub_into_trm.lisp +++ b/hub/prague/lookups/hub_into_trm.lisp @@ -5,18 +5,16 @@ (defclookup hub-into-trm ;; target columns ( - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI trm.IS_PRECOMPILE ) ;; source selector (hub-into-trm-trigger) ;; source columns ( + (:: hub.account/TRM_RAW_ADDRESS_HI hub.account/ADDRESS_LO) hub.account/ADDRESS_HI - hub.account/TRM_RAW_ADDRESS_HI - hub.account/ADDRESS_LO hub.account/IS_PRECOMPILE ) ) diff --git a/hub/shanghai/lookups/hub_into_trm.lisp b/hub/shanghai/lookups/hub_into_trm.lisp index 3a21730c6..abc1470ef 100644 --- a/hub/shanghai/lookups/hub_into_trm.lisp +++ b/hub/shanghai/lookups/hub_into_trm.lisp @@ -5,18 +5,16 @@ (defclookup hub-into-trm ;; target columns ( - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI trm.IS_PRECOMPILE ) ;; source selector (hub-into-trm-trigger) ;; source columns ( + (:: hub.account/TRM_RAW_ADDRESS_HI hub.account/ADDRESS_LO) hub.account/ADDRESS_HI - hub.account/TRM_RAW_ADDRESS_HI - hub.account/ADDRESS_LO hub.account/IS_PRECOMPILE ) ) diff --git a/rlpaddr/lookups/rlpaddr_into_trm.lisp b/rlpaddr/lookups/rlpaddr_into_trm.lisp index a8ef71c5b..46c5000d4 100644 --- a/rlpaddr/lookups/rlpaddr_into_trm.lisp +++ b/rlpaddr/lookups/rlpaddr_into_trm.lisp @@ -2,15 +2,13 @@ rlpaddr-into-trm ;reference columns ( - trm.RAW_ADDRESS_HI - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI ) ;source columns ( - rlpaddr.RAW_ADDR_HI + (:: rlpaddr.RAW_ADDR_HI rlpaddr.DEP_ADDR_LO) rlpaddr.DEP_ADDR_HI - rlpaddr.DEP_ADDR_LO )) diff --git a/rlptxn/cancun/lookups/rlptxn_into_trm.lisp b/rlptxn/cancun/lookups/rlptxn_into_trm.lisp index 6217c1bd2..5f1747518 100644 --- a/rlptxn/cancun/lookups/rlptxn_into_trm.lisp +++ b/rlptxn/cancun/lookups/rlptxn_into_trm.lisp @@ -4,15 +4,13 @@ (rlptxn-into-trm :unchecked) ;; target columns ( - trm.IOMF - trm.TRM_ADDRESS_HI - trm.RAW_ADDRESS_LO + trm.RAW_ADDRESS + trm.ADDRESS_HI ) ;; source selector (sel-rlptxn-to-trm) ;; source columns ( - 1 - rlptxn.cmp/EXO_DATA_1 - rlptxn.cmp/EXO_DATA_2 + (:: rlptxn.cmp/EXO_DATA_1 rlptxn.cmp/EXO_DATA_2) + rlptxn.cmp/EXO_DATA_1 )) diff --git a/trm/columns.lisp b/trm/columns.lisp deleted file mode 100644 index 3ce92e328..000000000 --- a/trm/columns.lisp +++ /dev/null @@ -1,17 +0,0 @@ -(module trm) - -(defcolumns - (IOMF :binary@prove) - (FIRST :binary) - (RAW_ADDRESS_HI :i128) - (RAW_ADDRESS_LO :i128) - (TRM_ADDRESS_HI :i32) - (IS_PRECOMPILE :binary) - (CT :i4) - (ARG_1_HI :i128) - (ARG_1_LO :i128) - (ARG_2_HI :i128) - (ARG_2_LO :i128) - (RES :binary) - (INST :byte :display :opcode) -) diff --git a/trm/constants.lisp b/trm/constants.lisp deleted file mode 100644 index 7f0b0633a..000000000 --- a/trm/constants.lisp +++ /dev/null @@ -1,10 +0,0 @@ -(module trm) - -(defconst -TRM_CT_MAX 3 -TRM_NB_ROWS (+ TRM_CT_MAX 1) -ROW_OFFSET_ADDRESS 0 -ROW_OFFSET_ADDRESS_TRM 1 -ROW_OFFSET_NON_ZERO_ADDR 2 -ROW_OFFSET_PRC_ADDR 3 -) \ No newline at end of file diff --git a/trm/constraints.lisp b/trm/constraints.lisp deleted file mode 100644 index 8958856b9..000000000 --- a/trm/constraints.lisp +++ /dev/null @@ -1,136 +0,0 @@ -(module trm) - -;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.1 heartbeat ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;; -;; 1 -(defconstraint first-row (:domain {0}) ;; "" - (vanishes! IOMF)) - -(defconstraint iomf-increment () - (or! (will-remain-constant! IOMF) (will-inc! IOMF 1))) - -;; 3 -(defconstraint automatic-vanishing-constraints-along-padding-rows () - (if-zero IOMF - (begin (vanishes! RAW_ADDRESS_HI) - (vanishes! RAW_ADDRESS_LO) - (vanishes! TRM_ADDRESS_HI) - (vanishes! IS_PRECOMPILE) - (vanishes! (next CT)) - (debug (vanishes! CT))))) - -(defconstraint constraining-FIRST (:guard IOMF) - (begin - (if-zero CT (eq! FIRST 1)) - (debug (if-not-zero CT (eq! FIRST 0))))) - -(defconstraint counter-cycle-constraints (:guard IOMF) - (if-zero (- TRM_CT_MAX CT) - ;; CT = CT MAX - (vanishes! (next CT)) - ;; CT != CT MAX - (will-inc! CT 1))) - -(defconstraint finalization-constraint (:domain {-1} :guard IOMF) ;;"" - (eq! CT TRM_CT_MAX)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.2 counter constancies ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconstraint counter-constancies () - (begin (counter-constancy CT RAW_ADDRESS_HI) - (counter-constancy CT RAW_ADDRESS_LO) - (counter-constancy CT TRM_ADDRESS_HI) - (counter-constancy CT IS_PRECOMPILE) - )) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.4 computations ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (wcpcall offset - inst - arg1hi - arg1lo - arg2hi - arg2lo) - (begin (eq! (shift INST offset) inst) - (eq! (shift ARG_1_HI offset) arg1hi) - (eq! (shift ARG_1_LO offset) arg1lo) - (eq! (shift ARG_2_HI offset) arg2hi) - (eq! (shift ARG_2_LO offset) arg2lo))) - -(defun (result-is-true offset) - (eq! (shift RES offset) 1)) - -;; -;; Processing row n°0 -;; -(defconstraint trimmed-address-is-20-bytes-integer (:guard FIRST) - (begin - (wcpcall ROW_OFFSET_ADDRESS - EVM_INST_LT - TRM_ADDRESS_HI - RAW_ADDRESS_LO - TWOFIFTYSIX_TO_THE_FOUR - 0) - (result-is-true ROW_OFFSET_ADDRESS))) - -;; -;; Processing row n°1 -;; -(defconstraint leading-bytes-is-twelve-bytes (:guard FIRST) - (begin - (eq! (shift INST ROW_OFFSET_ADDRESS_TRM) WCP_INST_LEQ) - (vanishes! (shift ARG_1_HI ROW_OFFSET_ADDRESS_TRM)) -;; (shift ARG_1_LO ROW_OFFSET_ADDRESS_TRM) ;; it is what it ... later on: (leading-bytes) - (vanishes! (shift ARG_2_HI ROW_OFFSET_ADDRESS_TRM)) - (eq! (shift ARG_2_LO ROW_OFFSET_ADDRESS_TRM) TWOFIFTYSIX_TO_THE_TWELVE_MO) - (result-is-true ROW_OFFSET_ADDRESS_TRM))) - -(defun (leading-bytes) (shift ARG_1_LO ROW_OFFSET_ADDRESS_TRM)) - -(defconstraint address-decomposition-constraint (:guard FIRST) - (eq! RAW_ADDRESS_HI - (+ (* TWOFIFTYSIX_TO_THE_FOUR (leading-bytes)) - TRM_ADDRESS_HI))) - -;; -;; Processing row n°2 -;; -(defconstraint iszero-check-for-address (:guard FIRST) - (begin - (eq! (shift INST ROW_OFFSET_NON_ZERO_ADDR) EVM_INST_ISZERO) - (eq! (shift ARG_1_HI ROW_OFFSET_NON_ZERO_ADDR) TRM_ADDRESS_HI) - (eq! (shift ARG_1_LO ROW_OFFSET_NON_ZERO_ADDR) RAW_ADDRESS_LO) - )) - -(defun (address-is-zero) (shift RES ROW_OFFSET_NON_ZERO_ADDR)) -(defun (address-is-nonzero) (- 1 (address-is-zero))) - -;; -;; Processing row n°3 -;; -(defconstraint address-is-prc-range (:guard FIRST) - (wcpcall ROW_OFFSET_PRC_ADDR - WCP_INST_LEQ - TRM_ADDRESS_HI - RAW_ADDRESS_LO - 0 - MAX_PRC_ADDRESS)) - -(defun (address-at-most-max-PRC) (shift RES ROW_OFFSET_PRC_ADDR)) - -(defconstraint justifying-the-precompile-flag (:guard FIRST) - (eq! IS_PRECOMPILE - (* (address-is-nonzero) - (address-at-most-max-PRC)))) diff --git a/trm/lookups/trm_into_wcp.lisp b/trm/lookups/trm_into_wcp.lisp deleted file mode 100644 index 2f867dd1f..000000000 --- a/trm/lookups/trm_into_wcp.lisp +++ /dev/null @@ -1,20 +0,0 @@ -(deflookup - trm-into-wcp - ; target columns - ( - wcp.ARGUMENT_1_HI - wcp.ARGUMENT_1_LO - wcp.ARGUMENT_2_HI - wcp.ARGUMENT_2_LO - wcp.RESULT - wcp.INST - ) - ; source columns - ( - trm.ARG_1_HI - trm.ARG_1_LO - trm.ARG_2_HI - trm.ARG_2_LO - trm.RES - trm.INST - )) \ No newline at end of file diff --git a/trm/trm.zkasm b/trm/trm.zkasm new file mode 100644 index 000000000..c69badee8 --- /dev/null +++ b/trm/trm.zkasm @@ -0,0 +1,39 @@ +;; The address trimming module does two things: (i) reduce 256bit +;; addresses into u160 addresses (i.e. modulo 2^160); (b) identify +;; addresses of precompiles. +;; +;; The need for this function arises as some EVM opcodes take an u256 +;; stack argument requires trimming to be interpreted as an address. +;; Likewise, when computing a deployment address associated with an +;; invocation of a CREATE-type, the raw KECCAK hash must be trimmed. +;; +;; The following opcodes may trigger it: +;; +;; * BALANCE +;; * EXTCODESIZE / EXTCODECOPY / EXTCODEHASH +;; * CALL / CALLCODE / STATICCALL +;; * SELFDESTRUCT +;; * DELEGATECALL +;; +;; NOTE: the function currently only returns the high word of the +;; trimmed address, since the low word is unchanged. +pub fn trm(RAW_ADDRESS u256) -> (ADDRESS_HI u32, IS_PRECOMPILE u1) { + var low, tmp u128 + var high u96 + var b u1 + ;; trim off most significant 96 bytes + high,ADDRESS_HI,low = RAW_ADDRESS + ;; if hi word not zero, cannot be precompile. + if ADDRESS_HI != 0 goto exit_0 + ;; discount address 0 + if low == 0 goto exit_0 + ;; determine low <= MAX_PRC_ADDRESS + b,tmp = low - MAX_PRC_ADDRESS - 1 + ;; done + IS_PRECOMPILE=b + return +exit_0: + ;; no, not precompile + IS_PRECOMPILE=0 + return +}