diff --git a/jolt-core/src/zkvm/claim_reductions/instruction_lookups.rs b/jolt-core/src/zkvm/claim_reductions/instruction_lookups.rs index cd5696dbbf..a2d6f3393e 100644 --- a/jolt-core/src/zkvm/claim_reductions/instruction_lookups.rs +++ b/jolt-core/src/zkvm/claim_reductions/instruction_lookups.rs @@ -1,3 +1,75 @@ +//! # InstructionClaimReduction (Stage 2) +//! +//! Source: `jolt-core/src/zkvm/claim_reductions/instruction_lookups.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! +//! +//! ## Batching randomness +//! +//! - `γ ∈ F`: fresh batching challenge (powers γ, γ², γ³, γ⁴ used) +//! +//! +//! ## Sumcheck +//! +//! `eq(r^(1)_cycle, X_j)` is the [multilinear Lagrange basis polynomial][ml]. +//! +//! [ml]: https://en.wikipedia.org/wiki/Multilinear_polynomial +//! +//! ```text +//! LHS := Σ_{X_j} eq(r^(1)_cycle, X_j) +//! · (LookupOutput(X_j) +//! + γ · LeftLookupOperand(X_j) +//! + γ² · RightLookupOperand(X_j) +//! + γ³ · LeftInstructionInput(X_j) +//! + γ⁴ · RightInstructionInput(X_j)) +//! +//! RHS := LookupOutput(r^(1)_cycle) +//! + γ · LeftLookupOperand(r^(1)_cycle) +//! + γ² · RightLookupOperand(r^(1)_cycle) +//! + γ³ · LeftInstructionInput(r^(1)_cycle) +//! + γ⁴ · RightInstructionInput(r^(1)_cycle) +//! +//! where X_j ∈ {0,1}^{log₂ T} +//! ``` +//! +//! Dimensions: `log₂ T` rounds (cycle only). +//! +//! The RHS is known: all five polynomials were opened at +//! `r^(1)_cycle` in Stage 1. +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(2)_cycle ∈ F^{log₂ T}`. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r^(1)_cycle, r^(2)_cycle) +//! · (LookupOutput(r^(2)_cycle) +//! + γ · LeftLookupOperand(r^(2)_cycle) +//! + γ² · RightLookupOperand(r^(2)_cycle) +//! + γ³ · LeftInstructionInput(r^(2)_cycle) +//! + γ⁴ · RightInstructionInput(r^(2)_cycle)) +//! ``` +//! +//! The `eq` term is computable by the verifier. The prover supplies +//! openings for all five VPs below. +//! +//! +//! ## VirtualPolynomials opened at `r^(2)_cycle` +//! +//! ```text +//! LookupOutput, LeftLookupOperand, RightLookupOperand, +//! LeftInstructionInput, RightInstructionInput +//! ``` use std::array; use std::sync::Arc; diff --git a/jolt-core/src/zkvm/claim_reductions/registers.rs b/jolt-core/src/zkvm/claim_reductions/registers.rs index 3a66f5c205..2bb7cb823d 100644 --- a/jolt-core/src/zkvm/claim_reductions/registers.rs +++ b/jolt-core/src/zkvm/claim_reductions/registers.rs @@ -1,3 +1,67 @@ +//! # RegistersClaimReduction (Stage 3) +//! +//! Source: `jolt-core/src/zkvm/claim_reductions/registers.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! +//! +//! ## Batching randomness +//! +//! - `γ ∈ F`: fresh batching challenge (powers γ, γ² used) +//! +//! +//! ## Sumcheck +//! +//! ```text +//! LHS := Σ_{X_j} eq(r^(1)_cycle, X_j) +//! · (RdWriteValue(X_j) +//! + γ · Rs1Value(X_j) +//! + γ² · Rs2Value(X_j)) +//! +//! RHS := RdWriteValue(r^(1)_cycle) +//! + γ · Rs1Value(r^(1)_cycle) +//! + γ² · Rs2Value(r^(1)_cycle) +//! +//! where X_j ∈ {0,1}^{log₂ T} +//! ``` +//! +//! Dimensions: `log₂ T` rounds (cycle only). +//! +//! The RHS is known: `RdWriteValue`, `Rs1Value`, and `Rs2Value` +//! were opened at `r^(1)_cycle` in Stage 1 (SpartanOuter). +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(3)_cycle ∈ F^{log₂ T}` (shared with Shift +//! and InstructionInput via Stage 3 batching). +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r^(1)_cycle, r^(3)_cycle) +//! · (RdWriteValue(r^(3)_cycle) +//! + γ · Rs1Value(r^(3)_cycle) +//! + γ² · Rs2Value(r^(3)_cycle)) +//! ``` +//! +//! `eq` is computable by the verifier. +//! The prover supplies openings for the 3 VPs below. +//! +//! +//! ## VirtualPolynomials opened at `r^(3)_cycle` +//! +//! ```text +//! RdWriteValue, +//! Rs1Value, +//! Rs2Value +//! ``` use std::array; use std::sync::Arc; diff --git a/jolt-core/src/zkvm/ram/output_check.rs b/jolt-core/src/zkvm/ram/output_check.rs index 35bed7ad7b..d6d15e2da8 100644 --- a/jolt-core/src/zkvm/ram/output_check.rs +++ b/jolt-core/src/zkvm/ram/output_check.rs @@ -1,3 +1,62 @@ +//! # OutputCheck (Stage 2) +//! +//! Source: `jolt-core/src/zkvm/ram/output_check.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - `r_address ∈ F^{log₂ K_RAM}`: fresh address challenge vector +//! +//! +//! ## Sumcheck +//! +//! `eq(r_address, X_k)` is the [multilinear Lagrange basis polynomial][ml]. +//! +//! [ml]: https://en.wikipedia.org/wiki/Multilinear_polynomial +//! +//! ```text +//! LHS := Σ_{X_k} eq(r_address, X_k) · io_mask(X_k) +//! · (RamValFinal(X_k) - ValIO(X_k)) +//! +//! RHS := 0 (zero-check) +//! +//! where X_k ∈ {0,1}^{log₂ K_RAM} +//! ``` +//! +//! Dimensions: `log₂ K_RAM` rounds (address only). +//! +//! - `io_mask(X_k)`: 1 if address `X_k` is in the I/O region, +//! 0 otherwise. Verifier-computable. +//! - `ValIO(X_k)`: publicly claimed output value at address `X_k`. +//! Verifier-computable (public input). +//! - `RamValFinal(X_k)`: final RAM state at address `X_k` after +//! all cycles (virtual). +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(2)_{K_RAM} ∈ F^{log₂ K_RAM}`. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r_address, r^(2)_{K_RAM}) · io_mask(r^(2)_{K_RAM}) +//! · (RamValFinal(r^(2)_{K_RAM}) - ValIO(r^(2)_{K_RAM})) +//! ``` +//! +//! `eq`, `io_mask`, and `ValIO` are computable by the verifier. +//! The prover supplies the opening for `RamValFinal`. +//! +//! +//! ## VirtualPolynomials opened at `r^(2)_{K_RAM}` +//! +//! ```text +//! RamValFinal +//! ``` +//! #[cfg(feature = "zk")] use crate::poly::opening_proof::OpeningId; #[cfg(feature = "zk")] @@ -32,17 +91,6 @@ use common::{constants::RAM_START_ADDRESS, jolt_device::MemoryLayout}; use rayon::prelude::*; use tracer::JoltDevice; -// RAM output sumchecks -// -// OutputSumcheck: -// Proves the zero-check -// Σ_k eq(r_address, k) ⋅ io_mask(k) ⋅ (Val_final(k) − Val_io(k)) = 0, -// where: -// - r_address is a random address challenge vector. -// - io_mask is the MLE of the I/O-region indicator (1 on matching {0,1}-points). -// - Val_final(k) is the final memory value at address k. -// - Val_io(k) is the publicly claimed output value at address k. - /// Degree bonud of the sumcheck round polynomials in [`OutputSumcheckVerifier`]. const OUTPUT_SUMCHECK_DEGREE_BOUND: usize = 3; diff --git a/jolt-core/src/zkvm/ram/raf_evaluation.rs b/jolt-core/src/zkvm/ram/raf_evaluation.rs index 033019fa38..1dcb8e9b63 100644 --- a/jolt-core/src/zkvm/ram/raf_evaluation.rs +++ b/jolt-core/src/zkvm/ram/raf_evaluation.rs @@ -1,3 +1,64 @@ +//! # RafEvaluation (Stage 2) +//! +//! Source: `jolt-core/src/zkvm/ram/raf_evaluation.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! +//! +//! ## Sumcheck +//! +//! `unmap(X_k)` is the MLE of the identity function over `{0,1}^{log₂ K_RAM}`: +//! it maps a boolean hypercube point to the integer it encodes. +//! Definition: `jolt-core/src/poly/identity_poly.rs` (`UnmapRamAddressPolynomial`). +//! +//! ```text +//! unmap(X_k) = Σ_{i=0}^{log₂ K_RAM - 1} 2^i · X_{k,i} +//! ``` +//! +//! The prover pre-computes +//! `ra(X_k) := Σ_j eq(r^(1)_cycle, j) · 1[address(j) = k]`, +//! aggregating access counts per remapped address `k`. +//! +//! ```text +//! LHS := Σ_{X_k} ra(X_k) · unmap(X_k) +//! +//! RHS := RamAddress(r^(1)_cycle) +//! +//! where X_k ∈ {0,1}^{log₂ K_RAM} +//! ``` +//! +//! Dimensions: `log₂ K_RAM` rounds (address only). +//! +//! - `ra(X_k)`: `RamRa` partially evaluated at `r^(1)_cycle` (virtual). +//! - `unmap(X_k)`: identity polynomial. Verifier-computable. +//! - `RamAddress(r^(1)_cycle)`: opened in Stage 1 (SpartanOuter). +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(2)_{K_RAM} ∈ F^{log₂ K_RAM}`. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! unmap(r^(2)_{K_RAM}) · RamRa(r^(2)_{K_RAM}, r^(1)_cycle) +//! ``` +//! +//! `unmap` is computable by the verifier. +//! The prover supplies the opening for `RamRa`. +//! +//! +//! ## VirtualPolynomials opened at `(r^(2)_{K_RAM}, r^(1)_cycle)` +//! +//! ```text +//! RamRa +//! ``` use common::jolt_device::MemoryLayout; use num_traits::Zero; diff --git a/jolt-core/src/zkvm/ram/read_write_checking.rs b/jolt-core/src/zkvm/ram/read_write_checking.rs index 9399f3df27..5765601aba 100644 --- a/jolt-core/src/zkvm/ram/read_write_checking.rs +++ b/jolt-core/src/zkvm/ram/read_write_checking.rs @@ -1,3 +1,73 @@ +//! # RamReadWriteChecking (Stage 2) +//! +//! Source: `jolt-core/src/zkvm/ram/read_write_checking.rs` +//! +//! +//! - `γ ∈ F`: Batching randomness +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! +//! +//! ## Sumcheck +//! +//! `eq(r^(1)_cycle, X_j)` is the [multilinear Lagrange basis polynomial][ml]. +//! +//! [ml]: https://en.wikipedia.org/wiki/Multilinear_polynomial +//! +//! ```text +//! LHS := Σ_{X_k, X_j} eq(r^(1)_cycle, X_j) · RamRa(X_k, X_j) +//! · (RamVal(X_k, X_j) +//! + γ · (RamVal(X_k, X_j) + RamInc(X_j))) +//! +//! RHS := RamReadValue(r^(1)_cycle) + γ · RamWriteValue(r^(1)_cycle) +//! +//! where X_k ∈ {0,1}^{log₂ K_RAM}, X_j ∈ {0,1}^{log₂ T} +//! ``` +//! +//! Dimensions: `log₂ K_RAM + log₂ T` rounds (address + cycle). +//! +//! The RHS is known: `RamReadValue` and `RamWriteValue` were opened +//! at `r^(1)_cycle` in Stage 1. +//! +//! - `RamRa(X_k, X_j)`: 1 if address `X_k` is accessed at cycle `X_j` (virtual) +//! - `RamVal(X_k, X_j)`: value at address `X_k` right before cycle `X_j` (virtual) +//! - `RamInc(X_j)`: write increment at cycle `X_j` (COMMITTED) +//! +//! +//! ## Opening point +//! +//! After sumcheck: `(r^(2)_{K_RAM}, r^(2)_cycle) ∈ F^{log₂ K_RAM + log₂ T}`. +//! Both components are used downstream. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r^(1)_cycle, r^(2)_cycle) · RamRa(r^(2)_{K_RAM}, r^(2)_cycle) +//! · (RamVal(r^(2)_{K_RAM}, r^(2)_cycle) +//! + γ · (RamVal(r^(2)_{K_RAM}, r^(2)_cycle) + RamInc(r^(2)_cycle))) +//! ``` +//! +//! The `eq` term is computable by the verifier. The prover supplies +//! openings for `RamRa`, `RamVal`, and `RamInc`. +//! +//! +//! ## Polynomials opened +//! +//! Virtual: +//! ```text +//! RamVal at (r^(2)_{K_RAM}, r^(2)_cycle) +//! RamRa at (r^(2)_{K_RAM}, r^(2)_cycle) +//! ``` +//! +//! Committed: +//! ```text +//! RamInc at r^(2)_cycle +//! ``` use common::jolt_device::MemoryLayout; use num::Integer; use num_traits::Zero; @@ -45,21 +115,6 @@ use allocative::FlameGraphBuilder; use rayon::prelude::*; use tracer::instruction::Cycle; -// RAM read-write checking sumcheck -// -// Proves the relation: -// Σ_{k,j} eq(r_cycle, j) ⋅ ra(k, j) ⋅ (Val(k, j) + γ ⋅ (inc(j) + Val(k, j))) -// = rv_claim + γ ⋅ wv_claim -// where: -// - r_cycle are the challenges for the cycle variables in this sumcheck (from Spartan outer) -// - ra(k, j) = 1 if memory address k is accessed at cycle j, and 0 otherwise -// - Val(k, j) is the value at memory address k right before cycle j -// - inc(j) is the change in value at cycle j if a write occurs, and 0 otherwise -// - rv_claim and wv_claim are the claimed read and write values from the Spartan outer sumcheck. -// -// This sumcheck ensures that the values read from and written to RAM are consistent -// with the memory trace and the initial/final memory states. - /// Degree bound of the sumcheck round polynomials in [`RamReadWriteCheckingVerifier`]. const DEGREE_BOUND: usize = 3; diff --git a/jolt-core/src/zkvm/spartan/instruction_input.rs b/jolt-core/src/zkvm/spartan/instruction_input.rs index ccababf7ee..b3cd5f8b88 100644 --- a/jolt-core/src/zkvm/spartan/instruction_input.rs +++ b/jolt-core/src/zkvm/spartan/instruction_input.rs @@ -1,3 +1,101 @@ +//! # InstructionInputVirtualization +//! +//! Source: `jolt-core/src/zkvm/spartan/instruction_input.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(2)_cycle ∈ F^{log₂ T}` from Stage 2 (ProductVirtualization) +//! +//! Both `ProductVirtualization` and `InstructionClaimReduction` +//! open `LeftInstructionInput` and `RightInstructionInput` at +//! the same point. The code asserts consistency: +//! +//! ```text +//! assert_eq!(r_left_claim_instruction, r_left_claim_stage_2); +//! assert_eq!(left_claim_instruction, left_claim_stage_2); +//! assert_eq!(r_right_claim_instruction, r_right_claim_stage_2); +//! assert_eq!(right_claim_instruction, right_claim_stage_2); +//! ``` +//! +//! +//! ## Batching randomness +//! +//! - `γ ∈ F`: fresh batching challenge (power γ used) +//! +//! +//! ## Sumcheck +//! +//! Decomposes `LeftInstructionInput` and `RightInstructionInput` into +//! flag-selected components: +//! +//! ```text +//! LeftInstructionInput(j) = IsRs1(j) · Rs1Value(j) +//! + IsPC(j) · UnexpandedPC(j) +//! +//! RightInstructionInput(j) = IsRs2(j) · Rs2Value(j) +//! + IsImm(j) · Imm(j) +//! ``` +//! +//! ```text +//! LHS := Σ_{X_j} eq(r^(2)_cycle, X_j) +//! · (IsRs2(X_j) · Rs2Value(X_j) +//! + IsImm(X_j) · Imm(X_j) +//! + γ · (IsRs1(X_j) · Rs1Value(X_j) +//! + IsPC(X_j) · UnexpandedPC(X_j))) +//! +//! RHS := RightInstructionInput(r^(2)_cycle) +//! + γ · LeftInstructionInput(r^(2)_cycle) +//! +//! where X_j ∈ {0,1}^{log₂ T} +//! ``` +//! +//! Dimensions: `log₂ T` rounds (cycle only). +//! +//! The RHS is known: `LeftInstructionInput` and `RightInstructionInput` +//! were opened at `r^(2)_cycle` in Stage 2 (ProductVirtualization). +//! +//! **Shorthand mapping:** +//! - `IsRs1` = `InstructionFlags(LeftOperandIsRs1Value)` +//! - `IsPC` = `InstructionFlags(LeftOperandIsPC)` +//! - `IsRs2` = `InstructionFlags(RightOperandIsRs2Value)` +//! - `IsImm` = `InstructionFlags(RightOperandIsImm)` +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(3)_cycle ∈ F^{log₂ T}` (shared with Shift +//! and RegistersClaimReduction via Stage 3 batching). +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r^(2)_cycle, r^(3)_cycle) +//! · (IsRs2(r^(3)_cycle) · Rs2Value(r^(3)_cycle) +//! + IsImm(r^(3)_cycle) · Imm(r^(3)_cycle) +//! + γ · (IsRs1(r^(3)_cycle) · Rs1Value(r^(3)_cycle) +//! + IsPC(r^(3)_cycle) · UnexpandedPC(r^(3)_cycle))) +//! ``` +//! +//! `eq` is computable by the verifier. +//! The prover supplies openings for the 8 VPs below. +//! +//! +//! ## VirtualPolynomials opened at `r^(3)_cycle` +//! +//! ```text +//! InstructionFlags(LeftOperandIsRs1Value), +//! Rs1Value, +//! InstructionFlags(LeftOperandIsPC), +//! UnexpandedPC, +//! InstructionFlags(RightOperandIsRs2Value), +//! Rs2Value, +//! InstructionFlags(RightOperandIsImm), +//! Imm +//! ``` use ark_ff::Zero; use allocative::Allocative; diff --git a/jolt-core/src/zkvm/spartan/outer.rs b/jolt-core/src/zkvm/spartan/outer.rs index 8c774279ea..131965ad67 100644 --- a/jolt-core/src/zkvm/spartan/outer.rs +++ b/jolt-core/src/zkvm/spartan/outer.rs @@ -1,3 +1,141 @@ +//! # SpartanOuter (Stage 1) +//! +//! Source: `jolt-core/src/zkvm/spartan/outer.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - `τ_t ∈ F^{log₂ T}` — random timestep challenge +//! - `τ_b ∈ F` — random group challenge +//! - `τ_c ∈ F` — random constraint index challenge +//! +//! +//! ## Sumcheck +//! +//! `eq((τ_t, τ_b), (X_t, X_b))` is the [multilinear Lagrange basis polynomial][ml]. +//! `L_{τ_c}(X_c)` is the [univariate Lagrange interpolation polynomial][ul] +//! over the domain `{-5, -4, …, 4}`. +//! +//! [ml]: https://en.wikipedia.org/wiki/Multilinear_polynomial +//! [ul]: https://en.wikipedia.org/wiki/Lagrange_polynomial +//! +//! ```text +//! LHS := Σ_{X_t, X_b, X_c} eq((τ_t, τ_b), (X_t, X_b)) +//! · L_{τ_c}(X_c) +//! · A[X_t, X_b, X_c] +//! · B[X_t, X_b, X_c] +//! +//! RHS := 0 +//! +//! where X_t ∈ {0,1}^{log₂ T}, X_b ∈ {0,1}, X_c ∈ {-5, …, 4} +//! ``` +//! +//! `A[X_t, X_b, X_c]` and `B[X_t, X_b, X_c]` are the R1CS constraint matrices. +//! `X_b ∈ {0,1}` selects the constraint group. +//! `X_c ∈ {-5, …, 4}` selects the constraint within the group. +//! For each `(b, c)`, `A[·, b, c]` and `B[·, b, c]` are specific +//! `VirtualPolynomial` expressions evaluated at `X_t`. +//! +//! +//! ### First group (`X_b = 0`): boolean A, ~64-bit B +//! +//! Grouping sourced from `R1CS_CONSTRAINTS_FIRST_GROUP_LABELS` in +//! `jolt-core/src/zkvm/r1cs/constraints.rs`. +//! A/B definitions sourced from `AzFirstGroup` / `BzFirstGroup` in +//! `jolt-core/src/zkvm/r1cs/evaluation.rs`. +//! +//! ```text +//! c | A (guard) | B (equality to enforce) +//! ---+----------------------------------------------------+-------------------------------------- +//! -5 | 1 - OpFlags(Load) - OpFlags(Store) | RamAddress +//! -4 | OpFlags(Load) | RamReadValue - RamWriteValue +//! -3 | OpFlags(Load) | RamReadValue - RdWriteValue +//! -2 | OpFlags(Store) | Rs2Value - RamWriteValue +//! -1 | OpFlags(Add) + OpFlags(Sub) + OpFlags(Mul) | LeftLookupOperand +//! 0 | 1 - OpFlags(Add) - OpFlags(Sub) - OpFlags(Mul) | LeftLookupOperand - LeftInstructionInput +//! 1 | OpFlags(Assert) | LookupOutput - 1 +//! 2 | ShouldJump | NextUnexpandedPC - LookupOutput +//! 3 | OpFlags(VirtualInstruction) - OpFlags(LastInSeq) | NextPC - PC - 1 +//! 4 | NextIsVirtual - NextIsFirstInSequence | 1 - OpFlags(DoNotUpdateUnexpandedPC) +//! ``` +//! +//! +//! ### Second group (`X_b = 1`): wider B (~128 bits), 9 constraints + 1 zero-padded +//! +//! Grouping sourced from `R1CS_CONSTRAINTS_SECOND_GROUP_LABELS` in +//! `jolt-core/src/zkvm/r1cs/constraints.rs`. +//! A/B definitions sourced from `AzSecondGroup` / `BzSecondGroup` in +//! `jolt-core/src/zkvm/r1cs/evaluation.rs`. +//! +//! ```text +//! c | A (guard) | B (equality to enforce) +//! ---+----------------------------------------------------+-------------------------------------- +//! -5 | OpFlags(Load) + OpFlags(Store) | RamAddress - Rs1Value - Imm +//! -4 | OpFlags(Add) | RightLookupOp - LeftInput - RightInput +//! -3 | OpFlags(Sub) | RightLookupOp - LeftInput + RightInput - 2^64 +//! -2 | OpFlags(Mul) | RightLookupOp - Product +//! -1 | 1 - OpFlags(Add) - OpFlags(Sub) | RightLookupOp - RightInput +//! | - OpFlags(Mul) - OpFlags(Advice) | +//! 0 | WriteLookupOutputToRD | RdWriteValue - LookupOutput +//! 1 | WritePCtoRD | RdWriteValue - UnexpandedPC - 4 +//! | | + 2·OpFlags(IsCompressed) +//! 2 | ShouldBranch | NextUnexpandedPC - UnexpandedPC - Imm +//! 3 | 1 - ShouldBranch - OpFlags(Jump) | NextUnexpandedPC - UnexpandedPC - 4 +//! | | + 4·OpFlags(DoNotUpdateUnexpandedPC) +//! | | + 2·OpFlags(IsCompressed) +//! 4 | 0 | 0 (zero-padded) +//! ``` +//! +//! **Note:** `OpFlags(Add)` is shorthand for `OpFlags(CircuitFlags::AddOperands)`, +//! `OpFlags(Sub)` for `SubtractOperands`, `OpFlags(Mul)` for `MultiplyOperands`, +//! `OpFlags(LastInSeq)` for `IsLastInSequence`. +//! `RightLookupOp` = `RightLookupOperand`, `LeftInput` = `LeftInstructionInput`, +//! `RightInput` = `RightInstructionInput`. +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(1)_cycle ∈ F^{log₂ T}`, `r^(1)_b ∈ F`, `r^(1)_c ∈ F`. +//! Only `r^(1)_cycle` is used downstream; `r^(1)_b` and `r^(1)_c` are absorbed. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq((τ_t, τ_b), (r^(1)_cycle, r^(1)_b)) +//! · L_{τ_c}(r^(1)_c) +//! · A(r^(1)_cycle, r^(1)_b, r^(1)_c) +//! · B(r^(1)_cycle, r^(1)_b, r^(1)_c) +//! ``` +//! +//! The `eq` and `L` terms are computable by the verifier. +//! The `A` and `B` terms are not committed — the prover supplies them +//! as openings of the constituent `VirtualPolynomial`s at `r^(1)_cycle`. +//! +//! +//! ## VirtualPolynomials opened at `r^(1)_cycle` +//! +//! All 37 `JoltR1CSInputs` from `ALL_R1CS_INPUTS` in +//! `jolt-core/src/zkvm/r1cs/inputs.rs`, each mapping 1:1 to a `VirtualPolynomial`: +//! +//! ```text +//! LeftInstructionInput, RightInstructionInput, Product, +//! WriteLookupOutputToRD, WritePCtoRD, ShouldBranch, +//! PC, UnexpandedPC, Imm, +//! RamAddress, Rs1Value, Rs2Value, RdWriteValue, +//! RamReadValue, RamWriteValue, +//! LeftLookupOperand, RightLookupOperand, +//! NextUnexpandedPC, NextPC, NextIsVirtual, NextIsFirstInSequence, +//! LookupOutput, ShouldJump, +//! OpFlags(AddOperands), OpFlags(SubtractOperands), OpFlags(MultiplyOperands), +//! OpFlags(Load), OpFlags(Store), OpFlags(Jump), +//! OpFlags(WriteLookupOutputToRD), OpFlags(VirtualInstruction), +//! OpFlags(Assert), OpFlags(DoNotUpdateUnexpandedPC), +//! OpFlags(Advice), OpFlags(IsCompressed), +//! OpFlags(IsFirstInSequence), OpFlags(IsLastInSequence) +//! ``` use std::marker::PhantomData; use std::sync::Arc; @@ -62,34 +200,6 @@ const OUTER_REMAINING_DEGREE_BOUND: usize = 3; // For example : MultiQuadratic has d=2; for cubic this would be 3 etc. const INFINITY: usize = 2; -// Spartan Outer sumcheck -// (with univariate-skip first round on Z, and no Cz term given all eq conditional constraints) -// -// We define a univariate in Z first-round polynomial -// s1(Y) := L(τ_high, Y) · Σ_{x_out ∈ {0,1}^{m_out}} Σ_{x_in ∈ {0,1}^{m_in}} -// E_out(r_out, x_out) · E_in(r_in, x_in) · -// [ Az(x_out, x_in, Y) · Bz(x_out, x_in, Y) ], -// where L(τ_high, Y) is the Lagrange basis polynomial over the univariate-skip -// base domain evaluated at τ_high, and Az(·,·,Y), Bz(·,·,Y) are the -// per-row univariate polynomials in Y induced by the R1CS row (split into two -// internal groups in code, but algebraically composing to Az·Bz at Y). -// The prover sends s1(Y) via univariate-skip by evaluating t1(Y) := Σ Σ E_out·E_in·(Az·Bz) -// on an extended grid Y ∈ {−D..D} outside the base window, interpolating t1, -// multiplying by L(τ_high, Y) to obtain s1, and the verifier samples r0. -// -// Subsequent outer rounds bind the cycle variables r_tail = (r1, r2, …) using -// a streaming first cycle-bit round followed by linear-time rounds: -// • Streaming round (after r0): compute -// t(0) = Σ_{x_out} E_out · Σ_{x_in} E_in · (Az(0)·Bz(0)) -// t(∞) = Σ_{x_out} E_out · Σ_{x_in} E_in · ((Az(1)−Az(0))·(Bz(1)−Bz(0))) -// send a cubic built from these endpoints, and bind cached coefficients by r1. -// • Remaining rounds: reuse bound coefficients to compute the same endpoints -// in linear time for each subsequent bit and bind by r_i. -// -// Final check (verifier): with r = [r0 || r_tail] and outer binding order from -// the top, evaluate Eq_τ(τ, r) and verify -// L(τ_high, r_high) · Eq_τ(τ, r) · (Az(r) · Bz(r)). - #[derive(Allocative, Clone)] pub struct OuterUniSkipParams { pub tau: Vec, diff --git a/jolt-core/src/zkvm/spartan/product.rs b/jolt-core/src/zkvm/spartan/product.rs index c3099b01d2..8de02095f1 100644 --- a/jolt-core/src/zkvm/spartan/product.rs +++ b/jolt-core/src/zkvm/spartan/product.rs @@ -1,3 +1,87 @@ +//! # ProductVirtualization (Stage 2) +//! +//! Source: `jolt-core/src/zkvm/spartan/product.rs` +//! Inputs: `jolt-core/src/zkvm/r1cs/inputs.rs` (`ProductCycleInputs`, `PRODUCT_UNIQUE_FACTOR_VIRTUALS`) +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - `τ_c ∈ F`: fresh constraint-index challenge +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! +//! +//! ## Sumcheck +//! +//! `eq(r^(1)_cycle, X_t)` is the [multilinear Lagrange basis polynomial][ml]. +//! `L_{τ_c}(X_c)` is the [univariate Lagrange interpolation polynomial][ul] +//! over the domain `{-2, -1, 0, 1, 2}`. +//! +//! [ml]: https://en.wikipedia.org/wiki/Multilinear_polynomial +//! [ul]: https://en.wikipedia.org/wiki/Lagrange_polynomial +//! +//! ```text +//! LHS := Σ_{X_t, X_c} eq(r^(1)_cycle, X_t) · L_{τ_c}(X_c) +//! · Left(X_t, X_c) · Right(X_t, X_c) +//! +//! RHS := Σ_{X_c} L_{τ_c}(X_c) · Output(r^(1)_cycle, X_c) +//! +//! where X_t ∈ {0,1}^{log₂ T}, X_c ∈ {-2, …, 2} +//! ``` +//! +//! Dimensions: `log₂ T + 1` rounds (cycle + univariate-skip constraint index). +//! +//! `Left(X_t, X_c)` and `Right(X_t, X_c)` are fused compositions — each +//! constraint index `c` selects a different pair of `VirtualPolynomial` factors: +//! +//! ```text +//! c | Output | Left factor | Right factor +//! ---+---------------------------+----------------------------------+---------------------------------- +//! -2 | Product | LeftInstructionInput | RightInstructionInput +//! -1 | WriteLookupOutputToRD | InstructionFlags(IsRdNotZero) | OpFlags(WriteLookupOutputToRD) +//! 0 | WritePCtoRD | InstructionFlags(IsRdNotZero) | OpFlags(Jump) +//! 1 | ShouldBranch | LookupOutput | InstructionFlags(Branch) +//! 2 | ShouldJump | OpFlags(Jump) | 1 - NextIsNoop +//! ``` +//! +//! Each row enforces `Left(t, c) · Right(t, c) = Output(t, c)`. +//! The RHS is known: the `Output` values are the Stage 1 openings of +//! `Product`, `WriteLookupOutputToRD`, `WritePCtoRD`, `ShouldBranch`, +//! `ShouldJump` at `r^(1)_cycle`, already in the openings table. +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(2)_cycle ∈ F^{log₂ T}`, `r^(2)_c ∈ F`. +//! Only `r^(2)_cycle` is used downstream; `r^(2)_c` is absorbed. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! eq(r^(1)_cycle, r^(2)_cycle) · L_{τ_c}(r^(2)_c) +//! · Left(r^(2)_cycle, r^(2)_c) · Right(r^(2)_cycle, r^(2)_c) +//! ``` +//! +//! The `eq` and `L` terms are computable by the verifier. +//! The `Left` and `Right` terms are fused Lagrange-weighted +//! combinations of the 9 factor polynomials below — the prover +//! supplies their openings at `r^(2)_cycle`. +//! +//! +//! ## VirtualPolynomials opened at `r^(2)_cycle` +//! +//! 9 unique factors from `PRODUCT_UNIQUE_FACTOR_VIRTUALS` in +//! `jolt-core/src/zkvm/r1cs/inputs.rs`: +//! +//! ```text +//! LeftInstructionInput, RightInstructionInput, +//! InstructionFlags(IsRdNotZero), +//! OpFlags(WriteLookupOutputToRD), OpFlags(Jump), +//! LookupOutput, InstructionFlags(Branch), +//! NextIsNoop, OpFlags(VirtualInstruction) +//! ``` use std::iter::zip; use std::sync::Arc; diff --git a/jolt-core/src/zkvm/spartan/shift.rs b/jolt-core/src/zkvm/spartan/shift.rs index 05afb03b24..522c676295 100644 --- a/jolt-core/src/zkvm/spartan/shift.rs +++ b/jolt-core/src/zkvm/spartan/shift.rs @@ -1,3 +1,91 @@ +//! # ShiftSumcheck +//! +//! Source: `jolt-core/src/zkvm/spartan/shift.rs` +//! +//! +//! ## Schwartz–Zippel randomness +//! +//! - Re-uses `r^(1)_cycle ∈ F^{log₂ T}` from Stage 1 (SpartanOuter) +//! - Re-uses `r^(2)_cycle ∈ F^{log₂ T}` from Stage 2 (ProductVirtualization) +//! +//! +//! ## Batching randomness +//! +//! - `γ ∈ F`: fresh batching challenge (powers γ, γ², γ³, γ⁴ used) +//! +//! +//! ## Sumcheck +//! +//! `EqPlusOne(X, Y)` for `X, Y ∈ {0,1}^ℓ` is the MLE of the Boolean +//! function that returns 1 iff the integer `Y = X + 1`, and 0 when +//! `X = 2^ℓ - 1` (no wrap-around). In other words, it "shifts" by +//! one timestep: `f(j+1)` is accessed via `EqPlusOne` at index `j`. +//! Definition: `jolt-core/src/poly/eq_plus_one_poly.rs`. +//! +//! ```text +//! LHS := Σ_{X_j} EqPlusOne(r^(1)_cycle, X_j) +//! · (UnexpandedPC(X_j) +//! + γ · PC(X_j) +//! + γ² · IsVirtual(X_j) +//! + γ³ · IsFirstInSeq(X_j)) +//! +//! + γ⁴ · Σ_{X_j} EqPlusOne(r^(2)_cycle, X_j) +//! · (1 - IsNoop(X_j)) +//! +//! RHS := NextUnexpandedPC(r^(1)_cycle) +//! + γ · NextPC(r^(1)_cycle) +//! + γ² · NextIsVirtual(r^(1)_cycle) +//! + γ³ · NextIsFirstInSeq(r^(1)_cycle) +//! + γ⁴ · (1 - NextIsNoop(r^(2)_cycle)) +//! +//! where X_j ∈ {0,1}^{log₂ T} +//! ``` +//! +//! Dimensions: `log₂ T` rounds (cycle only). +//! +//! The RHS is known: the first four `Next*` values were opened at +//! `r^(1)_cycle` in Stage 1, and `NextIsNoop` was opened at +//! `r^(2)_cycle` in Stage 2 (ProductVirtualization). +//! +//! **Shorthand mapping:** +//! - `IsVirtual` = `OpFlags(CircuitFlags::VirtualInstruction)` +//! - `IsFirstInSeq` = `OpFlags(CircuitFlags::IsFirstInSequence)` +//! - `IsNoop` = `InstructionFlags(InstructionFlags::IsNoop)` +//! +//! +//! ## Opening point +//! +//! After sumcheck: `r^(3)_cycle ∈ F^{log₂ T}`. +//! +//! +//! ## Verifier opening claim +//! +//! The verifier checks that the final sumcheck message equals: +//! +//! ```text +//! EqPlusOne(r^(1)_cycle, r^(3)_cycle) +//! · (UnexpandedPC(r^(3)_cycle) +//! + γ · PC(r^(3)_cycle) +//! + γ² · IsVirtual(r^(3)_cycle) +//! + γ³ · IsFirstInSeq(r^(3)_cycle)) +//! +//! + γ⁴ · EqPlusOne(r^(2)_cycle, r^(3)_cycle) +//! · (1 - IsNoop(r^(3)_cycle)) +//! ``` +//! +//! Both `EqPlusOne` terms are computable by the verifier. +//! The prover supplies openings for the 5 VPs below. +//! +//! +//! ## VirtualPolynomials opened at `r^(3)_cycle` +//! +//! ```text +//! UnexpandedPC, +//! PC, +//! OpFlags(VirtualInstruction), +//! OpFlags(IsFirstInSequence), +//! InstructionFlags(IsNoop) +//! ``` use std::array; use std::sync::Arc; @@ -36,21 +124,6 @@ use crate::zkvm::r1cs::inputs::ShiftSumcheckCycleState; use crate::zkvm::witness::VirtualPolynomial; use rayon::prelude::*; -// Spartan PC sumcheck -// -// Proves the batched identity over cycles j: -// Σ_j EqPlusOne(r_outer, j) ⋅ (UnexpandedPC_shift(j) + γ·PC_shift(j) + γ²·IsNoop_shift(j)) -// = NextUnexpandedPC(r_outer) + γ·NextPC(r_outer) + γ²·NextIsNoop(r_outer), -// -// where: -// - EqPlusOne(r_outer, j): MLE of the function that, -// on (i,j) returns 1 iff i = j + 1; no wrap-around at j = 2^{log T} − 1 -// - UnexpandedPC_shift(j), PC_shift(j), IsNoop_shift(j): -// SpartanShift MLEs encoding f(j+1) aligned at cycle j -// - NextUnexpandedPC(r_outer), NextPC(r_outer), NextIsNoop(r_outer) -// are claims from Spartan outer sumcheck -// - γ: batching scalar drawn from the transcript - /// Degree bound of the sumcheck round polynomials in [`ShiftSumcheckVerifier`]. const DEGREE_BOUND: usize = 2;