diff --git a/docs/assets/vm-architecture-v2.drawio b/docs/assets/vm-architecture-v2.drawio
new file mode 100644
index 00000000..42e49b4f
--- /dev/null
+++ b/docs/assets/vm-architecture-v2.drawio
@@ -0,0 +1,147 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/docs/pages/index.mdx b/docs/pages/index.mdx
index abc8d015..292dcef9 100644
--- a/docs/pages/index.mdx
+++ b/docs/pages/index.mdx
@@ -43,7 +43,7 @@ import { Callout } from 'nextra/components'
The Nexus zkVM (zero-knowledge virtual machine) is a modular, extensible, open-source, highly-parallelized, prover-optimized, contributor-friendly, [zkVM](specs/zkvm-overview.mdx) written in Rust, focused on performance and security.
-[Nexus zkVM v1.0.0](https://github.com/nexus-xyz/nexus-zkvm/releases/tag/v1.0.0) is the current stable release, implementing the zkVM component of the [Nexus 1.0](https://nexus-xyz.github.io/assets/nexus_whitepaper.pdf) system.
+[Nexus zkVM v0.2.0](https://github.com/nexus-xyz/nexus-zkvm/releases/tag/v0.2.0) is the current stable release, implementing the zkVM component of the Nexus 2.0 system.
## Proving Computation
diff --git a/docs/pages/network.mdx b/docs/pages/network.mdx
index 05e8ae4b..ae6debd1 100644
--- a/docs/pages/network.mdx
+++ b/docs/pages/network.mdx
@@ -35,7 +35,7 @@ import { Callout } from 'nextra/components'
The Nexus Network is a massively-parallelized proof network for executing and proving the Nexus zkVM.
-[Nexus Network v1.0.0](https://github.com/nexus-xyz/nexus-zkvm/releases/tag/v1.0.0) is the current stable release, implementing the network component of the [Nexus 1.0](https://nexus-xyz.github.io/assets/nexus_whitepaper.pdf) system.
+[Nexus Network v0.2.0](https://github.com/nexus-xyz/nexus-zkvm/releases/tag/v0.2.0) is the current stable release, implementing the network component of the Nexus 2.0 system.
The Nexus Network is currently in a prototype stage.
diff --git a/docs/pages/specs/nexus-costs.mdx b/docs/pages/specs/nexus-costs.mdx
index a215e0f9..02077065 100644
--- a/docs/pages/specs/nexus-costs.mdx
+++ b/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.
diff --git a/docs/pages/specs/nexus-memory-checking.mdx b/docs/pages/specs/nexus-memory-checking.mdx
index fa1f8037..afb5f36c 100644
--- a/docs/pages/specs/nexus-memory-checking.mdx
+++ b/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}}$
-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.
diff --git a/docs/pages/specs/nexus-vm.mdx b/docs/pages/specs/nexus-vm.mdx
index fbca0a59..f4f65897 100644
--- a/docs/pages/specs/nexus-vm.mdx
+++ b/docs/pages/specs/nexus-vm.mdx
@@ -9,218 +9,155 @@ import { Callout } from 'nextra/components'
## Nexus Virtual Machine
-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.
+The Nexus Virtual Machine (Nexus VM or NVM) is a reduced instruction set computer (RISC) with a byte-addressable random-access memory and a private input tape. 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.
- 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 0.2.0 release.
### 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.
+* $R$ denotes the state of registers;
+* $I$ is the private input.
-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 providing public inputs at runtime. Also, we remark that during compilation the Nexus VM may be configured to use memory sizes smaller than $2^{32}$ for efficiency 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 private input tape contains the byte-encoded private input 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 public 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.
+The program counter $pc$ is always advanced by 4 bytes after the execution of each instruction, unless the instruction itself sets the value of $pc$. Moreover, the Nexus VM enforces 4-byte memory alignment for the program counter by checking that $pc$ is a multiple of 4 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:
-* $\textbf{opcode}$ is a string defining the instruction;
+The Nexus VM instruction set contains 41 instructions in total, as summarized in table below. Each instruction is specified via an **mnemonic** and can take some arguments, typically register selectors and an immediate value. The exact format of each instruction is defined as follows:
+* $\textbf{mnemonic}$ is a string name of the instruction;
* $rd$ is a register selector specifying the destination register;
* $rs_1$ is a register selector specifying the first operand;
* $rs_2$ is a register selector specifying the second operand; and
-* $i$ is a full 32-bit immediate value.
+* $i$ is an immediate value, whose size varies according to instructions.
Table: Summary of the Nexus Virtual Machine Instruction Set, where operations are mod $2^{32}$.
| Instruction mnemonic| Arguments | Description of functionality |
| -------- | -------- | -------- |
-| $\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}$|
-| $\textbf{slr}$ | $rd$ $rs_1$ $rs_2$ $i$ | sets $R[rd]$ to $R[rs_1] \gg (R[rs_2] + i) \mathbin{\&} \mathtt{0x1F}$|
-| $\textbf{sra}$ | $rd$ $rs_1$ $rs_2$ $i$ | sets $R[rd]$ to $R[rs_1] \gg (R[rs_2] + i) \mathbin{\&} \mathtt{0x1F}$ ($R[rs_1]$ as integer) |
-| $\textbf{xor}$ | $rd$ $rs_1$ $rs_2$ $i$ | sets $R[rd]$ to the bitwise XOR of $R[rs_1]$ and $(R[rs_2] + i)$ |
-| $\textbf{and}$ | $rd$ $rs_1$ $rs_2$ $i$ | sets $R[rd]$ to the bitwise AND of $R[rs_1]$ and $(R[rs_2] + i)$|
-| $\textbf{or}$ | $rd$ $rs_1$ $rs_2$ $i$ | sets $R[rd]$ to the bitwise OR of $R[rs_1]$ and $(R[rs_2] + i)$|
-| $\textbf{beq}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] = R[rs_2])$ (signed comparison)|
-| $\textbf{bne}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \not= R[rs_2])$ (signed comparison)|
-| $\textbf{blt}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] < R[rs_2])$ (signed comparison)|
-| $\textbf{bge}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \geq R[rs_2])$ (signed comparison)|
-| $\textbf{bltu}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] < R[rs_2])$ (unsigned comparison)|
-| $\textbf{bgeu}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \geq R[rs_2])$ (unsigned comparison)|
-| $\textbf{lb}$ | $rd$ $rs_1$ $i$ | loads the sign extension of the byte at $M[R[rs_1] + i]$ into $R[rd]$|
-| $\textbf{lh}$ | $rd$ $rs_1$ $i$ | loads the sign extension of the half-word at $M[R[rs_1] + i]$ into $R[rd]$|
-| $\textbf{lw}$ | $rd$ $rs_1$ $i$ | loads the sign extension of the word at $M[R[rs_1] + i]$ into $R[rd]$|
-| $\textbf{lbu}$ | $rd$ $rs_1$ $i$ | loads the zero extension of the byte at $M[R[rs_1] + i]$ into $R[rd]$|
-| $\textbf{lhu}$ | $rd$ $rs_1$ $i$ | loads the zero extension of the half-word at $M[R[rs_1] + i]$ into $R[rd]$|
-| $\textbf{sb}$ | $rs_1$ $rs_2$ $i$ | stores the first byte of $R[rs_2]$ at $M[R[rs_1] + i]$|
-| $\textbf{sh}$ | $rs_1$ $rs_2$ $i$ | stores the first half-word of $R[rs_2]$ at $M[R[rs_1] + i]$|
-| $\textbf{sw}$ | $rs_1$ $rs_2$ $i$ | stores $R[rs_2]$ at $M[R[rs_1] + i]$|
-| $\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|
-
-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.
-
-Each instruction is encoded as a 64-bit-long string, starting with 8-bit-long $\textbf{opcode}$ string, followed by a 9-bit-long zero string, three 5-bit-long register selectors for $rd$, $rs_1$, and $rs_1$, and a 32-bit immediate value.
-
-Table: Binary Encoding of Nexus Virtual Machine Instructions, where $*^m$ denotes any binary string of $m$ bits, and $\langle d \rangle$, $\langle s_1 \rangle$, $\langle s_2 \rangle$, and $\langle i \rangle$ denote respectively the binary representation of the 5-bit-long register selectors $rd$, $rs_1$, $rs_2$, and the 32-bit-long immediate value $i$.
-
-| Instruction mnemonic| Arguments | Binary Encodings |
+| $\textbf{lui}$ | $rd$ $i$ | sets $R[rd]$ to $i$ |
+| $\textbf{auipc}$ | $rd$ $i$ | sets $R[rd]$ to $pc+i$ |
+| $\textbf{add}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $R[rs_1] + R[rs_2]$ |
+| $\textbf{addi}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $R[rs_1] + i$ |
+| $\textbf{sub}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $R[rs_1] - R[rs_2]$|
+| $\textbf{slt}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $(R[rs_1] < R[rs_2])$ (signed comparison) |
+| $\textbf{slti}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $(R[rs_1] < i)$ (signed comparison) |
+| $\textbf{sltu}$ | $rd$ $rs_1$ $rs_2$| sets $R[rd]$ to $(R[rs_1] < R[rs_2])$ (unsigned comparison)|
+| $\textbf{sltui}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $(R[rs_1] < i)$ (unsigned comparison)|
+| $\textbf{sll}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $R[rs_1] \ll R[rs_2] \mathbin{\&} \mathtt{0x1F}$|
+| $\textbf{slli}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $R[rs_1] \ll i \mathbin{\&} \mathtt{0x1F}$|
+| $\textbf{srl}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $R[rs_1] \gg R[rs_2] \mathbin{\&} \mathtt{0x1F}$ (with zero extension) |
+| $\textbf{srli}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $R[rs_1] \gg i \mathbin{\&} \mathtt{0x1F}$ (with zero extension)|
+| $\textbf{sra}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to $R[rs_1] \gg R[rs_2] \mathbin{\&} \mathtt{0x1F}$ (with sign extension) |
+| $\textbf{srai}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to $R[rs_1] \gg i \mathbin{\&} \mathtt{0x1F}$ (with sign extension) |
+| $\textbf{xor}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to the bitwise XOR of $R[rs_1]$ and $R[rs_2]$ |
+| $\textbf{xori}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to the bitwise XOR of $R[rs_1]$ and $i$ |
+| $\textbf{and}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to the bitwise AND of $R[rs_1]$ and $R[rs_2]$|
+| $\textbf{andi}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to the bitwise AND of $R[rs_1]$ and $i$|
+| $\textbf{or}$ | $rd$ $rs_1$ $rs_2$ | sets $R[rd]$ to the bitwise OR of $R[rs_1]$ and $R[rs_2]$|
+| $\textbf{ori}$ | $rd$ $rs_1$ $i$ | sets $R[rd]$ to the bitwise OR of $R[rs_1]$ and $i$|
+| $\textbf{beq}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] = R[rs_2])$|
+| $\textbf{bne}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \not= R[rs_2])$|
+| $\textbf{blt}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] < R[rs_2])$ (signed comparison)|
+| $\textbf{bge}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \geq R[rs_2])$ (signed comparison)|
+| $\textbf{bltu}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] < R[rs_2])$ (unsigned comparison)|
+| $\textbf{bgeu}$ | $rs_1$ $rs_2$ $i$ | branches to $pc+i$ if $(R[rs_1] \geq R[rs_2])$ (unsigned comparison)|
+| $\textbf{lb}$ | $rd$ $rs_1$ $i$ | loads the sign extension of the byte at $M[R[rs_1] + i]$ into $R[rd]$|
+| $\textbf{lh}$ | $rd$ $rs_1$ $i$ | loads the sign extension of the half-word at $M[R[rs_1] + i]$ into $R[rd]$|
+| $\textbf{lw}$ | $rd$ $rs_1$ $i$ | loads the word at $M[R[rs_1] + i]$ into $R[rd]$|
+| $\textbf{lbu}$ | $rd$ $rs_1$ $i$ | loads the zero extension of the byte at $M[R[rs_1] + i]$ into $R[rd]$|
+| $\textbf{lhu}$ | $rd$ $rs_1$ $i$ | loads the zero extension of the half-word at $M[R[rs_1] + i]$ into $R[rd]$|
+| $\textbf{sb}$ | $rs_1$ $rs_2$ $i$ | stores the least significant byte of $R[rs_2]$ at $M[R[rs_1] + i]$|
+| $\textbf{sh}$ | $rs_1$ $rs_2$ $i$ | stores the less significant half-word of $R[rs_2]$ at $M[R[rs_1] + i]$|
+| $\textbf{sw}$ | $rs_1$ $rs_2$ $i$ | stores $R[rs_2]$ at $M[R[rs_1] + i]$|
+| $\textbf{jal}$ | $rd$ $i$ | jumps to $pc+i$ and stores $pc+4$ into $R[rd]$|
+| $\textbf{jalr}$ | $rd$ $rs_1$ $i$ | jumps to $R[rs_1] + i$ and stores $pc+4$ into $R[rd]$|
+| $\textbf{fence}$ | | No operation |
+| $\textbf{ecall}$ | $rd$ | system call |
+| $\textbf{ebreak}$ | $rd$ | system call|
+| $\textbf{unimp}$ | | jumps to $pc$; in effect looping forever at the current program counter |
+
+The Nexus VM also enforces 2-byte and 4-byte memory alignments for the instructions operating on half-words and words.
+
+Each instruction is encoded as a 32-bit-long string, ending with 7-bit-long $\textbf{opcode}$ string, preceded by a 5-bit-long register selector in many cases, and other data depending on the operation.
+
+Table: Binary Encoding of Nexus Virtual Machine Instructions, where $*^m$ denotes any binary string of $m$ bits, and $\langle d \rangle$, $\langle s_1 \rangle$, $\langle s_2 \rangle$ denote respectively the binary representation of the 5-bit-long register selectors $rd$, $rs_1$, $rs_2$.
+
+The notation $\langle i_x \rangle$ each denote immediate values, interpreted the same way as $x$-immediate values of 32-bit RISC-V architecture. Some immediate values (type B and S) occupy discontiguous positions, so their fragments are written as $\langle i_\texttt{x0} \rangle$ and $\langle i_\texttt{x1} \rangle$. $\langle i_\texttt{SH} \rangle$ denotes a 5-bit long immediate value.
+
+$\langle i_\texttt{U}\rangle$ and $\langle i_\texttt{J}\rangle$ contain 20 bits.
+$\langle i_\texttt{I}\rangle$ contains 12 bits.
+$\langle i_\texttt{S0}\rangle$ and $\langle i_\texttt{B0}\rangle$ contain 5 bits.
+$\langle i_\texttt{S1}\rangle$ and $\langle i_\texttt{B1}\rangle$ contain 7 bits.
+
+| Instruction mnemonic| Arguments | Binary Encodings (left: most significant bit) |
| -------- | -------- | -------- |
-| $\textbf{nop}$ | | $\begin{array}{llllll} \texttt{0x01} & \mathtt{*^5} \; \ & \mathtt{*^5} \; \ & \; \mathtt{*^5} \; \ & \mathtt{*^{32}}\end{array}$|
-| $\textbf{halt}$ | $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x02} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle \end{array}$|
-| $\textbf{sys}$ | | $\begin{array}{llllll} \texttt{0x03} & \mathtt{*^5} \; \ & \mathtt{*^5} \; \ & \; \mathtt{*^5} \; \ & \mathtt{*^{32}}\end{array}$|
-| $\textbf{jal}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x10} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{beq}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x11} & \mathtt{*^5} \;\ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{bne}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x12} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{blt}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x13} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{bge}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x14} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{bltu}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x15} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{bgeu}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x16} & \mathtt{*^5} \; \ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{lb}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x20} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{lh}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x21} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{lw}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x22} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{lbu}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x23} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{lhu}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \texttt{0x24} & \langle d \rangle & \langle s_1 \rangle & \; \mathtt{*^5} \; \ & \langle i \rangle\end{array}$|
-| $\textbf{sb}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x30} & \mathtt{*^5} \;\ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{sh}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x31} & \mathtt{*^5} \;\ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{sw}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x32} & \mathtt{*^5} \;\ & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$|
-| $\textbf{add}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x40} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{sub}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x41} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{slt}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x42} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{sltu}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x43} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{sll}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x44} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{slr}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x45} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\textbf{sra}$ | $rd$ $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \texttt{0x46} & \langle d \rangle & \langle s_1 \rangle & \langle s_2 \rangle & \langle i \rangle\end{array}$ |
-| $\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.
-
-Similarly to the $\textbf{answer}$ instruction in the [TinyRAM architecture specification][TinyRAM], the output produced by $\textbf{halt}$ indicates whether the program halts in an accepting or rejecting state by setting $R[rs_1] + i=0$ or not.
-
-The current architecture does not specify an output tape. Nevertheless, one can easily return arbitrary strings as output by encoding that string in some specific region of the memory before halting in an accepting state.
-
-As we show in the next section, the RISC-V instruction set can be easily compiled to the instruction set of the Nexus VM, by applying a simple translation function to a subset of these instructions. As a result, the Nexus VM can effortlessly support the execution of programs written in high-level programming languages such as Rust and C++. In addition to that, as indicated further below, future versions of the Nexus VM will be able to be *extended* with custom instructions (e.g. SHA-256).
-
-### Translation from RISC-V to Nexus VM
-
-The syntax of RISC-V instructions supported by the Nexus VM is the following:
-
-$$
-\begin{align*}
- %\text{Binary Operators}\\
- i \in&\: \{0..2^{32}-1\} &\text{Immediate values} \\
- 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{slt}
- \mid \textbf{sltu}
- \mid \textbf{sll}
- \mid \textbf{srl}
- \mid \textbf{sra} \\
- \mid&\: \textbf{xor}
- \mid \textbf{and}
- \mid \textbf{or} & \text{Binary operators} \\
- bcc =&\: \textbf{beq}
- \mid \textbf{bne}
- \mid \textbf{blt}
- \mid \textbf{bge}
- \mid \textbf{bltu}
- \mid \textbf{bgeu} & \text{Branch conditions} \\
- ld =&\: \textbf{lb}
- \mid \textbf{lh}
- \mid \textbf{lw}
- \mid \textbf{lbu}
- \mid \textbf{lhu} & \text{Load operations} \\
- st =&\: \textbf{sb}
- \mid \textbf{sh}
- \mid \textbf{sw} & \text{Store operations} \\
- oper
- =&\: \textbf{lui}\;rd\;i & \text{Load immediate} \\
- \mid&\: \textbf{auipc}\;rd\;i & \text{Load immediate + PC} \\
- \mid&\: alu\;rd\;\;rs_1\;rs_2 & \text{ALU register-register} \\
- \mid&\: alu\;rd\;\;rs_1\;i & \text{ALU register-immediate} \\
- \mid&\: \textbf{ebreak} & \text{Breakpoint} \\
- \mid&\: \textbf{fence} & \text{Memory fence} \\
- branch
- =&\: \textbf{jal}\;rd\;i & \text{Jump and link} \\
- \mid&\: \textbf{jalr}\;rd\;rs_1\;i & \text{Jump and link register} \\
- \mid&\: bcc\;rs_1\;rs_2\;i & \text{Conditional branch} \\
- memory
- =&\: ld\;rd\;rs_1\;i & \text{Load memory} \\
- \mid&\: st\;rs_1\;rs_2\;i & \text{Store memory} \\
- inst
- =&\: oper & \text{Operations} \\
- \mid&\: branch & \text{Control transfer} \\
- \mid&\: memory & \text{Load and store} \\
- \mid&\: \textbf{ecall} & \text{Environment call} \\
- \mid&\: \textbf{unimp} & \text{Unimplemented} \\
-\end{align*}
-$$
-
-These RISC-V instructions can be easily converted to Nexus VM instructions according to:
-
-$$
-\begin{align*}
- \mathcal{C}(\textbf{lui}\;rd\;i) =& \textbf{add}\;rd\;x_0\;x_0\;i \\
- \mathcal{C}(\textbf{auipc}\;rd\;i) =& \textbf{add}\;rd\;x_0\;x_0\;(pc+i) \\
- \mathcal{C}(alu\;rd\;\;rs_1\;rs_2) =& alu\;rd\;rs_1\;rs_2\;0 \\
- \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{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 \\
- \mathcal{C}(st\;rs_1\;rs_2\;i) =& st\;rs_1\;rs_2\;i \\
- \mathcal{C}(\textbf{jal}\;rd\;i) =& \textbf{jal}\;rd\;x_0\;i \\
- \mathcal{C}(\textbf{jalr}\;rd\;rs_1\;i) =& \textbf{jal}\;rd\;rs_1\;i \\
- \end{align*}
-$$
-
-Note that the special RISC-V load immediate instructions ($\textbf{lui}$ and $\textbf{auipc}$) are a result of the fixed 32-bit encoding of instructions. The Nexus VM relaxes this constraint allowing for a reduced instruction set.
-
-Both $\textbf{ebreak}$ and $\textbf{fence}$ are mapped to $\textbf{nop}$ since they have no effect as we do not support debugging and our virtual machine only has one CPU core (a.k.a. Hart in RISC-V terminology),
-
-$\textbf{unimp}$ is mapped to $\textbf{halt}\;x_0\;1$ to indicate a failure condition.
+| $\textbf{lui}$ | $rd$ $i$ | $\begin{array}{lll} \langle i_\texttt{U} \rangle & \langle d \rangle & \texttt{0b\_011\_0111} \end{array}$ |
+| $\textbf{auipc}$ | $rd$ $i$ | $\begin{array}{lll} \langle i_\texttt{U} \rangle & \langle d \rangle & \texttt{0b\_001\_0111} \end{array}$ |
+| $\textbf{jal}$ | $rd$ $i$ | $\begin{array}{lll} \langle i_\texttt{J} \rangle & \langle d \rangle & \texttt{0b\_110\_1111} \end{array}$|
+| $\textbf{jalr}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \mathtt{0b\_000} & \langle d \rangle & \texttt{0b\_110\_0111} \end{array}$|
+| $\textbf{beq}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle&\langle s_1 \rangle &\texttt{0b\_000} &\langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{bne}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle &\langle s_1 \rangle & \texttt{0b\_001} & \langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{blt}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{bge}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_101} & \langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{bltu}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_110} & \langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{bgeu}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{B1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_111} & \langle i_\texttt{B0} \rangle \;\ &\texttt{0b\_110\_0011}\end{array}$|
+| $\textbf{lb}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}$|
+| $\textbf{lh}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}$|
+| $\textbf{lw}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}$|
+| $\textbf{lbu}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_011} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}$|
+| $\textbf{lhu}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}$|
+| $\textbf{sb}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{S1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle i_\texttt{S0} \rangle & \texttt{0b\_010\_0011}\end{array}$|
+| $\textbf{sh}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{S1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle i_\texttt{S0} \rangle & \texttt{0b\_010\_0011}\end{array}$|
+| $\textbf{sw}$ | $rs_1$ $rs_2$ $i$ | $\begin{array}{llllll} \langle i_\texttt{S1} \rangle & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle i_\texttt{S0} \rangle & \texttt{0b\_010\_0011}\end{array}$|
+| $\textbf{addi}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{slli}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{slti}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{sltui}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_011} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{xori}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle d \rangle & \texttt{0b\_001\_0011}\end{array}$ |
+| $\textbf{srli}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll}\texttt{0b\_000\_0000} & \langle i_\texttt{SH} \rangle & \langle s_1 \rangle & \texttt{0b\_101} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{srai}$ | $rd$ $rs_1$ $i$ | $\begin{array}{llllll}\texttt{0b\_010\_0000} & \langle i_\texttt{SH} \rangle & \langle s_1 \rangle & \texttt{0b\_101} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{ori}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_110} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{andi}$ | $rd$ $rs_1$ $i$ | $\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_111} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}$ |
+| $\textbf{add}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{sub}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\texttt{0b\_010\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{sll}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{slt}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{sltu}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_011} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{xor}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{srl}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\texttt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_101} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{sra}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\texttt{0b\_010\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_101} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{or}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_110} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{and}$ | $rd$ $rs_1$ $rs_2$ | $\begin{array}{llllll}\mathtt{0b\_000\_0000} & \langle s_2 \rangle & \langle s_1 \rangle & \texttt{0b\_111} & \langle d \rangle & \texttt{0b\_011\_0011} \end{array}$ |
+| $\textbf{fence}$ | | $\begin{array}{ll} \mathtt{*^{25}} & \texttt{0b\_000\_1111} \end{array}$|
+| $\textbf{ecall}$ | $rd$ | $\begin{array}{lll} \texttt{0x00000} & \langle d \rangle & \texttt{0b\_111\_0011} \end{array}$|
+| $\textbf{ebreak}$ | $rd$ | $\begin{array}{lll} \texttt{0x00100} & \langle d \rangle & \texttt{0b\_111\_0011} \end{array}$|
+| $\textbf{unimp}$ | | $\begin{array}{lll} \texttt{0xc0001} & \mathtt{*^5} & \texttt{0b\_111\_0011} \end{array}$|
+
+The current architecture does not specify an output tape. Nevertheless, one can easily return arbitrary strings as output by encoding that string in some specific region of the memory.
### 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}$. 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}$.
+Each instruction in the program is loaded one at a time into the memory starting at address $\mathtt{0x0000}$.
### Nexus Virtual Machine Extensions
-While the universality of the current instruction set allows for executing any program on the Nexus VM, the translation process may yield inefficient programs due to the limited instruction set of the Nexus VM. As a result, proving the correctness of such computations within the Nexus zkVM may become infeasible for more complex programs. The cost of such an abstraction may be multiplied by more than a $1000$ factor for functions such as the SHA-256 circuit.
+While the universality of the current instruction set allows for executing any program on the Nexus VM, writing a program for the VM may yield inefficient programs due to the limited instruction set of the Nexus VM. As a result, proving the correctness of such computations within the Nexus zkVM may become infeasible for more complex programs. The cost of such an abstraction may be multiplied by more than a $1000$ factor for functions such as the SHA-256 circuit.
To deal with such scenarios, the Nexus Virtual Machine is being designed with extensibility in mind in order to enable the addition of custom instructions for more complex functions, such as hashing and signature verification.
@@ -228,13 +165,9 @@ Currently, the Nexus Virtual Machine uses universal circuits to simulate the who
Nevertheless, we will soon be switching to a *non-uniform* computation model based on recent advances in folding and accumulation techniques (e.g., [[KS22](#references)], [[BC23](#references)]), via the concept of *zkVM precompiles*. In the new model, the cost of proving custom precompile extensions of the NVM instruction set only occurs when that particular precompile is executed by the program.
-
-
The main advantage of using precompiles is that it maintains a developer-friendly CPU abstraction while efficiently allowing for the addition of more complex functions.
-Though we first expect to implement these special functions as part of the Nexus VM instruction set, we do intend to eventually support user-defined precompiles written as CCS circuits [[STW23](#references)] that could be provided as input to the Nexus zkVM. we expect to first implement these special functions as part of the Nexus VM instruction set. CCS circuits are a generalization of R1CS [[GGPR13](#references)], Plonkish [[GWC19; CBBZ23](#references)], and AIR [[BBHR19; Sta21; BCKL22](#references)].
+We intend to eventually support user-defined precompiles that could be provided as extensions of the Nexus zkVM. We expect to first implement these special functions as part of the Nexus VM instruction set.
### References
diff --git a/docs/pages/specs/roadmap.mdx b/docs/pages/specs/roadmap.mdx
index de2f5178..ad47a5f0 100644
--- a/docs/pages/specs/roadmap.mdx
+++ b/docs/pages/specs/roadmap.mdx
@@ -15,12 +15,12 @@ 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:
+### 3.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 3.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 Nexus 2.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.
6. **Modularized Compiler**: A modularized compiler toolchain that will break the Nexus compiler into smaller tools, that developers can use and extend to add support for new ISAs and languages.
-7. **Network**: A globally deployed network that users can contribute compute to.
\ No newline at end of file
+7. **Network**: A globally deployed network that users can contribute compute to.
diff --git a/docs/pages/specs/zkvm-overview.mdx b/docs/pages/specs/zkvm-overview.mdx
index 9f5a788a..05956ba8 100644
--- a/docs/pages/specs/zkvm-overview.mdx
+++ b/docs/pages/specs/zkvm-overview.mdx
@@ -11,7 +11,7 @@ The *Nexus Zero-Knowledge Virtual Machine* (***Nexus zkVM***) is a general compu
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)].
+The first iterations of the Nexus Virtual Machine provide support for circuits encoded in Rank-1 Constraint Satisfiability (R1CS). Future versions of the Nexus zkVM will provide support for user-defined circuits written in alternative constraint systems.
### References
@@ -19,22 +19,20 @@ The first iteration of the Nexus Virtual Machine provides support for circuits e
[[BCKL22](https://eprint.iacr.org/2022/1542)] Eli Ben-Sasson, Dan Carmon, Swastik Kopparty, and David Levit. “Scalable and transparent proofs over all large fields, via elliptic curves”. In: Electronic Colloquium on Computational Complexity, Report. Vol. 110. 2022, p. 2022
-[[CGTV20](https://www.scipr-lab.org/doc/TinyRAM-spec-2.000.pdf)] Eli Ben-Sasson Alessandro Chiesa, Daniel Genkin, Eran Tromer, and Madars Virza. “TinyRAM Architecture Specification v2. 000”. (2020)
+[[CGTV20](https://www.scipr-lab.org/doc/TinyRAM-spec-2.000.pdf)] Eli Ben-Sasson Alessandro Chiesa, Daniel Genkin, Eran Tromer, and Madars Virza. “TinyRAM Architecture Specification v2. 000”. (2020)
-[[CBBZ23](https://eprint.iacr.org/2022/1355)] Binyi Chen, Benedikt Bünz, Dan Boneh, and Zhenfei Zhang. “Hyperplonk: Plonk with linear-time prover and high-degree custom gates”. In EUROCRYPT 2023.
+[[CBBZ23](https://eprint.iacr.org/2022/1355)] Binyi Chen, Benedikt Bünz, Dan Boneh, and Zhenfei Zhang. “Hyperplonk: Plonk with linear-time prover and high-degree custom gates”. In EUROCRYPT 2023.
[[GGPR13](https://eprint.iacr.org/2012/215.pdf)] Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova. “Quadratic span programs and succinct NIZKs without PCPs”. In EUROCRYPT 2013.
[[GWC19](https://eprint.iacr.org/2019/953)] Ariel Gabizon, Zachary J Williamson, and Oana Ciobotaru. “Plonk: Permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge”. In: Cryptology ePrint Archive (2019)
-[[Sta21](https://eprint.iacr.org/2021/582)] StarkWare. ethSTARK Documentation. Cryptology ePrint Archive, Paper 2021/582.
+[[Sta21](https://eprint.iacr.org/2021/582)] StarkWare. ethSTARK Documentation. Cryptology ePrint Archive, Paper 2021/582.
[[STW23](https://eprint.iacr.org/2023/552)] Srinath Setty, Justin Thaler, and Riad Wahby. “Customizable constraint systems for succinct arguments”. In: Cryptology ePrint Archive (2023)
[[WLPA14](https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-54.pdf)] Andrew Waterman, Yunsup Lee, David A Patterson, and Krste Asanovic. “The RISC-V instruction set manual, volume I: User-level ISA, version 2.0”. In: EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-54 (2014)
-
[TinyRAM]: (https://www.scipr-lab.org/doc/TinyRAM-spec-2.000.pdf)
[RISCZero]: (https://www.risczero.com)
[zkMISP]: (https://whitepaper.zkm.io/whitepaper1.2.pdf)
-
diff --git a/docs/public/images/nvm-architecture.svg b/docs/public/images/nvm-architecture.svg
index 2d7b5c37..61fbd389 100644
--- a/docs/public/images/nvm-architecture.svg
+++ b/docs/public/images/nvm-architecture.svg
@@ -1,4 +1,4 @@
-
\ No newline at end of file
+
\ No newline at end of file