​
Nexus Virtual Machine

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. 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.

​
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…232−1}\{0\ldots 2^{32}-1\}. The state of the machine is defined as a four-tuple, (pc;M;R;I)(pc;M;R;I), where

  • pcpc denotes the program counter register;
  • MM denotes the memory;
  • RR denotes the state of registers;
  • II is the private input.

Both MM and RR are finite maps. The keys of MM are addresses in the range {0,…,232−1}\{0,\ldots, 2^{32}-1\}. The values of MM are 8-bit bytes. The keys of RR are register selectors from the set {x0…x31}\{x_0\ldots x_{31}\}. The values of RR are 32-bit words. A word (resp. a halfword) is represented as four (resp. two) consecutive bytes in little endian. By design, updates to register x0x_0 are ignored and the value of R[x0]R[x_0] is always zero.

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 2322^{32} for efficiency reasons.

At initialization, all the general-purpose registers are set to 0. The program counter pcpc is set to 0x0000\mathtt{0x0000}. The private input tape contains the byte-encoded private input for the program. Since pcpc is initially 0x0000\mathtt{0x0000}, the first instruction to be executed will be the one stored at the position 0x0000\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 pcpc is always advanced by 4 bytes after the execution of each instruction, unless the instruction itself sets the value of pcpc. Moreover, the Nexus VM enforces 4-byte memory alignment for the program counter by checking that pcpc is a multiple of 4 when reading an instruction.

​
Nexus Virtual Machine Instruction Set

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:

  • mnemonic\textbf{mnemonic} is a string name of the instruction;
  • rdrd is a register selector specifying the destination register;
  • rs1rs_1 is a register selector specifying the first operand;
  • rs2rs_2 is a register selector specifying the second operand; and
  • ii is an immediate value, whose size varies according to instructions.

Table: Summary of the Nexus Virtual Machine Instruction Set, where operations are mod 2322^{32}.

