EIP-7623: Increase calldata cost

_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)"
+```

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,14 @@
 \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{\standardTokenCost}         {\redm{\texttt{STANDARD\_TOKEN\_COST}}}
+\newcommand{\floorTokenCost}            {\redm{\texttt{FLOOR\_TOKEN\_COST}}}

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

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}

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}

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}}

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/max_nonce_check}
+		\input{computations/balance_must_cover_value_and_gas}
+		\input{computations/gas_limit_must_cover_upfront_gas_cost}
+		\input{computations/gas_limit_must_cover_transaction_floor_cost}
+		\input{computations/refunds_upper_limit}
+		\input{computations/refunds_effective}
+		\input{computations/refunds_vs_floor_cost}
+		\input{computations/call_data_emptyness_check}
+		\input{computations/max_gas_price_vs_basefee}
+\end{description}

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}
+

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}$.

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}
+	\]
+

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
+	\]

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$.