@ -10,18 +10,19 @@
//! otherwise
//! otherwise
//! h1 = H(u2, i) and h2 = H(params = H(shape, gens), u1, i, z0, zi)
//! h1 = H(u2, i) and h2 = H(params = H(shape, gens), u1, i, z0, zi)
use super ::commitments ::Commitment ;
use super ::gadgets ::{
ecc ::AllocatedPoint ,
utils ::{
alloc_bignat_constant , alloc_num_equals , alloc_one , alloc_zero , conditionally_select ,
conditionally_select_bignat , le_bits_to_num ,
use super ::{
commitments ::Commitment ,
gadgets ::{
ecc ::AllocatedPoint ,
utils ::{
alloc_bignat_constant , alloc_num_equals , alloc_one , alloc_zero , conditionally_select ,
conditionally_select_bignat , le_bits_to_num ,
} ,
} ,
} ,
poseidon ::{ NovaPoseidonConstants , PoseidonROGadget } ,
r1cs ::RelaxedR1CSInstance ,
traits ::{ Group , PrimeField , StepCircuit } ,
} ;
} ;
use super ::poseidon ::NovaPoseidonConstants ;
use super ::poseidon ::PoseidonROGadget ;
use super ::r1cs ::RelaxedR1CSInstance ;
use super ::traits ::{ Group , InnerCircuit , PrimeField } ;
use bellperson ::{
use bellperson ::{
gadgets ::{ boolean ::Boolean , num ::AllocatedNum , Assignment } ,
gadgets ::{ boolean ::Boolean , num ::AllocatedNum , Assignment } ,
Circuit , ConstraintSystem , SynthesisError ,
Circuit , ConstraintSystem , SynthesisError ,
@ -33,12 +34,12 @@ use bellperson_nonnative::{
use ff ::PrimeFieldBits ;
use ff ::PrimeFieldBits ;
#[ derive(Debug, Clone) ]
#[ derive(Debug, Clone) ]
pub struct Verification CircuitParams {
pub struct NIFSVerifier CircuitParams {
limb_width : usize ,
limb_width : usize ,
n_limbs : usize ,
n_limbs : usize ,
}
}
impl Verification CircuitParams {
impl NIFSVerifier CircuitParams {
#[ allow(dead_code) ]
#[ allow(dead_code) ]
pub fn new ( limb_width : usize , n_limbs : usize ) -> Self {
pub fn new ( limb_width : usize , n_limbs : usize ) -> Self {
Self {
Self {
@ -48,7 +49,7 @@ impl VerificationCircuitParams {
}
}
}
}
pub struct Verification CircuitInputs< G >
pub struct NIFSVerifier CircuitInputs< G >
where
where
G : Group ,
G : Group ,
{
{
@ -63,7 +64,7 @@ where
w : Commitment < G > , // The commitment to the witness of the fresh r1cs instance
w : Commitment < G > , // The commitment to the witness of the fresh r1cs instance
}
}
impl < G > Verification CircuitInputs< G >
impl < G > NIFSVerifier CircuitInputs< G >
where
where
G : Group ,
G : Group ,
{
{
@ -95,30 +96,30 @@ where
}
}
/// Circuit that encodes only the folding verifier
/// Circuit that encodes only the folding verifier
pub struct Verification Circuit< G , I C>
pub struct NIFSVerifier Circuit< G , S C>
where
where
G : Group ,
G : Group ,
< G as Group > ::Base : ff ::PrimeField ,
< G as Group > ::Base : ff ::PrimeField ,
IC : Inner Circuit< G ::Base > ,
SC : Step Circuit< G ::Base > ,
{
{
params : Verification CircuitParams,
inputs : Option < Verification CircuitInputs< G > > ,
inner_circuit : Option < I C> , // The function that is applied for each step. may be None.
params : NIFSVerifier CircuitParams,
inputs : Option < NIFSVerifier CircuitInputs< G > > ,
step_circuit : Option < S C> , // The function that is applied for each step. may be None.
poseidon_constants : NovaPoseidonConstants < G ::Base > ,
poseidon_constants : NovaPoseidonConstants < G ::Base > ,
}
}
impl < G , IC > Verification Circuit< G , I C>
impl < G , SC > NIFSVerifier Circuit< G , S C>
where
where
G : Group ,
G : Group ,
< G as Group > ::Base : ff ::PrimeField ,
< G as Group > ::Base : ff ::PrimeField ,
IC : Inner Circuit< G ::Base > ,
SC : Step Circuit< G ::Base > ,
{
{
/// Create a new verification circuit for the input relaxed r1cs instances
/// Create a new verification circuit for the input relaxed r1cs instances
#[ allow(dead_code) ]
#[ allow(dead_code) ]
pub fn new (
pub fn new (
params : Verification CircuitParams,
inputs : Option < Verification CircuitInputs< G > > ,
inner_circuit : Option < I C> ,
params : NIFSVerifier CircuitParams,
inputs : Option < NIFSVerifier CircuitInputs< G > > ,
step_circuit : Option < S C> ,
poseidon_constants : NovaPoseidonConstants < G ::Base > ,
poseidon_constants : NovaPoseidonConstants < G ::Base > ,
) -> Self
) -> Self
where
where
@ -127,18 +128,18 @@ where
Self {
Self {
params ,
params ,
inputs ,
inputs ,
inner _circuit,
step _circuit,
poseidon_constants ,
poseidon_constants ,
}
}
}
}
}
}
impl < G , I C> Circuit < < G as Group > ::Base > for Verification Circuit< G , I C>
impl < G , S C> Circuit < < G as Group > ::Base > for NIFSVerifier Circuit< G , S C>
where
where
G : Group ,
G : Group ,
< G as Group > ::Base : ff ::PrimeField + PrimeField + PrimeFieldBits ,
< G as Group > ::Base : ff ::PrimeField + PrimeField + PrimeFieldBits ,
< G as Group > ::Scalar : PrimeFieldBits ,
< G as Group > ::Scalar : PrimeFieldBits ,
IC : Inner Circuit< G ::Base > ,
SC : Step Circuit< G ::Base > ,
{
{
fn synthesize < CS : ConstraintSystem < < G as Group > ::Base > > (
fn synthesize < CS : ConstraintSystem < < G as Group > ::Base > > (
self ,
self ,
@ -304,7 +305,7 @@ where
// Allocate W
// Allocate W
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
// T = (x, y, infinity)
// W = (x, y, infinity)
let W_x = AllocatedNum ::alloc ( cs . namespace ( | | "W.x" ) , | | {
let W_x = AllocatedNum ::alloc ( cs . namespace ( | | "W.x" ) , | | {
Ok ( self . inputs . get ( ) ? . w . comm . to_coordinates ( ) . 0 )
Ok ( self . inputs . get ( ) ? . w . comm . to_coordinates ( ) . 0 )
} ) ? ;
} ) ? ;
@ -336,7 +337,7 @@ where
// Compute default values of U2':
// Compute default values of U2':
let zero_commitment = AllocatedPoint ::new ( zero . clone ( ) , zero . clone ( ) , one ) ;
let zero_commitment = AllocatedPoint ::new ( zero . clone ( ) , zero . clone ( ) , one ) ;
//W_default and E_default are a commitment to zero
// W_default and E_default are a commitment to zero
let W_default = zero_commitment . clone ( ) ;
let W_default = zero_commitment . clone ( ) ;
let E_default = zero_commitment ;
let E_default = zero_commitment ;
@ -501,7 +502,7 @@ where
. collect ::< Result < Vec < AllocatedNum < G ::Base > > , _ > > ( ) ? ;
. collect ::< Result < Vec < AllocatedNum < G ::Base > > , _ > > ( ) ? ;
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
//Compute i + 1
// Compute i + 1
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
let next_i = AllocatedNum ::alloc ( cs . namespace ( | | "i + 1" ) , | | {
let next_i = AllocatedNum ::alloc ( cs . namespace ( | | "i + 1" ) , | | {
@ -515,7 +516,7 @@ where
| lc | lc + next_i . get_variable ( ) - CS ::one ( ) - i . get_variable ( ) ,
| lc | lc + next_i . get_variable ( ) - CS ::one ( ) - i . get_variable ( ) ,
) ;
) ;
if self . inner _circuit. is_some ( ) {
if self . step _circuit. is_some ( ) {
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
//Allocate z0
//Allocate z0
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
@ -590,7 +591,7 @@ where
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
let z_next = self
let z_next = self
. inner _circuit
. step _circuit
. unwrap ( )
. unwrap ( )
. synthesize ( & mut cs . namespace ( | | "F" ) , z_i ) ? ;
. synthesize ( & mut cs . namespace ( | | "F" ) , z_i ) ? ;
@ -641,12 +642,12 @@ where
h1_hash . absorb ( u_r ) ;
h1_hash . absorb ( u_r ) ;
h1_hash . absorb ( i . clone ( ) ) ;
h1_hash . absorb ( i . clone ( ) ) ;
//absorb each of the limbs of X_r[0]
// absorb each of the limbs of X_r[0]
for limb in Xr0_bn . into_iter ( ) {
for limb in Xr0_bn . into_iter ( ) {
h1_hash . absorb ( limb ) ;
h1_hash . absorb ( limb ) ;
}
}
//absorb each of the limbs of X_r[1]
// absorb each of the limbs of X_r[1]
for limb in Xr1_bn . into_iter ( ) {
for limb in Xr1_bn . into_iter ( ) {
h1_hash . absorb ( limb ) ;
h1_hash . absorb ( limb ) ;
}
}
@ -698,12 +699,13 @@ where
#[ cfg(test) ]
#[ cfg(test) ]
mod tests {
mod tests {
use super ::* ;
use super ::* ;
use crate ::bellperson ::shape_cs ::ShapeCS ;
use crate ::bellperson ::solver ::SatisfyingAssignment ;
use crate ::bellperson ::{ shape_cs ::ShapeCS , solver ::SatisfyingAssignment } ;
type G1 = pasta_curves ::pallas ::Point ;
type G1 = pasta_curves ::pallas ::Point ;
type G2 = pasta_curves ::vesta ::Point ;
type G2 = pasta_curves ::vesta ::Point ;
use crate ::bellperson ::r1cs ::{ NovaShape , NovaWitness } ;
use crate ::commitments ::CommitTrait ;
use crate ::{
bellperson ::r1cs ::{ NovaShape , NovaWitness } ,
commitments ::CommitTrait ,
} ;
use std ::marker ::PhantomData ;
use std ::marker ::PhantomData ;
struct TestCircuit < F >
struct TestCircuit < F >
@ -713,7 +715,7 @@ mod tests {
_p : PhantomData < F > ,
_p : PhantomData < F > ,
}
}
impl < F > Inner Circuit< F > for TestCircuit < F >
impl < F > Step Circuit< F > for TestCircuit < F >
where
where
F : PrimeField + ff ::PrimeField ,
F : PrimeField + ff ::PrimeField ,
{
{
@ -729,12 +731,12 @@ mod tests {
#[ test ]
#[ test ]
fn test_verification_circuit ( ) {
fn test_verification_circuit ( ) {
// We experiment with 8 limbs of 32 bits each
// We experiment with 8 limbs of 32 bits each
let params = Verification CircuitParams ::new ( 32 , 8 ) ;
let params = NIFSVerifier CircuitParams ::new ( 32 , 8 ) ;
// The first circuit that verifies G2
// The first circuit that verifies G2
let poseidon_constants1 : NovaPoseidonConstants < < G2 as Group > ::Base > =
let poseidon_constants1 : NovaPoseidonConstants < < G2 as Group > ::Base > =
NovaPoseidonConstants ::new ( ) ;
NovaPoseidonConstants ::new ( ) ;
let circuit1 : Verification Circuit< G2 , TestCircuit < < G2 as Group > ::Base > > =
Verification Circuit ::new (
let circuit1 : NIFSVerifier Circuit< G2 , TestCircuit < < G2 as Group > ::Base > > =
NIFSVerifier Circuit ::new (
params . clone ( ) ,
params . clone ( ) ,
None ,
None ,
Some ( TestCircuit {
Some ( TestCircuit {
@ -745,8 +747,7 @@ mod tests {
// First create the shape
// First create the shape
let mut cs : ShapeCS < G1 > = ShapeCS ::new ( ) ;
let mut cs : ShapeCS < G1 > = ShapeCS ::new ( ) ;
let _ = circuit1 . synthesize ( & mut cs ) ;
let _ = circuit1 . synthesize ( & mut cs ) ;
let shape1 = cs . r1cs_shape ( ) ;
let gens1 = cs . r1cs_gens ( ) ;
let ( shape1 , gens1 ) = ( cs . r1cs_shape ( ) , cs . r1cs_gens ( ) ) ;
println ! (
println ! (
"Circuit1 -> Number of constraints: {}" ,
"Circuit1 -> Number of constraints: {}" ,
cs . num_constraints ( )
cs . num_constraints ( )
@ -755,28 +756,29 @@ mod tests {
// The second circuit that verifies G1
// The second circuit that verifies G1
let poseidon_constants2 : NovaPoseidonConstants < < G1 as Group > ::Base > =
let poseidon_constants2 : NovaPoseidonConstants < < G1 as Group > ::Base > =
NovaPoseidonConstants ::new ( ) ;
NovaPoseidonConstants ::new ( ) ;
let circuit2 : Verification Circuit< G1 , TestCircuit < < G1 as Group > ::Base > > =
Verification Circuit ::new ( params . clone ( ) , None , None , poseidon_constants2 ) ;
let circuit2 : NIFSVerifier Circuit< G1 , TestCircuit < < G1 as Group > ::Base > > =
NIFSVerifier Circuit ::new ( params . clone ( ) , None , None , poseidon_constants2 ) ;
// First create the shape
// First create the shape
let mut cs : ShapeCS < G2 > = ShapeCS ::new ( ) ;
let mut cs : ShapeCS < G2 > = ShapeCS ::new ( ) ;
let _ = circuit2 . synthesize ( & mut cs ) ;
let _ = circuit2 . synthesize ( & mut cs ) ;
let shape2 = cs . r1cs_shape ( ) ;
let gens2 = cs . r1cs_gens ( ) ;
let ( shape2 , gens2 ) = ( cs . r1cs_shape ( ) , cs . r1cs_gens ( ) ) ;
println ! (
println ! (
"Circuit2 -> Number of constraints: {}" ,
"Circuit2 -> Number of constraints: {}" ,
cs . num_constraints ( )
cs . num_constraints ( )
) ;
) ;
//TODO: We need to hardwire default hash or give it as input
// TODO: We need to hardwire default hash or give it as input
let default_hash = < < G2 as Group > ::Base as ff ::PrimeField > ::from_str_vartime (
let default_hash = < < G2 as Group > ::Base as ff ::PrimeField > ::from_str_vartime (
"332553638888022689042501686561503049809" ,
"332553638888022689042501686561503049809" ,
)
)
. unwrap ( ) ;
. unwrap ( ) ;
let T = vec ! [ < G2 as Group > ::Scalar ::zero ( ) ] . commit ( & gens2 . gens_E ) ;
let T = vec ! [ < G2 as Group > ::Scalar ::zero ( ) ] . commit ( & gens2 . gens_E ) ;
let w = vec ! [ < G2 as Group > ::Scalar ::zero ( ) ] . commit ( & gens2 . gens_E ) ;
let w = vec ! [ < G2 as Group > ::Scalar ::zero ( ) ] . commit ( & gens2 . gens_E ) ;
// Now get an assignment
// Now get an assignment
let mut cs : SatisfyingAssignment < G1 > = SatisfyingAssignment ::new ( ) ;
let mut cs : SatisfyingAssignment < G1 > = SatisfyingAssignment ::new ( ) ;
let inputs : Verification CircuitInputs< G2 > = Verification CircuitInputs ::new (
let inputs : NIFSVerifier CircuitInputs< G2 > = NIFSVerifier CircuitInputs ::new (
default_hash ,
default_hash ,
RelaxedR1CSInstance ::default ( & gens2 , & shape2 ) ,
RelaxedR1CSInstance ::default ( & gens2 , & shape2 ) ,
< < G2 as Group > ::Base as PrimeField > ::zero ( ) , // TODO: provide real inputs
< < G2 as Group > ::Base as PrimeField > ::zero ( ) , // TODO: provide real inputs
@ -787,8 +789,9 @@ mod tests {
T , // TODO: provide real inputs
T , // TODO: provide real inputs
w ,
w ,
) ;
) ;
let circuit : VerificationCircuit < G2 , TestCircuit < < G2 as Group > ::Base > > =
VerificationCircuit ::new (
let circuit : NIFSVerifierCircuit < G2 , TestCircuit < < G2 as Group > ::Base > > =
NIFSVerifierCircuit ::new (
params ,
params ,
Some ( inputs ) ,
Some ( inputs ) ,
Some ( TestCircuit {
Some ( TestCircuit {