@ -3,29 +3,40 @@
use ark_crypto_primitives ::crh ::poseidon ::constraints ::CRHParametersVar ;
use ark_crypto_primitives ::crh ::poseidon ::constraints ::CRHParametersVar ;
use ark_crypto_primitives ::sponge ::{ poseidon ::PoseidonConfig , Absorb } ;
use ark_crypto_primitives ::sponge ::{ poseidon ::PoseidonConfig , Absorb } ;
use ark_ec ::{ CurveGroup , Group } ;
use ark_ec ::{ CurveGroup , Group } ;
use ark_ff ::PrimeField ;
use ark_ff ::{ BigInteger , PrimeField } ;
use ark_poly ::Polynomial ;
use ark_r1cs_std ::{
use ark_r1cs_std ::{
alloc ::{ AllocVar , AllocationMode } ,
alloc ::{ AllocVar , AllocationMode } ,
boolean ::Boolean ,
boolean ::Boolean ,
eq ::EqGadget ,
eq ::EqGadget ,
fields ::{ fp ::FpVar , nonnative ::NonNativeFieldVar , FieldVar } ,
fields ::{ fp ::FpVar , nonnative ::NonNativeFieldVar , FieldVar } ,
groups ::GroupOpsBounds ,
groups ::GroupOpsBounds ,
poly ::{ domain ::Radix2DomainVar , evaluations ::univariate ::EvaluationsVar } ,
prelude ::CurveVar ,
prelude ::CurveVar ,
ToConstraintFieldGadget ,
} ;
} ;
use ark_relations ::r1cs ::{ ConstraintSynthesizer , ConstraintSystemRef , Namespace , SynthesisError } ;
use ark_relations ::r1cs ::{ ConstraintSynthesizer , ConstraintSystemRef , Namespace , SynthesisError } ;
use ark_std ::{ One , Zero } ;
use ark_std ::{ log2 , One , Zero } ;
use core ::{ borrow ::Borrow , marker ::PhantomData } ;
use core ::{ borrow ::Borrow , marker ::PhantomData } ;
use super ::{ circuits ::ChallengeGadget , nifs ::NIFS } ;
use crate ::ccs ::r1cs ::R1CS ;
use crate ::ccs ::r1cs ::R1CS ;
use crate ::commitment ::{ pedersen ::Params as PedersenParams , CommitmentProver } ;
use crate ::commitment ::{ pedersen ::Params as PedersenParams , CommitmentScheme } ;
use crate ::folding ::circuits ::nonnative ::{ point_to_nonnative_limbs , NonNativeAffineVar } ;
use crate ::folding ::nova ::{
use crate ::folding ::nova ::{
circuits ::{ CommittedInstanceVar , CF1 , CF2 } ,
circuits ::{ CommittedInstanceVar , CF1 , CF2 } ,
CommittedInstance , Nova , Witness ,
CommittedInstance , Nova , Witness ,
} ;
} ;
use crate ::frontend ::FCircuit ;
use crate ::frontend ::FCircuit ;
use crate ::utils ::gadgets ::{
hadamard , mat_vec_mul_sparse , vec_add , vec_scalar_mul , SparseMatrixVar ,
use crate ::transcript ::{
poseidon ::{ PoseidonTranscript , PoseidonTranscriptVar } ,
Transcript , TranscriptVar ,
} ;
} ;
use crate ::utils ::{
gadgets ::{ hadamard , mat_vec_mul_sparse , vec_add , vec_scalar_mul , SparseMatrixVar } ,
vec ::poly_from_vec ,
} ;
use crate ::Error ;
#[ derive(Debug, Clone) ]
#[ derive(Debug, Clone) ]
pub struct RelaxedR1CSGadget < F : PrimeField , CF : PrimeField , FV : FieldVar < F , CF > > {
pub struct RelaxedR1CSGadget < F : PrimeField , CF : PrimeField , FV : FieldVar < F , CF > > {
@ -178,21 +189,21 @@ where
/// Circuit that implements the in-circuit checks needed for the onchain (Ethereum's EVM)
/// Circuit that implements the in-circuit checks needed for the onchain (Ethereum's EVM)
/// verification.
/// verification.
#[ derive(Clone, Debug) ]
#[ derive(Clone, Debug) ]
pub struct DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CP1 , CP 2 >
pub struct DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CS1 , CS 2 >
where
where
C1 : CurveGroup ,
C1 : CurveGroup ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
C2 : CurveGroup ,
C2 : CurveGroup ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
CP1 : CommitmentProver < C1 > ,
CP2 : CommitmentProver < C2 > ,
CS1 : CommitmentScheme < C1 > ,
CS2 : CommitmentScheme < C2 > ,
{
{
_c1 : PhantomData < C1 > ,
_c1 : PhantomData < C1 > ,
_gc1 : PhantomData < GC1 > ,
_gc1 : PhantomData < GC1 > ,
_c2 : PhantomData < C2 > ,
_c2 : PhantomData < C2 > ,
_gc2 : PhantomData < GC2 > ,
_gc2 : PhantomData < GC2 > ,
_cp1 : PhantomData < CP 1 > ,
_cp2 : PhantomData < CP 2 > ,
_cs1 : PhantomData < CS 1 > ,
_cs2 : PhantomData < CS 2 > ,
/// E vector's length of the Nova instance witness
/// E vector's length of the Nova instance witness
pub E_len : usize ,
pub E_len : usize ,
@ -215,36 +226,89 @@ where
pub w_i : Option < Witness < C1 > > ,
pub w_i : Option < Witness < C1 > > ,
pub U_i : Option < CommittedInstance < C1 > > ,
pub U_i : Option < CommittedInstance < C1 > > ,
pub W_i : Option < Witness < C1 > > ,
pub W_i : Option < Witness < C1 > > ,
pub U_i1 : Option < CommittedInstance < C1 > > ,
pub W_i1 : Option < Witness < C1 > > ,
pub cmT : Option < C1 > ,
pub r : Option < C1 ::ScalarField > ,
/// CycleFold running instance
/// CycleFold running instance
pub cf_U_i : Option < CommittedInstance < C2 > > ,
pub cf_U_i : Option < CommittedInstance < C2 > > ,
pub cf_W_i : Option < Witness < C2 > > ,
pub cf_W_i : Option < Witness < C2 > > ,
/// KZG challenges
pub kzg_c_W : Option < C1 ::ScalarField > ,
pub kzg_c_E : Option < C1 ::ScalarField > ,
pub eval_W : Option < C1 ::ScalarField > ,
pub eval_E : Option < C1 ::ScalarField > ,
}
}
impl < C1 , GC1 , C2 , GC2 , CP1 , CP2 > DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CP1 , CP2 >
impl < C1 , GC1 , C2 , GC2 , CS1 , CS 2 > DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CS1 , CS 2 >
where
where
C1 : CurveGroup ,
C1 : CurveGroup ,
C2 : CurveGroup ,
C2 : CurveGroup ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
CP1 : CommitmentProver < C1 > ,
// enforce that the CP2 is Pedersen commitment, since we're at Ethereum's EVM decider
CP2 : CommitmentProver < C2 , Params = PedersenParams < C2 > > ,
CS1 : CommitmentScheme < C1 > ,
// enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
CS2 : CommitmentScheme < C2 , ProverParams = PedersenParams < C2 > > ,
< C1 as Group > ::ScalarField : Absorb ,
< C1 as CurveGroup > ::BaseField : PrimeField ,
{
{
pub fn from_nova < FC : FCircuit < C1 ::ScalarField > > (
pub fn from_nova < FC : FCircuit < C1 ::ScalarField > > (
nova : Nova < C1 , GC1 , C2 , GC2 , FC , CP1 , CP2 > ,
) -> Self {
Self {
nova : Nova < C1 , GC1 , C2 , GC2 , FC , CS1 , CS2 > ,
) -> Result < Self , Error > {
// compute the U_{i+1}, W_{i+1}
let ( T , cmT ) = NIFS ::< C1 , CS1 > ::compute_cmT (
& nova . cs_params ,
& nova . r1cs . clone ( ) ,
& nova . w_i . clone ( ) ,
& nova . u_i . clone ( ) ,
& nova . W_i . clone ( ) ,
& nova . U_i . clone ( ) ,
) ? ;
let r_bits = ChallengeGadget ::< C1 > ::get_challenge_native (
& nova . poseidon_config ,
nova . U_i . clone ( ) ,
nova . u_i . clone ( ) ,
cmT ,
) ? ;
let r_Fr = C1 ::ScalarField ::from_bigint ( BigInteger ::from_bits_le ( & r_bits ) )
. ok_or ( Error ::OutOfBounds ) ? ;
let ( W_i1 , U_i1 ) = NIFS ::< C1 , CS1 > ::fold_instances (
r_Fr , & nova . W_i , & nova . U_i , & nova . w_i , & nova . u_i , & T , cmT ,
) ? ;
// compute the KZG challenges used as inputs in the circuit
let ( kzg_challenge_W , kzg_challenge_E ) =
KZGChallengesGadget ::< C1 > ::get_challenges_native ( & nova . poseidon_config , U_i1 . clone ( ) ) ? ;
// get KZG evals
let mut W = W_i1 . W . clone ( ) ;
W . extend (
std ::iter ::repeat ( C1 ::ScalarField ::zero ( ) )
. take ( W_i1 . W . len ( ) . next_power_of_two ( ) - W_i1 . W . len ( ) ) ,
) ;
let mut E = W_i1 . E . clone ( ) ;
E . extend (
std ::iter ::repeat ( C1 ::ScalarField ::zero ( ) )
. take ( W_i1 . E . len ( ) . next_power_of_two ( ) - W_i1 . E . len ( ) ) ,
) ;
let p_W = poly_from_vec ( W . to_vec ( ) ) ? ;
let eval_W = p_W . evaluate ( & kzg_challenge_W ) ;
let p_E = poly_from_vec ( E . to_vec ( ) ) ? ;
let eval_E = p_E . evaluate ( & kzg_challenge_E ) ;
Ok ( Self {
_c1 : PhantomData ,
_c1 : PhantomData ,
_gc1 : PhantomData ,
_gc1 : PhantomData ,
_c2 : PhantomData ,
_c2 : PhantomData ,
_gc2 : PhantomData ,
_gc2 : PhantomData ,
_cp1 : PhantomData ,
_cp2 : PhantomData ,
_cs 1 : PhantomData ,
_cs 2 : PhantomData ,
E_len : nova . W_i . E . len ( ) ,
E_len : nova . W_i . E . len ( ) ,
cf_E_len : nova . cf_W_i . E . len ( ) ,
cf_E_len : nova . cf_W_i . E . len ( ) ,
r1cs : nova . r1cs ,
r1cs : nova . r1cs ,
cf_r1cs : nova . cf_r1cs ,
cf_r1cs : nova . cf_r1cs ,
cf_pedersen_params : nova . cf_cm_params ,
cf_pedersen_params : nova . cf_cs _params ,
poseidon_config : nova . poseidon_config ,
poseidon_config : nova . poseidon_config ,
i : Some ( nova . i ) ,
i : Some ( nova . i ) ,
z_0 : Some ( nova . z_0 ) ,
z_0 : Some ( nova . z_0 ) ,
@ -253,21 +317,29 @@ where
w_i : Some ( nova . w_i ) ,
w_i : Some ( nova . w_i ) ,
U_i : Some ( nova . U_i ) ,
U_i : Some ( nova . U_i ) ,
W_i : Some ( nova . W_i ) ,
W_i : Some ( nova . W_i ) ,
U_i1 : Some ( U_i1 ) ,
W_i1 : Some ( W_i1 ) ,
cmT : Some ( cmT ) ,
r : Some ( r_Fr ) ,
cf_U_i : Some ( nova . cf_U_i ) ,
cf_U_i : Some ( nova . cf_U_i ) ,
cf_W_i : Some ( nova . cf_W_i ) ,
cf_W_i : Some ( nova . cf_W_i ) ,
}
kzg_c_W : Some ( kzg_challenge_W ) ,
kzg_c_E : Some ( kzg_challenge_E ) ,
eval_W : Some ( eval_W ) ,
eval_E : Some ( eval_E ) ,
} )
}
}
}
}
impl < C1 , GC1 , C2 , GC2 , CP1 , CP2 > ConstraintSynthesizer < CF1 < C1 > >
for DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CP1 , CP 2 >
impl < C1 , GC1 , C2 , GC2 , CS1 , CS 2 > ConstraintSynthesizer < CF1 < C1 > >
for DeciderEthCircuit < C1 , GC1 , C2 , GC2 , CS1 , CS 2 >
where
where
C1 : CurveGroup ,
C1 : CurveGroup ,
C2 : CurveGroup ,
C2 : CurveGroup ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
GC1 : CurveVar < C1 , CF2 < C1 > > ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
GC2 : CurveVar < C2 , CF2 < C2 > > ,
CP1 : CommitmentProver < C1 > ,
CP2 : CommitmentProver < C2 > ,
CS1 : CommitmentScheme < C1 > ,
CS2 : CommitmentScheme < C2 > ,
< C1 as CurveGroup > ::BaseField : PrimeField ,
< C1 as CurveGroup > ::BaseField : PrimeField ,
< C2 as CurveGroup > ::BaseField : PrimeField ,
< C2 as CurveGroup > ::BaseField : PrimeField ,
< C1 as Group > ::ScalarField : Absorb ,
< C1 as Group > ::ScalarField : Absorb ,
@ -299,14 +371,29 @@ where
let u_i = CommittedInstanceVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
let u_i = CommittedInstanceVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
Ok ( self . u_i . unwrap_or ( u_dummy_native . clone ( ) ) )
Ok ( self . u_i . unwrap_or ( u_dummy_native . clone ( ) ) )
} ) ? ;
} ) ? ;
let w_i = WitnessVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
Ok ( self . w_i . unwrap_or ( w_dummy_native . clone ( ) ) )
} ) ? ;
let U_i = CommittedInstanceVar ::< C1 > ::new_input ( cs . clone ( ) , | | {
let U_i = CommittedInstanceVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
Ok ( self . U_i . unwrap_or ( u_dummy_native . clone ( ) ) )
Ok ( self . U_i . unwrap_or ( u_dummy_native . clone ( ) ) )
} ) ? ;
} ) ? ;
let W_i = WitnessVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
Ok ( self . W_i . unwrap_or ( w_dummy_native . clone ( ) ) )
// here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
let U_i1 = CommittedInstanceVar ::< C1 > ::new_input ( cs . clone ( ) , | | {
Ok ( self . U_i1 . unwrap_or ( u_dummy_native . clone ( ) ) )
} ) ? ;
let W_i1 = WitnessVar ::< C1 > ::new_witness ( cs . clone ( ) , | | {
Ok ( self . W_i1 . unwrap_or ( w_dummy_native . clone ( ) ) )
} ) ? ;
// allocate the inputs for the check 6
let kzg_c_W = FpVar ::< CF1 < C1 > > ::new_input ( cs . clone ( ) , | | {
Ok ( self . kzg_c_W . unwrap_or_else ( CF1 ::< C1 > ::zero ) )
} ) ? ;
let kzg_c_E = FpVar ::< CF1 < C1 > > ::new_input ( cs . clone ( ) , | | {
Ok ( self . kzg_c_E . unwrap_or_else ( CF1 ::< C1 > ::zero ) )
} ) ? ;
let _eval_W = FpVar ::< CF1 < C1 > > ::new_input ( cs . clone ( ) , | | {
Ok ( self . eval_W . unwrap_or_else ( CF1 ::< C1 > ::zero ) )
} ) ? ;
let _eval_E = FpVar ::< CF1 < C1 > > ::new_input ( cs . clone ( ) , | | {
Ok ( self . eval_E . unwrap_or_else ( CF1 ::< C1 > ::zero ) )
} ) ? ;
} ) ? ;
let crh_params = CRHParametersVar ::< C1 ::ScalarField > ::new_constant (
let crh_params = CRHParametersVar ::< C1 ::ScalarField > ::new_constant (
@ -314,31 +401,17 @@ where
self . poseidon_config . clone ( ) ,
self . poseidon_config . clone ( ) ,
) ? ;
) ? ;
// 1. check RelaxedR1CS of u_i
let z_u : Vec < FpVar < CF1 < C1 > > > = [
vec ! [ FpVar ::< CF1 < C1 > > ::one ( ) ] ,
u_i . x . to_vec ( ) ,
w_i . W . to_vec ( ) ,
]
. concat ( ) ;
RelaxedR1CSGadget ::< C1 ::ScalarField , CF1 < C1 > , FpVar < CF1 < C1 > > > ::check (
r1cs . clone ( ) ,
w_i . E ,
u_i . u . clone ( ) ,
z_u ,
) ? ;
// 2. check RelaxedR1CS of U_i
let z_U : Vec < FpVar < CF1 < C1 > > > =
[ vec ! [ U_i . u . clone ( ) ] , U_i . x . to_vec ( ) , W_i . W . to_vec ( ) ] . concat ( ) ;
// 1. check RelaxedR1CS of U_{i+1}
let z_U1 : Vec < FpVar < CF1 < C1 > > > =
[ vec ! [ U_i1 . u . clone ( ) ] , U_i1 . x . to_vec ( ) , W_i1 . W . to_vec ( ) ] . concat ( ) ;
RelaxedR1CSGadget ::< C1 ::ScalarField , CF1 < C1 > , FpVar < CF1 < C1 > > > ::check (
RelaxedR1CSGadget ::< C1 ::ScalarField , CF1 < C1 > , FpVar < CF1 < C1 > > > ::check (
r1cs ,
r1cs ,
W_i . E ,
U_i . u . clone ( ) ,
z_U ,
W_i1 . E . clone ( ) ,
U_i1 . u . clone ( ) ,
z_U1 ,
) ? ;
) ? ;
// 3 . u_i.cmE==cm(0), u_i.u==1
// 2. u_i.cmE==cm(0), u_i.u==1
// Here zero_x & zero_y are the x & y coordinates of the zero point affine representation.
// Here zero_x & zero_y are the x & y coordinates of the zero point affine representation.
let zero_x = NonNativeFieldVar ::< C1 ::BaseField , C1 ::ScalarField > ::new_constant (
let zero_x = NonNativeFieldVar ::< C1 ::BaseField , C1 ::ScalarField > ::new_constant (
cs . clone ( ) ,
cs . clone ( ) ,
@ -348,19 +421,19 @@ where
cs . clone ( ) ,
cs . clone ( ) ,
C1 ::BaseField ::one ( ) ,
C1 ::BaseField ::one ( ) ,
) ? ;
) ? ;
( u_i . cmE . x . is_eq ( & zero_x ) ? ) . enforce_equal ( & Boolean ::TRUE ) ? ;
( u_i . cmE . y . is_eq ( & zero_y ) ? ) . enforce_equal ( & Boolean ::TRUE ) ? ;
u_i . cmE . x . enforce_equal ( & zero_x ) ? ;
u_i . cmE . y . enforce_equal ( & zero_y ) ? ;
( u_i . u . is_one ( ) ? ) . enforce_equal ( & Boolean ::TRUE ) ? ;
( u_i . u . is_one ( ) ? ) . enforce_equal ( & Boolean ::TRUE ) ? ;
// 4 . 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 ( ) ) ? ;
// 3 . u_i.x == H(i, z_0, z_i, U_i)
let ( u_i_x , U _i_vec ) =
U_i . clone ( )
. hash ( & crh_params , i . clone ( ) , z_0 . clone ( ) , z_i . clone ( ) ) ? ;
( u_i . x [ 0 ] ) . enforce_equal ( & u_i_x ) ? ;
( u_i . x [ 0 ] ) . enforce_equal ( & u_i_x ) ? ;
// The following two checks (and their respective allocations) are disabled for normal
// The following two checks (and their respective allocations) are disabled for normal
// tests since they take ~24.5M constraints and would take several minutes (and RAM) to run
// the test
// tests since they take several millions of constraints and would take several minutes
// (and RAM) to run the test.
#[ cfg(not(test)) ]
#[ cfg(not(test)) ]
{
{
// imports here instead of at the top of the file, so we avoid having multiple
// imports here instead of at the top of the file, so we avoid having multiple
@ -381,7 +454,7 @@ where
Ok ( self . cf_W_i . unwrap_or ( w_dummy_native . clone ( ) ) )
Ok ( self . cf_W_i . unwrap_or ( w_dummy_native . clone ( ) ) )
} ) ? ;
} ) ? ;
// 5 . check Pedersen commitments of cf_U_i.{cmE, cmW}
// 4 . check Pedersen commitments of cf_U_i.{cmE, cmW}
let H = GC2 ::new_constant ( cs . clone ( ) , self . cf_pedersen_params . h ) ? ;
let H = GC2 ::new_constant ( cs . clone ( ) , self . cf_pedersen_params . h ) ? ;
let G = Vec ::< GC2 > ::new_constant ( cs . clone ( ) , self . cf_pedersen_params . generators ) ? ;
let G = Vec ::< GC2 > ::new_constant ( cs . clone ( ) , self . cf_pedersen_params . generators ) ? ;
let cf_W_i_E_bits : Result < Vec < Vec < Boolean < CF1 < C1 > > > > , SynthesisError > =
let cf_W_i_E_bits : Result < Vec < Vec < Boolean < CF1 < C1 > > > > , SynthesisError > =
@ -406,7 +479,7 @@ where
NonNativeFieldVar < C1 ::BaseField , CF1 < C1 > > ,
NonNativeFieldVar < C1 ::BaseField , CF1 < C1 > > ,
> ::new_witness ( cs . clone ( ) , | | Ok ( self . cf_r1cs . clone ( ) ) ) ? ;
> ::new_witness ( cs . clone ( ) , | | Ok ( self . cf_r1cs . clone ( ) ) ) ? ;
// 6 . check RelaxedR1CS of cf_U_i
// 5 . check RelaxedR1CS of cf_U_i
let cf_z_U : Vec < NonNativeFieldVar < C2 ::ScalarField , CF1 < C1 > > > =
let cf_z_U : Vec < NonNativeFieldVar < C2 ::ScalarField , CF1 < C1 > > > =
[ vec ! [ cf_U_i . u . clone ( ) ] , cf_U_i . x . to_vec ( ) , cf_W_i . W . to_vec ( ) ] . concat ( ) ;
[ vec ! [ cf_U_i . u . clone ( ) ] , cf_U_i . x . to_vec ( ) , cf_W_i . W . to_vec ( ) ] . concat ( ) ;
RelaxedR1CSGadget ::<
RelaxedR1CSGadget ::<
@ -416,10 +489,122 @@ where
> ::check ( cf_r1cs , cf_W_i . E , cf_U_i . u . clone ( ) , cf_z_U ) ? ;
> ::check ( cf_r1cs , cf_W_i . E , cf_U_i . u . clone ( ) , cf_z_U ) ? ;
}
}
// 6. check KZG challenges
let ( incircuit_c_W , incircuit_c_E ) = KZGChallengesGadget ::< C1 > ::get_challenges_gadget (
cs . clone ( ) ,
& self . poseidon_config ,
U_i1 . clone ( ) ,
) ? ;
incircuit_c_W . enforce_equal ( & kzg_c_W ) ? ;
incircuit_c_E . enforce_equal ( & kzg_c_E ) ? ;
// Check 7 is temporary disabled due
// https://github.com/privacy-scaling-explorations/folding-schemes/issues/80
//
// 7. check eval_W==p_W(c_W) and eval_E==p_E(c_E)
// let incircuit_eval_W = evaluate_gadget::<CF1<C1>>(W_i1.W, incircuit_c_W)?;
// let incircuit_eval_E = evaluate_gadget::<CF1<C1>>(W_i1.E, incircuit_c_E)?;
// incircuit_eval_W.enforce_equal(&eval_W)?;
// incircuit_eval_E.enforce_equal(&eval_E)?;
// 8. compute the NIFS.V challenge and check that matches the one from the public input (so we
// avoid the verifier computing it)
let cmT =
NonNativeAffineVar ::new_input ( cs . clone ( ) , | | Ok ( self . cmT . unwrap_or_else ( C1 ::zero ) ) ) ? ;
let r_bits = ChallengeGadget ::< C1 > ::get_challenge_gadget (
cs . clone ( ) ,
& self . poseidon_config ,
U_i_vec ,
u_i . clone ( ) ,
cmT . clone ( ) ,
) ? ;
let r_Fr = Boolean ::le_bits_to_fp_var ( & r_bits ) ? ;
// check that the in-circuit computed r is equal to the inputted r
let r =
FpVar ::< CF1 < C1 > > ::new_input ( cs . clone ( ) , | | Ok ( self . r . unwrap_or_else ( CF1 ::< C1 > ::zero ) ) ) ? ;
r_Fr . enforce_equal ( & r ) ? ;
Ok ( ( ) )
Ok ( ( ) )
}
}
}
}
/// Interpolates the polynomial from the given vector, and then returns it's evaluation at the
/// given point.
#[ allow(unused) ] // unused while check 7 is disabled
fn evaluate_gadget < F : PrimeField > (
v : Vec < FpVar < F > > ,
point : FpVar < F > ,
) -> Result < FpVar < F > , SynthesisError > {
if ! v . len ( ) . is_power_of_two ( ) {
return Err ( SynthesisError ::Unsatisfiable ) ;
}
let n = v . len ( ) as u64 ;
let gen = F ::get_root_of_unity ( n ) . unwrap ( ) ;
let domain = Radix2DomainVar ::new ( gen , log2 ( v . len ( ) ) as u64 , FpVar ::one ( ) ) . unwrap ( ) ;
let evaluations_var = EvaluationsVar ::from_vec_and_domain ( v , domain , true ) ;
evaluations_var . interpolate_and_evaluate ( & point )
}
/// Gadget that computes the KZG challenges, also offers the rust native implementation compatible
/// with the gadget.
pub struct KZGChallengesGadget < C : CurveGroup > {
_c : PhantomData < C > ,
}
impl < C > KZGChallengesGadget < C >
where
C : CurveGroup ,
C ::ScalarField : PrimeField ,
< C as CurveGroup > ::BaseField : PrimeField ,
C ::ScalarField : Absorb ,
{
pub fn get_challenges_native (
poseidon_config : & PoseidonConfig < C ::ScalarField > ,
U_i : CommittedInstance < C > ,
) -> Result < ( C ::ScalarField , C ::ScalarField ) , Error > {
let ( cmE_x_limbs , cmE_y_limbs ) : ( Vec < C ::ScalarField > , Vec < C ::ScalarField > ) =
point_to_nonnative_limbs ::< C > ( U_i . cmE ) ? ;
let ( cmW_x_limbs , cmW_y_limbs ) : ( Vec < C ::ScalarField > , Vec < C ::ScalarField > ) =
point_to_nonnative_limbs ::< C > ( U_i . cmW ) ? ;
let transcript = & mut PoseidonTranscript ::< C > ::new ( poseidon_config ) ;
// compute the KZG challenges, which are computed in-circuit and checked that it matches
// the inputted one
transcript . absorb_vec ( & cmW_x_limbs ) ;
transcript . absorb_vec ( & cmW_y_limbs ) ;
let challenge_W = transcript . get_challenge ( ) ;
transcript . absorb_vec ( & cmE_x_limbs ) ;
transcript . absorb_vec ( & cmE_y_limbs ) ;
let challenge_E = transcript . get_challenge ( ) ;
Ok ( ( challenge_W , challenge_E ) )
}
// compatible with the native get_challenges_native
#[ allow(clippy::type_complexity) ]
pub fn get_challenges_gadget (
cs : ConstraintSystemRef < C ::ScalarField > ,
poseidon_config : & PoseidonConfig < C ::ScalarField > ,
U_i : CommittedInstanceVar < C > ,
) -> Result < ( FpVar < C ::ScalarField > , FpVar < C ::ScalarField > ) , SynthesisError > {
let mut transcript =
PoseidonTranscriptVar ::< CF1 < C > > ::new ( cs . clone ( ) , & poseidon_config . clone ( ) ) ;
let cmW_x_limbs = U_i . cmW . x . to_constraint_field ( ) ? ;
let cmW_y_limbs = U_i . cmW . y . to_constraint_field ( ) ? ;
transcript . absorb_vec ( & cmW_x_limbs ) ? ;
transcript . absorb_vec ( & cmW_y_limbs ) ? ;
let challenge_W = transcript . get_challenge ( ) ? ;
let cmE_x_limbs = U_i . cmE . x . to_constraint_field ( ) ? ;
let cmE_y_limbs = U_i . cmE . y . to_constraint_field ( ) ? ;
transcript . absorb_vec ( & cmE_x_limbs ) ? ;
transcript . absorb_vec ( & cmE_y_limbs ) ? ;
let challenge_E = transcript . get_challenge ( ) ? ;
Ok ( ( challenge_W , challenge_E ) )
}
}
#[ cfg(test) ]
#[ cfg(test) ]
pub mod tests {
pub mod tests {
use super ::* ;
use super ::* ;
@ -439,10 +624,11 @@ pub mod tests {
fields ::{ fp ::FpVar , nonnative ::NonNativeFieldVar } ,
fields ::{ fp ::FpVar , nonnative ::NonNativeFieldVar } ,
} ;
} ;
use ark_relations ::r1cs ::ConstraintSystem ;
use ark_relations ::r1cs ::ConstraintSystem ;
use ark_std ::UniformRand ;
use ark_vesta ::{ constraints ::GVar as GVar2 , Projective as Projective2 } ;
use ark_vesta ::{ constraints ::GVar as GVar2 , Projective as Projective2 } ;
use crate ::commitment ::pedersen ::Pedersen ;
use crate ::commitment ::pedersen ::Pedersen ;
use crate ::folding ::nova ::{ get_pedersen _params_len , ProverParams , VerifierParams } ;
use crate ::folding ::nova ::{ get_cs _params_len , ProverParams , VerifierParams } ;
use crate ::frontend ::tests ::{ CubicFCircuit , CustomFCircuit , WrapperCircuit } ;
use crate ::frontend ::tests ::{ CubicFCircuit , CustomFCircuit , WrapperCircuit } ;
use crate ::transcript ::poseidon ::poseidon_test_config ;
use crate ::transcript ::poseidon ::poseidon_test_config ;
use crate ::FoldingScheme ;
use crate ::FoldingScheme ;
@ -610,21 +796,21 @@ pub mod tests {
let F_circuit = CubicFCircuit ::< Fr > ::new ( ( ) ) ;
let F_circuit = CubicFCircuit ::< Fr > ::new ( ( ) ) ;
let z_0 = vec ! [ Fr ::from ( 3_ u32 ) ] ;
let z_0 = vec ! [ Fr ::from ( 3_ u32 ) ] ;
// get the CM & CF_CM len
let ( cm_len , cf_cm _len ) =
get_pedersen _params_len ::< Projective , GVar , Projective2 , GVar2 , CubicFCircuit < Fr > > (
// get the CS & CF_CS len
let ( cs_len , cf_cs _len ) =
get_cs _params_len ::< Projective , GVar , Projective2 , GVar2 , CubicFCircuit < Fr > > (
& poseidon_config ,
& poseidon_config ,
F_circuit ,
F_circuit ,
)
)
. unwrap ( ) ;
. unwrap ( ) ;
let pedersen_params = Pedersen ::< Projective > ::new_params ( & mut rng , cm_len ) ;
let cf_pedersen_params = Pedersen ::< Projective2 > ::new_params ( & mut rng , cf_cm_len ) ;
let ( pedersen_params , _ ) = Pedersen ::< Projective > ::setup ( & mut rng , cs_len ) . unwrap ( ) ;
let ( cf_pedersen_params , _ ) = Pedersen ::< Projective2 > ::setup ( & mut rng , cf_cs_len ) . unwrap ( ) ;
let prover_params =
let prover_params =
ProverParams ::< Projective , Projective2 , Pedersen < Projective > , Pedersen < Projective2 > > {
ProverParams ::< Projective , Projective2 , Pedersen < Projective > , Pedersen < Projective2 > > {
poseidon_config : poseidon_config . clone ( ) ,
poseidon_config : poseidon_config . clone ( ) ,
cm _params : pedersen_params ,
cf_cm _params : cf_pedersen_params ,
cs _params : pedersen_params ,
cf_cs _params : cf_pedersen_params ,
} ;
} ;
type NOVA = Nova <
type NOVA = Nova <
@ -666,12 +852,82 @@ pub mod tests {
GVar2 ,
GVar2 ,
Pedersen < Projective > ,
Pedersen < Projective > ,
Pedersen < Projective2 > ,
Pedersen < Projective2 > ,
> ::from_nova ( nova ) ;
> ::from_nova ( nova )
. unwrap ( ) ;
let cs = ConstraintSystem ::< Fr > ::new_ref ( ) ;
let cs = ConstraintSystem ::< Fr > ::new_ref ( ) ;
// generate the constraints and check that are satisfied by the inputs
// generate the constraints and check that are satisfied by the inputs
decider_circuit . generate_constraints ( cs . clone ( ) ) . unwrap ( ) ;
decider_circuit . generate_constraints ( cs . clone ( ) ) . unwrap ( ) ;
assert ! ( cs . is_satisfied ( ) . unwrap ( ) ) ;
assert ! ( cs . is_satisfied ( ) . unwrap ( ) ) ;
dbg ! ( cs . num_constraints ( ) ) ;
}
// checks that the gadget and native implementations of the challenge computation match
#[ test ]
fn test_kzg_challenge_gadget ( ) {
let mut rng = ark_std ::test_rng ( ) ;
let poseidon_config = poseidon_test_config ::< Fr > ( ) ;
let U_i = CommittedInstance ::< Projective > {
cmE : Projective ::rand ( & mut rng ) ,
u : Fr ::rand ( & mut rng ) ,
cmW : Projective ::rand ( & mut rng ) ,
x : vec ! [ Fr ::rand ( & mut rng ) ; 1 ] ,
} ;
// compute the challenge natively
let ( challenge_W , challenge_E ) =
KZGChallengesGadget ::< Projective > ::get_challenges_native ( & poseidon_config , U_i . clone ( ) )
. unwrap ( ) ;
let cs = ConstraintSystem ::< Fr > ::new_ref ( ) ;
let U_iVar =
CommittedInstanceVar ::< Projective > ::new_witness ( cs . clone ( ) , | | Ok ( U_i . clone ( ) ) )
. unwrap ( ) ;
let ( challenge_W_Var , challenge_E_Var ) =
KZGChallengesGadget ::< Projective > ::get_challenges_gadget (
cs . clone ( ) ,
& poseidon_config ,
U_iVar ,
)
. unwrap ( ) ;
assert ! ( cs . is_satisfied ( ) . unwrap ( ) ) ;
// check that the natively computed and in-circuit computed hashes match
use ark_r1cs_std ::R1CSVar ;
assert_eq ! ( challenge_W_Var . value ( ) . unwrap ( ) , challenge_W ) ;
assert_eq ! ( challenge_E_Var . value ( ) . unwrap ( ) , challenge_E ) ;
}
// The test test_polynomial_interpolation is temporary disabled due
// https://github.com/privacy-scaling-explorations/folding-schemes/issues/80
// for n<=11 it will work, but for n>11 it will fail with stack overflow.
#[ ignore ]
#[ test ]
fn test_polynomial_interpolation ( ) {
let mut rng = ark_std ::test_rng ( ) ;
let n = 12 ;
let l = 1 < < n ;
let v : Vec < Fr > = std ::iter ::repeat_with ( | | Fr ::rand ( & mut rng ) )
. take ( l )
. collect ( ) ;
let challenge = Fr ::rand ( & mut rng ) ;
use ark_poly ::Polynomial ;
let polynomial = poly_from_vec ( v . to_vec ( ) ) . unwrap ( ) ;
let eval = polynomial . evaluate ( & challenge ) ;
let cs = ConstraintSystem ::< Fr > ::new_ref ( ) ;
let vVar = Vec ::< FpVar < Fr > > ::new_witness ( cs . clone ( ) , | | Ok ( v ) ) . unwrap ( ) ;
let challengeVar = FpVar ::< Fr > ::new_witness ( cs . clone ( ) , | | Ok ( challenge ) ) . unwrap ( ) ;
let evalVar = evaluate_gadget ::< Fr > ( vVar , challengeVar ) . unwrap ( ) ;
use ark_r1cs_std ::R1CSVar ;
assert_eq ! ( evalVar . value ( ) . unwrap ( ) , eval ) ;
assert ! ( cs . is_satisfied ( ) . unwrap ( ) ) ;
}
}
}
}