allow 2 PIs

Author: Michael-EY

plonk/src/nightfall/accumulation/circuit/atomic_gadgets.rs

@@ -322,8 +322,8 @@ mod tests {
         circuit
             .finalize_for_recursive_mle_arithmetization::<RescueCRHF<FqBn254>>()
             .unwrap();
-        let pi = circuit.public_input().unwrap()[0];
-        circuit.check_circuit_satisfiability(&[pi]).unwrap();
+        let pi = circuit.public_input().unwrap();
+        circuit.check_circuit_satisfiability(&pi).unwrap();
     }
 
     #[test]
@@ -450,8 +450,8 @@ mod tests {
         circuit
             .finalize_for_recursive_mle_arithmetization::<RescueCRHF<FrBn254>>()
             .unwrap();
-        let pi = circuit.public_input().unwrap()[0];
-        circuit.check_circuit_satisfiability(&[pi]).unwrap();
+        let pi = circuit.public_input().unwrap();
+        circuit.check_circuit_satisfiability(&pi).unwrap();
         let srs_size = circuit.num_gates().ilog2() as usize;
         let srs = Zeromorph::<UnivariateIpaPCS<Grumpkin>>::gen_srs_for_testing(&mut rng, srs_size)
             .unwrap();

plonk/src/nightfall/circuit/plonk_partial_verifier/gadgets.rs

@@ -33,7 +33,7 @@ use super::{
 #[allow(clippy::too_many_arguments)]
 pub fn compute_scalars_for_native_field<F: PrimeField + RescueParameter>(
     circuit: &mut PlonkCircuit<F>,
-    pi: &Variable,
+    pi: &[Variable; 2],
     challenges: &ChallengesVar,
     proof_evals: &ProofEvalsVarNative,
     lookup_evals: &Option<PlookupEvalsVarNative>,
@@ -275,7 +275,7 @@ pub fn compute_scalars_for_native_field<F: PrimeField + RescueParameter>(
 #[allow(clippy::too_many_arguments)]
 pub(crate) fn compute_scalars_for_native_field_base<F: PrimeField + RescueParameter>(
     circuit: &mut PlonkCircuit<F>,
-    pi: &Variable,
+    pi: &[Variable; 2],
     challenges: &ChallengesVar,
     proof_evals: &ProofEvalsVarNative,
     lookup_evals: &Option<PlookupEvalsVarNative>,
@@ -307,6 +307,7 @@ pub(crate) fn compute_scalars_for_native_field_base<F: PrimeField + RescueParame
     let evals = poly::evaluate_poly_helper_native_base(
         circuit,
         challenges.zeta,
+        vk_var.domain.gen,
         gen_inv_var,
         vk_var.domain.domain_size,
         max_domain_size,
@@ -767,26 +768,35 @@ mod test {
         // 5. Verification
 
         for (i, proof) in proofs.iter().enumerate() {
-            let pi = public_inputs[i][0];
+            let pi = public_inputs[i].clone();
             let mut transcript = <RescueTranscript<F> as Transcript>::new_transcript(b"mle_plonk");
-            let mle_challenges = MLEChallenges::new_recursion(&proof.proof, &[pi], &mut transcript)
+            let mle_challenges = MLEChallenges::new_recursion(&proof.proof, &pi, &mut transcript)
                 .map_err(|_| {
-                    CircuitError::ParameterError("MLE challenge generation failed".to_string())
-                })?;
+                CircuitError::ParameterError("MLE challenge generation failed".to_string())
+            })?;
 
             let mut plonk_circuit = PlonkCircuit::<F>::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
             let mle_proof_var = SAMLEProofVar::from_struct::<P>(&mut plonk_circuit, &proof.proof)?;
 
             let mut transcript_var = RescueTranscriptVar::<F>::new_transcript(&mut plonk_circuit);
-            let pi_var = plonk_circuit.create_emulated_variable(pi)?;
+            let pi_vars: [EmulatedVariable<P::ScalarField>; 2] = pi
+                .iter()
+                .map(|val| plonk_circuit.create_emulated_variable(*val))
+                .collect::<Result<Vec<_>, CircuitError>>()?
+                .try_into()
+                .map_err(|_| {
+                    CircuitError::ParameterError(
+                        "Couldn't convert public inputs to fixed length array".to_string(),
+                    )
+                })?;
             let mle_challenges_var =
                 EmulatedMLEChallenges::<E::ScalarField>::compute_challenges_vars::<
                     PCS,
                     P,
                     RescueTranscriptVar<F>,
                 >(
                     &mut plonk_circuit,
-                    &pi_var,
+                    &pi_vars,
                     &mle_proof_var,
                     &mut transcript_var,
                 )?;

plonk/src/nightfall/circuit/plonk_partial_verifier/mod.rs

@@ -936,7 +936,9 @@ mod test {
             circuit
                 .finalize_for_recursive_arithmetization::<RescueCRHF<P::ScalarField>>()
                 .unwrap();
-            let pi = circuit.public_input().unwrap()[0];
+            let pi: [P::ScalarField; 2] = circuit.public_input()?.try_into().map_err(|_| {
+                CircuitError::ParameterError("Couldn't convert to fixed length array".to_string())
+            })?;
             let max_degree = circuit.srs_size(blind)?;
             let srs = FFTPlonk::<PCS>::universal_setup_for_testing(max_degree, rng).unwrap();
 
@@ -954,7 +956,7 @@ mod test {
             let pcs_info = verifier
                 .prepare_pcs_info::<RescueTranscript<P::BaseField>>(
                     &vk,
-                    &[pi],
+                    &pi,
                     &proof.proof,
                     &None,
                     blind,
@@ -969,7 +971,7 @@ mod test {
 
             let challenges = FFTVerifier::<PCS>::compute_challenges::<
                 RescueTranscript<P::BaseField>,
-            >(&vk, &[pi], &proof.proof, &None)?;
+            >(&vk, &pi, &proof.proof, &None)?;
 
             let mut circuit = PlonkCircuit::<P::ScalarField>::new_turbo_plonk();
             let tau = circuit.create_variable(challenges.tau)?;
@@ -999,11 +1001,20 @@ mod test {
                 &proof.proof.plookup_proof.as_ref().unwrap().poly_evals,
             )?;
 
-            let pi_var = circuit.create_variable(pi)?;
+            let pi_vars: [Variable; 2] = pi
+                .iter()
+                .map(|val| circuit.create_variable(*val))
+                .collect::<Result<Vec<Variable>, CircuitError>>()?
+                .try_into()
+                .map_err(|_| {
+                    CircuitError::ParameterError(
+                        "Couldn't convert to fixed length array".to_string(),
+                    )
+                })?;
 
             let scalars = compute_scalars_for_native_field::<P::ScalarField>(
                 &mut circuit,
-                &pi_var,
+                &pi_vars,
                 &challenges_var,
                 &proof_evals,
                 &Some(lookup_evals),
@@ -1083,7 +1094,7 @@ mod test {
             let vk_k = vec![Fr254::zero(); 6];
             let scalars = compute_scalars_for_native_field::<Fr254>(
                 &mut circuit,
-                &0,
+                &[0, 0],
                 &challenges_var,
                 &proof_evals,
                 &Some(lookup_evals),

plonk/src/nightfall/circuit/plonk_partial_verifier/poly.rs

@@ -120,7 +120,7 @@ where
 /// This helper function generate the variables for the following data
 /// - Circuit evaluation of vanishing polynomial at point `zeta` i.e., output =
 ///   zeta ^ domain_size - 1 mod Fr::modulus
-/// - Evaluations of the first and the last lagrange polynomial at point `zeta`
+/// - Evaluations of the first, second and last lagrange polynomial at point `zeta`
 ///
 /// Note that outputs and zeta are both Fr element
 /// so this needs to be carried out over a non-native circuit
@@ -138,7 +138,7 @@ pub(super) fn evaluate_poly_helper_native<F>(
     zeta_var: Variable,
     gen_inv: F,
     domain_size: usize,
-) -> Result<[Variable; 4], CircuitError>
+) -> Result<[Variable; 5], CircuitError>
 where
     F: PrimeField + RescueParameter,
 {
@@ -158,10 +158,16 @@ where
 
     // ================================
     // evaluate lagrange at 1
-    //  lagrange_1_eval = (zeta^n - 1) / (zeta - 1) / domain_size
+    //  lagrange_1_eval = (zeta^n - 1) / (domain_size * (zeta - 1))
     //
     // which is proven via
     //  domain_size * lagrange_1_eval * (zeta - 1) = zeta^n - 1 mod Fr::modulus
+    //
+    // similarly we calculate
+    //  lagrange_2_eval = (zeta^n - 1) * omega / (domain_size * (zeta - omega)) = (zeta^n - 1) / (domain_size * (zeta * omega^{-1} - 1))
+    // and
+    //  lagrange_n_eval = (zeta^n - 1) * omega^{-1} / (domain_size * (zeta - omega^{-1})) = (zeta^n - 1) / (domain_size * (zeta * omega - 1))
+    //
     // ================================
 
     let domain_size = F::from(domain_size as u64);
@@ -178,31 +184,42 @@ where
     // Constrain the lagrange_1_eval to be correct.
     circuit.mul_gate(divisor_var, lagrange_1_eval_var, zeta_n_minus_one_var)?;
 
+    // Compute lagrange_2_eval
+    let divisor_var = circuit.lin_comb(&[domain_size * gen_inv], &(-domain_size), &[zeta_var])?;
+    let divisor = circuit.witness(divisor_var)?;
+    let lagrange_2_eval = zeta_n_minus_one / divisor;
+    let lagrange_2_eval_var = circuit.create_variable(lagrange_2_eval)?;
+    // Constrain the lagrange_2_eval to be correct.
+    circuit.mul_gate(divisor_var, lagrange_2_eval_var, zeta_n_minus_one_var)?;
+
+    let gen = gen_inv
+        .inverse()
+        .ok_or(CircuitError::ParameterError("Inverse Failed".to_string()))?;
     // Compute lagrange_n_eval
-    let divisor_var = circuit.lin_comb(&[domain_size], &(-domain_size * gen_inv), &[zeta_var])?;
-    let numerator_var = circuit.mul_constant(zeta_n_minus_one_var, &gen_inv)?;
+    let divisor_var = circuit.lin_comb(&[domain_size * gen], &(-domain_size), &[zeta_var])?;
     let divisor = circuit.witness(divisor_var)?;
-    let numerator = circuit.witness(numerator_var)?;
-    let lagrange_n_eval = numerator / divisor;
+    let lagrange_n_eval = zeta_n_minus_one / divisor;
     let lagrange_n_eval_var = circuit.create_variable(lagrange_n_eval)?;
     // Constrain the lagrange_n_eval to be correct.
-    circuit.mul_gate(divisor_var, lagrange_n_eval_var, numerator_var)?;
+    circuit.mul_gate(divisor_var, lagrange_n_eval_var, zeta_n_minus_one_var)?;
 
     Ok([
         zeta_n_var,
         zeta_n_minus_one_var,
         lagrange_1_eval_var,
+        lagrange_2_eval_var,
         lagrange_n_eval_var,
     ])
 }
 
 pub(super) fn evaluate_poly_helper_native_base<F>(
     circuit: &mut PlonkCircuit<F>,
     zeta_var: Variable,
+    gen_var: Variable,
     gen_inv_var: Variable,
     domain_size_var: Variable,
     max_domain_size: usize,
-) -> Result<[Variable; 4], CircuitError>
+) -> Result<[Variable; 5], CircuitError>
 where
     F: PrimeField + RescueParameter,
 {
@@ -216,10 +233,16 @@ where
 
     // ================================
     // evaluate lagrange at 1
-    //  lagrange_1_eval = (zeta^n - 1) / (zeta - 1) / domain_size
+    //  lagrange_1_eval = (zeta^n - 1) / (domain_size * (zeta - 1))
     //
     // which is proven via
     //  domain_size * lagrange_1_eval * (zeta - 1) = zeta^n - 1 mod Fr::modulus
+    //
+    // similarly we calculate
+    //  lagrange_2_eval = (zeta^n - 1) * omega / (domain_size * (zeta - omega))
+    // and
+    //  lagrange_n_eval = (zeta^n - 1) * omega^{-1} / (domain_size * (zeta - omega^{-1}))
+    //
     // ================================
 
     // lagrange_1_eval
@@ -237,6 +260,19 @@ where
     // Constrain the lagrange_1_eval to be correct.
     circuit.mul_gate(divisor_var, lagrange_1_eval_var, zeta_n_minus_one_var)?;
 
+    // Compute lagrange_2_eval
+    let divisor_var = circuit.mul_add(
+        &[domain_size_var, zeta_var, domain_size_var, gen_var],
+        &[F::one(), -F::one()],
+    )?;
+    let numerator_var = circuit.mul(zeta_n_minus_one_var, gen_var)?;
+    let divisor = circuit.witness(divisor_var)?;
+    let numerator = circuit.witness(numerator_var)?;
+    let lagrange_2_eval = numerator / divisor;
+    let lagrange_2_eval_var = circuit.create_variable(lagrange_2_eval)?;
+    // Constrain the lagrange_n_eval to be correct.
+    circuit.mul_gate(divisor_var, lagrange_2_eval_var, numerator_var)?;
+
     // Compute lagrange_n_eval
     let divisor_var = circuit.mul_add(
         &[domain_size_var, zeta_var, domain_size_var, gen_inv_var],
@@ -254,6 +290,7 @@ where
         zeta_n_var,
         zeta_n_minus_one_var,
         lagrange_1_eval_var,
+        lagrange_2_eval_var,
         lagrange_n_eval_var,
     ])
 }
@@ -431,8 +468,8 @@ pub(super) fn compute_lin_poly_constant_term_circuit_native<F>(
     gen_inv: &F,
     challenges: &ChallengesVar,
     proof_evals: &ProofEvalsVarNative,
-    pi: &Variable,
-    evals: &[Variable; 4],
+    pi: &[Variable; 2],
+    evals: &[Variable; 5],
     lookup_evals: &Option<PlookupEvalsVarNative>,
 ) -> Result<Variable, CircuitError>
 where
@@ -493,7 +530,7 @@ where
     prod = circuit.mul(tmp, prod)?;
 
     // r_plonk
-    let pi_eval = circuit.mul(*pi, evals[2])?;
+    let pi_eval = circuit.mul_add(&[pi[0], evals[2], pi[1], evals[3]], &[F::one(), F::one()])?;
     let wires = [pi_eval, prod, evals[2], challenges.alphas[1]];
     let non_lookup = circuit.gen_quad_poly(
         &wires,
@@ -512,7 +549,7 @@ where
         ];
         let tmp = circuit.lc(&wires, &[F::one(), -F::one(), -F::one(), F::zero()])?;
         let term_one = circuit.mul_add(
-            &[evals[3], tmp, evals[2], challenges.alphas[0]],
+            &[evals[4], tmp, evals[2], challenges.alphas[0]],
             &[F::one(), -F::one()],
         )?;
 
@@ -581,8 +618,8 @@ pub(super) fn compute_lin_poly_constant_term_circuit_native_base<F>(
     gen_inv_var: &Variable,
     challenges: &ChallengesVar,
     proof_evals: &ProofEvalsVarNative,
-    pi: &Variable,
-    evals: &[Variable; 4],
+    pi: &[Variable; 2],
+    evals: &[Variable; 5],
     lookup_evals: &Option<PlookupEvalsVarNative>,
 ) -> Result<Variable, CircuitError>
 where
@@ -643,7 +680,7 @@ where
     prod = circuit.mul(tmp, prod)?;
 
     // r_plonk
-    let pi_eval = circuit.mul(*pi, evals[2])?;
+    let pi_eval = circuit.mul_add(&[pi[0], evals[2], pi[1], evals[3]], &[F::one(), F::one()])?;
     let wires = [pi_eval, prod, evals[2], challenges.alphas[1]];
     let non_lookup = circuit.gen_quad_poly(
         &wires,
@@ -662,7 +699,7 @@ where
         ];
         let tmp = circuit.lc(&wires, &[F::one(), -F::one(), -F::one(), F::zero()])?;
         let term_one = circuit.mul_add(
-            &[evals[3], tmp, evals[2], challenges.alphas[0]],
+            &[evals[4], tmp, evals[2], challenges.alphas[0]],
             &[F::one(), -F::one()],
         )?;
 
@@ -760,7 +797,7 @@ pub fn linearization_scalars_circuit_native<F>(
     circuit: &mut PlonkCircuit<F>,
     vk_k: &[F],
     challenges: &ChallengesVar,
-    evals: &[Variable; 4],
+    evals: &[Variable; 5],
     poly_evals: &ProofEvalsVarNative,
     lookup_evals: &Option<PlookupEvalsVarNative>,
     gen_inv: &F,
@@ -1004,7 +1041,7 @@ where
                 challenges.alphas[0],
                 evals[2],
                 challenges.alphas[1],
-                evals[3],
+                evals[4],
             ],
             &[F::one(), F::one()],
         )?;
@@ -1081,7 +1118,7 @@ pub fn linearization_scalars_circuit_native_base<F>(
     circuit: &mut PlonkCircuit<F>,
     vk_k: &[Variable],
     challenges: &ChallengesVar,
-    evals: &[Variable; 4],
+    evals: &[Variable; 5],
     poly_evals: &ProofEvalsVarNative,
     lookup_evals: &Option<PlookupEvalsVarNative>,
     gen_inv_var: &Variable,
@@ -1318,7 +1355,7 @@ where
                 challenges.alphas[0],
                 evals[2],
                 challenges.alphas[1],
-                evals[3],
+                evals[4],
             ],
             &[F::one(), F::one()],
         )?;

plonk/src/nightfall/circuit/plonk_partial_verifier/proof_to_var.rs

@@ -278,7 +278,7 @@ pub struct Bn254OutputScalarsAndBasesVar {
     /// The proof generated by the recursive prover.
     pub proof: Bn254ProofScalarsandBasesVar,
     /// The hash of the public inputs to this proof stored in the clear.
-    pub pi_hash: Fr254,
+    pub pi_hash: [Fr254; 2],
     /// The transcript of the proof stored in the clear.
     pub transcript: RescueTranscript<Fr254>,
 }