|
|
@ -1,40 +1,49 @@ |
|
|
|
/// contains [Nova](https://eprint.iacr.org/2021/370.pdf) related circuits
|
|
|
|
use ark_crypto_primitives::crh::{
|
|
|
|
poseidon::constraints::{CRHGadget, CRHParametersVar},
|
|
|
|
poseidon::CRH,
|
|
|
|
CRHScheme, CRHSchemeGadget,
|
|
|
|
CRHSchemeGadget,
|
|
|
|
};
|
|
|
|
use ark_crypto_primitives::sponge::{
|
|
|
|
constraints::CryptographicSpongeVar,
|
|
|
|
poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge},
|
|
|
|
Absorb, CryptographicSponge,
|
|
|
|
};
|
|
|
|
use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
|
|
|
|
use ark_ec::{AffineRepr, CurveGroup, Group};
|
|
|
|
use ark_ff::{Field, PrimeField};
|
|
|
|
use ark_r1cs_std::{
|
|
|
|
alloc::{AllocVar, AllocationMode},
|
|
|
|
boolean::Boolean,
|
|
|
|
eq::EqGadget,
|
|
|
|
fields::{fp::FpVar, FieldVar},
|
|
|
|
fields::{fp::FpVar, nonnative::NonNativeFieldVar, FieldVar},
|
|
|
|
groups::GroupOpsBounds,
|
|
|
|
prelude::CurveVar,
|
|
|
|
ToBitsGadget, ToConstraintFieldGadget,
|
|
|
|
};
|
|
|
|
use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
|
|
|
|
use ark_std::fmt::Debug;
|
|
|
|
use ark_std::Zero;
|
|
|
|
use ark_std::{One, Zero};
|
|
|
|
use core::{borrow::Borrow, marker::PhantomData};
|
|
|
|
|
|
|
|
use super::CommittedInstance;
|
|
|
|
use crate::folding::circuits::{
|
|
|
|
cyclefold::ECRLC,
|
|
|
|
nonnative::{point_to_nonnative_limbs, NonNativeAffineVar},
|
|
|
|
use super::{
|
|
|
|
cyclefold::{
|
|
|
|
CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
|
|
|
|
},
|
|
|
|
CommittedInstance,
|
|
|
|
};
|
|
|
|
use crate::constants::N_BITS_RO;
|
|
|
|
use crate::folding::circuits::nonnative::{point_to_nonnative_limbs, NonNativeAffineVar};
|
|
|
|
|
|
|
|
/// CF1 represents the ConstraintField used for the main Nova circuit which is over E1::Fr, where
|
|
|
|
/// E1 is the main curve where we do the folding.
|
|
|
|
pub type CF1<C> = <<C as CurveGroup>::Affine as AffineRepr>::ScalarField;
|
|
|
|
/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq,
|
|
|
|
/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf)
|
|
|
|
/// approach) where we check the folding of the commitments.
|
|
|
|
/// approach) where we check the folding of the commitments (elliptic curve points).
|
|
|
|
pub type CF2<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
|
|
|
|
|
|
|
|
/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
|
|
|
|
/// constraints field (E1::Fr, where E1 is the main curve).
|
|
|
|
/// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are
|
|
|
|
/// represented non-natively over the constraint field.
|
|
|
|
#[derive(Debug, Clone)]
|
|
|
|
pub struct CommittedInstanceVar<C: CurveGroup> {
|
|
|
|
u: FpVar<C::ScalarField>,
|
|
|
@ -108,43 +117,6 @@ where |
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/// CommittedInstanceCycleFoldVar represents the commitments to E and W from the CommittedInstance
|
|
|
|
/// on the E2, which are folded on the auxiliary curve constraints field (E2::Fr = E1::Fq).
|
|
|
|
pub struct CommittedInstanceCycleFoldVar<C: CurveGroup, GC: CurveVar<C, CF2<C>>>
|
|
|
|
where
|
|
|
|
for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
|
|
|
|
{
|
|
|
|
_c: PhantomData<C>,
|
|
|
|
cmE: GC,
|
|
|
|
cmW: GC,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C, GC> AllocVar<CommittedInstance<C>, CF2<C>> for CommittedInstanceCycleFoldVar<C, GC>
|
|
|
|
where
|
|
|
|
C: CurveGroup,
|
|
|
|
GC: CurveVar<C, CF2<C>>,
|
|
|
|
for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
|
|
|
|
{
|
|
|
|
fn new_variable<T: Borrow<CommittedInstance<C>>>(
|
|
|
|
cs: impl Into<Namespace<CF2<C>>>,
|
|
|
|
f: impl FnOnce() -> Result<T, SynthesisError>,
|
|
|
|
mode: AllocationMode,
|
|
|
|
) -> Result<Self, SynthesisError> {
|
|
|
|
f().and_then(|val| {
|
|
|
|
let cs = cs.into();
|
|
|
|
|
|
|
|
let cmE = GC::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
|
|
|
|
let cmW = GC::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
|
|
|
|
|
|
|
|
Ok(Self {
|
|
|
|
_c: PhantomData,
|
|
|
|
cmE,
|
|
|
|
cmW,
|
|
|
|
})
|
|
|
|
})
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
|
|
|
|
/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
|
|
|
|
/// delegated to the NIFSCycleFoldGadget.
|
|
|
@ -180,96 +152,12 @@ where |
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/// NIFSCycleFoldGadget performs the Nova NIFS.V elliptic curve points relation checks in the other
|
|
|
|
/// curve following [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
|
|
|
|
pub struct NIFSCycleFoldGadget<C: CurveGroup, GC: CurveVar<C, CF2<C>>> {
|
|
|
|
/// ChallengeGadget computes the RO challenge used for the Nova instances NIFS, it contains a
|
|
|
|
/// rust-native and a in-circuit compatible versions.
|
|
|
|
pub struct ChallengeGadget<C: CurveGroup> {
|
|
|
|
_c: PhantomData<C>,
|
|
|
|
_gc: PhantomData<GC>,
|
|
|
|
}
|
|
|
|
impl<C: CurveGroup, GC: CurveVar<C, CF2<C>>> NIFSCycleFoldGadget<C, GC>
|
|
|
|
where
|
|
|
|
C: CurveGroup,
|
|
|
|
GC: CurveVar<C, CF2<C>>,
|
|
|
|
for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
|
|
|
|
{
|
|
|
|
pub fn verify(
|
|
|
|
r_bits: Vec<Boolean<CF2<C>>>,
|
|
|
|
cmT: GC,
|
|
|
|
ci1: CommittedInstanceCycleFoldVar<C, GC>,
|
|
|
|
ci2: CommittedInstanceCycleFoldVar<C, GC>,
|
|
|
|
ci3: CommittedInstanceCycleFoldVar<C, GC>,
|
|
|
|
) -> Result<Boolean<CF2<C>>, SynthesisError> {
|
|
|
|
// cm(E) check: ci3.cmE == ci1.cmE + r * cmT + r^2 * ci2.cmE
|
|
|
|
let first_check = ci3.cmE.is_eq(
|
|
|
|
&((ci2.cmE.scalar_mul_le(r_bits.iter())? + cmT).scalar_mul_le(r_bits.iter())?
|
|
|
|
+ ci1.cmE),
|
|
|
|
)?;
|
|
|
|
// cm(W) check: ci3.cmW == ci1.cmW + r * ci2.cmW
|
|
|
|
let second_check = ECRLC::<C, GC>::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?;
|
|
|
|
|
|
|
|
first_check.and(&second_check)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/// FCircuit defines the trait of the circuit of the F function, which is the one being executed
|
|
|
|
/// inside the agmented F' function.
|
|
|
|
pub trait FCircuit<F: PrimeField>: Clone + Copy + Debug {
|
|
|
|
/// returns a new FCircuit instance
|
|
|
|
fn new() -> Self;
|
|
|
|
|
|
|
|
/// computes the next state values in place, assigning z_{i+1} into z_i, and
|
|
|
|
/// computing the new z_i
|
|
|
|
fn step_native(
|
|
|
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
|
|
|
// can hold a state if needed to store data to compute the next state.
|
|
|
|
self,
|
|
|
|
z_i: Vec<F>,
|
|
|
|
) -> Vec<F>;
|
|
|
|
|
|
|
|
/// generates the constraints for the step of F for the given z_i
|
|
|
|
fn generate_step_constraints(
|
|
|
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
|
|
|
// can hold a state if needed to store data to generate the constraints.
|
|
|
|
self,
|
|
|
|
cs: ConstraintSystemRef<F>,
|
|
|
|
z_i: Vec<FpVar<F>>,
|
|
|
|
) -> Result<Vec<FpVar<F>>, SynthesisError>;
|
|
|
|
}
|
|
|
|
|
|
|
|
/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
|
|
|
|
/// [Nova](https://eprint.iacr.org/2021/370.pdf).
|
|
|
|
#[derive(Debug, Clone)]
|
|
|
|
pub struct AugmentedFCircuit<C: CurveGroup, FC: FCircuit<CF1<C>>> {
|
|
|
|
pub poseidon_config: PoseidonConfig<CF1<C>>,
|
|
|
|
pub i: Option<CF1<C>>,
|
|
|
|
pub z_0: Option<Vec<C::ScalarField>>,
|
|
|
|
pub z_i: Option<Vec<C::ScalarField>>,
|
|
|
|
pub u_i: Option<CommittedInstance<C>>,
|
|
|
|
pub U_i: Option<CommittedInstance<C>>,
|
|
|
|
pub U_i1: Option<CommittedInstance<C>>,
|
|
|
|
pub cmT: Option<C>,
|
|
|
|
pub F: FC, // F circuit
|
|
|
|
pub x: Option<CF1<C>>, // public inputs (u_{i+1}.x)
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C: CurveGroup, FC: FCircuit<CF1<C>>> AugmentedFCircuit<C, FC> {
|
|
|
|
pub fn empty(poseidon_config: &PoseidonConfig<CF1<C>>, F_circuit: FC) -> Self {
|
|
|
|
Self {
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: None,
|
|
|
|
z_0: None,
|
|
|
|
z_i: None,
|
|
|
|
u_i: None,
|
|
|
|
U_i: None,
|
|
|
|
U_i1: None,
|
|
|
|
cmT: None,
|
|
|
|
F: F_circuit,
|
|
|
|
x: None,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C: CurveGroup, FC: FCircuit<CF1<C>>> AugmentedFCircuit<C, FC>
|
|
|
|
impl<C: CurveGroup> ChallengeGadget<C>
|
|
|
|
where
|
|
|
|
C: CurveGroup,
|
|
|
|
<C as CurveGroup>::BaseField: PrimeField,
|
|
|
@ -280,13 +168,14 @@ where |
|
|
|
u_i: CommittedInstance<C>,
|
|
|
|
U_i: CommittedInstance<C>,
|
|
|
|
cmT: C,
|
|
|
|
) -> Result<C::ScalarField, SynthesisError> {
|
|
|
|
) -> Result<Vec<bool>, SynthesisError> {
|
|
|
|
let (u_cmE_x, u_cmE_y) = point_to_nonnative_limbs::<C>(u_i.cmE)?;
|
|
|
|
let (u_cmW_x, u_cmW_y) = point_to_nonnative_limbs::<C>(u_i.cmW)?;
|
|
|
|
let (U_cmE_x, U_cmE_y) = point_to_nonnative_limbs::<C>(U_i.cmE)?;
|
|
|
|
let (U_cmW_x, U_cmW_y) = point_to_nonnative_limbs::<C>(U_i.cmW)?;
|
|
|
|
let (cmT_x, cmT_y) = point_to_nonnative_limbs::<C>(cmT)?;
|
|
|
|
|
|
|
|
let mut sponge = PoseidonSponge::<C::ScalarField>::new(poseidon_config);
|
|
|
|
let input = vec![
|
|
|
|
vec![u_i.u],
|
|
|
|
u_i.x.clone(),
|
|
|
@ -304,16 +193,22 @@ where |
|
|
|
cmT_y,
|
|
|
|
]
|
|
|
|
.concat();
|
|
|
|
Ok(CRH::<C::ScalarField>::evaluate(poseidon_config, input).unwrap())
|
|
|
|
sponge.absorb(&input);
|
|
|
|
let bits = sponge.squeeze_bits(N_BITS_RO);
|
|
|
|
Ok(bits)
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn get_challenge(
|
|
|
|
crh_params: &CRHParametersVar<C::ScalarField>,
|
|
|
|
// compatible with the native get_challenge_native
|
|
|
|
pub fn get_challenge_gadget(
|
|
|
|
cs: ConstraintSystemRef<C::ScalarField>,
|
|
|
|
poseidon_config: &PoseidonConfig<C::ScalarField>,
|
|
|
|
u_i: CommittedInstanceVar<C>,
|
|
|
|
U_i: CommittedInstanceVar<C>,
|
|
|
|
cmT: NonNativeAffineVar<C::ScalarField>,
|
|
|
|
) -> Result<FpVar<C::ScalarField>, SynthesisError> {
|
|
|
|
let input = vec![
|
|
|
|
) -> Result<Vec<Boolean<C::ScalarField>>, SynthesisError> {
|
|
|
|
let mut sponge = PoseidonSpongeVar::<C::ScalarField>::new(cs, poseidon_config);
|
|
|
|
|
|
|
|
let input: Vec<FpVar<C::ScalarField>> = vec![
|
|
|
|
vec![u_i.u.clone()],
|
|
|
|
u_i.x.clone(),
|
|
|
|
u_i.cmE.x,
|
|
|
@ -330,55 +225,148 @@ where |
|
|
|
cmT.y,
|
|
|
|
]
|
|
|
|
.concat();
|
|
|
|
CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)
|
|
|
|
sponge.absorb(&input)?;
|
|
|
|
let bits = sponge.squeeze_bits(N_BITS_RO)?;
|
|
|
|
Ok(bits)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C: CurveGroup, FC: FCircuit<CF1<C>>> ConstraintSynthesizer<CF1<C>> for AugmentedFCircuit<C, FC>
|
|
|
|
/// FCircuit defines the trait of the circuit of the F function, which is the one being executed
|
|
|
|
/// inside the agmented F' function.
|
|
|
|
pub trait FCircuit<F: PrimeField>: Clone + Copy + Debug {
|
|
|
|
/// returns a new FCircuit instance
|
|
|
|
fn new() -> Self;
|
|
|
|
|
|
|
|
/// computes the next state values in place, assigning z_{i+1} into z_i, and
|
|
|
|
/// computing the new z_i
|
|
|
|
fn step_native(
|
|
|
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
|
|
|
// can hold a state if needed to store data to compute the next state.
|
|
|
|
self,
|
|
|
|
z_i: Vec<F>,
|
|
|
|
) -> Vec<F>;
|
|
|
|
|
|
|
|
/// generates the constraints for the step of F for the given z_i
|
|
|
|
fn generate_step_constraints(
|
|
|
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
|
|
|
// can hold a state if needed to store data to generate the constraints.
|
|
|
|
self,
|
|
|
|
cs: ConstraintSystemRef<F>,
|
|
|
|
z_i: Vec<FpVar<F>>,
|
|
|
|
) -> Result<Vec<FpVar<F>>, SynthesisError>;
|
|
|
|
}
|
|
|
|
|
|
|
|
/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
|
|
|
|
/// [Nova](https://eprint.iacr.org/2021/370.pdf) together with the extra constraints defined in
|
|
|
|
/// [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
|
|
|
|
#[derive(Debug, Clone)]
|
|
|
|
pub struct AugmentedFCircuit<
|
|
|
|
C1: CurveGroup,
|
|
|
|
C2: CurveGroup,
|
|
|
|
GC2: CurveVar<C2, CF2<C2>>,
|
|
|
|
FC: FCircuit<CF1<C1>>,
|
|
|
|
> where
|
|
|
|
for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
|
|
|
|
{
|
|
|
|
pub _gc2: PhantomData<GC2>,
|
|
|
|
pub poseidon_config: PoseidonConfig<CF1<C1>>,
|
|
|
|
pub i: Option<CF1<C1>>,
|
|
|
|
pub z_0: Option<Vec<C1::ScalarField>>,
|
|
|
|
pub z_i: Option<Vec<C1::ScalarField>>,
|
|
|
|
pub u_i: Option<CommittedInstance<C1>>,
|
|
|
|
pub U_i: Option<CommittedInstance<C1>>,
|
|
|
|
pub U_i1: Option<CommittedInstance<C1>>,
|
|
|
|
pub cmT: Option<C1>,
|
|
|
|
pub F: FC, // F circuit
|
|
|
|
pub x: Option<CF1<C1>>, // public inputs (u_{i+1}.x)
|
|
|
|
|
|
|
|
// cyclefold verifier on C1
|
|
|
|
pub cf_u_i: Option<CommittedInstance<C2>>,
|
|
|
|
pub cf_U_i: Option<CommittedInstance<C2>>,
|
|
|
|
pub cf_U_i1: Option<CommittedInstance<C2>>,
|
|
|
|
pub cf_cmT: Option<C2>,
|
|
|
|
pub cf_r_nonnat: Option<C2::ScalarField>,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
|
|
|
|
AugmentedFCircuit<C1, C2, GC2, FC>
|
|
|
|
where
|
|
|
|
C: CurveGroup,
|
|
|
|
<C as CurveGroup>::BaseField: PrimeField,
|
|
|
|
<C as Group>::ScalarField: Absorb,
|
|
|
|
for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
|
|
|
|
{
|
|
|
|
fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C>>) -> Result<(), SynthesisError> {
|
|
|
|
let i =
|
|
|
|
FpVar::<CF1<C>>::new_witness(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C>::zero)))?;
|
|
|
|
let z_0 = Vec::<FpVar<CF1<C>>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.z_0.unwrap_or_else(|| vec![CF1::<C>::zero()]))
|
|
|
|
pub fn empty(poseidon_config: &PoseidonConfig<CF1<C1>>, F_circuit: FC) -> Self {
|
|
|
|
Self {
|
|
|
|
_gc2: PhantomData,
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: None,
|
|
|
|
z_0: None,
|
|
|
|
z_i: None,
|
|
|
|
u_i: None,
|
|
|
|
U_i: None,
|
|
|
|
U_i1: None,
|
|
|
|
cmT: None,
|
|
|
|
F: F_circuit,
|
|
|
|
x: None,
|
|
|
|
// cyclefold values
|
|
|
|
cf_u_i: None,
|
|
|
|
cf_U_i: None,
|
|
|
|
cf_U_i1: None,
|
|
|
|
cf_cmT: None,
|
|
|
|
cf_r_nonnat: None,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
|
|
|
|
where
|
|
|
|
C1: CurveGroup,
|
|
|
|
C2: CurveGroup,
|
|
|
|
GC2: CurveVar<C2, CF2<C2>>,
|
|
|
|
FC: FCircuit<CF1<C1>>,
|
|
|
|
<C1 as CurveGroup>::BaseField: PrimeField,
|
|
|
|
<C2 as CurveGroup>::BaseField: PrimeField,
|
|
|
|
<C1 as Group>::ScalarField: Absorb,
|
|
|
|
<C2 as Group>::ScalarField: Absorb,
|
|
|
|
C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
|
|
|
|
for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
|
|
|
|
{
|
|
|
|
fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
|
|
|
|
let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
|
|
|
|
})?;
|
|
|
|
let z_i = Vec::<FpVar<CF1<C>>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.z_i.unwrap_or_else(|| vec![CF1::<C>::zero()]))
|
|
|
|
let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
|
|
|
|
})?;
|
|
|
|
let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
|
|
|
|
})?;
|
|
|
|
|
|
|
|
let u_dummy_native = CommittedInstance::<C>::dummy(1);
|
|
|
|
|
|
|
|
let u_dummy =
|
|
|
|
CommittedInstanceVar::<C>::new_witness(cs.clone(), || Ok(u_dummy_native.clone()))?;
|
|
|
|
let u_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.u_i.unwrap_or_else(|| u_dummy_native.clone()))
|
|
|
|
let u_dummy_native = CommittedInstance::<C1>::dummy(1);
|
|
|
|
let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let U_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.U_i.unwrap_or_else(|| u_dummy_native.clone()))
|
|
|
|
let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.U_i.unwrap_or(u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let U_i1 = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.U_i1.unwrap_or_else(|| u_dummy_native.clone()))
|
|
|
|
let U_i1 = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.U_i1.unwrap_or(u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let cmT =
|
|
|
|
NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C::zero)))?;
|
|
|
|
NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
|
|
|
|
let x =
|
|
|
|
FpVar::<CF1<C>>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::<C>::zero)))?;
|
|
|
|
FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::<C1>::zero)))?;
|
|
|
|
|
|
|
|
let crh_params =
|
|
|
|
CRHParametersVar::<C::ScalarField>::new_constant(cs.clone(), self.poseidon_config)?;
|
|
|
|
let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
|
|
|
|
cs.clone(),
|
|
|
|
self.poseidon_config.clone(),
|
|
|
|
)?;
|
|
|
|
|
|
|
|
// get z_{i+1} from the F circuit
|
|
|
|
let z_i1 = self.F.generate_step_constraints(cs.clone(), z_i.clone())?;
|
|
|
|
|
|
|
|
let zero = FpVar::<CF1<C>>::new_constant(cs.clone(), CF1::<C>::zero())?;
|
|
|
|
let is_basecase = i.is_eq(&zero)?;
|
|
|
|
let zero = FpVar::<CF1<C1>>::new_constant(cs.clone(), CF1::<C1>::zero())?;
|
|
|
|
let is_not_basecase = i.is_neq(&zero)?;
|
|
|
|
|
|
|
|
// 1. h_{i+1} = u_i.X == H(i, z_0, z_i, U_i)
|
|
|
|
// 1. u_i.x == H(i, z_0, z_i, U_i)
|
|
|
|
let u_i_x = U_i
|
|
|
|
.clone()
|
|
|
|
.hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
|
|
|
@ -387,41 +375,107 @@ where |
|
|
|
(u_i.x[0]).conditional_enforce_equal(&u_i_x, &is_not_basecase)?;
|
|
|
|
|
|
|
|
// 2. u_i.cmE==cm(0), u_i.u==1
|
|
|
|
(u_i.cmE.x.is_eq(&u_dummy.cmE.x)?)
|
|
|
|
.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
(u_i.cmE.y.is_eq(&u_dummy.cmE.y)?)
|
|
|
|
.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
let zero_x = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
|
|
|
|
cs.clone(),
|
|
|
|
C1::BaseField::zero(),
|
|
|
|
)?
|
|
|
|
.to_constraint_field()?;
|
|
|
|
let zero_y = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
|
|
|
|
cs.clone(),
|
|
|
|
C1::BaseField::one(),
|
|
|
|
)?
|
|
|
|
.to_constraint_field()?;
|
|
|
|
(u_i.cmE.x.is_eq(&zero_x)?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
(u_i.cmE.y.is_eq(&zero_y)?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
(u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
|
|
|
|
// 3. nifs.verify, checks that folding u_i & U_i obtains U_{i+1}.
|
|
|
|
// compute r = H(u_i, U_i, cmT)
|
|
|
|
let r = Self::get_challenge(&crh_params, u_i.clone(), U_i.clone(), cmT)?;
|
|
|
|
let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
|
|
|
|
cs.clone(),
|
|
|
|
&self.poseidon_config,
|
|
|
|
u_i.clone(),
|
|
|
|
U_i.clone(),
|
|
|
|
cmT.clone(),
|
|
|
|
)?;
|
|
|
|
let r = Boolean::le_bits_to_fp_var(&r_bits)?;
|
|
|
|
|
|
|
|
// Notice that NIFSGadget::verify is not checking the folding of cmE & cmW, since it will
|
|
|
|
// be done on the other curve.
|
|
|
|
let nifs_check = NIFSGadget::<C>::verify(r, u_i, U_i.clone(), U_i1.clone())?;
|
|
|
|
let nifs_check = NIFSGadget::<C1>::verify(r, u_i.clone(), U_i.clone(), U_i1.clone())?;
|
|
|
|
nifs_check.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
|
|
|
|
// 4. (base case) u_{i+1}.X == H(1, z_0, F(z_0)=F(z_i)=z_i1, U_i) (with U_i being dummy)
|
|
|
|
let u_i1_x_basecase = U_i.hash(
|
|
|
|
// 4. u_{i+1}.x = H(i+1, z_0, z_i+1, U_{i+1}), this is the output of F'
|
|
|
|
let u_i1_x = U_i1.clone().hash(
|
|
|
|
&crh_params,
|
|
|
|
FpVar::<CF1<C>>::one(),
|
|
|
|
i + FpVar::<CF1<C1>>::one(),
|
|
|
|
z_0.clone(),
|
|
|
|
z_i1.clone(),
|
|
|
|
)?;
|
|
|
|
|
|
|
|
// 4. (non-base case). u_{i+1}.x = H(i+1, z_0, z_i+1, U_{i+1}), this is the output of F'
|
|
|
|
let u_i1_x = U_i1.hash(
|
|
|
|
&crh_params,
|
|
|
|
i + FpVar::<CF1<C>>::one(),
|
|
|
|
z_0.clone(),
|
|
|
|
z_i1.clone(),
|
|
|
|
)?;
|
|
|
|
u_i1_x.enforce_equal(&x)?;
|
|
|
|
|
|
|
|
// CycleFold part
|
|
|
|
let cf_u_dummy_native = CommittedInstance::<C2>::dummy(CF_IO_LEN);
|
|
|
|
let cf_u_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.cf_u_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let cf_U_i1 = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.cf_U_i1.unwrap_or_else(|| cf_u_dummy_native.clone()))
|
|
|
|
})?;
|
|
|
|
let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
|
|
|
|
// cf_r_nonnat is an auxiliary input
|
|
|
|
let cf_r_nonnat =
|
|
|
|
NonNativeFieldVar::<C2::ScalarField, CF2<C2>>::new_witness(cs.clone(), || {
|
|
|
|
Ok(self.cf_r_nonnat.unwrap_or_else(C2::ScalarField::zero))
|
|
|
|
})?;
|
|
|
|
|
|
|
|
// check that cf_u_i.x == [u_i, U_i, U_{i+1}]
|
|
|
|
let incircuit_x = vec![
|
|
|
|
u_i.cmE.x, u_i.cmE.y, u_i.cmW.x, u_i.cmW.y, U_i.cmE.x, U_i.cmE.y, U_i.cmW.x, U_i.cmW.y,
|
|
|
|
U_i1.cmE.x, U_i1.cmE.y, U_i1.cmW.x, U_i1.cmW.y,
|
|
|
|
]
|
|
|
|
.concat();
|
|
|
|
|
|
|
|
// if i==0: check x==u_{i+1}.x_basecase
|
|
|
|
u_i1_x_basecase.conditional_enforce_equal(&x, &is_basecase)?;
|
|
|
|
// else: check x==u_{i+1}.x
|
|
|
|
u_i1_x.conditional_enforce_equal(&x, &is_not_basecase)?;
|
|
|
|
let mut cf_u_i_x: Vec<FpVar<CF2<C2>>> = vec![];
|
|
|
|
for x_i in cf_u_i.x.iter() {
|
|
|
|
let mut x_fpvar = x_i.to_constraint_field()?;
|
|
|
|
cf_u_i_x.append(&mut x_fpvar);
|
|
|
|
}
|
|
|
|
cf_u_i_x.conditional_enforce_equal(&incircuit_x, &is_not_basecase)?;
|
|
|
|
|
|
|
|
// cf_r_bits is denoted by rho* in the paper
|
|
|
|
let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
|
|
|
|
cs.clone(),
|
|
|
|
&self.poseidon_config,
|
|
|
|
cf_u_i.clone(),
|
|
|
|
cf_U_i.clone(),
|
|
|
|
cf_cmT.clone(),
|
|
|
|
)?;
|
|
|
|
// assert that cf_r_bits == cf_r_nonnat converted to bits. cf_r_nonnat is just an auxiliary
|
|
|
|
// value used to compute RLC of NonNativeFieldVar values, since we can convert
|
|
|
|
// NonNativeFieldVar into Vec<Boolean>, but not in the other direction.
|
|
|
|
let cf_r_nonnat_bits = cf_r_nonnat.to_bits_le()?;
|
|
|
|
cf_r_bits.conditional_enforce_equal(&cf_r_nonnat_bits[..N_BITS_RO], &is_not_basecase)?;
|
|
|
|
|
|
|
|
// check cf_u_i.cmE=0, cf_u_i.u=1
|
|
|
|
(cf_u_i.cmE.is_zero()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
(cf_u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
|
|
|
|
// check the fold of all the parameteres of the CycleFold instances, where the elliptic
|
|
|
|
// curve points relations are checked natively in Curve1 circuit (this one)
|
|
|
|
let v = NIFSFullGadget::<C2, GC2>::verify(
|
|
|
|
cf_r_bits,
|
|
|
|
cf_r_nonnat,
|
|
|
|
cf_cmT,
|
|
|
|
cf_U_i,
|
|
|
|
cf_u_i,
|
|
|
|
cf_U_i1,
|
|
|
|
)?;
|
|
|
|
v.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
|
|
|
|
|
|
|
|
Ok(())
|
|
|
|
}
|
|
|
@ -431,19 +485,21 @@ where |
|
|
|
pub mod tests {
|
|
|
|
use super::*;
|
|
|
|
use ark_ff::BigInteger;
|
|
|
|
use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
|
|
|
|
use ark_pallas::{Fq, Fr, Projective};
|
|
|
|
use ark_r1cs_std::{alloc::AllocVar, R1CSVar};
|
|
|
|
use ark_relations::r1cs::{ConstraintLayer, ConstraintSystem, TracingMode};
|
|
|
|
use ark_std::One;
|
|
|
|
use ark_std::UniformRand;
|
|
|
|
use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
|
|
|
|
use tracing_subscriber::layer::SubscriberExt;
|
|
|
|
|
|
|
|
use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
|
|
|
|
use crate::folding::nova::{nifs::NIFS, traits::NovaR1CS, Witness};
|
|
|
|
use crate::folding::nova::nifs::tests::prepare_simple_fold_inputs;
|
|
|
|
use crate::folding::nova::{
|
|
|
|
ivc::get_committed_instance_coordinates, nifs::NIFS, traits::NovaR1CS, Witness,
|
|
|
|
};
|
|
|
|
use crate::frontend::arkworks::{extract_r1cs, extract_z};
|
|
|
|
use crate::pedersen::Pedersen;
|
|
|
|
use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript};
|
|
|
|
use crate::transcript::Transcript;
|
|
|
|
use crate::transcript::poseidon::tests::poseidon_test_config;
|
|
|
|
|
|
|
|
#[derive(Clone, Copy, Debug)]
|
|
|
|
/// TestFCircuit is a variation of `x^3 + x + 5 = y` (as in
|
|
|
@ -488,49 +544,14 @@ pub mod tests { |
|
|
|
CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
|
|
|
|
assert_eq!(ciVar.u.value().unwrap(), ci.u);
|
|
|
|
assert_eq!(ciVar.x.value().unwrap(), ci.x);
|
|
|
|
|
|
|
|
// check the instantiation of the CycleFold side:
|
|
|
|
let cs = ConstraintSystem::<Fq>::new_ref();
|
|
|
|
let ciVar =
|
|
|
|
CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs.clone(), || {
|
|
|
|
Ok(ci.clone())
|
|
|
|
})
|
|
|
|
.unwrap();
|
|
|
|
assert_eq!(ciVar.cmE.value().unwrap(), ci.cmE);
|
|
|
|
assert_eq!(ciVar.cmW.value().unwrap(), ci.cmW);
|
|
|
|
// the values cmE and cmW are checked in the CycleFold's circuit
|
|
|
|
// CommittedInstanceInCycleFoldVar in
|
|
|
|
// nova::cyclefold::tests::test_committed_instance_cyclefold_var
|
|
|
|
}
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
fn test_nifs_gadget() {
|
|
|
|
let r1cs = get_test_r1cs();
|
|
|
|
let z1 = get_test_z(3);
|
|
|
|
let z2 = get_test_z(4);
|
|
|
|
let (w1, x1) = r1cs.split_z(&z1);
|
|
|
|
let (w2, x2) = r1cs.split_z(&z2);
|
|
|
|
|
|
|
|
let w1 = Witness::<Projective>::new(w1.clone(), r1cs.A.n_rows);
|
|
|
|
let w2 = Witness::<Projective>::new(w2.clone(), r1cs.A.n_rows);
|
|
|
|
|
|
|
|
let mut rng = ark_std::test_rng();
|
|
|
|
let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_rows);
|
|
|
|
|
|
|
|
// compute committed instances
|
|
|
|
let ci1 = w1.commit(&pedersen_params, x1.clone()).unwrap();
|
|
|
|
let ci2 = w2.commit(&pedersen_params, x2.clone()).unwrap();
|
|
|
|
|
|
|
|
// NIFS.P
|
|
|
|
let (T, cmT) =
|
|
|
|
NIFS::<Projective>::compute_cmT(&pedersen_params, &r1cs, &w1, &ci1, &w2, &ci2).unwrap();
|
|
|
|
|
|
|
|
// get challenge from transcript, since we're in a test skip absorbing values into
|
|
|
|
// transcript
|
|
|
|
let poseidon_config = poseidon_test_config::<Fr>();
|
|
|
|
let mut tr = PoseidonTranscript::<Projective>::new(&poseidon_config);
|
|
|
|
let r_bits = tr.get_challenge_nbits(128);
|
|
|
|
let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
|
|
|
|
|
|
|
|
let (_, ci3) =
|
|
|
|
NIFS::<Projective>::fold_instances(r_Fr, &w1, &ci1, &w2, &ci2, &T, cmT).unwrap();
|
|
|
|
let (_, _, _, _, ci1, _, ci2, _, ci3, _, cmT, _, r_Fr) = prepare_simple_fold_inputs();
|
|
|
|
|
|
|
|
let ci3_verifier = NIFS::<Projective>::verify(r_Fr, &ci1, &ci2, &cmT);
|
|
|
|
assert_eq!(ci3_verifier, ci3);
|
|
|
@ -557,36 +578,6 @@ pub mod tests { |
|
|
|
.unwrap();
|
|
|
|
nifs_check.enforce_equal(&Boolean::<Fr>::TRUE).unwrap();
|
|
|
|
assert!(cs.is_satisfied().unwrap());
|
|
|
|
|
|
|
|
// cs_CC is the Constraint System on the Curve Cycle auxiliary curve constraints field
|
|
|
|
// (E2::Fr)
|
|
|
|
let cs_CC = ConstraintSystem::<Fq>::new_ref();
|
|
|
|
|
|
|
|
let r_bitsVar = Vec::<Boolean<Fq>>::new_witness(cs_CC.clone(), || Ok(r_bits)).unwrap();
|
|
|
|
|
|
|
|
let cmTVar = GVar::new_witness(cs_CC.clone(), || Ok(cmT)).unwrap();
|
|
|
|
let ci1Var =
|
|
|
|
CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
|
|
|
|
Ok(ci1.clone())
|
|
|
|
})
|
|
|
|
.unwrap();
|
|
|
|
let ci2Var =
|
|
|
|
CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
|
|
|
|
Ok(ci2.clone())
|
|
|
|
})
|
|
|
|
.unwrap();
|
|
|
|
let ci3Var =
|
|
|
|
CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
|
|
|
|
Ok(ci3.clone())
|
|
|
|
})
|
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
let nifs_cf_check = NIFSCycleFoldGadget::<Projective, GVar>::verify(
|
|
|
|
r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var,
|
|
|
|
)
|
|
|
|
.unwrap();
|
|
|
|
nifs_cf_check.enforce_equal(&Boolean::<Fq>::TRUE).unwrap();
|
|
|
|
assert!(cs_CC.is_satisfied().unwrap());
|
|
|
|
}
|
|
|
|
|
|
|
|
#[test]
|
|
|
@ -648,13 +639,14 @@ pub mod tests { |
|
|
|
let cmT = Projective::rand(&mut rng);
|
|
|
|
|
|
|
|
// compute the challenge natively
|
|
|
|
let r = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge_native(
|
|
|
|
let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
|
|
|
|
&poseidon_config,
|
|
|
|
u_i.clone(),
|
|
|
|
U_i.clone(),
|
|
|
|
cmT,
|
|
|
|
)
|
|
|
|
.unwrap();
|
|
|
|
let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
|
|
|
|
|
|
|
|
let cs = ConstraintSystem::<Fr>::new_ref();
|
|
|
|
let u_iVar =
|
|
|
@ -665,11 +657,10 @@ pub mod tests { |
|
|
|
.unwrap();
|
|
|
|
let cmTVar = NonNativeAffineVar::<Fr>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
|
|
|
|
|
|
|
|
let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
|
|
|
|
|
|
|
|
// compute the challenge in-circuit
|
|
|
|
let rVar = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge(
|
|
|
|
&crh_params,
|
|
|
|
let r_bitsVar = ChallengeGadget::<Projective>::get_challenge_gadget(
|
|
|
|
cs.clone(),
|
|
|
|
&poseidon_config,
|
|
|
|
u_iVar,
|
|
|
|
U_iVar,
|
|
|
|
cmTVar,
|
|
|
@ -678,7 +669,9 @@ pub mod tests { |
|
|
|
assert!(cs.is_satisfied().unwrap());
|
|
|
|
|
|
|
|
// check that the natively computed and in-circuit computed hashes match
|
|
|
|
let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
|
|
|
|
assert_eq!(rVar.value().unwrap(), r);
|
|
|
|
assert_eq!(r_bitsVar.value().unwrap(), r_bits);
|
|
|
|
}
|
|
|
|
|
|
|
|
#[test]
|
|
|
@ -699,7 +692,10 @@ pub mod tests { |
|
|
|
// prepare the circuit to obtain its R1CS
|
|
|
|
let F_circuit = TestFCircuit::<Fr>::new();
|
|
|
|
let mut augmented_F_circuit =
|
|
|
|
AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::empty(&poseidon_config, F_circuit);
|
|
|
|
AugmentedFCircuit::<Projective, Projective2, GVar2, TestFCircuit<Fr>>::empty(
|
|
|
|
&poseidon_config,
|
|
|
|
F_circuit,
|
|
|
|
);
|
|
|
|
augmented_F_circuit
|
|
|
|
.generate_constraints(cs.clone())
|
|
|
|
.unwrap();
|
|
|
@ -751,18 +747,26 @@ pub mod tests { |
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
// base case
|
|
|
|
augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: Some(i), // = 0
|
|
|
|
z_0: Some(z_0.clone()), // = z_i=3
|
|
|
|
z_i: Some(z_i.clone()),
|
|
|
|
u_i: Some(u_i.clone()), // = dummy
|
|
|
|
U_i: Some(U_i.clone()), // = dummy
|
|
|
|
U_i1: Some(U_i1.clone()), // = dummy
|
|
|
|
cmT: Some(cmT),
|
|
|
|
F: F_circuit,
|
|
|
|
x: Some(u_i1_x),
|
|
|
|
};
|
|
|
|
augmented_F_circuit =
|
|
|
|
AugmentedFCircuit::<Projective, Projective2, GVar2, TestFCircuit<Fr>> {
|
|
|
|
_gc2: PhantomData,
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: Some(i), // = 0
|
|
|
|
z_0: Some(z_0.clone()), // = z_i=3
|
|
|
|
z_i: Some(z_i.clone()),
|
|
|
|
u_i: Some(u_i.clone()), // = dummy
|
|
|
|
U_i: Some(U_i.clone()), // = dummy
|
|
|
|
U_i1: Some(U_i1.clone()), // = dummy
|
|
|
|
cmT: Some(cmT),
|
|
|
|
F: F_circuit,
|
|
|
|
x: Some(u_i1_x),
|
|
|
|
// cyclefold instances (not tested in this test)
|
|
|
|
cf_u_i: None,
|
|
|
|
cf_U_i: None,
|
|
|
|
cf_U_i1: None,
|
|
|
|
cf_cmT: None,
|
|
|
|
cf_r_nonnat: None,
|
|
|
|
};
|
|
|
|
} else {
|
|
|
|
r1cs.check_relaxed_instance_relation(&w_i, &u_i).unwrap();
|
|
|
|
r1cs.check_relaxed_instance_relation(&W_i, &U_i).unwrap();
|
|
|
@ -780,13 +784,14 @@ pub mod tests { |
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
// get challenge r
|
|
|
|
let r_Fr = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge_native(
|
|
|
|
let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
|
|
|
|
&poseidon_config,
|
|
|
|
u_i.clone(),
|
|
|
|
U_i.clone(),
|
|
|
|
cmT,
|
|
|
|
)
|
|
|
|
.unwrap();
|
|
|
|
let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
|
|
|
|
|
|
|
|
(W_i1, U_i1) =
|
|
|
|
NIFS::<Projective>::fold_instances(r_Fr, &w_i, &u_i, &W_i, &U_i, &T, cmT)
|
|
|
@ -800,18 +805,59 @@ pub mod tests { |
|
|
|
.hash(&poseidon_config, i + Fr::one(), z_0.clone(), z_i1.clone())
|
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: Some(i),
|
|
|
|
z_0: Some(z_0.clone()),
|
|
|
|
z_i: Some(z_i.clone()),
|
|
|
|
u_i: Some(u_i),
|
|
|
|
U_i: Some(U_i.clone()),
|
|
|
|
U_i1: Some(U_i1.clone()),
|
|
|
|
cmT: Some(cmT),
|
|
|
|
F: F_circuit,
|
|
|
|
x: Some(u_i1_x),
|
|
|
|
// set up dummy cyclefold instances just for the sake of this test. Warning, this
|
|
|
|
// is only because we are in a test were we're not testing the cyclefold side of
|
|
|
|
// things.
|
|
|
|
let cf_W_i = Witness::<Projective2>::new(vec![Fq::zero(); 1], 1);
|
|
|
|
let cf_U_i = CommittedInstance::<Projective2>::dummy(CF_IO_LEN);
|
|
|
|
let cf_u_i_x = [
|
|
|
|
get_committed_instance_coordinates(&u_i),
|
|
|
|
get_committed_instance_coordinates(&U_i),
|
|
|
|
get_committed_instance_coordinates(&U_i1),
|
|
|
|
]
|
|
|
|
.concat();
|
|
|
|
let cf_u_i = CommittedInstance::<Projective2> {
|
|
|
|
cmE: cf_U_i.cmE,
|
|
|
|
u: Fq::one(),
|
|
|
|
cmW: cf_U_i.cmW,
|
|
|
|
x: cf_u_i_x,
|
|
|
|
};
|
|
|
|
let cf_w_i = cf_W_i.clone();
|
|
|
|
let (cf_T, cf_cmT): (Vec<Fq>, Projective2) =
|
|
|
|
(vec![Fq::zero(); cf_W_i.E.len()], Projective2::zero());
|
|
|
|
let cf_r_bits =
|
|
|
|
CycleFoldChallengeGadget::<Projective2, GVar2>::get_challenge_native(
|
|
|
|
&poseidon_config,
|
|
|
|
cf_u_i.clone(),
|
|
|
|
cf_U_i.clone(),
|
|
|
|
cf_cmT,
|
|
|
|
)
|
|
|
|
.unwrap();
|
|
|
|
let cf_r_Fq = Fq::from_bigint(BigInteger::from_bits_le(&cf_r_bits)).unwrap();
|
|
|
|
let (_, cf_U_i1) = NIFS::<Projective2>::fold_instances(
|
|
|
|
cf_r_Fq, &cf_W_i, &cf_U_i, &cf_w_i, &cf_u_i, &cf_T, cf_cmT,
|
|
|
|
)
|
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
augmented_F_circuit =
|
|
|
|
AugmentedFCircuit::<Projective, Projective2, GVar2, TestFCircuit<Fr>> {
|
|
|
|
_gc2: PhantomData,
|
|
|
|
poseidon_config: poseidon_config.clone(),
|
|
|
|
i: Some(i),
|
|
|
|
z_0: Some(z_0.clone()),
|
|
|
|
z_i: Some(z_i.clone()),
|
|
|
|
u_i: Some(u_i),
|
|
|
|
U_i: Some(U_i.clone()),
|
|
|
|
U_i1: Some(U_i1.clone()),
|
|
|
|
cmT: Some(cmT),
|
|
|
|
F: F_circuit,
|
|
|
|
x: Some(u_i1_x),
|
|
|
|
cf_u_i: Some(cf_u_i),
|
|
|
|
cf_U_i: Some(cf_U_i),
|
|
|
|
cf_U_i1: Some(cf_U_i1),
|
|
|
|
cf_cmT: Some(cf_cmT),
|
|
|
|
cf_r_nonnat: Some(cf_r_Fq),
|
|
|
|
};
|
|
|
|
}
|
|
|
|
|
|
|
|
let cs = ConstraintSystem::<Fr>::new_ref();
|
|
|
@ -821,7 +867,7 @@ pub mod tests { |
|
|
|
.unwrap();
|
|
|
|
let is_satisfied = cs.is_satisfied().unwrap();
|
|
|
|
if !is_satisfied {
|
|
|
|
println!("{:?}", cs.which_is_unsatisfied());
|
|
|
|
dbg!(cs.which_is_unsatisfied().unwrap());
|
|
|
|
}
|
|
|
|
assert!(is_satisfied);
|
|
|
|
|
|
|
|