From 05aa1c6bef87ef2387e079f726809eab6a3c5659 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Fri, 10 Jan 2025 14:22:10 +0100 Subject: [PATCH] Implementation of TX_INIT and TX_FINL fix (#517) --- Makefile | 4 +- blockdata/columns.lisp | 10 +- constants/constants.lisp | 2 +- hub/columns/stack.lisp | 2 +- hub/constants.lisp | 7 +- .../generalities/revert_data_specific.lisp | 9 +- hub/constraints/heartbeat/hub_stamp.lisp | 10 +- .../heartbeat/transaction_phase_flags.lisp | 2 +- hub/constraints/instruction-handling/sto.lisp | 105 +++++--- .../{constraints.lisp => constraints.lispX} | 0 hub/constraints/tx_finl/peeking.lisp | 17 ++ .../tx_finl/rows/acc_coinbase_reward.lisp | 28 +++ .../tx_finl/rows/acc_sender_gas_refund.lisp | 25 ++ hub/constraints/tx_finl/rows/transaction.lisp | 17 ++ hub/constraints/tx_finl/shorthands.lisp | 34 +++ hub/constraints/tx_init/constraints.lisp | 231 ------------------ hub/constraints/tx_init/peeking.lisp | 57 +++++ .../rows/acc_recipient_value_transfer.lisp | 77 ++++++ .../tx_init/rows/acc_sender_gas_payment.lisp | 35 +++ .../rows/acc_sender_value_transfer.lisp | 25 ++ .../acc_undo_recipient_value_reception.lisp | 25 ++ .../rows/acc_undo_sender_value_transfer.lisp | 28 +++ .../tx_init/rows/con_initialization.lisp | 50 ++++ .../rows/first_execution_row_parameters.lisp | 31 +++ .../tx_init/rows/miscellaneous.lisp | 37 +++ hub/constraints/tx_init/rows/transaction.lisp | 37 +++ hub/constraints/tx_init/shorthands.lisp | 46 ++++ 27 files changed, 670 insertions(+), 281 deletions(-) rename hub/constraints/tx_finl/{constraints.lisp => constraints.lispX} (100%) create mode 100644 hub/constraints/tx_finl/peeking.lisp create mode 100644 hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp create mode 100644 hub/constraints/tx_finl/rows/acc_sender_gas_refund.lisp create mode 100644 hub/constraints/tx_finl/rows/transaction.lisp create mode 100644 hub/constraints/tx_finl/shorthands.lisp delete mode 100644 hub/constraints/tx_init/constraints.lisp create mode 100644 hub/constraints/tx_init/peeking.lisp create mode 100644 hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp create mode 100644 hub/constraints/tx_init/rows/acc_sender_gas_payment.lisp create mode 100644 hub/constraints/tx_init/rows/acc_sender_value_transfer.lisp create mode 100644 hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp create mode 100644 hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp create mode 100644 hub/constraints/tx_init/rows/con_initialization.lisp create mode 100644 hub/constraints/tx_init/rows/first_execution_row_parameters.lisp create mode 100644 hub/constraints/tx_init/rows/miscellaneous.lisp create mode 100644 hub/constraints/tx_init/rows/transaction.lisp create mode 100644 hub/constraints/tx_init/shorthands.lisp diff --git a/Makefile b/Makefile index 7e02ac4b..2dcfa87f 100644 --- a/Makefile +++ b/Makefile @@ -28,7 +28,9 @@ HUB := $(wildcard hub/columns/*lisp) \ $(wildcard hub/constraints/tx_skip/*lisp) \ $(wildcard hub/constraints/tx_prewarm/*lisp) \ $(wildcard hub/constraints/tx_init/*lisp) \ + $(wildcard hub/constraints/tx_init/rows/*lisp) \ $(wildcard hub/constraints/tx_finl/*lisp) \ + $(wildcard hub/constraints/tx_finl/rows/*lisp) \ $(wildcard hub/constraints/*lisp) \ $(wildcard hub/lookups/*lisp) \ hub/constants.lisp @@ -142,7 +144,7 @@ ZKEVM_MODULES := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB_COLUMNS} \ + ${HUB} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ diff --git a/blockdata/columns.lisp b/blockdata/columns.lisp index 16667362..71e38a5b 100644 --- a/blockdata/columns.lisp +++ b/blockdata/columns.lisp @@ -14,11 +14,11 @@ (INST :byte :display :opcode) (COINBASE_HI :i32) (COINBASE_LO :i128) - (BLOCK_GAS_LIMIT :i48) - (BASEFEE :i48) + (BLOCK_GAS_LIMIT :i64) + (BASEFEE :i64) (FIRST_BLOCK_NUMBER :i48) - (REL_BLOCK :i8) - (REL_TX_NUM_MAX :i10) + (REL_BLOCK :i16) + (REL_TX_NUM_MAX :i16) (DATA_HI :i128) (DATA_LO :i128) (ARG_1_HI :i128) @@ -26,7 +26,7 @@ (ARG_2_HI :i128) (ARG_2_LO :i128) (RES :i128) - (EXO_INST :byte) + (EXO_INST :byte :display :opcode) (WCP_FLAG :binary@prove) (EUC_FLAG :binary@prove) ) diff --git a/constants/constants.lisp b/constants/constants.lisp index b723db7d..2150549f 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -222,7 +222,7 @@ LINEA_DIFFICULTY 2 LINEA_MAX_NUMBER_OF_TRANSACTIONS_IN_BATCH 200 ETHEREUM_GAS_LIMIT_MINIMUM 5000 - ETHEREUM_GAS_LIMIT_MAXIMUM 0xffffffffffffffffffffffffffffffff ;; maxUint64 + ETHEREUM_GAS_LIMIT_MAXIMUM 0xffffffffffffffff ;; maxUint64 LINEA_GAS_LIMIT_MINIMUM 61000000 LINEA_GAS_LIMIT_MAXIMUM 2000000000 GAS_LIMIT_ADJUSTMENT_FACTOR 1024 diff --git a/hub/columns/stack.lisp b/hub/columns/stack.lisp index 36a430f7..66034a0d 100644 --- a/hub/columns/stack.lisp +++ b/hub/columns/stack.lisp @@ -12,7 +12,7 @@ ( STACK_ITEM_STAMP :array [4] :i36) ;; STAMP is :i32 and we consider 8 * STAMP + bla with 0 ≤ bla < 8 ;; instruction and instruction decoded flags - ( INSTRUCTION :display :opcode) + ( INSTRUCTION :byte :display :opcode) ( STATIC_GAS :i32 ) ;; TODO: vastly exagerated, shouldn't carry values greater than 32_000 so :i16 should suffice) ( ACC_FLAG :binary ) ( ADD_FLAG :binary ) diff --git a/hub/constants.lisp b/hub/constants.lisp index abde5ff9..8e9322a3 100644 --- a/hub/constants.lisp +++ b/hub/constants.lisp @@ -2,7 +2,8 @@ (defconst MULTIPLIER___STACK_STAMP 8 ;; \hubTau - MULTIPLIER___DOM_SUB_STAMPS 8 ;; \hubLambda - DOM_SUB_STAMP_OFFSET___REVERT 6 ;; \revertEpsilon - DOM_SUB_STAMP_OFFSET___SELFDESTRUCT 7 ;; \selfdestructEpsilon + MULTIPLIER___DOM_SUB_STAMPS 16 ;; \hubLambda + DOM_SUB_STAMP_OFFSET___REVERT 8 ;; \revertEpsilon + DOM_SUB_STAMP_OFFSET___FINALIZATION 9 ;; \finalizationEpsilon + DOM_SUB_STAMP_OFFSET___SELFDESTRUCT 10 ;; \selfdestructEpsilon ) diff --git a/hub/constraints/generalities/revert_data_specific.lisp b/hub/constraints/generalities/revert_data_specific.lisp index 0f1c7100..0ec58c59 100644 --- a/hub/constraints/generalities/revert_data_specific.lisp +++ b/hub/constraints/generalities/revert_data_specific.lisp @@ -39,7 +39,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (self_revert_trigger) (- (+ XAHOY (* stack/HALT_FLAG [stack/DEC_FLAG 2])) - (* XAHOY stack/HALT_FLAG [stack/DEC_FLAG 2]))) + (* XAHOY stack/HALT_FLAG [stack/DEC_FLAG 2]))) ;; "" (defconstraint recording-self-induced-revert (:perspective stack) (if-not-zero (force-bool (self_revert_trigger)) @@ -112,6 +112,13 @@ sub_stamp_offset )) +;; (defun (DOM-SUB-stamps---finalization rel_offset +;; sub_offset) +;; (undoing-dom-sub-stamps rel_offset +;; TX_END_STAMP +;; DOM_SUB_STAMP_OFFSET___FINALIZATION +;; sub_offset)) + (defun (selfdestruct-dom-sub-stamps relOffset) (undoing-dom-sub-stamps relOffset TX_END_STAMP diff --git a/hub/constraints/heartbeat/hub_stamp.lisp b/hub/constraints/heartbeat/hub_stamp.lisp index f428ae0b..39e95674 100644 --- a/hub/constraints/heartbeat/hub_stamp.lisp +++ b/hub/constraints/heartbeat/hub_stamp.lisp @@ -25,7 +25,15 @@ (will-inc! HUB_STAMP 1)))) (defconstraint heartbeat---hub-stamp---constancy-during-skipping-phase () - (if-not-zero (+ TX_SKIP TX_INIT TX_FINL) + (if-not-zero TX_SKIP + (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION)))) + +(defconstraint heartbeat---hub-stamp---constancy-during-initialization-phase () + (if-not-zero TX_INIT + (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_CONTEXT)))) + +(defconstraint heartbeat---hub-stamp---constancy-during-finalization-phase () + (if-not-zero TX_FINL (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION)))) (defconstraint heartbeat---hub-stamp---jumps-at-transaction-boundaries () diff --git a/hub/constraints/heartbeat/transaction_phase_flags.lisp b/hub/constraints/heartbeat/transaction_phase_flags.lisp index 6da5eab2..a9f4a2c0 100644 --- a/hub/constraints/heartbeat/transaction_phase_flags.lisp +++ b/hub/constraints/heartbeat/transaction_phase_flags.lisp @@ -47,7 +47,7 @@ (if-not-zero TX_WARM (eq! (next (+ TX_WARM TX_INIT)) 1)) (if-not-zero TX_INIT - (if-zero PEEK_AT_TRANSACTION + (if-zero PEEK_AT_CONTEXT (eq! (next TX_INIT) 1) (eq! (next TX_EXEC) 1))) (if-not-zero TX_EXEC diff --git a/hub/constraints/instruction-handling/sto.lisp b/hub/constraints/instruction-handling/sto.lisp index 3918e8a1..17ff8981 100644 --- a/hub/constraints/instruction-handling/sto.lisp +++ b/hub/constraints/instruction-handling/sto.lisp @@ -11,10 +11,14 @@ (defun (storage-instruction---value-to-store-lo) [ stack/STACK_ITEM_VALUE_LO 4 ]) (defun (storage-instruction---OOB-prediction-of-sstorex) (shift [ misc/OOB_DATA 7 ] 2)) ;; "" -(defconstraint storage-instruction---stack-pattern (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---stack-pattern + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (load-store-stack-pattern (storage-instruction---is-SSTORE))) -(defconstraint storage-instruction---valid-exceptions (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---valid-exceptions + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin (if-not-zero (storage-instruction---is-SLOAD) (eq! XAHOY stack/OOGX)) @@ -24,7 +28,9 @@ stack/SSTOREX stack/OOGX))))) -(defconstraint storage-instruction---setting-NSR-and-peeking-flags-STATICX (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-NSR-and-peeking-flags-STATICX + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; static exception ;;;;;;;;;;;;;;;;;;; (if-not-zero stack/STATICX @@ -34,7 +40,9 @@ (+ (shift PEEK_AT_CONTEXT 1) (shift PEEK_AT_CONTEXT 2)))))) -(defconstraint storage-instruction---setting-NSR-and-peeking-flags-SSTOREX (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-NSR-and-peeking-flags-SSTOREX + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; sstore gas exception ;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero stack/SSTOREX @@ -45,7 +53,9 @@ (shift PEEK_AT_MISCELLANEOUS 2) (shift PEEK_AT_CONTEXT 3)))))) -(defconstraint storage-instruction---setting-NSR-and-peeking-flags-OOGX (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-NSR-and-peeking-flags-OOGX + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; out of gas exception ;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero stack/OOGX @@ -58,7 +68,9 @@ (shift PEEK_AT_STORAGE 4) (shift PEEK_AT_CONTEXT 5)))))) -(defconstraint storage-instruction---setting-NSR-and-peeking-flags-UNEXCEPTIONAL (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-NSR-and-peeking-flags-UNEXCEPTIONAL + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; unexceptional ;;;;;;;;;;;;;;;; (if-zero XAHOY @@ -70,16 +82,22 @@ (shift PEEK_AT_STORAGE 3) (* CONTEXT_WILL_REVERT (shift PEEK_AT_STORAGE 4))))))) -(defconstraint storage-instruction---first-context-row (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---first-context-row + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (read-context-data 1 ;; row offset CONTEXT_NUMBER )) ;; context to read -(defconstraint storage-instruction---justifying-STATICX (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---justifying-STATICX + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! stack/STATICX (* (storage-instruction---is-SSTORE) (shift context/IS_STATIC 1)))) -(defconstraint storage-instruction---setting-MISC-row (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-MISC-row + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift PEEK_AT_MISCELLANEOUS 2) (begin (eq! (weighted-MISC-flag-sum 2) @@ -89,15 +107,20 @@ GAS_ACTUAL )) ;; GAS_ACTUAL ))) -(defconstraint storage-instruction---justifying-SSTOREX (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---justifying-SSTOREX + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift PEEK_AT_MISCELLANEOUS 2) (if-not-zero (storage-instruction---is-SSTORE) (eq! stack/SSTOREX (storage-instruction---OOB-prediction-of-sstorex))))) -(defun (oogx-or-no-exception) (+ stack/OOGX (- 1 XAHOY))) +(defun (no-exception) (- 1 XAHOY)) +(defun (oogx-or-no-exception) (+ stack/OOGX (no-exception))) -(defconstraint storage-instruction---setting-storage-slot-parameters (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-storage-slot-parameters + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (oogx-or-no-exception) (begin (eq! (shift storage/ADDRESS_HI 3) (shift context/ACCOUNT_ADDRESS_HI 1)) @@ -109,29 +132,37 @@ (DOM-SUB-stamps---standard 3 ;; kappa 0)))) ;; c -(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SLOAD (:guard (storage-instruction---no-stack-exceptions)) - (if-not-zero (oogx-or-no-exception) - (if-not-zero (force-bin (storage-instruction---is-SLOAD)) - (begin - (storage-reading 3) - (eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3)) - (eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3)))))) - -(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SSTORE (:guard (storage-instruction---no-stack-exceptions)) - (if-not-zero (oogx-or-no-exception) - (if-not-zero (force-bin (storage-instruction---is-SSTORE)) - (begin - (eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3)) - (eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3)))))) +(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SLOAD + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (storage-instruction---is-SLOAD) + (begin + (if-not-zero (oogx-or-no-exception) + (storage-reading 3)) + (if-not-zero (no-exception) + (begin + (eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3)) + (eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3))))))) + +(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SSTORE + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (storage-instruction---is-SSTORE) + (if-not-zero (oogx-or-no-exception) + (begin + (eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3)) + (eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3)))))) -(defconstraint storage-instruction---setting-storage-slot-values---undoing-storage-operation (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-storage-slot-values---undoing-storage-operation + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (oogx-or-no-exception) - (if-not-zero CONTEXT_WILL_REVERT - (begin - (storage-same-slot 4) - (undo-storage-warmth-and-value-update 4) - (DOM-SUB-stamps---revert-with-current 4 ;; kappa - 0))))) ;; c + (if-not-zero CONTEXT_WILL_REVERT + (begin + (storage-same-slot 4) + (undo-storage-warmth-and-value-update 4) + (DOM-SUB-stamps---revert-with-current 4 ;; kappa + 0))))) ;; c (defun (orig-is-zero) (shift storage/VALUE_ORIG_IS_ZERO 3)) (defun (curr-is-zero) (shift storage/VALUE_CURR_IS_ZERO 3)) @@ -190,10 +221,12 @@ (defun (r-dirty-reset) (* (next-not-curr) (curr-not-orig) (next-is-orig) - (+ (* (orig-is-zero) (- GAS_CONST_G_SSET GAS_CONST_G_WARM_ACCESS)) - (* (orig-not-zero) (- GAS_CONST_G_WARM_ACCESS GAS_CONST_G_SRESET))))) + (+ (* (orig-is-zero) (- GAS_CONST_G_SSET GAS_CONST_G_WARM_ACCESS)) + (* (orig-not-zero) (- GAS_CONST_G_SRESET GAS_CONST_G_WARM_ACCESS))))) -(defconstraint storage-instruction---setting-the-refund (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-the-refund + (:guard (storage-instruction---no-stack-exceptions)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! REFUND_COUNTER_NEW (+ REFUND_COUNTER diff --git a/hub/constraints/tx_finl/constraints.lisp b/hub/constraints/tx_finl/constraints.lispX similarity index 100% rename from hub/constraints/tx_finl/constraints.lisp rename to hub/constraints/tx_finl/constraints.lispX diff --git a/hub/constraints/tx_finl/peeking.lisp b/hub/constraints/tx_finl/peeking.lisp new file mode 100644 index 00000000..7f6d0b15 --- /dev/null +++ b/hub/constraints/tx_finl/peeking.lisp @@ -0,0 +1,17 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_FINL phase ;; +;; X.Y Introduction ;; +;; X.Y Setting the peeking flags ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-finl---setting-peeking-flags + (:guard (tx-finl---standard-precondition)) + (eq! 3 + (+ (shift PEEK_AT_ACCOUNT tx-finl---row-offset---ACC---sender-gas-refund) + (shift PEEK_AT_ACCOUNT tx-finl---row-offset---ACC---coinbase-reward) + (shift PEEK_AT_TRANSACTION tx-finl---row-offset---TXN)))) diff --git a/hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp b/hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp new file mode 100644 index 00000000..d43309d1 --- /dev/null +++ b/hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp @@ -0,0 +1,28 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_FINL phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Coinbase reward ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-finl---account-row---coinbase-reward + (:guard (tx-finl---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (account-trim-address tx-finl---row-offset---ACC---coinbase-reward ;; row offset + (tx-finl---coinbase-address-hi) ;; high part of raw, potentially untrimmed address + (tx-finl---coinbase-address-lo)) ;; low part of raw, potentially untrimmed address + ;; (eq! (shift account/ADDRESS_HI tx-finl---row-offset---ACC---coinbase-reward) (tx-finl---coinbase-address-hi)) + ;; (eq! (shift account/ADDRESS_LO tx-finl---row-offset---ACC---coinbase-reward) (tx-finl---coinbase-address-lo)) + (account-increment-balance-by tx-finl---row-offset---ACC---coinbase-reward (tx-finl---coinbase-reward)) + (account-same-nonce tx-finl---row-offset---ACC---coinbase-reward) + (account-same-code tx-finl---row-offset---ACC---coinbase-reward) + (account-same-deployment-number-and-status tx-finl---row-offset---ACC---coinbase-reward) + (account-same-warmth tx-finl---row-offset---ACC---coinbase-reward) + (account-same-marked-for-selfdestruct tx-finl---row-offset---ACC---coinbase-reward) + (DOM-SUB-stamps---standard tx-finl---row-offset---ACC---coinbase-reward + 1))) diff --git a/hub/constraints/tx_finl/rows/acc_sender_gas_refund.lisp b/hub/constraints/tx_finl/rows/acc_sender_gas_refund.lisp new file mode 100644 index 00000000..778aad73 --- /dev/null +++ b/hub/constraints/tx_finl/rows/acc_sender_gas_refund.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_FINL phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Sender gas refund ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-finl---account-row---sender-gas-refund + (:guard (tx-finl---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (shift account/ADDRESS_HI tx-finl---row-offset---ACC---sender-gas-refund) (tx-finl---sender-address-hi)) + (eq! (shift account/ADDRESS_LO tx-finl---row-offset---ACC---sender-gas-refund) (tx-finl---sender-address-lo)) + (account-increment-balance-by tx-finl---row-offset---ACC---sender-gas-refund (tx-finl---sender-gas-refund)) + (account-same-nonce tx-finl---row-offset---ACC---sender-gas-refund) + (account-same-code tx-finl---row-offset---ACC---sender-gas-refund) + (account-same-deployment-number-and-status tx-finl---row-offset---ACC---sender-gas-refund) + (account-same-warmth tx-finl---row-offset---ACC---sender-gas-refund) + (account-same-marked-for-selfdestruct tx-finl---row-offset---ACC---sender-gas-refund) + (DOM-SUB-stamps---standard tx-finl---row-offset---ACC---sender-gas-refund + 0))) diff --git a/hub/constraints/tx_finl/rows/transaction.lisp b/hub/constraints/tx_finl/rows/transaction.lisp new file mode 100644 index 00000000..fb16ae58 --- /dev/null +++ b/hub/constraints/tx_finl/rows/transaction.lisp @@ -0,0 +1,17 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_FINL phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Transaction row ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-finl---transaction-row---justifying-TXN_DATA-predictions + (:guard (tx-finl---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (shift transaction/STATUS_CODE tx-finl---row-offset---TXN) (tx-finl---transaction-success)) + (eq! (shift transaction/REFUND_COUNTER_INFINITY tx-finl---row-offset---TXN) (shift REFUND_COUNTER_NEW tx-finl---row-offset---row-preceding-the-finl-phase)) + (eq! (shift transaction/GAS_LEFTOVER tx-finl---row-offset---TXN) (shift GAS_NEXT tx-finl---row-offset---row-preceding-the-finl-phase)))) diff --git a/hub/constraints/tx_finl/shorthands.lisp b/hub/constraints/tx_finl/shorthands.lisp new file mode 100644 index 00000000..b568531d --- /dev/null +++ b/hub/constraints/tx_finl/shorthands.lisp @@ -0,0 +1,34 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_FINL phase ;; +;; X.Y Introduction ;; +;; X.Y Shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst + tx-finl---row-offset---row-preceding-the-finl-phase -1 + tx-finl---row-offset---ACC---sender-gas-refund 0 + tx-finl---row-offset---ACC---coinbase-reward 1 + tx-finl---row-offset---TXN 2 + ) + + + +(defun (tx-finl---standard-precondition) (* (shift TX_EXEC tx-finl---row-offset---row-preceding-the-finl-phase) TX_FINL)) +(defun (tx-finl---transaction-success) (- 1 (shift CONTEXT_WILL_REVERT tx-finl---row-offset---row-preceding-the-finl-phase))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-finl---sender-address-hi) (shift transaction/FROM_ADDRESS_HI tx-finl---row-offset---TXN)) +(defun (tx-finl---sender-address-lo) (shift transaction/FROM_ADDRESS_LO tx-finl---row-offset---TXN)) +(defun (tx-finl---coinbase-address-hi) (shift transaction/COINBASE_ADDRESS_HI tx-finl---row-offset---TXN)) +(defun (tx-finl---coinbase-address-lo) (shift transaction/COINBASE_ADDRESS_LO tx-finl---row-offset---TXN)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-finl---effective-gas-price) (shift transaction/GAS_PRICE tx-finl---row-offset---TXN)) +(defun (tx-finl---effective-gas-refund) (shift transaction/REFUND_EFFECTIVE tx-finl---row-offset---TXN)) +(defun (tx-finl---sender-gas-refund) (* (tx-finl---effective-gas-price) (tx-finl---effective-gas-refund))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-finl---priority-fee-per-gas) (shift transaction/PRIORITY_FEE_PER_GAS tx-finl---row-offset---TXN)) +(defun (tx-finl---gas-limit) (shift transaction/GAS_LIMIT tx-finl---row-offset---TXN)) +(defun (tx-finl---coinbase-reward) (* (- (tx-finl---gas-limit) (tx-finl---effective-gas-refund)) (tx-finl---priority-fee-per-gas))) diff --git a/hub/constraints/tx_init/constraints.lisp b/hub/constraints/tx_init/constraints.lisp deleted file mode 100644 index 742d2426..00000000 --- a/hub/constraints/tx_init/constraints.lisp +++ /dev/null @@ -1,231 +0,0 @@ -(module hub) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; X.1 Introduction ;; -;; X.2 Setting the peeking flags ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; TX_INIT[i - 1] = 0 && TX_INIT[i] = 1 -(defun (tx-init---standard-precondition) (* (- 1 (shift TX_INIT -1)) - TX_INIT)) - -(defconst - tx-init---row-offset---sender-account-row 0 - tx-init---row-offset---recipient-account-row 1 - tx-init---row-offset---miscellaneous-row 2 - tx-init---row-offset---context-initialization-row 3 - tx-init---row-offset---transaction-row 4 - tx-init---number-of-rows 5 - ) - -(defconstraint tx-initialization---setting-the-peeking-flags (:guard (tx-init---standard-precondition)) - (eq! (+ (shift PEEK_AT_ACCOUNT tx-init---row-offset---sender-account-row ) - (shift PEEK_AT_ACCOUNT tx-init---row-offset---recipient-account-row ) - (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---miscellaneous-row ) - (shift PEEK_AT_CONTEXT tx-init---row-offset---context-initialization-row ) - (shift PEEK_AT_TRANSACTION tx-init---row-offset---transaction-row )) - tx-init---number-of-rows)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; X.3 Common constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defun (tx-initialization---wei-cost-for-sender) (shift (+ transaction/VALUE - (* transaction/GAS_PRICE transaction/GAS_LIMIT)) - tx-init---row-offset---transaction-row)) - -;; sender account operation -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint tx-initialization---setting-sender-account-row (:guard (tx-init---standard-precondition)) - (begin - (eq! (shift account/ADDRESS_HI tx-init---row-offset---sender-account-row) (shift transaction/FROM_ADDRESS_HI tx-init---row-offset---transaction-row)) - (eq! (shift account/ADDRESS_LO tx-init---row-offset---sender-account-row) (shift transaction/FROM_ADDRESS_LO tx-init---row-offset---transaction-row)) - (account-decrement-balance-by tx-init---row-offset---sender-account-row (tx-initialization---wei-cost-for-sender)) - (account-increment-nonce tx-init---row-offset---sender-account-row) - (account-same-code tx-init---row-offset---sender-account-row) - (account-same-deployment-number-and-status tx-init---row-offset---sender-account-row) - (account-turn-on-warmth tx-init---row-offset---sender-account-row) - (account-same-marked-for-selfdestruct tx-init---row-offset---sender-account-row) - (account-isnt-precompile tx-init---row-offset---sender-account-row) - (DOM-SUB-stamps---standard tx-init---row-offset---sender-account-row - 0))) - -(defconstraint tx-initialization---EIP-3607---reject-transactions-from-senders-with-deployed-codey (:guard (tx-init---standard-precondition)) - (vanishes! (shift account/HAS_CODE tx-init---row-offset---sender-account-row))) - -;; recipient account operation -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defconstraint tx-initialization---setting-recipient-account-row (:guard (tx-init---standard-precondition)) - (begin - (eq! (shift account/ADDRESS_HI tx-init---row-offset---recipient-account-row) (shift transaction/TO_ADDRESS_HI tx-init---row-offset---transaction-row)) - (eq! (shift account/ADDRESS_LO tx-init---row-offset---recipient-account-row) (shift transaction/TO_ADDRESS_LO tx-init---row-offset---transaction-row)) - (account-increment-balance-by tx-init---row-offset---recipient-account-row (shift transaction/VALUE tx-init---row-offset---transaction-row)) - ;; (account-increment-nonce tx-init---row-offset---recipient-account-row) ;; message call tx vs deployment tx dependent - ;; (account-same-code tx-init---row-offset---recipient-account-row) ;; message call tx vs deployment tx dependent - ;; (account-same-deployment-number-and-status tx-init---row-offset---recipient-account-row) ;; message call tx vs deployment tx dependent - (account-turn-on-warmth tx-init---row-offset---recipient-account-row) - (account-same-marked-for-selfdestruct tx-init---row-offset---recipient-account-row) - (account-isnt-precompile tx-init---row-offset---recipient-account-row) - (account-retrieve-code-fragment-index tx-init---row-offset---recipient-account-row) - (DOM-SUB-stamps---standard tx-init---row-offset---recipient-account-row - 1))) - -(defun (tx-initialization---is-deployment) (force-bin (shift transaction/IS_DEPLOYMENT tx-init---row-offset---transaction-row))) - -;; message call case - -(defconstraint tx-initialization---recipient-account-row---message-call-tx---nonce-code-and-deployment-status (:guard (tx-init---standard-precondition)) - (if-zero (tx-initialization---is-deployment) - ;; deployment ≡ 0 i.e. smart contract call - (begin - (account-same-nonce tx-init---row-offset---recipient-account-row) - (account-same-code tx-init---row-offset---recipient-account-row) - (account-same-deployment-number-and-status tx-init---row-offset---recipient-account-row)))) - -(defconstraint tx-initialization---recipient-account-row---message-call-tx---address-trimming (:guard (tx-init---standard-precondition)) - (if-zero (tx-initialization---is-deployment) - ;; deployment ≡ 0 i.e. smart contract call - ;; trimming address - (account-trim-address tx-init---row-offset---recipient-account-row - (shift transaction/TO_ADDRESS_HI tx-init---row-offset---transaction-row) - (shift transaction/TO_ADDRESS_LO tx-init---row-offset---transaction-row)))) - -;; deployment case - -(defconstraint tx-initialization---recipient-account-row---deployment-transaction---nonce (:guard (tx-init---standard-precondition)) - (if-not-zero (tx-initialization---is-deployment) - ;; deployment ≡ 1 i.e. nontrivial deployments - (begin - ;; nonce - (account-increment-nonce tx-init---row-offset---recipient-account-row) - (debug (vanishes! (shift account/NONCE tx-init---row-offset---recipient-account-row)))))) - -(defconstraint tx-initialization---recipient-account-row---deployment-transaction---code (:guard (tx-init---standard-precondition)) - (if-not-zero (tx-initialization---is-deployment) - ;; deployment ≡ 1 i.e. nontrivial deployments - (begin - ;; code - ;; current code - (vanishes! (shift account/HAS_CODE tx-init---row-offset---recipient-account-row)) - (debug (eq! (shift account/CODE_HASH_HI tx-init---row-offset---recipient-account-row) EMPTY_KECCAK_HI)) - (debug (eq! (shift account/CODE_HASH_LO tx-init---row-offset---recipient-account-row) EMPTY_KECCAK_LO)) - (vanishes! (shift account/CODE_SIZE tx-init---row-offset---recipient-account-row)) - ;; updated code - (vanishes! (shift account/HAS_CODE_NEW tx-init---row-offset---recipient-account-row)) - (debug (eq! (shift account/CODE_HASH_HI_NEW tx-init---row-offset---recipient-account-row) EMPTY_KECCAK_HI)) - (debug (eq! (shift account/CODE_HASH_LO_NEW tx-init---row-offset---recipient-account-row) EMPTY_KECCAK_LO)) - (eq! (shift account/CODE_SIZE_NEW tx-init---row-offset---recipient-account-row) - (shift transaction/INIT_CODE_SIZE tx-init---row-offset---transaction-row))))) - -(defconstraint tx-initialization---recipient-account-row---deployment-transaction---deployment-number-and-status (:guard (tx-init---standard-precondition)) - (if-not-zero (tx-initialization---is-deployment) - ;; deployment ≡ 1 i.e. nontrivial deployments - (begin - ;; deployment - (account-increment-deployment-number tx-init---row-offset---recipient-account-row) - (debug (eq! (shift account/DEPLOYMENT_STATUS tx-init---row-offset---recipient-account-row) 0)) - (eq! (shift account/DEPLOYMENT_STATUS_NEW tx-init---row-offset---recipient-account-row) 1)))) - -;; miscellaneous row -;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;; - - -(defun (tx-initialization---call-data-context-number) (* HUB_STAMP - (shift transaction/COPY_TXCD tx-init---row-offset---transaction-row))) - -(defun (tx-initialization---call-data-size) (shift transaction/CALL_DATA_SIZE tx-init---row-offset---transaction-row)) - -(defconstraint tx-initialization---setting-miscellaneous-row-flags (:guard (tx-init---standard-precondition)) - (eq! (weighted-MISC-flag-sum tx-init---row-offset---miscellaneous-row) - (* MISC_WEIGHT_MMU - (shift transaction/COPY_TXCD tx-init---row-offset---transaction-row)))) - -(defconstraint tx-initialization---copying-transaction-call-data (:guard (tx-init---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG tx-init---row-offset---miscellaneous-row) - (set-MMU-instruction---exo-to-ram-transplants tx-init---row-offset---miscellaneous-row ;; offset - ABS_TX_NUM ;; source ID - (tx-initialization---call-data-context-number) ;; target ID - ;; aux_id ;; auxiliary ID - ;; src_offset_hi ;; source offset high - ;; src_offset_lo ;; source offset low - ;; tgt_offset_lo ;; target offset low - (tx-initialization---call-data-size) ;; size - ;; ref_offset ;; reference offset - ;; ref_size ;; reference size - ;; success_bit ;; success bit - ;; limb_1 ;; limb 1 - ;; limb_2 ;; limb 2 - EXO_SUM_WEIGHT_TXCD ;; weighted exogenous module flag sum - RLP_TXN_PHASE_DATA ;; phase - ))) - -(defconstraint tx-initialization---initializing-context (:guard (tx-init---standard-precondition)) - (begin - (initialize-context - tx-init---row-offset---context-initialization-row ;; row offset - CONTEXT_NUMBER_NEW ;; context number - 0 ;; call stack depth - 1 ;; is root - 0 ;; is static - (shift transaction/TO_ADDRESS_HI tx-init---row-offset---transaction-row) ;; account address high - (shift transaction/TO_ADDRESS_LO tx-init---row-offset---transaction-row) ;; account address low - (shift account/DEPLOYMENT_NUMBER_NEW tx-init---row-offset---recipient-account-row) ;; account deployment number - (shift transaction/TO_ADDRESS_HI tx-init---row-offset---transaction-row) ;; byte code address high - (shift transaction/TO_ADDRESS_LO tx-init---row-offset---transaction-row) ;; byte code address low - (shift account/DEPLOYMENT_NUMBER_NEW tx-init---row-offset---recipient-account-row) ;; byte code deployment number - (shift account/DEPLOYMENT_STATUS_NEW tx-init---row-offset---recipient-account-row) ;; byte code deployment status - (shift account/CODE_FRAGMENT_INDEX tx-init---row-offset---recipient-account-row) ;; byte code code fragment index - (shift transaction/FROM_ADDRESS_HI tx-init---row-offset---transaction-row) ;; caller address high - (shift transaction/FROM_ADDRESS_LO tx-init---row-offset---transaction-row) ;; caller address low - (shift transaction/VALUE tx-init---row-offset---transaction-row) ;; call value - (tx-initialization---call-data-context-number) ;; caller context - 0 ;; call data offset - (tx-initialization---call-data-size) ;; call data size - 0 ;; return at offset - 0 ;; return at capacity - ) - (debug (eq! CONTEXT_NUMBER_NEW (+ 1 HUB_STAMP))))) - - -(defconstraint tx-initialization---transaction-row-partially-justifying-requires-evm-execution (:guard (tx-init---standard-precondition)) - (begin - (eq! (shift transaction/REQUIRES_EVM_EXECUTION tx-init---row-offset---transaction-row) 1) - (if-zero (shift transaction/IS_DEPLOYMENT tx-init---row-offset---transaction-row) - (eq! (shift account/HAS_CODE tx-init---row-offset---recipient-account-row) 1) - (is-not-zero! (shift transaction/INIT_CODE_SIZE tx-init---row-offset---transaction-row))))) - -;; REFUNDS cannot be set at the present time - -(defconstraint tx-initialization---transaction-row-justifying-initial-balance (:guard (tx-init---standard-precondition)) - (eq! (shift account/BALANCE tx-init---row-offset---sender-account-row) - (shift transaction/INITIAL_BALANCE tx-init---row-offset---transaction-row))) - -(defconstraint tx-initialization---transaction-row-justifying-status-code (:guard (tx-init---standard-precondition)) - (eq! (shift transaction/STATUS_CODE tx-init---row-offset---transaction-row) - (- 1 (shift CONTEXT_WILL_REVERT (+ 1 tx-init---row-offset---transaction-row))))) - -(defconstraint tx-initialization---transaction-row-justifying-nonce (:guard (tx-init---standard-precondition)) - (eq! (shift transaction/NONCE tx-init---row-offset---transaction-row) - (shift account/NONCE tx-init---row-offset---sender-account-row))) - -;; LEFTOVER_GAS cannot be set at the present time - -(defconstraint tx-initialization---first-row-of-next-context-initializing-some-variables (:guard (tx-init---standard-precondition)) - (first-row-of-new-context (+ 1 tx-init---row-offset---transaction-row) ;; row offset - 0 ;; next caller context number - (shift account/CODE_FRAGMENT_INDEX tx-init---row-offset---recipient-account-row) ;; next CFI - (shift transaction/GAS_INITIALLY_AVAILABLE tx-init---row-offset---transaction-row ) ;; initially available gas - )) diff --git a/hub/constraints/tx_init/peeking.lisp b/hub/constraints/tx_init/peeking.lisp new file mode 100644 index 00000000..8e9e8f37 --- /dev/null +++ b/hub/constraints/tx_init/peeking.lisp @@ -0,0 +1,57 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Setting the peeking flags ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---setting-peeking-flags---unconditionally-on-the-first-two-rows + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC) + (shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN)) + 2)) + +(defconstraint tx-init---setting-peeking-flags---transaction-failure + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC ) + (shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-pay-for-gas ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer---undoing ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception---undoing ) + (shift PEEK_AT_CONTEXT tx-init---row-offset---CON---context-initialization-row---failure)) + 8))) + +(defconstraint tx-init---setting-peeking-flags---transaction-success + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-success-prediction) + (eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC ) + (shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-pay-for-gas ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer ) + (shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception ) + (shift PEEK_AT_CONTEXT tx-init---row-offset---CON---context-initialization-row---success)) + 6))) + +(defconstraint tx-init---justifying-predictions---transaction-failure + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (begin + (eq! (tx-init---transaction-failure-prediction) (shift CONTEXT_WILL_REVERT tx-init---row-offset---first-execution-phase-row---failure)) + (eq! (tx-init---transaction-end-stamp) (shift CONTEXT_REVERT_STAMP tx-init---row-offset---first-execution-phase-row---failure))))) + +(defconstraint tx-init---justifying-predictions---transaction-success + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-success-prediction) + (begin + (eq! (tx-init---transaction-failure-prediction) (shift CONTEXT_WILL_REVERT tx-init---row-offset---first-execution-phase-row---success)) + (eq! (tx-init---transaction-end-stamp) (shift CONTEXT_REVERT_STAMP tx-init---row-offset---first-execution-phase-row---success))))) diff --git a/hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp b/hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp new file mode 100644 index 00000000..9af709ec --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp @@ -0,0 +1,77 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Recipient accepts value transfer ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-init---account-row---recipient-value-reception + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (shift account/ADDRESS_HI tx-init---row-offset---ACC---recipient-value-reception) (tx-init---recipient-address-hi)) + (eq! (shift account/ADDRESS_LO tx-init---row-offset---ACC---recipient-value-reception) (tx-init---recipient-address-lo)) + (account-trim-address tx-init---row-offset---ACC---recipient-value-reception + (tx-init---recipient-address-hi) + (tx-init---recipient-address-lo)) + (account-increment-balance-by tx-init---row-offset---ACC---recipient-value-reception (tx-init---value)) + ;; (account-same-nonce tx-init---row-offset---ACC---recipient-value-reception) + ;; (account-same-code tx-init---row-offset---ACC---recipient-value-reception) + ;; (account-same-deployment-number-and-status tx-init---row-offset---ACC---recipient-value-reception) + (account-turn-on-warmth tx-init---row-offset---ACC---recipient-value-reception) + (account-same-marked-for-selfdestruct tx-init---row-offset---ACC---recipient-value-reception) + (account-retrieve-code-fragment-index tx-init---row-offset---ACC---recipient-value-reception) + (account-isnt-precompile tx-init---row-offset---ACC---recipient-value-reception) + (DOM-SUB-stamps---standard tx-init---row-offset---ACC---recipient-value-reception + 2))) + +(defconstraint tx-init---account-row---recipient-value-reception---message-call + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---is-message-call) + (begin + (account-same-nonce tx-init---row-offset---ACC---recipient-value-reception) + (account-same-code tx-init---row-offset---ACC---recipient-value-reception) + (account-same-deployment-number-and-status tx-init---row-offset---ACC---recipient-value-reception)))) + +(defconstraint tx-init---account-row---recipient-value-reception---deployment---nonce + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---is-deployment) + (begin + (account-increment-nonce tx-init---row-offset---ACC---recipient-value-reception) + (vanishes! (shift account/NONCE tx-init---row-offset---ACC---recipient-value-reception)) + ))) + +(defconstraint tx-init---account-row---recipient-value-reception---deployment---code + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---is-deployment) + (begin + ;; current code + (vanishes! (shift account/HAS_CODE tx-init---row-offset---ACC---recipient-value-reception)) + (debug (eq! (shift account/CODE_HASH_HI tx-init---row-offset---ACC---recipient-value-reception) EMPTY_KECCAK_HI)) + (debug (eq! (shift account/CODE_HASH_LO tx-init---row-offset---ACC---recipient-value-reception) EMPTY_KECCAK_LO)) + (vanishes! (shift account/CODE_SIZE tx-init---row-offset---ACC---recipient-value-reception)) + ;; updated code + (vanishes! (shift account/HAS_CODE_NEW tx-init---row-offset---ACC---recipient-value-reception)) + (debug (eq! (shift account/CODE_HASH_HI_NEW tx-init---row-offset---ACC---recipient-value-reception) EMPTY_KECCAK_HI)) + (debug (eq! (shift account/CODE_HASH_LO_NEW tx-init---row-offset---ACC---recipient-value-reception) EMPTY_KECCAK_LO)) + (eq! (shift account/CODE_SIZE_NEW tx-init---row-offset---ACC---recipient-value-reception) + (tx-init---init-code-size))))) + +(defconstraint tx-init---account-row---recipient-value-reception---deployment---deployment-number-and-status + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---is-deployment) + (begin + ;; deployment + (vanishes! (shift account/DEPLOYMENT_NUMBER tx-init---row-offset---ACC---recipient-value-reception)) + (account-increment-deployment-number tx-init---row-offset---ACC---recipient-value-reception) + (eq! (shift account/DEPLOYMENT_STATUS tx-init---row-offset---ACC---recipient-value-reception) 0) + (eq! (shift account/DEPLOYMENT_STATUS_NEW tx-init---row-offset---ACC---recipient-value-reception) 1)))) + diff --git a/hub/constraints/tx_init/rows/acc_sender_gas_payment.lisp b/hub/constraints/tx_init/rows/acc_sender_gas_payment.lisp new file mode 100644 index 00000000..b043b945 --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_sender_gas_payment.lisp @@ -0,0 +1,35 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Sender pays for gas_cost ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-init---account-row---sender-pays-for-gas + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (shift account/ADDRESS_HI tx-init---row-offset---ACC---sender-pay-for-gas) (tx-init---sender-address-hi)) + (eq! (shift account/ADDRESS_LO tx-init---row-offset---ACC---sender-pay-for-gas) (tx-init---sender-address-lo)) + (account-trim-address tx-init---row-offset---ACC---sender-pay-for-gas + (tx-init---sender-address-hi) + (tx-init---sender-address-lo)) + (account-decrement-balance-by tx-init---row-offset---ACC---sender-pay-for-gas (tx-init---gas-cost)) + (account-increment-nonce tx-init---row-offset---ACC---sender-pay-for-gas) + (account-same-code tx-init---row-offset---ACC---sender-pay-for-gas) + (account-same-deployment-number-and-status tx-init---row-offset---ACC---sender-pay-for-gas) + (account-turn-on-warmth tx-init---row-offset---ACC---sender-pay-for-gas) + (account-same-marked-for-selfdestruct tx-init---row-offset---ACC---sender-pay-for-gas) + (account-isnt-precompile tx-init---row-offset---ACC---sender-pay-for-gas) + (DOM-SUB-stamps---standard tx-init---row-offset---ACC---sender-pay-for-gas + 0))) + + +(defconstraint tx-init---EIP-3607---reject-transactions-from-senders-with-deployed-code + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift account/HAS_CODE tx-init---row-offset---ACC---sender-pay-for-gas))) diff --git a/hub/constraints/tx_init/rows/acc_sender_value_transfer.lisp b/hub/constraints/tx_init/rows/acc_sender_value_transfer.lisp new file mode 100644 index 00000000..8d6a3b1d --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_sender_value_transfer.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Transaction row ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---account-row---sender-value-transfer + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (account-same-address-as tx-init---row-offset---ACC---sender-value-transfer + tx-init---row-offset---ACC---sender-pay-for-gas) + (account-decrement-balance-by tx-init---row-offset---ACC---sender-value-transfer (tx-init---value)) + (account-same-nonce tx-init---row-offset---ACC---sender-value-transfer) + (account-same-code tx-init---row-offset---ACC---sender-value-transfer) + (account-same-deployment-number-and-status tx-init---row-offset---ACC---sender-value-transfer) + (account-same-warmth tx-init---row-offset---ACC---sender-value-transfer) + (account-same-marked-for-selfdestruct tx-init---row-offset---ACC---sender-value-transfer) + (account-isnt-precompile tx-init---row-offset---ACC---sender-value-transfer) + (DOM-SUB-stamps---standard tx-init---row-offset---ACC---sender-value-transfer + 1))) diff --git a/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp b/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp new file mode 100644 index 00000000..45e989f8 --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Undoing recipient account value reception ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---account-row---recipient-value-reception---undoing-row + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (begin + (account-same-address-as tx-init---row-offset---ACC---recipient-value-reception---undoing tx-init---row-offset---ACC---recipient-value-reception) + (account-undo-balance-update tx-init---row-offset---ACC---recipient-value-reception---undoing tx-init---row-offset---ACC---recipient-value-reception) + (account-undo-nonce-update tx-init---row-offset---ACC---recipient-value-reception---undoing tx-init---row-offset---ACC---recipient-value-reception) + (account-undo-code-update tx-init---row-offset---ACC---recipient-value-reception---undoing tx-init---row-offset---ACC---recipient-value-reception) + (account-same-warmth tx-init---row-offset---ACC---recipient-value-reception---undoing) + (account-undo-deployment-status-update tx-init---row-offset---ACC---recipient-value-reception---undoing tx-init---row-offset---ACC---recipient-value-reception) + (account-same-marked-for-selfdestruct tx-init---row-offset---ACC---recipient-value-reception---undoing) + (DOM-SUB-stamps---revert-with-child tx-init---row-offset---ACC---recipient-value-reception---undoing + 4 + (tx-init---transaction-end-stamp))))) diff --git a/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp b/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp new file mode 100644 index 00000000..07a67260 --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp @@ -0,0 +1,28 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Undoing sender account value transfer ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---account-row---sender-value-transfer---undoing-row + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (begin + (account-same-address-as tx-init---row-offset---ACC---sender-value-transfer---undoing + tx-init---row-offset---ACC---sender-value-transfer) + (account-undo-balance-update tx-init---row-offset---ACC---sender-value-transfer---undoing + tx-init---row-offset---ACC---sender-value-transfer) + (account-same-nonce tx-init---row-offset---ACC---sender-value-transfer---undoing) + (account-same-code tx-init---row-offset---ACC---sender-value-transfer---undoing) + (account-same-deployment-number-and-status tx-init---row-offset---ACC---sender-value-transfer---undoing) + (account-same-warmth tx-init---row-offset---ACC---sender-value-transfer---undoing) + (account-same-marked-for-selfdestruct tx-init---row-offset---ACC---sender-value-transfer---undoing) + (account-isnt-precompile tx-init---row-offset---ACC---sender-value-transfer---undoing) + (DOM-SUB-stamps---revert-with-child tx-init---row-offset---ACC---sender-value-transfer---undoing + 3 + (tx-init---transaction-end-stamp))))) diff --git a/hub/constraints/tx_init/rows/con_initialization.lisp b/hub/constraints/tx_init/rows/con_initialization.lisp new file mode 100644 index 00000000..d64ead53 --- /dev/null +++ b/hub/constraints/tx_init/rows/con_initialization.lisp @@ -0,0 +1,50 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Transaction row ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (tx-init---initialize-execution-context row-offset) + (begin (initialize-context row-offset + CONTEXT_NUMBER_NEW ;; context number + 0 ;; call stack depth + 1 ;; is root + 0 ;; is static + (tx-init---recipient-address-hi) ;; account address high + (tx-init---recipient-address-lo) ;; account address low + (shift account/DEPLOYMENT_NUMBER_NEW tx-init---row-offset---ACC---recipient-value-reception) ;; account deployment number + (tx-init---recipient-address-hi) ;; byte code address high + (tx-init---recipient-address-lo) ;; byte code address low + (shift account/DEPLOYMENT_NUMBER_NEW tx-init---row-offset---ACC---recipient-value-reception) ;; byte code deployment number + (shift account/DEPLOYMENT_STATUS_NEW tx-init---row-offset---ACC---recipient-value-reception) ;; byte code deployment status + (shift account/CODE_FRAGMENT_INDEX tx-init---row-offset---ACC---recipient-value-reception) ;; byte code code fragment index + (tx-init---sender-address-hi) ;; caller address high + (tx-init---sender-address-lo) ;; caller address low + (tx-init---value) ;; call value + (tx-init---call-data-context-number) ;; caller context + 0 ;; call data offset + (tx-init---call-data-size) ;; call data size + 0 ;; return at offset + 0 ;; return at capacity + ))) + +(defconstraint tx-init---initializing-execution-context---failure + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (tx-init---initialize-execution-context tx-init---row-offset---CON---context-initialization-row---failure))) + +(defconstraint tx-init---initializing-execution-context---success + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-success-prediction) + (tx-init---initialize-execution-context tx-init---row-offset---CON---context-initialization-row---success))) + +(defconstraint tx-init---CONTEXT_NUMBER_NEW-sanity-check + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! CONTEXT_NUMBER_NEW (+ 1 HUB_STAMP))) diff --git a/hub/constraints/tx_init/rows/first_execution_row_parameters.lisp b/hub/constraints/tx_init/rows/first_execution_row_parameters.lisp new file mode 100644 index 00000000..d2a1162d --- /dev/null +++ b/hub/constraints/tx_init/rows/first_execution_row_parameters.lisp @@ -0,0 +1,31 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z First row of execution ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---setting-parameters-on-the-first-row-of-new-context---failure + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-failure-prediction) + (first-row-of-new-context + tx-init---row-offset---first-execution-phase-row---failure ;; row offset + 0 ;; next caller context number + (shift account/CODE_FRAGMENT_INDEX tx-init---row-offset---ACC---recipient-value-reception) ;; next CFI + (shift transaction/GAS_INITIALLY_AVAILABLE tx-init---row-offset---TXN) ;; initially available gas + ))) + +(defconstraint tx-init---setting-parameters-on-the-first-row-of-new-context---success + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (tx-init---transaction-success-prediction) + (first-row-of-new-context + tx-init---row-offset---first-execution-phase-row---success ;; row offset + 0 ;; next caller context number + (shift account/CODE_FRAGMENT_INDEX tx-init---row-offset---ACC---recipient-value-reception) ;; next CFI + (shift transaction/GAS_INITIALLY_AVAILABLE tx-init---row-offset---TXN) ;; initially available gas + ))) diff --git a/hub/constraints/tx_init/rows/miscellaneous.lisp b/hub/constraints/tx_init/rows/miscellaneous.lisp new file mode 100644 index 00000000..bca30d5d --- /dev/null +++ b/hub/constraints/tx_init/rows/miscellaneous.lisp @@ -0,0 +1,37 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Miscellaneous row ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint tx-init---setting-miscellaneous-row-flags + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum tx-init---row-offset---MISC) + (* MISC_WEIGHT_MMU (shift transaction/COPY_TXCD tx-init---row-offset---TXN)))) + +(defconstraint tx-init---copying-transaction-call-data + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (shift misc/MMU_FLAG tx-init---row-offset---MISC) + (set-MMU-instruction---exo-to-ram-transplants tx-init---row-offset---MISC ;; offset + ABS_TX_NUM ;; source ID + (tx-init---call-data-context-number) ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + ;; src_offset_lo ;; source offset low + ;; tgt_offset_lo ;; target offset low + (tx-init---call-data-size) ;; size + ;; ref_offset ;; reference offset + ;; ref_size ;; reference size + ;; success_bit ;; success bit + ;; limb_1 ;; limb 1 + ;; limb_2 ;; limb 2 + EXO_SUM_WEIGHT_TXCD ;; weighted exogenous module flag sum + RLP_TXN_PHASE_DATA ;; phase + ))) diff --git a/hub/constraints/tx_init/rows/transaction.lisp b/hub/constraints/tx_init/rows/transaction.lisp new file mode 100644 index 00000000..278cc89b --- /dev/null +++ b/hub/constraints/tx_init/rows/transaction.lisp @@ -0,0 +1,37 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; +;; X.Y.Z Transaction row ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint tx-init---transaction-row---partially-justifying-requires-evm-execution + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! 1 (shift transaction/REQUIRES_EVM_EXECUTION tx-init---row-offset---TXN)) + (if-not-zero (tx-init---is-message-call) + (eq! 1 (shift account/HAS_CODE tx-init---row-offset---ACC---recipient-value-reception))) + (if-not-zero (tx-init---is-deployment) + (is-not-zero! (tx-init---init-code-size))))) + +(defconstraint tx-init---transaction-row---justifying-initial-balance + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (shift account/BALANCE tx-init---row-offset---ACC---sender-pay-for-gas) + (shift transaction/INITIAL_BALANCE tx-init---row-offset---TXN))) + +(defconstraint tx-init---transaction-row---justifying-status-code + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (shift transaction/STATUS_CODE tx-init---row-offset---TXN) + (tx-init---transaction-success-prediction))) + +(defconstraint tx-init---transaction-row---justifying-nonce + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (shift transaction/NONCE tx-init---row-offset---TXN) + (shift account/NONCE tx-init---row-offset---ACC---sender-pay-for-gas))) diff --git a/hub/constraints/tx_init/shorthands.lisp b/hub/constraints/tx_init/shorthands.lisp new file mode 100644 index 00000000..1529d0b9 --- /dev/null +++ b/hub/constraints/tx_init/shorthands.lisp @@ -0,0 +1,46 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Introduction ;; +;; X.Y Shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst + tx-init---row-offset---row-preceding-the-init-phase -1 + tx-init---row-offset---MISC 0 + tx-init---row-offset---TXN 1 + tx-init---row-offset---ACC---sender-pay-for-gas 2 + tx-init---row-offset---ACC---sender-value-transfer 3 + tx-init---row-offset---ACC---recipient-value-reception 4 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + tx-init---row-offset---CON---context-initialization-row---success 5 + tx-init---row-offset---first-execution-phase-row---success 6 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + tx-init---row-offset---ACC---sender-value-transfer---undoing 5 + tx-init---row-offset---ACC---recipient-value-reception---undoing 6 + tx-init---row-offset---CON---context-initialization-row---failure 7 + tx-init---row-offset---first-execution-phase-row---failure 8 + ) + + + +(defun (tx-init---standard-precondition) (* (shift (- 1 TX_INIT) tx-init---row-offset---row-preceding-the-init-phase) TX_INIT)) +(defun (tx-init---transaction-failure-prediction) (shift misc/CCSR_FLAG tx-init---row-offset---MISC)) +(defun (tx-init---transaction-success-prediction) (- 1 (tx-init---transaction-failure-prediction))) +(defun (tx-init---transaction-end-stamp) (shift misc/CCRS_STAMP tx-init---row-offset---MISC)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-init---sender-address-hi) (shift transaction/FROM_ADDRESS_HI tx-init---row-offset---TXN)) +(defun (tx-init---sender-address-lo) (shift transaction/FROM_ADDRESS_LO tx-init---row-offset---TXN)) +(defun (tx-init---recipient-address-hi) (shift transaction/TO_ADDRESS_HI tx-init---row-offset---TXN)) +(defun (tx-init---recipient-address-lo) (shift transaction/TO_ADDRESS_LO tx-init---row-offset---TXN)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-init---is-deployment) (shift transaction/IS_DEPLOYMENT tx-init---row-offset---TXN)) +(defun (tx-init---is-message-call) (- 1 (tx-init---is-deployment))) +(defun (tx-init---gas-cost) (shift (* transaction/GAS_LIMIT transaction/GAS_PRICE) tx-init---row-offset---TXN)) +(defun (tx-init---value) (shift transaction/VALUE tx-init---row-offset---TXN)) +(defun (tx-init---call-data-context-number) (* HUB_STAMP (shift transaction/COPY_TXCD tx-init---row-offset---TXN))) +(defun (tx-init---call-data-size) (shift transaction/CALL_DATA_SIZE tx-init---row-offset---TXN)) +(defun (tx-init---init-code-size) (shift transaction/INIT_CODE_SIZE tx-init---row-offset---TXN))