merge Sparsify -> Multi-Offset-Eq

Cargo.toml

@@ -61,9 +61,15 @@ clap = { version = "4.5.4", features = ["derive"] }
 eyre = "0.6.12"
 rand = "0.8.5"
 sysinfo = "0.30.8"
+syn = { version = "1.0.0", features = ["full"] }
+serde = { version = "1.0", features = ["derive"] }
+serde_json = "1.0.68"
+rmp-serde = "1.3.0"
+toml_edit = "0.22.14"
 
 jolt-sdk = { path = "./jolt-sdk" }
 jolt-core = { path = "./jolt-core" }
+common = { path = "./common" }
 
 [profile.test]
 opt-level = 3

README.md

@@ -10,7 +10,7 @@ The Jolt [paper](https://eprint.iacr.org/2023/1217.pdf) was written by Arasu Aru
 
 ## Resources
 
-- [Docs](https://jolt.a16zcrypto.com/)
+- [Docs](https://jolt.a16zcrypto.com/) (The Jolt Book)
 - Blog posts
   - [Accelerating the world computer: Implementing Jolt, a new state-of-the-art zkVM](https://a16zcrypto.com/posts/article/accelerating-the-world-computer-implementing-jolt)
   - [Building Jolt: A fast, easy-to-use zkVM](https://a16zcrypto.com/posts/article/building-jolt/)

book/src/SUMMARY.md

@@ -9,6 +9,7 @@
         - [Hosts](./usage/hosts.md)
     - [Allocators](./usage/allocators.md)
     - [Standard Library](./usage/stdlib.md)
+    - [WASM Support](./usage/wasm_support.md)
     - [Troubleshooting](./usage/troubleshooting.md)
 - [Contributors](./contributors.md)
     - [How it works](./how_it_works.md)
@@ -32,3 +33,6 @@
     - [Roadmap](./tasks.md)
         - [Optimizations](./future/opts.md)
         - [Zero Knowledge](./future/zk.md)
+        - [Groth16 Recursion](./future/groth-16.md)
+        - [Precompiles](./future/precompiles.md)
+        - [Continuations](./future/continuations.md)

book/src/future/continuations.md

@@ -0,0 +1,10 @@
+# Continuations via Chunking
+Today Jolt is a monolithic SNARK. RISC-V traces cannot be broken up, they must be proven monolithically or not at all. As a result, Jolt has a fixed maximum trace length that can be proved which is a function of the available RAM on the prover machine. Long term we'd like to solve this by implementing a streaming version of Jolt's prover such that prover RAM usage is tunable with minimal performance loss. *TODO(sragss): Streaming prover link*
+
+Short term we're going to solve this via monolithic chunking. The plan: Take a trace of length $N$ split it into $M$ chunks of size $N/M$ and prove each independently. $N/M$ is a function of the max RAM available to the prover. 
+
+For the direct on-chain verifier there will be a cost linear in $M$ to verify. If we wrap this in Groth16 our cost will become constant but the Groth16 prover time will be linear in $M$. We believe this short-term trade-off is worthwhile for usability until we can implement the (more complicated) streaming algorithms. 
+
+## Specifics
+A generic config parameter will be added to the `Jolt` struct called `ContinuationConfig`. At the highest level, before calling `Jolt::prove` the trace will be split into `M` chunks. `Jolt::prove` will be called on each and return `RAM_final` which can be fed into `RAM_init` during the next iteration of `Jolt::prove`. The [output zerocheck](https://jolt.a16zcrypto.com/how/read_write_memory.html#ouputs-and-panic) will only be run for the final chunk. 
+

book/src/future/groth-16.md

@@ -0,0 +1,60 @@
+# Groth16 Recursion
+Jolt's verifier today is expensive. We estimate 1-5 million gas to verify within the EVM. Better batching techniques on opening proofs can bring this down 5-10x, but it will remain expensive. Further, the short-term [continuations plan](https://jolt.a16zcrypto.com/future/continuations.html) causes a linear blowup depending on the count of monolithic trace chunks proven.
+
+To solve these two issues we're aiming to add a configuration option to the Jolt prover with a post processing step, which creates a Groth16 proof of the Jolt verifier for constant proof size / cost (~280k gas on EVM) regardless of continuation chunk count or opening proof cost. This technique is industry standard.
+
+## Strategy
+The easiest way to understand the workload of the verifier circuit is to jump through the codebase starting at `vm/mod.rs Jolt::verify(...)`.  Verification can be split into 4 logical modules: [instruction lookups](https://jolt.a16zcrypto.com/how/instruction_lookups.html), [read-write memory](https://jolt.a16zcrypto.com/how/read_write_memory.html), [bytecode](https://jolt.a16zcrypto.com/how/bytecode.html), [r1cs](https://jolt.a16zcrypto.com/how/r1cs_constraints.html).
+
+Each of the modules do some combination of the following:
+- [Sumcheck verification](https://jolt.a16zcrypto.com/background/sumcheck.html)
+- Polynomial opening proof verification
+- Multi-linear extension evaluations
+
+After recursively verifying sumcheck, the verifier needs to compare the claimed evaluation of the sumcheck operand at a random point $r$: $S(r)$ to their own evaluation of the polynomial at $r$. Jolt does this with a combination of opening proofs over the constituent polynomials of $S$ and direct evaluations of the multi-linear extensions of those polynomials if they have sufficient structure. 
+
+## Specifics
+### Polynomial opening proof verification 
+HyperKZG is currently the optimal commitment scheme for recursion due to the requirement of only 2-pairing operations per opening proof. Unfortunately non-native field arithmetic will always be expensive within a circuit. 
+
+There are two options:
+- Sumcheck and MLE evaluations using native arithmetic, pairing operations using non-native arithmetic
+- Sumcheck and MLE evaluations using non-native arithmetic, pairing operations using native arithmetic
+
+We believe the latter is more efficient albeit unergonomic. Some of the details are worked out in this paper [here](https://eprint.iacr.org/2023/961.pdf).
+
+### Polynomial opening proof batching
+Jolt requires tens of opening proofs across all constituent polynomials in all sumchecks. If we did these independently the verifier would be prohibitively expensive. Instead we [batch](https://jolt.a16zcrypto.com/background/batched-openings.html) all opening proofs for polynomials which share an evaluation point $r$. 
+
+### verify_instruction_lookups
+Instruction lookups does two sumchecks described in more detail [here](https://jolt.a16zcrypto.com/how/instruction_lookups.html). The first contains some complexity. The evaluation of the MLE of each of the instructions at the point $r$ spit out by sumcheck is computed directly by the verifier. The verifier is able to do this thanks to the property from Lasso that each table is SOS (decomposable). 
+
+The `LassoSubtable` trait is implemented for all subtables. `LassoSubtable::evaluate_mle(r)` computes the MLE of each subtable. The `JoltInstruction` trait combines a series of underlying subtables. The MLEs of these subtables are combined to an instruction MLE via `JoltInstruction::combine_lookups(vals: &[F])`. Finally each of the instruction MLEs are combined into a VM-wide lookup MLE via `InstructionLookupsProof::combine_lookups(...)`.
+
+The Groth16 verifier circuit would have to mimic this pattern. Implementing the MLE evaluation logic for each of the subtables, combination logic for each of the instructions, and combination logic to aggregate all instructions. It's possible that subtables / instructions will be added / removed in the future.
+
+### verify_r1cs
+[R1CS](https://jolt.a16zcrypto.com/how/r1cs_constraints.html)  is a modified Spartan instance which runs two sumchecks and a single opening proof.
+
+There are two difficult MLEs to evaluate:
+- $\widetilde{A}, \widetilde{B}, \widetilde{C}$  – evaluations of the R1CS coefficient
+- $\widetilde{z}$ – evaluation of the witness vector 
+
+> The sections below are under-described in the wiki. We'll flush these out shortly. Assume this step comes last.
+
+For $\widetilde{A}, \widetilde{B}, \widetilde{C}$ we must leverage the uniformity to efficiently evaluate. This is under-described in the wiki, but we'll get to it ASAP.
+
+The witness vector $z$ is comprised of all of the inputs to the R1CS circuit concatenated together in `trace_length`-sized chunks. All of these are committed independently and are checked via a batched opening proof.
+
+
+# Engineering Suggestions
+The Jolt codebase is rapidly undergoing improvements to reduce prover and verifier costs as well as simplify abstractions. As a result, it's recommended that each section above be built in modules that are convenient to rewire. Each part should be incrementally testable and adjustable. 
+
+A concrete example of changes to expect: we currently require 5-10 opening proofs per Jolt execution. Even for HyperKZG this requires 10-20 pairings which is prohibitively expensive. We are working on fixing this via better [batching](https://jolt.a16zcrypto.com/background/batched-openings.html).
+
+Suggested plan of attack:
+1. Circuit for HyperKZG verification
+2. Circuit for batched HyperKZG verification
+3. Circuit for sumcheck verification
+4. Circuit for instruction/subtable MLE evaluations
+5. Circuit for Spartan verification

book/src/future/precompiles.md

@@ -0,0 +1,15 @@
+# Precompiles
+Precompiles are highly optimized SNARK gadgets which can be invoked from the high-level programming language of the VM user. These gadgets can be much more efficient for the prover than compiling down to the underlying ISA by exploiting the structure of the workload. In practice zkVMs use these for heavy cryptographic operations such as hash functions, signatures and other elliptic curve arithmetic.
+
+By popular demand, Jolt will support these gadgets as well. The short term plan is to optimize for minimizing Jolt-core development resources rather than optimal prover speed.
+
+Precompile support plan:
+1. RV32 library wrapping syscalls of supported libraries
+2. Tracer picks up syscalls, sets relevant flag bits and loads memory accordingly
+3. Individual (uniform) Spartan instance for each precompile, repeated over `trace_length` steps
+4. Jolt config includes which precompiles are supported (there is some non-zero prover / verifier cost to including an unused precompile)
+5. Survey existing hash / elliptic curve arithmetic R1CS arithmetizations. Prioritize efficiency and audits.
+6. Use [circom-scotia](https://github.com/lurk-lab/circom-scotia) to convert $A, B, C$ matrices into static files in the Jolt codebase
+7. Write a converter to uniformly repeat the constraints `trace_length` steps
+
+*TODO(sragss): How do we deal with memory and loading more than 64-bits of inputs to precompiles.*

book/src/usage/wasm_support.md

@@ -0,0 +1,118 @@
+# WASM Support
+
+Jolt supports WebAssembly compatibility for the verification side of provable functions. This allows developers to run proof verification in WASM environments such as web browsers. Note that currently, only the verification process is supported in WASM; the proving process is not WASM-compatible at this time.
+
+## Creating a WASM-Compatible Project
+
+To create a new project with WASM verification support, use the following command:
+
+```bash
+jolt new <PROJECT_NAME> --wasm
+```
+
+This creates a new project with the necessary structure and configuration for WASM-compatible verification.
+
+## Marking Functions for WASM Verification
+
+For functions whose verification process should be WASM-compatible, extend the `#[jolt::provable]` macro with the `wasm` attribute:
+
+```rust
+#[jolt::provable(wasm)]
+fn my_wasm_verifiable_function() {
+    // function implementation
+}
+```
+
+## Building for WASM Verification
+
+To compile your project for WASM verification, use the following command:
+
+```bash
+jolt build-wasm
+```
+
+This command performs several actions:
+
+1. It extracts all functions marked with `#[jolt::provable(wasm)` from your `guest/src/lib.rs` file.
+2. For each WASM-verifiable function, it preprocesses the function and saves the necessary verification data.
+3. It creates an `index.html` file as an example of how to use your WASM-compiled verification functions in a web environment.
+4. It uses wasm-pack to build your project, targeting web environments.
+
+> **Important:** The build process only compiles the verification functions for WASM. The proving process must still be performed outside of the WASM environment.
+
+## Adding Dependencies
+
+When adding new dependencies for WASM-compatible projects, note that they must be added to both guest/Cargo.toml and the root Cargo.toml. The build-wasm process will automatically add necessary WASM-related dependencies to your project.
+
+## Switching Between WASM and Normal Compilation
+
+The build process modifies the `Cargo.toml` files to enable WASM compilation. If you need to switch back to normal compilation, you may need to manually adjust these files. In the root `Cargo.toml`, you can remove the following lines:
+
+```toml
+[lib]
+crate-type = ["cdylib"]
+path = "guest/src/lib.rs"
+```
+
+Remember to restore these lines before attempting another WASM build.
+
+## Example Project Structure
+
+After running `jolt build-wasm`, your project will include:
+
+- An `index.html` file in the root directory, providing a basic interface to verify proofs for each of your WASM-verifiable functions.
+- A `pkg` directory containing the WASM-compiled version of your project's verification functions.
+- Preprocessed data files for each WASM-verifiable function in the `target/wasm32-unknown-unknown/release/` directory.
+
+You can use this example as a starting point and customize it to fit your specific requirements.
+
+### Example: Modifying the Quickstart Project
+
+You can use the example from the [Quickstart](./quickstart.md#project-tour) chapter and modify the `/src/main.rs` file as follows:
+
+```rust
+pub fn main() {
+    let (prove_fib, _verify_fib) = guest::build_fib();
+
+    let (_output, proof) = prove_fib(50);
+
+    proof
+        .save_to_file("proof.bin")
+        .expect("Failed to save proof to file");
+}
+```
+
+Remember to modify the `Cargo.toml` as described [before](#switching-between-wasm-and-normal-compilation) for normal compilation, and then you can generate and save the proof with the following command:
+
+```bash
+cargo run -r
+```
+
+This will create a `proof.bin` file in the root directory. You can then verify this proof using the example `index.html`. Before doing this, change the crate type back to `cdylib` in the `Cargo.toml` and ensure that your `/guest/src/lib.rs` looks like this:
+
+```rust
+#![cfg_attr(feature = "guest", no_std)]
+#![no_main]
+
+#[jolt::provable(wasm)]
+fn fib(n: u32) -> u128 {
+    let mut a: u128 = 0;
+    let mut b: u128 = 1;
+    let mut sum: u128;
+    for _ in 1..n {
+        sum = a + b;
+        a = b;
+        b = sum;
+    }
+
+    b
+}
+```
+
+Then run `jolt build-wasm`. After successful compilation, you can verify the proof using the `index.html` file. Start a local server from the project directory, for example with:
+
+```bash
+npx http-server .
+```
+
+> Note: Make sure you have `npx` installed to use the `http-server` command.

common/Cargo.toml

@@ -8,3 +8,4 @@ ark-serialize = { version = "0.4.2", features = ["derive"] }
 serde = { version = "1.0.193", features = ["derive"] }
 serde_json = "1.0.108"
 strum_macros = "0.25.3"
+syn = { version = "1.0", features = ["full"] }

common/src/attributes.rs

@@ -0,0 +1,61 @@
+use std::collections::HashMap;
+use syn::{Lit, Meta, MetaNameValue, NestedMeta};
+
+use crate::constants::{
+    DEFAULT_MAX_INPUT_SIZE, DEFAULT_MAX_OUTPUT_SIZE, DEFAULT_MEMORY_SIZE, DEFAULT_STACK_SIZE,
+};
+
+pub struct Attributes {
+    pub wasm: bool,
+    pub memory_size: u64,
+    pub stack_size: u64,
+    pub max_input_size: u64,
+    pub max_output_size: u64,
+}
+
+pub fn parse_attributes(attr: &Vec<NestedMeta>) -> Attributes {
+    let mut attributes = HashMap::<_, u64>::new();
+    let mut wasm = false;
+
+    for attr in attr {
+        match attr {
+            NestedMeta::Meta(Meta::NameValue(MetaNameValue { path, lit, .. })) => {
+                let value: u64 = match lit {
+                    Lit::Int(lit) => lit.base10_parse().unwrap(),
+                    _ => panic!("expected integer literal"),
+                };
+                let ident = &path.get_ident().expect("Expected identifier");
+                match ident.to_string().as_str() {
+                    "memory_size" => attributes.insert("memory_size", value),
+                    "stack_size" => attributes.insert("stack_size", value),
+                    "max_input_size" => attributes.insert("max_input_size", value),
+                    "max_output_size" => attributes.insert("max_output_size", value),
+                    _ => panic!("invalid attribute"),
+                };
+            }
+            NestedMeta::Meta(Meta::Path(path)) if path.is_ident("wasm") => {
+                wasm = true;
+            }
+            _ => panic!("expected integer literal"),
+        }
+    }
+
+    let memory_size = *attributes
+        .get("memory_size")
+        .unwrap_or(&DEFAULT_MEMORY_SIZE);
+    let stack_size = *attributes.get("stack_size").unwrap_or(&DEFAULT_STACK_SIZE);
+    let max_input_size = *attributes
+        .get("max_input_size")
+        .unwrap_or(&DEFAULT_MAX_INPUT_SIZE);
+    let max_output_size = *attributes
+        .get("max_output_size")
+        .unwrap_or(&DEFAULT_MAX_OUTPUT_SIZE);
+
+    Attributes {
+        wasm,
+        memory_size,
+        stack_size,
+        max_input_size,
+        max_output_size,
+    }
+}

common/src/lib.rs

@@ -2,6 +2,7 @@ pub fn to_ram_address(index: usize) -> usize {
     index * constants::BYTES_PER_INSTRUCTION + constants::RAM_START_ADDRESS as usize
 }
 
+pub mod attributes;
 pub mod constants;
 pub mod parallel;
 pub mod rv_trace;

common/src/rv_trace.rs

@@ -348,11 +348,11 @@ impl ELFInstruction {
             None => false
         };
         flags[10] = matches!(self.opcode,
-            RV32IM::VIRTUAL_ASSERT_EQ     |
-            RV32IM::VIRTUAL_ASSERT_LTE    |
-            RV32IM::VIRTUAL_ASSERT_LTU    |
-            RV32IM::VIRTUAL_ASSERT_LT_ABS |
-            RV32IM::VIRTUAL_ASSERT_EQ_SIGNS,
+            RV32IM::VIRTUAL_ASSERT_EQ                        |
+            RV32IM::VIRTUAL_ASSERT_LTE                       |
+            RV32IM::VIRTUAL_ASSERT_VALID_SIGNED_REMAINDER    |
+            RV32IM::VIRTUAL_ASSERT_VALID_UNSIGNED_REMAINDER  |
+            RV32IM::VIRTUAL_ASSERT_VALID_DIV0,
         );
 
         flags
@@ -445,11 +445,11 @@ pub enum RV32IM {
     // Virtual instructions
     VIRTUAL_MOVSIGN,
     VIRTUAL_ADVICE,
-    VIRTUAL_ASSERT_LTU,
     VIRTUAL_ASSERT_LTE,
-    VIRTUAL_ASSERT_LT_ABS,
-    VIRTUAL_ASSERT_EQ_SIGNS,
+    VIRTUAL_ASSERT_VALID_UNSIGNED_REMAINDER,
+    VIRTUAL_ASSERT_VALID_SIGNED_REMAINDER,
     VIRTUAL_ASSERT_EQ,
+    VIRTUAL_ASSERT_VALID_DIV0,
 }
 
 impl FromStr for RV32IM {
@@ -577,9 +577,9 @@ impl RV32IM {
             RV32IM::BGEU |
             RV32IM::VIRTUAL_ASSERT_EQ     |
             RV32IM::VIRTUAL_ASSERT_LTE    |
-            RV32IM::VIRTUAL_ASSERT_LTU    |
-            RV32IM::VIRTUAL_ASSERT_LT_ABS |
-            RV32IM::VIRTUAL_ASSERT_EQ_SIGNS => RV32InstructionFormat::SB,
+            RV32IM::VIRTUAL_ASSERT_VALID_DIV0    |
+            RV32IM::VIRTUAL_ASSERT_VALID_SIGNED_REMAINDER    |
+            RV32IM::VIRTUAL_ASSERT_VALID_UNSIGNED_REMAINDER => RV32InstructionFormat::SB,
 
             RV32IM::LUI   |
             RV32IM::AUIPC |