Skip to content

Commit

Permalink
feat(ivc): cyclefold::pairing_check
Browse files Browse the repository at this point in the history
**Motivation**
As part of impl of sfc (#369) we delegate ecc_scalar_mul computing to a suppport circuit. Within primary sfc we must validate the input and reuse the output to deduce the W_commitment protogalaxy of the accumulator

**Overview**
I use the lagrange coefficients that we have already evaluated inside `protogalaxy::verify`.
  • Loading branch information
cyphersnake committed Dec 3, 2024
1 parent fafbf38 commit 46f3db4
Show file tree
Hide file tree
Showing 5 changed files with 156 additions and 25 deletions.
21 changes: 20 additions & 1 deletion src/gadgets/ecc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -371,6 +371,25 @@ pub(crate) mod tests {
y: C::Base,
is_inf: bool,
}
impl<C: CurveAffine> From<C> for Point<C> {
fn from(value: C) -> Self {
let c = value.coordinates().unwrap();

Self {
x: *c.x(),
y: *c.y(),
is_inf: value.is_identity().into(),
}
}
}

impl<C: CurveAffine> Point<C> {
pub fn into_curve(self) -> C {
let Self { x, y, is_inf: _ } = self;
C::from_xy(x, y).unwrap()
}
}

impl<C: CurveAffine> Point<C> {
fn default() -> Self {
Self {
Expand Down Expand Up @@ -441,7 +460,7 @@ pub(crate) mod tests {
}
}

fn scalar_mul<F: PrimeFieldBits>(&self, scalar: &F) -> Self {
pub fn scalar_mul<F: PrimeFieldBits>(&self, scalar: &F) -> Self {
let mut res = Self {
x: C::Base::ZERO,
y: C::Base::ZERO,
Expand Down
62 changes: 61 additions & 1 deletion src/ivc/cyclefold/sfc/input/assigned.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};
Expand Down Expand Up @@ -602,6 +606,62 @@ impl<const A: usize, F: PrimeField> Input<A, F> {

Ok(self)
}

pub fn pairing_check(
&self,
region: &mut RegionCtx<F>,
main_gate_config: &MainGateConfig,
poly_L_values: &[AssignedValue<F>],
new_acc: &mut ProtoGalaxyAccumulatorInstance<F>,
) -> 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>(
Expand Down
21 changes: 18 additions & 3 deletions src/ivc/cyclefold/sfc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -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()),
Expand All @@ -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)
},
)?;

Expand Down
25 changes: 15 additions & 10 deletions src/ivc/cyclefold/support_circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,14 +43,14 @@ impl<C: CurveAffine> InstanceInput<C> {
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(),
]]
}
}
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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(())
},
Expand All @@ -156,6 +156,7 @@ mod tests {

use super::*;
use crate::{
gadgets::ecc::tests::Point,
halo2_proofs::dev::MockProver,
prelude::{bn256::C1Affine as Curve, Field},
};
Expand All @@ -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();
Expand Down
52 changes: 42 additions & 10 deletions src/ivc/protogalaxy/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<const T: usize>(
region: &mut RegionCtx<'_, F>,
mg: &MainGate<F, T>,
Expand Down Expand Up @@ -828,9 +844,9 @@ pub mod verify_chip {
main_gate: &MainGate<F, T>,
acc: &AssignedPlonkInstance<F>,
incoming: &[AssignedPlonkInstance<F>; L],
gamma_cha: &mut ValuePowers<F>,
poly_L_values: &[AssignedValue<F>],
) -> Result<AssignedPlonkInstance<F>, Halo2PlonkError> {
let l_0 = eval_lagrange_poly::<F, T, L>(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
Expand All @@ -840,30 +856,30 @@ 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::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?,
challenges: acc
.challenges
.iter()
.map(|cell| main_gate.mul(region, cell, &l_0))
.map(|cell| main_gate.mul(region, cell, l_0))
.collect::<Result<Vec<_>, _>>()?,
};

incoming
.iter()
.enumerate()
.try_fold(new_acc, |mut acc, (index, tr)| {
let l_n = eval_lagrange_poly::<F, T, L>(region, main_gate, index + 1, gamma_cha)?;
let l_n = &poly_L_values[index + 1];

acc.instances
.iter_mut()
.zip_eq(tr.instances.iter())
.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)?;

Expand All @@ -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)?;

Expand Down Expand Up @@ -920,6 +936,11 @@ pub mod verify_chip {
Ok(())
}

pub struct VerifyResult<F: PrimeField> {
pub result_acc: AssignedAccumulatorInstance<F>,
pub poly_L_values: Box<[AssignedValue<F>]>,
}

/// Assigned version of `fn verify` logic from [`crate::nifs::protogalaxy::ProtoGalaxy`].
///
/// # Algorithm
Expand Down Expand Up @@ -951,7 +972,7 @@ pub mod verify_chip {
accumulator: AssignedAccumulatorInstance<F>,
incoming: &[AssignedPlonkInstance<F>; L],
proof: AssignedProof<F>,
) -> Result<AssignedAccumulatorInstance<F>, Error>
) -> Result<VerifyResult<F>, Error>
where
F: FromUniformBytes<64> + PrimeFieldBits,
{
Expand Down Expand Up @@ -998,16 +1019,27 @@ pub mod verify_chip {
)
.map_err(|err| Error::WhileE { err })?;

let poly_L_values = (0..)
.map(|index| {
eval_lagrange_poly::<F, T, L>(region, &main_gate, index, &mut gamma_powers)
})
.take(L + 1)
.collect::<Result<Box<[_]>, _>>()
.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)]
Expand Down

0 comments on commit 46f3db4

Please sign in to comment.