[WIP] Metropolis: EIP86 account abstraction

Paper.tex

@@ -593,14 +593,17 @@ \subsection{Execution}
 We define the checkpoint state $\boldsymbol{\sigma}_0$:
 \begin{eqnarray}
 \boldsymbol{\sigma}_0 & \equiv & \boldsymbol{\sigma} \quad \text{except:} \\
-\boldsymbol{\sigma}_0[S(T)]_b & \equiv & \boldsymbol{\sigma}[S(T)]_b - T_g T_p \\
-\boldsymbol{\sigma}_0[S(T)]_n & \equiv & \boldsymbol{\sigma}[S(T)]_n + 1
+\qquad\boldsymbol{\sigma}_0[S(T)]_b & \equiv & \boldsymbol{\sigma}[S(T)]_b - T_g T_p \\
+\qquad\boldsymbol{\sigma}_0[S(T)]_n & \equiv & \begin{cases}
+\boldsymbol{\sigma}[S(T)]_n &\text{if}\ S(T) = 2^{256} - 1 \\
+\boldsymbol{\sigma}[S(T)]_n + 1 &\text{otherwise} \\
+\end{cases}
 \end{eqnarray}
 
 Evaluating $\boldsymbol{\sigma}_P$ from $\boldsymbol{\sigma}_0$ depends on the transaction type; either contract creation or message call; we define the tuple of post-execution provisional state $\boldsymbol{\sigma}_P$, remaining gas $g'$ and substate $A$:
 \begin{equation}
 (\boldsymbol{\sigma}_P, g', A) \equiv \begin{cases}
-\Lambda(\boldsymbol{\sigma}_0, S(T), T_o, &\\ \quad\quad g, T_p, T_v, T_\mathbf{i}, 0) & \text{if} \quad T_t = \varnothing \\
+\Lambda(\boldsymbol{\sigma}_0, S(T), T_o, &\\ \quad\quad g, T_p, T_v, T_\mathbf{i}, 0, a) & \text{if} \quad T_t = \varnothing \\
 \Theta_{3}(\boldsymbol{\sigma}_0, S(T), T_o, &\\ \quad\quad T_t, T_t, g, T_p, T_v, T_v, T_\mathbf{d}, 0) & \text{otherwise}
 \end{cases}
 \end{equation}
@@ -609,7 +612,12 @@ \subsection{Execution}
 \begin{equation}
 g \equiv T_g - g_0
 \end{equation}
-and $T_o$ is the original transactor, which can differ from the sender in the case of a message call or contract creation not directly triggered by a transaction but coming from the execution of EVM-code.
+and $T_o$ is the original transactor, which can differ from the sender in the case of a message call or contract creation not directly triggered by a transaction but coming from the execution of EVM-code. $a$ is the address of the created account, which is defined as the rightmost 160 bits of the Keccak hash of the RLP encoding of the structure containing only the sender and the nonce. Thus we define the resultant address for the new account $a$:
+\begin{equation}
+a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\Big(\mathtt{\tiny RLP}\big(\;(s, \boldsymbol{\sigma}_0[s]_n - 1)\;\big)\Big)\Big)
+\end{equation}
+
+where $\mathtt{\tiny KEC}$ is the Keccak 256-bit hash function, $\mathtt{\tiny RLP}$ is the RLP encoding function, $\mathcal{B}_{a..b}(X)$ evaluates to binary value containing the bits of indices in the range $[a, b]$ of the binary data $X$ and $\boldsymbol{\sigma}_0[x]$ is the account state of $x$ or $\varnothing$ if none exists. Note we use one fewer than the sender's nonce value; we assert that we have incremented the sender account's nonce prior to this call, and so the value used is the sender's nonce at the beginning of the responsible transaction or VM operation.
 
 Note we use $\Theta_{3}$ to denote the fact that only the first three components of the function's value are taken; the final represents the message-call's output value (a byte array) and is unused in the context of transaction evaluation.
 