Instruction mnemonicArgumentsDescription of functionality
lui\textbf{lui}rdrd iisets R[rd]R[rd] to ii
auipc\textbf{auipc}rdrd iisets R[rd]R[rd] to pc+ipc+i
add\textbf{add}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to R[rs1]+R[rs2]R[rs_1] + R[rs_2]
addi\textbf{addi}rdrd rs1rs_1 iisets R[rd]R[rd] to R[rs1]+iR[rs_1] + i
sub\textbf{sub}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to R[rs1]−R[rs2]R[rs_1] - R[rs_2]
slt\textbf{slt}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to (R[rs1]<R[rs2])(R[rs_1] < R[rs_2]) (signed comparison)
slti\textbf{slti}rdrd rs1rs_1 iisets R[rd]R[rd] to (R[rs1]<i)(R[rs_1] < i) (signed comparison)
sltu\textbf{sltu}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to (R[rs1]<R[rs2])(R[rs_1] < R[rs_2]) (unsigned comparison)
sltui\textbf{sltui}rdrd rs1rs_1 iisets R[rd]R[rd] to (R[rs1]<i)(R[rs_1] < i) (unsigned comparison)
sll\textbf{sll}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to R[rs1]≪R[rs2]&0x1FR[rs_1] \ll R[rs_2] \mathbin{\&} \mathtt{0x1F}
slli\textbf{slli}rdrd rs1rs_1 iisets R[rd]R[rd] to R[rs1]≪i&0x1FR[rs_1] \ll i \mathbin{\&} \mathtt{0x1F}
srl\textbf{srl}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to R[rs1]≫R[rs2]&0x1FR[rs_1] \gg R[rs_2] \mathbin{\&} \mathtt{0x1F} (with zero extension)
srli\textbf{srli}rdrd rs1rs_1 iisets R[rd]R[rd] to R[rs1]≫i&0x1FR[rs_1] \gg i \mathbin{\&} \mathtt{0x1F} (with zero extension)
sra\textbf{sra}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to R[rs1]≫R[rs2]&0x1FR[rs_1] \gg R[rs_2] \mathbin{\&} \mathtt{0x1F} (with sign extension)
srai\textbf{srai}rdrd rs1rs_1 iisets R[rd]R[rd] to R[rs1]≫i&0x1FR[rs_1] \gg i \mathbin{\&} \mathtt{0x1F} (with sign extension)
xor\textbf{xor}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to the bitwise XOR of R[rs1]R[rs_1] and R[rs2]R[rs_2]
xori\textbf{xori}rdrd rs1rs_1 iisets R[rd]R[rd] to the bitwise XOR of R[rs1]R[rs_1] and ii
and\textbf{and}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to the bitwise AND of R[rs1]R[rs_1] and R[rs2]R[rs_2]
andi\textbf{andi}rdrd rs1rs_1 iisets R[rd]R[rd] to the bitwise AND of R[rs1]R[rs_1] and ii
or\textbf{or}rdrd rs1rs_1 rs2rs_2sets R[rd]R[rd] to the bitwise OR of R[rs1]R[rs_1] and R[rs2]R[rs_2]
ori\textbf{ori}rdrd rs1rs_1 iisets R[rd]R[rd] to the bitwise OR of R[rs1]R[rs_1] and ii
beq\textbf{beq}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]=R[rs2])(R[rs_1] = R[rs_2])
bne\textbf{bne}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]≠R[rs2])(R[rs_1] \not= R[rs_2])
blt\textbf{blt}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]<R[rs2])(R[rs_1] < R[rs_2]) (signed comparison)
bge\textbf{bge}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]≥R[rs2])(R[rs_1] \geq R[rs_2]) (signed comparison)
bltu\textbf{bltu}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]<R[rs2])(R[rs_1] < R[rs_2]) (unsigned comparison)
bgeu\textbf{bgeu}rs1rs_1 rs2rs_2 iibranches to pc+ipc+i if (R[rs1]≥R[rs2])(R[rs_1] \geq R[rs_2]) (unsigned comparison)
lb\textbf{lb}rdrd rs1rs_1 iiloads the sign extension of the byte at M[R[rs1]+i]M[R[rs_1] + i] into R[rd]R[rd]
lh\textbf{lh}rdrd rs1rs_1 iiloads the sign extension of the half-word at M[R[rs1]+i]M[R[rs_1] + i] into R[rd]R[rd]
lw\textbf{lw}rdrd rs1rs_1 iiloads the word at M[R[rs1]+i]M[R[rs_1] + i] into R[rd]R[rd]
lbu\textbf{lbu}rdrd rs1rs_1 iiloads the zero extension of the byte at M[R[rs1]+i]M[R[rs_1] + i] into R[rd]R[rd]
lhu\textbf{lhu}rdrd rs1rs_1 iiloads the zero extension of the half-word at M[R[rs1]+i]M[R[rs_1] + i] into R[rd]R[rd]
sb\textbf{sb}rs1rs_1 rs2rs_2 iistores the least significant byte of R[rs2]R[rs_2] at M[R[rs1]+i]M[R[rs_1] + i]
sh\textbf{sh}rs1rs_1 rs2rs_2 iistores the less significant half-word of R[rs2]R[rs_2] at M[R[rs1]+i]M[R[rs_1] + i]
sw\textbf{sw}rs1rs_1 rs2rs_2 iistores R[rs2]R[rs_2] at M[R[rs1]+i]M[R[rs_1] + i]
jal\textbf{jal}rdrd iijumps to pc+ipc+i and stores pc+4pc+4 into R[rd]R[rd]
jalr\textbf{jalr}rdrd rs1rs_1 iijumps to R[rs1]+iR[rs_1] + i and stores pc+4pc+4 into R[rd]R[rd]
fence\textbf{fence}No operation
ecall\textbf{ecall}rdrdsystem call
ebreak\textbf{ebreak}rdrdsystem call
unimp\textbf{unimp}jumps to pcpc; 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 opcode\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*^m denotes any binary string of mm bits, and ⟨d⟩\langle d \rangle, ⟨s1⟩\langle s_1 \rangle, ⟨s2⟩\langle s_2 \rangle denote respectively the binary representation of the 5-bit-long register selectors rdrd, rs1rs_1, rs2rs_2.

