Spec initial pass

docs/pages/specs/nexus-costs.mdx

@@ -9,5 +9,4 @@ image: "/nexus-head.png"
 
 Most 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 requires 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 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 potential 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 potential to significantly improve the efficiency of the Nexus Proof System.

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

@@ -5,7 +5,7 @@ description: "A description of the Nexus zkVM memory checking."
 image: "/nexus-head.png"
 ---
 
-## Nexus zkVM Memory Checking 
+## 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.
 
@@ -17,7 +17,7 @@ In the current version of Nexus VM, the memory size is set to $\mathbf{2^{22}}$
 
 ![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. 
+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
 
@@ -35,7 +35,7 @@ In order to prove that $m$ is the correct value at address $64$, the untrusted m
 
 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}$; 
+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)

docs/pages/specs/nexus-vm.mdx

@@ -12,33 +12,32 @@ import { Callout } from 'nextra/components'
 The Nexus Virtual Machine (Nexus VM or NVM) is a reduced instruction set computer (RISC) with a word-addressable random-access memory and input tapes. This virtual machine abstraction is comparable to others used in the zero-knowledge research space, such as the [TinyRAM architecture specification][TinyRAM]. The advantage of using such random-access machines is that they abstract away details of the underlying hardware or operating system and provide a convenient tool for generating claims and proofs about the correctness of a computation.
 
 <Callout type="info" emoji="ℹ️">
-  The NVM architecture has not yet stabilized. The following specification describes the architecture as of the Nexus zkVM 1.0.0 release.
+  The NVM architecture has not yet stabilized. The following specification describes the architecture as of the Nexus zkVM 2.0.0 release.
 </Callout>
 
 ### Nexus Virtual Machine Architecture
 
-The Nexus Virtual Machine has a *von Neumann* architecture, storing instructions and data in the same read-write memory space.  The machine has 32 registers and a read-write memory with addresses in the range $\{0\ldots 2^{32}-1\}$.   The state of the machine is defined as a five-tuple, $(pc;M;R;I;W)$, where
+The Nexus Virtual Machine has a *von Neumann* architecture, storing instructions and data in the same read-write memory space.  The machine has 32 registers and a read-write memory with addresses in the range $\{0\ldots 2^{32}-1\}$.   The state of the machine is defined as a four-tuple, $(pc;M;R;I)$, where
 * $pc$ denotes the program counter register;
 * $M$ denotes the memory;
 * $R$ denotes the set of registers;
-* $I$ is the public input;
-* $W$ is an auxiliary input, seen as a nondeterministic advice.
+* $I$ is the private input.
 
 <center>
 ![An abstraction of the Nexus Virtual Machine](/images/nvm-architecture.svg)
 </center>
 
-Both $M$ and $R$ are finite maps. The keys of $M$ are addresses in the range $\{0,\ldots, 2^{32}-1\}$ and the keys of $R$ are register selectors from the set $\{x_0\ldots x_{31}\}$. By design, updates to register $x_0$ are ignored and the value of $R[x_0]$ is always zero.
+Both $M$ and $R$ are finite maps. The keys of $M$ are addresses in the range $\{0,\ldots, 2^{32}-1\}$. The values of $M$ are 8-bit bytes. The keys of $R$ are register selectors from the set $\{x_0\ldots x_{31}\}$. The values of $R$ are 32-bit words. By design, updates to register $x_0$ are ignored and the value of $R[x_0]$ is always zero.
 
-The current implementation of the Nexus VM does not yet support public and auxiliary/private inputs, but this feature will soon be available. Also, we remark that specific implementations of the Nexus VM may choose memory sizes smaller than $2^{32}$ for efficient reasons.
+The current implementation of the Nexus VM does not yet support public inputs, but this feature will soon be available. Also, we remark that specific implementations of the Nexus VM may choose memory sizes smaller than $2^{32}$ for efficient reasons.
 
-At initialization, all the general-purpose registers are set to 0. The program counter $pc$ is set to $\mathtt{0x0000}$. The input and auxiliary tapes, once supported, should contain the public and input auxiliary inputs for the program. Since $pc$ is initially $\mathtt{0x0000}$, the first instruction to be executed will be the one stored at the position $\mathtt{0x0000}$ of the memory. Since the program code resides in the same area as the data, the initial memory can contain not only the program code but also some initial input data for the program.
+At initialization, all the general-purpose registers are set to 0. The program counter $pc$ is set to $\mathtt{0x0000}$. The input and tapes, once supported, should contain the public and input inputs for the program. Since $pc$ is initially $\mathtt{0x0000}$, the first instruction to be executed will be the one stored at the position $\mathtt{0x0000}$ of the memory. Since the program code resides in the same area as the data, the initial memory can contain not only the program code but also some initial input data for the program.
 
 The program counter $pc$ is always advanced by 8 bytes after the execution of each instruction, unless the instruction itself sets the value of $pc$. Moreover, the Nexus VM enforces 8-byte-memory alignment for the program counter by checking that $pc$ is a multiple of 8 when reading an instruction.
 
 ### Nexus Virtual Machine Instruction Set
 