@@ -648,16 +656,9 @@ \section{Contract Creation} \label{ch:create}
 
 We define the creation function formally as the function $\Lambda$, which evaluates from these values, together with the state $\boldsymbol{\sigma}$ to the tuple containing the new state, remaining gas and accrued transaction substate $(\boldsymbol{\sigma}', g', A)$, as in section \ref{ch:transactions}:
 \begin{equation}
-(\boldsymbol{\sigma}', g', A) \equiv \Lambda(\boldsymbol{\sigma}, s, o, g, p, v, \mathbf{i}, e)
+(\boldsymbol{\sigma}', g', A) \equiv \Lambda(\boldsymbol{\sigma}, s, o, g, p, v, \mathbf{i}, e, a)
 \end{equation}
 
-The address of the new account is defined as being the rightmost 160 bits of the Keccak hash of the RLP encoding of the structure containing only the sender and the nonce. Thus we define the resultant address for the new account $a$:
-\begin{equation}
-a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\Big(\mathtt{\tiny RLP}\big(\;(s, \boldsymbol{\sigma}[s]_n - 1)\;\big)\Big)\Big)
-\end{equation}
-
-where $\mathtt{\tiny KEC}$ is the Keccak 256-bit hash function, $\mathtt{\tiny RLP}$ is the RLP encoding function, $\mathcal{B}_{a..b}(X)$ evaluates to binary value containing the bits of indices in the range $[a, b]$ of the binary data $X$ and $\boldsymbol{\sigma}[x]$ is the address state of $x$ or $\varnothing$ if none exists. Note we use one fewer than the sender's nonce value; we assert that we have incremented the sender account's nonce prior to this call, and so the value used is the sender's nonce at the beginning of the responsible transaction or VM operation.
-
 The account's nonce is initially defined as zero, the balance as the value passed, the storage as empty and the code hash as the Keccak 256-bit hash of the empty string; the sender's balance is also reduced by the value passed. Thus the mutated state becomes $\boldsymbol{\sigma}^*$:
 \begin{equation}
 \boldsymbol{\sigma}^* \equiv \boldsymbol{\sigma} \quad \text{except:}
@@ -711,16 +712,17 @@ \section{Contract Creation} \label{ch:create}
 
 \begin{align}
 \quad g' &\equiv \begin{cases}
-0 & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \\
+0 & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \vee E(\boldsymbol{\sigma}, a) \\
 g^{**} & \text{if} \quad g^{**}<c \wedge H_i<\firsthomesteadblock \\
 g^{**} - c & \text{otherwise} \\
 \end{cases} \\
 \quad \boldsymbol{\sigma}' &\equiv  \begin{cases}
-\boldsymbol{\sigma} & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \\
+\boldsymbol{\sigma} & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \vee E(\boldsymbol{\sigma}, a) \\
 \boldsymbol{\sigma}^{**} & \text{if} \quad g^{**}<c \wedge H_i<\firsthomesteadblock \\
 \boldsymbol{\sigma}^{**} \quad \text{except:} & \\
 \quad\boldsymbol{\sigma}'[a]_c = \texttt{\small KEC}(\mathbf{o}) & \text{otherwise}
-\end{cases}
+\end{cases} \\
+E(\boldsymbol{\sigma}, a) &\equiv \big(\boldsymbol{\sigma}[a] \neq \varnothing \wedge (\boldsymbol{\sigma}[a]_c \neq \texttt{\small KEC}(()) \vee \boldsymbol{\sigma}[a]_n \neq 0)\big)
 \end{align}
 
 The exception in the determination of $\boldsymbol{\sigma}'$ dictates that $\mathbf{o}$, the resultant byte sequence from the execution of the initialisation code, specifies the final body code for the newly-created account.
@@ -1461,7 +1463,12 @@ \section{Signing Transactions}\label{app:signing}
 
 The assertion that the sender of a signed transaction equals the address of the signer should be self-evident:
 \begin{equation}
