diff --git a/src/circuits.rs b/src/circuits.rs index accda7d..8ebcee0 100644 --- a/src/circuits.rs +++ b/src/circuits.rs @@ -8,6 +8,7 @@ use ark_r1cs_std::{ fields::{fp::FpVar, nonnative::NonNativeFieldVar, FieldVar}, groups::GroupOpsBounds, prelude::CurveVar, + R1CSVar, ToBitsGadget, ToBytesGadget, ToConstraintFieldGadget, @@ -120,7 +121,6 @@ where phi3.cmW .enforce_equal(&(phi1.cmW + phi2.cmW.scalar_mul_le(r.to_bits_le()?.iter())?))?; - // wip x's check phi3.x.enforce_equal(&(phi1.x + r * phi2.x))?; Ok(()) } @@ -179,19 +179,22 @@ where let phiBigOut = PhiVar::::new_witness(cs.clone(), || Ok(self.phiBigOut.unwrap()))?; let cmT = GC::new_witness(cs.clone(), || Ok(self.cmT.unwrap()))?; + let r = NonNativeFieldVar::>::new_witness(cs.clone(), || { Ok(self.r.unwrap()) })?; // r will come from transcript - // if i=0, output H(vk_nifs, 1, z_0, z_i1, phi) - let phiOut_x = AugmentedFCircuit::::phi_x_hash_var( + let x = FpVar::>::new_input(cs.clone(), || Ok(self.x))?; + + // if i=0, output (φ_{i+1}.x), phiOut.x = H(vk_nifs, 1, z_0, z_i1, phi) + let phiOut_x_first_iter = AugmentedFCircuit::::phi_x_hash_var( cs.clone(), self.poseidon_config.clone(), FpVar::>::one(), z_0.clone(), z_i1.clone(), - phi.clone(), + phiBigOut.clone(), )?; // TODO WIP: x is the output when i=0 @@ -204,32 +207,37 @@ where z_i.clone(), phiBig.clone(), )?; - let x_CF = phi.x.to_constraint_field()?; // phi.x on the ConstraintF - // x_CF[0].enforce_equal(&h)?; // review + // check that h == phi.x. + // Note: phi.x is in ScalarField, while h is in ConstraintF (BaseField), that's why bytes + // are used in the comparison. + (phi.x.to_bytes()?).enforce_equal(&h.to_bytes()?)?; // TODO review // 2. phi.cmE==cm(0), phi.u==1 - // (phi.cmE.is_zero()?).enforce_equal(&Boolean::TRUE)?; // TODO check that cmE = cm(0) + // (phi.cmE.is_zero()?).enforce_equal(&Boolean::TRUE)?; // TODO not cmE=0, but check that cmE = cm(0) (phi.u.is_one()?).enforce_equal(&Boolean::TRUE)?; // 3. nifs.verify, checks that folding phi & phiBig obtains phiBigOut NIFSGadget::::verify(r, cmT, phi, phiBig, phiBigOut.clone())?; // 4. zksnark.V(vk_snark, phi_new, proof_phi) - // 5. phi.x == H(i+1, z_0, z_i+1, phiBigOut) - let h = AugmentedFCircuit::::phi_x_hash_var( + // 5. (φ_{i+1}.x) phiOut.x == H(i+1, z_0, z_i+1, phiBigOut) + let phiOut_x = AugmentedFCircuit::::phi_x_hash_var( cs.clone(), self.poseidon_config.clone(), i + FpVar::>::one(), z_0.clone(), z_i1.clone(), phiBigOut.clone(), - )?; - // WIP - let x_CF = phiBigOut.x.to_constraint_field()?; // phi.x on the ConstraintF - // x_CF[0].enforce_equal(&h)?; // TODO review + )?; // WIP + + // check that inputed 'x' is equal to phiOut_x_first_iter or phiOut_x depending if we're at + // i=0 or not. + // if i==0: check x==phiOut_x_first_iter + phiOut_x_first_iter.enforce_equal(&x)?; + // else: check x==phiOut_x // WIP assert that z_i1 == F(z_i).z_i1 - // self.F.generate_constraints(cs.clone())?; + self.F.generate_constraints(cs.clone())?; Ok(()) } @@ -494,6 +502,7 @@ mod test { let cs = ConstraintSystem::::new_ref(); + // note: gen_test_values ws is the F (internal) circuit witness only let (r1cs, ws, _) = nifs::gen_test_values::(2); let A = r1cs.A.clone(); @@ -504,7 +513,7 @@ mod test { let mut transcript_p = Transcript::::new(&poseidon_config_Fq); - let (_fw3, phi1, phi2, _T, cmT) = nifs::NIFS::::P( + let (_fw3, mut phi1, phi2, _T, cmT) = nifs::NIFS::::P( &mut transcript_p, &pedersen_params, r, @@ -512,15 +521,28 @@ mod test { fw1, fw2, ); - let phi3 = nifs::NIFS::::V(r, &phi1, &phi2, &cmT); - println!("phi1 {:?}", phi1.cmE); + // println!("phi1 {:?}", phi1.cmE); - let i = Fr::from(1_u32); + let i = Fr::from(0_u32); let z_0 = Fr::from(0_u32); let z_i = Fr::from(3_u32); let z_i1 = Fr::from(35_u32); let test_F_circuit = TestFCircuit:: { z_i, z_i1 }; + // TODO maybe phi.x should be set from fw1 (few lines above) + let phi1_x: Fr = + AugmentedFCircuit::>::phi_x_hash( + poseidon_config_Fr.clone(), + i, + z_0.clone(), + z_i.clone(), + phi2.clone(), // phiBig + ); + phi1.x = Fq::from_le_bytes_mod_order(&phi1_x.into_bigint().to_bytes_le()); + + // fold committed instance phi3 + let phi3 = nifs::NIFS::::V(r, &phi1, &phi2, &cmT); + let x = AugmentedFCircuit::>::phi_x_hash( poseidon_config_Fr.clone(), i + Fr::one(), diff --git a/src/ivc.rs b/src/ivc.rs index ce69c63..05f63da 100644 --- a/src/ivc.rs +++ b/src/ivc.rs @@ -1,6 +1,6 @@ use ark_crypto_primitives::sponge::Absorb; use ark_ec::{CurveGroup, Group}; -use ark_ff::{Field, PrimeField}; +use ark_ff::{BigInteger, Field, PrimeField}; use std::marker::PhantomData; use ark_crypto_primitives::sponge::poseidon::{PoseidonConfig, PoseidonSponge};