diff --git a/src/gadgets/ecc/mod.rs b/src/gadgets/ecc/mod.rs index f8575628..21ec4ae3 100644 --- a/src/gadgets/ecc/mod.rs +++ b/src/gadgets/ecc/mod.rs @@ -371,6 +371,25 @@ pub(crate) mod tests { y: C::Base, is_inf: bool, } + impl From for Point { + fn from(value: C) -> Self { + let c = value.coordinates().unwrap(); + + Self { + x: *c.x(), + y: *c.y(), + is_inf: value.is_identity().into(), + } + } + } + + impl Point { + pub fn into_curve(self) -> C { + let Self { x, y, is_inf: _ } = self; + C::from_xy(x, y).unwrap() + } + } + impl Point { fn default() -> Self { Self { @@ -441,7 +460,7 @@ pub(crate) mod tests { } } - fn scalar_mul(&self, scalar: &F) -> Self { + pub fn scalar_mul(&self, scalar: &F) -> Self { let mut res = Self { x: C::Base::ZERO, y: C::Base::ZERO, diff --git a/src/ivc/cyclefold/sfc/input/assigned.rs b/src/ivc/cyclefold/sfc/input/assigned.rs index 893929a5..e1ef8ec0 100644 --- a/src/ivc/cyclefold/sfc/input/assigned.rs +++ b/src/ivc/cyclefold/sfc/input/assigned.rs @@ -5,8 +5,12 @@ use itertools::Itertools; use tracing::error; use crate::{ + gadgets::nonnative::bn::big_uint_mul_mod_chip::BigUintMulModChip, halo2_proofs::plonk::Error as Halo2PlonkError, - ivc::{self, cyclefold::ro_chip}, + ivc::{ + self, + cyclefold::{ro_chip, DEFAULT_LIMBS_COUNT_LIMIT, DEFAULT_LIMB_WIDTH}, + }, main_gate::{self, AdviceCyclicAssignor, AssignedValue, MainGate, RegionCtx, WrapValue}, poseidon::ROCircuitTrait, }; @@ -498,6 +502,19 @@ impl PairedTrace { .chain(std::iter::once(WrapValue::Assigned(b.clone()))) })) } + + pub fn get_self_W_commitment_from_paired(&self) -> Vec>> { + self.incoming + .iter() + .map(|tr| { + let (W, _other) = tr.instances[0].split_at(2); + BigUintPoint { + x: W[0].clone(), + y: W[1].clone(), + } + }) + .collect::>() + } } pub struct Input { @@ -602,6 +619,62 @@ impl Input { Ok(self) } + + pub fn pairing_check( + &self, + region: &mut RegionCtx, + main_gate_config: &MainGateConfig, + poly_L_values: &[AssignedValue], + new_acc: &mut ProtoGalaxyAccumulatorInstance, + ) -> Result<(), Halo2PlonkError> { + let bn_chip = BigUintMulModChip::new( + main_gate_config.into_smaller_size().unwrap(), + DEFAULT_LIMB_WIDTH, + DEFAULT_LIMBS_COUNT_LIMIT, + ); + + let expected_l0 = bn_chip + .from_assigned_cell_to_limbs(region, &poly_L_values[0]) + .map_err(|err| { + error!("while make from L0 biguint form: {err:?}"); + Halo2PlonkError::Synthesis + })?; + + let expected_l1 = bn_chip + .from_assigned_cell_to_limbs(region, &poly_L_values[1]) + .map_err(|err| { + error!("while make from L1 biguint form: {err:?}"); + Halo2PlonkError::Synthesis + })?; + + for (acc_W, incoming_W, trace, new_acc_W) in itertools::multizip(( + self.self_trace.input_accumulator.ins.W_commitments.iter(), + self.self_trace.incoming.W_commitments.iter(), + self.paired_trace.incoming.iter(), + new_acc.ins.W_commitments.iter_mut(), + )) { + let [expected_x, expected_y, x0, y0, l0, x1, y1, l1] = + trace.instances[0].clone().try_into().unwrap(); + + l0.iter() + .zip_eq(expected_l0.iter()) + .try_for_each(|(l, r)| region.constrain_equal(l.cell(), r.cell()))?; + + l1.iter() + .zip_eq(expected_l1.iter()) + .try_for_each(|(l, r)| region.constrain_equal(l.cell(), r.cell()))?; + + BigUintPoint::constrain_equal(region, acc_W, &BigUintPoint { x: x0, y: y0 })?; + BigUintPoint::constrain_equal(region, incoming_W, &BigUintPoint { x: x1, y: y1 })?; + + *new_acc_W = BigUintPoint { + x: expected_x, + y: expected_y, + }; + } + + Ok(()) + } } pub fn iter_consistency_marker_wrap_values<'l, const ARITY: usize, F: PrimeField>( diff --git a/src/ivc/cyclefold/sfc/mod.rs b/src/ivc/cyclefold/sfc/mod.rs index 1a9dc1bd..7856b2e5 100644 --- a/src/ivc/cyclefold/sfc/mod.rs +++ b/src/ivc/cyclefold/sfc/mod.rs @@ -12,7 +12,10 @@ use crate::{ }, ivc::{ cyclefold::{self, ro_chip}, - protogalaxy::{self, verify_chip}, + protogalaxy::{ + self, + verify_chip::{self, VerifyResult}, + }, StepCircuit, }, main_gate::{MainGate, MainGateConfig, RegionCtx}, @@ -142,7 +145,10 @@ where |region| { let mut region = RegionCtx::new(region, 0); - protogalaxy::verify_chip::verify( + let VerifyResult { + mut result_acc, + poly_L_values, + } = protogalaxy::verify_chip::verify( &mut region, config.mg.clone(), ro_chip(config.mg.clone()), @@ -156,7 +162,16 @@ where .map_err(|err| { error!("while protogalaxy::verify: {err:?}"); Halo2PlonkError::Synthesis - }) + })?; + + input.pairing_check( + &mut region, + &config.mg, + &poly_L_values, + &mut result_acc, + )?; + + Ok(result_acc) }, )?; diff --git a/src/ivc/cyclefold/support_circuit/mod.rs b/src/ivc/cyclefold/support_circuit/mod.rs index 78c97b9e..3630b03f 100644 --- a/src/ivc/cyclefold/support_circuit/mod.rs +++ b/src/ivc/cyclefold/support_circuit/mod.rs @@ -43,14 +43,14 @@ impl InstanceInput { let p_out = self.p_out.coordinates().unwrap(); vec![vec![ + *p_out.x(), + *p_out.y(), *p0.x(), *p0.y(), self.l0, *p1.x(), *p1.y(), self.l1, - *p_out.x(), - *p_out.y(), ]] } } @@ -98,7 +98,7 @@ where |region| { let mut ctx = RegionCtx::new(region, 0); - let [x0, y0, l0, x1, y1, l1, _expected_x, _expected_y] = ecc_chip + let [expected_x, expected_y, x0, y0, l0, x1, y1, l1] = ecc_chip .gate .assign_values_from_instance(&mut ctx, config.instance, 0) .unwrap(); @@ -133,15 +133,15 @@ where trace!("p1 * l1_bits"); let AssignedPoint { - x: _actual_x, - y: _actual_y, + x: actual_x, + y: actual_y, } = ecc_chip.add(&mut ctx, &lhs, &rhs).unwrap(); trace!("add finished"); - //ctx.constrain_equal(expected_x.cell(), actual_x.cell()) - // .unwrap(); - //ctx.constrain_equal(expected_y.cell(), actual_y.cell()) - // .unwrap(); + ctx.constrain_equal(expected_x.cell(), actual_x.cell()) + .unwrap(); + ctx.constrain_equal(expected_y.cell(), actual_y.cell()) + .unwrap(); Ok(()) }, @@ -156,6 +156,7 @@ mod tests { use super::*; use crate::{ + gadgets::ecc::tests::Point, halo2_proofs::dev::MockProver, prelude::{bn256::C1Affine as Curve, Field}, }; @@ -177,7 +178,11 @@ mod tests { let tmp = p0 * l0; trace!("p0 * l0_bits = {:?}", tmp); - let p_out = ((p0 * l0) + (p1 * l1)).into(); + + let p_out = Point::from(p0) + .scalar_mul(&l0) + .add(&Point::from(p1).scalar_mul(&l1)) + .into_curve(); let l0 = Base::from_repr(l0.to_repr()).unwrap(); let l1 = Base::from_repr(l1.to_repr()).unwrap(); diff --git a/src/ivc/protogalaxy/mod.rs b/src/ivc/protogalaxy/mod.rs index 4ab020c4..d5e0c674 100644 --- a/src/ivc/protogalaxy/mod.rs +++ b/src/ivc/protogalaxy/mod.rs @@ -89,6 +89,22 @@ pub mod verify_chip { .map(|v| WrapValue::Assigned(v.clone())) } + pub fn constrain_equal( + region: &mut RegionCtx<'_, F>, + lhs: &Self, + rhs: &Self, + ) -> Result<(), Halo2PlonkError> { + lhs.x_limbs() + .zip_eq(rhs.x_limbs()) + .try_for_each(|(lhs, rhs)| region.constrain_equal(lhs.cell(), rhs.cell()))?; + + lhs.y_limbs() + .zip_eq(rhs.y_limbs()) + .try_for_each(|(lhs, rhs)| region.constrain_equal(lhs.cell(), rhs.cell()))?; + + Ok(()) + } + fn conditional_select( region: &mut RegionCtx<'_, F>, mg: &MainGate, @@ -828,9 +844,9 @@ pub mod verify_chip { main_gate: &MainGate, acc: &AssignedPlonkInstance, incoming: &[AssignedPlonkInstance; L], - gamma_cha: &mut ValuePowers, + poly_L_values: &[AssignedValue], ) -> Result, Halo2PlonkError> { - let l_0 = eval_lagrange_poly::(region, main_gate, 0, gamma_cha)?; + let l_0 = &poly_L_values[0]; let new_acc = AssignedPlonkInstance { W_commitments: acc.W_commitments.clone(), // Don't fold here, delegate it to secondary circuit @@ -840,14 +856,14 @@ pub mod verify_chip { .map(|instance| { instance .iter() - .map(|cell| main_gate.mul(region, cell, &l_0)) + .map(|cell| main_gate.mul(region, cell, l_0)) .collect::, _>>() }) .collect::, _>>()?, challenges: acc .challenges .iter() - .map(|cell| main_gate.mul(region, cell, &l_0)) + .map(|cell| main_gate.mul(region, cell, l_0)) .collect::, _>>()?, }; @@ -855,7 +871,7 @@ pub mod verify_chip { .iter() .enumerate() .try_fold(new_acc, |mut acc, (index, tr)| { - let l_n = eval_lagrange_poly::(region, main_gate, index + 1, gamma_cha)?; + let l_n = &poly_L_values[index + 1]; acc.instances .iter_mut() @@ -863,7 +879,7 @@ pub mod verify_chip { .try_for_each(|(acc_instances, instances)| { acc_instances.iter_mut().zip_eq(instances).try_for_each( |(acc_instance, instance)| { - let rhs = main_gate.mul(region, instance, &l_n)?; + let rhs = main_gate.mul(region, instance, l_n)?; let new = main_gate.add(region, acc_instance, &rhs)?; @@ -878,7 +894,7 @@ pub mod verify_chip { .iter_mut() .zip_eq(tr.challenges.iter()) .try_for_each(|(acc_challenge, challenge)| { - let rhs = main_gate.mul(region, challenge, &l_n)?; + let rhs = main_gate.mul(region, challenge, l_n)?; let new = main_gate.add(region, acc_challenge, &rhs)?; @@ -920,6 +936,11 @@ pub mod verify_chip { Ok(()) } + pub struct VerifyResult { + pub result_acc: AssignedAccumulatorInstance, + pub poly_L_values: Box<[AssignedValue]>, + } + /// Assigned version of `fn verify` logic from [`crate::nifs::protogalaxy::ProtoGalaxy`]. /// /// # Algorithm @@ -951,7 +972,7 @@ pub mod verify_chip { accumulator: AssignedAccumulatorInstance, incoming: &[AssignedPlonkInstance; L], proof: AssignedProof, - ) -> Result, Error> + ) -> Result, Error> where F: FromUniformBytes<64> + PrimeFieldBits, { @@ -998,16 +1019,27 @@ pub mod verify_chip { ) .map_err(|err| Error::WhileE { err })?; + let poly_L_values = (0..) + .map(|index| { + eval_lagrange_poly::(region, &main_gate, index, &mut gamma_powers) + }) + .take(L + 1) + .collect::, _>>() + .map_err(|err| Error::Fold { err })?; + let ins = fold_instances( region, &main_gate, &accumulator.ins, incoming, - &mut gamma_powers, + &poly_L_values, ) .map_err(|err| Error::Fold { err })?; - Ok(AssignedAccumulatorInstance { ins, betas, e }) + Ok(VerifyResult { + result_acc: AssignedAccumulatorInstance { ins, betas, e }, + poly_L_values, + }) } #[cfg(test)]