From 115fbc96e17f02961be3fce154bc90604f62d6cb Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Tue, 28 Feb 2017 17:19:53 +0100 Subject: [PATCH 01/12] Interpret the signature (chain_id, 0, 0) as signed by 2^{256} - 1 but only when the gas price, the nonce and the value are all zero. --- Paper.tex | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Paper.tex b/Paper.tex index c73dcffd..8264f34b 100644 --- a/Paper.tex +++ b/Paper.tex @@ -1461,7 +1461,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} From 825980fa5b87a80857b80039c68042a37119dac4 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Tue, 28 Feb 2017 19:58:33 +0100 Subject: [PATCH 02/12] EIP86: preparation before adding CREATE_P2SH The function \Lambda now takes the new address as a parameter --- Paper.tex | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/Paper.tex b/Paper.tex index 8264f34b..6bcc3547 100644 --- a/Paper.tex +++ b/Paper.tex @@ -600,7 +600,7 @@ \subsection{Execution} 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 +609,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 +653,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:} @@ -1953,7 +1951,8 @@ \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}$ \\ +&&&& where $a$ is defined as in (\ref{eq:address_calc}) \\ &&&& $\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$ \\ From 6e4c4b62718e21390d1ee0c4f656cc194a2c69a3 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 1 Mar 2017 10:45:36 +0100 Subject: [PATCH 03/12] EIP86: add CREATE_P2SH --- Paper.tex | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Paper.tex b/Paper.tex index 6bcc3547..34530193 100644 --- a/Paper.tex +++ b/Paper.tex @@ -2026,6 +2026,11 @@ \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 CREATE\_P2SH} & 3 & 1 & Create a new account with associated code on an address calculated using the \\ +&&&& creator's address. \\ +&&&& Exactly equivalent to {\small CREATE} except: \\ +&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\big(I_a \cdot \mathbf{i}\big)\Big)$ \\ +\midrule 0xfe & {\small INVALID} & $\varnothing$ & $\varnothing$ & Designated invalid instruction. \\ \midrule 0xff & {\small SELFDESTRUCT} & 1 & 0 & Halt execution and register account for later deletion. \\ From 7f58e986898fa5e493fc6c656d086aaf67ec5ba3 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 1 Mar 2017 15:50:12 +0100 Subject: [PATCH 04/12] Stop incrementing the nonce for transactions from the account at 2^{256} - 1 --- Paper.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Paper.tex b/Paper.tex index 34530193..1c65612b 100644 --- a/Paper.tex +++ b/Paper.tex @@ -594,7 +594,11 @@ \subsection{Execution} \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 +\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$: From cc48ade6a0c44d268d6550771549f678d7a0ad2b Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 12 Apr 2017 16:28:23 +0200 Subject: [PATCH 05/12] Take comments --- Paper.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Paper.tex b/Paper.tex index 1c65612b..4d8e765b 100644 --- a/Paper.tex +++ b/Paper.tex @@ -613,7 +613,7 @@ \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. $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$: +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} @@ -2033,7 +2033,7 @@ \subsection{Instruction Set} 0xfb & {\small CREATE\_P2SH} & 3 & 1 & Create a new account with associated code on an address calculated using the \\ &&&& creator's address. \\ &&&& Exactly equivalent to {\small CREATE} except: \\ -&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\big(I_a \cdot \mathbf{i}\big)\Big)$ \\ +&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\big(I_a \cdot \mathtt{\tiny KEC}(\mathbf{i})\big)\Big)$ \\ \midrule 0xfe & {\small INVALID} & $\varnothing$ & $\varnothing$ & Designated invalid instruction. \\ \midrule From 06f3da772ea6f46e629f511b6c3e0e575d38bdaf Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Mon, 24 Apr 2017 17:12:44 +0200 Subject: [PATCH 06/12] EIP 86: the original CREATE instruction retains the original address computation --- Paper.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Paper.tex b/Paper.tex index 4d8e765b..c22b8e67 100644 --- a/Paper.tex +++ b/Paper.tex @@ -1956,7 +1956,7 @@ \subsection{Instruction Set} 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, 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}$ \\ -&&&& where $a$ is defined as in (\ref{eq:address_calc}) \\ +&&&& $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$ \\ From 242e0f7e2b7375423db209358e8a60e1684b341a Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Tue, 9 May 2017 17:03:50 +0200 Subject: [PATCH 07/12] EIP86: specify CREATE2 --- Paper.tex | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/Paper.tex b/Paper.tex index c22b8e67..076e8306 100644 --- a/Paper.tex +++ b/Paper.tex @@ -2030,10 +2030,22 @@ \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 CREATE\_P2SH} & 3 & 1 & Create a new account with associated code on an address calculated using the \\ -&&&& creator's address. \\ -&&&& Exactly equivalent to {\small CREATE} except: \\ -&&&& $a \equiv \mathcal{B}_{96..255}\Big(\mathtt{\tiny KEC}\big(I_a \cdot \mathtt{\tiny KEC}(\mathbf{i})\big)\Big)$ \\ +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$ 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 fulfill the balance transfer) or \\ +&&&& $\boldsymbol{\sigma}[a]_c \neq ()$ (a contract already exists); 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 From b7ce477fdff1d40e5faffeff31a5d2231c9d7bb8 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 10 May 2017 14:02:25 +0200 Subject: [PATCH 08/12] EIP86 rule 5 --- Paper.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Paper.tex b/Paper.tex index 076e8306..3ee8255d 100644 --- a/Paper.tex +++ b/Paper.tex @@ -713,16 +713,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^{**} Date: Wed, 10 May 2017 14:11:48 +0200 Subject: [PATCH 09/12] EIP86: when CREATE(2) destination is occupied, the return value is zero --- Paper.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Paper.tex b/Paper.tex index 3ee8255d..df0873f8 100644 --- a/Paper.tex +++ b/Paper.tex @@ -1962,7 +1962,7 @@ \subsection{Instruction Set} &&&& $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. \\ @@ -2042,7 +2042,8 @@ \subsection{Instruction Set} &&&& $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$ or $I_e = 1024$ (the maximum call depth limit is reached) or \\ +&&&& 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) or \\ &&&& $\boldsymbol{\sigma}[a]_c \neq ()$ (a contract already exists); otherwise $x = a$. \\ &&&& $\boldsymbol{\mu}'_i \equiv M(\boldsymbol{\mu}_i, \boldsymbol{\mu}_\mathbf{s}[2], \boldsymbol{\mu}_\mathbf{s}[3])$ \\ From ea7f1d29e7ad56cab40b73fdadbeea92770bd662 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 10 May 2017 15:49:15 +0200 Subject: [PATCH 10/12] Remove a spurious newline --- Paper.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Paper.tex b/Paper.tex index df0873f8..857eb678 100644 --- a/Paper.tex +++ b/Paper.tex @@ -594,8 +594,7 @@ \subsection{Execution} \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 & -\begin{cases} +\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} From cecee911570e31b5d3de56d1754f0f1d9e0d3ad2 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 10 May 2017 16:04:30 +0200 Subject: [PATCH 11/12] Small adjustments --- Paper.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Paper.tex b/Paper.tex index 857eb678..c990796e 100644 --- a/Paper.tex +++ b/Paper.tex @@ -593,8 +593,8 @@ \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 & \begin{cases} +\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} @@ -2043,8 +2043,8 @@ \subsection{Instruction Set} &&&& 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) or \\ -&&&& $\boldsymbol{\sigma}[a]_c \neq ()$ (a contract already exists); otherwise $x = a$. \\ +&&&& $\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 From a3fc31c5dfed4d6ae37fc84f39623cf1db1887e8 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Thu, 11 May 2017 15:33:36 +0200 Subject: [PATCH 12/12] The code is stored as its Keccak hash --- Paper.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Paper.tex b/Paper.tex index c990796e..e6610d31 100644 --- a/Paper.tex +++ b/Paper.tex @@ -722,7 +722,7 @@ \section{Contract Creation} \label{ch:create} \boldsymbol{\sigma}^{**} \quad \text{except:} & \\ \quad\boldsymbol{\sigma}'[a]_c = \texttt{\small KEC}(\mathbf{o}) & \text{otherwise} \end{cases} \\ -E(\boldsymbol{\sigma}, a) &\equiv \big(\boldsymbol{\sigma}[a] \neq \varnothing \wedge (\boldsymbol{\sigma}[a]_c \neq () \vee \boldsymbol{\sigma}[a]_n \neq 0)\big) +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.