Skip to content

Commit

Permalink
refactor FCircuit to make it more suitable inside the AugmentedFCircuit
Browse files Browse the repository at this point in the history
  • Loading branch information
@arnaucube
arnaucube committed Oct 27, 2023
1 parent 7fc1aa8 commit a32002d
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 27 deletions.
4 changes: 2 additions & 2 deletions Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ ark-poly = "^0.4.0"
ark-std = "^0.4.0"
ark-crypto-primitives = { version = "^0.4.0", default-features = false, features = ["r1cs", "sponge", "crh"] }
ark-relations = { version = "^0.4.0", default-features = false }
ark-r1cs-std = { default-features = false } # use latest version of the patch
ark-r1cs-std = { default-features = false } # use latest version from the patch
ark-circom = { git = "https://github.com/gakonst/ark-circom.git" }
thiserror = "1.0"
rayon = "1.7.0"
Expand Down Expand Up @@ -42,7 +42,7 @@ parallel = [

# The following patch is to use a version of ark-r1cs-std compatible with
# v0.4.0 but that includes a cherry-picked commit from after v0.4.0 which fixes
# the in-circuit scalar multiplication of the zero point from
# the in-circuit scalar multiplication of the zero point. The commit is from
# https://github.com/arkworks-rs/r1cs-std/pull/124, without including other
# changes done between v0.4.0 and this fix which would break compatibility.
[patch.crates-io]
Expand Down
56 changes: 31 additions & 25 deletions src/folding/nova/circuits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,13 +213,18 @@ where

/// FCircuit defines the trait of the circuit of the F function, which is the one being executed
/// inside the agmented F' function.
pub trait FCircuit<F: PrimeField>: ConstraintSynthesizer<F> + Copy {
pub trait FCircuit<F: PrimeField>: Copy {
/// method that returns z_i (input), z_{i+1} (output)
fn public(self) -> (F, F);

/// method that computes the next state values in place, assigning z_{i+1} into z_i, and
/// computing the new z_i
fn step(&mut self);
fn step_native(&mut self);
fn step_circuit(
self,
cs: ConstraintSystemRef<F>,
z_i: FpVar<F>,
) -> Result<FpVar<F>, SynthesisError>;
}

/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
Expand All @@ -230,6 +235,7 @@ pub struct AugmentedFCircuit<C: CurveGroup, FC: FCircuit<CF1<C>>> {
pub poseidon_config: PoseidonConfig<CF1<C>>,
pub i: Option<CF1<C>>,
pub z_0: Option<C::ScalarField>,
pub z_i: Option<C::ScalarField>,
pub u_i: Option<CommittedInstance<C>>,
pub U_i: Option<CommittedInstance<C>>,
pub U_i1: Option<CommittedInstance<C>>,
Expand All @@ -251,11 +257,12 @@ where
let z_0 = FpVar::<CF1<C>>::new_witness(cs.clone(), || {
Ok(self.z_0.unwrap_or_else(CF1::<C>::zero))
})?;
let z_i = FpVar::<CF1<C>>::new_witness(cs.clone(), || {
Ok(self.z_i.unwrap_or_else(CF1::<C>::zero))
})?;

// get z_i & z_{i+1} from the folded circuit
let (z_i_native, z_i1_native) = self.F.public();
let z_i = FpVar::<CF1<C>>::new_witness(cs.clone(), || Ok(z_i_native))?;
let z_i1 = FpVar::<CF1<C>>::new_witness(cs.clone(), || Ok(z_i1_native))?;
// get z_{i+1} from the F circuit
let z_i1 = self.F.step_circuit(cs.clone(), z_i.clone())?;

let u_dummy_native = CommittedInstance {
cmE: C::zero(),
Expand Down Expand Up @@ -331,9 +338,6 @@ where
// else: check x==u_{i+1}.x
u_i1_x.conditional_enforce_equal(&x, &is_not_basecase)?;

// WIP assert that z_i1 == F(z_i)
self.F.generate_constraints(cs.clone())?;

Ok(())
}
}
Expand All @@ -350,6 +354,7 @@ mod tests {
use tracing_subscriber::layer::SubscriberExt;

use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
use crate::constants::N_BITS_CHALLENGE;
use crate::folding::nova::{check_instance_relation, nifs::NIFS, Witness};
use crate::frontend::arkworks::{extract_r1cs, extract_z};
use crate::pedersen::Pedersen;
Expand All @@ -369,20 +374,18 @@ mod tests {
fn public(self) -> (F, F) {
(self.z_i, self.z_i1)
}
fn step(&mut self) {
fn step_native(&mut self) {
self.z_i = self.z_i1;
self.z_i1 = self.z_i * self.z_i * self.z_i + self.z_i + F::from(5_u32);
}
}
impl<F: PrimeField> ConstraintSynthesizer<F> for TestFCircuit<F> {
fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
let z_i = FpVar::<F>::new_witness(cs.clone(), || Ok(self.z_i))?;
let z_i1 = FpVar::<F>::new_witness(cs.clone(), || Ok(self.z_i1))?;
fn step_circuit(
self,
cs: ConstraintSystemRef<F>,
z_i: FpVar<F>,
) -> Result<FpVar<F>, SynthesisError> {
let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;

let y = &z_i * &z_i * &z_i + &z_i + &five;
y.enforce_equal(&z_i1)?;
Ok(())
Ok(&z_i * &z_i * &z_i + &z_i + &five)
}
}

Expand Down Expand Up @@ -435,7 +438,7 @@ mod tests {
// get challenge from transcript
let poseidon_config = poseidon_test_config::<Fr>();
let mut tr = PoseidonTranscript::<Projective>::new(&poseidon_config);
let r_bits = tr.get_challenge_nbits(128);
let r_bits = tr.get_challenge_nbits(N_BITS_CHALLENGE);
let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();

let (_w3, ci3, _T, cmT) =
Expand Down Expand Up @@ -559,6 +562,7 @@ mod tests {
poseidon_config: poseidon_config.clone(),
i: None,
z_0: None,
z_i: None,
u_i: None,
U_i: None,
U_i1: None,
Expand All @@ -583,7 +587,7 @@ mod tests {

// first step
let z_0 = Fr::from(3_u32);
let z_i = z_0;
let mut z_i = z_0;
let mut z_i1 = Fr::from(35_u32);

// set the circuit to be folded with z_i=z_0=3 and z_{i+1}=35 (initial values)
Expand Down Expand Up @@ -623,8 +627,9 @@ mod tests {
augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
_c: PhantomData,
poseidon_config: poseidon_config.clone(),
i: Some(i), // = 0
z_0: Some(z_0), // = z_i=3
i: Some(i), // = 0
z_0: Some(z_0), // = z_i=3
z_i: Some(z_i),
u_i: Some(u_i.clone()), // = dummy
U_i: Some(U_i.clone()), // = dummy
U_i1: Some(U_i1.clone()), // = dummy
Expand All @@ -636,7 +641,7 @@ mod tests {
} else {
// get challenge from transcript (since this is a test, we skip absorbing values to
// the transcript for simplicity)
let r_bits = tr.get_challenge_nbits(128); // TODO N_BITS_CHALLENGE
let r_bits = tr.get_challenge_nbits(N_BITS_CHALLENGE);
let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();

check_instance_relation(&r1cs, &w_i, &u_i).unwrap();
Expand Down Expand Up @@ -667,6 +672,7 @@ mod tests {
poseidon_config: poseidon_config.clone(),
i: Some(i),
z_0: Some(z_0),
z_i: Some(z_i),
u_i: Some(u_i),
U_i: Some(U_i.clone()),
U_i1: Some(U_i1.clone()),
Expand Down Expand Up @@ -707,8 +713,8 @@ mod tests {

// set values for next iteration
i += Fr::one();
test_F_circuit.step(); // advance the F circuit state
(_, z_i1) = test_F_circuit.public();
test_F_circuit.step_native(); // advance the F circuit state
(z_i, z_i1) = test_F_circuit.public();
U_i = U_i1.clone();
W_i = W_i1.clone();
}
Expand Down

0 comments on commit a32002d

Please sign in to comment.