Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

R1CS folding generalization #153

Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 additions & 0 deletions src/gadgets/r1cs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,101 @@ impl<G: Group> AllocatedRelaxedR1CSInstance<G> {
})
}

/// Folds self with a relaxed r1cs instance and returns the result
#[allow(clippy::too_many_arguments)]
#[allow(unused)]
pub fn fold_with_relaxed_r1cs<CS: ConstraintSystem<<G as Group>::Base>>(
&self,
mut cs: CS,
params: AllocatedNum<G::Base>, // hash of R1CSShape of F'
u: AllocatedRelaxedR1CSInstance<G>,
T: AllocatedPoint<G>,
ro_consts: ROConstantsCircuit<G>,
limb_width: usize,
n_limbs: usize,
) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
// Compute r:
let mut ro = G::ROCircuit::new(ro_consts, NUM_FE_FOR_RO);
ro.absorb(params);
self.absorb_in_ro(cs.namespace(|| "absorb running instance"), &mut ro)?;
u.absorb_in_ro(cs.namespace(|| "absorb running instance u"), &mut ro)?;
ro.absorb(T.x.clone());
ro.absorb(T.y.clone());
ro.absorb(T.is_infinity.clone());
let r_bits = ro.squeeze(cs.namespace(|| "r bits"), NUM_CHALLENGE_BITS)?;
let r = le_bits_to_num(cs.namespace(|| "r"), r_bits.clone())?;

// W_fold = self.W + r * u.W
let rW = u.W.scalar_mul(cs.namespace(|| "r * u.W"), r_bits.clone())?;
let W_fold = self.W.add(cs.namespace(|| "self.W + r * u.W"), &rW)?;

// E_fold = self.E + r * T + r * r * U.E
let rT = T.scalar_mul(cs.namespace(|| "r * T"), r_bits.clone())?;
let r_e_2 = u.E.scalar_mul(cs.namespace(|| "r * E_2"), r_bits.clone())?;
// Todo - there has to be a better way than 2 scalar mul
let r_squared_e_2 = r_e_2.scalar_mul(cs.namespace(|| "r * r * E_2"), r_bits)?;
let rT_plus_r_squared_E_2 = rT.add(cs.namespace(|| "r * r * E_2"), &r_squared_e_2)?;
let E_fold = self.E.add(cs.namespace(|| "self.E + r * T"), &rT_plus_r_squared_E_2)?;

// u_fold = u_r + r
let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || {
Ok(*self.u.get_value().get()? + r.get_value().get()?)
})?;
cs.enforce(
|| "Check u_fold",
|lc| lc,
|lc| lc,
|lc| lc + u_fold.get_variable() - self.u.get_variable() - r.get_variable(),
);

// Fold the IO:
// Analyze r into limbs
let r_bn = BigNat::from_num(
cs.namespace(|| "allocate r_bn"),
Num::from(r.clone()),
limb_width,
n_limbs,
)?;

// Allocate the order of the non-native field as a constant
let m_bn = alloc_bignat_constant(
cs.namespace(|| "alloc m"),
&G::get_curve_params().2,
limb_width,
n_limbs,
)?;

// Analyze X0 to bignat, NOTE - we copied this code from above but here changed it because the u.X0 is already BigNat
// for u of the type relaxed R1CS
let X0_bn = u.X0.clone();

// Fold self.X[0] + r * X[0]
let (_, r_0) = X0_bn.mult_mod(cs.namespace(|| "r*X[0]"), &r_bn, &m_bn)?;
// add X_r[0]
let r_new_0 = self.X0.add::<CS>(&r_0)?;
// Now reduce
let X0_fold = r_new_0.red_mod(cs.namespace(|| "reduce folded X[0]"), &m_bn)?;

// Analyze X1 to bignat, NOTE - we copied this code from above but here changed it because the u.X0 is already BigNat
// for u of the type relaxed R1CS
let X1_bn = u.X1.clone();

// Fold self.X[1] + r * X[1]
let (_, r_1) = X1_bn.mult_mod(cs.namespace(|| "r*X[1]"), &r_bn, &m_bn)?;
// add X_r[1]
let r_new_1 = self.X1.add::<CS>(&r_1)?;
// Now reduce
let X1_fold = r_new_1.red_mod(cs.namespace(|| "reduce folded X[1]"), &m_bn)?;

Ok(Self {
W: W_fold,
E: E_fold,
u: u_fold,
X0: X0_fold,
X1: X1_fold,
})
}

/// If the condition is true then returns this otherwise it returns the other
pub fn conditionally_select<CS: ConstraintSystem<<G as Group>::Base>>(
&self,
Expand Down
1 change: 1 addition & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ mod circuit;
mod constants;
mod nifs;
mod r1cs;
mod parallel_circuit;

// public modules
pub mod errors;
Expand Down
Loading