Skip to content

Commit

Permalink
feat(ivc): impl cyclefold::sfc verify protogalaxy
Browse files Browse the repository at this point in the history
**Motvation**
As part of the sfc implementation (#369), we call `protogalaxy::verify_chip` for its own trace, among other things

**Overview**
Since ivc::protogalaxy & ivc::cyclefold are independent types, we have
structures that are independent of each other, yet similar one to one.
We need to cast them to an equivalent form (`BigUintPoint`)

- [ ] WIP: W_commitment to BigUintPoint in both structure
  • Loading branch information
cyphersnake committed Dec 16, 2024
1 parent 9b3e6df commit 541f20d
Show file tree
Hide file tree
Showing 3 changed files with 163 additions and 41 deletions.
9 changes: 5 additions & 4 deletions src/ivc/cyclefold/sfc/input/assigned.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ type BigUint<F> = Vec<AssignedValue<F>>;

#[derive(Clone)]
pub struct BigUintPoint<F: PrimeField> {
x_limbs: BigUint<F>,
y_limbs: BigUint<F>,
pub x_limbs: BigUint<F>,
pub y_limbs: BigUint<F>,
}

impl<F: PrimeField> BigUintPoint<F> {
Expand Down Expand Up @@ -141,9 +141,10 @@ impl<F: PrimeField> ProtoGalaxyAccumulatorInstance<F> {
}
}

#[derive(Debug, Clone)]
pub struct ProtogalaxyProof<F: PrimeField> {
poly_F: Vec<AssignedValue<F>>,
poly_K: Vec<AssignedValue<F>>,
pub poly_F: Vec<AssignedValue<F>>,
pub poly_K: Vec<AssignedValue<F>>,
}

impl<F: PrimeField> ProtogalaxyProof<F> {
Expand Down
139 changes: 131 additions & 8 deletions src/ivc/cyclefold/sfc/mod.rs
Original file line number Diff line number Diff line change
@@ -1,20 +1,29 @@
use std::num::NonZeroUsize;

use itertools::Itertools;
use tracing::error;

use crate::{
halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner},
halo2curves::CurveAffine,
plonk::{Circuit, ConstraintSystem, Error as Halo2PlonkError},
},
ivc::{cyclefold, StepCircuit},
ivc::{
cyclefold::{self, ro_chip},
protogalaxy::{self, verify_chip},
StepCircuit,
},
main_gate::{MainGate, MainGateConfig, RegionCtx},
polynomial::univariate::UnivariatePoly,
poseidon::ROTrait,
};

mod input;
use halo2_proofs::halo2curves::ff::{FromUniformBytes, PrimeField, PrimeFieldBits};
pub use input::Input;

use crate::halo2_proofs::halo2curves::ff::{FromUniformBytes, PrimeField, PrimeFieldBits};

const T_MAIN_GATE: usize = 5;

/// 'SCC' here is 'Step Circuit Config'
Expand Down Expand Up @@ -63,6 +72,8 @@ where

impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> Circuit<C::ScalarExt>
for StepFoldingCircuit<'_, ARITY, C, SC>
where
C::ScalarExt: PrimeFieldBits + FromUniformBytes<64>,
{
type Config = Config<SC::Config>;
type FloorPlanner = SimpleFloorPlanner;
Expand All @@ -86,16 +97,64 @@ impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> C
config: Self::Config,
mut layouter: impl Layouter<C::ScalarExt>,
) -> Result<(), Halo2PlonkError> {
layouter.assign_region(
|| "sfc main",
let input = layouter.assign_region(
|| "sfc input",
|region| {
let mut region = RegionCtx::new(region, 0);

let _input = input::assigned::Input::assign_advice_from(
input::assigned::Input::assign_advice_from(&mut region, &self.input, &config.mg)
},
)?;

let z_out = self
.sc
.synthesize_step(config.sc, &mut layouter, &input.z_i)
.map_err(|err| {
error!("while synthesize_step: {err:?}");
Halo2PlonkError::Synthesis
})?;

let _self_acc_out = layouter.assign_region(
|| "sfc protogalaxy",
|region| {
let mut region = RegionCtx::new(region, 0);

protogalaxy::verify_chip::verify(
&mut region,
&self.input,
&config.mg,
)?;
config.mg.clone(),
ro_chip(config.mg.clone()),
verify_chip::AssignedVerifierParam {
pp_digest: input.pp_digest.clone(),
},
input.self_trace.input_accumulator.clone().into(),
&[input.self_trace.incoming.clone().into()],
input.self_trace.proof.clone().into(),
)
.map_err(|err| {
error!("while protogalaxy::verify: {err:?}");
Halo2PlonkError::Synthesis
})
},
)?;

layouter.assign_region(
|| "sfc out",
|region| {
let mut region = RegionCtx::new(region, 0);

let mg = MainGate::new(config.mg.clone());
let is_zero_step = mg.is_zero_term(&mut region, input.step.clone())?;

let _z_out: [_; ARITY] = input
.z_0
.iter()
.zip_eq(z_out.iter())
.map(|(z_0_i, z_out_i)| {
mg.conditional_select(&mut region, z_0_i, z_out_i, &is_zero_step)
})
.collect::<Result<Vec<_>, _>>()?
.try_into()
.unwrap();

Ok(())
},
Expand All @@ -104,3 +163,67 @@ impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> C
todo!()
}
}

impl<F: PrimeField> From<input::assigned::ProtoGalaxyAccumulatorInstance<F>>
for verify_chip::AssignedAccumulatorInstance<F>
{
fn from(value: input::assigned::ProtoGalaxyAccumulatorInstance<F>) -> Self {
use self::input::assigned::{NativePlonkInstance, ProtoGalaxyAccumulatorInstance};

let ProtoGalaxyAccumulatorInstance {
ins:
NativePlonkInstance {
W_commitments,
instances,
challenges,
},
betas,
e,
} = value;

Self {
betas,
e,
ins: verify_chip::AssignedPlonkInstance {
instances,
challenges,
W_commitments: W_commitments
.into_iter()
.map(|W_commitment| (W_commitment.x_limbs, W_commitment.y_limbs))
.collect(),
},
}
}
}

impl<F: PrimeField> From<input::assigned::ProtogalaxyProof<F>> for verify_chip::AssignedProof<F> {
fn from(value: input::assigned::ProtogalaxyProof<F>) -> Self {
let input::assigned::ProtogalaxyProof { poly_F, poly_K } = value;

verify_chip::AssignedProof {
poly_F: verify_chip::AssignedUnivariatePoly(UnivariatePoly(poly_F.into_boxed_slice())),
poly_K: verify_chip::AssignedUnivariatePoly(UnivariatePoly(poly_K.into_boxed_slice())),
}
}
}

impl<F: PrimeField> From<input::assigned::NativePlonkInstance<F>>
for verify_chip::AssignedPlonkInstance<F>
{
fn from(value: input::assigned::NativePlonkInstance<F>) -> Self {
let input::assigned::NativePlonkInstance {
W_commitments,
instances,
challenges,
} = value;

Self {
instances,
challenges,
W_commitments: W_commitments
.into_iter()
.map(|W_commitment| (W_commitment.x_limbs, W_commitment.y_limbs))
.collect(),
}
}
}
56 changes: 27 additions & 29 deletions src/ivc/protogalaxy/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ pub mod verify_chip {
use crate::{
gadgets::nonnative::bn::big_uint,
halo2_proofs::{
arithmetic::Field,
circuit::{AssignedCell, Chip, Value as Halo2Value},
halo2curves::{
ff::{FromUniformBytes, PrimeField, PrimeFieldBits},
Expand Down Expand Up @@ -63,9 +62,9 @@ pub mod verify_chip {

/// Assigned version of [`crate::plonk::PlonkInstance`]
pub struct AssignedPlonkInstance<F: PrimeField> {
W_commitments: Vec<BigUintPoint<AssignedValue<F>>>,
instances: Vec<Vec<AssignedValue<F>>>,
challenges: Vec<AssignedValue<F>>,
pub W_commitments: Vec<BigUintPoint<AssignedValue<F>>>,
pub instances: Vec<Vec<AssignedValue<F>>>,
pub challenges: Vec<AssignedValue<F>>,
}

fn to_bn<C: CurveAffine>(v: &C) -> Result<BigUintPoint<C::ScalarExt>, big_uint::Error> {
Expand Down Expand Up @@ -168,9 +167,9 @@ pub mod verify_chip {

/// Assigned version of [`crate::nifs::protogalaxy::accumulator::AccumulatorInstance`]
pub struct AssignedAccumulatorInstance<F: PrimeField> {
ins: AssignedPlonkInstance<F>,
betas: Box<[AssignedValue<F>]>,
e: AssignedValue<F>,
pub ins: AssignedPlonkInstance<F>,
pub betas: Box<[AssignedValue<F>]>,
pub e: AssignedValue<F>,
}

impl<F: PrimeField> AssignedAccumulatorInstance<F> {
Expand Down Expand Up @@ -276,7 +275,7 @@ pub mod verify_chip {
}

/// Assigned version of [`crate::polynomial::univariate::UnivariatePoly`]
pub struct AssignedUnivariatePoly<F: PrimeField>(UnivariatePoly<AssignedValue<F>>);
pub struct AssignedUnivariatePoly<F: PrimeField>(pub UnivariatePoly<AssignedValue<F>>);

impl<F: PrimeField> AssignedUnivariatePoly<F> {
pub fn assign<const T: usize>(
Expand Down Expand Up @@ -407,8 +406,8 @@ pub mod verify_chip {

/// Assigned version of [`crate::nifs::protogalaxy::Proof]
pub struct AssignedProof<F: PrimeField> {
poly_F: AssignedUnivariatePoly<F>,
poly_K: AssignedUnivariatePoly<F>,
pub poly_F: AssignedUnivariatePoly<F>,
pub poly_K: AssignedUnivariatePoly<F>,
}

impl<F: PrimeField> AssignedProof<F> {
Expand Down Expand Up @@ -556,11 +555,11 @@ pub mod verify_chip {
.collect::<Result<Box<[_]>, Halo2PlonkError>>()
}

fn calculate_betas_stroke<C: CurveAffine, const T: usize>(
region: &mut RegionCtx<C::ScalarExt>,
main_gate: &MainGate<C::ScalarExt, T>,
cha: PolyChallenges<AssignedCell<C::ScalarExt, C::ScalarExt>>,
) -> Result<Box<[AssignedCell<C::ScalarExt, C::ScalarExt>]>, Error> {
fn calculate_betas_stroke<F: PrimeField, const T: usize>(
region: &mut RegionCtx<F>,
main_gate: &MainGate<F, T>,
cha: PolyChallenges<AssignedValue<F>>,
) -> Result<Box<[AssignedValue<F>]>, Error> {
let deltas =
calculate_exponentiation_sequence(region, main_gate, cha.delta, cha.betas.len())
.map_err(|err| Error::Deltas { err })?;
Expand Down Expand Up @@ -795,18 +794,17 @@ pub mod verify_chip {
///
/// 5. **Fold the Instance:**
/// - [`ProtoGalaxy::fold_instance`]
pub fn verify<C: CurveAffine, const L: usize, const T: usize>(
region: &mut RegionCtx<C::ScalarExt>,
pub fn verify<F, const L: usize, const T: usize>(
region: &mut RegionCtx<F>,
main_gate_config: MainGateConfig<T>,
ro_circuit: impl ROCircuitTrait<C::ScalarExt>,
vp: AssignedVerifierParam<C::ScalarExt>,
accumulator: AssignedAccumulatorInstance<C::ScalarExt>,
incoming: &[AssignedPlonkInstance<C::ScalarExt>; L],
proof: AssignedProof<C::ScalarExt>,
) -> Result<AssignedAccumulatorInstance<C::ScalarExt>, Error>
ro_circuit: impl ROCircuitTrait<F>,
vp: AssignedVerifierParam<F>,
accumulator: AssignedAccumulatorInstance<F>,
incoming: &[AssignedPlonkInstance<F>; L],
proof: AssignedProof<F>,
) -> Result<AssignedAccumulatorInstance<F>, Error>
where
C::ScalarExt: FromUniformBytes<64> + PrimeFieldBits,
C::ScalarExt: FromUniformBytes<64> + PrimeFieldBits,
F: FromUniformBytes<64> + PrimeFieldBits,
{
let AssignedChallanges {
delta,
Expand All @@ -817,7 +815,7 @@ pub mod verify_chip {

let main_gate = MainGate::new(main_gate_config);

let betas = calculate_betas_stroke::<C, T>(
let betas = calculate_betas_stroke::<F, T>(
region,
&main_gate,
PolyChallenges {
Expand All @@ -831,7 +829,7 @@ pub mod verify_chip {
.assign_advice(
|| "one",
main_gate.config().state[0],
Halo2Value::known(C::ScalarExt::ONE),
Halo2Value::known(F::ONE),
)
.map_err(|err| Error::Assign {
annotation: "one",
Expand All @@ -842,7 +840,7 @@ pub mod verify_chip {
let mut gamma_powers = ValuePowers::new(one.clone(), gamma);
let mut alpha_powers = ValuePowers::new(one, alpha);

let e = calculate_e::<C::ScalarExt, T, L>(
let e = calculate_e::<F, T, L>(
region,
&main_gate,
&proof,
Expand Down Expand Up @@ -1069,7 +1067,7 @@ pub mod verify_chip {
let main_gate = MainGate::<Scalar, T>::new(main_gate_config.clone());

Ok(
calculate_betas_stroke::<Affine1, T>(&mut region, &main_gate, cha)
calculate_betas_stroke::<Scalar, T>(&mut region, &main_gate, cha)
.unwrap(),
)
},
Expand Down

0 comments on commit 541f20d

Please sign in to comment.