Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Spec update to v0.2.0 #216

Merged
merged 26 commits into from
Jul 16, 2024
Merged

Spec update to v0.2.0 #216

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
4559e92
Spec initial pass
yoichi-nexus Jul 8, 2024
387a629
Remove translation
yoichi-nexus Jul 9, 2024
f50b8ee
Update instruction list
yoichi-nexus Jul 9, 2024
1eaddff
Updating instruction layout table
yoichi-nexus Jul 9, 2024
4bc583f
Update prose
yoichi-nexus Jul 10, 2024
c50ca35
Describe auipc instruction
yoichi-nexus Jul 10, 2024
3c9f16b
Describe lui instruction
yoichi-nexus Jul 10, 2024
8f3813d
Fix typo
yoichi-nexus Jul 10, 2024
c5a406b
Describe unimp instruction
yoichi-nexus Jul 10, 2024
4cf6aa0
Describe fence instruction
yoichi-nexus Jul 10, 2024
1ffa68e
Another pass on the prose
yoichi-nexus Jul 10, 2024
123cc19
Add vm architecture drawio file
yoichi-nexus Jul 10, 2024
9baf43d
Update architecture diagram
yoichi-nexus Jul 10, 2024
1079889
Another pass
yoichi-nexus Jul 10, 2024
090856c
Review
yoichi-nexus Jul 10, 2024
35030c2
Review: ecall and ebreak take rd register selector
yoichi-nexus Jul 11, 2024
c566740
Strictor bit pattern as in RISC-V
yoichi-nexus Jul 11, 2024
3533b4d
Explicitly describe the sizes of immediates
yoichi-nexus Jul 11, 2024
92ce72b
Opcode vs mnemonic changes
yoichi-nexus Jul 11, 2024
1e4586a
Rephrase sign/zero extension
yoichi-nexus Jul 11, 2024
26cad33
lw doesn't perform any extension, zero or signed
yoichi-nexus Jul 11, 2024
828b233
More specific wording on which byte/half-word gets stored
yoichi-nexus Jul 11, 2024
b041a82
Add missing angle brackets
yoichi-nexus Jul 11, 2024
a9333c2
Modify version numbers
yoichi-nexus Jul 16, 2024
32457c5
Addressing review comments
yoichi-nexus Jul 16, 2024
9784dea
Change version sequences in the roadmap
yoichi-nexus Jul 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
147 changes: 147 additions & 0 deletions docs/assets/vm-architecture-v2.drawio
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,147 @@
<mxfile host="app.diagrams.net" modified="2024-07-10T14:51:44.602Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_7) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/126.0.0.0 Safari/537.36" etag="l7Lf5QJtHEjRTgupIl3P" version="24.6.4" type="device">
<diagram name="Page-1" id="I8bB1_BSA_W8SCRYw5Tl">
<mxGraphModel dx="934" dy="595" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="850" pageHeight="1100" math="1" shadow="0">
<root>
<mxCell id="0" />
<mxCell id="1" parent="0" />
<mxCell id="ex7kHfUKGhylopWH0X7d-3" value="" style="rounded=0;whiteSpace=wrap;html=1;strokeColor=none;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="100" y="120" width="600" height="380" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-43" value="$$M$$" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="590" y="130" width="60" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-47" value="$$\textrm{Private Input }I$$" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="191.25" y="320" width="254.75" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-1" value="" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="130" y="160" width="360" height="100" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-2" value="PC" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="410" y="192" width="40" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-46" value="" style="edgeStyle=elbowEdgeStyle;elbow=horizontal;endArrow=classic;html=1;curved=0;rounded=0;endSize=8;startSize=8;exitX=1;exitY=0.5;exitDx=0;exitDy=0;" parent="1" source="lRC7-Jg-s2bIB4YIQtNB-2" edge="1">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="447" y="212" as="sourcePoint" />
<mxPoint x="577" y="360" as="targetPoint" />
<Array as="points" />
</mxGeometry>
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-61" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;exitX=0.137;exitY=1.015;exitDx=0;exitDy=0;exitPerimeter=0;" parent="1" source="lRC7-Jg-s2bIB4YIQtNB-1" edge="1">
<mxGeometry relative="1" as="geometry">
<mxPoint x="311.24" y="321" as="targetPoint" />
<mxPoint x="162.25234567901248" y="241" as="sourcePoint" />
<Array as="points">
<mxPoint x="179" y="290" />
<mxPoint x="311" y="290" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-21" value="" style="rounded=0;whiteSpace=wrap;html=1;direction=south;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="576.5" y="160" width="90" height="320" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-25" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576.5" y="172" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-26" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576.5" y="188" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-27" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="577.5" y="204" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-28" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576.5" y="220" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-29" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576.5" y="459" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-30" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576.5" y="443" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-31" value="" style="line;strokeWidth=1;html=1;perimeter=backbonePerimeter;points=[];outlineConnect=0;" parent="1" vertex="1">
<mxGeometry x="576" y="430" width="90" height="12" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-36" value="" style="group" parent="1" vertex="1" connectable="0">
<mxGeometry x="614.5" y="289" width="20" height="42" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-33" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-36" vertex="1">
<mxGeometry y="11" width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-34" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-36" vertex="1">
<mxGeometry y="22" width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-35" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-36" vertex="1">
<mxGeometry width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-3" value="" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;" parent="1" vertex="1">
<mxGeometry x="151.5" y="192" width="225" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-6" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="175" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-9" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="202.5" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-10" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="230.5" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-11" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="258" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-12" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="316.5" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-13" value="" style="line;strokeWidth=1;direction=south;html=1;" parent="1" vertex="1">
<mxGeometry x="344.5" y="192" width="10" height="40" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-24" value="" style="group" parent="1" vertex="1" connectable="0">
<mxGeometry x="272.5" y="202" width="40" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-18" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-24" vertex="1">
<mxGeometry width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-22" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-24" vertex="1">
<mxGeometry x="10" width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="lRC7-Jg-s2bIB4YIQtNB-23" value="" style="shape=waypoint;sketch=0;fillStyle=solid;size=6;pointerEvents=1;points=[];fillColor=none;resizable=0;rotatable=0;perimeter=centerPerimeter;snapToPoint=1;" parent="lRC7-Jg-s2bIB4YIQtNB-24" vertex="1">
<mxGeometry x="20" width="20" height="20" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-96" value="$$x_0$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="136" y="197" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-97" value="$$x_1$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="163" y="197" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-99" value="$$x_2$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="191.25" y="197" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-100" value="$$x_3$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="220" y="197" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-101" value="$$x_{30}$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="306" y="198" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-102" value="$$x_{31}$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="334" y="198" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-104" value="$$R$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="232.5" y="165" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-105" value="$$2^{32}-2$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="517" y="441" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-106" value="$$2^{32}-1$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="516.5" y="458" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-107" value="$$0$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="532" y="154" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-109" value="$$1$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="532" y="170" width="60" height="30" as="geometry" />
</mxCell>
<mxCell id="U1pjUIA-5XBeJITS1JO2-110" value="$$2$$" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
<mxGeometry x="532" y="186" width="60" height="30" as="geometry" />
</mxCell>
</root>
</mxGraphModel>
</diagram>
</mxfile>
2 changes: 1 addition & 1 deletion docs/pages/index.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
yoichi-nexus marked this conversation as resolved.
Show resolved Hide resolved

## Proving Computation

Expand Down
2 changes: 1 addition & 1 deletion docs/pages/network.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

<Callout type="info" emoji="ℹ️">
The Nexus Network is currently in a prototype stage.
Expand Down
3 changes: 1 addition & 2 deletions docs/pages/specs/nexus-costs.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
6 changes: 3 additions & 3 deletions docs/pages/specs/nexus-memory-checking.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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

Expand All @@ -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)
Expand Down
Loading