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.

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

Merged
merged 47 commits into from
May 30, 2024
Merged

Convert NVM Back to RV32 Base #164

merged 47 commits into from
May 30, 2024

Conversation

sjudson
Copy link
Contributor

@sjudson sjudson commented May 28, 2024

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 and EBREAK instructions, which are modified to the include a rdcomponent (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:

    // BEGIN RV32Nexus EXTENSION

    // ECALL: An overload of the RV32i ECALL instruction, with explicit return.
    //
    //        In the RV32i spec, ECALL looks like:
    //
    //           00000 00 00000 00000 000 00000 11100 11
    //
    //        We overload the instruction as:
    //
    //           00000 00 00000 00000 000 {-rd} 11100 11
    //
    //        We then use rd as the return location for the ecall. By making the return
    //        explicit in this way, circuit generation is much cleaner since the memory
    //        updates involved are all captured explicitly in the instruction.
    ECALL { rd: u32 },

    // EBREAK: An overload of the RV32i EBREAK instruction, with explicit return.
    //
    //        In the RV32i spec, EBREAK looks like:
    //
    //           00000 00 00001 00000 000 00000 11100 11
    //
    //        We overload the instruction as:
    //
    //           00000 00 00001 00000 000 {-rd} 11100 11
    //
    //        We then use rd as the return location for the ebreak. By making the return
    //        explicit in this way, circuit generation is much cleaner since the memory
    //        updates involved are all captured explicitly in the instruction.
    EBREAK { rd: u32 },

@sjudson sjudson requested review from slumber and mx00s May 28, 2024 20:34
Copy link

vercel bot commented May 28, 2024

The latest updates on your projects. Learn more about Vercel for Git ↗︎

Name Status Preview Comments Updated (UTC)
nexus-docs ✅ Ready (Inspect) Visit Preview 💬 Add feedback May 30, 2024 4:26pm

vm/src/circuit/r1cs.rs Outdated Show resolved Hide resolved
vm/src/error.rs Outdated Show resolved Hide resolved
vm/src/eval.rs Show resolved Hide resolved
vm/src/rv32/parse.rs Outdated Show resolved Hide resolved
vm/src/rv32/parse.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@mx00s mx00s left a 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));
Copy link
Contributor

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

Copy link
Contributor

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

@mx00s
Copy link
Contributor

mx00s commented May 30, 2024

While testing I discovered a regression with the current default prover implementation, nova-seq.

First, reinstall the cargo-nexus binary from this branch:

$ 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 main (rev bc517fe) I found it succeeds; the regression must be in this branch.

@sjudson
Copy link
Contributor Author

sjudson commented May 30, 2024

Appears to be an issue with tracking branching instructions for larger k, just pushed up some code that seems to solve it on my end.

@mx00s
Copy link
Contributor

mx00s commented May 30, 2024

I repeated the same test with the default prover on f60ef84. It worked!

@sjudson sjudson merged commit 119f74a into main May 30, 2024
6 checks passed
@sjudson sjudson deleted the only-riscv branch May 30, 2024 19:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants