From 43fe5e89010dcb3465d4f1eb39de0ac4bea01d36 Mon Sep 17 00:00:00 2001 From: amkCha <29160563+amkCha@users.noreply.github.com> Date: Mon, 15 Dec 2025 16:29:48 +0100 Subject: [PATCH 1/2] increase GAS_LIMIT size for Prague --- Makefile | 4 +- hub/prague/columns/transaction.lisp | 10 +- rlptxn/cancun/columns/transaction.lisp | 2 +- rlptxn/osaka/columns/computation.lisp | 27 ++++ rlptxn/osaka/columns/shared.lisp | 54 ++++++++ rlptxn/osaka/columns/transaction.lisp | 21 +++ rlptxn/osaka/constants.lisp | 7 + .../constraints/generalities/aux_ccc_k.lisp | 15 ++ .../generalities/byte_size_countdown.lisp | 19 +++ .../constraints/generalities/constancies.lisp | 12 ++ .../constraints/generalities/counter.lisp | 19 +++ .../generalities/finalization.lisp | 7 + .../constraints/generalities/indexes.lisp | 19 +++ .../constraints/generalities/lc_lt_lx.lisp | 56 ++++++++ .../generalities/miscellanous.lisp | 15 ++ .../generalities/perspective_flag_sum.lisp | 43 ++++++ .../constraints/generalities/phase_end.lisp | 25 ++++ .../constraints/generalities/phase_flag.lisp | 25 ++++ .../generalities/phase_transitions.lisp | 130 ++++++++++++++++++ .../generalities/requires_evm.lisp | 4 + .../transaction_type_rlp_components.lisp | 62 +++++++++ .../constraints/generalities/type_k.lisp | 25 ++++ .../generalities/user_txn_number.lisp | 7 + .../phase/access_list/access_list_bits.lisp | 13 ++ .../phase/access_list/address_constancy.lisp | 19 +++ .../AL_RLP_length_countdown_constraints.lisp | 14 ++ ...item_RLP_length_countdown_constraints.lisp | 20 +++ ...ccess_list_item_countdown_constraints.lisp | 22 +++ .../storage_key_countdown_constraint.lisp | 22 +++ ...torage_key_list_countdown_constraints.lisp | 18 +++ .../phase/access_list/legal_transitions.lisp | 43 ++++++ .../phase/access_list/shorthands.lisp | 36 +++++ .../sub_phases/RLP-ization_of_address.lisp | 7 + ...LP-ization_of_prefix_access_list_item.lisp | 8 ++ ...ion_of_prefix_of_the_full_access_list.lisp | 26 ++++ .../RLP-ization_of_storage_key_list.lisp | 30 ++++ .../RLP-ization_of_storage_keys.lisp | 28 ++++ .../access_list/sub_phases/finalization.lisp | 19 +++ rlptxn/osaka/constraints/phase/beta.lisp | 44 ++++++ rlptxn/osaka/constraints/phase/data/limb.lisp | 34 +++++ .../osaka/constraints/phase/data/prefix.lisp | 40 ++++++ .../constraints/phase/data/shorthands.lisp | 7 + .../constraints/phase/global_rlp_prefix.lisp | 50 +++++++ rlptxn/osaka/constraints/phase/integer.lisp | 47 +++++++ rlptxn/osaka/constraints/phase/to.lisp | 28 ++++ .../specialized/compound_address.lisp | 25 ++++ .../compound_byte_string_prefix.lisp | 55 ++++++++ .../specialized/compound_bytes32.lisp | 25 ++++ .../specialized/compound_integer.lisp | 47 +++++++ .../limb_membership_constraints.lisp | 16 +++ .../constraints/specialized/limb_setting.lisp | 22 +++ .../specialized/rlputils_calls.lisp | 49 +++++++ .../osaka/lookups/rlptxn_into_blockdata.lisp | 16 +++ rlptxn/osaka/lookups/rlptxn_into_hub.lisp | 38 +++++ .../osaka/lookups/rlptxn_into_rlputils.lisp | 32 +++++ rlptxn/osaka/lookups/rlptxn_into_rom.lisp | 24 ++++ rlptxn/osaka/lookups/rlptxn_into_trm.lisp | 16 +++ rlptxn/osaka/lookups/rlptxn_into_txndata.lisp | 59 ++++++++ .../osaka/prover/prover_columns_corset.lisp | 33 +++++ txndata/prague/columns/hub_view.lisp | 10 +- txndata/prague/columns/rlp_view.lisp | 2 +- 61 files changed, 1639 insertions(+), 13 deletions(-) create mode 100644 rlptxn/osaka/columns/computation.lisp create mode 100644 rlptxn/osaka/columns/shared.lisp create mode 100644 rlptxn/osaka/columns/transaction.lisp create mode 100644 rlptxn/osaka/constants.lisp create mode 100644 rlptxn/osaka/constraints/generalities/aux_ccc_k.lisp create mode 100644 rlptxn/osaka/constraints/generalities/byte_size_countdown.lisp create mode 100644 rlptxn/osaka/constraints/generalities/constancies.lisp create mode 100644 rlptxn/osaka/constraints/generalities/counter.lisp create mode 100644 rlptxn/osaka/constraints/generalities/finalization.lisp create mode 100644 rlptxn/osaka/constraints/generalities/indexes.lisp create mode 100644 rlptxn/osaka/constraints/generalities/lc_lt_lx.lisp create mode 100644 rlptxn/osaka/constraints/generalities/miscellanous.lisp create mode 100644 rlptxn/osaka/constraints/generalities/perspective_flag_sum.lisp create mode 100644 rlptxn/osaka/constraints/generalities/phase_end.lisp create mode 100644 rlptxn/osaka/constraints/generalities/phase_flag.lisp create mode 100644 rlptxn/osaka/constraints/generalities/phase_transitions.lisp create mode 100644 rlptxn/osaka/constraints/generalities/requires_evm.lisp create mode 100644 rlptxn/osaka/constraints/generalities/transaction_type_rlp_components.lisp create mode 100644 rlptxn/osaka/constraints/generalities/type_k.lisp create mode 100644 rlptxn/osaka/constraints/generalities/user_txn_number.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/access_list_bits.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/address_constancy.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_RLP_length_countdown_constraints.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_item_RLP_length_countdown_constraints.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/countdown_constraints/access_list_item_countdown_constraints.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_countdown_constraint.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_list_countdown_constraints.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/legal_transitions.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/shorthands.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_address.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_access_list_item.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_of_the_full_access_list.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_key_list.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_keys.lisp create mode 100644 rlptxn/osaka/constraints/phase/access_list/sub_phases/finalization.lisp create mode 100644 rlptxn/osaka/constraints/phase/beta.lisp create mode 100644 rlptxn/osaka/constraints/phase/data/limb.lisp create mode 100644 rlptxn/osaka/constraints/phase/data/prefix.lisp create mode 100644 rlptxn/osaka/constraints/phase/data/shorthands.lisp create mode 100644 rlptxn/osaka/constraints/phase/global_rlp_prefix.lisp create mode 100644 rlptxn/osaka/constraints/phase/integer.lisp create mode 100644 rlptxn/osaka/constraints/phase/to.lisp create mode 100644 rlptxn/osaka/constraints/specialized/compound_address.lisp create mode 100644 rlptxn/osaka/constraints/specialized/compound_byte_string_prefix.lisp create mode 100644 rlptxn/osaka/constraints/specialized/compound_bytes32.lisp create mode 100644 rlptxn/osaka/constraints/specialized/compound_integer.lisp create mode 100644 rlptxn/osaka/constraints/specialized/limb_membership_constraints.lisp create mode 100644 rlptxn/osaka/constraints/specialized/limb_setting.lisp create mode 100644 rlptxn/osaka/constraints/specialized/rlputils_calls.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_blockdata.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_hub.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_rlputils.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_rom.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_trm.lisp create mode 100644 rlptxn/osaka/lookups/rlptxn_into_txndata.lisp create mode 100644 rlptxn/osaka/prover/prover_columns_corset.lisp diff --git a/Makefile b/Makefile index c3a3cb030..6a27db842 100644 --- a/Makefile +++ b/Makefile @@ -73,7 +73,9 @@ RLP_ADDR := rlpaddr RLP_TXN_LONDON := rlptxn/london RLP_TXN_CANCUN := rlptxn/cancun RLP_TXN_PRAGUE := rlptxn/cancun +RLP_TXN_OSAKA := rlptxn/osaka # TODO: update for Prague v2 + add RLP_AUTH +# only difference between cancun and prague is the size of GAS_LIMIT (i25 vs i32) RLP_TXN_RCPT := rlptxrcpt @@ -214,7 +216,7 @@ ZKEVM_MODULES_OSAKA := ${ZKEVM_MODULES_COMMON} \ ${MMU_OSAKA} \ ${MXP_CANCUN} \ ${OOB_OSAKA} \ - ${RLP_TXN_PRAGUE} \ + ${RLP_TXN_OSAKA} \ ${RLP_UTILS_CANCUN} \ ${TRM_OSAKA} \ ${TXN_DATA_OSAKA} diff --git a/hub/prague/columns/transaction.lisp b/hub/prague/columns/transaction.lisp index 0d1bb83f5..e2b4b37f7 100644 --- a/hub/prague/columns/transaction.lisp +++ b/hub/prague/columns/transaction.lisp @@ -23,8 +23,8 @@ ( IS_TYPE2 :binary ) ;; gas related - ( GAS_LIMIT :i25 ) - ( GAS_INITIALLY_AVAILABLE :i25 ) + ( GAS_LIMIT :i33 ) + ( GAS_INITIALLY_AVAILABLE :i33 ) ( GAS_PRICE :i64 ) ( PRIORITY_FEE_PER_GAS :i64 ) ( BASEFEE :i64 ) ;; in Linea London this is hard-coded to 7 ... but in the reference tests this may be much larger @@ -35,9 +35,9 @@ ;; end of transaction predictions ( STATUS_CODE :binary ) - ( GAS_LEFTOVER :i25 ) - ( REFUND_COUNTER_INFINITY :i25 ) - ( REFUND_EFFECTIVE :i25 ) + ( GAS_LEFTOVER :i33 ) + ( REFUND_COUNTER_INFINITY :i33 ) + ( REFUND_EFFECTIVE :i33 ) ;; coinbase related ( COINBASE_ADDRESS_HI :i32 ) diff --git a/rlptxn/cancun/columns/transaction.lisp b/rlptxn/cancun/columns/transaction.lisp index d7f5249a9..471ec0d43 100644 --- a/rlptxn/cancun/columns/transaction.lisp +++ b/rlptxn/cancun/columns/transaction.lisp @@ -10,7 +10,7 @@ ( GAS_PRICE :i64 ) ( MAX_PRIORITY_FEE_PER_GAS :i64 ) ( MAX_FEE_PER_GAS :i64 ) - ( GAS_LIMIT :i25 ) + ( GAS_LIMIT :i33 ) ( TO_HI :i32 ) ( TO_LO :i128 ) ( VALUE :i96 ) diff --git a/rlptxn/osaka/columns/computation.lisp b/rlptxn/osaka/columns/computation.lisp new file mode 100644 index 000000000..ddb39547c --- /dev/null +++ b/rlptxn/osaka/columns/computation.lisp @@ -0,0 +1,27 @@ +(module rlptxn) + +(defperspective cmp + ;; selector + CMP + ( + ( LIMB :i128 ) + ( LIMB_SIZE :i8 ) + ( TRM_FLAG :binary ) + ( RLPUTILS_FLAG :binary ) + ( RLPUTILS_INST :i8 ) + ( EXO_DATA_1 :i128 ) + ( EXO_DATA_2 :i128 ) + ( EXO_DATA_3 :binary ) + ( EXO_DATA_4 :binary ) + ( EXO_DATA_5 :binary ) + ( EXO_DATA_6 :i128 ) + ( EXO_DATA_7 :i128 ) + ( EXO_DATA_8 :i8 ) + ( AUX_CCC_1 :i16 ) + ( AUX_CCC_2 :i16 ) + ( AUX_CCC_3 :i16 ) + ( AUX_CCC_4 :i32 ) + ( AUX_CCC_5 :i128 ) + ( AUX_1 :i24 ) + ( AUX_2 :i24 ) + )) diff --git a/rlptxn/osaka/columns/shared.lisp b/rlptxn/osaka/columns/shared.lisp new file mode 100644 index 000000000..1bdf8caf4 --- /dev/null +++ b/rlptxn/osaka/columns/shared.lisp @@ -0,0 +1,54 @@ +(module rlptxn) + +(defcolumns + ;; ( USER_TXN_NUMBER :i24 ) ;; defcomputed column + ( TXN :binary@prove ) + ( CMP :binary@prove ) + ( LIMB_CONSTRUCTED :binary@prove ) + ( LT :binary@prove ) + ( LX :binary@prove ) + ;; ( INDEX_LT :i32 ) ;; defcomputed column + ;; ( INDEX_LX :i32 ) ;; defcomputed column + ( LT_BYTE_SIZE_COUNTDOWN :i32 ) + ( LX_BYTE_SIZE_COUNTDOWN :i32 ) + ;; ( TO_HASH_BY_PROVER :binary ) ;; defcomputed column + ( CODE_FRAGMENT_INDEX :i24 ) + ( TYPE_0 :binary@prove ) + ( TYPE_1 :binary@prove ) + ( TYPE_2 :binary@prove ) + ;; ( TYPE_3 :binary@prove ) + ;; ( TYPE_4 :binary@prove ) + ( IS_RLP_PREFIX :binary@prove ) + ( IS_CHAIN_ID :binary@prove ) + ( IS_NONCE :binary@prove ) + ( IS_GAS_PRICE :binary@prove ) + ( IS_GAS_LIMIT :binary@prove ) + ( IS_TO :binary@prove ) + ( IS_VALUE :binary@prove ) + ( IS_DATA :binary@prove ) + ( IS_ACCESS_LIST :binary@prove ) + ( IS_BETA :binary@prove ) + ( IS_MAX_PRIORITY_FEE_PER_GAS :binary@prove ) + ( IS_MAX_FEE_PER_GAS :binary@prove ) + ( IS_Y :binary@prove ) + ( IS_R :binary@prove ) + ( IS_S :binary@prove ) + ;; ( PHASE_END :binary ) ;; defcomputed column + ( CT :i32 ) ;; Linea call data is capped at 120kB < 2**17 limbs = 2**13 bytes + ( CT_MAX :i32 ) ;; i16 is not enough for ref tests + ;; ( DONE :binary ) ;; defcomputed column + ( REPLAY_PROTECTION :binary@prove ) + ( Y_PARITY :binary@prove ) + ( REQUIRES_EVM_EXECUTION :binary ) + ( IS_DEPLOYMENT :binary ) + ( IS_PREFIX_OF_ACCESS_LIST_ITEM :binary@prove ) + ( IS_PREFIX_OF_STORAGE_KEY_LIST :binary@prove ) + ( IS_ACCESS_LIST_ADDRESS :binary@prove ) + ( IS_ACCESS_LIST_STORAGE_KEY :binary@prove ) + ) + +;; aliases +(defalias + LC LIMB_CONSTRUCTED + CFI CODE_FRAGMENT_INDEX + ) diff --git a/rlptxn/osaka/columns/transaction.lisp b/rlptxn/osaka/columns/transaction.lisp new file mode 100644 index 000000000..d7f5249a9 --- /dev/null +++ b/rlptxn/osaka/columns/transaction.lisp @@ -0,0 +1,21 @@ +(module rlptxn) + +(defperspective txn + ;; selector + TXN + ( + ( TX_TYPE :i8 ) + ( CHAIN_ID :i64 ) + ( NONCE :i64 ) + ( GAS_PRICE :i64 ) + ( MAX_PRIORITY_FEE_PER_GAS :i64 ) + ( MAX_FEE_PER_GAS :i64 ) + ( GAS_LIMIT :i25 ) + ( TO_HI :i32 ) + ( TO_LO :i128 ) + ( VALUE :i96 ) + ( NUMBER_OF_ZERO_BYTES :i32 ) + ( NUMBER_OF_NONZERO_BYTES :i32 ) + ( NUMBER_OF_PREWARMED_ADDRESSES :i24 ) + ( NUMBER_OF_PREWARMED_STORAGE_KEYS :i24 ) + )) diff --git a/rlptxn/osaka/constants.lisp b/rlptxn/osaka/constants.lisp new file mode 100644 index 000000000..60bb33f50 --- /dev/null +++ b/rlptxn/osaka/constants.lisp @@ -0,0 +1,7 @@ +(module rlptxn) + +(defconst +RLP_TXN_CT_MAX_INTEGER 2 +RLP_TXN_CT_MAX_BYTES32 2 +RLP_TXN_CT_MAX_ADDRESS 2 +) \ No newline at end of file diff --git a/rlptxn/osaka/constraints/generalities/aux_ccc_k.lisp b/rlptxn/osaka/constraints/generalities/aux_ccc_k.lisp new file mode 100644 index 000000000..bde84994e --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/aux_ccc_k.lisp @@ -0,0 +1,15 @@ +(module rlptxn) + +(defconstraint counter-constancies-for-the-AUX_CCC_k-columns () + (begin + (counter-constant cmp/AUX_CCC_1 CT) + (counter-constant cmp/AUX_CCC_2 CT) + (counter-constant cmp/AUX_CCC_3 CT) + (counter-constant cmp/AUX_CCC_4 CT) + (counter-constant cmp/AUX_CCC_5 CT))) + + + + + + diff --git a/rlptxn/osaka/constraints/generalities/byte_size_countdown.lisp b/rlptxn/osaka/constraints/generalities/byte_size_countdown.lisp new file mode 100644 index 000000000..15742df26 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/byte_size_countdown.lisp @@ -0,0 +1,19 @@ +(module rlptxn) + +(defconstraint byte-size-countdown-update-constraints () + (if-zero IS_RLP_PREFIX + (begin + (eq! LT_BYTE_SIZE_COUNTDOWN + (- (prev LT_BYTE_SIZE_COUNTDOWN) + (* LC LT cmp/LIMB_SIZE))) + (eq! LX_BYTE_SIZE_COUNTDOWN + (- (prev LX_BYTE_SIZE_COUNTDOWN) + (* LC LX cmp/LIMB_SIZE)))))) + +(defconstraint byte-size-countdown-finalization-constraints () + (if-not-zero (* IS_S PHASE_END) + (begin + (vanishes! LT_BYTE_SIZE_COUNTDOWN) + (vanishes! LX_BYTE_SIZE_COUNTDOWN)))) + +(defcomputedcolumn (TO_HASH_BY_PROVER :binary) (* LC LX)) diff --git a/rlptxn/osaka/constraints/generalities/constancies.lisp b/rlptxn/osaka/constraints/generalities/constancies.lisp new file mode 100644 index 000000000..9fe984b9d --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/constancies.lisp @@ -0,0 +1,12 @@ +(module rlptxn) + +(defun (transaction-constant col) + (if-not (== USER_TXN_NUMBER (+ 1 (prev USER_TXN_NUMBER))) + (remained-constant! col))) + +(defconstraint transaction-constancies () + (begin + (transaction-constant CFI) + (transaction-constant REPLAY_PROTECTION) + (transaction-constant Y_PARITY) + )) diff --git a/rlptxn/osaka/constraints/generalities/counter.lisp b/rlptxn/osaka/constraints/generalities/counter.lisp new file mode 100644 index 000000000..7dc7db5f6 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/counter.lisp @@ -0,0 +1,19 @@ +(module rlptxn) + +(defconstraint counter-constancy-of-ct-max () (counter-constant CT_MAX CT)) + +(defconstraint automatic-vanishing-of-counters-outside-of-computation-rows () + (if-zero CMP + (begin + (vanishes! CT) + (vanishes! CT_MAX)))) + +(defconstraint ct-loop () + (if (== CT CT_MAX) + (vanishes! (next CT)) + (will-inc! CT 1))) + +(defcomputedcolumn (DONE :binary) + (if (== CT CT_MAX) + (phase-flag-sum) + 0)) diff --git a/rlptxn/osaka/constraints/generalities/finalization.lisp b/rlptxn/osaka/constraints/generalities/finalization.lisp new file mode 100644 index 000000000..6e26699fe --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/finalization.lisp @@ -0,0 +1,7 @@ +(module rlptxn) + +(defconstraint finalization (:domain {-1}) + (if-not-zero USER_TXN_NUMBER + (begin + (eq! PHASE_END 1) + (eq! IS_S 1)))) \ No newline at end of file diff --git a/rlptxn/osaka/constraints/generalities/indexes.lisp b/rlptxn/osaka/constraints/generalities/indexes.lisp new file mode 100644 index 000000000..45d449dcd --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/indexes.lisp @@ -0,0 +1,19 @@ +(module rlptxn) + +;;note: :i16 is not enough for ref tests + +(defcomputedcolumn (INDEX_LT :i32 :fwd) + (if-not-zero (is-first-row-of-transaction) + ;; initialization + 0 + ;; update + (+ (prev INDEX_LT) (* (prev LC) (prev LT))) + )) + +(defcomputedcolumn (INDEX_LX :i32 :fwd) + (if-not-zero (is-first-row-of-transaction) + ;; initialization + 0 + ;; update + (+ (prev INDEX_LX) (* (prev LC) (prev LX))) + )) \ No newline at end of file diff --git a/rlptxn/osaka/constraints/generalities/lc_lt_lx.lisp b/rlptxn/osaka/constraints/generalities/lc_lt_lx.lisp new file mode 100644 index 000000000..4ca20eaae --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/lc_lt_lx.lisp @@ -0,0 +1,56 @@ +(module rlptxn) + +(defun (limb-unconditionally-partakes-in-LX) + (force-bin (+ + ;; IS_RLP_PREFIX + IS_CHAIN_ID + IS_NONCE + IS_GAS_PRICE + IS_MAX_PRIORITY_FEE_PER_GAS + IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + IS_TO + IS_VALUE + IS_DATA + IS_ACCESS_LIST + ;; IS_BETA + ;; IS_Y + ;; IS_R + ;; IS_S + ))) + +(defun (limb-unconditionally-partakes-in-LT) +(force-bin (+ + (limb-unconditionally-partakes-in-LX) + IS_Y + IS_R + IS_S + ))) + +;; ;; I've added them to the :binary@prove columns +;; (defproperty lc-lt-lx-binaries +;; (begin +;; (is-binary LC) +;; (is-binary LX) +;; (is-binary LT))) + +(defconstraint counter-constancies-for-LT-and-LX () + (begin + (counter-constant LT CT) + (counter-constant LX CT) + )) + +(defconstraint setting-LT-and-LX-for-most-phases () + (if-not-zero (limb-unconditionally-partakes-in-LT) + (begin + (eq! LT (limb-unconditionally-partakes-in-LT)) + (eq! LX (limb-unconditionally-partakes-in-LX))))) + +(defconstraint LC-may-only-turn-on-along-computation-rows () + (if-zero CMP (vanishes! LC))) + +(defproperty LT-and-LX-automatically-vanish-on-padding-rows + (if-zero (phase-flag-sum) + (begin + (vanishes! LT) + (vanishes! LX)))) diff --git a/rlptxn/osaka/constraints/generalities/miscellanous.lisp b/rlptxn/osaka/constraints/generalities/miscellanous.lisp new file mode 100644 index 000000000..faa7d3a9d --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/miscellanous.lisp @@ -0,0 +1,15 @@ +(module rlptxn) + +;; binarity is taken care of via :binary@prove + +;; transaction-constancy is taken care of in eponymous section + +(defconstraint replay-protection-means-no-chain-id () + (if-not-zero TXN + (if-not-zero txn/CHAIN_ID + (eq! REPLAY_PROTECTION 1) + (eq! REPLAY_PROTECTION 0)))) + +(defconstraint only-frontier-tx-are-not-replay-protection () + (if-not-zero TXN + (if-zero TYPE_0 (eq! REPLAY_PROTECTION 1)))) diff --git a/rlptxn/osaka/constraints/generalities/perspective_flag_sum.lisp b/rlptxn/osaka/constraints/generalities/perspective_flag_sum.lisp new file mode 100644 index 000000000..a5e165a7d --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/perspective_flag_sum.lisp @@ -0,0 +1,43 @@ +(module rlptxn) + +(defun (persp-flag-sum) (force-bin (+ TXN CMP))) + +(defun (about-to-enter-new-phase) + (force-bin (+ + (* (- 1 IS_RLP_PREFIX ) (next IS_RLP_PREFIX )) + (* (- 1 IS_CHAIN_ID ) (next IS_CHAIN_ID )) + (* (- 1 IS_NONCE ) (next IS_NONCE )) + (* (- 1 IS_GAS_PRICE ) (next IS_GAS_PRICE )) + (* (- 1 IS_MAX_PRIORITY_FEE_PER_GAS ) (next IS_MAX_PRIORITY_FEE_PER_GAS )) + (* (- 1 IS_MAX_FEE_PER_GAS ) (next IS_MAX_FEE_PER_GAS )) + (* (- 1 IS_GAS_LIMIT ) (next IS_GAS_LIMIT )) + (* (- 1 IS_TO ) (next IS_TO )) + (* (- 1 IS_VALUE ) (next IS_VALUE )) + (* (- 1 IS_DATA ) (next IS_DATA )) + (* (- 1 IS_ACCESS_LIST ) (next IS_ACCESS_LIST )) + (* (- 1 IS_BETA ) (next IS_BETA )) + (* (- 1 IS_Y ) (next IS_Y )) + (* (- 1 IS_R ) (next IS_R )) + (* (- 1 IS_S ) (next IS_S )) + ))) + +(defconstraint persp-flag-is-phase-flag () (eq! (persp-flag-sum) (phase-flag-sum))) + +(defconstraint every-phase-starts-with-a-transaction-row () (eq! (about-to-enter-new-phase) (next TXN))) + +(defconstraint computation-follows-transaction-row () (if-not-zero TXN (will-eq! CMP 1))) + + +(defproperty outside-of-padding-rows-entering-a-new-phase-coincides-with-exiting-the-current-one + (if-not-zero (phase-flag-sum) + (eq! (about-to-enter-new-phase) (about-to-exit-current-phase)))) + +;; This constraint isn't in the spec AFAICT +;; indeed the spec doesn't contain the +;; +;; upcoming_phase_transition +;; +;; shorthand. +(defproperty prop-outside-of-padding-rows-entering-a-new-phase-coincides-with-exiting-the-current-one + (if-not-zero (phase-flag-sum) + (eq! (about-to-enter-new-phase) (upcoming-phase-transition)))) diff --git a/rlptxn/osaka/constraints/generalities/phase_end.lisp b/rlptxn/osaka/constraints/generalities/phase_end.lisp new file mode 100644 index 000000000..15952ee88 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/phase_end.lisp @@ -0,0 +1,25 @@ +(module rlptxn) + +(defun (about-to-exit-current-phase) + (force-bin (+ + (* IS_RLP_PREFIX (- 1 (next IS_RLP_PREFIX ))) + (* IS_CHAIN_ID (- 1 (next IS_CHAIN_ID ))) + (* IS_NONCE (- 1 (next IS_NONCE ))) + (* IS_GAS_PRICE (- 1 (next IS_GAS_PRICE ))) + (* IS_MAX_PRIORITY_FEE_PER_GAS (- 1 (next IS_MAX_PRIORITY_FEE_PER_GAS ))) + (* IS_MAX_FEE_PER_GAS (- 1 (next IS_MAX_FEE_PER_GAS ))) + (* IS_GAS_LIMIT (- 1 (next IS_GAS_LIMIT ))) + (* IS_TO (- 1 (next IS_TO ))) + (* IS_VALUE (- 1 (next IS_VALUE ))) + (* IS_DATA (- 1 (next IS_DATA ))) + (* IS_ACCESS_LIST (- 1 (next IS_ACCESS_LIST ))) + (* IS_BETA (- 1 (next IS_BETA ))) + (* IS_Y (- 1 (next IS_Y ))) + (* IS_R (- 1 (next IS_R ))) + (* IS_S (- 1 (next IS_S ))) + ))) + +(defproperty about-to-exit-current-phase-shorthand-is-binary + (is-binary (about-to-exit-current-phase))) + +(defcomputedcolumn (PHASE_END :binary) (about-to-exit-current-phase)) diff --git a/rlptxn/osaka/constraints/generalities/phase_flag.lisp b/rlptxn/osaka/constraints/generalities/phase_flag.lisp new file mode 100644 index 000000000..c37a04545 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/phase_flag.lisp @@ -0,0 +1,25 @@ +(module rlptxn) + +(defun (phase-flag-sum) + (force-bin + (+ IS_RLP_PREFIX + IS_CHAIN_ID + IS_NONCE + IS_GAS_PRICE + IS_MAX_PRIORITY_FEE_PER_GAS + IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + IS_TO + IS_VALUE + IS_DATA + IS_ACCESS_LIST + IS_BETA + IS_Y + IS_R + IS_S + ))) + +(defconstraint the-phase-flag-vanishes-precisely-along-padding-rows () + (if-zero USER_TXN_NUMBER + (vanishes! (phase-flag-sum)) + (eq! (phase-flag-sum) 1))) diff --git a/rlptxn/osaka/constraints/generalities/phase_transitions.lisp b/rlptxn/osaka/constraints/generalities/phase_transitions.lisp new file mode 100644 index 000000000..9b3a7ebe0 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/phase_transitions.lisp @@ -0,0 +1,130 @@ +(module rlptxn) + +(defun (upcoming-phase-transition-type-0) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_NONCE )) + ;; (* IS_CHAIN_ID (next IS_CHAIN_ID )) + (* IS_NONCE (next IS_GAS_PRICE )) + (* IS_GAS_PRICE (next IS_GAS_LIMIT )) + ;; (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_PRIORITY_FEE_PER_GAS)) + ;; (* IS_MAX_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_GAS_LIMIT (next IS_TO )) + (* IS_TO (next IS_VALUE )) + (* IS_VALUE (next IS_DATA )) + (* IS_DATA (next IS_BETA )) + ;; (* IS_ACCESS_LIST (next IS_ACCESS_LIST )) + (* IS_BETA (next IS_R )) + ;; (* IS_Y (next IS_Y )) + (* IS_R (next IS_S )) + (* IS_S (next IS_RLP_PREFIX )) + ))) + +(defun (will-remain-in-same-phase-type-0) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_RLP_PREFIX )) + ;; (* IS_CHAIN_ID (next IS_CHAIN_ID )) + (* IS_NONCE (next IS_NONCE )) + (* IS_GAS_PRICE (next IS_GAS_PRICE )) + ;; (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_PRIORITY_FEE_PER_GAS)) + ;; (* IS_MAX_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_GAS_LIMIT (next IS_GAS_LIMIT )) + (* IS_TO (next IS_TO )) + (* IS_VALUE (next IS_VALUE )) + (* IS_DATA (next IS_DATA )) + ;; (* IS_ACCESS_LIST (next IS_ACCESS_LIST )) + (* IS_BETA (next IS_BETA )) + ;; (* IS_Y (next IS_Y )) + (* IS_R (next IS_R )) + (* IS_S (next IS_S )) + ))) + +(defun (upcoming-phase-transition-type-1) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_CHAIN_ID )) + (* IS_CHAIN_ID (next IS_NONCE )) + (* IS_NONCE (next IS_GAS_PRICE )) + (* IS_GAS_PRICE (next IS_GAS_LIMIT )) + ;; (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_PRIORITY_FEE_PER_GAS)) + ;; (* IS_MAX_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_GAS_LIMIT (next IS_TO )) + (* IS_TO (next IS_VALUE )) + (* IS_VALUE (next IS_DATA )) + (* IS_DATA (next IS_ACCESS_LIST )) + (* IS_ACCESS_LIST (next IS_Y )) + ;; (* IS_BETA (next IS_BETA )) + (* IS_Y (next IS_R )) + (* IS_R (next IS_S )) + (* IS_S (next IS_RLP_PREFIX )) + ))) + +(defun (will-remain-in-same-phase-type-1) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_RLP_PREFIX )) + (* IS_CHAIN_ID (next IS_CHAIN_ID )) + (* IS_NONCE (next IS_NONCE )) + (* IS_GAS_PRICE (next IS_GAS_PRICE )) + ;; (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_PRIORITY_FEE_PER_GAS)) + ;; (* IS_MAX_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_GAS_LIMIT (next IS_GAS_LIMIT )) + (* IS_TO (next IS_TO )) + (* IS_VALUE (next IS_VALUE )) + (* IS_DATA (next IS_DATA )) + (* IS_ACCESS_LIST (next IS_ACCESS_LIST )) + ;; (* IS_BETA (next IS_BETA )) + (* IS_Y (next IS_Y )) + (* IS_R (next IS_R )) + (* IS_S (next IS_S )) + ))) + +(defun (upcoming-phase-transition-type-2) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_CHAIN_ID )) + (* IS_CHAIN_ID (next IS_NONCE )) + (* IS_NONCE (next IS_MAX_PRIORITY_FEE_PER_GAS)) + ;; (* IS_GAS_PRICE (next IS_GAS_LIMITs )) + (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_MAX_FEE_PER_GAS (next IS_GAS_LIMIT )) + (* IS_GAS_LIMIT (next IS_TO )) + (* IS_TO (next IS_VALUE )) + (* IS_VALUE (next IS_DATA )) + (* IS_DATA (next IS_ACCESS_LIST )) + (* IS_ACCESS_LIST (next IS_Y )) + ;; (* IS_BETA (next IS_BETA )) + (* IS_Y (next IS_R )) + (* IS_R (next IS_S )) + (* IS_S (next IS_RLP_PREFIX )) + ))) + +(defun (will-remain-in-same-phase-type-2) + (force-bin (+ + (* IS_RLP_PREFIX (next IS_RLP_PREFIX )) + (* IS_CHAIN_ID (next IS_CHAIN_ID )) + (* IS_NONCE (next IS_NONCE )) + ;; (* IS_GAS_PRICE (next IS_GAS_PRICE )) + (* IS_MAX_PRIORITY_FEE_PER_GAS (next IS_MAX_PRIORITY_FEE_PER_GAS)) + (* IS_MAX_FEE_PER_GAS (next IS_MAX_FEE_PER_GAS )) + (* IS_GAS_LIMIT (next IS_GAS_LIMIT )) + (* IS_TO (next IS_TO )) + (* IS_VALUE (next IS_VALUE )) + (* IS_DATA (next IS_DATA )) + (* IS_ACCESS_LIST (next IS_ACCESS_LIST )) + ;; (* IS_BETA (next IS_BETA )) + (* IS_Y (next IS_Y )) + (* IS_R (next IS_R )) + (* IS_S (next IS_S )) + ))) + +;; this shorthand isn't defined in the spec AFAICT +(defun (upcoming-phase-transition) + (force-bin (+ (* (upcoming-phase-transition-type-0) TYPE_0) + (* (upcoming-phase-transition-type-1) TYPE_1) + (* (upcoming-phase-transition-type-2) TYPE_2)))) + +(defconstraint type-0-phases () + (if-not-zero TYPE_0 (eq! (+ (upcoming-phase-transition-type-0) (will-remain-in-same-phase-type-0)) 1))) + +(defconstraint type-1-phases () + (if-not-zero TYPE_1 (eq! (+ (upcoming-phase-transition-type-1) (will-remain-in-same-phase-type-1)) 1))) + +(defconstraint type-2-phases () + (if-not-zero TYPE_2 (eq! (+ (upcoming-phase-transition-type-2) (will-remain-in-same-phase-type-2)) 1))) diff --git a/rlptxn/osaka/constraints/generalities/requires_evm.lisp b/rlptxn/osaka/constraints/generalities/requires_evm.lisp new file mode 100644 index 000000000..f2f1c43fc --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/requires_evm.lisp @@ -0,0 +1,4 @@ +(module rlptxn) + +(defconstraint transaction-constancies-requires-evm () + (transaction-constant REQUIRES_EVM_EXECUTION)) diff --git a/rlptxn/osaka/constraints/generalities/transaction_type_rlp_components.lisp b/rlptxn/osaka/constraints/generalities/transaction_type_rlp_components.lisp new file mode 100644 index 000000000..0c197d227 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/transaction_type_rlp_components.lisp @@ -0,0 +1,62 @@ +(module rlptxn) + +(defun (RLP-components-of-type-0-transactions) + (+ + IS_RLP_PREFIX + ;; IS_CHAIN_ID + IS_NONCE + IS_GAS_PRICE + ;; IS_MAX_PRIORITY_FEE_PER_GAS + ;; IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + IS_TO + IS_VALUE + IS_DATA + ;; IS_ACCESS_LIST + IS_BETA + ;; IS_Y + IS_R + IS_S + )) + +(defun (RLP-components-of-type-1-transactions) + (+ + IS_RLP_PREFIX + IS_CHAIN_ID + IS_NONCE + IS_GAS_PRICE + ;; IS_MAX_PRIORITY_FEE_PER_GAS + ;; IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + IS_TO + IS_VALUE + IS_DATA + IS_ACCESS_LIST + ;; IS_BETA + IS_Y + IS_R + IS_S + )) + +(defun (RLP-components-of-type-2-transactions) + (+ + IS_RLP_PREFIX + IS_CHAIN_ID + IS_NONCE + ;; IS_GAS_PRICE + IS_MAX_PRIORITY_FEE_PER_GAS + IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + IS_TO + IS_VALUE + IS_DATA + IS_ACCESS_LIST + ;; IS_BETA + IS_Y + IS_R + IS_S + )) + +(defproperty admissible-RLP-components-for-type-0-transactions (if (== TYPE_0 1) (eq! (RLP-components-of-type-0-transactions) 1))) +(defproperty admissible-RLP-components-for-type-1-transactions (if (== TYPE_1 1) (eq! (RLP-components-of-type-1-transactions) 1))) +(defproperty admissible-RLP-components-for-type-2-transactions (if (== TYPE_2 1) (eq! (RLP-components-of-type-2-transactions) 1))) diff --git a/rlptxn/osaka/constraints/generalities/type_k.lisp b/rlptxn/osaka/constraints/generalities/type_k.lisp new file mode 100644 index 000000000..43ebafbcc --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/type_k.lisp @@ -0,0 +1,25 @@ +(module rlptxn) + +(defun (tx-type-flag-sum) + (force-bin (+ + TYPE_0 + TYPE_1 + TYPE_2))) + +(defun (tx-type-wght-sum) + (+ + (* 0 TYPE_0 ) + (* 1 TYPE_1 ) + (* 2 TYPE_2 ))) + +(defconstraint transaction-constancies-of-type-k-columns () + (begin + (transaction-constant TYPE_0) + (transaction-constant TYPE_1) + (transaction-constant TYPE_2) + )) + +(defconstraint tx-type-flag-sum-equals-phase-flag-sum () (eq! (tx-type-flag-sum) (phase-flag-sum))) + +(defconstraint decoding-type () + (if-not-zero TXN (eq! txn/TX_TYPE (tx-type-wght-sum)))) diff --git a/rlptxn/osaka/constraints/generalities/user_txn_number.lisp b/rlptxn/osaka/constraints/generalities/user_txn_number.lisp new file mode 100644 index 000000000..666b2ba70 --- /dev/null +++ b/rlptxn/osaka/constraints/generalities/user_txn_number.lisp @@ -0,0 +1,7 @@ +(module rlptxn) + +(defun (is-first-row-of-transaction) (force-bin (* (- 1 (prev IS_RLP_PREFIX)) IS_RLP_PREFIX))) + +(defconstraint user-tx-num-vanishes-in-padding (:domain {0}) (vanishes! USER_TXN_NUMBER)) + +(defcomputedcolumn (USER_TXN_NUMBER :i16 :fwd) (+ (prev USER_TXN_NUMBER) (is-first-row-of-transaction))) \ No newline at end of file diff --git a/rlptxn/osaka/constraints/phase/access_list/access_list_bits.lisp b/rlptxn/osaka/constraints/phase/access_list/access_list_bits.lisp new file mode 100644 index 000000000..9cf339076 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/access_list_bits.lisp @@ -0,0 +1,13 @@ +(module rlptxn) + +(defconstraint ct-constancies-of-access-list-subphase () + (begin + (counter-constant IS_PREFIX_OF_ACCESS_LIST_ITEM CT) + (counter-constant IS_PREFIX_OF_STORAGE_KEY_LIST CT) + (counter-constant IS_ACCESS_LIST_ADDRESS CT) + (counter-constant IS_ACCESS_LIST_STORAGE_KEY CT))) + +(defconstraint access-list-flag-exclusivity () + (eq! (is-access-list-data) + (* (prev CMP) CMP IS_ACCESS_LIST))) + diff --git a/rlptxn/osaka/constraints/phase/access_list/address_constancy.lisp b/rlptxn/osaka/constraints/phase/access_list/address_constancy.lisp new file mode 100644 index 000000000..4c08e0ca9 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/address_constancy.lisp @@ -0,0 +1,19 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T address constancy conditions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; address constancy +(defconstraint access-list---address-constancy-condition () + (if-not-zero (force-bin (+ IS_ACCESS_LIST_ADDRESS + IS_PREFIX_OF_STORAGE_KEY_LIST + IS_ACCESS_LIST_STORAGE_KEY)) + (begin + (remained-constant! (rlptxn---access-list---address-hi)) + (remained-constant! (rlptxn---access-list---address-lo))))) + diff --git a/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_RLP_length_countdown_constraints.lisp b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_RLP_length_countdown_constraints.lisp new file mode 100644 index 000000000..757d952b3 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_RLP_length_countdown_constraints.lisp @@ -0,0 +1,14 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T AL_RLP_length_coundown constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint rlptxn---access-list---AL-RLP-length-countdown---update () + (if-not-zero (is-access-list-data) + (did-dec! (rlptxn---access-list---AL-RLP-length-countdown) + (* LC cmp/LIMB_SIZE)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_item_RLP_length_countdown_constraints.lisp b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_item_RLP_length_countdown_constraints.lisp new file mode 100644 index 000000000..4759c2530 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/AL_item_RLP_length_countdown_constraints.lisp @@ -0,0 +1,20 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T AL_item_RLP_length_coundown constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint rlptxn---access-list---AL-item-RLP-length-countdown---update () + (if-not-zero (force-bin (+ IS_ACCESS_LIST_ADDRESS + IS_PREFIX_OF_STORAGE_KEY_LIST + IS_ACCESS_LIST_STORAGE_KEY)) + (did-dec! (rlptxn---access-list---AL-item-RLP-length-countdown) + (* LC cmp/LIMB_SIZE)))) + +(defconstraint rlptxn---access-list---AL-item-RLP-length-countdown---finalization () + (if-not-zero (end-of-tuple-or-end-of-phase) + (vanishes! (rlptxn---access-list---AL-item-RLP-length-countdown)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/access_list_item_countdown_constraints.lisp b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/access_list_item_countdown_constraints.lisp new file mode 100644 index 000000000..734eac353 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/access_list_item_countdown_constraints.lisp @@ -0,0 +1,22 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T access_list_item_countdown constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint rlptxn---access-list-item-countdown---initialization () + (if-not-zero (is-access-list-prefix) + (eq! (rlptxn---access-list---access-list-item-countdown) + (prev txn/NUMBER_OF_PREWARMED_ADDRESSES)))) + +(defun (rlptxn---access-list---new-access-list-item) (* IS_PREFIX_OF_ACCESS_LIST_ITEM + (prev DONE))) + +(defconstraint rlptxn---access-list-item-countdown---update () + (if-not-zero (is-access-list-data) + (did-dec! (rlptxn---access-list---access-list-item-countdown) + (rlptxn---access-list---new-access-list-item)))) + diff --git a/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_countdown_constraint.lisp b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_countdown_constraint.lisp new file mode 100644 index 000000000..8d75f8c07 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_countdown_constraint.lisp @@ -0,0 +1,22 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T storage_key_countdown constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint rlptxn---access-list---storage-key-countdown---initialization () + (if-not-zero (is-access-list-prefix) + (eq! (rlptxn---access-list---storage-key-countdown) + (prev txn/NUMBER_OF_PREWARMED_STORAGE_KEYS)))) + +(defun (start-RLP-izing-new-storage-key) (* IS_ACCESS_LIST_STORAGE_KEY + (prev DONE))) + +(defconstraint rlptxn---access-list---storage-key-countdown---update () + (if-not-zero (is-access-list-data) + (did-dec! (rlptxn---access-list---storage-key-countdown) + (start-RLP-izing-new-storage-key)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_list_countdown_constraints.lisp b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_list_countdown_constraints.lisp new file mode 100644 index 000000000..f3f82799f --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/countdown_constraints/storage_key_list_countdown_constraints.lisp @@ -0,0 +1,18 @@ +(module rlptxn) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.T storage_key_list_countdown constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint rlptxn---access-list---storage-key-list-countdown---update () + (if-not-zero IS_ACCESS_LIST_STORAGE_KEY + (did-dec! (rlptxn---access-list---storage-key-list-countdown) + (prev DONE)))) + +(defconstraint rlptxn---access-list---storage-key-list-countdown---finalization () + (if-not-zero (end-of-tuple-or-end-of-phase) + (vanishes! (rlptxn---access-list---storage-key-list-countdown)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/legal_transitions.lisp b/rlptxn/osaka/constraints/phase/access_list/legal_transitions.lisp new file mode 100644 index 000000000..0a46aa8df --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/legal_transitions.lisp @@ -0,0 +1,43 @@ +(module rlptxn) + +(defconstraint access-list---setting-first-row-after-prefix () + (if-not-zero (is-access-list-prefix) + (eq! (next IS_PREFIX_OF_ACCESS_LIST_ITEM) (next IS_ACCESS_LIST)))) + +(defconstraint access-list---setting-flag-after-rlp-tuple () + (if-not-zero IS_PREFIX_OF_ACCESS_LIST_ITEM + (begin + (eq! (+ (next IS_PREFIX_OF_ACCESS_LIST_ITEM) + (next IS_ACCESS_LIST_ADDRESS)) + 1) + (eq! (next IS_ACCESS_LIST_ADDRESS) + DONE)))) + +(defconstraint access-list---setting-flag-after-address () + (if-not-zero IS_ACCESS_LIST_ADDRESS + (begin + (eq! (+ (next IS_ACCESS_LIST_ADDRESS) + (next IS_PREFIX_OF_STORAGE_KEY_LIST)) + 1) + (eq! (next IS_PREFIX_OF_STORAGE_KEY_LIST) + DONE)))) + +(defconstraint access-list---setting-flag-after-storage-list-list-rlp () + (if-not-zero IS_PREFIX_OF_STORAGE_KEY_LIST + (begin + (eq! (+ (next IS_PREFIX_OF_STORAGE_KEY_LIST) + (next IS_ACCESS_LIST_STORAGE_KEY) + (next IS_PREFIX_OF_ACCESS_LIST_ITEM)) + (next IS_ACCESS_LIST)) + (eq! (+ (next IS_ACCESS_LIST_STORAGE_KEY) + (next IS_PREFIX_OF_ACCESS_LIST_ITEM)) + (* (next IS_ACCESS_LIST) DONE))))) + +(defconstraint access-list---setting-flag-after-storage-key () + (if-not-zero IS_ACCESS_LIST_STORAGE_KEY + (begin + (eq! (+ (next IS_ACCESS_LIST_STORAGE_KEY) + (next IS_PREFIX_OF_ACCESS_LIST_ITEM)) + (next IS_ACCESS_LIST)) + (if-not-zero (next IS_PREFIX_OF_ACCESS_LIST_ITEM) + (eq! DONE 1))))) diff --git a/rlptxn/osaka/constraints/phase/access_list/shorthands.lisp b/rlptxn/osaka/constraints/phase/access_list/shorthands.lisp new file mode 100644 index 000000000..16f80143c --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/shorthands.lisp @@ -0,0 +1,36 @@ +(module rlptxn) + +;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Shorthands I ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (is-access-list-prefix) (* (prev TXN) IS_ACCESS_LIST)) +(defun (is-access-list-data) (force-bin (+ IS_PREFIX_OF_ACCESS_LIST_ITEM + IS_PREFIX_OF_STORAGE_KEY_LIST + IS_ACCESS_LIST_ADDRESS + IS_ACCESS_LIST_STORAGE_KEY + ))) + + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Shorthands II ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (rlptxn---access-list---AL-RLP-length-countdown) cmp/AUX_1) +(defun (rlptxn---access-list---AL-item-RLP-length-countdown) cmp/AUX_2) +(defun (rlptxn---access-list---access-list-item-countdown) cmp/AUX_CCC_1) +(defun (rlptxn---access-list---storage-key-countdown) cmp/AUX_CCC_2) +(defun (rlptxn---access-list---storage-key-list-countdown) cmp/AUX_CCC_3) ;; "" + +;; ;; shorthand defined outside of the module to be accessible in lookups +;; (defun (rlptxn---access-list---address-hi) rlptxn.cmp/AUX_CCC_4) +;; (defun (rlptxn---access-list---address-lo) rlptxn.cmp/AUX_CCC_5) + +(defun (storage-stuff) (force-bin (+ IS_PREFIX_OF_STORAGE_KEY_LIST IS_ACCESS_LIST_STORAGE_KEY))) +(defun (not-storage-stuff) (force-bin (- 1 (storage-stuff)))) +(defun (end-of-tuple-or-end-of-phase) (* (storage-stuff) (next (not-storage-stuff)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_address.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_address.lisp new file mode 100644 index 000000000..cb6b43e72 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_address.lisp @@ -0,0 +1,7 @@ +(module rlptxn) + +(defconstraint access-list---RLP-ization-of-addresses---RLP_UTILS-calls () + (if-not-zero (* IS_ACCESS_LIST_ADDRESS (prev DONE)) + (rlp-compound-constraint---ADDRESS 0 + (rlptxn---access-list---address-hi) + (rlptxn---access-list---address-lo)))) diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_access_list_item.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_access_list_item.lisp new file mode 100644 index 000000000..e68a6f70f --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_access_list_item.lisp @@ -0,0 +1,8 @@ +(module rlptxn) + +(defconstraint access-list---rlp-prefix-of-access-list-items---RLP_UTILS-calls () + (if-not-zero (* IS_PREFIX_OF_ACCESS_LIST_ITEM (prev DONE)) + (rlp-compound-constraint---BYTE_STRING_PREFIX-non-trivial 0 + (rlptxn---access-list---AL-item-RLP-length-countdown) + 1 + 1))) diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_of_the_full_access_list.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_of_the_full_access_list.lisp new file mode 100644 index 000000000..30c611e77 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_prefix_of_the_full_access_list.lisp @@ -0,0 +1,26 @@ +(module rlptxn) + +(defconstraint access-list---rlp-prefix-of-the-full-access-list---RLP_UTILS-call + (:guard (is-access-list-prefix)) + (rlp-compound-constraint---BYTE_STRING_PREFIX-non-trivial 0 + (rlptxn---access-list---AL-RLP-length-countdown) + 1 + 0)) + + +(defconstraint access-list---rlp-prefix-of-the-full-access-list---setting-PHASE_END + (:guard (is-access-list-prefix)) + (eq! PHASE_END + (access-list-is-empty))) + +(defun (access-list-is-non-empty) cmp/EXO_DATA_4) ;; "" +(defun (access-list-is-empty) (- 1 (access-list-is-non-empty))) + +(defproperty access-list---rlp-prefix-of-the-full-access-list---sanity-checks + (if-not-zero (is-access-list-prefix) + (if-zero PHASE_END + (begin + (eq! (next IS_PREFIX_OF_ACCESS_LIST_ITEM) 1) + (eq! (next IS_ACCESS_LIST_ADDRESS) 0) + (eq! (next IS_PREFIX_OF_STORAGE_KEY_LIST) 0) + (eq! (next IS_ACCESS_LIST_STORAGE_KEY) 0))))) diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_key_list.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_key_list.lisp new file mode 100644 index 000000000..216d160df --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_key_list.lisp @@ -0,0 +1,30 @@ +(module rlptxn) + + +(defun (access-list---first-row-of-storage-key-list-processing) (* IS_PREFIX_OF_STORAGE_KEY_LIST + (prev DONE))) + +(defconstraint access-list---RLP-prefix-for-storage-key-lists---calling-RLP_UTILS + (:guard (access-list---first-row-of-storage-key-list-processing)) + (rlp-compound-constraint---BYTE_STRING_PREFIX-non-trivial 0 + (length-of-concatenated-storage-key-RLPs) + 1 + 0)) + +(defun (length-of-concatenated-storage-key-RLPs) (* 33 (rlptxn---access-list---storage-key-list-countdown))) +(defun (storage-key-list-is-nonempty) (force-bin cmp/EXO_DATA_4)) +(defun (storage-key-list-is-empty) (force-bin (- 1 (storage-key-list-is-nonempty)))) ;; "" + +(defconstraint access-list---RLP-prefix-for-storage-key-lists---setting-the-next-step-I + (:guard (access-list---first-row-of-storage-key-list-processing)) + (eq! (next IS_ACCESS_LIST_STORAGE_KEY) + (storage-key-list-is-nonempty))) + +(defconstraint access-list---RLP-prefix-for-storage-key-lists---setting-the-next-step-II + (:guard (access-list---first-row-of-storage-key-list-processing)) + (if-not-zero (storage-key-list-is-empty) + (if-not-zero (rlptxn---access-list---access-list-item-countdown) + (eq! (next IS_PREFIX_OF_ACCESS_LIST_ITEM) 1) + (eq! PHASE_END 1)))) + + diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_keys.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_keys.lisp new file mode 100644 index 000000000..85558111d --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/RLP-ization_of_storage_keys.lisp @@ -0,0 +1,28 @@ +(module rlptxn) + + +(defun (access-list---first-row-of-storage-key-processing) (* IS_ACCESS_LIST_STORAGE_KEY + (prev DONE))) + + +(defconstraint access-list---rlp-ization-of-storage-keys---calling-RLP_UTILS + (:guard (access-list---first-row-of-storage-key-processing)) + (rlp-compound-constraint---BYTES32 0 + (rlptxn---access-list---storage-hi) + (rlptxn---access-list---storage-lo))) + + +(defun (rlptxn---access-list---storage-hi) cmp/EXO_DATA_1) +(defun (rlptxn---access-list---storage-lo) cmp/EXO_DATA_2) ;; "" + + +(defconstraint access-list---rlp-ization-of-storage-keys---setting-the-next-step + (:guard (access-list---first-row-of-storage-key-processing)) + (let ((ROFF_CURR_FINAL 2) ;; row offset of final row of current IS_ACCESS_LIST_STORAGE_KEY-cycle + (ROFF_NEXT_START 3)) ;; row offset of first row of next cycle + (if-not-zero (rlptxn---access-list---storage-key-list-countdown) + (eq! (shift IS_ACCESS_LIST_STORAGE_KEY ROFF_NEXT_START) 1) + (if-not-zero (rlptxn---access-list---access-list-item-countdown) + (eq! (shift IS_PREFIX_OF_ACCESS_LIST_ITEM ROFF_NEXT_START) 1) + (eq! (shift PHASE_END ROFF_CURR_FINAL) 1))))) + diff --git a/rlptxn/osaka/constraints/phase/access_list/sub_phases/finalization.lisp b/rlptxn/osaka/constraints/phase/access_list/sub_phases/finalization.lisp new file mode 100644 index 000000000..44aae3205 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/access_list/sub_phases/finalization.lisp @@ -0,0 +1,19 @@ +(module rlptxn) + +(defconstraint access-list---finalization-constraints () + (if-not-zero (* IS_ACCESS_LIST PHASE_END) + (begin + (vanishes! (rlptxn---access-list---access-list-item-countdown)) + (vanishes! (rlptxn---access-list---storage-key-countdown)) + (vanishes! (rlptxn---access-list---storage-key-list-countdown)) + (vanishes! (rlptxn---access-list---AL-RLP-length-countdown)) + (vanishes! (rlptxn---access-list---AL-item-RLP-length-countdown)) + ))) + + +(defproperty access-list---finish-either-on-prefix-or-storage-key-list-or-storage-key + (if-not-zero (* IS_ACCESS_LIST PHASE_END) + (eq! (+ (is-access-list-prefix) + IS_PREFIX_OF_STORAGE_KEY_LIST + IS_ACCESS_LIST_STORAGE_KEY) + 1))) diff --git a/rlptxn/osaka/constraints/phase/beta.lisp b/rlptxn/osaka/constraints/phase/beta.lisp new file mode 100644 index 000000000..a8302bdb5 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/beta.lisp @@ -0,0 +1,44 @@ +(module rlptxn) + + +(defun (first-row-of-beta-phase) (* IS_BETA TXN)) +(defun (first-row-of-beta-phase-with-replay-protection) (* (first-row-of-beta-phase) REPLAY_PROTECTION)) +(defun (beta-phase---Tw-scalar) (if-zero REPLAY_PROTECTION + ;; replay_protection ≡ + (+ UNPROTECTED_V Y_PARITY) + ;; replay_protection ≡ + (+ (* 2 txn/CHAIN_ID) + PROTECTED_BASE_V + Y_PARITY))) + +(defconstraint beta-phase---RLP-ization-of-Tw + (:guard (first-row-of-beta-phase)) + (let ((ROFF 1)) + (begin + (limb-of-lt-only ROFF) + (rlp-compound-constraint---INTEGER ROFF + 0 + (beta-phase---Tw-scalar) + (- 1 REPLAY_PROTECTION))))) + +(defconstraint beta-phase---RLP-ization-of-the-transactions-chain-id + (:guard (first-row-of-beta-phase-with-replay-protection)) + (let ((ROFF (+ 3 1))) + (begin + (limb-of-lx-only ROFF) + (rlp-compound-constraint---INTEGER ROFF + 0 + txn/CHAIN_ID + 0)))) + +(defconstraint beta-phase---accounting-for-RLP-empty-RLP-empty-in-the-RLP-string + (:guard (first-row-of-beta-phase-with-replay-protection)) + (let ((ROFF (+ 3 3 1))) + (begin + (limb-of-lx-only ROFF) + (set-limb ROFF + (+ (* RLP_PREFIX_INT_SHORT (^ 256 LLARGEMO)) + (* RLP_PREFIX_INT_SHORT (^ 256 14))) + 2) + (eq! (shift PHASE_END ROFF) 1) + ))) diff --git a/rlptxn/osaka/constraints/phase/data/limb.lisp b/rlptxn/osaka/constraints/phase/data/limb.lisp new file mode 100644 index 000000000..537bf22bb --- /dev/null +++ b/rlptxn/osaka/constraints/phase/data/limb.lisp @@ -0,0 +1,34 @@ +(module rlptxn) + + +(defconstraint data-phase---limb-content-analysis---RLP_UTILS-call + (:guard (is-limb-content-analysis-row)) + (rlputils-call---DATA_PRICING 0 + cmp/LIMB + cmp/LIMB_SIZE) + ) + +(defun (zeros-in-limb) cmp/EXO_DATA_6) +(defun (nonzs-in-limb) cmp/EXO_DATA_7) ;; "" + +(defconstraint data-phase---limb-content-analysis---updating-countdowns + (:guard (is-limb-content-analysis-row)) + (begin + (eq! (zeros-countdown) (- (prev (zeros-countdown)) (zeros-in-limb))) + (eq! (nonzs-countdown) (- (prev (nonzs-countdown)) (nonzs-in-limb))) + )) + +(defconstraint data-phase---limb-content-analysis---PHASE_END-constraints-and-further-relations + (:guard (is-limb-content-analysis-row)) + (begin + (if-zero PHASE_END (eq! cmp/LIMB_SIZE LLARGE)) + ;; (eq! PHASE_END (* (- 1 (~ (zeros-countdown))) (- 1 (~ (nonzs-countdown))))) is equivalent to the two following constraints + (if (and! (== (zeros-countdown) 0) + (== (nonzs-countdown) 0)) + (eq! PHASE_END 1)) + (if-not-zero PHASE_END + (begin + (vanishes! (zeros-countdown)) + (vanishes! (nonzs-countdown)))) + (eq! PHASE_END DONE) + )) diff --git a/rlptxn/osaka/constraints/phase/data/prefix.lisp b/rlptxn/osaka/constraints/phase/data/prefix.lisp new file mode 100644 index 000000000..301e0377e --- /dev/null +++ b/rlptxn/osaka/constraints/phase/data/prefix.lisp @@ -0,0 +1,40 @@ +(module rlptxn) + +(defun (rlptxn---DATA-phase---payload-size) (+ (rlptxn---DATA-phase---zeros-in-payload) + (rlptxn---DATA-phase---nonzs-in-payload))) +(defun (rlptxn---DATA-phase---zeros-in-payload) (prev txn/NUMBER_OF_ZERO_BYTES)) +(defun (rlptxn---DATA-phase---nonzs-in-payload) (prev txn/NUMBER_OF_NONZERO_BYTES)) +(defun (rlptxn---DATA-phase---first-byte-or-zero) (* (rlptxn---DATA-phase---payload-is-nonempty) (rlptxn---DATA-phase---maybe-first-byte-of-payload))) +(defun (rlptxn---DATA-phase---maybe-first-byte-of-payload) (next cmp/EXO_DATA_8)) +(defun (rlptxn---DATA-phase---payload-is-nonempty) cmp/EXO_DATA_4) ;; "" +(defun (rlptxn---DATA-phase---payload-is-empty) (force-bin (- 1 (rlptxn---DATA-phase---payload-is-nonempty)))) + +(defconstraint data-phase---payload-size-analysis-row---calling-RLP_UTILS + (:guard (is-payload-size-analysis-row)) + ;; RLP_UTILS instruction call + (rlp-compound-constraint---BYTE_STRING_PREFIX 0 + (rlptxn---DATA-phase---payload-size) + (rlptxn---DATA-phase---first-byte-or-zero) + 0 + 0) + ) + +(defconstraint data-phase---payload-size-analysis-row---initializing-countdowns + (:guard (is-payload-size-analysis-row)) + (begin + (eq! (zeros-countdown) (rlptxn---DATA-phase---zeros-in-payload)) + (eq! (nonzs-countdown) (rlptxn---DATA-phase---nonzs-in-payload)) + )) + +(defconstraint data-phase---payload-size-analysis-row---empty-payload-sanity-check + (:guard (is-payload-size-analysis-row)) + (if-not-zero (rlptxn---DATA-phase---payload-is-empty) + (begin + (vanishes! (rlptxn---DATA-phase---zeros-in-payload)) + (vanishes! (rlptxn---DATA-phase---nonzs-in-payload)))) + ) + +(defconstraint data-phase---payload-size-analysis-row---empty-payload-sanity-check2 + (:guard (is-payload-size-analysis-row)) + (eq! PHASE_END (rlptxn---DATA-phase---payload-is-empty)) + ) diff --git a/rlptxn/osaka/constraints/phase/data/shorthands.lisp b/rlptxn/osaka/constraints/phase/data/shorthands.lisp new file mode 100644 index 000000000..445a721d5 --- /dev/null +++ b/rlptxn/osaka/constraints/phase/data/shorthands.lisp @@ -0,0 +1,7 @@ +(module rlptxn) + +(defun (zeros-countdown) cmp/AUX_1) +(defun (nonzs-countdown) cmp/AUX_2) +(defun (is-payload-size-analysis-row) (* (prev TXN) IS_DATA)) +;; defined outside of the module to be accessible in lookups +;; (defun (is-limb-content-analysis-row) (* (prev CMP) CMP IS_DATA)) diff --git a/rlptxn/osaka/constraints/phase/global_rlp_prefix.lisp b/rlptxn/osaka/constraints/phase/global_rlp_prefix.lisp new file mode 100644 index 000000000..59e9a108b --- /dev/null +++ b/rlptxn/osaka/constraints/phase/global_rlp_prefix.lisp @@ -0,0 +1,50 @@ +(module rlptxn) + +(defconstraint IS_RLP_PREFIX-phase---byte-size-countdowns-remain-constant-throughout + (:guard IS_RLP_PREFIX) + (begin + (eq! LT_BYTE_SIZE_COUNTDOWN (next LT_BYTE_SIZE_COUNTDOWN)) + (eq! LX_BYTE_SIZE_COUNTDOWN (next LX_BYTE_SIZE_COUNTDOWN)))) + +(defproperty IS_RLP_PREFIX-phase---setting-ct-max + (if-not-zero IS_RLP_PREFIX (vanishes! CT_MAX))) + +(defun (first-row-of-IS_RLP_PREFIX) (* IS_RLP_PREFIX TXN)) + +;; row i + 1 +(defconstraint IS_RLP_PREFIX-phase---first-computation-row---transaction-type-prefix + (:guard (first-row-of-IS_RLP_PREFIX)) + (let ((ROFF 1)) + (begin + (limb-of-both-lt-and-lx ROFF) + (if-not-zero (shift TYPE_0 ROFF) + (discard-limb ROFF) + (set-limb ROFF + (* txn/TX_TYPE (^ 256 LLARGEMO)) + 1)) ;; "" + (vanishes! (next PHASE_END)) + ))) + +;; row i + 2 +(defconstraint IS_RLP_PREFIX-phase---second-computation-row---global-prefix-for-LT + (:guard (first-row-of-IS_RLP_PREFIX)) + (let ((ROFF 2)) + (begin + (limb-of-lt-only ROFF) + (rlputils-call---BYTE_STRING_PREFIX-non-trivial ROFF + LT_BYTE_SIZE_COUNTDOWN + 1) + (vanishes! (shift PHASE_END ROFF)) + ))) + +;; row i + 3 +(defconstraint IS_RLP_PREFIX-phase---third-computation-row---global-prefix-for-LX + (:guard (first-row-of-IS_RLP_PREFIX)) + (let ((ROFF 3)) + (begin + (limb-of-lx-only ROFF) + (rlputils-call---BYTE_STRING_PREFIX-non-trivial ROFF + LX_BYTE_SIZE_COUNTDOWN + 1) + (eq! (shift PHASE_END ROFF) 1) + ))) diff --git a/rlptxn/osaka/constraints/phase/integer.lisp b/rlptxn/osaka/constraints/phase/integer.lisp new file mode 100644 index 000000000..d6a7cbc1f --- /dev/null +++ b/rlptxn/osaka/constraints/phase/integer.lisp @@ -0,0 +1,47 @@ +(module rlptxn) + +(defun (is-integer-phase) + (force-bin (+ + ;; IS_RLP_PREFIX + IS_CHAIN_ID + IS_NONCE + IS_GAS_PRICE + IS_MAX_PRIORITY_FEE_PER_GAS + IS_MAX_FEE_PER_GAS + IS_GAS_LIMIT + ;; IS_TO + IS_VALUE + ;; IS_DATA + ;; IS_ACCESS_LIST + ;; IS_BETA + IS_Y + IS_R + IS_S + ))) + +(defun (phase-appropriate-integer-hi) + (+ (* IS_R (next cmp/EXO_DATA_1)) + (* IS_S (next cmp/EXO_DATA_1)))) + +(defun (phase-appropriate-integer-lo) + (+ (* IS_CHAIN_ID txn/CHAIN_ID ) + (* IS_NONCE txn/NONCE ) + (* IS_GAS_PRICE txn/GAS_PRICE ) + (* IS_MAX_PRIORITY_FEE_PER_GAS txn/MAX_PRIORITY_FEE_PER_GAS ) + (* IS_MAX_FEE_PER_GAS txn/MAX_FEE_PER_GAS ) + (* IS_GAS_LIMIT txn/GAS_LIMIT ) + (* IS_VALUE txn/VALUE ) + (* IS_Y Y_PARITY ) + (* IS_R (next cmp/EXO_DATA_2) ) + (* IS_S (next cmp/EXO_DATA_2) ) + )) + + +(defun (is-first-row-of-integer-phase) (* (is-integer-phase) TXN)) + +(defconstraint integer-phase-constraint + (:guard (is-first-row-of-integer-phase)) + (rlp-compound-constraint---INTEGER 1 + (phase-appropriate-integer-hi) + (phase-appropriate-integer-lo) + 1)) diff --git a/rlptxn/osaka/constraints/phase/to.lisp b/rlptxn/osaka/constraints/phase/to.lisp new file mode 100644 index 000000000..fe808d8de --- /dev/null +++ b/rlptxn/osaka/constraints/phase/to.lisp @@ -0,0 +1,28 @@ +(module rlptxn) + +(defun (is-first-row-of-TO-phase) (* IS_TO TXN)) + +(defconstraint TO-phase-constraints () + (if-not-zero (is-first-row-of-TO-phase) + (if-not-zero IS_DEPLOYMENT + ;; deployment transaction case + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + ;; setting CT_MAX + (debug (vanishes! (shift CT_MAX 1))) + ;; writing the RLP prefix to the RLP string + (set-limb 1 + (* RLP_PREFIX_INT_SHORT (^ 256 LLARGEMO)) ;; "" + 1) + ;; setting PHASE_END + (eq! (shift PHASE_END 1) 1)) + ;; message call transaction case + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + ;; calling the RLP_UTILS instruction + (rlp-compound-constraint---ADDRESS 1 + txn/TO_HI + txn/TO_LO) + ;; setting PHASE_END + (eq! (shift PHASE_END 3) 1)) + ))) diff --git a/rlptxn/osaka/constraints/specialized/compound_address.lisp b/rlptxn/osaka/constraints/specialized/compound_address.lisp new file mode 100644 index 000000000..e2f4fe319 --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/compound_address.lisp @@ -0,0 +1,25 @@ +(module rlptxn) + +(defun (rlp-compound-constraint---ADDRESS relOffset + address-hi + address-lo) + (begin + ;; setting CT_MAX + (eq! (shift CT_MAX relOffset) RLP_TXN_CT_MAX_ADDRESS) + ;; calling RLPADDR + (eq! (shift cmp/TRM_FLAG relOffset) 1) + (eq! (shift cmp/EXO_DATA_1 relOffset) address-hi) + (eq! (shift cmp/EXO_DATA_2 relOffset) address-lo) + ;; enshrining the RLP-prefix into the RLP string + (set-limb relOffset + (* 148 (^ 256 LLARGEMO)) ;; "" ... "" + 1) + ;; enshrining the hi part of the address into the RLP string + (set-limb (+ relOffset 1) + (* address-hi (^ 256 12)) + 4) + ;; enshrining the hi part of the address into the RLP string + (set-limb (+ relOffset 2) + address-lo + LLARGE) + )) diff --git a/rlptxn/osaka/constraints/specialized/compound_byte_string_prefix.lisp b/rlptxn/osaka/constraints/specialized/compound_byte_string_prefix.lisp new file mode 100644 index 000000000..df03087b6 --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/compound_byte_string_prefix.lisp @@ -0,0 +1,55 @@ +(module rlptxn) + +(defun (rlp-compound-constraint---BYTE_STRING_PREFIX-non-trivial relOffset + length + is-list + must-be-non-trivial) + (begin + ;; setting CT_MAX + (vanishes! (shift CT_MAX relOffset)) + ;; RLP_UTILS instruction call + (rlputils-call---BYTE_STRING_PREFIX-non-trivial relOffset + length + is-list) + ;; enshrining the byte string's RLP prefix into the RLP string + (conditionally-set-limb relOffset + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-required relOffset) + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix relOffset) + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-byte-size relOffset)) + ;; imposing nontriviality + (if-not-zero must-be-non-trivial + (begin + (eq! (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-required relOffset) 1) + (eq! (rlptxn---BYTE_STRING_PREFIX---bs-is-non-empty relOffset) 1))) + )) + +(defun (rlp-compound-constraint---BYTE_STRING_PREFIX relOffset + length + first-byte + is-list + must-be-non-trivial) + (begin + ;; setting CT_MAX + (vanishes! (shift CT_MAX relOffset)) + ;; RLP_UTILS instruction call + (rlputils-call---BYTE_STRING_PREFIX relOffset + length + first-byte + is-list) + ;; enshrining the byte string's RLP prefix into the RLP string + (conditionally-set-limb relOffset + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-required relOffset) + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix relOffset) + (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-byte-size relOffset)) + ;; imposing nontriviality + (if-not-zero must-be-non-trivial + (begin + (eq! (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-required relOffset) 1) + (eq! (rlptxn---BYTE_STRING_PREFIX---bs-is-non-empty relOffset) 1))) + )) + +;; defining shorthands +(defun (rlptxn---BYTE_STRING_PREFIX---bs-is-non-empty relOffset) (shift cmp/EXO_DATA_4 relOffset)) +(defun (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-required relOffset) (shift cmp/EXO_DATA_5 relOffset)) +(defun (rlptxn---BYTE_STRING_PREFIX---rlp-prefix relOffset) (shift cmp/EXO_DATA_6 relOffset)) +(defun (rlptxn---BYTE_STRING_PREFIX---rlp-prefix-byte-size relOffset) (shift cmp/EXO_DATA_8 relOffset)) diff --git a/rlptxn/osaka/constraints/specialized/compound_bytes32.lisp b/rlptxn/osaka/constraints/specialized/compound_bytes32.lisp new file mode 100644 index 000000000..e85ae80b0 --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/compound_bytes32.lisp @@ -0,0 +1,25 @@ +(module rlptxn) + +(defun (rlp-compound-constraint---BYTES32 relOffset + data-hi + data-lo) + (begin + ;; setting CT_MAX + (eq! (shift CT_MAX relOffset) RLP_TXN_CT_MAX_BYTES32) + ;; RLP_UTILS instruction call + (rlputils-call---BYTES32 relOffset + data-hi + data-lo) + ;; enshrining the RLP-prefix into the RLP string + (set-limb relOffset + (* 160 (^ 256 LLARGEMO)) + 1) ;; "" + ;; enshrining data-hi into the RLP string + (set-limb (+ relOffset 1) + data-hi + LLARGE) + ;; enshrining data-lo into the RLP string + (set-limb (+ relOffset 2) + data-lo + LLARGE) + )) diff --git a/rlptxn/osaka/constraints/specialized/compound_integer.lisp b/rlptxn/osaka/constraints/specialized/compound_integer.lisp new file mode 100644 index 000000000..5105b4367 --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/compound_integer.lisp @@ -0,0 +1,47 @@ +(module rlptxn) + +(defun (rlp-compound-constraint---INTEGER relOffset + integer-hi + integer-lo + is-end-of-phase) + (begin + ;; setting CT_MAX + (eq! (shift CT_MAX relOffset) RLP_TXN_CT_MAX_INTEGER) + ;; constraining PHASE_END + (eq! (shift PHASE_END (+ relOffset RLP_TXN_CT_MAX_INTEGER)) is-end-of-phase) + ;; RLP_UTILS instruction call + (rlputils-call---INTEGER relOffset + integer-hi + integer-lo) + ;; enshrining the integer's RLP prefix into the RLP string + (conditionally-set-limb relOffset + (rlptxn---INTEGER---OUT-rlp-prefix-required relOffset) + (rlptxn---INTEGER---OUT-rlp-prefix relOffset) + 1) + ;; enshrining the hi part of a (nonzero) integer into the RLP string + (conditionally-set-limb (+ relOffset 1) + (rlptxn---INTEGER---OUT-integer-has-non-zero-hi-part relOffset) + (rlptxn---INTEGER---OUT-leading-limb-left-shifted relOffset) + (rlptxn---INTEGER---OUT-leading-limb-byte-size relOffset)) + ;; enshrining the lo part of a (nonzero) integer into the RLP string + (conditionally-set-limb (+ relOffset 2) + (rlptxn---INTEGER---OUT-integer-is-non-zero relOffset) + (rlptxn---INTEGER---last-limb integer-lo relOffset) + (rlptxn---INTEGER---last-limb-byte-size relOffset)) + )) + +;; deriving shorthands +(defun (rlptxn---INTEGER---OUT-integer-is-non-zero relOffset) (shift cmp/EXO_DATA_3 relOffset)) +(defun (rlptxn---INTEGER---OUT-integer-has-non-zero-hi-part relOffset) (shift cmp/EXO_DATA_4 relOffset)) +(defun (rlptxn---INTEGER---OUT-rlp-prefix-required relOffset) (shift cmp/EXO_DATA_5 relOffset)) +(defun (rlptxn---INTEGER---OUT-rlp-prefix relOffset) (shift cmp/EXO_DATA_6 relOffset)) +(defun (rlptxn---INTEGER---OUT-leading-limb-left-shifted relOffset) (shift cmp/EXO_DATA_7 relOffset)) +(defun (rlptxn---INTEGER---OUT-leading-limb-byte-size relOffset) (shift cmp/EXO_DATA_8 relOffset)) +(defun (rlptxn---INTEGER---last-limb integer-lo relOffset) + (if-zero (rlptxn---INTEGER---OUT-integer-has-non-zero-hi-part relOffset) + (rlptxn---INTEGER---OUT-leading-limb-left-shifted relOffset) + integer-lo)) +(defun (rlptxn---INTEGER---last-limb-byte-size relOffset) + (if-zero (rlptxn---INTEGER---OUT-integer-has-non-zero-hi-part relOffset) + (rlptxn---INTEGER---OUT-leading-limb-byte-size relOffset) + LLARGE)) diff --git a/rlptxn/osaka/constraints/specialized/limb_membership_constraints.lisp b/rlptxn/osaka/constraints/specialized/limb_membership_constraints.lisp new file mode 100644 index 000000000..17c7b520a --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/limb_membership_constraints.lisp @@ -0,0 +1,16 @@ +(module rlptxn) + +(defun (limb-of-lt-only w) + (begin + (eq! (shift LT w) 1) + (eq! (shift LX w) 0))) + +(defun (limb-of-lx-only w) + (begin + (eq! (shift LT w) 0) + (eq! (shift LX w) 1))) + +(defun (limb-of-both-lt-and-lx w) + (begin + (eq! (shift LT w) 1) + (eq! (shift LX w) 1))) diff --git a/rlptxn/osaka/constraints/specialized/limb_setting.lisp b/rlptxn/osaka/constraints/specialized/limb_setting.lisp new file mode 100644 index 000000000..c4a10241d --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/limb_setting.lisp @@ -0,0 +1,22 @@ +(module rlptxn) + +(defun (conditionally-set-limb w + condition-bit + limb + number-of-bytes) + (begin + (eq! (shift LC w) condition-bit) + (eq! (shift cmp/LIMB w) (* condition-bit limb)) + (eq! (shift cmp/LIMB_SIZE w) (* condition-bit number-of-bytes)))) + +(defun (set-limb w + limb + number-of-bytes) + (begin + (eq! (shift LC w) 1) + (eq! (shift cmp/LIMB w) limb) + (eq! (shift cmp/LIMB_SIZE w) number-of-bytes))) + +(defun (discard-limb w) + (eq! (shift LC w) 0)) + diff --git a/rlptxn/osaka/constraints/specialized/rlputils_calls.lisp b/rlptxn/osaka/constraints/specialized/rlputils_calls.lisp new file mode 100644 index 000000000..f68e168a4 --- /dev/null +++ b/rlptxn/osaka/constraints/specialized/rlputils_calls.lisp @@ -0,0 +1,49 @@ +(module rlptxn) + +(defun (rlputils-call---INTEGER relOffset + integer-hi + integer-lo) + (begin + (eq! (shift cmp/RLPUTILS_FLAG relOffset) 1) + (eq! (shift cmp/RLPUTILS_INST relOffset) RLP_UTILS_INST_INTEGER) + (eq! (shift cmp/EXO_DATA_1 relOffset) integer-hi) + (eq! (shift cmp/EXO_DATA_2 relOffset) integer-lo))) + +(defun (rlputils-call---BYTE_STRING_PREFIX-non-trivial relOffset + length + is-list) + (begin + (eq! (shift cmp/RLPUTILS_FLAG relOffset) 1) + (eq! (shift cmp/RLPUTILS_INST relOffset) RLP_UTILS_INST_BYTE_STRING_PREFIX) + (eq! (shift cmp/EXO_DATA_1 relOffset) length) + ;; (eq! (shift cmp/EXO_DATA_2 relOffset) first-byte) + (eq! (shift cmp/EXO_DATA_3 relOffset) is-list))) + +(defun (rlputils-call---BYTE_STRING_PREFIX relOffset + length + first-byte + is-list) + (begin + (eq! (shift cmp/RLPUTILS_FLAG relOffset) 1) + (eq! (shift cmp/RLPUTILS_INST relOffset) RLP_UTILS_INST_BYTE_STRING_PREFIX) + (eq! (shift cmp/EXO_DATA_1 relOffset) length) + (eq! (shift cmp/EXO_DATA_2 relOffset) first-byte) + (eq! (shift cmp/EXO_DATA_3 relOffset) is-list))) + +(defun (rlputils-call---BYTES32 relOffset + data-hi + data-lo) + (begin + (eq! (shift cmp/RLPUTILS_FLAG relOffset) 1) + (eq! (shift cmp/RLPUTILS_INST relOffset) RLP_UTILS_INST_BYTES32) + (eq! (shift cmp/EXO_DATA_1 relOffset) data-hi) + (eq! (shift cmp/EXO_DATA_2 relOffset) data-lo))) + +(defun (rlputils-call---DATA_PRICING relOffset + limb + n-bytes) + (begin + (eq! (shift cmp/RLPUTILS_FLAG relOffset) 1) + (eq! (shift cmp/RLPUTILS_INST relOffset) RLP_UTILS_INST_DATA_PRICING) + (eq! (shift cmp/EXO_DATA_1 relOffset) limb) + (eq! (shift cmp/EXO_DATA_2 relOffset) n-bytes))) diff --git a/rlptxn/osaka/lookups/rlptxn_into_blockdata.lisp b/rlptxn/osaka/lookups/rlptxn_into_blockdata.lisp new file mode 100644 index 000000000..4ca4a5133 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_blockdata.lisp @@ -0,0 +1,16 @@ +(defun (sel-rlptxn-to-blockdata) (force-bin (* rlptxn.TXN rlptxn.REPLAY_PROTECTION))) + +(defclookup + rlptxn-into-blockdata + ;; target columns + ( + blockdata.IS_CHAINID + blockdata.DATA_LO + ) + ;; source selector + (sel-rlptxn-to-blockdata) + ;; source columns + ( + 1 + rlptxn.txn/CHAIN_ID + )) \ No newline at end of file diff --git a/rlptxn/osaka/lookups/rlptxn_into_hub.lisp b/rlptxn/osaka/lookups/rlptxn_into_hub.lisp new file mode 100644 index 000000000..c779f5ef5 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_hub.lisp @@ -0,0 +1,38 @@ +(defun (sel-rlp-txn-into-hub) +(force-bin + (* rlptxn.REQUIRES_EVM_EXECUTION + (+ rlptxn.IS_ACCESS_LIST_ADDRESS rlptxn.IS_ACCESS_LIST_STORAGE_KEY ) + (prev rlptxn.DONE)))) + +(defun (rlptxn---access-list---address-hi) rlptxn.cmp/AUX_CCC_4) +(defun (rlptxn---access-list---address-lo) rlptxn.cmp/AUX_CCC_5) + +(defclookup + rlptxn-into-hub + ;; target columns + ( + hub.TX_WARM + hub.USER_TXN_NUMBER + hub.PEEK_AT_ACCOUNT + hub.PEEK_AT_STORAGE + (prewarming-phase-address-hi) + (prewarming-phase-address-lo) + (prewarming-phase-storage-key-hi) + (prewarming-phase-storage-key-lo) + ) + ;; source selector + (sel-rlp-txn-into-hub) + ;; source columns + ( + 1 + rlptxn.USER_TXN_NUMBER + rlptxn.IS_ACCESS_LIST_ADDRESS + rlptxn.IS_ACCESS_LIST_STORAGE_KEY + (rlptxn---access-list---address-hi) + (rlptxn---access-list---address-lo) + (* rlptxn.cmp/EXO_DATA_1 rlptxn.IS_ACCESS_LIST_STORAGE_KEY) + (* rlptxn.cmp/EXO_DATA_2 rlptxn.IS_ACCESS_LIST_STORAGE_KEY) + ) + ) + + diff --git a/rlptxn/osaka/lookups/rlptxn_into_rlputils.lisp b/rlptxn/osaka/lookups/rlptxn_into_rlputils.lisp new file mode 100644 index 000000000..3c2e191e4 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_rlputils.lisp @@ -0,0 +1,32 @@ +(defun (sel-rlptxn-to-rlputils) (* rlptxn.CMP rlptxn.cmp/RLPUTILS_FLAG)) + +(defclookup + rlptxn-into-rlputils + ;; target columns + ( + rlputils.MACRO + rlputils.macro/INST + rlputils.macro/DATA_1 + rlputils.macro/DATA_2 + rlputils.macro/DATA_3 + rlputils.macro/DATA_4 + rlputils.macro/DATA_5 + rlputils.macro/DATA_6 + rlputils.macro/DATA_7 + rlputils.macro/DATA_8 + ) + ;; source selector + (sel-rlptxn-to-rlputils) + ;; source columns + ( + 1 + rlptxn.cmp/RLPUTILS_INST + rlptxn.cmp/EXO_DATA_1 + rlptxn.cmp/EXO_DATA_2 + rlptxn.cmp/EXO_DATA_3 + rlptxn.cmp/EXO_DATA_4 + rlptxn.cmp/EXO_DATA_5 + rlptxn.cmp/EXO_DATA_6 + rlptxn.cmp/EXO_DATA_7 + rlptxn.cmp/EXO_DATA_8 + )) \ No newline at end of file diff --git a/rlptxn/osaka/lookups/rlptxn_into_rom.lisp b/rlptxn/osaka/lookups/rlptxn_into_rom.lisp new file mode 100644 index 000000000..61146c6e6 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_rom.lisp @@ -0,0 +1,24 @@ +(defun (sel-rlptxn-to-rom) (* rlptxn.IS_DEPLOYMENT rlptxn.REQUIRES_EVM_EXECUTION (is-limb-content-analysis-row))) + +(defun (is-limb-content-analysis-row) (* (prev rlptxn.CMP) rlptxn.CMP rlptxn.IS_DATA)) + +(defclookup + rlptxn-into-rom + ;; target columns + ( + rom.CODE_FRAGMENT_INDEX + rom.LIMB + rom.INDEX + rom.nBYTES + ) + ;; source selector + (sel-rlptxn-to-rom) + ;; source columns + ( + rlptxn.CODE_FRAGMENT_INDEX + rlptxn.cmp/LIMB + rlptxn.CT + rlptxn.cmp/LIMB_SIZE + )) + + diff --git a/rlptxn/osaka/lookups/rlptxn_into_trm.lisp b/rlptxn/osaka/lookups/rlptxn_into_trm.lisp new file mode 100644 index 000000000..5f1747518 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_trm.lisp @@ -0,0 +1,16 @@ +(defun (sel-rlptxn-to-trm) (* rlptxn.CMP rlptxn.cmp/TRM_FLAG)) + +(defclookup + (rlptxn-into-trm :unchecked) + ;; target columns + ( + trm.RAW_ADDRESS + trm.ADDRESS_HI + ) + ;; source selector + (sel-rlptxn-to-trm) + ;; source columns + ( + (:: rlptxn.cmp/EXO_DATA_1 rlptxn.cmp/EXO_DATA_2) + rlptxn.cmp/EXO_DATA_1 + )) diff --git a/rlptxn/osaka/lookups/rlptxn_into_txndata.lisp b/rlptxn/osaka/lookups/rlptxn_into_txndata.lisp new file mode 100644 index 000000000..38bb9fae8 --- /dev/null +++ b/rlptxn/osaka/lookups/rlptxn_into_txndata.lisp @@ -0,0 +1,59 @@ +(defun (src-selector---rlp-txn---into---txn-data) rlptxn.TXN ) ;; +(defun (tgt-selector---rlp-txn---into---txn-data) txndata.USER ) ;; "" +(defun (txn-data-hub-view-cfi) (shift txndata.hub/CFI -1)) + +(defclookup + (rlp-txn-rcpt---into---txn-data :unchecked) + ;; target selector: none + (tgt-selector---rlp-txn---into---txn-data) + ;; target columns + ( + txndata.USER + txndata.RLP + txndata.USER_TXN_NUMBER + txndata.prover___USER_TXN_NUMBER_MAX + (txn-data-hub-view-cfi) + txndata.rlp/REQUIRES_EVM_EXECUTION + txndata.rlp/IS_DEPLOYMENT + txndata.rlp/TX_TYPE + txndata.rlp/TO_ADDRESS_HI + txndata.rlp/TO_ADDRESS_LO + txndata.rlp/VALUE + txndata.rlp/NONCE + txndata.rlp/NUMBER_OF_ZERO_BYTES + txndata.rlp/NUMBER_OF_NONZERO_BYTES + txndata.rlp/NUMBER_OF_ACCESS_LIST_ADDRESSES + txndata.rlp/NUMBER_OF_ACCESS_LIST_STORAGE_KEYS + txndata.rlp/GAS_LIMIT + txndata.rlp/GAS_PRICE + txndata.rlp/MAX_PRIORITY_FEE_PER_GAS + txndata.rlp/MAX_FEE_PER_GAS + ) + ;; source selector + (src-selector---rlp-txn---into---txn-data) + ;; source columns + ( + 1 + 1 + rlptxn.USER_TXN_NUMBER + rlptxn.prover___USER_TXN_NUMBER_MAX + rlptxn.CODE_FRAGMENT_INDEX + rlptxn.REQUIRES_EVM_EXECUTION + rlptxn.IS_DEPLOYMENT + rlptxn.txn/TX_TYPE + rlptxn.txn/TO_HI + rlptxn.txn/TO_LO + rlptxn.txn/VALUE + rlptxn.txn/NONCE + rlptxn.txn/NUMBER_OF_ZERO_BYTES + rlptxn.txn/NUMBER_OF_NONZERO_BYTES + rlptxn.txn/NUMBER_OF_PREWARMED_ADDRESSES + rlptxn.txn/NUMBER_OF_PREWARMED_STORAGE_KEYS + rlptxn.txn/GAS_LIMIT + rlptxn.txn/GAS_PRICE + rlptxn.txn/MAX_PRIORITY_FEE_PER_GAS + rlptxn.txn/MAX_FEE_PER_GAS + ) + ) + + diff --git a/rlptxn/osaka/prover/prover_columns_corset.lisp b/rlptxn/osaka/prover/prover_columns_corset.lisp new file mode 100644 index 000000000..faf0d4621 --- /dev/null +++ b/rlptxn/osaka/prover/prover_columns_corset.lisp @@ -0,0 +1,33 @@ +(module rlptxn) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constraints verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defcolumns + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + USRMAX prover___USER_TXN_NUMBER_MAX + ) + + + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---constancy () + (if-not-zero USER_TXN_NUMBER + (will-remain-constant! USRMAX))) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization + (:domain {-1}) ;; "" + (eq! USRMAX USER_TXN_NUMBER)) + + + +;; TOTL|USER|SYSF|SYSI|prover diff --git a/txndata/prague/columns/hub_view.lisp b/txndata/prague/columns/hub_view.lisp index 1383a79b3..453826868 100644 --- a/txndata/prague/columns/hub_view.lisp +++ b/txndata/prague/columns/hub_view.lisp @@ -29,9 +29,9 @@ ( IS_DEPLOYMENT :binary@prove ) ( NONCE :i64 ) ;; recall the EIP capping nonces to 2^64 - 1 or so ( VALUE :i128 ) - ( GAS_LIMIT :i25 ) + ( GAS_LIMIT :i33 ) ( GAS_PRICE :i64 ) - ( GAS_INITIALLY_AVAILABLE :i25 ) + ( GAS_INITIALLY_AVAILABLE :i33 ) ( CALL_DATA_SIZE :i24 ) ( INIT_CODE_SIZE :i24 ) ( HAS_EIP_1559_GAS_SEMANTICS :binary@prove ) @@ -40,9 +40,9 @@ ( CFI :i16 ) ( INIT_BALANCE :i128 ) ( STATUS_CODE :binary@prove ) - ( GAS_LEFTOVER :i25 ) - ( REFUND_COUNTER_FINAL :i25 ) - ( REFUND_EFFECTIVE :i25 ) + ( GAS_LEFTOVER :i33 ) + ( REFUND_COUNTER_FINAL :i33 ) + ( REFUND_EFFECTIVE :i33 ) ( EIP_4788 :binary@prove ) ( EIP_2935 :binary@prove ) ( NOOP :binary@prove ) diff --git a/txndata/prague/columns/rlp_view.lisp b/txndata/prague/columns/rlp_view.lisp index 8592a61e7..953be5271 100644 --- a/txndata/prague/columns/rlp_view.lisp +++ b/txndata/prague/columns/rlp_view.lisp @@ -29,7 +29,7 @@ ( NUMBER_OF_NONZERO_BYTES :i32 ) ( DATA_SIZE :i24 ) ( INIT_SIZE :i24 ) - ( GAS_LIMIT :i25 ) + ( GAS_LIMIT :i33 ) ( GAS_PRICE :i64 ) ( MAX_PRIORITY_FEE_PER_GAS :i64 ) ( MAX_FEE_PER_GAS :i64 ) From 624eebc3c935c8e5706f6d854f71a686d55a43ee Mon Sep 17 00:00:00 2001 From: amkCha <29160563+amkCha@users.noreply.github.com> Date: Mon, 15 Dec 2025 22:06:49 +0100 Subject: [PATCH 2/2] i64 i/o i33 --- hub/prague/columns/transaction.lisp | 10 +++++----- rlptxn/cancun/columns/transaction.lisp | 2 +- txndata/prague/columns/hub_view.lisp | 10 +++++----- txndata/prague/columns/rlp_view.lisp | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/hub/prague/columns/transaction.lisp b/hub/prague/columns/transaction.lisp index e2b4b37f7..d62ef3cb0 100644 --- a/hub/prague/columns/transaction.lisp +++ b/hub/prague/columns/transaction.lisp @@ -23,8 +23,8 @@ ( IS_TYPE2 :binary ) ;; gas related - ( GAS_LIMIT :i33 ) - ( GAS_INITIALLY_AVAILABLE :i33 ) + ( GAS_LIMIT :i64 ) + ( GAS_INITIALLY_AVAILABLE :i64 ) ( GAS_PRICE :i64 ) ( PRIORITY_FEE_PER_GAS :i64 ) ( BASEFEE :i64 ) ;; in Linea London this is hard-coded to 7 ... but in the reference tests this may be much larger @@ -35,9 +35,9 @@ ;; end of transaction predictions ( STATUS_CODE :binary ) - ( GAS_LEFTOVER :i33 ) - ( REFUND_COUNTER_INFINITY :i33 ) - ( REFUND_EFFECTIVE :i33 ) + ( GAS_LEFTOVER :i64 ) + ( REFUND_COUNTER_INFINITY :i64 ) + ( REFUND_EFFECTIVE :i64 ) ;; coinbase related ( COINBASE_ADDRESS_HI :i32 ) diff --git a/rlptxn/cancun/columns/transaction.lisp b/rlptxn/cancun/columns/transaction.lisp index 471ec0d43..bd5b3e706 100644 --- a/rlptxn/cancun/columns/transaction.lisp +++ b/rlptxn/cancun/columns/transaction.lisp @@ -10,7 +10,7 @@ ( GAS_PRICE :i64 ) ( MAX_PRIORITY_FEE_PER_GAS :i64 ) ( MAX_FEE_PER_GAS :i64 ) - ( GAS_LIMIT :i33 ) + ( GAS_LIMIT :i64 ) ( TO_HI :i32 ) ( TO_LO :i128 ) ( VALUE :i96 ) diff --git a/txndata/prague/columns/hub_view.lisp b/txndata/prague/columns/hub_view.lisp index 453826868..cf9654820 100644 --- a/txndata/prague/columns/hub_view.lisp +++ b/txndata/prague/columns/hub_view.lisp @@ -29,9 +29,9 @@ ( IS_DEPLOYMENT :binary@prove ) ( NONCE :i64 ) ;; recall the EIP capping nonces to 2^64 - 1 or so ( VALUE :i128 ) - ( GAS_LIMIT :i33 ) + ( GAS_LIMIT :i64 ) ( GAS_PRICE :i64 ) - ( GAS_INITIALLY_AVAILABLE :i33 ) + ( GAS_INITIALLY_AVAILABLE :i64 ) ( CALL_DATA_SIZE :i24 ) ( INIT_CODE_SIZE :i24 ) ( HAS_EIP_1559_GAS_SEMANTICS :binary@prove ) @@ -40,9 +40,9 @@ ( CFI :i16 ) ( INIT_BALANCE :i128 ) ( STATUS_CODE :binary@prove ) - ( GAS_LEFTOVER :i33 ) - ( REFUND_COUNTER_FINAL :i33 ) - ( REFUND_EFFECTIVE :i33 ) + ( GAS_LEFTOVER :i64 ) + ( REFUND_COUNTER_FINAL :i64 ) + ( REFUND_EFFECTIVE :i64 ) ( EIP_4788 :binary@prove ) ( EIP_2935 :binary@prove ) ( NOOP :binary@prove ) diff --git a/txndata/prague/columns/rlp_view.lisp b/txndata/prague/columns/rlp_view.lisp index 953be5271..dd59906e2 100644 --- a/txndata/prague/columns/rlp_view.lisp +++ b/txndata/prague/columns/rlp_view.lisp @@ -29,7 +29,7 @@ ( NUMBER_OF_NONZERO_BYTES :i32 ) ( DATA_SIZE :i24 ) ( INIT_SIZE :i24 ) - ( GAS_LIMIT :i33 ) + ( GAS_LIMIT :i64 ) ( GAS_PRICE :i64 ) ( MAX_PRIORITY_FEE_PER_GAS :i64 ) ( MAX_FEE_PER_GAS :i64 )