Update Memory in specs (#1362)

* Update Memory specs

* Apply comment

Co-authored-by: Robin Salen <30937548+Nashtare@users.noreply.github.com>

---------

Co-authored-by: Robin Salen <30937548+Nashtare@users.noreply.github.com>

evm/spec/tables/memory.tex

@@ -11,40 +11,40 @@ Each row of the memory table corresponds to a single memory operation (a read or
   \item $v$, the value being read or written
   \item $\tau$, the timestamp of the operation
 \end{enumerate}
-The memory table should be ordered by $(a, \tau)$. Note that the correctness memory could be checked as follows:
+The memory table should be ordered by $(a, \tau)$. Note that the correctness of the memory could be checked as follows:
 \begin{enumerate}
-  \item Verify the ordering by checking that $(a_i, \tau_i) < (a_{i+1}, \tau_{i+1})$ for each consecutive pair.
-  \item Enumerate the purportedly-ordered log while tracking a ``current'' value $c$, which is initially zero.\footnote{EVM memory is zero-initialized.}
+  \item Verify the ordering by checking that $(a_i, \tau_i) \leq (a_{i+1}, \tau_{i+1})$ for each consecutive pair.
+  \item Enumerate the purportedly-ordered log while tracking the ``current'' value of $v$, which is initially zero.\footnote{EVM memory is zero-initialized.}
   \begin{enumerate}
-    \item Upon observing an address which doesn't match that of the previous row, set $c \leftarrow 0$.
-    \item Upon observing a write, set $c \leftarrow v$.
-    \item Upon observing a read, check that $v = c$.
+    \item Upon observing an address which doesn't match that of the previous row, if the operation is a read, check that  $v = 0$.
+    \item Upon observing a write, don't constrain $v$.
+    \item Upon observing a read at timestamp $\tau_i$ which isn't the first operation at this address, check that $v_i = v_{i-1}$.
   \end{enumerate}
 \end{enumerate}
 
-The ordering check is slightly involved since we are comparing multiple columns. To facilitate this, we add an additional column $e$, where the prover can indicate whether two consecutive addresses are equal. An honest prover will set
+The ordering check is slightly involved since we are comparing multiple columns. To facilitate this, we add an additional column $e$, where the prover can indicate whether two consecutive addresses changed. An honest prover will set
 $$
 e_i \leftarrow \begin{cases}
-  1 & \text{if } a_i = a_{i + 1}, \\
+  1 & \text{if } a_i \neq a_{i + 1}, \\
   0 & \text{otherwise}.
 \end{cases}
 $$
+We also introduce a range-check column $c$, which should hold:
+$$
+c_i \leftarrow \begin{cases}
+  a_{i + 1} - a_i - 1 & \text{if } e_i = 1, \\
+  \tau_{i+1} - \tau_i & \text{otherwise}.
+\end{cases}
+$$
+The extra $-1$ ensures that the address actually changed if $e_i = 1$.
 We then impose the following transition constraints:
 \begin{enumerate}
   \item $e_i (e_i - 1) = 0$,
-  \item $e_i (a_i - a_{i + 1}) = 0$,
-  \item $e_i (\tau_{i + 1} - \tau_i) + (1 - e_i) (a_{i + 1} - a_i - 1) < 2^{32}$.
+  \item $(1 - e_i) (a_{i + 1} - a_i) = 0$,
+  \item $c_i < 2^{32}$.
 \end{enumerate}
 The last constraint emulates a comparison between two addresses or timestamps by bounding their difference; this assumes that all addresses and timestamps fit in 32 bits and that the field is larger than that.
 
-Finally, the iterative checks can be arithmetized by introducing a trace column for the current value $c$. We add a boundary constraint $c_0 = 0$, and the following transition constraints:
-\todo{This is out of date, we don't actually need a $c$ column.}
-\begin{enumerate}
-  \item $v_{\text{from},i} = c_i$,
-  \item $c_{i + 1} = e_i v_{\text{to},i}$.
-\end{enumerate}
-
-
 \subsubsection{Virtual memory}
 
 In the EVM, each contract call has its own address space. Within that address space, there are separate segments for code, main memory, stack memory, calldata, and returndata. Thus each address actually has three compoments:
@@ -55,7 +55,15 @@ In the EVM, each contract call has its own address space. Within that address sp
 \end{enumerate}
 The comparisons now involve several columns, which requires some minor adaptations to the technique described above; we will leave these as an exercise to the reader.
 
-
 \subsubsection{Timestamps}
 
-TODO: Explain $\tau = \texttt{NUM\_CHANNELS} \times \texttt{cycle} + \texttt{channel}$.
+Memory operations are sorted by address $a$ and timestamp $\tau$. For a memory operation in the CPU, we have:
+$$\tau = \texttt{NUM\_CHANNELS} \times \texttt{cycle} + \texttt{channel}.$$
+Since a memory channel can only hold at most one memory operation, every CPU memory operation's timestamp is unique.
+
+Note that it doesn't mean that all memory operations have unique timestamps. There are two exceptions:
+
+\begin{itemize}
+  \item Before bootstrapping, we write some global metadata in memory. These extra operations are done at timestamp $\tau = 0$.
+  \item Some tables other than CPU can generate memory operations, like KeccakSponge. When this happens, these operations all have the timestamp of the CPU row of the instruction which invoked the table (for KeccakSponge, KECCAK\_GENERAL).
+\end{itemize}