New Memory Checking Section in docs

docs/pages/Specs/_meta.json

@@ -2,5 +2,6 @@
   "zkvm-overview": "Nexus zkVM Overview",
   "nexus-vm": "Nexus Virtual Machine",
   "nexus-prover": "Nexus Proof System",
+  "nexus-memory-checking": "Nexus zkVM Memory Checking",
   "nexus-costs": "Nexus zkVM Costs"
 }

docs/pages/Specs/nexus-costs.mdx

@@ -7,7 +7,7 @@ image: "/nexus-head.png"
 
 # Summary of Nexus zkVM costs
 
-Most of instructions of the Nexus VM instruction set can be implemented quite efficiently requiring less than 2000 constraints in total. The main exception are memory operations, which require expensive Merkle proof computations. More precisely, in the case of a memory update, one needs to compute 3 Merkle proofs, one to read the current instruction from memory, one to read the current contents of the memory location, and one to update that memory location. Each of the Merkle proofs require about 6800 constraints (about 400 constraints for each of the 17 levels of the Merkle tree).
+Most of instructions of the Nexus VM instruction set can be implemented quite efficiently requiring less than 2000 constraints in total. The main exception are memory operations, which require expensive Merkle proof computations. More precisely, in the case of a memory update, one needs to compute 3 Merkle proofs, one to read the current instruction from memory, one to read the current contents of the memory location, and one to update that memory location. Since each of these Merkle proofs require about 4300 constraints, as indicated in the [memory checking costs section](nexus-memory-checking#cost-profile), the total cost of a memory update is about 13000 constraints.
 
-Since the current version of the Nexus VM uses a universal model of computation, the total cost of each proof accumulation step is currently around 22000 constraints, which is quite inefficient. However, we expect to significantly improve these costs by using better memory checking techniques and a non-uniform model of computation. The use of precompiles also has the pontential to significantly improve the efficiency of the Nexus Proof System. 
+Since the current version of the Nexus VM uses a universal model of computation, the total cost of each proof accumulation step ends up being around 15000 constraints, which is quite inefficient. However, we expect to significantly improve these costs by using better memory checking techniques and a non-uniform model of computation. The use of precompiles also has the pontential to significantly improve the efficiency of the Nexus Proof System. 
 

docs/pages/Specs/nexus-memory-checking.mdx

@@ -0,0 +1,54 @@
+---
+title: "Nexus zkVM Memory Checking"
+lang: en-US
+description: "A description of the Nexus zkVM memory checking."
+image: "/nexus-head.png"
+---
+
+# Nexus zkVM Memory Checking 
+
+Since the external memory used by the Nexus Virtual Machine is assumed to be untrusted, the Nexus zkVM must ensure read-write consistency throughout the execution of a program. Informally, this requires that reading the contents of any cell of the memory should always return the value last written to that cell.
+
+In order to enforce the consistency of read-write operations into the memory, the Nexus zkVM currently uses Merkle Trees [[M87](#references)] together with the Poseidon hash function [[GKR21](#references)]. In this method, the contents of the memory are first associated with leaves of a Merkle tree and then Merkle-hashed into a Merkle root. The latter Merkle root serves as a binding commitment to the memory and needs to be updated whenever the contents of the memory change.
+
+## Merkle Tree Setup
+
+In the current version of Nexus VM, the memory size is set to $\mathbf{2^{22}}$ bytes. Hence, we associate leafs to 256-bit-long strings (i.e., 32 bytes) and then use a Merkle binary tree with 17 levels to describe its contents, as in the figure below.
+
+![merkle-hash-tree](/images/merkle-hash-tree.svg)
+
+Initially, each memory cell is assumed to be the $0$ string. Hence, in order to compute the Merkle root for the initial memory, we first compute the default hashes for each level of the tree, starting with the leaves and ending with the Merkle root. For the leaves, the default value is simply the hash of the $0$ string. For any subsequent level, their default values then become the hash of the concatenation of two of the default values for the level below it. 
+
+## Merkle Tree Updates and Proofs
+
+After setting up the initial Merkle root for the memory, this value will be used or updated with each memory access, depending on whether the operation is a read or write.
+
+### Read Operations
+
+For ease of illustration, let us assume the memory configuration $\textbf{M}$ shown in the figure below and consider the case of a *read operation* at address $64$. Let $m=\textbf{M}[64]$ be the value of the cell at memory address $64$, and let $\textbf{MS}=\textbf{M}[64 \ldots 95]$ be the 32-byte memory segment that contains $m$.
+
+![merkle-hash-tree-path](/images/merkle-hash-tree-path.svg)
+
+In order to prove that $m$ is the correct value at address $64$, the untrusted memory needs to provide not only $m$, but also a Merkle opening proof that attests to the authenticity of the value $m$. Let $\{h_{17}^{0,\ldots,1,0},\ldots, h_{1}^0, h_{0}\}$ denote the path (highlighted in red in the figure above) from the leaf $h_{17}^{0,\ldots,1,0}$ associated with $\textbf{MS}$ to the Merkle root $h_{0}$. Then the Merkle opening proof will consist of the memory segment $\textbf{MS}$ along with *all the siblings* of the nodes in the aforementioned leaf-to-root path (highlighted with red boxes in the figure above). Note that, given $\textbf{MS}$ and the nodes in the authentication path, one can easily recompute the value of the Merkle root in order to verify its correctness. Finally, given the segment $\textbf{MS}=\textbf{M}[64 \ldots 95]$, it is also possible to check that $m=\textbf{MS}[0]=\textbf{M}[64]=\mathtt{0x0F}$ is the correct return value for this read operation.
+
+
+### Write Operations
+
+Next, consider the case of a *write operation* at address $64$, where a new value $\mathtt{0xFF}$ should replace the old value $\mathtt{0x0F}$. In order to update the Merkle tree to match the new desired memory configuration, all the node values along the path from the leaf associated with $\textbf{MS}$ to the Merkle root $h_{0}$ need to be recomputed. We highlight these values in  blue in the figure below. To achieve this goal, the zkVM should proceed as follows:
+1. First perform a *read operation* to obtain $\textbf{M}[64]$ along with a Merkle opening proof for it (highlighted by red boxes in the figure below);
+2. Next, update the value at $\textbf{M}[64]$ to $\mathtt{0xFF}$ in the memory segment $\textbf{MS}=\textbf{M}[64 \ldots 95]$ as well as all the nodes in the path $\{h_{17}^{0,\ldots,1,0},\ldots, h_{1}^0, h_{0}\}$ starting from the leaf associated with $\textbf{MS}$; 
+3. Finally, keep the updated value $h_0$ as the new Merkle root.
+
+![merkle-hash-tree-path-update](/images/merkle-hash-tree-path-update.svg)
+
+## Cost Profile
+
+For a memory $\textbf{M}$ of size $2^{22}$, read and write operations will respectively cost $18$ and $18*2$ hash computations. Since each hash operation translates to about 240 constraints using the Poseidon hash function, read and write operations will result in about $4.3k$ and $8.6k$ constraints, respectively.
+
+
+## References
+
+[[GKR21](https://www.usenix.org/system/files/sec21-grassi.pdf)] Lorenzo Grassi, Dmitry Khovratovich, Christian Rechberger, Arnab Roy, and Markus Schofnegger. “Poseidon: A new hash function for Zero-Knowledge proof systems”. In: 30th USENIX Security Symposium (USENIX Security 21). 2021, pp. 519–535
+
+[[M87](https://link.springer.com/chapter/10.1007/3-540-48184-2_32)] Ralph C Merkle. “A digital signature based on a conventional encryption function”. In CRYPTO 1987.
+

docs/pages/Specs/nexus-prover.mdx

@@ -23,8 +23,6 @@ Let $P$ be a program that which we execute in a verifiable manner. As described
 
 In order to enforce the consistency of the memory throughout the execution of the program $P$, the Nexus zkVM currently uses Merkle Trees [[M87](#references)] for memory checking together with the Poseidon hash function [[GKR21](#references)]. In this method, we compute a Merkle root associated with the current contents of the memory and we update its value whenever the contents of the memory change.
 
-In the current version of Nexus VM, the memory size is set to $2^{22}$ bytes. Hence, we associate leafs to 256-bit-long strings (i.e., 32 bytes) and then use a Merkle binary tree with 17 levels to describe its contents. In order to compute the Merkle root for the initial memory, we compute a default value for each tree level starting from the leaves and ending with the Merkle root. To compute the default value for a given level, we simply compute the hash of the concatenation of two default values for the level below.
-
 Once the Merkle Root for the initial state is computed, the Nexus zkVM starts loading the program $P$ one instruction at a time, updating the Merkle Tree Root accordingly after each memory update. 
 
 Finally, once $P$ is fully loaded into the memory, we use the Merkle Root for the current state of the memory as the public input to the execution step of the proof system.

docs/pages/Specs/zkvm-overview.mdx

@@ -9,8 +9,6 @@ image: "/nexus-head.png"
 
 The *Nexus Zero-Knowledge Virtual Machine* (***Nexus zkVM*** for short) is a general computing platform allowing programs to be executed in a verifiable way.  The Nexus zkVM architecture has two main components: the *Nexus Virtual Machine* and the *Nexus Proof System*.
 
-The Nexus zkVM provides not only a general computing platform on which programs written in other languages can be compiled to run, but also a unified computing paradigm enabling the generation of accurate claims and proofs about the correctness of the computation.
-
 Being inspired by the RISC-V ISA [[WLPA14](#references)] and the vnTinyRAM architecture [[CGTV20](#references)], the Nexus VM can be easily translated from the RISC-V instruction set, for which a rich set of compilation tools already exists. As a result, the Nexus zkVM can easily support the verifiable execution of programs written in high-level programming languages such as Rust and C++. Support for other machine architectures such as EVM and Wasm can be provided through translation, emulation, or native execution.
 
 The first iteration of the Nexus Virtual Machine provides support for circuits encoded in Rank-1 Constraint Satisfiability (R1CS). Future versions of the Nexus zkVM will provide support for user-defined circuits encoded in CCS [[STW23](#references)], a modern encoding that simultaneously captures R1CS [[GGPR13](#references)], Plonkish [[GWC19; CBBZ23](#references)], and AIR [[BBHR19; Sta21; BCKL22](#references)].