The notation ⟨ix⟩\langle i_x \rangle each denote immediate values, interpreted the same way as xx-immediate values of 32-bit RISC-V architecture. Some immediate values (type B and S) occupy discontiguous positions, so their fragments are written as ⟨ix0⟩\langle i_\texttt{x0} \rangle and ⟨ix1⟩\langle i_\texttt{x1} \rangle. ⟨iSH⟩\langle i_\texttt{SH} \rangle denotes a 5-bit long immediate value.

⟨iU⟩\langle i_\texttt{U}\rangle and ⟨iJ⟩\langle i_\texttt{J}\rangle contain 20 bits. ⟨iI⟩\langle i_\texttt{I}\rangle contains 12 bits. ⟨iS0⟩\langle i_\texttt{S0}\rangle and ⟨iB0⟩\langle i_\texttt{B0}\rangle contain 5 bits. ⟨iS1⟩\langle i_\texttt{S1}\rangle and ⟨iB1⟩\langle i_\texttt{B1}\rangle contain 7 bits.

Instruction mnemonicArgumentsBinary Encodings (left: most significant bit)
lui\textbf{lui}rdrd ii⟨iU⟩⟨d⟩0b_011_0111\begin{array}{lll} \langle i_\texttt{U} \rangle & \langle d \rangle & \texttt{0b\_011\_0111} \end{array}
auipc\textbf{auipc}rdrd ii⟨iU⟩⟨d⟩0b_001_0111\begin{array}{lll} \langle i_\texttt{U} \rangle & \langle d \rangle & \texttt{0b\_001\_0111} \end{array}
jal\textbf{jal}rdrd ii⟨iJ⟩⟨d⟩0b_110_1111\begin{array}{lll} \langle i_\texttt{J} \rangle & \langle d \rangle & \texttt{0b\_110\_1111} \end{array}
jalr\textbf{jalr}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_000⟨d⟩0b_110_0111\begin{array}{llllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \mathtt{0b\_000} & \langle d \rangle & \texttt{0b\_110\_0111} \end{array}
beq\textbf{beq}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_000⟨iB0⟩   0b_110_0011\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}
bne\textbf{bne}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_001⟨iB0⟩   0b_110_0011\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}
blt\textbf{blt}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_100⟨iB0⟩   0b_110_0011\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}
bge\textbf{bge}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_101⟨iB0⟩   0b_110_0011\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}
bltu\textbf{bltu}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_110⟨iB0⟩   0b_110_0011\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}
bgeu\textbf{bgeu}rs1rs_1 rs2rs_2 ii⟨iB1⟩⟨s2⟩⟨s1⟩0b_111⟨iB0⟩   0b_110_0011\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}
lb\textbf{lb}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_000⟨d⟩0b_000_0011\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}
lh\textbf{lh}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_001⟨d⟩0b_000_0011\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}
lw\textbf{lw}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_010⟨d⟩0b_000_0011\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}
lbu\textbf{lbu}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_011⟨d⟩0b_000_0011\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_011} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}
lhu\textbf{lhu}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_100⟨d⟩0b_000_0011\begin{array}{lllll} \langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle d \rangle &\texttt{0b\_000\_0011}\end{array}
sb\textbf{sb}rs1rs_1 rs2rs_2 ii⟨iS1⟩⟨s2⟩⟨s1⟩0b_000⟨iS0⟩0b_010_0011\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}
sh\textbf{sh}rs1rs_1 rs2rs_2 ii⟨iS1⟩⟨s2⟩⟨s1⟩0b_001⟨iS0⟩0b_010_0011\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}
sw\textbf{sw}rs1rs_1 rs2rs_2 ii⟨iS1⟩⟨s2⟩⟨s1⟩0b_010⟨iS0⟩0b_010_0011\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}
addi\textbf{addi}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_000⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_000} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
slli\textbf{slli}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_001⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_001} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
slti\textbf{slti}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_010⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_010} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
sltui\textbf{sltui}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_011⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_011} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
xori\textbf{xori}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_100⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_100} & \langle d \rangle & \texttt{0b\_001\_0011}\end{array}
srli\textbf{srli}rdrd rs1rs_1 ii0b_000_0000⟨iSH⟩⟨s1⟩0b_101⟨d⟩0b_001_0011\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}
srai\textbf{srai}rdrd rs1rs_1 ii0b_010_0000⟨iSH⟩⟨s1⟩0b_101⟨d⟩0b_001_0011\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}
ori\textbf{ori}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_110⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_110} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
andi\textbf{andi}rdrd rs1rs_1 ii⟨iI⟩⟨s1⟩0b_111⟨d⟩0b_001_0011\begin{array}{lllll}\langle i_\texttt{I} \rangle & \langle s_1 \rangle & \texttt{0b\_111} & \langle d \rangle & \texttt{0b\_001\_0011} \end{array}
add\textbf{add}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_000⟨d⟩0b_011_0011\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}
sub\textbf{sub}rdrd rs1rs_1 rs2rs_20b_010_0000⟨s2⟩⟨s1⟩0b_000⟨d⟩0b_011_0011\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}
sll\textbf{sll}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_001⟨d⟩0b_011_0011\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}
slt\textbf{slt}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_010⟨d⟩0b_011_0011\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}
sltu\textbf{sltu}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_011⟨d⟩0b_011_0011\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}
xor\textbf{xor}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_100⟨d⟩0b_011_0011\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}
srl\textbf{srl}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_101⟨d⟩0b_011_0011\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}
sra\textbf{sra}rdrd rs1rs_1 rs2rs_20b_010_0000⟨s2⟩⟨s1⟩0b_101⟨d⟩0b_011_0011\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}
or\textbf{or}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_110⟨d⟩0b_011_0011\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}
and\textbf{and}rdrd rs1rs_1 rs2rs_20b_000_0000⟨s2⟩⟨s1⟩0b_111⟨d⟩0b_011_0011\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}
fence\textbf{fence}∗250b_000_1111\begin{array}{ll} \mathtt{*^{25}} & \texttt{0b\_000\_1111} \end{array}
ecall\textbf{ecall}rdrd0x00000⟨d⟩0b_111_0011\begin{array}{lll} \texttt{0x00000} & \langle d \rangle & \texttt{0b\_111\_0011} \end{array}
ebreak\textbf{ebreak}rdrd0x00100⟨d⟩0b_111_0011\begin{array}{lll} \texttt{0x00100} & \langle d \rangle & \texttt{0b\_111\_0011} \end{array}
unimp\textbf{unimp}0xc0001∗50b_111_0011\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 pcpc is also set to 0x0000\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.

