refactor(ecc): soundness fix of wiring ecc evaluations to gkr-circuit

ceno_recursion/src/zkvm_verifier/verifier.rs

@@ -579,15 +579,7 @@ pub fn verify_chip_proof<C: Config>(
         is_infinity: Usize::uninit(builder),
     };
 
-    if composed_cs.has_ecc_ops() {
-        builder.assert_nonzero(&chip_proof.has_ecc_proof);
-        let ecc_proof = &chip_proof.ecc_proof;
-        builder.assert_usize_eq(ecc_proof.sum.is_infinity.clone(), Usize::from(0));
-        verify_ecc_proof(builder, challenger, ecc_proof, unipoly_extrapolator);
-        builder.assign(&shard_ec_sum, ecc_proof.sum.clone());
-    } else {
-        builder.assign(&shard_ec_sum.is_infinity, Usize::from(1));
-    }
+    builder.assign(&shard_ec_sum.is_infinity, Usize::from(1));
 
     let tower_proof = &chip_proof.tower_proof;
     let num_variables: Array<C, Usize<C::N>> = builder.dyn_array(num_batched);
@@ -631,6 +623,14 @@ pub fn verify_chip_proof<C: Config>(
             });
     }
 
+    if composed_cs.has_ecc_ops() {
+        builder.assert_nonzero(&chip_proof.has_ecc_proof);
+        let ecc_proof = &chip_proof.ecc_proof;
+        builder.assert_usize_eq(ecc_proof.sum.is_infinity.clone(), Usize::from(0));
+        verify_ecc_proof(builder, challenger, ecc_proof, unipoly_extrapolator);
+        builder.assign(&shard_ec_sum, ecc_proof.sum.clone());
+    }
+
     let num_rw_records: Usize<C::N> = builder.eval(r_counts_per_instance + w_counts_per_instance);
     builder.assert_usize_eq(record_evals.len(), num_rw_records.clone());
     builder.assert_usize_eq(logup_p_evals.len(), lk_counts_per_instance.clone());
@@ -849,6 +849,101 @@ pub fn verify_chip_proof<C: Config>(
         }
     }
 
+    if composed_cs.has_ecc_ops() {
+        let [x_group_idx, y_group_idx, slope_group_idx] = first_layer
+            .ecc_bridge_group_indices()
+            .expect("ecc bridge selectors missing");
+
+        transcript_observe_label(builder, challenger, b"ecc_gkr_bridge_r");
+        let sample_r: Ext<C::F, C::EF> = challenger.sample_ext(builder);
+        let one_minus_r: Ext<C::F, C::EF> = builder.eval(one - sample_r);
+        let ecc_proof = &chip_proof.ecc_proof;
+
+        let xy_point_len: Usize<C::N> = builder.eval(ecc_proof.rt.fs.len() + Usize::from(1));
+        let xy_point: Array<C, Ext<C::F, C::EF>> = builder.dyn_array(xy_point_len);
+        builder.set(&xy_point, 0, sample_r);
+        builder
+            .range(0, ecc_proof.rt.fs.len())
+            .for_each(|idx_vec, builder| {
+                let idx = idx_vec[0];
+                let v = builder.get(&ecc_proof.rt.fs, idx);
+                let shifted_idx = Usize::Var(Var::uninit(builder));
+                builder.assign(&shifted_idx, idx + Usize::from(1));
+                builder.set(&xy_point, shifted_idx, v);
+            });
+
+        let s_point_len: Usize<C::N> = builder.eval(ecc_proof.rt.fs.len() + Usize::from(1));
+        let s_point: Array<C, Ext<C::F, C::EF>> = builder.dyn_array(s_point_len);
+        builder
+            .range(0, ecc_proof.rt.fs.len())
+            .for_each(|idx_vec, builder| {
+                let idx = idx_vec[0];
+                let v = builder.get(&ecc_proof.rt.fs, idx);
+                builder.set(&s_point, idx, v);
+            });
+        builder.set(&s_point, ecc_proof.rt.fs.len(), sample_r);
+
+        let degree = SEPTIC_EXTENSION_DEGREE;
+        for (idx, eval_expr) in first_layer.out_sel_and_eval_exprs[x_group_idx]
+            .1
+            .iter()
+            .enumerate()
+        {
+            let EvalExpression::Single(out_idx) = eval_expr else {
+                panic!("ecc bridge x group must use EvalExpression::Single");
+            };
+            let x0 = builder.get(&ecc_proof.evals, 3 + degree + idx);
+            let x1 = builder.get(&ecc_proof.evals, 3 + degree * 3 + idx);
+            let eval = builder.eval(x0 * one_minus_r + x1 * sample_r);
+            let claim: PointAndEvalVariable<C> = builder.eval(PointAndEvalVariable {
+                point: PointVariable {
+                    fs: xy_point.clone(),
+                },
+                eval,
+            });
+            builder.set(&out_evals, *out_idx, claim);
+        }
+
+        for (idx, eval_expr) in first_layer.out_sel_and_eval_exprs[y_group_idx]
+            .1
+            .iter()
+            .enumerate()
+        {
+            let EvalExpression::Single(out_idx) = eval_expr else {
+                panic!("ecc bridge y group must use EvalExpression::Single");
+            };
+            let y0 = builder.get(&ecc_proof.evals, 3 + degree * 2 + idx);
+            let y1 = builder.get(&ecc_proof.evals, 3 + degree * 4 + idx);
+            let eval = builder.eval(y0 * one_minus_r + y1 * sample_r);
+            let claim: PointAndEvalVariable<C> = builder.eval(PointAndEvalVariable {
+                point: PointVariable {
+                    fs: xy_point.clone(),
+                },
+                eval,
+            });
+            builder.set(&out_evals, *out_idx, claim);
+        }
+
+        for (idx, eval_expr) in first_layer.out_sel_and_eval_exprs[slope_group_idx]
+            .1
+            .iter()
+            .enumerate()
+        {
+            let EvalExpression::Single(out_idx) = eval_expr else {
+                panic!("ecc bridge slope group must use EvalExpression::Single");
+            };
+            let s1 = builder.get(&ecc_proof.evals, 3 + idx);
+            let eval = builder.eval(s1 * sample_r);
+            let claim: PointAndEvalVariable<C> = builder.eval(PointAndEvalVariable {
+                point: PointVariable {
+                    fs: s_point.clone(),
+                },
+                eval,
+            });
+            builder.set(&out_evals, *out_idx, claim);
+        }
+    }
+
     builder.cycle_tracker_start("Verify GKR Circuit");
     let rt = verify_gkr_circuit(
         builder,
@@ -904,9 +999,8 @@ pub fn verify_gkr_circuit<C: Config>(
                 },
         } = layer_proof;
 
