From 55e3b6b9d707c28f2e0531f50d371258ee6358c0 Mon Sep 17 00:00:00 2001 From: 10to4 Date: Thu, 12 Dec 2024 16:52:44 +0800 Subject: [PATCH] skip structural witin commitment & PCS(#654): - cargo fmt check --- ceno_zkvm/src/circuit_builder.rs | 7 +- ceno_zkvm/src/expression.rs | 85 +++++++++++++++++---- ceno_zkvm/src/expression/monomial.rs | 4 +- ceno_zkvm/src/scheme/mock_prover.rs | 43 +++++++---- ceno_zkvm/src/scheme/prover.rs | 23 ++++-- ceno_zkvm/src/scheme/verifier.rs | 3 +- ceno_zkvm/src/structs.rs | 11 ++- ceno_zkvm/src/tables/ops/ops_circuit.rs | 2 +- ceno_zkvm/src/tables/program.rs | 2 +- ceno_zkvm/src/tables/ram/ram_circuit.rs | 5 +- ceno_zkvm/src/tables/ram/ram_impl.rs | 3 +- ceno_zkvm/src/tables/range/range_circuit.rs | 2 +- 12 files changed, 140 insertions(+), 50 deletions(-) diff --git a/ceno_zkvm/src/circuit_builder.rs b/ceno_zkvm/src/circuit_builder.rs index 6e89662aa..0d19a6215 100644 --- a/ceno_zkvm/src/circuit_builder.rs +++ b/ceno_zkvm/src/circuit_builder.rs @@ -9,7 +9,7 @@ use crate::{ ROMType, chip_handler::utils::rlc_chip_record, error::ZKVMError, - expression::{Expression, Fixed, Instance, WitIn, StructuralWitIn}, + expression::{Expression, Fixed, Instance, StructuralWitIn, WitIn}, structs::{ProgramParams, ProvingKey, RAMType, VerifyingKey, WitnessId}, witness::RowMajorMatrix, }; @@ -243,7 +243,10 @@ impl ConstraintSystem { wit_in } - pub fn create_structural_witin, N: FnOnce() -> NR>(&mut self, n: N) -> StructuralWitIn{ + pub fn create_structural_witin, N: FnOnce() -> NR>( + &mut self, + n: N, + ) -> StructuralWitIn { let wit_in = StructuralWitIn { id: { let id = self.num_structural_witin; diff --git a/ceno_zkvm/src/expression.rs b/ceno_zkvm/src/expression.rs index 611eb25d8..4f7830183 100644 --- a/ceno_zkvm/src/expression.rs +++ b/ceno_zkvm/src/expression.rs @@ -116,31 +116,87 @@ impl Expression { Expression::Constant(scalar) => constant(*scalar), Expression::Sum(a, b) => { let a = a.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); let b = b.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); sum(a, b) } Expression::Product(a, b) => { let a = a.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); let b = b.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); product(a, b) } Expression::ScaledSum(x, a, b) => { let x = x.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); let a = a.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); let b = b.evaluate_with_instance( - fixed_in, wit_in, structural_wit_in, instance, constant, challenge, sum, product, scaled, + fixed_in, + wit_in, + structural_wit_in, + instance, + constant, + challenge, + sum, + product, + scaled, ); scaled(x, a, b) } @@ -217,13 +273,14 @@ impl Neg for Expression { type Output = Expression; fn neg(self) -> Self::Output { match self { - Expression::Fixed(_) | Expression::WitIn(_) | Expression::StructuralWitIn(_) | Expression::Instance(_) => { - Expression::ScaledSum( - Box::new(self), - Box::new(Expression::Constant(E::BaseField::ONE.neg())), - Box::new(Expression::Constant(E::BaseField::ZERO)), - ) - } + Expression::Fixed(_) + | Expression::WitIn(_) + | Expression::StructuralWitIn(_) + | Expression::Instance(_) => Expression::ScaledSum( + Box::new(self), + Box::new(Expression::Constant(E::BaseField::ONE.neg())), + Box::new(Expression::Constant(E::BaseField::ZERO)), + ), Expression::Constant(c1) => Expression::Constant(c1.neg()), Expression::Sum(a, b) => { Expression::Sum(Box::new(-a.deref().clone()), Box::new(-b.deref().clone())) diff --git a/ceno_zkvm/src/expression/monomial.rs b/ceno_zkvm/src/expression/monomial.rs index e72a529a6..85ffedec0 100644 --- a/ceno_zkvm/src/expression/monomial.rs +++ b/ceno_zkvm/src/expression/monomial.rs @@ -146,6 +146,8 @@ mod tests { E::random(&mut rng), E::random(&mut rng), ]; - move |expr: &Expression| eval_by_expr_with_fixed(&fixed, &witnesses, &[], &challenges, expr) + move |expr: &Expression| { + eval_by_expr_with_fixed(&fixed, &witnesses, &[], &challenges, expr) + } } } diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index 019af7a3c..732edf095 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -315,7 +315,7 @@ fn load_tables(cb: &CircuitBuilder, challenge: [E; 2]) -> (b as usize).into(), (c as usize).into(), ]); - let rlc_record = eval_by_expr(&[], &[],&challenge, &rlc_record); + let rlc_record = eval_by_expr(&[], &[], &challenge, &rlc_record); t_vec.push(rlc_record.to_canonical_u64_vec()); } } @@ -657,7 +657,8 @@ impl<'a, E: ExtensionField + Hash> MockProver { .iter() .map(|v| unsafe { (*v).assume_init() }.into()) .collect::>(); - let rlc_record = eval_by_expr_with_fixed(&row, &[], &[], &challenge, &table_expr.values); + let rlc_record = + eval_by_expr_with_fixed(&row, &[], &[], &challenge, &table_expr.values); t_vec.push(rlc_record.to_canonical_u64_vec()); } } @@ -847,15 +848,21 @@ Hints: .iter() .zip(cs.lk_expressions_items_map.clone().into_iter()) { - let lk_table = - wit_infer_by_expr(&fixed, &witness, &[], &pi_mles, &challenges, &expr.values) - .get_ext_field_vec() - .to_vec(); + let lk_table = wit_infer_by_expr( + &fixed, + &witness, + &[], + &pi_mles, + &challenges, + &expr.values, + ) + .get_ext_field_vec() + .to_vec(); let multiplicity = wit_infer_by_expr( &fixed, &witness, - &[], + &[], &pi_mles, &challenges, &expr.multiplicity, @@ -920,7 +927,7 @@ Hints: eval_by_expr_with_instance( &[], &witness, - &[], + &[], &instance, challenges.as_slice(), expr, @@ -979,10 +986,16 @@ Hints: .zip_eq(cs.w_ram_types.iter()) .filter(|((_, _), (ram_type, _))| *ram_type == $ram_type) { - let write_rlc_records = - (wit_infer_by_expr(fixed, witness, &[], &pi_mles, &challenges, w_rlc_expr) - .get_ext_field_vec())[..*num_rows] - .to_vec(); + let write_rlc_records = (wit_infer_by_expr( + fixed, + witness, + &[], + &pi_mles, + &challenges, + w_rlc_expr, + ) + .get_ext_field_vec())[..*num_rows] + .to_vec(); if $ram_type == RAMType::GlobalState { // w_exprs = [GlobalState, pc, timestamp] @@ -994,7 +1007,7 @@ Hints: let v = wit_infer_by_expr( fixed, witness, - &[], + &[], &pi_mles, &challenges, expr, @@ -1154,7 +1167,7 @@ Hints: gs_rs.insert(eval_by_expr_with_instance( &[], &[], - &[], + &[], &instance, &challenges, &gs_final, @@ -1162,7 +1175,7 @@ Hints: gs_ws.insert(eval_by_expr_with_instance( &[], &[], - &[], + &[], &instance, &challenges, &gs_init, diff --git a/ceno_zkvm/src/scheme/prover.rs b/ceno_zkvm/src/scheme/prover.rs index f1742fc0d..00f52d643 100644 --- a/ceno_zkvm/src/scheme/prover.rs +++ b/ceno_zkvm/src/scheme/prover.rs @@ -95,7 +95,7 @@ impl> ZKVMProver { let commit_dur = std::time::Instant::now(); let num_instances = structural_witness.num_instances(); let structural_witness = structural_witness.into_mles(); - + tracing::info!( "commit to {} traces took {:?}", circuit_name, @@ -134,7 +134,6 @@ impl> ZKVMProver { } exit_span!(commit_to_traces_span); - // squeeze two challenges from transcript let challenges = [ transcript.read_challenge().elements, @@ -157,11 +156,11 @@ impl> ZKVMProver { continue; } let wits_commit = commitments.remove(circuit_name).unwrap(); - let (structural_witness, structural_num_instances) = + let (structural_witness, structural_num_instances) = if structural_wits.contains_key(circuit_name) { structural_wits - .remove(circuit_name) - .ok_or(ZKVMError::WitnessNotFound(circuit_name.clone()))? + .remove(circuit_name) + .ok_or(ZKVMError::WitnessNotFound(circuit_name.clone()))? } else { (vec![], 0) }; @@ -206,7 +205,10 @@ impl> ZKVMProver { pk, witness.into_iter().map(|v| v.into()).collect_vec(), wits_commit, - structural_witness.into_iter().map(|v| v.into()).collect_vec(), + structural_witness + .into_iter() + .map(|v| v.into()) + .collect_vec(), &pi, transcript, &challenges, @@ -746,7 +748,14 @@ impl> ZKVMProver { .chain(cs.lk_table_expressions.par_iter().map(|lk| &lk.values)) .map(|expr| { assert_eq!(expr.degree(), 1); - wit_infer_by_expr(&fixed, &witnesses, &structural_witnesses, pi, challenges, expr) + wit_infer_by_expr( + &fixed, + &witnesses, + &structural_witnesses, + pi, + challenges, + expr, + ) }) .collect(); let max_log2_num_instance = records_wit.iter().map(|mle| mle.num_vars()).max().unwrap(); diff --git a/ceno_zkvm/src/scheme/verifier.rs b/ceno_zkvm/src/scheme/verifier.rs index cab5923a1..15b66dbeb 100644 --- a/ceno_zkvm/src/scheme/verifier.rs +++ b/ceno_zkvm/src/scheme/verifier.rs @@ -475,7 +475,8 @@ impl> ZKVMVerifier // verify zero expression (degree = 1) statement, thus no sumcheck if cs.assert_zero_expressions.iter().any(|expr| { - eval_by_expr_with_instance(&[], &proof.wits_in_evals, &[], pi, challenges, expr) != E::ZERO + eval_by_expr_with_instance(&[], &proof.wits_in_evals, &[], pi, challenges, expr) + != E::ZERO }) { return Err(ZKVMError::VerifyError("zero expression != 0".into())); } diff --git a/ceno_zkvm/src/structs.rs b/ceno_zkvm/src/structs.rs index 390d4e1b8..335021eb0 100644 --- a/ceno_zkvm/src/structs.rs +++ b/ceno_zkvm/src/structs.rs @@ -255,7 +255,10 @@ impl ZKVMWitnesses { self.witnesses_tables.get(name).cloned() } - pub fn get_table_structural_witness(&self, name: &String) -> Option> { + pub fn get_table_structural_witness( + &self, + name: &String, + ) -> Option> { self.structural_witnesses_tables.get(name).cloned() } @@ -330,7 +333,11 @@ impl ZKVMWitnesses { self.combined_lk_mlt.as_ref().unwrap(), input, )?; - assert!(self.structural_witnesses_tables.insert(TC::name(), structural_witness).is_none()); + assert!( + self.structural_witnesses_tables + .insert(TC::name(), structural_witness) + .is_none() + ); assert!(!self.witnesses_opcodes.contains_key(&TC::name())); diff --git a/ceno_zkvm/src/tables/ops/ops_circuit.rs b/ceno_zkvm/src/tables/ops/ops_circuit.rs index bc94300c7..921c3f0ee 100644 --- a/ceno_zkvm/src/tables/ops/ops_circuit.rs +++ b/ceno_zkvm/src/tables/ops/ops_circuit.rs @@ -73,7 +73,7 @@ impl TableCircuit for OpsTableCircuit _num_witin: usize, _multiplicity: &[HashMap], _final_v: &Self::WitnessInput, - ) -> Result, ZKVMError>{ + ) -> Result, ZKVMError> { Ok(RowMajorMatrix::new(0, 0)) } } diff --git a/ceno_zkvm/src/tables/program.rs b/ceno_zkvm/src/tables/program.rs index 8a3345fea..7da98fbba 100644 --- a/ceno_zkvm/src/tables/program.rs +++ b/ceno_zkvm/src/tables/program.rs @@ -228,7 +228,7 @@ impl TableCircuit for ProgramTableCircuit { _num_witin: usize, _multiplicity: &[HashMap], _final_v: &Self::WitnessInput, - ) -> Result, ZKVMError>{ + ) -> Result, ZKVMError> { Ok(RowMajorMatrix::new(0, 0)) } } diff --git a/ceno_zkvm/src/tables/ram/ram_circuit.rs b/ceno_zkvm/src/tables/ram/ram_circuit.rs index 2f7bf41d3..b1115cd87 100644 --- a/ceno_zkvm/src/tables/ram/ram_circuit.rs +++ b/ceno_zkvm/src/tables/ram/ram_circuit.rs @@ -104,7 +104,7 @@ impl TableCirc num_witin: usize, _multiplicity: &[HashMap], final_v: &Self::WitnessInput, - ) -> Result, ZKVMError>{ + ) -> Result, ZKVMError> { config.assign_structural_instances(num_witin, final_v) } } @@ -160,7 +160,7 @@ impl TableCirc num_witin: usize, _multiplicity: &[HashMap], final_cycles: &[Cycle], - ) -> Result, ZKVMError>{ + ) -> Result, ZKVMError> { config.assign_structural_instances(num_witin, final_cycles) } } @@ -241,7 +241,6 @@ impl TableC _multiplicity: &[HashMap], final_v: &Self::WitnessInput, ) -> Result, ZKVMError> { - config.assign_structural_instances(num_witin, final_v) } } diff --git a/ceno_zkvm/src/tables/ram/ram_impl.rs b/ceno_zkvm/src/tables/ram/ram_impl.rs index e37eb27fb..e0551b960 100644 --- a/ceno_zkvm/src/tables/ram/ram_impl.rs +++ b/ceno_zkvm/src/tables/ram/ram_impl.rs @@ -9,7 +9,7 @@ use rayon::iter::{IndexedParallelIterator, IntoParallelIterator, ParallelIterato use crate::{ circuit_builder::{CircuitBuilder, DynamicAddr, SetTableAddrType, SetTableSpec}, error::ZKVMError, - expression::{Expression, Fixed, ToExpr, WitIn, StructuralWitIn}, + expression::{Expression, Fixed, StructuralWitIn, ToExpr, WitIn}, instructions::riscv::constants::{LIMB_BITS, LIMB_MASK}, scheme::constants::MIN_PAR_SIZE, set_fixed_val, set_val, @@ -452,7 +452,6 @@ impl DynVolatileRamTableConfig .with_min_len(MIN_PAR_SIZE) .for_each(|(i, row)| { set_val!(row, self.addr, DVRAM::addr(&self.params, i) as u64); - }); Ok(final_table) diff --git a/ceno_zkvm/src/tables/range/range_circuit.rs b/ceno_zkvm/src/tables/range/range_circuit.rs index c4cbf1609..90a645d83 100644 --- a/ceno_zkvm/src/tables/range/range_circuit.rs +++ b/ceno_zkvm/src/tables/range/range_circuit.rs @@ -66,7 +66,7 @@ impl TableCircuit for RangeTableCircuit _num_witin: usize, _multiplicity: &[HashMap], _input: &(), - ) -> Result, ZKVMError>{ + ) -> Result, ZKVMError> { Ok(RowMajorMatrix::new(0, 0)) } }