-\forall T: \forall p_r: S(G(T, p_r)) \equiv A(p_r)
+\forall T: \forall p_r: S(G(T, p_r)) \equiv A(p_r) \quad \text{ where } (T_w, T_r, T_s) \text{ is a valid signature.}
+\end{equation}
+
+When a transaction has a particular invalid signature and it has zero gas price, zero nonce and zero value, the sender of the transaction is $2^{256} - 1$.
+\begin{equation}
+\forall T: S(T) \equiv 2^{256} - 1 \quad \text{ where } \quad (T_w, T_r, T_s) = (\mathtt{chain\_id}, 0, 0) \,\wedge\, T_p = T_n = T_v = 0.
 \end{equation}
 
 \section{Fee Schedule}\label{app:fees}
@@ -1948,12 +1955,13 @@ \subsection{Instruction Set}
 \textbf{Value} & \textbf{Mnemonic} & $\delta$ & $\alpha$ & \textbf{Description} \vspace{5pt} \\
 0xf0 & {\small CREATE} & 3 & 1 & Create a new account with associated code. \\
 &&&& $\mathbf{i} \equiv \boldsymbol{\mu}_\mathbf{m}[ \boldsymbol{\mu}_\mathbf{s}[1] \dots (\boldsymbol{\mu}_\mathbf{s}[1] + \boldsymbol{\mu}_\mathbf{s}[2] - 1) ]$ \\
-&&&& $(\boldsymbol{\sigma}', \boldsymbol{\mu}'_g, A^+) \equiv \begin{cases}\Lambda(\boldsymbol{\sigma}^*, I_a, I_o, L(\boldsymbol{\mu}_g), I_p, \boldsymbol{\mu}_\mathbf{s}[0], \mathbf{i}, I_e + 1) & \text{if} \quad \boldsymbol{\mu}_\mathbf{s}[0] \leqslant \boldsymbol{\sigma}[I_a]_b \;\wedge\; I_e < 1024\\ \big(\boldsymbol{\sigma}, \boldsymbol{\mu}_g, \varnothing\big) & \text{otherwise} \end{cases}$ \\
+&&&& $(\boldsymbol{\sigma}', \boldsymbol{\mu}'_g, A^+) \equiv \begin{cases}\Lambda(\boldsymbol{\sigma}^*, I_a, I_o, L(\boldsymbol{\mu}_g), I_p, \boldsymbol{\mu}_\mathbf{s}[0], \mathbf{i}, I_e + 1, a) & \text{if} \quad \boldsymbol{\mu}_\mathbf{s}[0] \leqslant \boldsymbol{\sigma}[I_a]_b \;\wedge\; I_e < 1024\\ \big(\boldsymbol{\sigma}, \boldsymbol{\mu}_g, \varnothing\big) & \text{otherwise} \end{cases}$ \\
+&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\Big(\mathtt{\tiny RLP}\big(\;(I_a, \boldsymbol{\sigma}[I_a]_n - 1)\;\big)\Big)\Big)$ \\
 &&&& $\boldsymbol{\sigma}^* \equiv \boldsymbol{\sigma} \quad \text{except} \quad \boldsymbol{\sigma}^*[I_a]_n = \boldsymbol{\sigma}[I_a]_n + 1$ \\
 &&&& $A' \equiv A \Cup A^+$ which implies: $A'_\mathbf{s} \equiv A_\mathbf{s} \cup A^+_\mathbf{s} \quad \wedge \quad A'_\mathbf{l} \equiv A_\mathbf{l} \cdot A^+_\mathbf{l} \quad \wedge \quad A'_\mathbf{r} \equiv A_\mathbf{r} + A^+_\mathbf{r}$ \\
 &&&& $\boldsymbol{\mu}'_\mathbf{s}[0] \equiv x$ \\
 &&&& where $x=0$ if the code execution for this operation failed due to an exceptional halting \\
