Add exceptions to specs (#1372)

* Add exceptions to specs

* Apply comments

evm/spec/exceptions.tex

@@ -0,0 +1,44 @@
+\section{Exceptions}
+\label{exceptions}
+
+Sometimes, when executing user code (i.e. contract or transaction code), the EVM halts exceptionally (i.e. outside of a STOP, a RETURN or a REVERT).
+When this happens, the CPU table invokes a special instruction with a dedicated operation flag \texttt{exception}.
+Exceptions can only happen in user mode; triggering an exception in kernel mode would make the proof unverifiable.
+No matter the exception, the handling is the same:
+
+-- The opcode which would trigger the exception is not executed. The operation flag set is \texttt{exception} instead of the opcode's flag.
+
+-- We push a value to the stack which contains: the current program counter (to retrieve the faulty opcode), and the current value of \texttt{gas\_used}.
+The program counter is then set to the corresponding exception handler in the kernel (e.g. \texttt{exc\_out\_of\_gas}).
+
+-- The exception handler verifies that the given exception would indeed be triggered by the faulty opcode. If this is not the case (if the exception has already happened or if it doesn't happen after executing
+the faulty opcode), then the kernel panics: there was an issue during witness generation.
+
+-- The kernel consumes the remaining gas and returns from the current context with \texttt{success} set to 0 to indicate an execution failure.
+
+Here is the list of the possible exceptions:
+
+\begin{enumerate}[align=left]
+  \item[\textbf{Out of gas:}] Raised when a native instruction (i.e. not a syscall) in user mode pushes the amount of gas used over the current gas limit.
+When this happens, the EVM jumps to \texttt{exc\_out\_of\_gas}. The kernel then checks that the consumed gas is currently below the gas limit,
+and that adding the gas cost of the faulty instruction pushes it over it.
+If the exception is not raised, the prover will panic when returning from the execution: the remaining gas is checked to be positive after STOP, RETURN or REVERT.
+  \item[\textbf{Invalid opcode:}] Raised when the read opcode is invalid. It means either that it doesn't exist, or that it's a privileged instruction and
+thus not available in user mode. When this happens, the EVM jumps to \texttt{exc\_invalid\_opcode}. The kernel then checks that the given opcode is indeed invalid.
+If the exception is not raised, decoding constraints ensure no operation flag is set to 1, which would make it a padding row. Halting constraints would then make the proof
+unverifiable.
+  \item[\textbf{Stack underflow:}] Raised when an instruction which pops from the stack is called when the stack doesn't have enough elements.
+When this happens, the EVM jumps to \texttt{exc\_stack\_overflow}. The kernel then checks that the current stack length is smaller than the minimum 
+stack length required by the faulty opcode.
+If the exception is not raised, the popping memory operation's address offset would underflow, and the Memory range check would require the Memory trace to be too
+large to be provable ($>2^{60}$).
+  \item[\textbf{Invalid JUMP destination:}] Raised when the program counter jumps to an invalid location (i.e. not a JUMPDEST). When this happens, the EVM jumps to
+\texttt{exc\_invalid\_jump\_destination}. The kernel then checks that the opcode is a JUMP, and that the destination is not a JUMPDEST by checking the
+JUMPDEST segment.
+If the exception is not raised, jumping constraints will fail the proof.
+  \item[\textbf{Invalid JUMPI destination:}] Same as the above, for JUMPI.
+  \item[\textbf{Stack overflow:}] Raised when a pushing instruction in user mode pushes the stack over 1024. When this happens, the EVM jumps
+to \texttt{exc\_stack\_overflow}. The kernel then checks that the current stack length is exactly equal to 1024 (since an instruction can only
+push once at most), and that the faulty instruction is pushing.
+If the exception is not raised, stack constraints ensure that a stack length of 1025 in user mode will fail the proof.
+\end{enumerate}

evm/spec/zkevm.tex

@@ -54,6 +54,7 @@
 \input{tables}
 \input{mpts}
 \input{instructions}
+\input{exceptions}
 
 \bibliography{bibliography}{}
 \bibliographystyle{ieeetr}

evm/src/cpu/kernel/asm/core/exception.asm

@@ -1,4 +1,6 @@
 // These exception codes are arbitrary and assigned by us.
+// Note that exceptions can only be triggered in user mode. Triggering an exception
+// in kernel mode wwill fail the constraints.
 global exception_jumptable:
     // exception 0: out of gas
     JUMPTABLE exc_out_of_gas