From b7a939a86857a647e176251c9d0308e506bd8519 Mon Sep 17 00:00:00 2001
From: Yoichi Hirai <i@yoichihirai.com>
Date: Mon, 20 Feb 2017 17:18:23 +0100
Subject: [PATCH] Define REVERT instruction

Fixes #232
---
 Paper.tex | 40 +++++++++++++++++++++++++++-------------
 1 file changed, 27 insertions(+), 13 deletions(-)

diff --git a/Paper.tex b/Paper.tex
index 87ba3880..787fc40d 100644
--- a/Paper.tex
+++ b/Paper.tex
@@ -704,9 +704,13 @@ \section{Contract Creation} \label{ch:create}
 Code execution depletes gas, and gas may not go below zero, thus execution may exit before the code has come to a natural halting state. In this (and several other) exceptional cases we say an out-of-gas (OOG) exception has occurred: The evaluated state is defined as being the empty set, $\varnothing$, and the entire create operation should have no effect on the state, effectively leaving it as it was immediately prior to attempting the creation.
 
 If the initialization code completes successfully, a final contract-creation cost is paid, the code-deposit cost, $c$, proportional to the size of the created contract's code:
-\begin{equation}
-c \equiv G_{codedeposit} \times |\mathbf{o}|
-\end{equation}
+\begin{eqnarray}
+ c & \equiv &
+ \begin{cases}
+  G_{codedeposit} \times |\mathbf{o}| & \text{if}\quad \boldsymbol{\sigma}^{**} \neq \varnothing \\
+  0 & \text{otherwise}
+ \end{cases}
+\end{eqnarray}
 
 If there is not enough gas remaining to pay this, \ie $g^{**} < c$, then we also declare an out-of-gas exception.
 
@@ -716,7 +720,8 @@ \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 \wedge \mathbf{o} = \varnothing \\
+g^{**} & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \wedge \mathbf{o} \neq \varnothing \\
 g^{**} & \text{if} \quad g^{**}<c \wedge H_i<\firsthomesteadblock \\
 g^{**} - c & \text{otherwise} \\
 \end{cases} \\
@@ -775,7 +780,8 @@ \section{Message Call} \label{ch:call}
 \boldsymbol{\sigma}^{**} & \text{otherwise}
 \end{cases} \\
 g' & \equiv & \begin{cases}
-0 & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \\
+0 & \text{if} \quad \boldsymbol{\sigma}^{**} = \varnothing \wedge
+               \mathbf{o} = \varnothing \\
 g^{**} & \text{otherwise}
 \end{cases} \\
 (\boldsymbol{\sigma}^{**}, g^{**}, \mathbf{s}, \mathbf{o}) & \equiv & \begin{cases}
@@ -845,7 +851,7 @@ \subsection{Execution Environment}
 
 \subsection{Execution Overview}
 
-We must now define the $\Xi$ function. In most practical implementations this will be modelled as an iterative progression of the pair comprising the full system state, $\boldsymbol{\sigma}$ and the machine state, $\boldsymbol{\mu}$. Formally, we define it recursively with a function $X$. This uses an iterator function $O$ (which defines the result of a single cycle of the state machine) together with functions $Z$ which determines if the present state is an exceptional halting state of the machine and $H$, specifying the output data of the instruction if and only if the present state is a normal halting state of the machine.
+We must now define the $\Xi$ function. In most practical implementations this will be modelled as an iterative progression of the pair comprising the full system state, $\boldsymbol{\sigma}$ and the machine state, $\boldsymbol{\mu}$. Formally, we define it recursively with a function $X$. This uses an iterator function $O$ (which defines the result of a single cycle of the state machine) together with functions $Z$ which determines if the present state is an exceptional halting state of the machine and $H$, specifying the output data of the instruction.
 
 The empty sequence, denoted $()$, is not equal to the empty set, denoted $\varnothing$; this is important when interpreting the output of $H$, which evaluates to $\varnothing$ when execution is to continue but a series (potentially empty) when execution should halt.
 \begin{eqnarray}
@@ -859,7 +865,7 @@ \subsection{Execution Overview}
 \begin{equation}
 X\big( (\boldsymbol{\sigma}, \boldsymbol{\mu}, A, I) \big) \equiv \begin{cases}
 \big(\varnothing, \boldsymbol{\mu}, A^0, I, ()\big) & \text{if} \quad Z(\boldsymbol{\sigma}, \boldsymbol{\mu}, I)\\
