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.

Sign up for GitHub

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
Merged

Finalize #334

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
27f8b80
finalize method
npwardberkeley Dec 31, 2020
31a16cd
setter/getter, and wrapprs in ConstraintSystemRef
npwardberkeley Dec 31, 2020
4c4ad1c
style
npwardberkeley Dec 31, 2020
afd19bb
incorporate comments
npwardberkeley Dec 31, 2020
974ef4f
constraints as default optimization goal
npwardberkeley Dec 31, 2020
32e5206
remove reduce_constraint_weight
npwardberkeley Jan 3, 2021
a31f000
None still inlines
npwardberkeley Jan 3, 2021
7f9ef99
export OptimizationGoal; add assertion checks
weikengchen Jan 4, 2021
b58393a
retouch the comments
weikengchen Jan 4, 2021
9de6b0c
update the changelog
weikengchen Jan 4, 2021
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
101 changes: 72 additions & 29 deletions relations/src/r1cs/constraint_system.rs
View file
Open in desktop
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,18 @@ 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 •
edited
Loading

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 •
edited
Loading

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.

/// Make no attempt to optimize.
None,
/// 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 +125,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 +147,8 @@ impl<F: Field> ConstraintSystem<F> {
mode: SynthesisMode::Prove {
construct_matrices: true,
},

optimization_goal: OptimizationGoal::Constraints,
}
}

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

/// Check whether this constraint system aims to optimize weight,
/// number of constraints, or neither.
pub fn optimization_goal(&self) -> OptimizationGoal {
self.optimization_goal
}

/// Specify whether this constraint system should aim to optimize weight,
/// number of constraints, or neither.
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 +268,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 Down Expand Up @@ -269,7 +300,6 @@ impl<F: Field> ConstraintSystem<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 @@ -473,16 +504,14 @@ impl<F: Field> ConstraintSystem<F> {
}
}

/// Reduce the constraint weight.
///
/// At this moment, it is a wrapper to `outline_lcs`.
/// More weight reductions may be added later.
///
/// 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) {
self.outline_lcs();
/// Finalize the constraint system (either by outlining or inlining,
/// if an optimization goal is set).
pub fn finalize(&mut self) {
match self.optimization_goal {
OptimizationGoal::None => (),
weikengchen marked this conversation as resolved.
Show resolved Hide resolved
OptimizationGoal::Constraints => self.inline_all_lcs(),
OptimizationGoal::Weight => self.outline_lcs(),
};
}

/// This step must be called after constraint generation has completed, and
Expand Down Expand Up @@ -782,6 +811,23 @@ impl<F: Field> ConstraintSystemRef<F> {
.map_or(0, |cs| cs.borrow().num_witness_variables)
}

/// Check whether this constraint system aims to optimize weight,
/// number of constraints, or neither.
#[inline]
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,
/// number of constraints, or neither.
#[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 @@ -864,14 +910,11 @@ impl<F: Field> ConstraintSystemRef<F> {
}
}

/// Reduce the constraint weight.
///
/// 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(&self) {
/// Finalize the constraint system (either by outlining or inlining,
/// if an optimization goal is set).
pub fn finalize(&self) {
if let Some(cs) = self.inner() {
cs.borrow_mut().reduce_constraint_weight()
cs.borrow_mut().finalize()
}
}

Expand Down
26 changes: 14 additions & 12 deletions snark/src/lib.rs
View file
Open in desktop
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