diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index fa232e630..dbb0c5ffb 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -240,7 +240,7 @@ pub fn verify_tower_proof( builder.dyn_array(proof.prod_specs_eval.data.length.clone()); let logup_specs_eval: Array> = builder.dyn_array(proof.logup_specs_eval.data.length.clone()); - builder.set(&input_ctx, 9, Usize::from(0)); + builder.set(&input_ctx, 9, Usize::from(1)); // writeback: copy hint data into local arrays builder.range(0, op_range).for_each(|i_vec, builder| { let round_var = i_vec[0]; @@ -289,6 +289,43 @@ pub fn verify_tower_proof( builder.assert_ext_eq(expected_evaluation, sub_e); builder.cycle_tracker_end("check expected evaluation"); + // Bind prover-supplied prod/logup evals into transcript (Fiat-Shamir soundness). + // After sumcheck_layer_eval with writeback=1, the local arrays contain the hint data. + let prod_stride: Var = builder.eval( + proof.prod_specs_eval.inner_length * proof.prod_specs_eval.inner_inner_length, + ); + builder + .range(0, num_prod_spec.get_var()) + .for_each(|idx, builder| { + let offset: Var = builder.eval( + idx[0] * prod_stride + round_var * proof.prod_specs_eval.inner_inner_length, + ); + let end: Var = + builder.eval(offset + proof.prod_specs_eval.inner_inner_length); + let slice = prod_specs_eval.slice(builder, offset, end); + unsafe { + let felts = exts_to_felts(builder, &slice); + challenger_multi_observe(builder, challenger, &felts); + } + }); + let logup_stride: Var = builder.eval( + proof.logup_specs_eval.inner_length * proof.logup_specs_eval.inner_inner_length, + ); + builder + .range(0, num_logup_spec.get_var()) + .for_each(|idx, builder| { + let offset: Var = builder.eval( + idx[0] * logup_stride + round_var * proof.logup_specs_eval.inner_inner_length, + ); + let end: Var = + builder.eval(offset + proof.logup_specs_eval.inner_inner_length); + let slice = logup_specs_eval.slice(builder, offset, end); + unsafe { + let felts = exts_to_felts(builder, &slice); + challenger_multi_observe(builder, challenger, &felts); + } + }); + builder.cycle_tracker_start("derive next layer's expected sum"); // derive single eval // rt' = r_merge || rt diff --git a/ceno_recursion/src/zkvm_verifier/verifier.rs b/ceno_recursion/src/zkvm_verifier/verifier.rs index a745c916d..0b36d0486 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -6,6 +6,7 @@ use crate::{ arithmetics::{ PolyEvaluator, UniPolyExtrapolator, arr_product, assert_ext_arr_eq, build_eq_x_r_vec_sequential, challenger_hint_observe, challenger_multi_observe, concat, + exts_to_felts, dot_product as ext_dot_product, eq_eval, eq_eval_less_or_equal_than, eval_ceno_expr_with_instance, eval_wellform_address_vec, gen_alpha_pows, mask_arr, reverse, }, @@ -961,6 +962,12 @@ pub fn verify_gkr_circuit( unipoly_extrapolator, ); + // Bind prover-supplied evaluations into transcript (Fiat-Shamir soundness). + unsafe { + let main_evals_felts = exts_to_felts(builder, &main_evals); + challenger_multi_observe(builder, challenger, &main_evals_felts); + } + let structural_witin_offset = layer.n_witin + layer.n_fixed + layer.n_instance; // check selector evaluations @@ -1197,6 +1204,12 @@ pub fn verify_rotation( unipoly_extrapolator, ); + // Bind prover-supplied rotation evaluations into transcript (Fiat-Shamir soundness). + unsafe { + let evals_felts = exts_to_felts(builder, evals); + challenger_multi_observe(builder, challenger, &evals_felts); + } + // compute the selector evaluation let selector_eval = rotation_selector_eval( builder, diff --git a/ceno_zkvm/src/scheme/cpu/mod.rs b/ceno_zkvm/src/scheme/cpu/mod.rs index 929c7850d..0aa96aecc 100644 --- a/ceno_zkvm/src/scheme/cpu/mod.rs +++ b/ceno_zkvm/src/scheme/cpu/mod.rs @@ -482,44 +482,56 @@ impl CpuTowerProver { proofs.push_sumcheck_proofs(sumcheck_proofs.proofs); - // rt' = r_merge || rt - let r_merge = transcript.sample_and_append_vec(b"merge", log_num_fanin); - let rt_prime = [state.collect_raw_challenges(), r_merge].concat(); - - // generate next round challenge - let next_alpha_pows = get_challenge_pows( - prod_specs_len + logup_specs_len * 2, /* logup occupy 2 sumcheck: numerator and denominator */ - transcript, - ); let evals = state.get_mle_flatten_final_evaluations(); + // Bind prod/logup evals into transcript before sampling r_merge (Fiat-Shamir soundness). // retrieve final evaluation to proof + let mut prod_evals_per_spec = Vec::with_capacity(prod_specs_len); for (i, witness_prod_expr) in witness_prod_expr.iter().enumerate().take(prod_specs_len) { - let evals = witness_prod_expr + let spec_evals = witness_prod_expr .iter() .map(|expr| match expr { Expression::WitIn(wit_id) => evals[*wit_id as usize], _ => unreachable!(), }) .collect_vec(); - if !evals.is_empty() { - assert_eq!(evals.len(), num_fanin); - proofs.push_prod_evals_and_point(i, evals, rt_prime.clone()); + if !spec_evals.is_empty() { + assert_eq!(spec_evals.len(), num_fanin); + transcript.append_field_element_exts(&spec_evals); + prod_evals_per_spec.push((i, spec_evals)); } } + let mut logup_evals_per_spec = Vec::with_capacity(logup_specs_len); for (i, witness_lk_expr) in witness_lk_expr.iter().enumerate().take(logup_specs_len) { - let evals = witness_lk_expr + let spec_evals = witness_lk_expr .iter() .map(|expr| match expr { Expression::WitIn(wit_id) => evals[*wit_id as usize], _ => unreachable!(), }) .collect_vec(); - if !evals.is_empty() { - assert_eq!(evals.len(), 4); // p1, p2, q1, q2 - proofs.push_logup_evals_and_point(i, evals, rt_prime.clone()); + if !spec_evals.is_empty() { + assert_eq!(spec_evals.len(), 4); // p1, p2, q1, q2 + transcript.append_field_element_exts(&spec_evals); + logup_evals_per_spec.push((i, spec_evals)); } } + + // rt' = r_merge || rt + let r_merge = transcript.sample_and_append_vec(b"merge", log_num_fanin); + let rt_prime = [state.collect_raw_challenges(), r_merge].concat(); + + // generate next round challenge + let next_alpha_pows = get_challenge_pows( + prod_specs_len + logup_specs_len * 2, /* logup occupy 2 sumcheck: numerator and denominator */ + transcript, + ); + for (i, spec_evals) in prod_evals_per_spec { + proofs.push_prod_evals_and_point(i, spec_evals, rt_prime.clone()); + } + for (i, spec_evals) in logup_evals_per_spec { + proofs.push_logup_evals_and_point(i, spec_evals, rt_prime.clone()); + } out_rt = rt_prime; alpha_pows = next_alpha_pows; } diff --git a/ceno_zkvm/src/scheme/verifier.rs b/ceno_zkvm/src/scheme/verifier.rs index 9d595d0a5..d5a26163b 100644 --- a/ceno_zkvm/src/scheme/verifier.rs +++ b/ceno_zkvm/src/scheme/verifier.rs @@ -787,6 +787,18 @@ impl TowerVerify { let rt: Point = sumcheck_claim.point.iter().map(|c| c.elements).collect(); let eq = eq_eval(out_rt, &rt); + // Bind prover-supplied prod/logup evals into transcript (Fiat-Shamir soundness). + for (spec_index, num_vars) in num_variables.iter().enumerate().take(num_prod_spec) { + if round < *num_vars - 1 { + transcript.append_field_element_exts(&tower_proofs.prod_specs_eval[spec_index][round]); + } + } + for (spec_index, num_vars) in num_variables.iter().skip(num_prod_spec).enumerate().take(num_logup_spec) { + if round < *num_vars - 1 { + transcript.append_field_element_exts(&tower_proofs.logup_specs_eval[spec_index][round]); + } + } + let expected_evaluation: E = (0..num_prod_spec) .zip(alpha_pows.iter()) .zip(num_variables.iter()) diff --git a/gkr_iop/src/gkr/layer/cpu/mod.rs b/gkr_iop/src/gkr/layer/cpu/mod.rs index 00e472bf0..578bf79d1 100644 --- a/gkr_iop/src/gkr/layer/cpu/mod.rs +++ b/gkr_iop/src/gkr/layer/cpu/mod.rs @@ -92,11 +92,10 @@ impl> SumcheckLayerProver< builder.to_virtual_polys(&[layer.exprs[0].clone()], challenges), transcript, ); + let evals = prover_state.get_mle_flatten_final_evaluations(); + transcript.append_field_element_exts(&evals); LayerProof { - main: SumcheckLayerProof { - proof, - evals: prover_state.get_mle_flatten_final_evaluations(), - }, + main: SumcheckLayerProof { proof, evals }, rotation: None, } } @@ -262,6 +261,7 @@ impl> ZerocheckLayerProver ); let evals = prover_state.get_mle_flatten_final_evaluations(); + transcript.append_field_element_exts(&evals); exit_span!(span); ( LayerProof { @@ -409,6 +409,7 @@ pub(crate) fn prove_rotation>(); exit_span!(span); + transcript.append_field_element_exts(&evals); ( SumcheckLayerProof { proof: rotation_proof, diff --git a/gkr_iop/src/gkr/layer/gpu/mod.rs b/gkr_iop/src/gkr/layer/gpu/mod.rs index 3ec80e99b..262726239 100644 --- a/gkr_iop/src/gkr/layer/gpu/mod.rs +++ b/gkr_iop/src/gkr/layer/gpu/mod.rs @@ -300,6 +300,7 @@ impl> ZerocheckLayerProver let row_challenges_e = unsafe { std::mem::transmute::, Vec>(row_challenges) }; + transcript.append_field_element_exts(&evals_gpu_e); exit_span!(span); ( LayerProof { @@ -467,6 +468,7 @@ pub(crate) fn prove_rotation_gpu>(); exit_span!(span); + transcript.append_field_element_exts(&evals); ( SumcheckLayerProof { diff --git a/gkr_iop/src/gkr/layer/sumcheck_layer.rs b/gkr_iop/src/gkr/layer/sumcheck_layer.rs index fb739935f..5fbf081f1 100644 --- a/gkr_iop/src/gkr/layer/sumcheck_layer.rs +++ b/gkr_iop/src/gkr/layer/sumcheck_layer.rs @@ -106,6 +106,9 @@ impl SumcheckLayer for Layer { transcript, ); + // Bind the prover-supplied evaluations into the transcript (Fiat-Shamir soundness). + transcript.append_field_element_exts(&evals); + // Check the final evaluations. let got_claim = eval_by_expr_with_instance(&[], &evals, &[], &[], challenges, &self.exprs[0]) diff --git a/gkr_iop/src/gkr/layer/zerocheck_layer.rs b/gkr_iop/src/gkr/layer/zerocheck_layer.rs index cb0b91fa1..0ae2986f0 100644 --- a/gkr_iop/src/gkr/layer/zerocheck_layer.rs +++ b/gkr_iop/src/gkr/layer/zerocheck_layer.rs @@ -320,6 +320,9 @@ impl ZerocheckLayer for Layer { ); let in_point = in_point.into_iter().map(|c| c.elements).collect_vec(); + // Bind the prover-supplied evaluations into the transcript (Fiat-Shamir soundness). + transcript.append_field_element_exts(&main_evals); + let structural_witin_offset = self.n_witin + self.n_fixed + self.n_instance; // eval selector and set to respective witin izip!( @@ -742,6 +745,9 @@ fn verify_rotation( ); let origin_point = in_point.into_iter().map(|c| c.elements).collect_vec(); + // Bind the prover-supplied rotation evaluations into the transcript (Fiat-Shamir soundness). + transcript.append_field_element_exts(&evals); + // compute the selector evaluation let bh = BooleanHypercube::new(rotation_cyclic_group_log2); let selector_eval = rotation_selector_eval(