-        let expected_main_evals_len: Usize<C::N> = Usize::from(
-            layer.n_witin + layer.n_fixed + layer.n_instance + layer.n_structural_witin,
-        );
+        let expected_main_evals_len: Usize<C::N> =
+            Usize::from(layer.n_witin + layer.n_fixed + layer.n_structural_witin);
         builder.assert_usize_eq(expected_main_evals_len, main_evals.len());
 
         transcript_observe_label(builder, challenger, b"combine subset evals");
@@ -947,7 +1041,7 @@ pub fn verify_gkr_circuit<C: Config>(
             unipoly_extrapolator,
         );
 
-        let structural_witin_offset = layer.n_witin + layer.n_fixed + layer.n_instance;
+        let structural_witin_offset = layer.n_witin + layer.n_fixed;
 
         // check selector evaluations
         layer

ceno_zkvm/src/scheme/cpu/mod.rs

@@ -8,15 +8,17 @@ use crate::{
         constants::{NUM_FANIN, SEPTIC_EXTENSION_DEGREE},
         hal::{DeviceProvingKey, EccQuarkProver, ProofInput, TowerProverSpec},
         septic_curve::{SepticExtension, SepticPoint, SymbolicSepticExtension},
-        utils::{infer_tower_logup_witness, infer_tower_product_witness},
+        utils::{
+            assign_group_evals, derive_ecc_bridge_claims, extract_ecc_quark_witness_inputs,
+            infer_tower_logup_witness, infer_tower_product_witness, split_rotation_evals,
+        },
     },
     structs::{ComposedConstrainSystem, EccQuarkProof, PointAndEval, TowerProofs},
 };
 use either::Either;
 use ff_ext::ExtensionField;
 use gkr_iop::{
     cpu::{CpuBackend, CpuProver},
-    evaluation::EvalExpression,
     gkr::{self, Evaluation, GKRProof, GKRProverOutput, layer::LayerWitness},
     hal::ProverBackend,
     selector::{SelectorContext, SelectorType},
@@ -312,19 +314,22 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> EccQuarkProver<CpuBa
 {
     fn prove_ec_sum_quark<'a>(
         &self,
-        num_instances: usize,
-        xs: Vec<Arc<MultilinearExtension<'a, E>>>,
-        ys: Vec<Arc<MultilinearExtension<'a, E>>>,
-        invs: Vec<Arc<MultilinearExtension<'a, E>>>,
+        cs: &ComposedConstrainSystem<E>,
+        input: &ProofInput<'a, CpuBackend<E, PCS>>,
         transcript: &mut impl Transcript<E>,
-    ) -> Result<EccQuarkProof<E>, ZKVMError> {
-        Ok(CpuEccProver::create_ecc_proof(
-            num_instances,
-            xs,
-            ys,
-            invs,
+    ) -> Result<Option<EccQuarkProof<E>>, ZKVMError> {
+        let Some(ecc_inputs) = extract_ecc_quark_witness_inputs::<CpuBackend<E, PCS>>(cs, input)
+        else {
+            return Ok(None);
+        };
+
+        Ok(Some(CpuEccProver::create_ecc_proof(
+            input.num_instances(),
+            ecc_inputs.xs,
+            ecc_inputs.ys,
+            ecc_inputs.slopes,
             transcript,
-        ))
+        )))
     }
 }
 
