From 2fc07250f771edc25bad3ecfa9bd37053db1e870 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 16:15:49 +0700 Subject: [PATCH 1/6] wip --- hub/constraints/tx_init/common.lisp | 0 hub/constraints/tx_init/peeking.lisp | 10 ++++++++ hub/constraints/tx_init/shorthands.lisp | 31 +++++++++++++++++++++++++ 3 files changed, 41 insertions(+) create mode 100644 hub/constraints/tx_init/common.lisp create mode 100644 hub/constraints/tx_init/peeking.lisp create mode 100644 hub/constraints/tx_init/shorthands.lisp diff --git a/hub/constraints/tx_init/common.lisp b/hub/constraints/tx_init/common.lisp new file mode 100644 index 00000000..e69de29b diff --git a/hub/constraints/tx_init/peeking.lisp b/hub/constraints/tx_init/peeking.lisp new file mode 100644 index 00000000..ee2e4d2b --- /dev/null +++ b/hub/constraints/tx_init/peeking.lisp @@ -0,0 +1,10 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Setting the peeking flags ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + diff --git a/hub/constraints/tx_init/shorthands.lisp b/hub/constraints/tx_init/shorthands.lisp new file mode 100644 index 00000000..ebf1ac44 --- /dev/null +++ b/hub/constraints/tx_init/shorthands.lisp @@ -0,0 +1,31 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Introduction ;; +;; X.Y Shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst + tx-init---row-offset---last-execution-row -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---WILL_REVERT 5 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + tx-init---row-offset---ACC---undoing-sender-value-transfer 5 + tx-init---row-offset---ACC---undoing-recipient-value-reception 6 + tx-init---row-offset---CON---context-initialization-row---WILL_REVERT 7 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + tx-init---number-of-rows---WILL_REVERT 6 + tx-init---number-of-rows---WONT_REVERT 8 + ) + +(defun (tx-init---transaction-will-revert) (shift CONTEXT_WILL_REVERT tx-init---row-offset---last-execution-row)) +(defun (tx-init---transaction-wont-revert) (- 1 (tx-init---transaction-will-revert)) +(defun (tx-init---transaction-end-stamp) (shift TX_END_STAMP tx-init---row-offset---last-execution-row)) From d9fa89a1da57c174846e984e4e6fc495effa03c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sun, 1 Dec 2024 20:19:20 +0700 Subject: [PATCH 2/6] feat: update of initialization phase --- hub/constraints/tx_init/peeking.lisp | 47 +++++++++++ .../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 | 24 ++++++ .../rows/acc_undo_sender_value_transfer.lisp | 27 +++++++ .../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 | 37 ++++++--- 11 files changed, 416 insertions(+), 11 deletions(-) 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 diff --git a/hub/constraints/tx_init/peeking.lisp b/hub/constraints/tx_init/peeking.lisp index ee2e4d2b..a3865e8c 100644 --- a/hub/constraints/tx_init/peeking.lisp +++ b/hub/constraints/tx_init/peeking.lisp @@ -7,4 +7,51 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(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-will-revert) + (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) + (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-will-revert) (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-will-revert) (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..20d02d96 --- /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---sender-address-hi) + (tx-init---sender-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-same-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))) + +(defcontraint 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)))) + +(defcontraint 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)) + )) + +(defcontraint 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))))) + +(defcontraint 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..d5b44a98 --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp @@ -0,0 +1,24 @@ +(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 + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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..e818672f --- /dev/null +++ b/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp @@ -0,0 +1,27 @@ +(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 + (:guard (tx-init---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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..056e78cf --- /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---sender-pay-for-gas) ;; 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---sender-pay-for-gas) ;; 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 index ebf1ac44..5f057099 100644 --- a/hub/constraints/tx_init/shorthands.lisp +++ b/hub/constraints/tx_init/shorthands.lisp @@ -9,23 +9,38 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconst - tx-init---row-offset---last-execution-row -1 + 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---WILL_REVERT 5 + 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---undoing-sender-value-transfer 5 - tx-init---row-offset---ACC---undoing-recipient-value-reception 6 - tx-init---row-offset---CON---context-initialization-row---WILL_REVERT 7 - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - tx-init---number-of-rows---WILL_REVERT 6 - tx-init---number-of-rows---WONT_REVERT 8 + 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-case 8 ) -(defun (tx-init---transaction-will-revert) (shift CONTEXT_WILL_REVERT tx-init---row-offset---last-execution-row)) -(defun (tx-init---transaction-wont-revert) (- 1 (tx-init---transaction-will-revert)) -(defun (tx-init---transaction-end-stamp) (shift TX_END_STAMP tx-init---row-offset---last-execution-row)) + + +(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-will-revert))) +(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)) From ab1e32edf5b83e5a423794235afb3901347cc9a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sun, 1 Dec 2024 20:40:36 +0700 Subject: [PATCH 3/6] fix: make it compile --- Makefile | 1 + hub/constraints/tx_init/common.lisp | 0 hub/constraints/tx_init/constraints.lisp | 231 ------------------ hub/constraints/tx_init/peeking.lisp | 12 +- .../rows/acc_recipient_value_transfer.lisp | 84 +++---- .../acc_undo_recipient_value_reception.lisp | 14 +- .../rows/acc_undo_sender_value_transfer.lisp | 2 +- hub/constraints/tx_init/shorthands.lisp | 4 +- 8 files changed, 59 insertions(+), 289 deletions(-) delete mode 100644 hub/constraints/tx_init/common.lisp delete mode 100644 hub/constraints/tx_init/constraints.lisp diff --git a/Makefile b/Makefile index c9eed6d8..79305073 100644 --- a/Makefile +++ b/Makefile @@ -28,6 +28,7 @@ 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/*lisp) \ $(wildcard hub/lookups/*lisp) \ diff --git a/hub/constraints/tx_init/common.lisp b/hub/constraints/tx_init/common.lisp deleted file mode 100644 index e69de29b..00000000 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 index a3865e8c..8e9e8f37 100644 --- a/hub/constraints/tx_init/peeking.lisp +++ b/hub/constraints/tx_init/peeking.lisp @@ -17,7 +17,7 @@ (defconstraint tx-init---setting-peeking-flags---transaction-failure (:guard (tx-init---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (tx-init---transaction-will-revert) + (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 ) @@ -31,7 +31,7 @@ (defconstraint tx-init---setting-peeking-flags---transaction-success (:guard (tx-init---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (tx-init---transaction-success) + (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 ) @@ -45,13 +45,13 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (tx-init---transaction-failure-prediction) (begin - (eq! (tx-init---transaction-will-revert) (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))))) + (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-will-revert) (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))))) + (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 index 20d02d96..29d61781 100644 --- a/hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp +++ b/hub/constraints/tx_init/rows/acc_recipient_value_transfer.lisp @@ -29,49 +29,49 @@ (DOM-SUB-stamps---standard tx-init---row-offset---ACC---recipient-value-reception 2))) -(defcontraint 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---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)))) -(defcontraint 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---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)) + )) -(defcontraint 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---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))))) -(defcontraint 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)))) +(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_undo_recipient_value_reception.lisp b/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp index d5b44a98..338ea7f1 100644 --- a/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp +++ b/hub/constraints/tx_init/rows/acc_undo_recipient_value_reception.lisp @@ -1,14 +1,14 @@ (module hub) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; X TX_INIT phase ;; -;; X.Y Common constraints ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X TX_INIT phase ;; +;; X.Y Common constraints ;; ;; X.Y.Z Undoing recipient account value reception ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint tx-init---account-row---recipient-value-reception +(defconstraint tx-init---account-row---recipient-value-reception---undoing-row (:guard (tx-init---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin 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 index e818672f..7ac518aa 100644 --- a/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp +++ b/hub/constraints/tx_init/rows/acc_undo_sender_value_transfer.lisp @@ -8,7 +8,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint tx-init---account-row---sender-value-transfer +(defconstraint tx-init---account-row---sender-value-transfer---undoing-row (:guard (tx-init---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin diff --git a/hub/constraints/tx_init/shorthands.lisp b/hub/constraints/tx_init/shorthands.lisp index 5f057099..1529d0b9 100644 --- a/hub/constraints/tx_init/shorthands.lisp +++ b/hub/constraints/tx_init/shorthands.lisp @@ -22,14 +22,14 @@ 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-case 8 + 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-will-revert))) +(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)) From d1240cd3f6656544f4c8c3c35e624f65e2a7370a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sun, 1 Dec 2024 22:52:12 +0700 Subject: [PATCH 4/6] feat: finalization phase update --- hub/constants.lisp | 7 ++-- hub/constraints/tx_finl/peeking.lisp | 17 ++++++++++ .../tx_finl/rows/acc_coinbase_reward.lisp | 25 ++++++++++++++ .../tx_finl/rows/acc_sender_gas_refund.lisp | 25 ++++++++++++++ hub/constraints/tx_finl/rows/transaction.lisp | 17 ++++++++++ hub/constraints/tx_finl/shorthands.lisp | 34 +++++++++++++++++++ 6 files changed, 122 insertions(+), 3 deletions(-) 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 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/tx_finl/peeking.lisp b/hub/constraints/tx_finl/peeking.lisp new file mode 100644 index 00000000..b548b36a --- /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-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..5b87fdb3 --- /dev/null +++ b/hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp @@ -0,0 +1,25 @@ +(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 + (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---finalization tx-finl---row-offset---ACC---coinbase-reward + 0))) 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..c0a0e616 --- /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---finalization tx-finl---row-offset---ACC---sender-gas-refund + 1))) 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..a8542f89 --- /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-init---row-offset---TXN)) +(defun (tx-finl---sender-address-lo) (shift transaction/FROM_ADDRESS_LO tx-init---row-offset---TXN)) +(defun (tx-finl---recipient-address-hi) (shift transaction/TO_ADDRESS_HI tx-init---row-offset---TXN)) +(defun (tx-finl---recipient-address-lo) (shift transaction/TO_ADDRESS_LO tx-init---row-offset---TXN)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (tx-finl---effective-gas-price) (shift transaction/GAS_PRICE tx-init---row-offset---TXN)) +(defun (tx-finl---effective-gas-refund) (shift transaction/REFUND_EFFECTIVE tx-init---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-init---row-offset---TXN)) +(defun (tx-finl---gas-limit) (shift transaction/GAS_LIMIT tx-init---row-offset---TXN)) +(defun (tx-finl---coinbase-reward) (* (- (tx-finl---gas-limit) (tx-finl---effective-gas-price)) (tx-finl---priority-fee-per-gas))) From dcb72af2aec3c3ac8f057a352e5b3115e048f95e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sun, 1 Dec 2024 22:55:56 +0700 Subject: [PATCH 5/6] fix: make it compile --- hub/constraints/generalities/revert_data_specific.lisp | 9 ++++++++- hub/constraints/tx_finl/peeking.lisp | 2 +- hub/constraints/tx_finl/shorthands.lisp | 4 ++-- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/hub/constraints/generalities/revert_data_specific.lisp b/hub/constraints/generalities/revert_data_specific.lisp index 0f1c7100..c22d2997 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/tx_finl/peeking.lisp b/hub/constraints/tx_finl/peeking.lisp index b548b36a..7f6d0b15 100644 --- a/hub/constraints/tx_finl/peeking.lisp +++ b/hub/constraints/tx_finl/peeking.lisp @@ -12,6 +12,6 @@ (defconstraint tx-finl---setting-peeking-flags (:guard (tx-finl---standard-precondition)) (eq! 3 - (+ (shift PEEK_AT_ACCOUNT tx-finl---row-offset---ACC---sender-refund) + (+ (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/shorthands.lisp b/hub/constraints/tx_finl/shorthands.lisp index a8542f89..d9929e66 100644 --- a/hub/constraints/tx_finl/shorthands.lisp +++ b/hub/constraints/tx_finl/shorthands.lisp @@ -22,8 +22,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (tx-finl---sender-address-hi) (shift transaction/FROM_ADDRESS_HI tx-init---row-offset---TXN)) (defun (tx-finl---sender-address-lo) (shift transaction/FROM_ADDRESS_LO tx-init---row-offset---TXN)) -(defun (tx-finl---recipient-address-hi) (shift transaction/TO_ADDRESS_HI tx-init---row-offset---TXN)) -(defun (tx-finl---recipient-address-lo) (shift transaction/TO_ADDRESS_LO tx-init---row-offset---TXN)) +(defun (tx-finl---coinbase-address-hi) (shift transaction/COINBASE_ADDRESS_HI tx-init---row-offset---TXN)) +(defun (tx-finl---coinbase-address-lo) (shift transaction/COINBASE_ADDRESS_LO tx-init---row-offset---TXN)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (tx-finl---effective-gas-price) (shift transaction/GAS_PRICE tx-init---row-offset---TXN)) (defun (tx-finl---effective-gas-refund) (shift transaction/REFUND_EFFECTIVE tx-init---row-offset---TXN)) From d6cb2946a87271b00e521aa4dd4db752e3bf9b7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 2 Dec 2024 12:41:25 +0700 Subject: [PATCH 6/6] fix: added lisp files for TX_FINL --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 79305073..73e8d515 100644 --- a/Makefile +++ b/Makefile @@ -30,6 +30,7 @@ HUB := $(wildcard hub/columns/*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