-
Notifications
You must be signed in to change notification settings - Fork 367
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.
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
Convert NVM Back to RV32 Base #164
Conversation
The latest updates on your projects. Learn more about Vercel for Git ↗︎
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM after the rd
for ECALL
and EBREAK
is generalized to support all possible 32 registers!
Co-authored-by: Sage Mitchell <[email protected]>
?addr, | ||
"Unsupported instruction", | ||
); | ||
return Err(Error::Unsupported(inst.inst)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Based on a discussion with @sjudson, I anticipated the Jolt prover wouldn't fully work yet, at least not with ECALL
s, but I also wanted to test and document the latest behavior.
I tried out the Jolt prover using the steps described at #159 (comment), except with --impl jolt
since it's no longer the default, and on the HEAD of this branch instead, currently adc3886.
The default "Hello, World" program fails with the following error:
$ cargo nexus prove --impl jolt
Compiling proc-macro2 v1.0.84
Compiling unicode-ident v1.0.12
Compiling syn v1.0.109
Compiling nexus-rt v1.0.0 (.../nexus-zkvm/only-riscv/runtime)
Compiling quote v1.0.36
Compiling nexus-rt-macros v0.1.0 (.../nexus-zkvm/only-riscv/runtime/macros)
Compiling pr-164 v0.1.0 (/private/tmp/pr-164)
Finished release-unoptimized [unoptimized] target(s) in 3.03s
Error: Instruction isn't supported: ecall x10
Based on the error message, it must be coming from the highlighted line. Again, this isn't surprising and on its own doesn't necessarily warrant blocking the PR since Jolt isn't the default prover.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I removed any source of ECALL
s in the program to prove/verify, the jolt
impl worked as expected. I've not audited to see what, if anything, the optimizer elided as dead code, but it's good to see there's no apparent regression here.
diff --git a/src/main.rs b/src/main.rs
index 69a7814..f271880 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -5,5 +5,8 @@ use nexus_rt::write_log;
#[nexus_rt::main]
fn main() {
- write_log("Hello, World!\n");
+ let mut i = 0;
+ while i < 10 {
+ i += 1;
+ }
}
Prove then verify with --impl jolt
:
$ cargo nexus prove --impl jolt
Compiling proc-macro2 v1.0.84
Compiling unicode-ident v1.0.12
Compiling syn v1.0.109
Compiling nexus-rt v1.0.0 (.../nexus-zkvm/only-riscv/runtime)
Compiling quote v1.0.36
Compiling nexus-rt-macros v0.1.0 (.../nexus-zkvm/only-riscv/runtime/macros)
Compiling pr-164 v0.1.0 (/private/tmp/pr-164)
warning: unused import: `nexus_rt::write_log`
...
Finished release-unoptimized [unoptimized] target(s) in 2.64s
Preprocessing bytecode ... 533ms
Finished in 533ms; bytecode size: 55
Executing program...
Executed 104 instructions in 8.011541ms
Proving program execution ... 2.5s
Finished in 2.5s
Saving proof ... 1ms
Finished in 1ms
$ cargo nexus verify --impl jolt
Preprocessing bytecode ... 480ms
Finished in 480ms; bytecode size: 55
Verifying proof ... 143ms
Finished in 143ms
While testing I discovered a regression with the current default prover implementation, First, reinstall the $ git rev-parse --short HEAD
adc3886
$ cargo install --path tools Generate a new Nexus project and point the runtime dependency to the local clone of this branch. $ cd /tmp
$ cargo nexus new pr-164
$ cd pr-164
$ cargo add nexus-rt --path <<LOCAL_CLONE>>/runtime And finally, run the prover followed by the verifier: $ cargo nexus prove
Compiling proc-macro2 v1.0.84
Compiling unicode-ident v1.0.12
Compiling syn v1.0.109
Compiling nexus-rt v1.0.0 (.../nexus-zkvm/only-riscv/runtime)
Compiling quote v1.0.36
Compiling nexus-rt-macros v0.1.0 (.../nexus-zkvm/only-riscv/runtime/macros)
Compiling pr-164 v0.1.0 (/private/tmp/pr-164)
Finished release-unoptimized [unoptimized] target(s) in 2.32s
Setting up public parameters for IVC ... 16.7s
Finished in 16.7s
Hello, World!
Loading public parameters ... 4.1s
Finished in 4.1s
Computing step 0 ... 653ms
Computing step 1 ... 744ms
Computing step 2 ... 904ms
Computing step 3 ... 944ms
Computing step 4 ... 929ms
Computing step 5 ... 926ms
Computing step 6 ... 948ms
Proved 7 step(s) in 6.1s; 18.51 instructions / second
Saving proof ... 23ms
Finished in 23ms
$ cargo nexus verify
Loading public parameters ... 4.5s
Finished in 4.5s
Verifying proof . 0ms
2024-05-29T18:21:13.403012-07:00 ERROR nexus-tools: Proof is invalid, err: not satisfied, k: 16, nova_impl: nova-seq When I repeated the following manual test on |
Appears to be an issue with tracking branching instructions for larger |
I repeated the same test with the default prover on f60ef84. It worked! |
In a line of work culminating in #53, we introduced a dedicated Nexus VM (NVM) ISA. Although this ISA is similar to RISC-V32i, it is not identical, and further uses a single 64-bit encoding for all instructions.
This change had the benefit of producing slightly smaller circuits (due to the circuit simplifications enabled by the single instruction encoding), as well as enabling some additional simple optimizations and other changes that had some forward-looking potential benefits as the NVM develops, aimed at the unique nature of a zkVM. On the other hand, this change also introduced a potentially unsound transformation from RISC-V to the NVM ISA that we would have to maintain, and also meant that existing tooling infrastructure and other zkVM techniques designed for RV32i would not be directly usable on the code the zkVM was actually executing/proving.
Recent developments in the zkVM space, particularly the significant performance improvements enabled by lookup arguments, have tipped the balance back in the other direction, and mean that it was probably a bit premature to move away from direct RV32i execution/proving. So this PR "reverts" that line of work, while also backporting new functionalities added since (e.g., private input tape reading and an unchecked, paged memory model).
This PR also formalizes an idea implicit in our existing RV32 implementation, which is to introduce an RV32Nexus ISA extension that captures overridden or new instructions (especially precompiles). At the moment, this extension includes overloaded versions of the
ECALL
andEBREAK
instructions, which are modified to the include ard
component (porting #150), thereby simplifying circuit generation. The VM now also keeps track of which instruction sets (RV32i or RV32Nexus) are used during the course of a given execution.We can think of the NVM ISA as now being composed of the RV32i + RV32Nexus ISAs, as well as any future extensions we might develop or import (such as multiplication or floating-point extensions).
The following snippet captures how this is defined in the code: