Skip to content

Commit

Permalink
feat(ivc): impl ext::synthesize_step_non_base_case (#109)
Browse files Browse the repository at this point in the history
# Enhancements to IVC and ECC in Incrementally Verifiable Computation

This PR introduces significant improvements to the IVC algorithm, focusing on the implementation of conditional selection between base and non-base cases, and refining the ECC component. 

Here's a breakdown of the changes:

## What has been done?
### Implementation of Selection Between Base and Non-Base Cases (IVC):

A new feature is introduced to handle the selection between base and non-base cases in the IVC process. At step zero our task is simply to generate a relaxed plonk instance, and at any other step to commit folding. But we are running on-circuit, so we perform both of these actions each time, and then choose one of the options depending on the step.

### Implement `synthesize_step_base_case` for step circuit module

Implemented a method to synthesize steps specifically for the base case of IVC. That is, make a call to the key folding-chip inside the `StepCircutiExt` abstraction. This is a preparation for synthesizing the step circuit itself

### New Method for On-Circuit Conditional Selection (IVC and ECC)

- Developed a new method, `AssignedRelaxed::conditional_select`, for on-circuit conditional selection between the base and non-base cases. This method plays a key role in choosing the correct assigned relaxed Plonk instance based on the step in IVC

- Enhanced the ECC component with the implementation of `conditional_select`. This auxiliary function is simplify on-circuit conditional selection of curve point.

Part of #32
  • Loading branch information
cyphersnake authored Jan 17, 2024
1 parent 1f38cbd commit 07555c7
Show file tree
Hide file tree
Showing 4 changed files with 207 additions and 55 deletions.
17 changes: 17 additions & 0 deletions src/gadgets/ecc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -356,6 +356,23 @@ impl<C: CurveAffine<Base = F>, F: PrimeFieldBits, const T: usize> EccChip<C, F,
let yr = self.main_gate.sub(ctx, &tmp3, &p.y)?;
Ok(AssignedPoint { x: xr, y: yr })
}

pub fn conditional_select(
&self,
ctx: &mut RegionCtx<'_, C::Base>,
lhs: &AssignedPoint<C>,
rhs: &AssignedPoint<C>,
condition: &AssignedValue<C::Base>,
) -> Result<AssignedPoint<C>, Error> {
Ok(AssignedPoint {
x: self
.main_gate
.conditional_select(ctx, &lhs.x, &rhs.x, condition)?,
y: self
.main_gate
.conditional_select(ctx, &lhs.y, &rhs.y, condition)?,
})
}
}

#[cfg(test)]
Expand Down
88 changes: 82 additions & 6 deletions src/ivc/fold_relaxed_plonk_instance_chip.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,27 +88,103 @@ where
pub(crate) struct AssignedRelaxedPlonkInstance<C: CurveAffine> {
/// Assigned point representing the folded accumulator W.
/// Derived from [`FoldRelaxedPlonkInstanceChip::W`]
folded_W: Vec<AssignedPoint<C>>,
pub folded_W: Vec<AssignedPoint<C>>,

/// Assigned point representing the folded accumulator E.
/// Derived from [`FoldRelaxedPlonkInstanceChip::E`]
folded_E: AssignedPoint<C>,
pub folded_E: AssignedPoint<C>,

/// Assigned value of the folded scalar u.
/// Derived from [`FoldRelaxedPlonkInstanceChip::u`]
folded_u: AssignedValue<C::Base>,
pub folded_u: AssignedValue<C::Base>,

/// Vector of vectors of assigned values for each limb of the folded challenges.
/// Derived from [`FoldRelaxedPlonkInstanceChip::challenges`].
folded_challenges: Vec<Vec<AssignedValue<C::Base>>>,
pub folded_challenges: Vec<Vec<AssignedValue<C::Base>>>,

/// Vector of assigned values for each limb of the folded big number X0.
/// Derived from [`FoldRelaxedPlonkInstanceChip::X0`]
folded_X0: Vec<AssignedValue<C::Base>>,
pub folded_X0: Vec<AssignedValue<C::Base>>,

/// Vector of assigned values for each limb of the folded big number X1.
/// Derived from [`FoldRelaxedPlonkInstanceChip::X1`]
folded_X1: Vec<AssignedValue<C::Base>>,
pub folded_X1: Vec<AssignedValue<C::Base>>,
}
impl<C: CurveAffine> AssignedRelaxedPlonkInstance<C> {
pub fn conditional_select<const T: usize>(
region: &mut RegionCtx<C::Base>,
config: &MainGateConfig<T>,
lhs: &Self,
rhs: &Self,
condition: AssignedValue<C::Base>,
) -> Result<Self, Error>
where
C::Base: PrimeFieldBits,
{
let ecc = EccChip::<C, C::Base, T>::new(config.clone());
let gate = MainGate::<C::Base, T>::new(config.clone());

let Self {
folded_W: lhs_folded_W,
folded_E: lhs_folded_E,
folded_u: lhs_folded_u,
folded_challenges: lhs_folded_challenges,
folded_X0: lhs_folded_X0,
folded_X1: lhs_folded_X1,
} = lhs;

let Self {
folded_W: rhs_folded_W,
folded_E: rhs_folded_E,
folded_u: rhs_folded_u,
folded_challenges: rhs_folded_challenges,
folded_X0: rhs_folded_X0,
folded_X1: rhs_folded_X1,
} = rhs;

let folded_W = lhs_folded_W
.iter()
.zip_eq(rhs_folded_W.iter())
.map(|(lhs_Wi, rhs_Wi)| ecc.conditional_select(region, lhs_Wi, rhs_Wi, &condition))
.collect::<Result<Vec<_>, _>>()?;

let folded_E = ecc.conditional_select(region, lhs_folded_E, rhs_folded_E, &condition)?;

let folded_u = gate.conditional_select(region, lhs_folded_u, rhs_folded_u, &condition)?;

let folded_challenges = lhs_folded_challenges
.iter()
.zip_eq(rhs_folded_challenges.iter())
.map(|(lhs_challenge, rhs_challenge)| {
lhs_challenge
.iter()
.zip_eq(rhs_challenge.iter())
.map(|(lhs, rhs)| gate.conditional_select(region, lhs, rhs, &condition))
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;

let folded_X0 = lhs_folded_X0
.iter()
.zip_eq(rhs_folded_X0.iter())
.map(|(lhs, rhs)| gate.conditional_select(region, lhs, rhs, &condition))
.collect::<Result<Vec<_>, _>>()?;

let folded_X1 = lhs_folded_X1
.iter()
.zip_eq(rhs_folded_X1.iter())
.map(|(lhs, rhs)| gate.conditional_select(region, lhs, rhs, &condition))
.collect::<Result<Vec<_>, _>>()?;

Ok(Self {
folded_W,
folded_E,
folded_u,
folded_challenges,
folded_X0,
folded_X1,
})
}
}

/// Holds the assigned values and points resulting from the folding process.
Expand Down
40 changes: 34 additions & 6 deletions src/ivc/incrementally_verifiable_computation.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
use std::{marker::PhantomData, num::NonZeroUsize};

use ff::{FromUniformBytes, PrimeFieldBits};
use ff::{Field, FromUniformBytes, PrimeField, PrimeFieldBits};
use group::prime::PrimeCurveAffine;
use halo2curves::CurveAffine;

use crate::{
commitment::CommitmentKey,
plonk::{PlonkTrace, RelaxedPlonkTrace, TableData},
poseidon::ROCircuitTrait,
poseidon::{AbsorbInRO, ROCircuitTrait, ROTrait},
};

use super::step_circuit::SynthesizeStepParams;
Expand All @@ -17,17 +17,30 @@ pub use super::{
};

// TODO #31 docs
pub struct CircuitPublicParams<C, RO>
pub struct CircuitPublicParams<C, ROC>
where
C: CurveAffine,
C::Base: PrimeFieldBits + FromUniformBytes<64>,
RO: ROCircuitTrait<C::Base>,
ROC: ROCircuitTrait<C::Base>,
{
ck: CommitmentKey<C>,
td: TableData<C::Scalar>,
ro_consts: RO::Args,
ro_consts: ROC::Args,
// ro_consts_circuit: ROTrait::Constants, // NOTE: our `ROTraitCircuit` don't have main initializer
params: SynthesizeStepParams<C, RO>,
params: SynthesizeStepParams<C, ROC>,
}

impl<AnyCurve, CC, RO, ROC> AbsorbInRO<AnyCurve, RO> for CircuitPublicParams<CC, ROC>
where
AnyCurve: CurveAffine,
CC: CurveAffine,
CC::Base: PrimeFieldBits + FromUniformBytes<64>,
RO: ROTrait<AnyCurve>,
ROC: ROCircuitTrait<CC::Base>,
{
fn absorb_into(&self, _ro: &mut RO) {
todo!("#32")
}
}

// TODO #31 docs
Expand Down Expand Up @@ -71,6 +84,21 @@ where
// https://github.com/microsoft/Nova/blob/fb83e30e16e56b3b21c519b15b83c4ce1f077a13/src/lib.rs#L98
todo!("Impl creation of pub params")
}

pub fn digest<ROT: ROTrait<C1>>(&self, constant: ROT::Constants) -> C1::ScalarExt {
let mut ro = ROT::new(constant);

let Self {
primary,
secondary,
_p,
} = &self;
primary.absorb_into(&mut ro);
secondary.absorb_into(&mut ro);

let bytes_count = C1::Base::ZERO.to_repr().as_ref().len();
ro.squeeze(NonZeroUsize::new(bytes_count * 8).unwrap())
}
}

// TODO #31 docs
Expand Down
117 changes: 74 additions & 43 deletions src/ivc/step_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,14 @@ use std::num::NonZeroUsize;

use ff::PrimeField;
use halo2_proofs::{
circuit::{AssignedCell, Layouter},
circuit::{AssignedCell, Layouter, Value},
plonk::ConstraintSystem,
};
use halo2curves::CurveAffine;

use crate::{
ivc::fold_relaxed_plonk_instance_chip::FoldRelaxedPlonkInstanceChip,
main_gate::{self, RegionCtx},
main_gate::{self, MainGate, RegionCtx},
plonk::{PlonkInstance, RelaxedPlonkInstance},
poseidon::ROCircuitTrait,
};
Expand Down Expand Up @@ -108,9 +108,9 @@ pub(crate) enum ConfigureError {
}

// TODO #32 Rename
pub(crate) struct SynthesizeStepParams<G: CurveAffine, RO: ROCircuitTrait<G::Base>>
pub(crate) struct SynthesizeStepParams<C: CurveAffine, RO: ROCircuitTrait<C::Base>>
where
G::Base: ff::PrimeFieldBits + ff::FromUniformBytes<64>,
C::Base: ff::PrimeFieldBits + ff::FromUniformBytes<64>,
{
pub limb_width: NonZeroUsize,
pub n_limbs: NonZeroUsize,
Expand All @@ -123,20 +123,21 @@ pub(crate) struct StepInputs<'link, const ARITY: usize, C: CurveAffine, RO: ROCi
where
C::Base: ff::PrimeFieldBits + ff::FromUniformBytes<64>,
{
public_params: &'link SynthesizeStepParams<C, RO>,
step_public_params: &'link SynthesizeStepParams<C, RO>,
public_params_hash: C,
step: C::Base,

z_0: [AssignedCell<C::Scalar, C::Scalar>; ARITY],
z_in: [AssignedCell<C::Scalar, C::Scalar>; ARITY],

// TODO docs
U: Option<RelaxedPlonkInstance<C>>,
U: RelaxedPlonkInstance<C>,

// TODO docs
u: Option<PlonkInstance<C>>,
u: PlonkInstance<C>,

// TODO docs
T_commitments: Option<Vec<C::Scalar>>,
cross_term_commits: Vec<C>,
}

// TODO #35 Change to real `T` and move it to IVC module level
Expand Down Expand Up @@ -170,6 +171,7 @@ pub(crate) trait StepCircuitExt<'link, const ARITY: usize, C: CurveAffine>:
StepCircuit<ARITY, C::Scalar> + Sized
where
<C as CurveAffine>::Base: ff::PrimeFieldBits + ff::FromUniformBytes<64>,
<C as CurveAffine>::ScalarExt: ff::PrimeField,
{
/// The crate-only expanding trait that checks that no instance columns have
/// been created during [`StepCircuit::configure`].
Expand Down Expand Up @@ -198,16 +200,40 @@ where
input: StepInputs<ARITY, C, RO>,
) -> Result<[AssignedCell<C::Scalar, C::Scalar>; ARITY], SynthesisError> {
// Synthesize the circuit for the base case and get the new running instance
let _U_new_base = self.synthesize_step_base_case(
let U_new_base = self.synthesize_step_base_case(
layouter,
input.public_params,
input.u.as_ref(),
input.step_public_params,
&input.u,
config.main_gate_config.clone(),
)?;

// Synthesize the circuit for the non-base case and get the new running
// instance along with a boolean indicating if all checks have passed
let _U_new_non_base = self.synthesize_step_non_base_case(&config, layouter, input)?;
let U_new_non_base = self.synthesize_step_non_base_case(&config, layouter, &input)?;

let _new_U = layouter.assign_region(
|| "choose case",
move |region| {
let mut region = RegionCtx::new(region, 0);
let gate = MainGate::new(config.main_gate_config.clone());

let assigned_step = region.assign_advice(
|| "step",
config.main_gate_config.input,
Value::known(input.step),
)?;

let assigned_is_zero_step = gate.is_zero_term(&mut region, assigned_step)?;

Ok(AssignedRelaxedPlonkInstance::<C>::conditional_select(
&mut region,
&config.main_gate_config,
&U_new_non_base,
&U_new_base,
assigned_is_zero_step,
)?)
},
)?;

todo!("#32")
}
Expand All @@ -216,11 +242,9 @@ where
&self,
layouter: &mut impl Layouter<C::Base>,
public_params: &SynthesizeStepParams<C, RO>,
u: Option<&PlonkInstance<C>>,
u: &PlonkInstance<C>,
config: MainGateConfig,
) -> Result<AssignedRelaxedPlonkInstance<C>, SynthesisError> {
let u = u.cloned().unwrap_or_default();

let Unew_base = layouter.assign_region(
|| "synthesize_step_base_case",
move |region| {
Expand Down Expand Up @@ -252,35 +276,42 @@ where
&self,
config: &StepConfig<ARITY, C, Self>,
layouter: &mut impl Layouter<C::Base>,
input: StepInputs<ARITY, C, RO>,
) -> Result<FoldRelaxedPlonkInstanceChip<MAIN_GATE_CONFIG_SIZE, C>, SynthesisError> {
// TODO Check hash of params

let U = input
.U
.unwrap_or_else(|| todo!("understand what we should use in that case"));

let _Unew_base: FoldRelaxedPlonkInstanceChip<MAIN_GATE_CONFIG_SIZE, C> = layouter
.assign_region(
|| "synthesize_step_non_base_case",
move |_region| {
let _U = FoldRelaxedPlonkInstanceChip::from_relaxed(
U.clone(),
input.public_params.limb_width,
input.public_params.n_limbs,
config.main_gate_config.clone(),
);

let _ro_circuit = RO::new(
config.main_gate_config.clone(),
input.public_params.ro_constant.clone(),
);

todo!()
},
)?;
input: &StepInputs<ARITY, C, RO>,
) -> Result<AssignedRelaxedPlonkInstance<C>, SynthesisError> {
let StepInputs {
U,
u,
cross_term_commits,
public_params_hash,
..
} = input;

let (_chip, assigned_U_new_base) = layouter.assign_region(
|| "synthesize_step_non_base_case",
move |region| {
let chip = FoldRelaxedPlonkInstanceChip::from_relaxed(
U.clone(),
input.step_public_params.limb_width,
input.step_public_params.n_limbs,
config.main_gate_config.clone(),
);

let ro_circuit = RO::new(
config.main_gate_config.clone(),
input.step_public_params.ro_constant.clone(),
);

Ok(chip.fold(
&mut RegionCtx::new(region, 0),
ro_circuit,
public_params_hash,
u,
cross_term_commits,
)?)
},
)?;

todo!("#32")
Ok(assigned_U_new_base)
}
}

Expand Down

0 comments on commit 07555c7

Please sign in to comment.