From 87671770e7f6008b812c192d7858960914a39c7e Mon Sep 17 00:00:00 2001 From: arnaucube Date: Sun, 30 Apr 2023 23:37:17 +0200 Subject: [PATCH] add initial IVC proof generation impl --- README.md | 2 +- src/circuits.rs | 36 ++++++++----- src/ivc.rs | 134 ++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 1 + src/nifs.rs | 8 +-- 5 files changed, 164 insertions(+), 17 deletions(-) create mode 100644 src/ivc.rs diff --git a/README.md b/README.md index c1044c6..fb1fe49 100644 --- a/README.md +++ b/README.md @@ -11,4 +11,4 @@ Thanks to [Levs57](https://twitter.com/levs57), [Nalin Bhardwaj](https://twitter ### Details _"Nova: Recursive Zero-Knowledge Arguments from Folding Schemes"_ (https://eprint.iacr.org/2021/370) by [Abhiram Kothapalli](https://twitter.com/abhiramko/), [Srinath Setty](https://twitter.com/srinathtv/), [Ioanna Tzialla](https://scholar.google.com/citations?user=IXTY4MYAAAAJ). -Current implementation uses a cycle of pairing-friendly curves with Groth16 for the folding proofs (as an example, the tests use MNT4, MNT6 curves), once the full scheme works, will see how many constraints the folding circuits need and might change one of the sides to a non-pairing curve with a non-pairing proof instead of Groth16. Eventually would like to explore also using BN254 with Grumpkin for ending up verifying the proofs in Ethereum. +Current implementation uses a cycle of pairing-friendly curves with Groth16 for the compressed IVC proofs (as an example, the tests use MNT4, MNT6 curves), once the full scheme works, will see how many constraints the circuits need and might change one of the sides to a non-pairing curve with a non-pairing proof instead of Groth16. Eventually would like to explore also using BN254 with Grumpkin for ending up verifying the proofs in Ethereum. diff --git a/src/circuits.rs b/src/circuits.rs index f35fe13..d40feab 100644 --- a/src/circuits.rs +++ b/src/circuits.rs @@ -125,17 +125,18 @@ pub struct AugmentedFCircuit>> where <::BaseField as Field>::BasePrimeField: Absorb, { - _c: PhantomData, - _gc: PhantomData, + pub _c: PhantomData, + pub _gc: PhantomData, - pub poseidon_native: PoseidonSponge>, + // pub poseidon_native: PoseidonSponge>, pub poseidon_config: PoseidonConfig>, pub i: Option, pub z_0: Option, pub z_i: Option, - pub phi: Option>, // phi in the paper sometimes appears as phi (φ) and others as 𝗎 - pub phiBig: Option>, - pub phiOut: Option>, + pub z_i1: Option, // z_{i+1} + pub phi: Option>, // phi_i in the paper sometimes appears as phi (φ) and others as 𝗎 + pub phiBig: Option>, // ϕ_i + pub phiOut: Option>, // ϕ_{i+1} pub cmT: Option, pub r: Option, // This will not be an input and derived from a hash internally in the circuit (poseidon transcript) } @@ -156,6 +157,7 @@ where let i = FpVar::>::new_witness(cs.clone(), || Ok(self.i.unwrap()))?; let z_0 = FpVar::>::new_witness(cs.clone(), || Ok(self.z_0.unwrap()))?; let z_i = FpVar::>::new_witness(cs.clone(), || Ok(self.z_i.unwrap()))?; + let z_i1 = FpVar::>::new_witness(cs.clone(), || Ok(self.z_i1.unwrap()))?; let phi = PhiVar::::new_witness(cs.clone(), || Ok(self.phi.unwrap()))?; let phiBig = PhiVar::::new_witness(cs.clone(), || Ok(self.phiBig.unwrap()))?; @@ -168,8 +170,9 @@ where })?; // r will come from transcript // 1. phi.x == H(vk_nifs, i, z_0, z_i, phiBig) - let mut sponge = PoseidonSpongeVar::>::new(cs, &self.poseidon_config); - let input = vec![i, z_0, z_i]; + let mut sponge = + PoseidonSpongeVar::>::new(cs.clone(), &self.poseidon_config); + let input = vec![i.clone(), z_0.clone(), z_i.clone()]; sponge.absorb(&input)?; let input = vec![ phiBig.u.to_constraint_field()?, @@ -182,15 +185,24 @@ where let x_CF = phi.x.to_constraint_field()?; // phi.x on the ConstraintF x_CF[0].enforce_equal(&h[0])?; // review - // // 2. phi.cmE==0, phi.u==1 - // >>::is_zero(&phi.cmE)?; + // 2. phi.cmE==0, phi.u==1 (phi.cmE.is_zero()?).enforce_equal(&Boolean::TRUE)?; (phi.u.is_one()?).enforce_equal(&Boolean::TRUE)?; - // 3. nifs.verify - NIFSGadget::::verify(r, cmT, phi, phiBig, phiOut)?; + // 3. nifs.verify, checks that folding phi & phiBig obtains phiOut + NIFSGadget::::verify(r, cmT, phi, phiBig, phiOut.clone())?; // 4. zksnark.V(vk_snark, phi_new, proof_phi) + // 5. phiOut.x == H(i+1, z_0, z_i+1, phiOut) + // WIP + let mut sponge = PoseidonSpongeVar::>::new(cs, &self.poseidon_config); + let input = vec![i + FpVar::>::one(), z_0, z_i1]; + sponge.absorb(&input)?; + let input = vec![phiOut.cmE.to_bytes()?, phiOut.cmW.to_bytes()?]; + sponge.absorb(&input)?; + let h = sponge.squeeze_field_elements(1).unwrap(); + let x_CF = phiOut.x.to_constraint_field()?; // phi.x on the ConstraintF + x_CF[0].enforce_equal(&h[0])?; // review Ok(()) } diff --git a/src/ivc.rs b/src/ivc.rs new file mode 100644 index 0000000..9d53db5 --- /dev/null +++ b/src/ivc.rs @@ -0,0 +1,134 @@ +use ark_crypto_primitives::sponge::Absorb; +use ark_ec::{CurveGroup, Group}; +use ark_ff::{Field, PrimeField}; +use std::marker::PhantomData; + +use ark_crypto_primitives::sponge::poseidon::{PoseidonConfig, PoseidonSponge}; +use ark_r1cs_std::{groups::GroupOpsBounds, prelude::CurveVar}; +use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError}; + +use crate::circuits::{AugmentedFCircuit, ConstraintF}; +use crate::nifs::{FWit, Phi, NIFS, R1CS}; +use crate::pedersen::{Commitment, Params as PedersenParams, Pedersen, Proof as PedersenProof}; +use crate::transcript::Transcript; + +use ark_std::{One, Zero}; +use core::ops::Deref; + +pub struct IVCProof { + phi: Phi, + // w: FWit, + w: Vec, + phiBig: Phi, + // W: FWit, + W: Vec, +} + +pub struct IVC< + C1: CurveGroup, + GC1: CurveVar>, + C2: CurveGroup, + GC2: CurveVar>, +> where + C1: CurveGroup::ScalarField>, + C2: CurveGroup::ScalarField>, +{ + _c1: PhantomData, + _gc1: PhantomData, + _c2: PhantomData, + _gc2: PhantomData, + + pub poseidon_config: PoseidonConfig>, + pub pedersen_params_C1: PedersenParams, + pub pedersen_params_C2: PedersenParams, +} + +impl< + C1: CurveGroup, + GC1: CurveVar>, + C2: CurveGroup, + GC2: CurveVar>, + > IVC +where + for<'a> &'a GC1: GroupOpsBounds<'a, C1, GC1>, + for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>, + C1: CurveGroup::ScalarField>, + C2: CurveGroup::ScalarField>, + + ::ScalarField: Absorb, + ::BaseField: Absorb, + <::BaseField as Field>::BasePrimeField: Absorb, + ::BaseField: PrimeField, + // 2 + ::ScalarField: Absorb, + ::BaseField: Absorb, + <::BaseField as Field>::BasePrimeField: Absorb, + ::BaseField: PrimeField, +{ + pub fn prove( + &self, + cs: ConstraintSystemRef>, + tr1: &mut Transcript, + tr2: &mut Transcript, + r1cs: &R1CS, + i: C1::ScalarField, + z_0: C1::ScalarField, + z_i: C1::ScalarField, + // phi1: &Phi, + // phi2: &Phi, + fw1: FWit, + fw2: FWit, + ) -> Result, SynthesisError> { + tr1.get_challenge(); + let r = tr2.get_challenge(); // TODO transcript usage is still WIP, will update with expected adds & gets + + // fold phi_i and phiBig_i + let (fw3, phi1, phi2, _T, cmT) = + NIFS::::P(tr2, &self.pedersen_params_C2, r, r1cs, fw1, fw2); + let phi3 = NIFS::::V(r, &phi1, &phi2, &cmT); + + // TODO compute z_{i+1} + let z_i1 = z_i.clone(); // WIP this will be the actual computed z_{i+1} + + let c = AugmentedFCircuit:: { + _c: PhantomData, + _gc: PhantomData, + poseidon_config: self.poseidon_config.clone(), + i: Some(i), + z_0: Some(z_0), + z_i: Some(z_i), + z_i1: Some(z_i1), + phi: Some(phi1), + phiBig: Some(phi2), + phiOut: Some(phi3.clone()), + cmT: Some(cmT.0), + r: Some(r), + }; + + c.generate_constraints(cs.clone())?; + + // get w_{i+1} + let cs1 = cs.borrow().unwrap(); + let cs2 = cs1.deref(); + let w_i1 = cs2.witness_assignment.clone(); + let x_i1 = cs2.instance_assignment.clone(); + + let rW = tr1.get_challenge(); + let _ = tr2.get_challenge(); + + // phi_{i+1} small + let phi = Phi:: { + cmE: Commitment::(C1::zero()), + u: C1::ScalarField::one(), + cmW: Pedersen::commit(&self.pedersen_params_C1, &w_i1, &rW), + x: x_i1[0], // check if pos 0 is 1 + }; + + Ok(IVCProof { + phiBig: phi3, + W: fw3.W, + phi, // phi_{i+1} + w: w_i1, // w_{i+1} + }) + } +} diff --git a/src/lib.rs b/src/lib.rs index 2392260..c91499a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,6 +6,7 @@ #![allow(dead_code)] // TMP mod circuits; +mod ivc; mod nifs; mod pedersen; mod sumcheck; diff --git a/src/nifs.rs b/src/nifs.rs index 6a795e5..48acb0c 100644 --- a/src/nifs.rs +++ b/src/nifs.rs @@ -26,10 +26,10 @@ pub struct Phi { // FWit: Folded Witness pub struct FWit { - E: Vec, - rE: C::ScalarField, - W: Vec, - rW: C::ScalarField, + pub E: Vec, + pub rE: C::ScalarField, + pub W: Vec, + pub rW: C::ScalarField, } impl FWit