diff --git a/_eips/EIP-7623: Increase calldata cost.md b/_eips/EIP-7623: Increase calldata cost.md new file mode 100644 index 00000000..bccb0857 --- /dev/null +++ b/_eips/EIP-7623: Increase calldata cost.md @@ -0,0 +1,48 @@ +# Notes + +This EIP affects two parts of transaction processing: initialization and finalization. + +## Transaction validity + +```java +long upfrontTransactionGasCost = 21_000 + + (isDeployment ? 32_000 : 0) + + dataCost(payload) + + accessListCost(accessList) + + (isDeployment ? initializationCodeWordCost(payload) : 0) + + accountDelegationCost(); + +long transactionFloorCost = 21_000 + 10 * weightedTokenCount(payload); + +dataCost(payload) = 4 * weightedTokenCount(payload); +weightedTokenCount(payload) = numberOfZeroBytes(payload) + 4 * numberOfNonzeroBytes(payload); +``` + +Transaction validity encompasses all the usual checks (nonce, balance, comparing `upfrontTransactionGasCost` to `tx.gasLimit()`, ...) and a new check: + +```java +boolean validTransaction = ... // nonce, balance, ... + ∧ upfrontTransactionGasCost ≤ tx.gasLimit() + ∧ transactionFloorCost ≤ tx.gasLimit() + ∧ ...; +``` + +The initial amount of gas the root frame starts with remains the same: + +```java +long gasAvailableForExecution = tx.gasLimit() - upfrontTransactionGasCost; +``` + +## Transaction finalization + +Transaction finalization works just as previously but a floor price `transactionFloorCost` applies to the transaction. This amounts to + +```java +long gasLimit = tx.gasLimit() +long gasRemaining = frame.getRemainingGas() +long effectiveRefund = min( frame.accruedRefunds(), (gasLimit - gasRemaining) / 5) + +long consumedGas = max( gasLimit - gasRemaining - effectiveRefund, transactionFloorCost ) // this is new: previously just "gasLimit - gasRemaining - effectiveRefund" + +senderAccount.getEndOfTransactionGasRefund( effectiveGasPrice, gasLimit, consumedGas ) // something à la "sender.balance += effectiveGasPrice * (gasLimit - consumedGas)" +``` diff --git a/pkg/txn_data.sty b/pkg/txn_data.sty index 40f08b2e..e39bea37 100644 --- a/pkg/txn_data.sty +++ b/pkg/txn_data.sty @@ -32,9 +32,9 @@ \newcommand{\txIsTypeTwo} {\transactionSignifier\col{TYPE\_2}} -\newcommand{\maxCtTypeZero} {\redm{7}} -\newcommand{\maxCtTypeOne} {\redm{8}} -\newcommand{\maxCtTypeTwo} {\redm{8}} +\newcommand{\maxCtTypeZero} {\redm{ 8}} +\newcommand{\maxCtTypeOne} {\redm{10}} +\newcommand{\maxCtTypeTwo} {\redm{10}} \newcommand{\txInitialBalance} {\transactionSignifier\col{INIT\_BALANCE}} \newcommand{\txRequiresEvmExecution} {\transactionSignifier\col{REQUIRES\_EVM\_EXECUTION}} @@ -45,16 +45,16 @@ \newcommand{\txEffectiveRefund} {\transactionSignifier\col{REFUND\_EFFECTIVE}} \newcommand{\txCumulativeConsumedGas} {\transactionSignifier\col{GAS\_CUMULATIVE}} -\newcommand{\typeZeroRows}{\redm{7}} -\newcommand{\typeOneRows}{\redm{9}} -\newcommand{\typeTwoRows}{\redm{10}} - -\newcommand{\phaseNumRlpTxn}{\col{PHASE\_RLP\_TXN}} -\newcommand{\phaseNumRlpTxnRcpt}{\col{PHASE\_RLP\_TXNRCPT}} -\newcommand{\outgoingTxrcpt}{\col{OUTGOING\_RLP\_TXRCPT}} +\newcommand{\phaseNumRlpTxn} {\col{PHASE\_RLP\_TXN}} +\newcommand{\phaseNumRlpTxnRcpt} {\col{PHASE\_RLP\_TXNRCPT}} +\newcommand{\outgoingTxrcpt} {\col{OUTGOING\_RLP\_TXRCPT}} \newcommand{\isLastTxOfBlock} {\col{IS\_LAST\_TX\_OF\_BLOCK}} -\newcommand{\lineaBlockGasLimit} {\redm{\texttt{LINEA\_BLOCK\_GAS\_LIMIT}}} -\newcommand{\maxRefundQuotient} {\redm{\texttt{MAX\_REFUND\_QUOTIENT}}} -\newcommand{\maxNonce} {\redm{\texttt{EIP2681\_MAX\_NONCE}}} +\newcommand{\lineaBlockGasLimit} {\red{\texttt{LINEA\_BLOCK\_GAS\_LIMIT}}} +\newcommand{\maxRefundQuotient} {\red{\texttt{MAX\_REFUND\_QUOTIENT}}} +\newcommand{\maxNonce} {\red{\texttt{EIP2681\_MAX\_NONCE}}} +\newcommand{\standardTokenCost} {\red{\texttt{STANDARD\_TOKEN\_COST}}} +\newcommand{\floorTokenCost} {\red{\texttt{FLOOR\_TOKEN\_COST}}} +\newcommand{\standardTokenCostValue} {\red{4}} +\newcommand{\floorTokenCostValue} {\red{10}} diff --git a/pkg/xkeyval_macros/wcp_calls.sty b/pkg/xkeyval_macros/wcp_calls.sty index 747b7d26..088ec75c 100644 --- a/pkg/xkeyval_macros/wcp_calls.sty +++ b/pkg/xkeyval_macros/wcp_calls.sty @@ -113,4 +113,38 @@ \resultMustBeTrueName _{\cmdWCP@var@anchorRow} \big[ \, \cmdWCP@var@relOffset \, \big]} + +\newcommand{\smallCallToLtName} {\texttt{smallCallToLT}} +\newcommand{\smallCallToLeqName} {\texttt{smallCallToLEQ}} +\newcommand{\smallCallToIszeroName} {\texttt{smallCallToISZERO}} + +\newcommand{\smallCallToLt} [1] { + \setkeys[WCP]{var}{#1} + \smallCallToLtName _{\cmdWCP@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Row offset:} & \cmdWCP@var@relOffset \\ + \utt{Argument 1:} & \cmdWCP@var@argOneLo \\ + \utt{Argument 2:} & \cmdWCP@var@argTwoLo \\ + \end{array} \right] +} + +\newcommand{\smallCallToLeq} [1] { + \setkeys[WCP]{var}{#1} + \smallCallToLeqName _{\cmdWCP@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Row offset:} & \cmdWCP@var@relOffset \\ + \utt{Argument 1:} & \cmdWCP@var@argOneLo \\ + \utt{Argument 2:} & \cmdWCP@var@argTwoLo \\ + \end{array} \right] +} + +\newcommand{\smallCallToIszero} [1] { + \setkeys[WCP]{var}{#1} + \smallCallToIszeroName _{\cmdWCP@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Row offset:} & \cmdWCP@var@relOffset \\ + \utt{Argument 1:} & \cmdWCP@var@argOneLo \\ + \end{array} \right] +} + \makeatother diff --git a/txn_data/_all_txn_data.tex b/txn_data/_all_txn_data.tex index 9c9fb022..95dd06f1 100644 --- a/txn_data/_all_txn_data.tex +++ b/txn_data/_all_txn_data.tex @@ -1,7 +1,8 @@ \documentclass[fleqn]{article} \usepackage[dvipsnames]{xcolor} +\usepackage{xkeyval} +\usepackage{../pkg/xkeyval_macros/wcp_calls} \usepackage{../pkg/common} -% \usepackage{../pkg/dark_theme} \usepackage{../pkg/std} \usepackage{../pkg/IEEEtrantools} \usepackage{../pkg/rom} diff --git a/txn_data/_inputs.tex b/txn_data/_inputs.tex index d1ea82bd..98e24949 100644 --- a/txn_data/_inputs.tex +++ b/txn_data/_inputs.tex @@ -12,8 +12,8 @@ \subsection{Graphical representation of data} \lab \subsection{Shorthands} \label{txn_data: constraints: shorthands} \input{shorthands} \subsection{Horizontalization for \rlpTxnMod{}} \label{txn_data: constraints: horizontalization rlpTxn} \input{horizontalization_rlp_txn} \subsection{\wcpFlag{}, \eucFlag{} and parametrized constraint systems} \label{txn_data: constraints: comparison constraints} \input{constraint_systems} -\subsection{Shared computations} \label{txn_data: constraints: common computations} \input{shared_computations} -\subsection{Specialized computations} \label{txn_data: constraints: specialized computations} \input{specialized_computations} +\subsection{Common computations} \label{txn_data: constraints: common computations} \input{computations/_common} +\subsection{Specialized computations} \label{txn_data: constraints: specialized computations} \input{computations/_specialized} \subsection{Setting certain variables} \label{txn_data: constraints: setting variables} \input{setting} \subsection{Horizontalization for \rlpTxnRcptMod{}} \label{txn_data: constraints: horizontalization rlpTxnRcpt} \input{horizontalization_rlp_txnrcpt} \subsection{Cumulative gas} \label{txn_data: constraints: cumulative gas} \input{cumulative} diff --git a/txn_data/_local.tex b/txn_data/_local.tex index e903b760..ce41cb64 100644 --- a/txn_data/_local.tex +++ b/txn_data/_local.tex @@ -6,70 +6,55 @@ \def\rZero {\redm{0}} \def\rOne {\redm{1}} -\def\MAX {\col{\_MAX}} -\def\locAbs {\col{ABS}} -\def\locAbsMax {\col{ABS}^\infty} -\def\block {\col{BLK}} -\def\locRel {\col{REL}} -\def\locRelMax {\col{REL}^\infty} -\def\locTxType {\col{tx\_type}} -\def\locToAddrHi {\col{[is\_dep ? 0 : to\_hi]}} -\def\locToAddrLo {\col{[is\_dep ? 0 : to\_lo]}} -\def\locNonce {\col{nonce}} -\def\locValue {\col{value}} -\def\locDataSize {\col{data\_size}} -\def\locDataCost {\col{data\_cost}} -\def\locGasLimit {\col{gas\_limit}} -\def\locIsDep {\col{is\_dep}} -\def\locGasPrice {\col{gas\_price}} -\def\locMaxFee {\col{max\_fee}} -\def\locMaximalGasPrice {\col{maximal\_gas\_price}} -\def\locGetFullTip {\col{get\_full\_tip}} -\def\locMaxPriorityFee {\col{max\_priority\_fee}} -\def\locNumAddr {\col{num\_addr}} -\def\locNumKeys {\col{num\_keys}} -\def\locUpfrontGasCost {\col{upfront\_gas\_cost}} -\def\locLegacyUpfrontGasCost {\col{legacy\_\locUpfrontGasCost}} -\def\locAccessUpfrontGasCost {\col{access\_\locUpfrontGasCost}} -\def\locXxxUpfrontGasCost {\col{xxx\_\locUpfrontGasCost}} -\def\locRefundLimit {\col{refund\_limit}} -\def\locGetFullRefund {\col{get\_full\_refund}} -\def\locExecutionGasCost {\col{execution\_gas\_cost}} -\def\locNonzeroDataSize {\col{nonzero\_data\_size}} -\def\fillCell {\cellcolor{gray}} +\def\MAX {\col{\_MAX}} +\def\locAbs {\col{ABS}} +\def\locAbsMax {\col{ABS}^\infty} +\def\block {\col{BLK}} +\def\locRel {\col{REL}} +\def\locRelMax {\col{REL}^\infty} +\def\locTxType {\col{tx\_type}} +\def\locToAddrHi {\col{[is\_dep ? 0 : to\_hi]}} +\def\locToAddrLo {\col{[is\_dep ? 0 : to\_lo]}} +\def\locNonce {\col{nonce}} +\def\locValue {\col{value}} +\def\locDataSize {\col{data\_size}} +\def\locDataCost {\col{data\_cost}} +\def\locGasLimit {\col{gas\_limit}} +\def\locIsDep {\col{is\_dep}} +\def\locGasPrice {\col{gas\_price}} +\def\locMaxFee {\col{max\_fee}} +\def\locMaximalGasPrice {\col{maximal\_gas\_price}} +\def\locGetFullTip {\col{get\_full\_tip}} +\def\locMaxPriorityFee {\col{max\_priority\_fee}} +\def\locNumAddr {\col{num\_addr}} +\def\locNumKeys {\col{num\_keys}} +\def\locUpfrontGasCost {\col{upfront\_gas\_cost}} +\def\locLegacyUpfrontGasCost {\col{legacy\_\locUpfrontGasCost}} +\def\locAccessUpfrontGasCost {\col{access\_\locUpfrontGasCost}} +\def\locXxxUpfrontGasCost {\col{xxx\_\locUpfrontGasCost}} +\def\locRefundLimit {\col{refund\_limit}} +\def\locGetFullRefund {\col{get\_full\_refund}} +\def\locRefundFromTransactionProcessing {\col{refund\_of\_processing}} +\def\locGasPaidAfterRefunds {\col{gas\_paid\_after\_refunds}} +\def\locPayFloorCost {\col{pay\_floor\_cost}} +\def\locExecutionGasCost {\col{execution\_gas\_cost}} +\def\locNonzeroDataSize {\col{nonzero\_data\_size}} +\def\fillCell {\cellcolor{gray}} \def\locTypeSum {\col{type\_sum}} -\def\nonceRowOffset {\yellowm{0}} -\def\balanceRowOffset {\yellowm{1}} -\def\gasLimitRowOffset {\yellowm{2}} -\def\maxRefundRowOffset {\yellowm{3}} -\def\effectiveRefundRowOffset {\yellowm{4}} -\def\detectingEmptyCallDataRowOffset {\yellowm{5}} -\def\maxFeeVsBaseFeeRowOffset {\yellowm{6}} -\def\maxFeeVsMaxPriorityFee {\yellowm{7}} -\def\effectiveGasPriceRowOffset {\yellowm{8}} - - -\newcommand{\smallCallToLt} [4] { - \texttt{smallCallToLT} _{#1} - \left[ \begin{array}{ll} - \utt{Row offset:} & #2 \\ - \utt{Argument 1:} & #3 \\ - \utt{Argument 2:} & #4 \\ - \end{array} \right]} - -\newcommand{\smallCallToLeq} [4] { - \texttt{smallCallToLEQ} _{#1} - \left[ \begin{array}{ll} - \utt{Row offset:} & #2 \\ - \utt{Argument 1:} & #3 \\ - \utt{Argument 2:} & #4 \\ - \end{array} \right]} - -\newcommand{\smallCallToIszero} [3] { - \texttt{smallCallToISZERO} _{#1} - \left[ \begin{array}{ll} - \utt{Row offset:} & #2 \\ - \utt{Argument 1:} & #3 \\ - \end{array} \right]} +\def\weightedTokenCount {\col{wght\_token\_count}} +\def\locTransactionFloorCost {\col{txn\_floor\_cost}} +\def\locRefundFromTransactionFloorCost {\col{refund\_of\_floor\_cost}} + +\def\nonceRowOffset {\yellowm{0}} +\def\balanceRowOffset {\yellowm{1}} +\def\gasLimitRowOffset {\yellowm{2}} +\def\transactionFloorCostRowOffset {\yellowm{3}} +\def\maxRefundRowOffset {\yellowm{4}} +\def\effectiveRefundRowOffset {\yellowm{5}} +\def\effectiveRefundVsTransactionFloorCostRowOffset {\yellowm{6}} +\def\detectingEmptyCallDataRowOffset {\yellowm{7}} +\def\maxFeeVsBaseFeeRowOffset {\yellowm{8}} +\def\maxFeeVsMaxPriorityFee {\yellowm{9}} +\def\effectiveGasPriceRowOffset {\yellowm{10}} diff --git a/txn_data/computations/_common.tex b/txn_data/computations/_common.tex new file mode 100644 index 00000000..49c28061 --- /dev/null +++ b/txn_data/computations/_common.tex @@ -0,0 +1,16 @@ +\begin{center} + \boxed{\text{The constraints below assume that } \locAbs_{i} \neq \locAbs_{i - 1}.} +\end{center} +The present section constrains the columns that offload comparisons to the \wcpMod{} module. +The following constraints hold for all transaction types: +\begin{description} + \input{computations/eip-2681/max_nonce_check} + \input{computations/balance_must_cover_value_and_gas} + \input{computations/gas_limit_must_cover_upfront_gas_cost} + \input{computations/eip-7623/gas_limit_must_cover_transaction_floor_cost} + \input{computations/refunds_upper_limit} + \input{computations/refunds_effective} + \input{computations/eip-7623/refunds_vs_floor_cost} + \input{computations/call_data_emptyness_check} + \input{computations/max_gas_price_vs_basefee} +\end{description} diff --git a/txn_data/computations/_specialized.tex b/txn_data/computations/_specialized.tex new file mode 100644 index 00000000..8ac27e18 --- /dev/null +++ b/txn_data/computations/_specialized.tex @@ -0,0 +1,13 @@ +\begin{center} + \boxed{\text{The constraints below assume that } + \left\{ \begin{array}{lcl} + \locAbs_{i} & \neq & \locAbs_{i - 1} \\ + \txIsTypeTwo_{i} & = & 1 \\ + \end{array} \right.} +\end{center} +The following constraints apply to type 2 transactions only: +\begin{description} + \input{computations/eip-1559/max_fee_vs_max_priority_fee} + \input{computations/eip-1559/effective_gas_price} +\end{description} + diff --git a/txn_data/computations/balance_must_cover_value_and_gas.tex b/txn_data/computations/balance_must_cover_value_and_gas.tex new file mode 100644 index 00000000..143f3e81 --- /dev/null +++ b/txn_data/computations/balance_must_cover_value_and_gas.tex @@ -0,0 +1,24 @@ +\item[\underline{\underline{Row n$^\circ(i + \balanceRowOffset)$: initial balance must cover value and gas:}}] + we impose that + \[ + \left\{\begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \balanceRowOffset , + argOneLo = \locValue + \locMaxFee \cdot \locGasLimit , + argTwoLo = \txInitialBalance _{i} , + } + % {i}{\balanceRowOffset} + % {\locValue + \locMaxFee \cdot \locGasLimit} + % {\txInitialBalance_{i}} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \balanceRowOffset , + } + \\ + \end{array}\right. + \] + \saNote{} + In other words we require that $\locValue + \locMaxFee \cdot \locGasLimit \leq \txInitialBalance_{i}$. diff --git a/txn_data/computations/call_data_emptyness_check.tex b/txn_data/computations/call_data_emptyness_check.tex new file mode 100644 index 00000000..7b09d9de --- /dev/null +++ b/txn_data/computations/call_data_emptyness_check.tex @@ -0,0 +1,15 @@ +\item[\underline{\underline{Row n$°(i + \detectingEmptyCallDataRowOffset)$: detecting empty call data:}}] + \[ + \smallCallToIszero { + anchorRow = i , + relOffset = \detectingEmptyCallDataRowOffset , + argOneLo = \locDataSize , + } + % {i}{\detectingEmptyCallDataRowOffset} + % {\locDataSize} + \] + we further set + \[ + \locNonzeroDataSize \define 1 - \res_{i + \detectingEmptyCallDataRowOffset} + \] + diff --git a/txn_data/computations/eip-1559/effective_gas_price.tex b/txn_data/computations/eip-1559/effective_gas_price.tex new file mode 100644 index 00000000..93a42e87 --- /dev/null +++ b/txn_data/computations/eip-1559/effective_gas_price.tex @@ -0,0 +1,22 @@ +\item[\underline{\underline{Row n$°(i + \effectiveGasPriceRowOffset)$: computing the effective gas price:}}] + we impose that + \[ + \smallCallToLeq { + anchorRow = i , + relOffset = \effectiveGasPriceRowOffset , + argOneLo = \locMaxPriorityFee + \txBasefee , + argTwoLo = \locMaxFee , + } + % {i}{\effectiveGasPriceRowOffset} + % {\locMaxPriorityFee + \txBasefee} + % {\locMaxFee } + \] + and we define the following shorthand + \[ + \locGetFullTip \define \res_{i + \effectiveGasPriceRowOffset} + \] + \saNote{} + By construction + \[ + \locGetFullTip = 1 \iff \locMaxPriorityFee + \txBasefee \leq \locMaxFee + \] diff --git a/txn_data/computations/eip-1559/max_fee_vs_max_priority_fee.tex b/txn_data/computations/eip-1559/max_fee_vs_max_priority_fee.tex new file mode 100644 index 00000000..a7c39b34 --- /dev/null +++ b/txn_data/computations/eip-1559/max_fee_vs_max_priority_fee.tex @@ -0,0 +1,25 @@ +\item[\underline{\underline{Row n$°(i + \maxFeeVsMaxPriorityFee)$: comparing \locMaxFee{} and \locMaxPriorityFee{}:}}] + we impose that + \[ + \left\{ \begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \maxFeeVsMaxPriorityFee , + argOneLo = \locMaxPriorityFee , + argTwoLo = \locMaxFee , + } + % {i}{\maxFeeVsMaxPriorityFee} + % {\locMaxPriorityFee} + % {\locMaxFee} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxFeeVsMaxPriorityFee , + } + \\ + \end{array} \right. + \] + \saNote{} + The above thus enforces that + $\locMaxPriorityFee \leq \locMaxFee$. diff --git a/txn_data/computations/eip-2681/max_nonce_check.tex b/txn_data/computations/eip-2681/max_nonce_check.tex new file mode 100644 index 00000000..0ebfefff --- /dev/null +++ b/txn_data/computations/eip-2681/max_nonce_check.tex @@ -0,0 +1,26 @@ +\item[\underline{\underline{Row n$^\circ(i + \nonceRowOffset)$: $\maxNonce$ upper bound check:}}] + we impose that + \[ + \left\{\begin{array}{l} + \smallCallToLt { + anchorRow = i , + relOffset = \nonceRowOffset , + argOneLo = \txNonce_{i} , + argTwoLo = \maxNonce , + } + % {i}{\nonceRowOffset} + % {\txNonce_{i}} + % {\maxNonce} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \nonceRowOffset , + } + \\ + \end{array}\right. + \] + where, as per \cite{EIP-2681}, $\maxNonce \define 2^{64} - 1$. + + \saNote{} + In other words we require that $\txNonce_{i} < \maxNonce$. diff --git a/txn_data/computations/eip-7623/gas_limit_must_cover_transaction_floor_cost.tex b/txn_data/computations/eip-7623/gas_limit_must_cover_transaction_floor_cost.tex new file mode 100644 index 00000000..2d4c4444 --- /dev/null +++ b/txn_data/computations/eip-7623/gas_limit_must_cover_transaction_floor_cost.tex @@ -0,0 +1,62 @@ +\item[\underline{\underline{Row n$°(i + \transactionFloorCostRowOffset)$: gas limit must cover the transaction floor cost:}}] + we introduce the following shorthand plus constraint + \[ + \left\{ \begin{array}{lcl} + \multicolumn{3}{l}{\standardTokenCost \cdot \locTransactionFloorCost = \floorTokenCost \cdot \locDataCost } \vspace{2mm} \\ + \standardTokenCost & \define & \standardTokenCostValue \\ + \floorTokenCost & \define & \floorTokenCostValue \\ + \locTransactionFloorCost & \define & \argOneLo _{i + \transactionFloorCostRowOffset} \\ + \locRefundFromTransactionFloorCost & \define & \locGasLimit - \locTransactionFloorCost \\ + \end{array} \right. + \] + and we impose + \[ + \left\{ \begin{array}{lcl} + \smallCallToLeq { + anchorRow = i , + relOffset = \transactionFloorCostRowOffset , + argOneLo = \locTransactionFloorCost , + argTwoLo = \locGasLimit , + } + % {i}{\transactionFloorCostRowOffset} + % {\locTransactionFloorCost} + % {\locGasLimit} + \vspace{2mm} \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \transactionFloorCostRowOffset , + } \\ + \end{array} \right. + \] + In other words we are requiring $\locTransactionFloorCost \leq \locGasLimit$. + + \saNote{} + We explain the rationale behind the first constraint. + Starting with \cite{EIP-7623} transaction call data induces a ``\textbf{transaction floor price}'' which has to be covered by the transaction's \textbf{gas limit}. + That floor price (and the usual call data cost) is defined like so + \[ + \left\{ \begin{array}{lcr} + \locTransactionFloorCost & \define & \standardTokenCost \cdot \weightedTokenCount \\ + \locDataCost & \define & \floorTokenCost \cdot \weightedTokenCount \vspace{2mm} \\ + \weightedTokenCount & \define & \multicolumn{1}{l}{\displaystyle \sum_{i \in T_\textbf{i}, T_\textbf{d}} ~ + \begin{cases} + ~ 1 & \text{if } i = 0 \\ + ~ 4 & \text{otherwise} \\ + \end{cases}} + \end{array} \right. + \] + Where we use \cite{EYP} notations: + the call data $T_\textbf{d}$ for message call transactions and + the init code $T_\textbf{i}$ for deployment transactions. + Thus, by requiring + \[ + \standardTokenCost \cdot \locTransactionFloorCost = \floorTokenCost \cdot \locDataCost + \] + we are effectively imposing + \[ + \begin{array}{lcl} + \locTransactionFloorCost + & = & \displaystyle \frac{\floorTokenCost}{\standardTokenCost} \cdot \locDataCost \vspace{2mm} \\ + & = & \displaystyle \floorTokenCost \cdot \weightedTokenCount \\ + \end{array} + \] diff --git a/txn_data/computations/eip-7623/refunds_vs_floor_cost.tex b/txn_data/computations/eip-7623/refunds_vs_floor_cost.tex new file mode 100644 index 00000000..1b3ff228 --- /dev/null +++ b/txn_data/computations/eip-7623/refunds_vs_floor_cost.tex @@ -0,0 +1,26 @@ +\item[\underline{\underline{Row n$°(i + \effectiveRefundVsTransactionFloorCostRowOffset)$: comparing effective refund to transaction floor cost:}}] + we impose that + \[ + \left\{ \begin{array}{lcl} + \multicolumn{3}{l}{% + \smallCallToLt { + anchorRow = i , + relOffset = \effectiveRefundVsTransactionFloorCostRowOffset , + argOneLo = \locGasPaidAfterRefunds , + argTwoLo = \locTransactionFloorCost , + }} + % {i}{\effectiveRefundVsTransactionFloorCostRowOffset} + % {\locGasPaidAfterRefunds} + % {\locTransactionFloorCost}} + \vspace{2mm} \\ + \locGasPaidAfterRefunds & \define & \locGasLimit - \locRefundFromTransactionProcessing \\ + \locPayFloorCost & \define & \res _{i + \effectiveRefundVsTransactionFloorCostRowOffset} \\ + \end{array} \right. + \] + In other words $\locPayFloorCost \equiv \texttt{true} \iff \big[ \locGasPaidAfterRefunds < \locTransactionFloorCost \big]$. + We further set + \begin{enumerate} + \item \If $\locPayFloorCost = 0$ \Then $\txEffectiveRefund _{i} = \locRefundFromTransactionProcessing$ + \item \If $\locPayFloorCost = 1$ \Then $\txEffectiveRefund _{i} = \locRefundFromTransactionFloorCost$ + \end{enumerate} + diff --git a/txn_data/computations/gas_limit_must_cover_upfront_gas_cost.tex b/txn_data/computations/gas_limit_must_cover_upfront_gas_cost.tex new file mode 100644 index 00000000..708a14b0 --- /dev/null +++ b/txn_data/computations/gas_limit_must_cover_upfront_gas_cost.tex @@ -0,0 +1,62 @@ +\item[\underline{\underline{Row n$°(i + \gasLimitRowOffset)$: gas limit must cover the upfront gas cost:}}] + we impose that + \[ + \left\{\begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \gasLimitRowOffset , + argOneLo = \locUpfrontGasCost , + argTwoLo = \locGasLimit , + } + % {i}{\gasLimitRowOffset} + % {\locUpfrontGasCost} + % {\locGasLimit} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \gasLimitRowOffset , + } + \\ + \end{array}\right. + \] + where, in order to define the transaction's upfront gas cost \locUpfrontGasCost{} + we must distinguish between transaction types that support access sets (types 1 and 2) and those that do not (type 0) + \[ + \left\{ \begin{array}{lcl} + \locUpfrontGasCost & \define & + \left[ \begin{array}{crcl} + + \!\!\! & \txIsLegacy _{i} & \cdot & \locLegacyUpfrontGasCost \\ + + \!\!\! & \txIsAccessSet _{i} & \cdot & \locAccessUpfrontGasCost \\ + + \!\!\! & \txIsTypeTwo _{i} & \cdot & \locAccessUpfrontGasCost \\ + \end{array} \right] \vspace{4mm} \\ + \locLegacyUpfrontGasCost & \define & + \left[ \begin{array}{crcl} + + \!\!\! & & & \locDataCost \\ + + \!\!\! & & & G_{\text{transaction}} \\ + + \!\!\! & \locIsDep & \cdot & G_{\text{txcreate}} \\ + \end{array} \right] \vspace{4mm} \\ + \locAccessUpfrontGasCost & \define & + \left[ \begin{array}{crcl} + + \!\!\! & & & \locDataCost \\ + + \!\!\! & & & G_{\text{transaction}} \\ + + \!\!\! & \locIsDep & \!\!\! \cdot \!\!\! & G_{\text{txcreate}} \\ + + \!\!\! & \locNumAddr & \!\!\! \cdot \!\!\! & G_\text{accesslistaddress} \\ + + \!\!\! & \locNumKeys & \!\!\! \cdot \!\!\! & G_\text{accessliststorage} \\ + \end{array} \right] \\ + \end{array} \right. + \] + \saNote{} + In other words we require that + $\locUpfrontGasCost \leq \locGasLimit$. + + \saNote{} + We remind the reader of the values of the following constants + \[ + \left\{ \begin{array}{lcr} + G_\text{transaction} & \!\!\! = \!\!\! & 21\,000 \\ + G_\text{create} & \!\!\! = \!\!\! & 32\,000 \\ + G_\text{accesslistaddress} & \!\!\! = \!\!\! & 2\,400 \\ + G_\text{accessliststorage} & \!\!\! = \!\!\! & 1\,900 \\ + \end{array} \right. + \] diff --git a/txn_data/computations/max_gas_price_vs_basefee.tex b/txn_data/computations/max_gas_price_vs_basefee.tex new file mode 100644 index 00000000..e4eb974e --- /dev/null +++ b/txn_data/computations/max_gas_price_vs_basefee.tex @@ -0,0 +1,35 @@ +\item[\underline{\underline{Row n$°(i + \maxFeeVsBaseFeeRowOffset)$: comparing the maximum gas price and \txBasefee{}:}}] + we impose that + \[ + \left\{ \begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \maxFeeVsBaseFeeRowOffset , + argOneLo = \txBasefee , + argTwoLo = \locMaximalGasPrice , + } + % {i}{\maxFeeVsBaseFeeRowOffset} + % {\txBasefee} + % {\locMaximalGasPrice} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxFeeVsBaseFeeRowOffset , + } + \\ + \end{array} \right. + \] + where we set + \[ + \locMaximalGasPrice \define + \left[ \begin{array}{clcl} + + \!\!\! & \txIsLegacy _{i} & \cdot & \locGasPrice \\ + + \!\!\! & \txIsAccessSet _{i} & \cdot & \locGasPrice \\ + + \!\!\! & \txIsTypeTwo _{i} & \cdot & \locMaxFee \\ + \end{array} \right] + \] + \saNote{} + In other words we require that + $\txBasefee \leq \locMaximalGasPrice$. + diff --git a/txn_data/computations/refunds_effective.tex b/txn_data/computations/refunds_effective.tex new file mode 100644 index 00000000..ce9a84d1 --- /dev/null +++ b/txn_data/computations/refunds_effective.tex @@ -0,0 +1,26 @@ +\item[\underline{\underline{Row n$°(i + \effectiveRefundRowOffset)$: effective refund:}}] + we impose that + \[ + \smallCallToLt { + anchorRow = i , + relOffset = \effectiveRefundRowOffset , + argOneLo = \txFinalRefundCounter_{i} , + argTwoLo = \locRefundLimit , + } + % {i}{\effectiveRefundRowOffset} + % {\txFinalRefundCounter _{i}} + % {\locRefundLimit} + \] + and define the following shorthands + \begin{enumerate} + \item $\locGetFullRefund \define \res_{i + \effectiveRefundRowOffset}$ + \item \If $\locGetFullRefund = 0$ \Then $\locRefundFromTransactionProcessing \define \txLeftoverGas _{i} + \locRefundLimit$ + \item \If $\locGetFullRefund = 1$ \Then $\locRefundFromTransactionProcessing \define \txLeftoverGas _{i} + \txFinalRefundCounter _{i}$ + \end{enumerate} + \saNote{} + The interpretation is as follows: + \begin{IEEEeqnarray*}{LCL} + \locGetFullRefund = 1 & \iff & \txFinalRefundCounter _{i} < \locRefundLimit \\ + & \iff & \txFinalRefundCounter _{i} < \left\lfloor\frac{\locGasLimit - \txLeftoverGas_{i}}\maxRefundQuotient\right\rfloor \\ + \end{IEEEeqnarray*} + diff --git a/txn_data/computations/refunds_upper_limit.tex b/txn_data/computations/refunds_upper_limit.tex new file mode 100644 index 00000000..066b7f73 --- /dev/null +++ b/txn_data/computations/refunds_upper_limit.tex @@ -0,0 +1,21 @@ +\item[\underline{\underline{Row n$°(i + \maxRefundRowOffset)$: upper limit for refunds:}}] + we impose that + \[ + \callToEuc + {i}{\maxRefundRowOffset} + {\locExecutionGasCost} + {\maxRefundQuotient} + \] + where we set / have used the following shorthands + \[ + \left\{ \begin{array}{lcl} + \locExecutionGasCost & \define & \locGasLimit - \txLeftoverGas_{i} \\ + \locRefundLimit & \define & \res_{i + \maxRefundRowOffset} \\ + \end{array} \right. + \] + where we have set + \[ + \maxRefundQuotient \define 5 + \] + \saNote{} + By construction $\locRefundLimit \equiv \displaystyle \left\lfloor\frac{\locExecutionGasCost}\maxRefundQuotient\right\rfloor$. diff --git a/txn_data/constraint_systems.tex b/txn_data/constraint_systems.tex index 2f4ad340..a5215498 100644 --- a/txn_data/constraint_systems.tex +++ b/txn_data/constraint_systems.tex @@ -7,10 +7,15 @@ We define parametrized constraint families to deal with setting comparisons \[ \left\{ \begin{array}{lcl} - \smallCallToLt - {i}{\relof} - {\col{arg\_1}} - {\col{arg\_2}} + \smallCallToLt { + anchorRow = i , + relOffset = \relof , + argOneLo = \col{arg\_1} , + argTwoLo = \col{arg\_2} , + } + % {i}{\relof} + % {\col{arg\_1}} + % {\col{arg\_2}} & \iff & \left\{ \begin{array}{lcl} \wcpFlag _{i + \relof} & = & \rOne \\ @@ -20,10 +25,15 @@ \INST _{i + \relof} & = & \inst{LT} \\ \end{array} \right. \vspace{2mm} \\ - \smallCallToLeq - {i}{\relof} - {\col{arg\_1}} - {\col{arg\_2}} + \smallCallToLeq { + anchorRow = i , + relOffset = \relof , + argOneLo = \col{arg\_1} , + argTwoLo = \col{arg\_2} , + } + % {i}{\relof} + % {\col{arg\_1}} + % {\col{arg\_2}} & \iff & \left\{ \begin{array}{lcl} \wcpFlag _{i + \relof} & = & \rOne \\ @@ -33,9 +43,13 @@ \INST _{i + \relof} & = & \inst{LEQ} \\ \end{array} \right. \vspace{2mm} \\ - \smallCallToIszero - {i}{\relof} - {\col{arg\_1}} + \smallCallToIszero { + anchorRow = i , + relOffset = \relof , + argOneLo = \col{arg\_1} , + } + % {i}{\relof} + % {\col{arg\_1}} & \iff & \left\{ \begin{array}{lcl} \wcpFlag _{i + \relof} & = & \rOne \\ @@ -59,10 +73,14 @@ \resultMustBeFalse { anchorRow = i , relOffset = \relof , - } & \iff & \res _{i + \relof} = \rZero \\ + } + & \iff & + \res _{i + \relof} = \rZero \\ \resultMustBeTrue { anchorRow = i , relOffset = \relof , - } & \iff & \res _{i + \relof} = \rOne \\ + } + & \iff & + \res _{i + \relof} = \rOne \\ \end{array} \right. \] diff --git a/txn_data/cumulative.tex b/txn_data/cumulative.tex index 35f921f5..c926c644 100644 --- a/txn_data/cumulative.tex +++ b/txn_data/cumulative.tex @@ -20,54 +20,69 @@ \begin{enumerate}[resume] \item \If $\locAbs_{i} \neq \locAbs_{i - 1}$ \et $\isLastTxOfBlock_{i} = 1$: - \begin{enumerate} - \item \If $\txIsLegacy_{i} = 1$ \Then: - \[ - \left\{ \begin{array}{l} - \smallCallToLeq - {i}{\maxCtTypeZero + 1} - {\txCumulativeConsumedGas} - {\blockGasLimit} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \maxCtTypeZero + 1 , - } - \\ - \end{array} \right. - \] - \item \If $\txIsAccessSet_{i} = 1$ \Then: - \[ - \left\{ \begin{array}{l} - \smallCallToLeq - {i}{\maxCtTypeOne + 1} - {\txCumulativeConsumedGas} - {\blockGasLimit} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \maxCtTypeOne + 1 , - } - \\ - \end{array} \right. - \] - \item \If $\txIsTypeTwo_{i} = 1$ \Then: - \[ - \left\{ \begin{array}{l} - \smallCallToLeq - {i}{\maxCtTypeTwo + 1} - {\txCumulativeConsumedGas} - {\blockGasLimit} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \maxCtTypeTwo + 1 , - } - \\ - \end{array} \right. - \] + \begin{enumerate} + \item \If $\txIsLegacy_{i} = 1$ \Then: + \[ + \left\{ \begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \maxCtTypeZero + 1 , + argOneLo = \txCumulativeConsumedGas , + argTwoLo = \blockGasLimit , + } + % {i}{\maxCtTypeZero + 1} + % {\txCumulativeConsumedGas} + % {\blockGasLimit} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeZero + 1 , + } + \\ + \end{array} \right. + \] + \item \If $\txIsAccessSet_{i} = 1$ \Then: + \[ + \left\{ \begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \maxCtTypeOne + 1 , + argOneLo = \txCumulativeConsumedGas , + argTwoLo = \blockGasLimit , + } + % {i}{\maxCtTypeOne + 1} + % {\txCumulativeConsumedGas} + % {\blockGasLimit} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeOne + 1 , + } + \\ + \end{array} \right. + \] + \item \If $\txIsTypeTwo_{i} = 1$ \Then: + \[ + \left\{ \begin{array}{l} + \smallCallToLeq { + anchorRow = i , + relOffset = \maxCtTypeTwo + 1 , + argOneLo = \txCumulativeConsumedGas , + argTwoLo = \blockGasLimit , + } + % {i}{\maxCtTypeTwo + 1} + % {\txCumulativeConsumedGas} + % {\blockGasLimit} + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeTwo + 1 , + } + \\ + \end{array} \right. + \] + \end{enumerate} \end{enumerate} -\end{enumerate} diff --git a/txn_data/heartbeat.tex b/txn_data/heartbeat.tex index f906e2cb..6c58fe76 100644 --- a/txn_data/heartbeat.tex +++ b/txn_data/heartbeat.tex @@ -14,17 +14,17 @@ \item \If $\txIsLegacy_{i} = 1$ \Then \begin{enumerate} \item \If $\ct_{i} \neq \maxCtTypeZero + \isLastTxOfBlock_{i}$ \Then $\ct_{i + 1} = 1 + \ct_{i}$; - \item \If $\ct_{i} = \maxCtTypeZero + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; + \item \If $\ct_{i} = \maxCtTypeZero + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; \end{enumerate} \item \If $\txIsAccessSet_{i} = 1$ \Then \begin{enumerate} \item \If $\ct_{i} \neq \maxCtTypeOne + \isLastTxOfBlock_{i}$ \Then $\ct_{i + 1} = 1 + \ct_{i}$; - \item \If $\ct_{i} = \maxCtTypeOne + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; + \item \If $\ct_{i} = \maxCtTypeOne + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; \end{enumerate} \item \If $\txIsTypeTwo_{i} = 1$ \Then \begin{enumerate} \item \If $\ct_{i} \neq \maxCtTypeTwo + \isLastTxOfBlock_{i}$ \Then $\ct_{i + 1} = 1 + \ct_{i}$; - \item \If $\ct_{i} = \maxCtTypeTwo + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; + \item \If $\ct_{i} = \maxCtTypeTwo + \isLastTxOfBlock_{i}$ \Then $\locAbs_{i + 1} = 1 + \locAbs_{i}$; \end{enumerate} \end{enumerate} \saNote{} The last transaction of a block requires one more row. diff --git a/txn_data/shared_computations.tex b/txn_data/shared_computations.tex deleted file mode 100644 index 00b77fca..00000000 --- a/txn_data/shared_computations.tex +++ /dev/null @@ -1,184 +0,0 @@ -\begin{center} - \boxed{\text{The constraints below assume that } \locAbs_{i} \neq \locAbs_{i - 1}.} -\end{center} -The present section constrains the columns that offload comparisons to the \wcpMod{} module. -The following constraints hold for all transaction types: -\begin{description} - \item[\underline{\underline{Row n$^\circ(i + \nonceRowOffset)$: Initial nonce check:}}] - we impose that - \[ - \left\{\begin{array}{l} - \smallCallToLt - {i}{\nonceRowOffset} - {\txNonce_{i}} - {\maxNonce} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \nonceRowOffset , - } - \\ - \end{array}\right. - \] - where, as per \cite{EIP2681}, $\maxNonce \define 2^{64} - 1$. - - \saNote{} - In other words we require that $\txNonce_{i} < \maxNonce$. - \item[\underline{\underline{Row n$^\circ(i + \balanceRowOffset)$: Initial balance check:}}] - we impose that - \[ - \left\{\begin{array}{l} - \smallCallToLeq - {i}{\balanceRowOffset} - {\locValue + \locMaxFee \cdot \locGasLimit} - {\txInitialBalance_{i}} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \balanceRowOffset , - } - \\ - \end{array}\right. - \] - \saNote{} - In other words we require that $\locValue + \locMaxFee \cdot \locGasLimit \leq \txInitialBalance_{i}$. - \item[\underline{\underline{Row n$°(i + \gasLimitRowOffset)$: Sufficient gas limit:}}] - we impose that - \[ - \left\{\begin{array}{l} - \smallCallToLeq - {i}{\gasLimitRowOffset} - {\locUpfrontGasCost} - {\locGasLimit} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \gasLimitRowOffset , - } - \\ - \end{array}\right. - \] - where, in order to define the transaction's upfront gas cost \locUpfrontGasCost{} - we must distinguish between transaction types that support access sets (types 1 and 2) and those that do not (type 0) - \[ - \left\{ \begin{array}{lcl} - \locUpfrontGasCost & \define & - \left[ \begin{array}{crcl} - + \!\!\! & \txIsLegacy _{i} & \cdot & \locLegacyUpfrontGasCost \\ - + \!\!\! & \txIsAccessSet _{i} & \cdot & \locAccessUpfrontGasCost \\ - + \!\!\! & \txIsTypeTwo _{i} & \cdot & \locAccessUpfrontGasCost \\ - \end{array} \right] \vspace{4mm} \\ - \locLegacyUpfrontGasCost & \define & - \left[ \begin{array}{crcl} - + \!\!\! & & & \locDataCost \\ - + \!\!\! & & & G_{\text{transaction}} \\ - + \!\!\! & \locIsDep & \cdot & G_{\text{txcreate}} \\ - \end{array} \right] \vspace{4mm} \\ - \locAccessUpfrontGasCost & \define & - \left[ \begin{array}{crcl} - + \!\!\! & & & \locDataCost \\ - + \!\!\! & & & G_{\text{transaction}} \\ - + \!\!\! & \locIsDep & \!\!\! \cdot \!\!\! & G_{\text{txcreate}} \\ - + \!\!\! & \locNumAddr & \!\!\! \cdot \!\!\! & G_\text{accesslistaddress} \\ - + \!\!\! & \locNumKeys & \!\!\! \cdot \!\!\! & G_\text{accessliststorage} \\ - \end{array} \right] \\ - \end{array} \right. - \] - \saNote{} - In other words we require that - $\locUpfrontGasCost \leq \locGasLimit$. - - \saNote{} - We remind the reader of the values of the following constants - \[ - \left\{ \begin{array}{lcr} - G_\text{transaction} & \!\!\! = \!\!\! & 21\,000 \\ - G_\text{create} & \!\!\! = \!\!\! & 32\,000 \\ - G_\text{accesslistaddress} & \!\!\! = \!\!\! & 2\,400 \\ - G_\text{accessliststorage} & \!\!\! = \!\!\! & 1\,900 \\ - \end{array} \right. - \] - \item[\underline{\underline{Row n$°(i + \maxRefundRowOffset)$: Upper limit for refunds:}}] - we impose that - \[ - \callToEuc - {i}{\maxRefundRowOffset} - {\locExecutionGasCost} - {\maxRefundQuotient} - \] - where we set / have used the following shorthands - \[ - \left\{ \begin{array}{lcl} - \locExecutionGasCost & \define & \locGasLimit - \txLeftoverGas_{i} \\ - \locRefundLimit & \define & \res_{i + \maxRefundRowOffset} \\ - \end{array} \right. - \] - where we have set - \[ - \maxRefundQuotient = 5 - \] - \saNote{} - By construction $\locRefundLimit \equiv \displaystyle \left\lfloor\frac{\locExecutionGasCost}\maxRefundQuotient\right\rfloor$. - \item[\underline{\underline{Row n$°(i + \effectiveRefundRowOffset)$: Effective refund:}}] - we impose that - \[ - \smallCallToLt - {i}{\effectiveRefundRowOffset} - {\txFinalRefundCounter _{i}} - {\locRefundLimit} - \] - and define the following shorthand - \[ - \locGetFullRefund - \define - \res_{i + \effectiveRefundRowOffset} - \] - \saNote{} - The interpretation is as follows: - \begin{IEEEeqnarray*}{LCL} - \locGetFullRefund = 1 & \iff & \txFinalRefundCounter _{i} < \locRefundLimit \\ - & \iff & \txFinalRefundCounter _{i} < \left\lfloor\frac{\locGasLimit - \txLeftoverGas_{i}}\maxRefundQuotient\right\rfloor \\ - \end{IEEEeqnarray*} - \item[\underline{\underline{Row n$°(i + \detectingEmptyCallDataRowOffset)$: Detecting empty call data:}}] - \[ - \smallCallToIszero - {i}{\detectingEmptyCallDataRowOffset} - {\locDataSize} - \] - we further set - \[ - \locNonzeroDataSize \define 1 - \res_{i + \detectingEmptyCallDataRowOffset} - \] - \item[\underline{\underline{Row n$°(i + \maxFeeVsBaseFeeRowOffset)$: Comparing the maximum gas price and \txBasefee{}:}}] - we impose that - \[ - \left\{ \begin{array}{l} - \smallCallToLeq - {i}{\maxFeeVsBaseFeeRowOffset} - {\txBasefee} - {\locMaximalGasPrice} - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \maxFeeVsBaseFeeRowOffset , - } - \\ - \end{array} \right. - \] - where we set - \[ - \locMaximalGasPrice \define - \left[ \begin{array}{clcl} - + \!\!\! & \txIsLegacy _{i} & \cdot & \locGasPrice \\ - + \!\!\! & \txIsAccessSet _{i} & \cdot & \locGasPrice \\ - + \!\!\! & \txIsTypeTwo _{i} & \cdot & \locMaxFee \\ - \end{array} \right] - \] - \saNote{} - In other words we require that - $\txBasefee \leq \locMaximalGasPrice$. -\end{description} diff --git a/txn_data/specialized_computations.tex b/txn_data/specialized_computations.tex deleted file mode 100644 index e8bdd795..00000000 --- a/txn_data/specialized_computations.tex +++ /dev/null @@ -1,47 +0,0 @@ -\begin{center} - \boxed{\text{The constraints below assume that } - \left\{ \begin{array}{lcl} - \locAbs_{i} & \neq & \locAbs_{i - 1} \\ - \txIsTypeTwo_{i} & = & 1 \\ - \end{array} \right.} -\end{center} -The following constraints apply to type 2 transactions only: -\begin{description} - \item[\underline{\underline{Row n$°(i + \maxFeeVsMaxPriorityFee)$: Comparing \locMaxFee{} and \locMaxPriorityFee{}:}}] - we impose that - \[ - \left\{ \begin{array}{l} - \smallCallToLeq - {i}{\maxFeeVsMaxPriorityFee} - {\locMaxPriorityFee} - {\locMaxFee } - \vspace{2mm} - \\ - \resultMustBeTrue { - anchorRow = i , - relOffset = \maxFeeVsMaxPriorityFee , - } - \\ - \end{array} \right. - \] - \saNote{} - The above thus enforces that - $\locMaxPriorityFee \leq \locMaxFee$. - \item[\underline{\underline{Row n$°(i + \effectiveGasPriceRowOffset)$: Computing the effective gas price:}}] - we impose that - \[ - \smallCallToLeq - {i}{\effectiveGasPriceRowOffset} - {\locMaxPriorityFee + \txBasefee} - {\locMaxFee } - \] - and we define the following shorthand - \[ - \locGetFullTip \define \res_{i + \effectiveGasPriceRowOffset} - \] - \saNote{} - By construction - \[ - \locGetFullTip = 1 \iff \locMaxPriorityFee + \txBasefee \leq \locMaxFee - \] -\end{description}