-&&&& $Z(\boldsymbol{\sigma}^*, \boldsymbol{\mu}, I) = \top$ or $I_e = 1024$ \\
+&&&& $Z(\boldsymbol{\sigma}^*, \boldsymbol{\mu}, I) = \top$, $E(\boldsymbol{\sigma}^*, a) = \top$ (the address is occupied) or $I_e = 1024$ \\
 &&&& (the maximum call depth limit is reached) or $\boldsymbol{\mu}_\mathbf{s}[0] > \boldsymbol{\sigma}[I_a]_b$ (balance of the caller is too \\
 &&&& low to fulfil the value transfer); and otherwise $x=A(I_a, \boldsymbol{\sigma}[I_a]_n)$, the address of the newly \\
 &&&& created account, otherwise. \\
@@ -2022,6 +2030,24 @@ \subsection{Instruction Set}
 &&&& This means that the recipient is in fact the same account as at present, simply\\
 &&&& that the code is overwritten {\it and} the context is almost entirely identical.\\
 \midrule
+0xfb & {\small CREATE2} & 4 & 1 & Create a new account with associated code on a predictable address. \\
+&&&& $\mathbf{i} \equiv \boldsymbol{\mu}_\mathbf{m}[\boldsymbol{\mu}_\mathbf{s}[2]..(\boldsymbol{\mu}_\mathbf{s}[2] + \boldsymbol{\mu}_\mathbf{s}[3] - 1)]$ \\
+&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\big(I_a\cdot \boldsymbol{\mu}_\mathbf{s}[1]\cdot \mathtt{\tiny KEC}(\mathbf i)\big)\Big)$ \\
+&&&& $(\boldsymbol{\sigma}', \boldsymbol{\mu}_g', A^+) \equiv \begin{cases}
+\begin{array}{l}\Lambda(\boldsymbol{\sigma}^*, I_a, I_o, L(\boldsymbol{\mu}_g), I_p, \\ \phantom{\Lambda(}\boldsymbol{\mu}_\mathbf{s}[0], \mathbf{i}, I_e + 1, a)\end{array} & \text{if}\begin{array}{l}(\boldsymbol{\sigma}^*[a]=\varnothing\vee\boldsymbol{\sigma}^*[a]_c=())\wedge\\\boldsymbol{\mu}_\mathbf{s}[0]\le\boldsymbol{\sigma}[I_a]_b\wedge I_e<1024\end{array}\\
+(\boldsymbol{\sigma},\boldsymbol{\mu}_g,\varnothing)&\text{otherwise}
+\end{cases}$ \\
+&&&& $\boldsymbol{\sigma}^*\equiv\boldsymbol{\sigma}$ except $\boldsymbol{\sigma}^*[I_a]_n=\boldsymbol{\sigma}[I_a]_n+1$ \\
+&&&& $A'\equiv A\Cup A^+$ (with $\Cup$ defined in the definition of {\small CREATE}) \\
+&&&& $\boldsymbol{\mu}'_\mathbf{s}[0] \equiv x$ \\
+&&&& where $x = 0$ if the code execution for this operation failed due to an exceptional \\
+&&&& halting $Z(\boldsymbol{\sigma}^*,\boldsymbol{\mu}, I) = \top$, $E(\boldsymbol{\sigma}, a) = \top$ (the address is already occupied) or \\
+&&&& $I_e = 1024$ (the maximum call depth limit is reached), \\
+&&&& $\boldsymbol{\mu}_\mathbf{s}[0] > \boldsymbol{\sigma}[I_a]_b$ (balance of the caller is too low to fulfill the balance transfer); \\
+&&&& otherwise $x = a$. \\
+&&&& $\boldsymbol{\mu}'_i \equiv M(\boldsymbol{\mu}_i, \boldsymbol{\mu}_\mathbf{s}[2], \boldsymbol{\mu}_\mathbf{s}[3])$ \\
+&&&& Thus the operand order is: value, salt, input offset, input size. \\
+\midrule
 0xfe & {\small INVALID} & $\varnothing$ & $\varnothing$ & Designated invalid instruction. \\
 \midrule
 0xff & {\small SELFDESTRUCT} & 1 & 0 & Halt execution and register account for later deletion. \\