diff --git a/Cargo.toml b/Cargo.toml index 8da4f31..12132b1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,31 +13,34 @@ edition = "2018" ################################# Dependencies ################################ [dependencies] -ark-serialize = { git = "https://github.com/arkworks-rs/algebra", default-features = false, features = [ "derive" ] } -ark-ff = { git = "https://github.com/arkworks-rs/algebra", default-features = false } -ark-ec = { git = "https://github.com/arkworks-rs/algebra", default-features = false } -ark-poly = { git = "https://github.com/arkworks-rs/algebra", default-features = false } +ark-serialize = { version = "^0.2.0", default-features = false, features = [ "derive" ] } +ark-ff = { version = "^0.2.0", default-features = false } +ark-ec = { version = "^0.2.0", default-features = false } +ark-poly = { version = "^0.2.0", default-features = false } -ark-std = { git = "https://github.com/arkworks-rs/utils", default-features = false } +ark-std = { version = "^0.2.0", default-features = false } -ark-relations = { git = "https://github.com/arkworks-rs/snark", default-features = false } -ark-crypto-primitives = { git = "https://github.com/arkworks-rs/crypto-primitives", default-features = false, branch = "main", features = [ "r1cs" ] } +ark-relations = { version = "^0.2.0", default-features = false } +ark-crypto-primitives = { version = "^0.2.0", default-features = false, features = [ "r1cs" ] } -ark-r1cs-std = { git = "https://github.com/arkworks-rs/r1cs-std", default-features = false } +ark-r1cs-std = { version = "^0.2.0", default-features = false } ark-nonnative-field = { git = "https://github.com/arkworks-rs/nonnative", default-features = false } -ark-snark = { git = "https://github.com/arkworks-rs/snark", default-features = false } +ark-snark = { version = "^0.2.0", default-features = false } -ark-ed-on-mnt4-298 = { git = "https://github.com/arkworks-rs/curves", default-features = false } -ark-ed-on-bls12-381 = { git = "https://github.com/arkworks-rs/curves", default-features = false } -ark-mnt4-298 = { git = "https://github.com/arkworks-rs/curves", default-features = false, features = [ "curve", "r1cs" ] } -ark-mnt6-298 = { git = "https://github.com/arkworks-rs/curves", default-features = false, features = [ "r1cs" ] } +ark-accumulation = { git = "https://github.com/arkworks-rs/accumulation/", branch = "main", default-features = false, features = [ "r1cs-nark-as", "r1cs" ] } +ark-sponge = { git = "https://github.com/arkworks-rs/sponge/", branch = "accumulation-experimental", default-features = false, features = [ "r1cs" ] } + +ark-ed-on-mnt4-298 = { version = "^0.2.0", default-features = false } +ark-ed-on-bls12-381 = { version = "^0.2.0", default-features = false } +ark-mnt4-298 = { version = "^0.2.0", default-features = false, features = [ "curve", "r1cs" ] } +ark-mnt6-298 = { version = "^0.2.0", default-features = false, features = [ "r1cs" ] } rand_chacha = { version = "0.2.1", default-features = false } derivative = { version = "2.0", features = ["use_core"] } -ark-groth16 = { git = "https://github.com/arkworks-rs/groth16", features = [ "r1cs" ], default-features = false } -ark-gm17 = { git = "https://github.com/arkworks-rs/gm17", features = [ "r1cs" ], default-features = false } +ark-groth16 = { version = "^0.2.0", features = [ "r1cs" ], default-features = false } +ark-gm17 = { version = "^0.2.0", features = [ "r1cs" ], default-features = false } ark-marlin = { git = "https://github.com/arkworks-rs/marlin", branch = "constraints", default-features = false } ark-poly-commit = { git = "https://github.com/arkworks-rs/poly-commit", branch = "constraints", default-features = false, features = [ "r1cs" ] } diff --git a/src/ec_cycle_pcd/mod.rs b/src/ec_cycle_pcd/mod.rs index 3b374e6..528ee23 100644 --- a/src/ec_cycle_pcd/mod.rs +++ b/src/ec_cycle_pcd/mod.rs @@ -16,6 +16,7 @@ use ark_r1cs_std::{ use ark_relations::r1cs::{ ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, OptimizationGoal, SynthesisError, }; +use ark_sponge::Absorbable; use ark_std::rand::{CryptoRng, Rng, RngCore}; use ark_std::{boxed::Box, marker::PhantomData, vec::Vec}; @@ -253,12 +254,15 @@ where { } -pub struct BoundTestingPredicate + Clone> { +pub struct BoundTestingPredicate< + F: PrimeField + Absorbable, + BoundCircuit: ConstraintSynthesizer + Clone, +> { pub bound_circuit: BoundCircuit, pub field_phantom: PhantomData, } -impl + Clone> Clone +impl, BoundCircuit: ConstraintSynthesizer + Clone> Clone for BoundTestingPredicate { fn clone(&self) -> Self { @@ -269,7 +273,7 @@ impl + Clone> Clone } } -impl + Clone> PCDPredicate +impl, BoundCircuit: ConstraintSynthesizer + Clone> PCDPredicate for BoundTestingPredicate { type Message = F; @@ -301,9 +305,11 @@ impl + Clone> PCDPredicate } } -impl> - UniversalSetupPCD for ECCyclePCD +impl UniversalSetupPCD for ECCyclePCD where + MainField: PrimeField + Absorbable, + HelpField: PrimeField + Absorbable, + IC: ECCyclePCDConfig, IC::MainSNARK: UniversalSetupSNARK, IC::HelpSNARK: UniversalSetupSNARK, IC::MainSNARKGadget: UniversalSetupSNARKGadget, diff --git a/src/error.rs b/src/error.rs new file mode 100644 index 0000000..9614fe5 --- /dev/null +++ b/src/error.rs @@ -0,0 +1,31 @@ +use ark_std::error::Error; + +/// Common errors that PCD schemes may throw. +#[derive(Debug)] +pub enum PCDError { + /// The number of prior messages does not match the predicate. + InvalidPriorMessagesLength(usize, usize), + + /// The number of prior proofs does not match the predicate. + InvalidPriorProofsLength(usize, usize), +} + +impl core::fmt::Display for PCDError { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + let error_text = match self { + PCDError::InvalidPriorMessagesLength(expected, actual) => format!( + "Expected the number of prior messages to be `{}` but got `{}` instead", + expected, actual + ), + + PCDError::InvalidPriorProofsLength(expected, actual) => format!( + "Expected the number of prior proofs to be `{}` but got `{}` instead", + expected, actual + ), + }; + + write!(f, "{}", error_text) + } +} + +impl Error for PCDError {} diff --git a/src/lib.rs b/src/lib.rs index 034c4ea..0ffdd6b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -7,14 +7,19 @@ use ark_r1cs_std::alloc::AllocVar; use ark_r1cs_std::bits::boolean::Boolean; use ark_r1cs_std::ToBytesGadget; use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError}; +use ark_sponge::constraints::AbsorbableGadget; +use ark_sponge::Absorbable; use ark_std::rand::{CryptoRng, RngCore}; use ark_std::{boxed::Box, fmt::Debug}; +#[macro_use] +extern crate derivative; + pub type Error = Box; pub trait PCDPredicate: Clone { - type Message: ToBytes + Sized + Clone + Default; - type MessageVar: ToBytesGadget + AllocVar; + type Message: Absorbable + ToBytes + Sized + Clone + Default; + type MessageVar: AbsorbableGadget + ToBytesGadget + AllocVar; type LocalWitness: Sized + Clone + Default; type LocalWitnessVar: AllocVar; @@ -76,5 +81,190 @@ pub trait UniversalSetupPCD: PCD { ) -> Result<(>::ProvingKey, >::VerifyingKey), Error>; } +/// Common errors that PCD schemes may throw. +pub mod error; + pub mod ec_cycle_pcd; pub mod variable_length_crh; + +/// A PCD that does not rely on SNARKs but instead builds on an R1CS NARK construction and its +/// accumulation scheme. +/// The implementation is based on the construction detailed in Section 5 of [\[BCLMS20\]][bclms20]. +/// +/// [bclms20]: https://eprint.iacr.org/2020/1618 +pub mod r1cs_nark_pcd; + +#[cfg(test)] +pub mod tests { + use crate::{PCDPredicate, PCD}; + use ark_ff::PrimeField; + use ark_r1cs_std::bits::boolean::Boolean; + use ark_r1cs_std::eq::EqGadget; + use ark_r1cs_std::fields::fp::FpVar; + use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError}; + use ark_sponge::Absorbable; + use ark_std::marker::PhantomData; + + #[derive(Clone)] + pub struct TestIVCPredicate> { + pub field_phantom: PhantomData, + } + + impl> TestIVCPredicate { + fn new() -> Self { + Self { + field_phantom: PhantomData, + } + } + } + + impl> PCDPredicate for TestIVCPredicate { + type Message = F; + type MessageVar = FpVar; + type LocalWitness = F; + type LocalWitnessVar = FpVar; + + const PRIOR_MSG_LEN: usize = 1; + + fn generate_constraints( + &self, + _cs: ConstraintSystemRef, + msg: &Self::MessageVar, + witness: &Self::LocalWitnessVar, + prior_msgs: &[Self::MessageVar], + _base_case: &Boolean, + ) -> Result<(), SynthesisError> { + let msg_supposed = &prior_msgs[0] + witness; + msg_supposed.enforce_equal(&msg)?; + + Ok(()) + } + } + + #[derive(Clone)] + pub struct TestPCDPredicate> { + pub field_phantom: PhantomData, + } + + impl> TestPCDPredicate { + fn new() -> Self { + Self { + field_phantom: PhantomData, + } + } + } + + impl> PCDPredicate for TestPCDPredicate { + type Message = F; + type MessageVar = FpVar; + type LocalWitness = F; + type LocalWitnessVar = FpVar; + + const PRIOR_MSG_LEN: usize = 2; + + fn generate_constraints( + &self, + _cs: ConstraintSystemRef, + msg: &Self::MessageVar, + witness: &Self::LocalWitnessVar, + prior_msgs: &[Self::MessageVar], + _base_case: &Boolean, + ) -> Result<(), SynthesisError> { + let msg_supposed = &prior_msgs[0] + &prior_msgs[1] + witness; + msg_supposed.enforce_equal(&msg)?; + + Ok(()) + } + } + + pub fn test_ivc_base_case, TestPCD: PCD>() { + let mut rng = ark_std::test_rng(); + + let witness = F::one(); + let msg_0 = F::one(); + + let circ = TestIVCPredicate::::new(); + let (pk, vk) = TestPCD::circuit_specific_setup(&circ, &mut rng).unwrap(); + + let proof_0 = TestPCD::prove(&pk, &circ, &msg_0, &witness, &[], &[], &mut rng).unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_0, &proof_0).unwrap()); + } + + pub fn test_ivc, TestPCD: PCD>() { + let mut rng = ark_std::test_rng(); + + let witness = F::one(); + let msg_0 = F::one(); + let msg_1 = msg_0 + &witness; + let msg_2 = msg_1 + &witness; + + let circ = TestIVCPredicate::::new(); + let (pk, vk) = TestPCD::circuit_specific_setup(&circ, &mut rng).unwrap(); + + let proof_0 = TestPCD::prove(&pk, &circ, &msg_0, &witness, &[], &[], &mut rng).unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_0, &proof_0).unwrap()); + + let proof_1 = TestPCD::prove( + &pk, + &circ, + &msg_1, + &witness, + &[msg_0], + &vec![proof_0], + &mut rng, + ) + .unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_1, &proof_1).unwrap()); + + let proof_2 = TestPCD::prove( + &pk, + &circ, + &msg_2, + &witness, + &[msg_1], + &vec![proof_1], + &mut rng, + ) + .unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_2, &proof_2).unwrap()); + } + + pub fn test_pcd, TestPCD: PCD>() { + let mut rng = ark_std::test_rng(); + + let witness = F::one(); + let msg_0 = F::one(); + let msg_1 = msg_0 + &msg_0 + &witness; + let msg_2 = msg_1 + &msg_1 + &witness; + + let circ = TestPCDPredicate::::new(); + let (pk, vk) = TestPCD::circuit_specific_setup(&circ, &mut rng).unwrap(); + + let proof_0 = TestPCD::prove(&pk, &circ, &msg_0, &witness, &[], &[], &mut rng).unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_0, &proof_0).unwrap()); + + let proof_1 = TestPCD::prove( + &pk, + &circ, + &msg_1, + &witness, + &[msg_0, msg_0], + &vec![proof_0.clone(), proof_0], + &mut rng, + ) + .unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_1, &proof_1).unwrap()); + + let proof_2 = TestPCD::prove( + &pk, + &circ, + &msg_2, + &witness, + &[msg_1, msg_1], + &vec![proof_1.clone(), proof_1], + &mut rng, + ) + .unwrap(); + assert!(TestPCD::verify::>(&vk, &msg_2, &proof_2).unwrap()); + } +} diff --git a/src/r1cs_nark_pcd/data_structures.rs b/src/r1cs_nark_pcd/data_structures.rs new file mode 100644 index 0000000..a0f3e94 --- /dev/null +++ b/src/r1cs_nark_pcd/data_structures.rs @@ -0,0 +1,80 @@ +use ark_accumulation::r1cs_nark_as; +use ark_accumulation::r1cs_nark_as::{r1cs_nark, AccumulatorInstance, AccumulatorWitness}; +use ark_ec::{AffineCurve, CurveCycle}; + +pub(crate) type MainAffine = ::E1; +pub(crate) type HelpAffine = ::E2; + +pub(crate) type MainField = <::E2 as AffineCurve>::BaseField; +pub(crate) type HelpField = <::E2 as AffineCurve>::ScalarField; + +pub(crate) type MainProjective = as AffineCurve>::Projective; +pub(crate) type HelpProjective = as AffineCurve>::Projective; + +/// The proving key of [`R1CSNarkPCD`][nark_pcd]. +/// +/// [nark_pcd]: crate::r1cs_nark_pcd::R1CSNarkPCD +#[derive(Derivative)] +#[derivative(Clone(bound = "E: CurveCycle"))] +pub struct ProvingKey { + /// The key for accumulating arguments about the main circuit. + pub(crate) main_apk: r1cs_nark_as::ProverKey>, + + /// The key for verifying the accumulation of arguments about the main circuit. + pub(crate) main_avk: r1cs_nark_as::VerifierKey, + + /// The key for accumulating arguments about the help circuit. + pub(crate) help_apk: r1cs_nark_as::ProverKey>, + + /// The key for verifying the accumulation of arguments about the help circuit. + pub(crate) help_avk: r1cs_nark_as::VerifierKey, +} + +/// The verifying key of [`R1CSNarkPCD`][nark_pcd]. +/// +/// [nark_pcd]: crate::r1cs_nark_pcd::R1CSNarkPCD +#[derive(Derivative)] +#[derivative(Clone(bound = "E: CurveCycle"))] +pub struct VerifyingKey { + /// The key for verifying the accumulation of arguments about the main circuit. + pub(crate) main_avk: r1cs_nark_as::VerifierKey, + + /// The key for verifying the accumulation of arguments about the help circuit. + pub(crate) help_avk: r1cs_nark_as::VerifierKey, + + /// The key for verifying the arguments about the main circuit. + pub(crate) main_ivk: r1cs_nark::IndexVerifierKey>, + + /// The key for verifying the arguments about the help circuit. + pub(crate) help_ivk: r1cs_nark::IndexVerifierKey>, +} + +/// The proof of [`R1CSNarkPCD`][nark_pcd]. +/// +/// [nark_pcd]: crate::r1cs_nark_pcd::R1CSNarkPCD +#[derive(Derivative)] +#[derivative(Clone(bound = "E: CurveCycle"))] +pub struct Proof +where + E: CurveCycle, +{ + /// A proof attesting that the R1CS relation of the main circuit holds in the most recent step. + pub(crate) main_nark_proof: r1cs_nark::Proof>, + + /// A proof attesting that the R1CS relation of the help circuit holds in the most recent step. + pub(crate) help_nark_proof: r1cs_nark::Proof>, + + /// An accumulator used to determine whether all of the arguments for the main circuit is + /// verified to be true. + pub(crate) main_accumulator: ( + AccumulatorInstance>, + AccumulatorWitness>, + ), + + /// An accumulator used to determine whether all of the arguments for the help circuit is + /// verified to be true. + pub(crate) help_accumulator: ( + AccumulatorInstance>, + AccumulatorWitness>, + ), +} diff --git a/src/r1cs_nark_pcd/help_circuit.rs b/src/r1cs_nark_pcd/help_circuit.rs new file mode 100644 index 0000000..a184b0e --- /dev/null +++ b/src/r1cs_nark_pcd/help_circuit.rs @@ -0,0 +1,267 @@ +use crate::r1cs_nark_pcd::data_structures::{HelpAffine, HelpField, MainAffine, MainField}; +use crate::r1cs_nark_pcd::main_circuit::MainCircuit; +use crate::r1cs_nark_pcd::{R1CSNarkPCDConfig, MAKE_ZK}; +use crate::PCDPredicate; +use ark_accumulation::constraints::ASVerifierGadget; +use ark_accumulation::r1cs_nark_as; +use ark_accumulation::r1cs_nark_as::constraints::{ + ASForR1CSNarkVerifierGadget, AccumulatorInstanceVar, InputInstanceVar, +}; +use ark_accumulation::r1cs_nark_as::{AccumulatorInstance, InputInstance}; +use ark_ec::CurveCycle; +use ark_ff::{PrimeField, Zero}; +use ark_r1cs_std::alloc::AllocVar; +use ark_r1cs_std::bits::boolean::Boolean; +use ark_r1cs_std::eq::EqGadget; +use ark_r1cs_std::fields::fp::FpVar; +use ark_relations::ns; +use ark_relations::r1cs::{ + ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError, +}; +use ark_sponge::constraints::CryptographicSpongeVar; +use ark_sponge::{absorb, absorb_gadget, Absorbable, CryptographicSponge}; +use ark_std::marker::PhantomData; + +/// A circuit used to verify that the accumulation of arguments about the main circuit was computed +/// correctly. +#[derive(Derivative)] +#[derivative(Clone(bound = "E: CurveCycle"))] +pub(crate) struct HelpCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + /// The key for verifying the accumulation of arguments about the main circuit. + pub(crate) main_avk: r1cs_nark_as::VerifierKey, + + /// The accumulation input instances of the arguments about the main circuit in the previous + /// step. + pub(crate) main_accumulation_input_instances: Option>>>, + + /// The old accumulators that have accumulated arguments about the main circuit in the previous + /// step. + pub(crate) main_old_accumulator_instances: Option>>>, + + /// The new accumulator computed from accumulating arguments and accumulators of the main + /// circuit of the previous step. + pub(crate) main_new_accumulator_instance: AccumulatorInstance>, + + /// The new proof computed from accumulating arguments and accumulators of the main + /// circuit of the previous step. + pub(crate) main_accumulation_proof: r1cs_nark_as::Proof>, + + #[doc(hidden)] + pub(crate) _config_phantom: PhantomData, + + #[doc(hidden)] + pub(crate) _predicate_phantom: PhantomData