@@ -876,6 +881,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> MainSumcheckProver<C
         &self,
         rt_tower: Vec<E>,
         rotation: Option<RotationProverOutput<E>>,
+        ecc_proof: Option<&EccQuarkProof<E>>,
         input: &'b ProofInput<'a, CpuBackend<E, PCS>>,
         composed_cs: &ComposedConstrainSystem<E>,
         challenges: &[E; 2],
@@ -937,58 +943,66 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> MainSumcheckProver<C
 
         let mut out_evals =
             vec![PointAndEval::new(rt_tower.clone(), E::ZERO); gkr_circuit.n_evaluations];
+
         if let Some(rotation) = rotation.as_ref() {
             let Some([left_group_idx, right_group_idx, point_group_idx]) =
                 first_layer.rotation_selector_group_indices()
             else {
                 panic!("rotation proof provided for non-rotation layer")
             };
 
-            let mut left_evals = Vec::new();
-            let mut right_evals = Vec::new();
-            let mut point_evals = Vec::new();
-            for chunk in rotation.proof.evals.chunks_exact(3) {
-                left_evals.push(chunk[0]);
-                right_evals.push(chunk[1]);
-                point_evals.push(chunk[2]);
-            }
+            let (left_evals, right_evals, point_evals) =
+                split_rotation_evals(&rotation.proof.evals);
 
-            let assign_group = |out_evals: &mut [PointAndEval<E>],
-                                eval_exprs: &[EvalExpression<E>],
-                                evals: &[E],
-                                point: &Point<E>| {
-                assert_eq!(
-                    eval_exprs.len(),
-                    evals.len(),
-                    "rotation eval length mismatch"
-                );
-                for (eval_expr, eval) in eval_exprs.iter().zip_eq(evals.iter()) {
-                    let EvalExpression::Single(index) = eval_expr else {
-                        panic!("rotation groups must use EvalExpression::Single");
-                    };
-                    out_evals[*index] = PointAndEval::new(point.clone(), *eval);
-                }
-            };
-
-            assign_group(
+            assign_group_evals(
                 &mut out_evals,
                 &first_layer.out_sel_and_eval_exprs[left_group_idx].1,
                 &left_evals,
                 &rotation.left_point,
             );
-            assign_group(
+            assign_group_evals(
                 &mut out_evals,
                 &first_layer.out_sel_and_eval_exprs[right_group_idx].1,
                 &right_evals,
                 &rotation.right_point,
             );
-            assign_group(
+            assign_group_evals(
                 &mut out_evals,
                 &first_layer.out_sel_and_eval_exprs[point_group_idx].1,
                 &point_evals,
                 &rotation.point,
             );
         }
+
+        if let Some(ecc_proof) = ecc_proof {
+            let Some([x_group_idx, y_group_idx, slope_group_idx]) =
+                first_layer.ecc_bridge_group_indices()
+            else {
+                panic!("ecc proof provided for non-ecc layer")
+            };
+
+            let sample_r = transcript.sample_and_append_vec(b"ecc_gkr_bridge_r", 1)[0];
+            let claims = derive_ecc_bridge_claims(ecc_proof, sample_r, num_var_with_rotation);
+
+            assign_group_evals(
+                &mut out_evals,
+                &first_layer.out_sel_and_eval_exprs[x_group_idx].1,
+                &claims.x_evals,
+                &claims.xy_point,
+            );
+            assign_group_evals(
+                &mut out_evals,
+                &first_layer.out_sel_and_eval_exprs[y_group_idx].1,
+                &claims.y_evals,
+                &claims.xy_point,
+            );
+            assign_group_evals(
+                &mut out_evals,
+                &first_layer.out_sel_and_eval_exprs[slope_group_idx].1,
+                &claims.s_evals,
+                &claims.s_point,
+            );
+        }
         let GKRProverOutput {
             gkr_proof,
             opening_evaluations,