-The Nexus VM instruction set contains 30 instructions in total, as summarized in table below. Each instruction is specified via an **opcode** and takes three arguments, two register selectors and a full 32-bit immediate value. The exact format $(\textbf{opcode}\;rd\;\;rs_1\;rs_2\;i)$ of each instruction is defined as follows:
+The Nexus VM instruction set contains 28 instructions in total, as summarized in table below. Each instruction is specified via an **opcode** and takes three arguments, two register selectors and a full 32-bit immediate value. The exact format $(\textbf{opcode}\;rd\;\;rs_1\;rs_2\;i)$ of each instruction is defined as follows:
 * $\textbf{opcode}$ is a string defining the instruction;
 * $rd$ is a register selector specifying the destination register;
 * $rs_1$ is a register selector specifying the first operand;
@@ -50,8 +49,6 @@ Table: Summary of the Nexus Virtual Machine Instruction Set, where operations ar
 | -------- | -------- | -------- |
 | $\textbf{add}$     | $rd$ $rs_1$  $rs_2$  $i$     | sets $R[rd]$ to $R[rs_1] + (R[rs_2] + i)$     |
 | $\textbf{sub}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to $R[rs_1] - (R[rs_2] + i)$|
-| $\textbf{mul}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to the least significant bits of $R[rs_1] \times (R[rs_2] + i)$|
-| $\textbf{div}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to the quotient of $R[rs_1] / (R[rs_2] + i)$|  % What if $R[rs_2] + i) = 0$?
 | $\textbf{slt}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to $(R[rs_1] < (R[rs_2] + i)$ (signed comparison) |
 | $\textbf{sltu}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to $(R[rs_1] < (R[rs_2] + i)$ (unsigned comparison)|
 | $\textbf{sll}$ | $rd$ $rs_1$  $rs_2$  $i$ | sets $R[rd]$ to $R[rs_1] \ll (R[rs_2] + i) \mathbin{\&} \mathtt{0x1F}$|
@@ -77,7 +74,7 @@ Table: Summary of the Nexus Virtual Machine Instruction Set, where operations ar
 | $\textbf{jal}$ | $rd$ $rs_1$ $i$ | jumps to $M[R[rs_1] + i]$  and stores $pc+8$ into $R[rd]$|
 | $\textbf{nop}$ |  | no operation |
 | $\textbf{halt}$ | $rs_1$ $i$ | halts execution with a return value $(R[rs_1] + i)$, $pc$ is not updated|
-| $\textbf{sys}$ |  | system call|
+| $\textbf{ecall}$ |  | system call|
 
 The Nexus VM also enforces 2-byte and 4-byte memory alignments for the instructions operating on half-words and words. In particular, one cannot read or write half-words and words to addresses which are not a multiple of $2$ and $4$, respectively.
 
@@ -115,8 +112,6 @@ Table: Binary Encoding of Nexus Virtual Machine Instructions, where $*^m$ denote
 | $\textbf{or}$     | $rd$ $rs_1$  $rs_2$  $i$     |  $\begin{array}{llllll} \texttt{0x47}  & \langle d \rangle  & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$    |
 | $\textbf{and}$     | $rd$ $rs_1$  $rs_2$  $i$     |  $\begin{array}{llllll} \texttt{0x48}  & \langle d \rangle  & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$    |
 | $\textbf{xor}$     | $rd$ $rs_1$  $rs_2$  $i$     |  $\begin{array}{llllll} \texttt{0x49}  & \langle d \rangle  & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$    |
-| $\textbf{mul}$     | $rd$ $rs_1$  $rs_2$  $i$     |  $\begin{array}{llllll} \texttt{0x4A}  & \langle d \rangle  & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$    |
-| $\textbf{div}$     | $rd$ $rs_1$  $rs_2$  $i$     |  $\begin{array}{llllll} \texttt{0x4B}  & \langle d \rangle  & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$    |
 
 Compared to RISC-V, Nexus VM instructions are longer (64 bits versus 32 bits) and allow for an additional argument.  One of the advantages of having an additional argument is that it allows for a reduced instruction set. In particular, as noted in the section describing the translation from RISC-V to Nexus VM,  different RISC-V instructions can be emulated with a single Nexus VM instruction.
 
@@ -137,9 +132,7 @@ $$
     pc \in&\: \{0..2^{32}-1\} &\text{Program counter} \\
     rd,rs_1,rs_2 \in&\: \{x_0 .. x_{31}\} &\text{Register selectors} \\
     alu    =&\: \textbf{add}
-         \mid   \textbf{sub}
-         \mid   \textbf{mul}
-         \mid   \textbf{div} \\
+         \mid   \textbf{sub} \\
         \mid&\: \textbf{slt}
          \mid   \textbf{sltu}
          \mid   \textbf{sll}
@@ -195,7 +188,7 @@ $$
     \mathcal{C}(alu\;rd\;\;rs_1\;i)    =& alu\;rd\;rs_1\;x_0\;i \\
     \mathcal{C}(\textbf{ebreak})       =& \textbf{nop} \\
     \mathcal{C}(\textbf{fence})        =& \textbf{nop} \\
-    \mathcal{C}(\textbf{ecall})        =& \textbf{sys} \\
+    \mathcal{C}(\textbf{ecall})        =& \textbf{ecall} \\
     \mathcal{C}(\textbf{unimp})        =& \textbf{halt}\;x_0\;1 \\
     \mathcal{C}(bcc\;rs_1\;rs_2\;i) =& bcc\;rs_1\;rs_2\;i \\
     \mathcal{C}(ld\;rs_1\;i) =& ld\;rs_1\;i \\
@@ -213,7 +206,7 @@ $\textbf{unimp}$ is mapped to $\textbf{halt}\;x_0\;1$ to indicate a failure cond
 
 ### Nexus Virtual Machine Initialization
 
-Initially, the memory is assumed to only contain zero values and all the general-purpose registers are set to 0. The program counter $pc$ is also set to $\mathtt{0x0000}$. Although the current version of the Nexus VM does not yet support input and auxiliary tapes, these will be eventually implemented and initialized with the contents of the public and auxiliary inputs for the program. The program itself is provided to the Nexus VM via a file in an Executable and Linkable Format (ELF) encoded according to the RV32I Instruction Set in the *Volume I, Unprivileged Specification version 20191213* in the [The RISC-V Instruction Set Manual](https://drive.google.com/file/d/1s0lZxUZaa7eV_O0_WsZzaurFLLww7ou5/view?usp=drive_link).
+Initially, the memory is assumed to only contain zero values and all the general-purpose registers are set to 0. The program counter $pc$ is also set to $\mathtt{0x0000}$. Although the current version of the Nexus VM does not yet support public input tapes, these will be eventually implemented and initialized with the contents of the public inputs for the program. The program itself is provided to the Nexus VM via a file in an Executable and Linkable Format (ELF) encoded according to the RV32I Instruction Set in the *Volume I, Unprivileged Specification version 20191213* in the [The RISC-V Instruction Set Manual](https://drive.google.com/file/d/1s0lZxUZaa7eV_O0_WsZzaurFLLww7ou5/view?usp=drive_link).
 
 In order to load the ELF file into the Nexus VM memory, the RISC-V assembly code provided in the ELF file based on 32-bit-long RV32I instruction set is first translated to Nexus VM 64-bit-long instruction set following the translation process described in the previous section. Next, each instruction in the program is loaded one at a time into the memory starting at address $\mathtt{0x0000}$.
 

docs/pages/specs/roadmap.mdx

@@ -15,10 +15,10 @@ The Nexus zkVM and Nexus Network are both undergoing rapid development.
 
 Contribute or follow along with the latest updates to the system on [Github](https://github.com/nexus-xyz/nexus-zkvm).
 
-### v1.0 to v2.0 to Beyond
-This documentation is for the Nexus 1.0 system. Many improvements to individual components are incoming, to be featured in the Nexus 2.0 system and future upgrade cycles beyond. Expected improvements include:
+### v2.0 to Beyond
+This documentation is for the Nexus 2.0 system. Many improvements to individual components are incoming, to be featured in the Nexus 2.0 system and future upgrade cycles beyond. Expected improvements include:
 1. **Prover**: A new (family of) proof systems combining the latest theoretical developments in folding schemes and lookup arguments.
-2. **Proof Compression**: A second phase of proof compression, on top of the v1.0 $O(log(n))$ proof compression mechanism, which will bring the proof to $O(log(log(n)))$. That is, a proof of a proof of a proof.
+2. **Proof Compression**: A second phase of proof compression, on top of the v2.0 $O(log(n))$ proof compression mechanism, which will bring the proof to $O(log(log(n)))$. That is, a proof of a proof of a proof.
 3. **NVM**: A revised NVM architecture, with a simpler ISA and a dedicated compiler toolchain with further prover-related compiler optimizations.
 4. **Precompile System**: A library of Nexus precompiles, with in-depth guides showing how to write precompiles in R1CS, Plonkish and AIR.
 5. **Memory Checking**: An upgraded memory checking mechanism that is exponentially more performant than Merkle Trees, based on permutation checks and instruction sorting.