-O(\boldsymbol{\sigma}, \boldsymbol{\mu}, A, I) \cdot \mathbf{o} & \text{if} \quad \mathbf{o} \neq \varnothing\\
+O(\boldsymbol{\sigma}, \boldsymbol{\mu}, A, I) \cdot \mathbf{o} & \text{if} \quad \mathbf{o} \neq \varnothing \\
 X\big(O(\boldsymbol{\sigma}, \boldsymbol{\mu}, A, I)\big) & \text{otherwise}\\
 \end{cases}
 \end{equation}
@@ -902,7 +908,7 @@ \subsubsection{Exceptional Halting}
 \end{array}
 \end{equation}
 
-This states that the execution is in an exceptional halting state if there is insufficient gas, if the instruction is invalid (and therefore its $\delta$ subscript is undefined), if there are insufficient stack items, if a {\small JUMP}/{\small JUMPI} destination is invalid or the new stack size would be larger then 1024. The astute reader will realise that this implies that no instruction can, through its execution, cause an exceptional halt.
+This states that the execution is in an exceptional halting state if there is insufficient gas, if the instruction is invalid (and therefore its $\delta$ subscript is undefined), if there are insufficient stack items, if a {\small JUMP}/{\small JUMPI} destination is invalid or the new stack size would be larger then 1024.
 
 \subsubsection{Jump Destination Validity}
 
@@ -931,12 +937,13 @@ \subsubsection{Jump Destination Validity}
 i + 1 & \text{otherwise} \end{cases}
 \end{equation}
 
-\subsubsection{Normal Halting}
+\subsubsection{Post-Execution Halting}
 
-The normal halting function $H$ is defined:
-\begin{equation}
+The post-execution halting function $H$ is defined:
+\begin{equation} \label{eq:output}
 H(\boldsymbol{\mu}, I) \equiv \begin{cases}
-H_{\text{\tiny RETURN}}(\boldsymbol{\mu}) & \text{if} \quad w = \text{\small RETURN} \\
+H_{\text{\tiny RETURN}}(\boldsymbol{\mu}) & \text{if} \quad w \in
+                               \{\text{\small RETURN}, \text{\small REVERT}\}  \\
 () & \text{if} \quad w \in \{ \text{\small STOP}, \text{\small SELFDESTRUCT} \} \\
 \varnothing & \text{otherwise}
 \end{cases}
@@ -1567,7 +1574,7 @@ \subsection{Gas Cost}
 
 with $C_\text{\tiny CALL}$, $C_\text{\tiny SELFDESTRUCT}$ and $C_\text{\tiny SSTORE}$ as specified in the appropriate section below. We define the following subsets of instructions:
 
-$W_{zero}$ = \{{\small STOP}, {\small RETURN}\}
+$W_{zero}$ = \{{\small STOP}, {\small RETURN}, {\small REVERT}\}
 
 $W_{base}$ = \{{\small ADDRESS}, {\small ORIGIN}, {\small CALLER}, {\small CALLVALUE}, {\small CALLDATASIZE}, {\small CODESIZE}, {\small GASPRICE}, {\small COINBASE},\newline \noindent\hspace*{1cm} {\small TIMESTAMP}, {\small NUMBER}, {\small DIFFICULTY}, {\small GASLIMIT}, {\small POP}, {\small PC}, {\small MSIZE}, {\small GAS}\}
 
@@ -2025,6 +2032,13 @@ \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
+0xfd & {\small REVERT} & 2 & 0 & Halt execution reverting state changes
+                 but returning data. \\
+&&&& The definition of $H$ mentions {\small REVERT} and that has the effect of halting the execution.\\
+&&&& See equation (\ref{eq:output}). \\
+&&&& $\boldsymbol{\mu}'_i \equiv M(\boldsymbol{\mu}_i, \boldsymbol{\mu}_\mathbf{s}[0], \boldsymbol{\mu}_\mathbf{s}[1])$ \\
+&&&& $\sigma' = \varnothing,\quad A' = A^0$ \\
+\midrule
 0xfe & {\small INVALID} & $\varnothing$ & $\varnothing$ & Designated invalid instruction. \\
 \midrule
 0xff & {\small SELFDESTRUCT} & 1 & 0 & Halt execution and register account for later deletion. \\