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

Finalize #334

Merged
merged 10 commits into from
Jan 4, 2021
107 changes: 86 additions & 21 deletions relations/src/r1cs/constraint_system.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,10 @@ pub struct ConstraintSystem<F: Field> {
/// The number of linear combinations
pub num_linear_combinations: usize,

/// The parameter we aim to minimize in this constraint system (either the
/// number of constraints or their total weight).
pub optimization_goal: OptimizationGoal,

/// Assignments to the public input variables. This is empty if `self.mode
/// == SynthesisMode::Setup`.
pub instance_assignment: Vec<F>,
Expand Down Expand Up @@ -91,6 +95,16 @@ pub enum SynthesisMode {
},
}

/// Defines the parameter to optimize for a `ConstraintSystem`.
#[derive(Copy, Clone, Debug, Eq, PartialEq, Ord, PartialOrd)]
pub enum OptimizationGoal {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we have a None here, which will do no optimization passes?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That makes sense. Do you think None, or Constraints, should be the default?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think constraints should be the default

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What are the semantics of calling finalize with None? In the end we have to get rid of all SymbolicLC before converting to matrices

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think None would still need to inline Symbolic LC (self.inline_all_lcs(), without which to_matrices would fail.

Dev, what do you think? Basically, at this moment, None would be the same as Constraints, and it is uncertain if in the future we will treat them differently.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think given that no specific use cases pop up for None, and we currently do not have a good idea of faster inlining (without optimization to reduce constraints), maybe we can omit None and add it later. Dev, what do you think?

Copy link
Member

@ValarDragon ValarDragon Jan 3, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good to me!

Copy link
Member

@ValarDragon ValarDragon Jan 3, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, I do think None is still useful, in that it could just make far fewer symbolic LC's for memory reduction. E.g. when multiplying by a constant, we don't need to make a new symbolic LC if we don't care about optimizations

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And we could have drop semantics to symbolic LC's to remove intermediate variables from the map as soon as they're dropped from memory. It is a significant engineering effort though, so maybe not worth having it now. (Its non breaking to add it later)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That makes sense. Then let us keep None and, for now, let None also do inline_all_lcs. More changes may be coming in the future.

/// Minimize the number of constraints.
Constraints,
/// Minimize the total weight of the constraints (the number of nonzero
/// entries across all constraints).
Weight,
}

impl<F: Field> ConstraintSystem<F> {
#[inline]
fn make_row(&self, l: &LinearCombination<F>) -> Vec<(F, usize)> {
Expand All @@ -109,7 +123,7 @@ impl<F: Field> ConstraintSystem<F> {
.collect()
}

/// Construct an ampty `ConstraintSystem`.
/// Construct an empty `ConstraintSystem`.
pub fn new() -> Self {
Self {
num_instance_variables: 1,
Expand All @@ -131,6 +145,8 @@ impl<F: Field> ConstraintSystem<F> {
mode: SynthesisMode::Prove {
construct_matrices: true,
},

optimization_goal: OptimizationGoal::Constraints,
}
}

Expand All @@ -149,6 +165,18 @@ impl<F: Field> ConstraintSystem<F> {
self.mode == SynthesisMode::Setup
}

/// Check whether this constraint system aims to optimize weight or
/// number of constraints.
pub fn get_optimization_goal(&self) -> OptimizationGoal {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
pub fn get_optimization_goal(&self) -> OptimizationGoal {
pub fn optimization_goal(&self) -> OptimizationGoal {

self.optimization_goal
}

/// Specify whether this constraint system should aim to optimize weight
/// or number of constraints.
pub fn set_optimization_goal(&mut self, goal: OptimizationGoal) {
self.optimization_goal = goal;
weikengchen marked this conversation as resolved.
Show resolved Hide resolved
}

/// Check whether or not `self` will construct matrices.
pub fn should_construct_matrices(&self) -> bool {
match self.mode {
Expand Down Expand Up @@ -238,7 +266,8 @@ impl<F: Field> ConstraintSystem<F> {
Ok(())
}

/// Count the number of times each LC is used within other LCs in the constraint system
/// Count the number of times each LC is used within other LCs in the
/// constraint system
fn lc_num_times_used(&self, count_sinks: bool) -> Vec<usize> {
let mut num_times_used = vec![0; self.lc_map.len()];

Expand All @@ -260,16 +289,17 @@ impl<F: Field> ConstraintSystem<F> {
/// Transform the map of linear combinations.
/// Specifically, allow the creation of additional witness assignments.
///
/// This method is used as a subroutine of `inline_all_lcs` and `outline_lcs`.
///
/// The transformer function is given a references of this constraint system (&self),
/// number of times used, and a mutable reference of the linear combination to be transformed.
/// (&ConstraintSystem<F>, usize, &mut LinearCombination<F>)
/// This method is used as a subroutine of `inline_all_lcs` and
/// `outline_lcs`.
///
/// The transformer function returns the number of new witness variables needed
/// and a vector of new witness assignments (if not in the setup mode).
/// (usize, Option<Vec<F>>)
/// The transformer function is given a references of this constraint system
/// (&self), number of times used, and a mutable reference of the linear
/// combination to be transformed. (&ConstraintSystem<F>, usize,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Were these comments re-ordered by a linter? Its kinda weird imo that the tuple is split across a new line

/// &mut LinearCombination<F>)
///
/// The transformer function returns the number of new witness variables
/// needed and a vector of new witness assignments (if not in the setup
/// mode). (usize, Option<Vec<F>>)
pub fn transform_lc_map(
&mut self,
transformer: &mut dyn FnMut(
Expand Down Expand Up @@ -309,14 +339,14 @@ impl<F: Field> ConstraintSystem<F> {
// Delete linear combinations that are no longer used.
//
// Deletion is safe for both outlining and inlining:
// * Inlining: the LC is substituted directly into all use
// sites, and so once it is fully inlined, it is redundant.
// * Inlining: the LC is substituted directly into all use sites, and so once it
// is fully inlined, it is redundant.
//
// * Outlining: the LC is associated with a new variable `w`,
// and a new constraint of the form `lc_data * 1 = w`, where
// `lc_data` is the actual data in the linear combination.
// Furthermore, we replace its entry in `new_lc_map` with `(1, w)`.
// Once `w` is fully inlined, then we can delete the entry from `new_lc_map`
// * Outlining: the LC is associated with a new variable `w`, and a new
// constraint of the form `lc_data * 1 = w`, where `lc_data` is the actual
// data in the linear combination. Furthermore, we replace its entry in
// `new_lc_map` with `(1, w)`. Once `w` is fully inlined, then we can delete
// the entry from `new_lc_map`
//
num_times_used[lc_index.0] -= 1;
if num_times_used[lc_index.0] == 0 {
Expand Down Expand Up @@ -404,8 +434,9 @@ impl<F: Field> ConstraintSystem<F> {
// If true, the LC is replaced with 1 * this witness variable.
// Otherwise, the LC is inlined.
//
// Each iteration first updates the LC according to outlinings in prior iterations,
// and then sees if it should be outlined, and if so adds the outlining to the map.
// Each iteration first updates the LC according to outlinings in prior
// iterations, and then sees if it should be outlined, and if so adds
// the outlining to the map.
//
self.transform_lc_map(&mut |cs, num_times_used, inlined_lc| {
let mut should_dedicate_a_witness_variable = false;
Expand Down Expand Up @@ -481,10 +512,19 @@ impl<F: Field> ConstraintSystem<F> {
/// Useful for SNARKs like [\[Marlin\]](https://eprint.iacr.org/2019/1047) or
/// [\[Fractal\]](https://eprint.iacr.org/2019/1076), where addition gates
/// are not cheap.
pub fn reduce_constraint_weight(&mut self) {
fn reduce_constraint_weight(&mut self) {
self.outline_lcs();
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can remove this now, right?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wasn't the idea to add other weight-reducing optimizations, apart from just outlining? (That's what the comment here says.) In which case we'd still want this as a separate function


/// Finalize the constraint system (either by outlining or inlining,
/// depending on the set optimization mode).
pub fn finalize(&mut self) {
match self.optimization_goal {
OptimizationGoal::Constraints => self.inline_all_lcs(),
OptimizationGoal::Weight => self.outline_lcs(),
};
}

/// This step must be called after constraint generation has completed, and
/// after all symbolic LCs have been inlined into the places that they
/// are used.
Expand Down Expand Up @@ -604,7 +644,7 @@ impl<F: Field> ConstraintSystem<F> {
self.lc_assignment_cache.borrow_mut().insert(idx, value);
Some(value)
}
}
},
}
}
}
Expand Down Expand Up @@ -782,6 +822,23 @@ impl<F: Field> ConstraintSystemRef<F> {
.map_or(0, |cs| cs.borrow().num_witness_variables)
}

/// Check whether this constraint system aims to optimize weight or
/// number of constraints.
#[inline]
pub fn get_optimization_goal(&self) -> OptimizationGoal {
self.inner().map_or(OptimizationGoal::Constraints, |cs| {
cs.borrow().get_optimization_goal()
})
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
pub fn get_optimization_goal(&self) -> OptimizationGoal {
self.inner().map_or(OptimizationGoal::Constraints, |cs| {
cs.borrow().get_optimization_goal()
})
}
pub fn optimization_goal(&self) -> OptimizationGoal {
self.inner().map_or(OptimizationGoal::Constraints, |cs| {
cs.borrow().optimization_goal()
})
}


/// Specify whether this constraint system should aim to optimize weight
/// or number of constraints.
#[inline]
pub fn set_optimization_goal(&self, goal: OptimizationGoal) {
self.inner()
.map_or((), |cs| cs.borrow_mut().set_optimization_goal(goal))
}

/// Check whether or not `self` will construct matrices.
#[inline]
pub fn should_construct_matrices(&self) -> bool {
Expand Down Expand Up @@ -875,6 +932,14 @@ impl<F: Field> ConstraintSystemRef<F> {
}
}

/// Finalize the constraint system (either by outlining or inlining,
/// depending on the set optimization mode).
pub fn finalize(&self) {
if let Some(cs) = self.inner() {
cs.borrow_mut().finalize()
}
}

/// This step must be called after constraint generation has completed, and
/// after all symbolic LCs have been inlined into the places that they
/// are used.
Expand Down
6 changes: 3 additions & 3 deletions relations/src/r1cs/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,17 @@ impl fmt::Display for SynthesisError {
SynthesisError::MissingCS => write!(f, "the constraint system was `None`"),
SynthesisError::AssignmentMissing => {
write!(f, "an assignment for a variable could not be computed")
}
},
SynthesisError::DivisionByZero => write!(f, "division by zero"),
SynthesisError::Unsatisfiable => write!(f, "unsatisfiable constraint system"),
SynthesisError::PolynomialDegreeTooLarge => write!(f, "polynomial degree is too large"),
SynthesisError::UnexpectedIdentity => {
write!(f, "encountered an identity element in the CRS")
}
},
SynthesisError::MalformedVerifyingKey => write!(f, "malformed verifying key"),
SynthesisError::UnconstrainedVariable => {
write!(f, "auxiliary variable was unconstrained")
}
},
}
}
}
6 changes: 3 additions & 3 deletions relations/src/r1cs/impl_lc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,16 +228,16 @@ where
Ordering::Greater => {
new_vec.push((push_fn(other[j].0), other[j].1));
j += 1;
}
},
Ordering::Less => {
new_vec.push(*self_cur);
i += 1;
}
},
Ordering::Equal => {
new_vec.push((combine_fn(self_cur.0, other_cur.0), self_cur.1));
i += 1;
j += 1;
}
},
};
}
new_vec.extend_from_slice(&cur[i..]);
Expand Down
2 changes: 1 addition & 1 deletion relations/src/r1cs/trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ where
id if id == TypeId::of::<Self>() => Some(self as *const _ as *const ()),
id if id == TypeId::of::<WithContext>() => {
Some(&self.get_context as *const _ as *const ())
}
},
_ => None,
}
}
Expand Down
26 changes: 14 additions & 12 deletions snark/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ pub trait SNARK<F: PrimeField> {
/// Errors encountered during setup, proving, or verification.
type Error: 'static + ark_std::error::Error;

/// Takes in a description of a computation (specified in R1CS constraints), and
/// samples proving and verification keys for that circuit.
/// Takes in a description of a computation (specified in R1CS constraints),
/// and samples proving and verification keys for that circuit.
fn circuit_specific_setup<C: ConstraintSynthesizer<F>, R: RngCore + CryptoRng>(
circuit: C,
rng: &mut R,
Expand All @@ -51,8 +51,8 @@ pub trait SNARK<F: PrimeField> {
) -> Result<Self::Proof, Self::Error>;

/// Checks that `proof` is a valid proof of the satisfaction of circuit
/// encoded in `circuit_vk`, with respect to the public input `public_input`.
/// as R1CS constraints).
/// encoded in `circuit_vk`, with respect to the public input
/// `public_input`. as R1CS constraints).
fn verify(
circuit_vk: &Self::VerifyingKey,
public_input: &[F],
Expand All @@ -68,8 +68,8 @@ pub trait SNARK<F: PrimeField> {
) -> Result<Self::ProcessedVerifyingKey, Self::Error>;

/// Checks that `proof` is a valid proof of the satisfaction of circuit
/// encoded in `circuit_pvk`, with respect to the public input `public_input`.
/// as R1CS constraints).
/// encoded in `circuit_pvk`, with respect to the public input
/// `public_input`. as R1CS constraints).
fn verify_with_processed_vk(
circuit_pvk: &Self::ProcessedVerifyingKey,
public_input: &[F],
Expand Down Expand Up @@ -102,21 +102,23 @@ pub enum UniversalSetupIndexError<Bound, E> {
/// A SNARK with universal setup. That is, a SNARK where the trusted setup is
/// circuit-independent.
pub trait UniversalSetupSNARK<F: PrimeField>: SNARK<F> {
/// Specifies how to bound the size of public parameters required to generate
/// the index proving and verification keys for a given circuit.
/// Specifies how to bound the size of public parameters required to
/// generate the index proving and verification keys for a given
/// circuit.
type ComputationBound: Clone + Default + Debug;
/// Specifies the type of universal public parameters.
type PublicParameters: Clone + Debug;

/// Specifies how to bound the size of public parameters required to generate
/// the index proving and verification keys for a given circuit.
/// Specifies how to bound the size of public parameters required to
/// generate the index proving and verification keys for a given
/// circuit.
fn universal_setup<R: RngCore + CryptoRng>(
compute_bound: &Self::ComputationBound,
rng: &mut R,
) -> Result<Self::PublicParameters, Self::Error>;

/// Indexes the public parameters according to the circuit `circuit`, and outputs
/// circuit-specific proving and verification keys.
/// Indexes the public parameters according to the circuit `circuit`, and
/// outputs circuit-specific proving and verification keys.
fn index<C: ConstraintSynthesizer<F>, R: RngCore + CryptoRng>(
pp: &Self::PublicParameters,
circuit: C,
Expand Down