diff --git a/jolt-core/src/field/binius.rs b/jolt-core/src/field/binius.rs index 5b7fb583d..759eba1e2 100644 --- a/jolt-core/src/field/binius.rs +++ b/jolt-core/src/field/binius.rs @@ -273,3 +273,9 @@ impl ark_serialize::Valid for BiniusField { todo!() } } + +impl std::fmt::Display for BiniusField { + fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + todo!() + } +} diff --git a/jolt-core/src/field/mod.rs b/jolt-core/src/field/mod.rs index 02ee610c9..aa76b5f27 100644 --- a/jolt-core/src/field/mod.rs +++ b/jolt-core/src/field/mod.rs @@ -1,4 +1,4 @@ -use std::fmt::Debug; +use std::fmt::{Debug, Display}; use std::ops::{Add, AddAssign, Div, Mul, MulAssign, Neg, Sub, SubAssign}; use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; @@ -31,6 +31,7 @@ pub trait JoltField: + Copy + Sync + Send + + Display + Debug + Default + CanonicalSerialize diff --git a/jolt-core/src/jolt/vm/bytecode.rs b/jolt-core/src/jolt/vm/bytecode.rs index 63835cb2c..18ea53b93 100644 --- a/jolt-core/src/jolt/vm/bytecode.rs +++ b/jolt-core/src/jolt/vm/bytecode.rs @@ -37,6 +37,7 @@ pub struct BytecodeStuff { a_init_final: VerifierComputedOpening, v_init_final: VerifierComputedOpening<[T; 6]>, } + pub type BytecodePolynomials = BytecodeStuff>; pub type BytecodeOpenings = BytecodeStuff; pub type BytecodeCommitments = BytecodeStuff; diff --git a/jolt-core/src/jolt/vm/instruction_lookups.rs b/jolt-core/src/jolt/vm/instruction_lookups.rs index 2b61318b7..35dde0682 100644 --- a/jolt-core/src/jolt/vm/instruction_lookups.rs +++ b/jolt-core/src/jolt/vm/instruction_lookups.rs @@ -34,7 +34,7 @@ use crate::{ use super::{JoltCommitments, JoltPolynomials, JoltTraceStep}; -#[derive(Default, CanonicalSerialize, CanonicalDeserialize)] +#[derive(Debug, Default, CanonicalSerialize, CanonicalDeserialize)] pub struct InstructionLookupStuff { pub(crate) dim: Vec, read_cts: Vec, @@ -604,19 +604,10 @@ where transcript, ); - // let sumcheck_opening_proof = PrimarySumcheckOpenings::prove_openings( - // generators, - // witness, - // &r_primary_sumcheck, - // &sumcheck_openings, - // transcript, - // ); - let primary_sumcheck = PrimarySumcheck { sumcheck_proof: primary_sumcheck_proof, num_rounds, openings: sumcheck_openings, - // opening_proof: sumcheck_opening_proof, }; let memory_checking = Self::prove_memory_checking( @@ -669,6 +660,9 @@ where "Primary sumcheck check failed." ); + // TODO(moodlezoup) + opening_accumulator.append(&vec![], r_primary_sumcheck.clone(), &vec![], transcript); + // proof.primary_sumcheck.openings.verify_openings( // generators, // &proof.primary_sumcheck.opening_proof, @@ -1072,6 +1066,7 @@ where preprocessing: &InstructionLookupsPreprocessing, instruction_flags: &[F], ) -> Vec { + debug_assert_eq!(instruction_flags.len(), Self::NUM_INSTRUCTIONS); let mut memory_flags = vec![F::zero(); preprocessing.num_memories]; for instruction_index in 0..Self::NUM_INSTRUCTIONS { for memory_index in &preprocessing.instruction_to_memory_indices[instruction_index] { diff --git a/jolt-core/src/jolt/vm/mod.rs b/jolt-core/src/jolt/vm/mod.rs index dedbb72a6..5a47db8b8 100644 --- a/jolt-core/src/jolt/vm/mod.rs +++ b/jolt-core/src/jolt/vm/mod.rs @@ -478,6 +478,7 @@ pub trait Jolt, const C: usize, c Self::Constraints::construct_constraints(padded_trace_length, memory_start); let spartan_key = spartan::UniformSpartanProof::setup_precommitted(&r1cs_builder, padded_trace_length); + transcript.append_scalar(&spartan_key.vk_digest); let r1cs_proof = R1CSProof { key: spartan_key, diff --git a/jolt-core/src/jolt/vm/read_write_memory.rs b/jolt-core/src/jolt/vm/read_write_memory.rs index 2325f6a9d..8c46e6fdf 100644 --- a/jolt-core/src/jolt/vm/read_write_memory.rs +++ b/jolt-core/src/jolt/vm/read_write_memory.rs @@ -1326,7 +1326,12 @@ where "Output sumcheck check failed." ); - opening_accumulator.append(&[&commitment.v_final], r_sumcheck, &[&proof.opening]); + opening_accumulator.append( + &[&commitment.v_final], + r_sumcheck, + &[&proof.opening], + transcript, + ); Ok(()) } @@ -1416,6 +1421,7 @@ where TimestampValidityProof::verify( &mut self.timestamp_validity_proof, generators, + opening_accumulator, // &commitment.timestamp_range_check, // &commitment.read_write_memory, transcript, diff --git a/jolt-core/src/jolt/vm/timestamp_range_check.rs b/jolt-core/src/jolt/vm/timestamp_range_check.rs index 61c2e0aab..3bbd60bfa 100644 --- a/jolt-core/src/jolt/vm/timestamp_range_check.rs +++ b/jolt-core/src/jolt/vm/timestamp_range_check.rs @@ -676,6 +676,7 @@ where pub fn verify( &mut self, generators: &PCS::Setup, + opening_accumulator: &mut VerifierOpeningAccumulator, // TODO(moodlezoup) // range_check_commitment: &RangeCheckCommitment, // memory_commitment: &MemoryCommitment, @@ -708,6 +709,9 @@ where Some(generators), ); + // TODO(moodleozoup) + opening_accumulator.append(&vec![], r_grand_product.clone(), &vec![], transcript); + // // TODO(moodlezoup): Make indexing less disgusting // let t_read_commitments = &memory_commitment.trace_commitments // [1 + MEMORY_OPS_PER_INSTRUCTION + 5..1 + 2 * MEMORY_OPS_PER_INSTRUCTION + 5]; diff --git a/jolt-core/src/lasso/memory_checking.rs b/jolt-core/src/lasso/memory_checking.rs index f5d4d807c..7eb4acfcb 100644 --- a/jolt-core/src/lasso/memory_checking.rs +++ b/jolt-core/src/lasso/memory_checking.rs @@ -235,7 +235,7 @@ where } fn compute_openings( - _preprocessing: &Self::Preprocessing, + preprocessing: &Self::Preprocessing, opening_accumulator: &mut ProverOpeningAccumulator, polynomials: &Self::Polynomials, jolt_polynomials: &JoltPolynomials, @@ -243,18 +243,18 @@ where r_init_final: &[F], transcript: &mut ProofTranscript, ) -> (Self::Openings, Self::ExogenousOpenings) { - let mut openings = Self::Openings::default(); + let mut openings = Self::Openings::initialize(preprocessing); let mut exogenous_openings = Self::ExogenousOpenings::default(); let eq_read_write = EqPolynomial::evals(r_read_write); polynomials .read_write_values() .par_iter() - .zip(openings.read_write_values_mut().into_par_iter()) + .zip_eq(openings.read_write_values_mut().into_par_iter()) .chain( Self::ExogenousOpenings::exogenous_data(jolt_polynomials) .par_iter() - .zip(exogenous_openings.openings_mut().into_par_iter()), + .zip_eq(exogenous_openings.openings_mut().into_par_iter()), ) .for_each(|(poly, opening)| { let claim = poly.evaluate_at_chi(&eq_read_write); @@ -280,7 +280,7 @@ where polynomials .init_final_values() .par_iter() - .zip(openings.init_final_values_mut().into_par_iter()) + .zip_eq(openings.init_final_values_mut().into_par_iter()) .for_each(|(poly, opening)| { let claim = poly.evaluate_at_chi(&eq_init_final); *opening = claim; @@ -426,7 +426,7 @@ where pcs_setup: &PCS::Setup, mut proof: MemoryCheckingProof, commitments: &Self::Commitments, - exogenous_commitments: &JoltCommitments, + jolt_commitments: &JoltCommitments, opening_accumulator: &mut VerifierOpeningAccumulator, transcript: &mut ProofTranscript, ) -> Result<(), ProofVerifyError> { @@ -457,7 +457,7 @@ where let read_write_commits: Vec<_> = [ commitments.read_write_values(), - exogenous_commitments.read_write_values(), + Self::ExogenousOpenings::exogenous_data(jolt_commitments), ] .concat(); let read_write_claims: Vec<_> = [ @@ -469,12 +469,14 @@ where &read_write_commits, r_read_write.to_vec(), &read_write_claims, + transcript, ); opening_accumulator.append( &commitments.init_final_values(), r_read_write.to_vec(), &proof.openings.init_final_values(), + transcript, ); // proof.read_write_openings.verify_openings( diff --git a/jolt-core/src/poly/opening_proof.rs b/jolt-core/src/poly/opening_proof.rs index ce8b1ad7a..45dfdea48 100644 --- a/jolt-core/src/poly/opening_proof.rs +++ b/jolt-core/src/poly/opening_proof.rs @@ -85,8 +85,11 @@ impl ProverOpeningAccumulator { claims: &[&F], transcript: &mut ProofTranscript, ) { + assert_eq!(polynomials.len(), claims.len()); // Generate batching challenge \rho and powers 1,...,\rho^{m-1} let rho: F = transcript.challenge_scalar(); + // let rho: F = F::one(); // TODO(moodlezoup) + let mut rho_powers = vec![F::one()]; for i in 1..polynomials.len() { rho_powers.push(rho_powers[i - 1] * rho); @@ -355,8 +358,11 @@ impl> VerifierOpeningAccumulator< commitments: &[&PCS::Commitment], opening_point: Vec, claims: &[&F], + transcript: &mut ProofTranscript, ) { - todo!("Compute RLC commitment/claim"); + assert_eq!(commitments.len(), claims.len()); + let _: F = transcript.challenge_scalar(); + // todo!("Compute RLC commitment/claim"); // self.openings // .push(VerifierOpening::new(commitment, opening_point, claim)); } diff --git a/jolt-core/src/r1cs/builder.rs b/jolt-core/src/r1cs/builder.rs index 3ee1d25c7..70af91c99 100644 --- a/jolt-core/src/r1cs/builder.rs +++ b/jolt-core/src/r1cs/builder.rs @@ -31,62 +31,48 @@ struct Constraint { } impl Constraint { - fn pretty_fmt(&self, f: &mut String) -> std::fmt::Result { + #[cfg(test)] + fn pretty_fmt( + &self, + f: &mut String, + flattened_polynomials: &[&DensePolynomial], + step_index: usize, + ) -> std::fmt::Result { self.a.pretty_fmt::(f)?; write!(f, " ⋅ ")?; self.b.pretty_fmt::(f)?; write!(f, " == ")?; - self.c.pretty_fmt::(f) - } + self.c.pretty_fmt::(f)?; + writeln!(f, "")?; - #[cfg(test)] - fn is_sat(&self, inputs: &[i64]) -> bool { - todo!("fix") - // // Find the number of variables and the number of aux. Inputs should be equal to this combined length - // let num_inputs = I::COUNT; - - // let mut aux_set = std::collections::HashSet::new(); - // for constraint in [&self.a, &self.b, &self.c] { - // for Term(var, _value) in constraint.terms() { - // if let Variable::Auxiliary(aux) = var { - // aux_set.insert(aux); - // } - // } - // } - // let num_aux = aux_set.len(); - // if !aux_set.is_empty() { - // assert_eq!(num_aux, *aux_set.iter().max().unwrap() + 1); // Ensure there are no gaps - // } - // let aux_index = |aux_index: usize| num_inputs + aux_index; - - // let num_vars = num_inputs + num_aux; - // assert_eq!(num_vars, inputs.len()); - - // let mut a = 0; - // let mut b = 0; - // let mut c = 0; - // let mut buckets = [&mut a, &mut b, &mut c]; - // let constraints = [&self.a, &self.b, &self.c]; - // for (bucket, constraint) in buckets.iter_mut().zip(constraints.iter()) { - // for Term(var, coefficient) in constraint.terms() { - // match var { - // Variable::Input(input) => { - // let in_u: usize = (*input).into(); - // **bucket += inputs[in_u] * *coefficient; - // } - // Variable::Auxiliary(aux) => { - // **bucket += inputs[aux_index(*aux)] * *coefficient; - // } - // Variable::Constant => { - // **bucket += *coefficient; - // } - // } - // } - // } - - // println!("a * b == c {a} * {b} == {c}"); - - // a * b == c + let mut terms = Vec::new(); + for term in self + .a + .terms() + .iter() + .chain(self.b.terms().iter()) + .chain(self.c.terms().iter()) + { + if !terms.contains(term) { + terms.push(*term); + } + } + + for term in terms { + match term.0 { + Variable::Input(var_index) | Variable::Auxiliary(var_index) => { + writeln!( + f, + " {:?} = {}", + I::from_index::(var_index), + flattened_polynomials[var_index][step_index] + )?; + } + Variable::Constant => {} + } + } + + Ok(()) } } @@ -257,18 +243,6 @@ impl R1CSBuilder { new_aux } - /// Index of variable within z. - #[cfg(test)] - pub fn witness_index(&self, var: impl Into) -> usize { - todo!("fix"); - // let var: Variable = var.into(); - // match var { - // Variable::Input(inner) => inner.into(), - // Variable::Auxiliary(aux_index) => I::COUNT + aux_index, - // Variable::Constant => I::COUNT + self.next_aux, - // } - } - pub fn constrain_eq(&mut self, left: impl Into, right: impl Into) { // left - right == 0 let left: LC = left.into(); @@ -465,14 +439,6 @@ impl R1CSBuilder { self.allocate_aux(aux_symbol, symbolic_inputs, compute) } - // fn variable_to_column(&self, var: Variable) -> usize { - // match var { - // Variable::Input(inner) => inner.into(), - // Variable::Auxiliary(aux) => I::COUNT + aux, - // Variable::Constant => (I::COUNT + self.num_aux()).next_power_of_two(), - // } - // } - fn materialize(&self) -> UniformR1CS { let a_len: usize = self.constraints.iter().map(|c| c.a.num_vars()).sum(); let b_len: usize = self.constraints.iter().map(|c| c.b.num_vars()).sum(); @@ -521,6 +487,7 @@ pub type OffsetLC = (bool, LC); /// A conditional constraint that Linear Combinations a, b are equal where a and b need not be in the same step an a /// uniform constraint system. +#[derive(Debug)] pub struct OffsetEqConstraint { cond: OffsetLC, a: OffsetLC, @@ -638,15 +605,17 @@ impl CombinedUniformBuilder condition - .offset_vars - .push((inner, constraint.cond.0, F::from_i64(term.1))), + Variable::Input(inner) | Variable::Auxiliary(inner) => { + eq.offset_vars + .push((inner, constraint.a.0, F::from_i64(term.1))) + } Variable::Constant => {} }); rhs.terms().iter().for_each(|term| match term.0 { - Variable::Input(inner) | Variable::Auxiliary(inner) => condition - .offset_vars - .push((inner, constraint.cond.0, F::from_i64(term.1))), + Variable::Input(inner) | Variable::Auxiliary(inner) => { + eq.offset_vars + .push((inner, constraint.b.0, F::from_i64(term.1))) + } Variable::Constant => {} }); @@ -779,7 +748,7 @@ impl CombinedUniformBuilder CombinedUniformBuilder], az: &SparsePolynomial, bz: &SparsePolynomial, cz: &SparsePolynomial, @@ -805,19 +775,20 @@ impl CombinedUniformBuilder= self.uniform_builder.constraints.len() { panic!( - "Mismatch at non-uniform constraint: {}\n\ - step: {step_index}", + "Non-uniform constraint {} violated at step {step_index}", uniform_constraint_index - self.uniform_builder.constraints.len() ) } else { let mut constraint_string = String::new(); let _ = self.uniform_builder.constraints[uniform_constraint_index] - .pretty_fmt::(&mut constraint_string); + .pretty_fmt::( + &mut constraint_string, + flattened_polynomials, + step_index, + ); + println!("{constraint_string}"); panic!( - "Mismatch at global constraint {constraint_index} => {:?}\n\ - uniform constraint: {uniform_constraint_index}\n\ - step: {step_index}", - constraint_string + "Uniform constraint {uniform_constraint_index} violated at step {step_index}", ); } } diff --git a/jolt-core/src/r1cs/constraints.rs b/jolt-core/src/r1cs/constraints.rs index 5216551f3..2da83e2a1 100644 --- a/jolt-core/src/r1cs/constraints.rs +++ b/jolt-core/src/r1cs/constraints.rs @@ -215,7 +215,7 @@ impl R1CSConstraints for JoltRV32IMConstrain JoltIn::Bytecode_RD, JoltIn::OpFlags(CircuitFlags::Jump), ); - let lhs = JoltIn::Bytecode_ELFAddress + (PC_START_ADDRESS - PC_NOOP_SHIFT); + let lhs = 4 * JoltIn::Bytecode_ELFAddress + PC_START_ADDRESS; // TODO(moodlezoup): is this right? let rhs = JoltIn::RD_Write; cs.constrain_eq_conditional(rd_nonzero_and_jmp, lhs, rhs); diff --git a/jolt-core/src/r1cs/inputs.rs b/jolt-core/src/r1cs/inputs.rs index 4cd780d30..ee018b4bb 100644 --- a/jolt-core/src/r1cs/inputs.rs +++ b/jolt-core/src/r1cs/inputs.rs @@ -344,7 +344,7 @@ impl ConstraintInput for JoltIn { JoltIn::RS1_Read => &jolt_polynomials.read_write_memory.v_read[0], JoltIn::RS2_Read => &jolt_polynomials.read_write_memory.v_read[1], JoltIn::RD_Read => &jolt_polynomials.read_write_memory.v_read[2], - JoltIn::RAM_Read(i) => &jolt_polynomials.read_write_memory.v_read[2 + i], + JoltIn::RAM_Read(i) => &jolt_polynomials.read_write_memory.v_read[3 + i], JoltIn::RD_Write => &jolt_polynomials.read_write_memory.v_write_rd, JoltIn::RAM_Write(i) => &jolt_polynomials.read_write_memory.v_write_ram[*i], JoltIn::ChunksQuery(i) => &jolt_polynomials.instruction_lookups.dim[*i], diff --git a/jolt-core/src/r1cs/key.rs b/jolt-core/src/r1cs/key.rs index 25cd235fb..4c777d3d9 100644 --- a/jolt-core/src/r1cs/key.rs +++ b/jolt-core/src/r1cs/key.rs @@ -74,7 +74,7 @@ pub struct UniformR1CS { /// NonUniformR1CSConstraint only supports a single additional equality constraint. 'a' holds the equality (something minus something), /// 'b' holds the condition. 'a' * 'b' == 0. Each SparseEqualityItem stores a uniform_column (pointing to a variable) and an offset /// suggesting which other step to point to. -#[derive(CanonicalSerialize, CanonicalDeserialize)] +#[derive(Debug, CanonicalSerialize, CanonicalDeserialize)] pub struct NonUniformR1CSConstraint { pub eq: SparseEqualityItem, pub condition: SparseEqualityItem, diff --git a/jolt-core/src/r1cs/ops.rs b/jolt-core/src/r1cs/ops.rs index 13b24dd3f..ea90d8910 100644 --- a/jolt-core/src/r1cs/ops.rs +++ b/jolt-core/src/r1cs/ops.rs @@ -20,7 +20,7 @@ pub enum Variable { Constant, } -#[derive(Clone, Copy, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct Term(pub Variable, pub i64); impl Term { fn pretty_fmt(&self, f: &mut String) -> std::fmt::Result { @@ -35,7 +35,7 @@ impl Term { } /// Linear Combination of terms. -#[derive(Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct LC(Vec); impl LC { diff --git a/jolt-core/src/r1cs/spartan.rs b/jolt-core/src/r1cs/spartan.rs index bf6330ff2..b932b5ac6 100644 --- a/jolt-core/src/r1cs/spartan.rs +++ b/jolt-core/src/r1cs/spartan.rs @@ -110,7 +110,7 @@ impl UniformSpartanProof(&flattened_polys); let comb_func_outer = |eq: &F, az: &F, bz: &F, cz: &F| -> F { - // Below is an optimized form of: *A * (*B * *C - *D) + // Below is an optimized form of: eq * (Az * Bz - Cz) if az.is_zero() || bz.is_zero() { if cz.is_zero() { F::zero() @@ -181,21 +181,13 @@ impl UniformSpartanProof = I::flatten::() - .iter() - .map(|witness| witness.get_poly_ref(polynomials)) - .collect(); - let claimed_witness_evals: Vec<_> = I::flatten::() + let claimed_witness_evals: Vec<_> = flattened_polys .par_iter() - .map(|witness| { - witness - .get_poly_ref(polynomials) - .evaluate_at_chi_low_optimized(&chi) - }) + .map(|poly| poly.evaluate_at_chi_low_optimized(&chi)) .collect(); opening_accumulator.append( - &witness_polys, + &flattened_polys, DensePolynomial::new(chi), r_col_step.to_vec(), &claimed_witness_evals.iter().collect::>(), diff --git a/jolt-core/src/subprotocols/sumcheck.rs b/jolt-core/src/subprotocols/sumcheck.rs index 79e2ecd1b..935e04b08 100644 --- a/jolt-core/src/subprotocols/sumcheck.rs +++ b/jolt-core/src/subprotocols/sumcheck.rs @@ -337,6 +337,8 @@ impl SumcheckInstanceProof { let len = poly_A.len() / 2; let trace_len = W[0].len(); + W.iter() + .for_each(|poly| debug_assert_eq!(poly.len(), trace_len)); let witness_value = |index: usize| { if (index / trace_len) >= W.len() { @@ -346,8 +348,6 @@ impl SumcheckInstanceProof { } }; - // assert_eq!(len, W.len()); - let poly = { // eval_point_0 = \sum_i A[i] * B[i] // where B[i] = W.r1cs_witness_value::(i) for i in 0..len @@ -423,7 +423,7 @@ impl SumcheckInstanceProof { /* Round 0 END */ - for i in 1..num_rounds { + for _i in 1..num_rounds { let poly = { let (eval_point_0, eval_point_2) = Self::compute_eval_points_spartan_quadratic(poly_A, &poly_B); @@ -450,10 +450,6 @@ impl SumcheckInstanceProof { || poly_A.bound_poly_var_top_zero_optimized(&r_i), || poly_B.bound_poly_var_top_zero_optimized(&r_i), ); - - if i == num_rounds - 1 { - assert_eq!(poly.evaluate(&r_i), poly_A[0] * poly_B[0]); - } } let evals = vec![poly_A[0], poly_B[0]];