, +} + +impl HelpCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + /// Returns the public input size of the help circuit. + pub(crate) fn public_input_size() -> usize { + let cs = ConstraintSystem::>::new_ref(); + let _hash = FpVar::new_input(cs.clone(), || Ok(HelpField::::zero())).unwrap(); + return cs.num_instance_variables(); + } + + /// Computes a hash of the following elements. + pub(crate) fn compute_hash( + main_avk: &r1cs_nark_as::VerifierKey, + main_accumulator_instance: &AccumulatorInstance>, + ) -> HelpField { + let mut sponge = PC::HelpSponge::new(); + absorb!(&mut sponge, main_avk, main_accumulator_instance); + sponge.squeeze_field_elements(1).pop().unwrap() + } + + /// Computes a hash of the following elements in the constraint system. + pub(crate) fn compute_hash_var( + cs: ConstraintSystemRef>, + main_avk_var: &r1cs_nark_as::constraints::VerifierKeyVar>, + main_accumulator_instance_var: &AccumulatorInstanceVar, PC::MainCurveVar>, + ) -> Result>, SynthesisError> { + let mut sponge = PC::HelpSpongeVar::new(cs); + absorb_gadget!(&mut sponge, main_avk_var, main_accumulator_instance_var); + Ok(sponge.squeeze_field_elements(1)?.pop().unwrap()) + } + + /// Computes the public input of the help circuit. + pub(crate) fn compute_public_input( + main_avk: &r1cs_nark_as::VerifierKey, + main_accumulator_instance: &AccumulatorInstance>, + ) -> Result>, SynthesisError> { + let cs = ConstraintSystem::>::new_ref(); + + let _hash = FpVar::new_input(cs.clone(), || { + Ok(Self::compute_hash(main_avk, main_accumulator_instance)) + })?; + + let r1cs_input = cs.borrow().unwrap().instance_assignment.clone(); + Ok(r1cs_input) + } +} + +impl ConstraintSynthesizer> for HelpCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + fn generate_constraints( + self, + cs: ConstraintSystemRef>, + ) -> Result<(), SynthesisError> { + let HelpCircuit { + main_avk, + main_accumulation_input_instances: main_input_instances, + main_old_accumulator_instances, + main_new_accumulator_instance, + mut main_accumulation_proof, + _config_phantom, + _predicate_phantom, + } = self; + + // Ensure that prior data exist together. + assert_eq!( + main_input_instances.is_some(), + main_old_accumulator_instances.is_some() + ); + + // Ensure that prior data has the correct length. + assert!( + main_input_instances.is_none() + || main_input_instances.as_ref().unwrap().len() == P::PRIOR_MSG_LEN + ); + + assert!( + main_old_accumulator_instances.is_none() + || main_old_accumulator_instances.as_ref().unwrap().len() == P::PRIOR_MSG_LEN + ); + + // Process the inputs + + let base_case = main_input_instances.is_none(); + let main_circuit_input_len = MainCircuit::::public_input_size(); + let (main_input_instances, main_old_accumulator_instances) = if base_case { + ( + vec![InputInstance::zero(main_circuit_input_len, MAKE_ZK); P::PRIOR_MSG_LEN], + vec![AccumulatorInstance::placeholder(main_circuit_input_len); P::PRIOR_MSG_LEN], + ) + } else { + ( + main_input_instances.unwrap(), + main_old_accumulator_instances.unwrap(), + ) + }; + + let claimed_input_hash: HelpField = + Self::compute_hash(&main_avk, &main_new_accumulator_instance); + + // In the base case, the size of the proof will be incorrect due to the low and high + // T commitments in the underlying HP_AS proof. We substitute the base case proof with a + // dummy proof to ensure the size of the circuit remains constant. We are able to do so + // because the result of the r1cs_nark_as verify does not matter in the base case. + if base_case { + main_accumulation_proof = r1cs_nark_as::Proof::placeholder( + main_circuit_input_len, + P::PRIOR_MSG_LEN * 2, + MAKE_ZK, + ); + }; + + // Allocation + + let claimed_input_hash_var = FpVar::new_input(ns!(cs, "alloc_claimed_input_hash"), || { + Ok(claimed_input_hash) + })?; + + let base_case_var = Boolean::new_witness(ns!(cs, "alloc_base_case_bit"), || Ok(base_case))?; + + let main_avk_var = r1cs_nark_as::constraints::VerifierKeyVar::new_witness( + ns!(cs, "alloc_main_avk"), + || Ok(main_avk), + )?; + + let main_input_instance_vars = main_input_instances + .into_iter() + .map(|input_instance| { + InputInstanceVar::, PC::MainCurveVar>::new_witness( + ns!(cs, "alloc_main_input_instances"), + || Ok(input_instance), + ) + }) + .collect::, SynthesisError>>()?; + + let main_old_accumulator_instance_vars = main_old_accumulator_instances + .into_iter() + .map(|accumulator_instance| { + AccumulatorInstanceVar::, PC::MainCurveVar>::new_witness( + ns!(cs, "alloc_main_old_accumulator_instances"), + || Ok(accumulator_instance), + ) + }) + .collect::, SynthesisError>>()?; + + let main_new_accumulator_instance_var = + AccumulatorInstanceVar::, PC::MainCurveVar>::new_witness( + ns!(cs, "alloc_main_new_accumulator_instance"), + || Ok(main_new_accumulator_instance), + )?; + + let main_accumulation_proof_var = + r1cs_nark_as::constraints::ProofVar::, PC::MainCurveVar>::new_witness( + ns!(cs, "alloc_main_accumulation_proof"), + || Ok(main_accumulation_proof), + )?; + + // Verification + + let input_hash_var: FpVar> = Self::compute_hash_var( + ns!(cs, "input_hash_sponge").cs(), + &main_avk_var, + &main_new_accumulator_instance_var, + )?; + + input_hash_var.enforce_equal(&claimed_input_hash_var)?; + + let as_verify = ASForR1CSNarkVerifierGadget::< + MainAffine, + PC::MainCurveVar, + PC::HelpSponge, + PC::HelpSpongeVar, + >::verify( + ns!(cs, "main_accumulation_verify").cs(), + &main_avk_var, + &main_input_instance_vars, + &main_old_accumulator_instance_vars, + &main_new_accumulator_instance_var, + &main_accumulation_proof_var, + None, + )?; + + base_case_var + .or(&as_verify)? + .enforce_equal(&Boolean::TRUE)?; + + Ok(()) + } +} diff --git a/src/r1cs_nark_pcd/main_circuit.rs b/src/r1cs_nark_pcd/main_circuit.rs new file mode 100644 index 0000000..5c47bbd --- /dev/null +++ b/src/r1cs_nark_pcd/main_circuit.rs @@ -0,0 +1,315 @@ +use crate::r1cs_nark_pcd::data_structures::{HelpAffine, HelpField, MainAffine, MainField}; +use crate::r1cs_nark_pcd::help_circuit::HelpCircuit; +use crate::r1cs_nark_pcd::{R1CSNarkPCDConfig, MAKE_ZK}; +use crate::PCDPredicate; +use ark_accumulation::constraints::ASVerifierGadget; +use ark_accumulation::r1cs_nark_as; +use ark_accumulation::r1cs_nark_as::constraints::{ + ASForR1CSNarkVerifierGadget, AccumulatorInstanceVar, InputInstanceVar, +}; +use ark_accumulation::r1cs_nark_as::{AccumulatorInstance, InputInstance}; +use ark_ec::CurveCycle; +use ark_ff::{PrimeField, Zero}; +use ark_r1cs_std::alloc::AllocVar; +use ark_r1cs_std::bits::boolean::Boolean; +use ark_r1cs_std::eq::EqGadget; +use ark_r1cs_std::fields::fp::FpVar; +use ark_relations::ns; +use ark_relations::r1cs::{ + ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError, +}; +use ark_sponge::constraints::CryptographicSpongeVar; +use ark_sponge::{absorb, absorb_gadget, Absorbable, CryptographicSponge}; +use ark_std::marker::PhantomData; + +/// A circuit used to verify that the accumulation of arguments about the help circuit was computed +/// correctly and that the PCD predicate holds for the new message. +#[derive(Derivative)] +#[derivative(Clone(bound = "E: CurveCycle"))] +pub(crate) struct MainCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + /// The PCD predicate. + pub(crate) predicate: P, + + /// The new PCD message. + pub(crate) msg: P::Message, + + /// The local PCD witness. + pub(crate) witness: P::LocalWitness, + + /// PCD messages from the previous step. + pub(crate) prior_msgs: Option>, + + /// The key for verifying the accumulation of arguments about the help circuit. + pub(crate) help_avk: r1cs_nark_as::VerifierKey, + + /// The accumulation input instances of the arguments about the help circuit in the previous + /// step. + pub(crate) help_accumulation_input_instances: Option>>>, + + /// The old accumulators that have accumulated arguments about the help circuit in the previous + /// step. + pub(crate) help_old_accumulator_instances: Option>>>, + + /// The new accumulator computed from accumulating arguments and accumulators of the help + /// circuit of the previous step. + pub(crate) help_new_accumulator_instance: AccumulatorInstance>, + + /// The new proof computed from accumulating arguments and accumulators of the help + /// circuit of the previous step. + pub(crate) help_accumulation_proof: r1cs_nark_as::Proof>, + + #[doc(hidden)] + pub(crate) _config_phantom: PhantomData, +} + +impl MainCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + /// Returns the public input size of the main circuit. + pub(crate) fn public_input_size() -> usize { + let cs = ConstraintSystem::>::new_ref(); + let _hash = FpVar::new_input(cs.clone(), || Ok(MainField::::zero())).unwrap(); + return cs.num_instance_variables(); + } + + /// Computes a hash of the following elements. + pub(crate) fn compute_hash( + help_avk: &r1cs_nark_as::VerifierKey, + help_accumulator_instance: &AccumulatorInstance>, + msg: &P::Message, + ) -> MainField { + let mut sponge = PC::MainSponge::new(); + absorb!(&mut sponge, help_avk, help_accumulator_instance, msg); + sponge.squeeze_field_elements(1).pop().unwrap() + } + + /// Computes a hash of the following elements in the constraint system. + pub(crate) fn compute_hash_var( + cs: ConstraintSystemRef>, + help_avk_var: &r1cs_nark_as::constraints::VerifierKeyVar>, + help_accumulator_instance_var: &AccumulatorInstanceVar, PC::HelpCurveVar>, + msg_var: &P::MessageVar, + ) -> Result>, SynthesisError> { + let mut sponge = PC::MainSpongeVar::new(cs); + absorb_gadget!( + &mut sponge, + help_avk_var, + help_accumulator_instance_var, + msg_var + ); + Ok(sponge.squeeze_field_elements(1)?.pop().unwrap()) + } + + /// Computes the public input of the main circuit. + pub(crate) fn compute_public_input( + help_avk: &r1cs_nark_as::VerifierKey, + help_accumulator_instance: &AccumulatorInstance>, + msg: &P::Message, + ) -> Result>, SynthesisError> { + let cs = ConstraintSystem::>::new_ref(); + + let _hash = FpVar::new_input(cs.clone(), || { + Ok(Self::compute_hash(help_avk, help_accumulator_instance, msg)) + })?; + + let r1cs_input = cs.borrow().unwrap().instance_assignment.clone(); + Ok(r1cs_input) + } +} + +impl ConstraintSynthesizer> for MainCircuit +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, + P: PCDPredicate>, +{ + fn generate_constraints( + self, + cs: ConstraintSystemRef>, + ) -> Result<(), SynthesisError> { + let MainCircuit { + predicate, + msg, + witness, + prior_msgs, + help_avk, + help_accumulation_input_instances: help_input_instances, + help_old_accumulator_instances, + help_new_accumulator_instance, + mut help_accumulation_proof, + _config_phantom, + } = self; + + // Ensure that prior data exist together. + assert_eq!(help_input_instances.is_some(), prior_msgs.is_some()); + + assert_eq!( + help_input_instances.is_some(), + help_old_accumulator_instances.is_some() + ); + + // Ensure that prior data has the correct length. + assert!(prior_msgs.is_none() || prior_msgs.as_ref().unwrap().len() == P::PRIOR_MSG_LEN); + + assert!( + help_input_instances.is_none() + || help_input_instances.as_ref().unwrap().len() == P::PRIOR_MSG_LEN + ); + + assert!( + help_old_accumulator_instances.is_none() + || help_old_accumulator_instances.as_ref().unwrap().len() == P::PRIOR_MSG_LEN + ); + + // Process the inputs + + let base_case = help_input_instances.is_none(); + let help_circuit_input_len = HelpCircuit::::public_input_size(); + let (help_input_instances, help_old_accumulator_instances, prior_msgs) = if base_case { + // Populate the prior data with default data. + ( + vec![InputInstance::zero(help_circuit_input_len, MAKE_ZK); P::PRIOR_MSG_LEN], + vec![AccumulatorInstance::placeholder(help_circuit_input_len); P::PRIOR_MSG_LEN], + vec![P::Message::default(); P::PRIOR_MSG_LEN], + ) + } else { + ( + help_input_instances.unwrap(), + help_old_accumulator_instances.unwrap(), + prior_msgs.unwrap(), + ) + }; + + // In the base case, the size of the proof will be incorrect due to the low and high + // T commitments in the underlying HP_AS proof. We substitute the base case proof with a + // dummy proof to ensure the size of the circuit remains constant. We are able to do so + // because the result of the r1cs_nark_as verify does not matter in the base case. + if base_case { + help_accumulation_proof = r1cs_nark_as::Proof::placeholder( + help_circuit_input_len, + P::PRIOR_MSG_LEN * 2, + MAKE_ZK, + ); + }; + + let claimed_input_hash: MainField = + Self::compute_hash(&help_avk, &help_new_accumulator_instance, &msg); + + // Allocation + + let claimed_input_hash_var = FpVar::new_input(ns!(cs, "alloc_claimed_input_hash"), || { + Ok(claimed_input_hash) + })?; + + let base_case_var = Boolean::new_witness(ns!(cs, "alloc_base_case_bit"), || Ok(base_case))?; + + let help_avk_var = r1cs_nark_as::constraints::VerifierKeyVar::new_witness( + ns!(cs, "alloc_help_avk"), + || Ok(help_avk), + )?; + + let msg_var = P::MessageVar::new_witness(ns!(cs, "alloc_msg"), || Ok(msg))?; + + let witness_var = + P::LocalWitnessVar::new_witness(ns!(cs, "alloc_witness"), || Ok(witness))?; + + let prior_msg_vars = prior_msgs + .into_iter() + .map(|prior_msg| { + P::MessageVar::new_witness(ns!(cs, "alloc_prior_msg"), || Ok(prior_msg)) + }) + .collect::, SynthesisError>>()?; + + let help_input_instance_vars = help_input_instances + .into_iter() + .map(|input_instance| { + InputInstanceVar::, PC::HelpCurveVar>::new_witness( + ns!(cs, "alloc_help_input_instances"), + || Ok(input_instance), + ) + }) + .collect::, SynthesisError>>()?; + + let help_old_accumulator_instance_vars = help_old_accumulator_instances + .into_iter() + .map(|accumulator_instance| { + AccumulatorInstanceVar::, PC::HelpCurveVar>::new_witness( + ns!(cs, "alloc_help_old_accumulator_instances"), + || Ok(accumulator_instance), + ) + }) + .collect::, SynthesisError>>()?; + + let help_new_accumulator_instance_var = + AccumulatorInstanceVar::, PC::HelpCurveVar>::new_witness( + ns!(cs, "alloc_help_new_accumulator_instance"), + || Ok(help_new_accumulator_instance), + )?; + + let help_accumulation_proof_var = + r1cs_nark_as::constraints::ProofVar::, PC::HelpCurveVar>::new_witness( + ns!(cs, "alloc_help_accumulation_proof"), + || Ok(help_accumulation_proof), + )?; + + // Verification + + predicate.generate_constraints( + ark_relations::ns!(cs, "check_predicate").cs(), + &msg_var, + &witness_var, + &prior_msg_vars, + &base_case_var, + )?; + + let input_hash_var: FpVar> = Self::compute_hash_var( + ns!(cs, "input_hash_sponge").cs(), + &help_avk_var, + &help_new_accumulator_instance_var, + &msg_var, + )?; + + input_hash_var.enforce_equal(&claimed_input_hash_var)?; + + let as_verify = ASForR1CSNarkVerifierGadget::< + HelpAffine, + PC::HelpCurveVar, + PC::MainSponge, + PC::MainSpongeVar, + >::verify( + ns!(cs, "help_accumulation_verify").cs(), + &help_avk_var, + &help_input_instance_vars, + &help_old_accumulator_instance_vars, + &help_new_accumulator_instance_var, + &help_accumulation_proof_var, + None, + )?; + + base_case_var + .or(&as_verify)? + .enforce_equal(&Boolean::TRUE)?; + + Ok(()) + } +} diff --git a/src/r1cs_nark_pcd/mod.rs b/src/r1cs_nark_pcd/mod.rs new file mode 100644 index 0000000..89524be --- /dev/null +++ b/src/r1cs_nark_pcd/mod.rs @@ -0,0 +1,612 @@ +use crate::error::PCDError; +use crate::{CircuitSpecificSetupPCD, Error, PCDPredicate, PCD}; +use ark_accumulation::r1cs_nark_as::r1cs_nark::R1CSNark; +use ark_accumulation::r1cs_nark_as::{ASForR1CSNark, AccumulatorInstance, InputInstance}; +use ark_accumulation::{ + r1cs_nark_as, AccumulationScheme, Accumulator, AccumulatorRef, InputRef, MakeZK, +}; +use ark_ec::CurveCycle; +use ark_ff::PrimeField; +use ark_r1cs_std::groups::CurveVar; +use ark_sponge::constraints::{AbsorbableGadget, CryptographicSpongeVar}; +use ark_sponge::{Absorbable, CryptographicSponge}; +use ark_std::marker::PhantomData; +use ark_std::rand::{CryptoRng, Rng}; +use help_circuit::HelpCircuit; +use main_circuit::MainCircuit; + +/// Defines the public data structures that the [R1CSNarkPCD] uses. +pub mod data_structures; +use data_structures::*; + +/// The help circuit of the recursion. +mod help_circuit; + +/// The main circuit of the recursion. +mod main_circuit; + +pub(crate) const MAKE_ZK: bool = true; + +/// The different types needed by the [`R1CSNarkPCD`][nark_pcd] construction. +/// +/// [nark_pcd]: crate::r1cs_nark_pcd::R1CSNarkPCD +pub trait R1CSNarkPCDConfig +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, +{ + /// The curve var for the main affine. + type MainCurveVar: CurveVar, HelpField> + AbsorbableGadget>; + + /// The curve var for the help affine. + type HelpCurveVar: CurveVar, MainField> + AbsorbableGadget>; + + /// The sponge that the main circuit uses. + type MainSponge: CryptographicSponge>; + + /// The sponge var that the main circuit uses. + type MainSpongeVar: CryptographicSpongeVar, Self::MainSponge>; + + /// The sponge that the help circuit uses. + type HelpSponge: CryptographicSponge>; + + /// The sponge var that the help circuit uses. + type HelpSpongeVar: CryptographicSpongeVar, Self::HelpSponge>; +} + +/// A PCD that does not rely on SNARKs but instead builds on an R1CS NARK construction and its +/// accumulation scheme. +/// +/// The implementation is based on the construction detailed in Section 5 of [\[BCLMS20\]][bclms20] +/// but slightly differs: +/// +/// 1. To generalize for different R1CS NARK constructions and their respective accumulation +/// schemes, the implementation hashes the verifier key, messages, and accumulator instances and +/// allocates them as witnesses rather than inputs. +/// +/// 2. There are now two circuits used in the recursion: the main circuit and help circuit. The main +/// circuit ensures that the accumulation of arguments about the help circuit is computed correctly +/// and that the PCD predicate holds. The help circuit ensures that the accumulation of arguments +/// about the main circuit is computed correctly. +/// +/// [bclms20]: https://eprint.iacr.org/2020/1618 +/// +/// The scheme is as follows on a high level. +/// Assume the PCD messages and witness are already passed into the main circuit and the operations +/// related to arguments about the main circuit whenever possible. +/// +/// ```rust,ignore +/// prove (old_help_nark_pf, old_main_nark_pf, old_help_acc, old_main_acc): +/// accumulate ((old_main_acc, old_help_nark_pf), old_help_acc) +/// -> new_help_acc, new_help_acc_pf +/// MainCircuit ((old_main_acc, old_help_nark_pf), old_help_acc, new_help_acc, +/// new_help_acc_pf) +/// -> main_circuit +/// nark_prove (main_circuit) +/// -> new_main_nark_pf +/// +/// accumulate ((old_help_acc, old_main_nark_pf), old_main_acc) +/// -> new_main_acc, new_main_acc_pf +/// HelpCircuit ((old_help_acc, old_main_nark_pf), old_main_acc, new_main_acc, +/// new_main_acc_pf) +/// -> help_circuit +/// nark_prove (help_circuit) +/// -> new_help_nark_pf +/// +/// return new_main_nark_pf, new_help_nark_pf, new_main_acc, new_help_acc +/// +/// verify (main_nark_pf, help_nark_pf, main_acc, help_acc): +/// return nark_verify (main_nark_pf) +/// && nark_verify (help_nark_pf) +/// && acc_decide (main_acc) +/// && acc_decide (help_acc) +/// ``` +pub struct R1CSNarkPCD +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, +{ + _curve_cycle_phantom: PhantomData, + _config_phantom: PhantomData, +} + +impl PCD> for R1CSNarkPCD +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, +{ + type ProvingKey = ProvingKey; + type VerifyingKey = VerifyingKey; + type Proof = Proof; + + fn circuit_specific_setup>, R: Rng + CryptoRng>( + predicate: &P, + rng: &mut R, + ) -> Result<(Self::ProvingKey, Self::VerifyingKey), Error> { + let (main_apk, main_avk, main_adk) = { + let help_public_inputs = HelpCircuit::::public_input_size(); + let placeholder_main_circuit = MainCircuit:: { + predicate: predicate.clone(), + msg: P::Message::default(), + witness: P::LocalWitness::default(), + prior_msgs: None, + help_avk: r1cs_nark_as::VerifierKey::placeholder(help_public_inputs), + help_accumulation_input_instances: None, + help_old_accumulator_instances: None, + help_new_accumulator_instance: AccumulatorInstance::placeholder(help_public_inputs), + help_accumulation_proof: r1cs_nark_as::Proof::placeholder( + help_public_inputs, + P::PRIOR_MSG_LEN * 2, + MAKE_ZK, + ), + _config_phantom: PhantomData, + }; + + let main_nark_pp = R1CSNark::, PC::HelpSponge>::setup(); + let main_nark_index = R1CSNark::, PC::HelpSponge>::index( + &main_nark_pp, + placeholder_main_circuit, + )?; + + let main_as_pp = ASForR1CSNark::, PC::HelpSponge>::setup(rng)?; + + let (main_apk, main_avk, main_adk) = + ASForR1CSNark::, PC::HelpSponge>::index( + &main_as_pp, + &(), + &main_nark_index, + )?; + + (main_apk, main_avk, main_adk) + }; + + let (help_apk, help_avk, help_adk) = { + let main_public_inputs = MainCircuit::::public_input_size(); + + let placeholder_help_circuit = HelpCircuit:: { + main_avk: main_avk.clone(), + main_accumulation_input_instances: None, + main_old_accumulator_instances: None, + main_new_accumulator_instance: AccumulatorInstance::placeholder(main_public_inputs), + main_accumulation_proof: r1cs_nark_as::Proof::placeholder( + main_public_inputs, + P::PRIOR_MSG_LEN * 2, + MAKE_ZK, + ), + _config_phantom: PhantomData, + _predicate_phantom: PhantomData, + }; + + let help_nark_pp = R1CSNark::, PC::MainSponge>::setup(); + let help_nark_index = R1CSNark::, PC::MainSponge>::index( + &help_nark_pp, + placeholder_help_circuit, + )?; + + let help_as_pp = ASForR1CSNark::, PC::MainSponge>::setup(rng)?; + + let (help_apk, help_avk, help_adk) = + ASForR1CSNark::, PC::MainSponge>::index( + &help_as_pp, + &(), + &help_nark_index, + )?; + + (help_apk, help_avk, help_adk) + }; + + let pk = ProvingKey { + main_apk, + main_avk: main_avk.clone(), + help_apk, + help_avk: help_avk.clone(), + }; + + let vk = VerifyingKey { + main_avk, + help_avk, + main_ivk: main_adk, + help_ivk: help_adk, + }; + + Ok((pk, vk)) + } + + fn prove>, R: Rng + CryptoRng>( + pk: &Self::ProvingKey, + predicate: &P, + msg: &P::Message, + witness: &P::LocalWitness, + prior_msgs: &[P::Message], + prior_proofs: &[Self::Proof], + rng: &mut R, + ) -> Result { + if prior_msgs.len() != 0 && prior_msgs.len() != P::PRIOR_MSG_LEN { + return Err(Box::new(PCDError::InvalidPriorMessagesLength( + P::PRIOR_MSG_LEN, + prior_msgs.len(), + ))); + } + + if prior_msgs.len() != prior_proofs.len() { + return Err(Box::new(PCDError::InvalidPriorProofsLength( + prior_msgs.len(), + prior_proofs.len(), + ))); + } + + let base_case = prior_msgs.is_empty(); + + // In the base case, these vectors will be empty. + let mut help_accumulation_input_instances = Vec::new(); + let mut help_old_accumulator_instances = Vec::new(); + + let mut main_accumulation_input_instances = Vec::new(); + let mut main_old_accumulator_instances = Vec::new(); + + // Extract the input and accumulator instances to be passed into the main and help circuits. + for (msg, proof) in prior_msgs.into_iter().zip(prior_proofs) { + let Proof { + help_nark_proof, + help_accumulator, + main_nark_proof, + main_accumulator, + } = proof; + + help_accumulation_input_instances.push(InputInstance { + r1cs_input: HelpCircuit::::compute_public_input( + &pk.main_avk, + &main_accumulator.0, + )?, + first_round_message: help_nark_proof.first_msg.clone(), + }); + + help_old_accumulator_instances.push(help_accumulator.0.clone()); + + main_accumulation_input_instances.push(InputInstance { + r1cs_input: MainCircuit::::compute_public_input( + &pk.help_avk, + &help_accumulator.0, + msg, + )?, + first_round_message: main_nark_proof.first_msg.clone(), + }); + + main_old_accumulator_instances.push(main_accumulator.0.clone()); + } + + let (help_new_accumulator, main_nark_proof) = { + let (help_new_accumulator, help_accumulation_proof) = { + let help_accumulation_input_refs = help_accumulation_input_instances + .iter() + .zip(prior_proofs) + .map(|(instance, proof)| InputRef::< + MainField, + PC::MainSponge, + ASForR1CSNark, PC::MainSponge>, + > { + instance, + witness: &proof.help_nark_proof.second_msg, + }); + + let help_old_accumulator_refs = prior_proofs.iter().map(|proof| AccumulatorRef::< + MainField, + PC::MainSponge, + ASForR1CSNark, PC::MainSponge>, + > { + instance: &proof.help_accumulator.0, + witness: &proof.help_accumulator.1, + }); + + ASForR1CSNark::, PC::MainSponge>::prove( + &pk.help_apk, + help_accumulation_input_refs, + help_old_accumulator_refs, + if MAKE_ZK { + MakeZK::Enabled(rng) + } else { + MakeZK::Disabled + }, + None, + )? + }; + + let main_nark_proof = { + let (prior_msgs, help_accumulation_input_instances, help_old_accumulator_instances) = + if !base_case { + ( + Some(prior_msgs.to_vec()), + Some(help_accumulation_input_instances), + Some(help_old_accumulator_instances), + ) + } else { + (None, None, None) + }; + + // Circuit to verify the predicate holds and the help accumulation was properly computed. + let main_circuit = MainCircuit:: { + predicate: predicate.clone(), + msg: msg.clone(), + witness: witness.clone(), + prior_msgs, + help_avk: pk.help_avk.clone(), + help_accumulation_input_instances, + help_old_accumulator_instances, + help_new_accumulator_instance: help_new_accumulator.instance.clone(), + help_accumulation_proof, + _config_phantom: PhantomData, + }; + + let help_sponge = PC::HelpSponge::new(); + let main_nark_sponge = + ASForR1CSNark::, PC::HelpSponge>::nark_sponge(&help_sponge); + + R1CSNark::prove( + &pk.main_apk.nark_pk, + main_circuit, + MAKE_ZK, + Some(main_nark_sponge), + if MAKE_ZK { Some(rng) } else { None }, + )? + }; + + // Convert the accumulator to tuple to store in the proof. + let help_new_accumulator = { + let Accumulator::< + MainField, + PC::MainSponge, + ASForR1CSNark, PC::MainSponge>, + > { + instance, + witness, + } = help_new_accumulator; + + (instance, witness) + }; + + (help_new_accumulator, main_nark_proof) + }; + + let (main_new_accumulator, help_nark_proof) = { + let (main_new_accumulator, main_accumulation_proof) = { + let main_accumulation_input_refs = main_accumulation_input_instances + .iter() + .zip(prior_proofs) + .map(|(instance, proof)| InputRef::< + HelpField, + PC::HelpSponge, + ASForR1CSNark, PC::HelpSponge>, + > { + instance, + witness: &proof.main_nark_proof.second_msg, + }); + + let main_old_accumulator_refs = prior_proofs.iter().map(|proof| AccumulatorRef::< + HelpField, + PC::HelpSponge, + ASForR1CSNark, PC::HelpSponge>, + > { + instance: &proof.main_accumulator.0, + witness: &proof.main_accumulator.1, + }); + + ASForR1CSNark::, PC::HelpSponge>::prove( + &pk.main_apk, + main_accumulation_input_refs, + main_old_accumulator_refs, + if MAKE_ZK { + MakeZK::Enabled(rng) + } else { + MakeZK::Disabled + }, + None, + )? + }; + + let help_nark_proof = { + let (main_accumulation_input_instances, main_old_accumulator_instances) = + if !base_case { + ( + Some(main_accumulation_input_instances), + Some(main_old_accumulator_instances), + ) + } else { + (None, None) + }; + + // Circuit to verify main accumulation was properly computed. + let help_circuit = HelpCircuit:: { + main_avk: pk.main_avk.clone(), + main_accumulation_input_instances, + main_old_accumulator_instances, + main_new_accumulator_instance: main_new_accumulator.instance.clone(), + main_accumulation_proof, + _config_phantom: PhantomData, + _predicate_phantom: PhantomData, + }; + + let main_sponge = PC::MainSponge::new(); + let help_nark_sponge = + ASForR1CSNark::, PC::MainSponge>::nark_sponge(&main_sponge); + + R1CSNark::prove( + &pk.help_apk.nark_pk, + help_circuit, + MAKE_ZK, + Some(help_nark_sponge), + if MAKE_ZK { Some(rng) } else { None }, + )? + }; + + // Convert the accumulator to tuple to store in the proof. + let main_new_accumulator = { + let Accumulator::< + HelpField, + PC::HelpSponge, + ASForR1CSNark, PC::HelpSponge>, + > { + instance, + witness, + } = main_new_accumulator; + + (instance, witness) + }; + + (main_new_accumulator, help_nark_proof) + }; + + Ok(Proof:: { + main_nark_proof, + help_nark_proof, + main_accumulator: main_new_accumulator, + help_accumulator: help_new_accumulator, + }) + } + + fn verify>>( + vk: &Self::VerifyingKey, + msg: &P::Message, + proof: &Self::Proof, + ) -> Result { + let main_nark_verify = { + let help_sponge = PC::HelpSponge::new(); + let main_nark_sponge = + ASForR1CSNark::, PC::HelpSponge>::nark_sponge(&help_sponge); + + R1CSNark::verify( + &vk.main_ivk, + &MainCircuit::::compute_public_input( + &vk.help_avk, + &proof.help_accumulator.0, + msg, + )?, + &proof.main_nark_proof, + Some(main_nark_sponge), + ) + }; + + let help_nark_verify = { + let main_sponge = PC::MainSponge::new(); + let help_nark_sponge = + ASForR1CSNark::, PC::MainSponge>::nark_sponge(&main_sponge); + + R1CSNark::verify( + &vk.help_ivk, + &HelpCircuit::::compute_public_input( + &vk.main_avk, + &proof.main_accumulator.0, + )?, + &proof.help_nark_proof, + Some(help_nark_sponge), + ) + }; + + let main_accumulation_decide = { + let main_accumulator_ref = AccumulatorRef::< + HelpField, + PC::HelpSponge, + ASForR1CSNark, PC::HelpSponge>, + > { + instance: &proof.main_accumulator.0, + witness: &proof.main_accumulator.1, + }; + + ASForR1CSNark::, PC::HelpSponge>::decide( + &vk.main_ivk, + main_accumulator_ref, + None, + )? + }; + + let help_accumulation_decide = { + let help_accumulator_ref = AccumulatorRef::< + MainField, + PC::MainSponge, + ASForR1CSNark, PC::MainSponge>, + > { + instance: &proof.help_accumulator.0, + witness: &proof.help_accumulator.1, + }; + + ASForR1CSNark::, PC::MainSponge>::decide( + &vk.help_ivk, + help_accumulator_ref, + None, + )? + }; + + Ok(main_nark_verify + && help_nark_verify + && main_accumulation_decide + && help_accumulation_decide) + } +} + +impl CircuitSpecificSetupPCD> for R1CSNarkPCD +where + E: CurveCycle, + MainField: PrimeField + Absorbable>, + HelpField: PrimeField + Absorbable>, + MainAffine: Absorbable>, + HelpAffine: Absorbable>, + PC: R1CSNarkPCDConfig, +{ +} + +#[cfg(test)] +pub mod tests { + use crate::r1cs_nark_pcd::{R1CSNarkPCD, R1CSNarkPCDConfig}; + use ark_ec::{CurveCycle, PairingEngine}; + use ark_sponge::poseidon::constraints::PoseidonSpongeVar; + use ark_sponge::poseidon::PoseidonSponge; + + type MainAffine = ::G1Affine; + type MainField = ::Fr; + type MainCurveVar = ark_mnt4_298::constraints::G1Var; + type MainSponge = PoseidonSponge; + type MainSpongeVar = PoseidonSpongeVar; + + type HelpAffine = ::G1Affine; + type HelpField = ::Fr; + type HelpCurveVar = ark_mnt6_298::constraints::G1Var; + type HelpSponge = PoseidonSponge; + type HelpSpongeVar = PoseidonSpongeVar; + + pub struct TestCycle; + impl CurveCycle for TestCycle { + type E1 = MainAffine; + type E2 = HelpAffine; + } + + pub struct TestConfig {} + impl R1CSNarkPCDConfig for TestConfig { + type MainCurveVar = MainCurveVar; + type HelpCurveVar = HelpCurveVar; + type MainSponge = MainSponge; + type MainSpongeVar = MainSpongeVar; + type HelpSponge = HelpSponge; + type HelpSpongeVar = HelpSpongeVar; + } + + type TestPCD = R1CSNarkPCD; + + #[test] + pub fn test_ivc() { + #[cfg(ci)] + crate::tests::test_ivc_base_case::(); + + #[cfg(not(ci))] + crate::tests::test_ivc::(); + } +} diff --git a/tests/mnt4_gm17.rs b/tests/mnt4_gm17.rs index a45cc60..4a89f29 100644 --- a/tests/mnt4_gm17.rs +++ b/tests/mnt4_gm17.rs @@ -17,6 +17,7 @@ use ark_r1cs_std::eq::EqGadget; use ark_r1cs_std::fields::fp::FpVar; use ark_relations::r1cs::ConstraintSystemRef; use ark_relations::r1cs::SynthesisError; +use ark_sponge::Absorbable; use core::marker::PhantomData; use rand_chacha::ChaChaRng; @@ -50,7 +51,7 @@ impl Clone for TestPredicate { } } -impl PCDPredicate for TestPredicate { +impl> PCDPredicate for TestPredicate { type Message = F; type MessageVar = FpVar; type LocalWitness = F; diff --git a/tests/mnt4_groth16.rs b/tests/mnt4_groth16.rs index 04aed45..e82d3b4 100644 --- a/tests/mnt4_groth16.rs +++ b/tests/mnt4_groth16.rs @@ -16,6 +16,7 @@ use ark_r1cs_std::eq::EqGadget; use ark_r1cs_std::fields::fp::FpVar; use ark_relations::r1cs::ConstraintSystemRef; use ark_relations::r1cs::SynthesisError; +use ark_sponge::Absorbable; use core::marker::PhantomData; use rand_chacha::ChaChaRng; @@ -49,7 +50,7 @@ impl Clone for TestPredicate { } } -impl PCDPredicate for TestPredicate { +impl> PCDPredicate for TestPredicate { type Message = F; type MessageVar = FpVar; type LocalWitness = F; diff --git a/tests/mnt4_marlin.rs b/tests/mnt4_marlin.rs index b53635c..9f1e130 100644 --- a/tests/mnt4_marlin.rs +++ b/tests/mnt4_marlin.rs @@ -25,6 +25,7 @@ use ark_r1cs_std::eq::EqGadget; use ark_r1cs_std::fields::fp::FpVar; use ark_relations::r1cs::ConstraintSystemRef; use ark_relations::r1cs::SynthesisError; +use ark_sponge::Absorbable; use core::marker::PhantomData; use rand_chacha::ChaChaRng; @@ -113,7 +114,7 @@ impl Clone for TestPredicate { } } -impl PCDPredicate for TestPredicate { +impl> PCDPredicate for TestPredicate { type Message = F; type MessageVar = FpVar; type LocalWitness = F; diff --git a/tests/mnt4_mix_gm17groth16.rs b/tests/mnt4_mix_gm17groth16.rs index e4ad99d..c3b8c8b 100644 --- a/tests/mnt4_mix_gm17groth16.rs +++ b/tests/mnt4_mix_gm17groth16.rs @@ -18,6 +18,7 @@ use ark_r1cs_std::eq::EqGadget; use ark_r1cs_std::fields::fp::FpVar; use ark_relations::r1cs::ConstraintSystemRef; use ark_relations::r1cs::SynthesisError; +use ark_sponge::Absorbable; use core::marker::PhantomData; use rand_chacha::ChaChaRng; @@ -51,7 +52,7 @@ impl Clone for TestPredicate { } } -impl PCDPredicate for TestPredicate { +impl> PCDPredicate for TestPredicate { type Message = F; type MessageVar = FpVar; type LocalWitness = F; diff --git a/tests/mnt4_mix_groth16gm17.rs b/tests/mnt4_mix_groth16gm17.rs index f4ef024..ec6323d 100644 --- a/tests/mnt4_mix_groth16gm17.rs +++ b/tests/mnt4_mix_groth16gm17.rs @@ -18,6 +18,7 @@ use ark_r1cs_std::eq::EqGadget; use ark_r1cs_std::fields::fp::FpVar; use ark_relations::r1cs::ConstraintSystemRef; use ark_relations::r1cs::SynthesisError; +use ark_sponge::Absorbable; use core::marker::PhantomData; use rand_chacha::ChaChaRng; @@ -51,7 +52,7 @@ impl Clone for TestPredicate { } } -impl PCDPredicate for TestPredicate { +impl> PCDPredicate for TestPredicate { type Message = F; type MessageVar = FpVar; type LocalWitness = F;