Each instruction in the program is loaded one at a time into the memory starting at address 0x0000\mathtt{0x0000}.

​
Nexus Virtual Machine Extensions

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 10001000 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.

Currently, the Nexus Virtual Machine uses universal circuits to simulate the whole CPU and this unfortunately increases the complexity of the Nexus Proof System with each additional instruction.

Nevertheless, we will soon be switching to a non-uniform computation model based on recent advances in folding and accumulation techniques (e.g., [KS22], [BC23]), 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.

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

[BBHR19] Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev. “Scalable zero knowledge with no trusted setup”. In CRYPTO 2019.

[BC23] Benedikt Bünz and Binyi Chen. “Protostar: Generic efficient accumulation/folding for special sound protocols”. In: Cryptology ePrint Archive (2023)

[BCKL22] 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

[CBBZ23] 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] Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova. “Quadratic span programs and succinct NIZKs without PCPs”. In EUROCRYPT 2013.

[GWC19] Ariel Gabizon, Zachary J Williamson, and Oana Ciobotaru. “Plonk: Permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge”. In: Cryptology ePrint Archive (2019)

[KS22] Abhiram Kothapalli and Srinath Setty. “SuperNova: Proving universal machine executions without universal circuits”. In: Cryptology ePrint Archive (2022)

[Sta21] StarkWare. ethSTARK Documentation. Cryptology ePrint Archive, Paper 2021/582.

[STW23] Srinath Setty, Justin Thaler, and Riad Wahby. “Customizable constraint systems for succinct arguments”. In: Cryptology ePrint Archive (2023)

Was this page helpful?

OverviewNexus Proof System