From e686eeaee35878ab3853588f12259f0fb524c429 Mon Sep 17 00:00:00 2001 From: Alireza Shirzad Date: Tue, 6 Aug 2024 17:36:19 -0400 Subject: [PATCH] r1cs replaced with gr1cs --- Cargo.toml | 3 +- relations/Cargo.toml | 2 + relations/src/gr1cs/constraint_system.rs | 660 ++++++++++ relations/src/gr1cs/constraint_system_ref.rs | 366 ++++++ .../local_predicate/lookup_constraint.rs | 18 + relations/src/gr1cs/local_predicate/mod.rs | 150 +++ .../local_predicate/polynomial_constraint.rs | 34 + relations/src/gr1cs/mod.rs | 100 ++ relations/src/gr1cs/namespace.rs | 44 + relations/src/gr1cs/tests/circuit1.rs | 137 ++ relations/src/gr1cs/tests/circuit2.rs | 75 ++ relations/src/gr1cs/tests/mod.rs | 104 ++ relations/src/{r1cs => gr1cs}/trace.rs | 34 +- relations/src/lib.rs | 3 +- relations/src/r1cs/constraint_system.rs | 1171 ----------------- relations/src/{r1cs => utils}/error.rs | 23 + .../linear_combination.rs} | 13 +- relations/src/utils/matrix.rs | 30 + relations/src/utils/mod.rs | 11 + .../src/{r1cs/mod.rs => utils/variable.rs} | 58 +- rustfmt.toml | 2 +- snark/src/lib.rs | 16 +- 22 files changed, 1805 insertions(+), 1249 deletions(-) create mode 100644 relations/src/gr1cs/constraint_system.rs create mode 100644 relations/src/gr1cs/constraint_system_ref.rs create mode 100644 relations/src/gr1cs/local_predicate/lookup_constraint.rs create mode 100644 relations/src/gr1cs/local_predicate/mod.rs create mode 100644 relations/src/gr1cs/local_predicate/polynomial_constraint.rs create mode 100644 relations/src/gr1cs/mod.rs create mode 100644 relations/src/gr1cs/namespace.rs create mode 100644 relations/src/gr1cs/tests/circuit1.rs create mode 100644 relations/src/gr1cs/tests/circuit2.rs create mode 100644 relations/src/gr1cs/tests/mod.rs rename relations/src/{r1cs => gr1cs}/trace.rs (92%) delete mode 100644 relations/src/r1cs/constraint_system.rs rename relations/src/{r1cs => utils}/error.rs (72%) rename relations/src/{r1cs/impl_lc.rs => utils/linear_combination.rs} (96%) create mode 100644 relations/src/utils/matrix.rs create mode 100644 relations/src/utils/mod.rs rename relations/src/{r1cs/mod.rs => utils/variable.rs} (64%) diff --git a/Cargo.toml b/Cargo.toml index e7340958b..0db5a326a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -36,4 +36,5 @@ debug = true ark-ff = { git = "https://github.com/arkworks-rs/algebra/" } ark-ec = { git = "https://github.com/arkworks-rs/algebra/" } ark-poly = { git = "https://github.com/arkworks-rs/algebra/" } -ark-serialize = { git = "https://github.com/arkworks-rs/algebra/" } \ No newline at end of file +ark-serialize = { git = "https://github.com/arkworks-rs/algebra/" } +ark-std = { git = "https://github.com/arkworks-rs/std" } \ No newline at end of file diff --git a/relations/Cargo.toml b/relations/Cargo.toml index 2729f8eb8..7cde41a34 100644 --- a/relations/Cargo.toml +++ b/relations/Cargo.toml @@ -15,6 +15,8 @@ edition = "2021" [dependencies] ark-ff = { version = "0.4.0", default-features = false } ark-std = { version = "0.4.0", default-features = false } +ark-poly = { version = "0.4.0", default-features = false } +ark-serialize = { version = "0.4.0", default-features = false } tracing = { version = "0.1", default-features = false } tracing-subscriber = { version = "0.2", default-features = false, optional = true } diff --git a/relations/src/gr1cs/constraint_system.rs b/relations/src/gr1cs/constraint_system.rs new file mode 100644 index 000000000..0b72e5c72 --- /dev/null +++ b/relations/src/gr1cs/constraint_system.rs @@ -0,0 +1,660 @@ +use super::{ + local_predicate::{polynomial_constraint::R1CS_PREDICATE_LABEL, LocalPredicate}, + Constraint, ConstraintSystemRef, Label, OptimizationGoal, SynthesisMode, +}; +#[cfg(feature = "std")] +use crate::gr1cs::ConstraintTrace; +use crate::gr1cs::{LcIndex, LinearCombination, Matrix, SynthesisError, Variable}; +use ark_ff::Field; +use ark_std::{ + any::{Any, TypeId}, + boxed::Box, + cell::{Ref, RefCell, RefMut}, + collections::BTreeMap, + format, + iterable::Iterable, + rc::Rc, + string::{String, ToString}, + vec::{self, Vec}, +}; + +/////////////////////////////////////////////////////////////////////////////////////// + +/// An Rank-One `ConstraintSystem`. Enforces constraints of the form +/// `L_i(⟨M_{i,1}, z⟩ , ⟨M_{i,2}, z⟩ , ..., ⟨M_{i,t_i}, z⟩)=0`, where L_i is a +/// local predicate, and `M_{i,j}`s are linear combinations over variables, and +/// `z` is the concrete assignment to these variables. refer to //TODO: Paper Url +#[derive(Debug, Clone)] +pub struct ConstraintSystem { + /// The mode in which the constraint system is operating. `self` can either + /// be in setup mode (i.e., `self.mode == SynthesisMode::Setup`) or in + /// proving mode (i.e., `self.mode == SynthesisMode::Prove`). If we are + /// in proving mode, then we have the additional option of whether or + /// not to construct the A, B, and C matrices of the constraint system + mode: SynthesisMode, + + /// The number of variables that are "public inputs" to the constraint + /// system. + num_instance_variables: usize, + + /// The number of variables that are "private inputs" to the constraint + /// system. + num_witness_variables: usize, + + /// The number of linear combinations + num_linear_combinations: usize, + + /// The parameter we aim to minimize in this constraint system (either the + /// number of constraints or their total weight). + optimization_goal: OptimizationGoal, + + /// Assignments to the public input variables. This is empty if `self.mode + /// == SynthesisMode::Setup`. + instance_assignment: Vec, + + /// Assignments to the private input variables. This is empty if `self.mode + /// == SynthesisMode::Setup`. + witness_assignment: Vec, + + /// Map for gadgets to cache computation results. + cache_map: Rc>>>, + + /// A data structure to store the linear combinations. We use map because + /// it's easier to inline and outline the linear combinations. + lc_map: BTreeMap>, + + /// A map from the the local predicate labels to the local predicates + local_predicates: BTreeMap>, + + /// A cache for the linear combination assignments. It shows evaluation + /// result of each linear combination + lc_assignment_cache: Rc>>, + + /// data structure to store the traces for each predicate + #[cfg(feature = "std")] + pub predicate_traces: BTreeMap>>, +} + +impl Default for ConstraintSystem { + fn default() -> Self { + Self::new() + } +} + +impl ConstraintSystem { + pub fn new() -> Self { + Self { + num_instance_variables: 1, + num_witness_variables: 0, + num_linear_combinations: 0, + local_predicates: BTreeMap::new(), + instance_assignment: vec![F::one()], + witness_assignment: Vec::new(), + cache_map: Rc::new(RefCell::new(BTreeMap::new())), + lc_map: BTreeMap::new(), + lc_assignment_cache: Rc::new(RefCell::new(BTreeMap::new())), + mode: SynthesisMode::Prove { + construct_matrices: true, + }, + optimization_goal: OptimizationGoal::Constraints, + #[cfg(feature = "std")] + predicate_traces: BTreeMap::new(), + } + } + + /// Create a new `ConstraintSystemRef`. + pub fn new_ref() -> ConstraintSystemRef { + ConstraintSystemRef::new(Self::new()) + } + + /// Returns the number of constraints which is the sum of the number of + /// constraints in each local predicate. + pub fn num_constraints(&self) -> usize { + self.local_predicates + .values() + .map(|p| p.num_constraints()) + .sum() + } + + /// Returns the number of instance variables. + pub fn num_instance_variables(&self) -> usize { + self.num_instance_variables + } + + /// Returns the number of witness variables. + pub fn num_witness_variables(&self) -> usize { + self.num_witness_variables + } + + /// Returns the number of local predicates + pub fn num_local_predicates(&self) -> usize { + self.local_predicates.len() + } + + /// Enforce a constraint in the constraint system. It takes a local + /// predicate name and enforces a vector of linear combinations of the + /// length of the arity of the local predicate enforces the constraint. + #[inline] + pub fn enforce_constraint( + &mut self, + local_predicate_label: &str, + lc_vec: Vec>, + ) -> crate::gr1cs::Result<()> { + if !self.local_predicates.contains_key(local_predicate_label) { + return Err(SynthesisError::PredicateNotFound); + } + if self.should_construct_matrices() { + let constraint = self.new_lc_vec(lc_vec)?; + self.local_predicates + .get_mut(local_predicate_label) + .unwrap() + .enforce_constraint(constraint)?; + } + #[cfg(feature = "std")] + { + let trace = ConstraintTrace::capture(); + match self.predicate_traces.get_mut(local_predicate_label) { + Some(traces) => traces.push(trace), + None => (), + } + } + Ok(()) + } + + /// Enforce an r1cs constraint in the constraint system. It takes a, b, and + /// c and enforces `a * b = c`. If R1CS predicate does not exist in the + /// constraint system, It will create one. This function is a special case + /// of `enforce_constraint` and is used as the legacy R1CS API to be bacward + /// compatible with R1CS gadgets + #[inline] + pub(super) fn enforce_r1cs_constraint( + &mut self, + a: LinearCombination, + b: LinearCombination, + c: LinearCombination, + cs: ConstraintSystemRef, + ) -> crate::gr1cs::Result<()> { + if !self.local_predicates.contains_key(R1CS_PREDICATE_LABEL) { + self.register_predicate( + R1CS_PREDICATE_LABEL, + LocalPredicate::build_r1cs_predicate(cs), + )?; + } + self.enforce_constraint(R1CS_PREDICATE_LABEL, vec![a, b, c]) + // if self.should_construct_matrices() { + // let constraints = self.new_lc_vec(vec![a, b, c])?; + // self.local_predicates + // .get_mut(R1CS_PREDICATE_LABEL) + // .unwrap() + // .enforce_constraint(constraints)?; + // } + // Ok(()) + } + + /// Add a new vector of linear combinations to the constraint system. + pub fn new_lc_vec( + &mut self, + lc_vec: Vec>, + ) -> crate::gr1cs::Result { + let mut constraints: Constraint = Vec::new(); + for lc in lc_vec { + let var = self.new_lc(lc)?; + match var { + Variable::SymbolicLc(index) => constraints.push(index), + _ => return Err(SynthesisError::UnexpectedVariable), + } + } + Ok(constraints) + } + + // TODO: Check whether It's worth it to deduplicate the linear combinations + // Reduces the memory but each time we need to check the map + #[inline] + pub fn new_lc(&mut self, lc: LinearCombination) -> crate::gr1cs::Result { + for (this_lc_ind, this_lc) in self.lc_map.iter() { + if lc == *this_lc { + return Ok(Variable::SymbolicLc(*this_lc_ind)); + } + } + let index = LcIndex(self.num_linear_combinations); + self.lc_map.insert(index, lc); + self.num_linear_combinations += 1; + Ok(Variable::SymbolicLc(index)) + } + + /// Set `self.mode` to `mode`. + pub fn set_mode(&mut self, mode: SynthesisMode) { + self.mode = mode; + } + + /// Check whether `self.mode == SynthesisMode::Setup`. + /// Returns true if 1- There is an underlying ConstraintSystem and + /// 2- It's in setup mode + pub fn is_in_setup_mode(&self) -> bool { + 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 + } + + /// Check whether this constraint system is new, i.e., it is just created + fn is_new(&self) -> bool { + self.num_instance_variables == 1 + && self.num_witness_variables == 0 + && self.num_constraints() == 0 + && self.num_linear_combinations == 0 + } + + /// Specify whether this constraint system should aim to optimize weight, + /// number of constraints, or neither. + pub fn set_optimization_goal(&mut self, goal: OptimizationGoal) { + assert!(self.is_new()); + self.optimization_goal = goal; + } + + /// Check whether or not `self` will construct matrices. + pub fn should_construct_matrices(&self) -> bool { + match self.mode { + SynthesisMode::Setup => true, + SynthesisMode::Prove { construct_matrices } => construct_matrices, + } + } + + /// Obtain a variable representing a new public instance input + /// This function takes a closure, this closure returns `Result` + /// Internally, this function calls new_input_variable of the constraint + /// system to which it's pointing + #[inline] + pub fn new_input_variable(&mut self, f: Func) -> crate::utils::Result + where + Func: FnOnce() -> crate::utils::Result, + { + let index = self.num_instance_variables; + self.num_instance_variables += 1; + + if !self.is_in_setup_mode() { + self.instance_assignment.push(f()?); + } + Ok(Variable::Instance(index)) + } + + /// Obtain a variable representing a new private witness input. + #[inline] + pub fn new_witness_variable(&mut self, f: Func) -> crate::utils::Result + where + Func: FnOnce() -> crate::utils::Result, + { + let index = self.num_witness_variables; + self.num_witness_variables += 1; + + if !self.is_in_setup_mode() { + self.witness_assignment.push(f()?); + } + Ok(Variable::Witness(index)) + } + + /// Register a local predicate in the constraint system with a given label. + pub fn register_predicate( + &mut self, + predicate_label: &str, + predicate: LocalPredicate, + ) -> crate::utils::Result<()> { + self.local_predicates + .insert(predicate_label.to_string(), predicate); + #[cfg(feature = "std")] + { + self.predicate_traces + .insert(predicate_label.to_string(), Vec::new()); + } + Ok(()) + } + + /// Obtain the assignment corresponding to the `Variable` `v`. + pub fn assigned_value(&self, v: Variable) -> Option { + match v { + Variable::One => Some(F::one()), + Variable::Zero => Some(F::zero()), + Variable::Witness(idx) => self.witness_assignment.get(idx).copied(), + Variable::Instance(idx) => self.instance_assignment.get(idx).copied(), + Variable::SymbolicLc(idx) => { + let value = self.lc_assignment_cache.borrow().get(&idx).copied(); + if value.is_some() { + value + } else { + let value = self.eval_lc(idx)?; + self.lc_assignment_cache.borrow_mut().insert(idx, value); + Some(value) + } + }, + } + } + + /// Evaluate the linear combination `lc` with the assigned values and return + /// the result. + fn eval_lc(&self, lc: LcIndex) -> Option { + let lc = self.lc_map.get(&lc)?; + let mut acc = F::zero(); + for (coeff, var) in lc.iter() { + acc += *coeff * self.assigned_value(*var)?; + } + Some(acc) + } + + /// If `self` is satisfied, outputs `Ok(true)`. + /// If `self` is unsatisfied, outputs `Ok(false)`. + /// If `self.is_in_setup_mode()` or if `self == None`, outputs `Err(())`. + pub fn is_satisfied(&self) -> crate::utils::Result { + self.which_predicate_is_unsatisfied().map(|s| s.is_none()) + } + + /// If `self` is satisfied, outputs `Ok(None)`. + /// If `self` is unsatisfied, outputs `Some(s,i)`, where `s` is the label of + /// the unsatisfied local prediacate and `i` is the index of + /// the first unsatisfied constraint in that local predicate. + /// If `self.is_in_setup_mode()` or `self == None`, outputs `Err(())`. + pub fn which_predicate_is_unsatisfied(&self) -> crate::utils::Result> { + if self.is_in_setup_mode() { + Err(SynthesisError::AssignmentMissing) + } else { + for (label, predicate) in self.local_predicates.iter() { + if let Some(unsatisfied_constraint) = predicate.which_constraint_is_unsatisfied() { + let mut trace: String = "".to_string(); + #[cfg(feature = "std")] + { + trace = self + .predicate_traces + .get(label) + .unwrap() + .get(unsatisfied_constraint) + .unwrap() + .as_ref() + .map_or_else( + || { + eprintln!( + "Constraint trace requires enabling `ConstraintLayer`" + ); + format!("{} - {}", label.clone(), unsatisfied_constraint) + }, + |t| format!("{}", t), + ); + } + #[cfg(not(feature = "std"))] + { + trace = format!("{} - {}", label.clone(), unsatisfied_constraint); + } + return Ok(Some(trace)); + } + } + Ok(None) + } + } + + /// 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 => self.inline_all_lcs(), + OptimizationGoal::Constraints => self.inline_all_lcs(), + OptimizationGoal::Weight => self.outline_lcs(), + }; + } + + /// Naively inlines symbolic linear combinations into the linear + /// combinations that use them. + /// + /// Useful for standard pairing-based SNARKs where addition gates are cheap. + /// For example, in the SNARKs such as [\[Groth16\]](https://eprint.iacr.org/2016/260) and + /// [\[Groth-Maller17\]](https://eprint.iacr.org/2017/540), addition gates + /// do not contribute to the size of the multi-scalar multiplication, which + /// is the dominating cost. + pub fn inline_all_lcs(&mut self) { + // Only inline when a matrix representing R1CS is needed. + if !self.should_construct_matrices() { + return; + } + + // A dummy closure is used, which means that + // - it does not modify the inlined LC. + // - it does not add new witness variables. + self.transform_lc_map(&mut |_, _, _| (0, None)); + } + + /// If a `SymbolicLc` is used in more than one location and has sufficient + /// length, this method makes a new variable for that `SymbolicLc`, adds + /// a constraint ensuring the equality of the variable and the linear + /// combination, and then uses that variable in every location the + /// `SymbolicLc` is used. + /// + /// 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. + fn outline_lcs(&mut self) { + // Only inline when a matrix representing R1CS is needed. + if !self.should_construct_matrices() { + return; + } + + // Store information about new witness variables created + // for outlining. New constraints will be added after the + // transformation of the LC map. + let mut new_witness_linear_combinations = Vec::new(); + let mut new_witness_indices = Vec::new(); + + // It goes through all the LCs in the map, starting from + // the early ones, and decides whether or not to dedicate a witness + // variable for this LC. + // + // 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. + // + self.transform_lc_map(&mut |cs, num_times_used, inlined_lc| { + let mut should_dedicate_a_witness_variable = false; + let mut new_witness_index = None; + let mut new_witness_assignment = Vec::new(); + + // Check if it is worthwhile to dedicate a witness variable. + let this_used_times = num_times_used + 1; + let this_len = inlined_lc.len(); + + // Cost with no outlining = `lc_len * number of usages` + // Cost with outlining is one constraint for `(lc_len) * 1 = {new variable}` and + // using that single new variable in each of the prior usages. + // This has total cost `number_of_usages + lc_len + 2` + if this_used_times * this_len > this_used_times + 2 + this_len { + should_dedicate_a_witness_variable = true; + } + + // If it is worthwhile to dedicate a witness variable, + if should_dedicate_a_witness_variable { + // Add a new witness (the value of the linear combination). + // This part follows the same logic of `new_witness_variable`. + let witness_index = cs.num_witness_variables; + new_witness_index = Some(witness_index); + + // Compute the witness assignment. + if !cs.is_in_setup_mode() { + let mut acc = F::zero(); + for (coeff, var) in inlined_lc.iter() { + acc += *coeff * &cs.assigned_value(*var).unwrap(); + } + new_witness_assignment.push(acc); + } + + // Add a new constraint for this new witness. + new_witness_linear_combinations.push(inlined_lc.clone()); + new_witness_indices.push(witness_index); + + // Replace the linear combination with (1 * this new witness). + *inlined_lc = LinearCombination::from(Variable::Witness(witness_index)); + } + // Otherwise, the LC remains unchanged. + + // Return information about new witness variables. + if new_witness_index.is_some() { + (1, Some(new_witness_assignment)) + } else { + (0, None) + } + }); + + // Add the constraints for the newly added witness variables. + for (new_witness_linear_combination, new_witness_variable) in + new_witness_linear_combinations + .iter() + .zip(new_witness_indices.iter()) + { + // Add a new constraint + self.enforce_r1cs_constraint( + new_witness_linear_combination.clone(), + LinearCombination::from(Variable::one()), + LinearCombination::from(Variable::Witness(*new_witness_variable)), + ConstraintSystemRef::new(self.clone()), + ) + .unwrap(); + } + } + + /// 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, usize, + /// &mut LinearCombination) + /// + /// The transformer function returns the number of new witness variables + /// needed and a vector of new witness assignments (if not in the setup + /// mode). + pub fn transform_lc_map( + &mut self, + transformer: &mut dyn FnMut( + &ConstraintSystem, + usize, + &mut LinearCombination, + ) -> (usize, Option>), + ) { + // `transformed_lc_map` stores the transformed linear combinations. + let mut transformed_lc_map = BTreeMap::<_, LinearCombination>::new(); + let mut num_times_used = self.lc_num_times_used(false); + + // This loop goes through all the LCs in the map, starting from + // the early ones. The transformer function is applied to the + // inlined LC, where new witness variables can be created. + for (&index, lc) in &self.lc_map { + let mut transformed_lc = LinearCombination::new(); + + // Inline the LC, unwrapping symbolic LCs that may constitute it, + // and updating them according to transformations in prior iterations. + for &(coeff, var) in lc.iter() { + if var.is_lc() { + let lc_index = var.get_lc_index().expect("should be lc"); + + // If `var` is a `SymbolicLc`, fetch the corresponding + // inlined LC, and substitute it in. + // + // We have the guarantee that `lc_index` must exist in + // `new_lc_map` since a LC can only depend on other + // LCs with lower indices, which we have transformed. + // + let lc = transformed_lc_map + .get(&lc_index) + .expect("should be inlined"); + transformed_lc.extend((lc * coeff).0.into_iter()); + + // 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. + // + // * 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 { + // This lc is not used any more, so remove it. + transformed_lc_map.remove(&lc_index); + } + } else { + // Otherwise, it's a concrete variable and so we + // substitute it in directly. + transformed_lc.push((coeff, var)); + } + } + transformed_lc.compactify(); + + // Call the transformer function. + let (num_new_witness_variables, new_witness_assignments) = + transformer(&self, num_times_used[index.0], &mut transformed_lc); + + // Insert the transformed LC. + transformed_lc_map.insert(index, transformed_lc); + + // Update the witness counter. + self.num_witness_variables += num_new_witness_variables; + + // Supply additional witness assignments if not in the + // setup mode and if new witness variables are created. + if !self.is_in_setup_mode() && num_new_witness_variables > 0 { + assert!(new_witness_assignments.is_some()); + if let Some(new_witness_assignments) = new_witness_assignments { + assert_eq!(new_witness_assignments.len(), num_new_witness_variables); + self.witness_assignment + .extend_from_slice(&new_witness_assignments); + } + } + } + // Replace the LC map. + self.lc_map = transformed_lc_map; + } + + /// Count the number of times each linear combination is used. + fn lc_num_times_used(&self, count_sinks: bool) -> Vec { + let mut num_times_used = vec![0; self.lc_map.len()]; + + // Iterate over every lc in constraint system + for (index, lc) in self.lc_map.iter() { + num_times_used[index.0] += count_sinks as usize; + + // Increment the counter for each lc that this lc has a direct dependency on. + for &(_, var) in lc.iter() { + if var.is_lc() { + let lc_index = var.get_lc_index().expect("should be lc"); + num_times_used[lc_index.0] += 1; + } + } + } + num_times_used + } + + pub fn to_matrices(&self) -> crate::gr1cs::Result>>> { + let mut matrices = BTreeMap::new(); + for (label, predicate) in self.local_predicates.iter() { + matrices.insert(label.clone(), predicate.to_matrices()); + } + Ok(matrices) + } + + /// Get the linear combination corresponding to the given `lc_index`. + /// TODO: This function should return a reference to the linear combination + /// and not clone it. + pub fn get_lc(&self, lc_index: LcIndex) -> crate::gr1cs::Result> { + self.lc_map + .get(&lc_index) + .cloned() + .ok_or(SynthesisError::LcNotFound) + } +} diff --git a/relations/src/gr1cs/constraint_system_ref.rs b/relations/src/gr1cs/constraint_system_ref.rs new file mode 100644 index 000000000..a714e56d3 --- /dev/null +++ b/relations/src/gr1cs/constraint_system_ref.rs @@ -0,0 +1,366 @@ +use ark_std::collections::BTreeMap; +use core::cell::{Ref, RefCell, RefMut}; + +use ark_ff::Field; +use ark_std::{rc::Rc, string::String, vec::Vec}; + +use super::{ + constraint_system::ConstraintSystem, local_predicate::LocalPredicate, Constraint, Label, + LcIndex, LinearCombination, Matrix, OptimizationGoal, SynthesisError, SynthesisMode, Variable, +}; + +/// A shared reference to a constraint system that can be stored in high level +/// variables. +#[derive(Debug, Clone)] +pub enum ConstraintSystemRef { + /// Represents the case where we *don't* need to allocate variables or + /// enforce constraints. Encountered when operating over constant + /// values. + None, + /// Represents the case where we *do* allocate variables or enforce + /// constraints. + CS(Rc>>), +} + +impl PartialEq for ConstraintSystemRef { + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (Self::None, Self::None) => true, + (..) => false, + } + } +} + +impl Eq for ConstraintSystemRef {} + +impl ConstraintSystemRef { + /// Construct a `ConstraintSystemRef` from a `ConstraintSystem`. + #[inline] + pub fn new(inner: ConstraintSystem) -> Self { + Self::CS(Rc::new(RefCell::new(inner))) + } + + /// Returns the number of constraints which is the sum of the number of + /// constraints in each local predicate. #[inline] + pub fn num_constraints(&self) -> usize { + self.inner().map_or(0, |cs| cs.borrow().num_constraints()) + } + + /// Returns the number of instance variables. + #[inline] + pub fn num_instance_variables(&self) -> usize { + self.inner() + .map_or(0, |cs| cs.borrow().num_instance_variables()) + } + + /// Returns the number of witness variables. + #[inline] + pub fn num_witness_variables(&self) -> usize { + self.inner() + .map_or(0, |cs| cs.borrow().num_witness_variables()) + } + + /// Returns the number of local predicates + #[inline] + pub fn num_local_predicates(&self) -> usize { + self.inner() + .map_or(0, |cs| cs.borrow().num_local_predicates()) + } + + /// Enforce a constraint in the constraint system. It takes a local + /// predicate name and enforces a vector of linear combinations of the + /// length of the arity of the local predicate enforces the constraint. + #[inline] + pub fn enforce_constraint( + &mut self, + local_predicate_label: &str, + lc_vec: Vec>, + ) -> crate::gr1cs::Result<()> { + self.call_on_mut_inner(|cs| cs.enforce_constraint(local_predicate_label, lc_vec)) + } + + /// Enforce an r1cs constraint in the constraint system. It takes a, b, and + /// c and enforces `a * b = c`. If R1CS predicate does not exist in the + /// constraint system, It will create one. This function is a special case + /// of `enforce_constraint` and is used as the legacy R1CS API to be bacward + /// compatible with R1CS gadgets. + #[inline] + pub fn enforce_r1cs_constraint( + &self, + a: LinearCombination, + b: LinearCombination, + c: LinearCombination, + ) -> crate::gr1cs::Result<()> { + self.call_on_mut_inner(|cs| cs.enforce_r1cs_constraint(a, b, c,self.clone())) + } + + /// Obtain a variable representing a linear combination. + #[inline] + pub fn new_lc( + &self, + lc: LinearCombination, + ) -> crate::gr1cs::Result { + self.call_on_mut_inner(|cs| cs.new_lc(lc)) + } + /// Set `self.mode` to `mode`. + /// Sets the mode if there exists an underlying ConstrainSystem + pub fn set_mode(&self, mode: SynthesisMode) { + self.inner().map_or((), |cs| cs.borrow_mut().set_mode(mode)) + } + + /// Check whether `self.mode == SynthesisMode::Setup`. + /// Returns true if 1- There is an underlying ConstraintSystem and + /// 2- It's in setup mode + #[inline] + pub fn is_in_setup_mode(&self) -> bool { + self.inner() + .map_or(false, |cs| cs.borrow().is_in_setup_mode()) + } + + /// 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 { + self.inner() + .map_or(false, |cs| cs.borrow().should_construct_matrices()) + } + + /// Obtain a variable representing a new public instance input + /// This function takes a closure, this closure returns `Result` + /// Internally, this function calls new_input_variable of the constraint + /// system to which it's pointing + #[inline] + pub fn new_input_variable(&self, f: Func) -> crate::utils::Result + where + Func: FnOnce() -> crate::utils::Result, + { + self.inner() + .ok_or(SynthesisError::MissingCS) + .and_then(|cs| { + if !self.is_in_setup_mode() { + // This is needed to avoid double-borrows, because `f` + // might itself mutably borrow `cs` (eg: `f = || g.value()`). + let value = f(); + cs.borrow_mut().new_input_variable(|| value) + } else { + cs.borrow_mut().new_input_variable(f) + } + }) + } + + /// Obtain a variable representing a new private witness input. + #[inline] + pub fn new_witness_variable(&self, f: Func) -> crate::utils::Result + where + Func: FnOnce() -> crate::utils::Result, + { + self.inner() + .ok_or(SynthesisError::MissingCS) + .and_then(|cs| { + if !self.is_in_setup_mode() { + // This is needed to avoid double-borrows, because `f` + // might itself mutably borrow `cs` (eg: `f = || g.value()`). + let value = f(); + cs.borrow_mut().new_witness_variable(|| value) + } else { + cs.borrow_mut().new_witness_variable(f) + } + }) + } + + /// Register a local predicate in the constraint system with a given label. + pub fn register_predicate( + &mut self, + predicate_label: &str, + predicate: LocalPredicate, + ) -> crate::utils::Result<()> { + self.call_on_mut_inner(|cs| cs.register_predicate(predicate_label, predicate)) + } + + /// Obtain the assignment corresponding to the `Variable` `v`. + pub fn assigned_value(&self, v: Variable) -> Option { + self.inner().and_then(|cs| cs.borrow().assigned_value(v)) + } + + /// If `self` is satisfied, outputs `Ok(true)`. + /// If `self` is unsatisfied, outputs `Ok(false)`. + /// If `self.is_in_setup_mode()` or if `self == None`, outputs `Err(())`. + pub fn is_satisfied(&self) -> crate::utils::Result { + self.call_on_inner(|cs| cs.is_satisfied()) + } + + /// If `self` is satisfied, outputs `Ok(None)`. + /// If `self` is unsatisfied, outputs `Some(s,i)`, where `s` is the label of + /// the unsatisfied local prediacate and `i` is the index of + /// the first unsatisfied constraint in that local predicate. + /// If `self.is_in_setup_mode()` or `self == None`, outputs `Err(())`. + pub fn which_predicate_is_unsatisfied(&self) -> crate::utils::Result> { + self.call_on_inner(|cs| cs.which_predicate_is_unsatisfied()) + } + + /// 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().finalize() + } + } + + /// Naively inlines symbolic linear combinations into the linear + /// combinations that use them. + /// + /// Useful for standard pairing-based SNARKs where addition gates are cheap. + /// For example, in the SNARKs such as [\[Groth16\]](https://eprint.iacr.org/2016/260) and + /// [\[Groth-Maller17\]](https://eprint.iacr.org/2017/540), addition gates + /// do not contribute to the size of the multi-scalar multiplication, which + /// is the dominating cost. + pub fn inline_all_lcs(&self) { + if let Some(cs) = self.inner() { + cs.borrow_mut().inline_all_lcs() + } + } + + /// Returns `self` if `!self.is_none()`, otherwise returns `other`. + pub fn or(self, other: Self) -> Self { + match self { + ConstraintSystemRef::None => other, + _ => self, + } + } + + /// Returns `true` is `self == ConstraintSystemRef::None`. + pub fn is_none(&self) -> bool { + matches!(self, ConstraintSystemRef::None) + } + + fn call_on_mut_inner(&self, f: T) -> crate::gr1cs::Result + where + T: FnOnce(&mut ConstraintSystem) -> crate::gr1cs::Result, + { + match self { + ConstraintSystemRef::None => Err(SynthesisError::MissingCS), + ConstraintSystemRef::CS(ref cs) => f(&mut cs.borrow_mut()), + } + } + + fn call_on_inner(&self, f: T) -> crate::gr1cs::Result + where + T: FnOnce(&ConstraintSystem) -> crate::gr1cs::Result, + { + match self { + ConstraintSystemRef::None => Err(SynthesisError::MissingCS), + ConstraintSystemRef::CS(ref cs) => f(&cs.borrow()), + } + } + + fn inner(&self) -> Option<&Rc>>> { + match self { + Self::CS(a) => Some(a), + Self::None => None, + } + } + + /// Consumes self to return the inner `ConstraintSystem`. Returns + /// `None` if `Self::CS` is `None` or if any other references to + /// `Self::CS` exist. + pub fn into_inner(self) -> Option> { + match self { + Self::CS(a) => Rc::try_unwrap(a).ok().map(|s| s.into_inner()), + Self::None => None, + } + } + + /// Obtain an immutable reference to the underlying `ConstraintSystem`. + /// + /// # Panics + /// This method panics if `self` is already mutably borrowed. + #[inline] + pub fn borrow(&self) -> Option>> { + self.inner().map(|cs| cs.borrow()) + } + + /// Obtain a mutable reference to the underlying `ConstraintSystem`. + /// + /// # Panics + /// This method panics if `self` is already mutably borrowed. + #[inline] + pub fn borrow_mut(&self) -> Option>> { + self.inner().map(|cs| cs.borrow_mut()) + } + + pub fn to_matrices(&self) -> crate::gr1cs::Result>>> { + self.call_on_inner(|cs| cs.to_matrices()) + } + + pub fn get_lc(&self, lc_index: LcIndex) -> crate::utils::Result> { + self.call_on_inner(|cs| cs.get_lc(lc_index)) + } + +// TODO: Implement this function +// /// Get trace information about all constraints in the system +// pub fn constraint_names(&self) -> Option> { +// #[cfg(feature = "std")] +// { +// self.inner().and_then(|cs| { +// cs.borrow() +// .constraint_traces +// .iter() +// .map(|trace| { +// let mut constraint_path = String::new(); +// let mut prev_module_path = ""; +// let mut prefixes = ark_std::collections::BTreeSet::new(); +// for step in trace.as_ref()?.path() { +// let module_path = if prev_module_path == step.module_path { +// prefixes.insert(step.module_path.to_string()); +// String::new() +// } else { +// let mut parts = step +// .module_path +// .split("::") +// .filter(|&part| part != "r1cs_std" && part != "constraints"); +// let mut path_so_far = String::new(); +// for part in parts.by_ref() { +// if path_so_far.is_empty() { +// path_so_far += part; +// } else { +// path_so_far += &["::", part].join(""); +// } +// if prefixes.contains(&path_so_far) { +// continue; +// } else { +// prefixes.insert(path_so_far.clone()); +// break; +// } +// } +// parts.collect::>().join("::") + "::" +// }; +// prev_module_path = step.module_path; +// constraint_path += &["/", &module_path, step.name].join(""); +// } +// Some(constraint_path) +// }) +// .collect::>>() +// }) +// } +// #[cfg(not(feature = "std"))] +// { +// None +// } +// } +} diff --git a/relations/src/gr1cs/local_predicate/lookup_constraint.rs b/relations/src/gr1cs/local_predicate/lookup_constraint.rs new file mode 100644 index 000000000..5008e134d --- /dev/null +++ b/relations/src/gr1cs/local_predicate/lookup_constraint.rs @@ -0,0 +1,18 @@ +use core::marker::PhantomData; + +use ark_ff::Field; +use ark_std::vec::Vec; + +use super::Evaluatable; + +// TODO +#[derive(Debug, Clone)] +pub struct LookupConstraint { + _marker: PhantomData, +} + +impl Evaluatable for LookupConstraint { + fn evaluate(&self, _point: Vec) -> F { + unimplemented!() + } +} diff --git a/relations/src/gr1cs/local_predicate/mod.rs b/relations/src/gr1cs/local_predicate/mod.rs new file mode 100644 index 000000000..7d3498f4f --- /dev/null +++ b/relations/src/gr1cs/local_predicate/mod.rs @@ -0,0 +1,150 @@ +pub mod lookup_constraint; +pub mod polynomial_constraint; + +use core::{fmt::Debug, ops::Not, pin::Pin}; + +use ark_ff::Field; + +use super::{ + constraint_system, Constraint, ConstraintSystemRef, LcIndex, LinearCombination, Matrix, +}; +use crate::utils::{error::SynthesisError::ArityMismatch, variable::Variable::SymbolicLc}; +use ark_std::{boxed::Box, rc::Rc, vec::Vec}; +use lookup_constraint::LookupConstraint; +use polynomial_constraint::PolynomialConstraint; + +// use crate::{gr1cs::ConstraintSystemRef, utils::Result}; +pub trait Evaluatable { + fn evaluate(&self, point: Vec) -> F; +} + +#[derive(Debug, Clone)] +pub enum ConstraintType +where + PolynomialConstraint: Evaluatable, + LookupConstraint: Evaluatable, +{ + Polynomial(PolynomialConstraint), + Lookup(LookupConstraint), +} + +impl Evaluatable for ConstraintType { + fn evaluate(&self, point: Vec) -> F { + match self { + ConstraintType::Polynomial(p) => p.evaluate(point), + ConstraintType::Lookup(l) => l.evaluate(point), + } + } +} + +#[derive(Debug, Clone)] +pub struct LocalPredicate { + arity: usize, + cs: ConstraintSystemRef, + constraints: Vec, + constraint_type: ConstraintType, +} + +impl LocalPredicate { + fn new(cs: ConstraintSystemRef, arity: usize, constraint_type: ConstraintType) -> Self { + Self { + arity, + cs, + constraints: Vec::new(), + constraint_type, + } + } + + pub fn new_polynomial_predicate( + cs: ConstraintSystemRef, + arity: usize, + terms: Vec<(F, Vec<(usize, usize)>)>, + ) -> Self { + Self::new( + cs, + arity, + ConstraintType::Polynomial(PolynomialConstraint::new(arity, terms)), + ) + } + pub fn get_arity(&self) -> usize { + self.arity + } + + pub fn num_constraints(&self) -> usize { + self.constraints.len() + } + + pub fn get_constraints(&self) -> &Vec { + &self.constraints + } + + pub fn get_cs(&self) -> ConstraintSystemRef { + self.cs.clone() + } + + pub fn get_constraint_type(&self) -> &ConstraintType { + &self.constraint_type + } + + pub fn enforce_constraint(&mut self, constraint: Constraint) -> crate::utils::Result<()> { + if constraint.len() != self.arity { + return Err(ArityMismatch); + } + self.constraints.push(constraint); + Ok(()) + } + + pub fn which_constraint_is_unsatisfied(&self) -> Option { + for (i, constraint) in self.constraints.iter().enumerate() { + let point: Vec = constraint + .iter() + .map(|lc_index| self.cs.assigned_value(SymbolicLc(*lc_index)).unwrap()) + .collect(); + let result = self.constraint_type.evaluate(point); + if !result.is_zero() { + return Some(i); + } + } + None + } + pub fn to_matrices(&self) -> Vec> { + let mut matrices: Vec> = vec![Vec::new(); self.arity]; + for constraint in self.constraints.iter() { + for (matrix_ind, lc_index) in constraint.iter().enumerate() { + let lc: LinearCombination = self.cs.get_lc(*lc_index).unwrap(); + let row: Vec<(F, usize)> = self.make_row(&lc); + matrices[matrix_ind].push(row); + } + } + + matrices + } + + #[inline] + fn make_row(&self, l: &LinearCombination) -> Vec<(F, usize)> { + let num_input = self.cs.num_instance_variables(); + l.0.iter() + .filter_map(|(coeff, var)| { + if coeff.is_zero() { + None + } else { + Some(( + *coeff, + var.get_index_unchecked(num_input).expect("no symbolic LCs"), + )) + } + }) + .collect() + } + + pub fn build_r1cs_predicate(cs: ConstraintSystemRef) -> Self { + Self::new_polynomial_predicate( + cs, + 3, + vec![ + (F::from(1u8), vec![(0, 1),(1,1)]), + (F::from(-1i8), vec![(2, 1)]), + ], + ) + } +} diff --git a/relations/src/gr1cs/local_predicate/polynomial_constraint.rs b/relations/src/gr1cs/local_predicate/polynomial_constraint.rs new file mode 100644 index 000000000..6fc706c83 --- /dev/null +++ b/relations/src/gr1cs/local_predicate/polynomial_constraint.rs @@ -0,0 +1,34 @@ +use ark_ff::Field; +use ark_poly::{ + multivariate::{SparsePolynomial, SparseTerm, Term}, + DenseMVPolynomial, Polynomial, +}; +use ark_std::vec::Vec; + +use crate::gr1cs::{Constraint, ConstraintSystemRef}; + +use super::Evaluatable; + +#[derive(Debug, Clone)] +pub struct PolynomialConstraint { + polynomial: SparsePolynomial, +} + +impl PolynomialConstraint { + pub fn new(arity: usize, terms: Vec<(F, Vec<(usize, usize)>)>) -> Self { + let sparse_terms = terms + .iter() + .map(|(coeff, term)| (coeff.clone(), SparseTerm::new(term.clone()))) + .collect(); + Self { + polynomial: SparsePolynomial::from_coefficients_vec(arity, sparse_terms), + } + } +} + +impl Evaluatable for PolynomialConstraint { + fn evaluate(&self, point: Vec) -> F { + self.polynomial.evaluate(&point) + } +} +pub const R1CS_PREDICATE_LABEL: &str = "R1CS"; diff --git a/relations/src/gr1cs/mod.rs b/relations/src/gr1cs/mod.rs new file mode 100644 index 000000000..4080fa592 --- /dev/null +++ b/relations/src/gr1cs/mod.rs @@ -0,0 +1,100 @@ +//! Core interface for working with Generalized Rank-1 Constraint Systems +//! (GR1CS). +mod constraint_system_ref; +mod local_predicate; +mod namespace; +#[macro_use] +mod constraint_system; +#[cfg(test)] +mod tests; +#[cfg(feature = "std")] +mod trace; +/////////////////////////////////////////////////////////////////////////////////////// + +#[cfg(feature = "std")] +pub use crate::gr1cs::trace::{ConstraintLayer, ConstraintTrace, TraceStep, TracingMode}; + +use ark_std::vec::Vec; +pub use tracing::info_span; + +pub use ark_ff::{Field, ToConstraintField}; + +pub use crate::{ + gr1cs::{constraint_system::ConstraintSystem, constraint_system_ref::ConstraintSystemRef}, + lc, + utils::{ + error::SynthesisError, + linear_combination::{LcIndex, LinearCombination}, + matrix::Matrix, + variable::Variable, + Result, + }, +}; +pub use namespace::Namespace; +/////////////////////////////////////////////////////////////////////////////////////// + +/// Computations are expressed in terms of rank-1 constraint systems (R1CS). +/// The `generate_constraints` method is called to generate constraints for +/// both CRS generation and for proving. +// TODO: Think: should we replace this with just a closure? +pub trait ConstraintSynthesizer { + /// Drives generation of new constraints inside `cs`. + fn generate_constraints(self, cs: ConstraintSystemRef) -> crate::gr1cs::Result<()>; +} + +/////////////////////////////////////////////////////////////////////////////////////// + +/// In GR1CS a constraint is a vector of linear combinations associated with a +/// local predicate +pub type Constraint = Vec; + +/// Each predicate is associated with a label +pub type Label = ark_std::string::String; +/////////////////////////////////////////////////////////////////////////////////////// + +/// Defines the mode of operation of a `ConstraintSystem`. +#[derive(Copy, Clone, Debug, Eq, PartialEq, Ord, PartialOrd)] +pub enum SynthesisMode { + /// Indicate to the `ConstraintSystem` that it should only generate + /// constraint matrices and not populate the variable assignments. + Setup, + /// Indicate to the `ConstraintSystem` that it populate the variable + /// assignments. If additionally `construct_matrices == true`, then generate + /// the matrices as in the `Setup` case. + Prove { + /// If `construct_matrices == true`, then generate + /// the matrices as in the `Setup` case. + construct_matrices: bool, + }, +} + +/////////////////////////////////////////////////////////////////////////////////////// + +/// Defines the parameter to optimize for a `ConstraintSystem`. +#[derive(Copy, Clone, Debug, Eq, PartialEq, Ord, PartialOrd)] +pub enum OptimizationGoal { + /// Make no attempt to optimize. + None, + /// Minimize the number of constraints by inlining the linear combinations. + Constraints, + /// Minimize the total weight of the constraints (the number of nonzero + /// entries across all constraints) by outlining the linear combinations + /// and creating new witness variables. + Weight, +} + +/////////////////////////////////////////////////////////////////////////////////////// + +/// Generate a `Namespace` with name `name` from `ConstraintSystem` `cs`. +/// `name` must be a `&'static str`. +#[macro_export] +macro_rules! ns { + ($cs:expr, $name:expr) => {{ + let span = $crate::gr1cs::info_span!(target: "gr1cs", $name); + let id = span.id(); + let _enter_guard = span.enter(); + core::mem::forget(_enter_guard); + core::mem::forget(span); + $crate::gr1cs::Namespace::new($cs.clone(), id) + }}; +} diff --git a/relations/src/gr1cs/namespace.rs b/relations/src/gr1cs/namespace.rs new file mode 100644 index 000000000..6ab4e92fb --- /dev/null +++ b/relations/src/gr1cs/namespace.rs @@ -0,0 +1,44 @@ +use super::ConstraintSystemRef; +use ark_ff::Field; + +/// A namespaced `ConstraintSystemRef`. +#[derive(Debug, Clone)] +pub struct Namespace { + inner: ConstraintSystemRef, + id: Option, +} + +impl From> for Namespace { + fn from(other: ConstraintSystemRef) -> Self { + Self { + inner: other, + id: None, + } + } +} + +impl Namespace { + /// Construct a new `Namespace`. + pub fn new(inner: ConstraintSystemRef, id: Option) -> Self { + Self { inner, id } + } + + /// Obtain the inner `ConstraintSystemRef`. + pub fn cs(&self) -> ConstraintSystemRef { + self.inner.clone() + } + + /// Manually leave the namespace. + pub fn leave_namespace(self) { + drop(self) + } +} + +impl Drop for Namespace { + fn drop(&mut self) { + if let Some(id) = self.id.as_ref() { + tracing::dispatcher::get_default(|dispatch| dispatch.exit(id)) + } + let _ = self.inner; + } +} diff --git a/relations/src/gr1cs/tests/circuit1.rs b/relations/src/gr1cs/tests/circuit1.rs new file mode 100644 index 000000000..7d68d2197 --- /dev/null +++ b/relations/src/gr1cs/tests/circuit1.rs @@ -0,0 +1,137 @@ +use ark_ff::Field; +use ark_poly::{ + multivariate::{SparsePolynomial, SparseTerm, Term}, + DenseMVPolynomial, +}; +use ark_std::{ + collections::BTreeMap, + string::ToString, + vec::{self, Vec}, +}; + +use crate::{ + gr1cs::{ + local_predicate::{self, ConstraintType, LocalPredicate}, + ConstraintSynthesizer, ConstraintSystemRef, + }, + lc, +}; + +use super::{Label, Matrix}; + +#[derive(Debug, Clone)] +pub struct Circuit1 { + pub x1: F, + pub x2: F, + pub x3: F, + pub x4: F, + pub x5: F, + pub w1: F, + pub w2: F, + pub w3: F, + pub w4: F, + pub w5: F, + pub w6: F, + pub w7: F, + pub w8: F, +} + +impl Circuit1 { + pub fn get_matrices() -> BTreeMap>> { + let mut map: BTreeMap>> = BTreeMap::new(); + map.insert( + "poly-predicate-A".to_string(), + vec![ + vec![vec![(F::one(), 1)]], + vec![vec![(F::one(), 2)]], + vec![vec![(F::one(), 3)]], + vec![vec![(F::one(), 9)]], + ], + ); + + map.insert( + "poly-predicate-B".to_string(), + vec![ + vec![vec![(F::one(), 4)], vec![(F::one(), 10)]], + vec![vec![(F::one(), 6)], vec![(F::one(), 11)]], + vec![vec![(F::one(), 10)], vec![(F::one(), 13)]], + ], + ); + map.insert( + "poly-predicate-C".to_string(), + vec![ + vec![vec![(F::one(), 7)], vec![(F::one(), 9), (F::one(), 10)]], + vec![vec![(F::one(), 8)], vec![(F::one(), 13)]], + vec![vec![(F::one(), 11)], vec![(F::one(), 5)]], + ], + ); + map + } +} +impl> ConstraintSynthesizer for Circuit1 { + fn generate_constraints(self, mut cs: ConstraintSystemRef) -> crate::utils::Result<()> { + // Variable declarations -> Instance variables + Witness variables + + let x1 = cs.new_input_variable(|| Ok(self.x1)).unwrap(); + let x2 = cs.new_input_variable(|| Ok(self.x2)).unwrap(); + let x3 = cs.new_input_variable(|| Ok(self.x3)).unwrap(); + let x4 = cs.new_input_variable(|| Ok(self.x4)).unwrap(); + let x5 = cs.new_input_variable(|| Ok(self.x5)).unwrap(); + let w1 = cs.new_witness_variable(|| Ok(self.w1)).unwrap(); + let w2 = cs.new_witness_variable(|| Ok(self.w2)).unwrap(); + let w3 = cs.new_witness_variable(|| Ok(self.w3)).unwrap(); + let w4 = cs.new_witness_variable(|| Ok(self.w4)).unwrap(); + let w5 = cs.new_witness_variable(|| Ok(self.w5)).unwrap(); + let w6 = cs.new_witness_variable(|| Ok(self.w6)).unwrap(); + let w7 = cs.new_witness_variable(|| Ok(self.w7)).unwrap(); + let w8 = cs.new_witness_variable(|| Ok(self.w8)).unwrap(); + + // Local predicate declarations -> Polynomial predicates + + let local_predicate_a = LocalPredicate::new_polynomial_predicate( + cs.clone(), + 4, + vec![ + (F::from(1u8), vec![(0, 1), (1, 1)]), + (F::from(3u8), vec![(2, 2)]), + (F::from(-1i8), vec![(3, 1)]), + ], + ); + let local_predicate_b = LocalPredicate::new_polynomial_predicate( + cs.clone(), + 3, + vec![ + (F::from(7u8), vec![(1, 1)]), + (F::from(1u8), vec![(0, 3)]), + (F::from(-1i8), vec![(2, 1)]), + ], + ); + + let local_predicate_c = LocalPredicate::new_polynomial_predicate( + cs.clone(), + 3, + vec![ + (F::from(1u8), vec![(0, 1), (1, 1)]), + (F::from(-1i8), vec![(2, 1)]), + ], + ); + cs.register_predicate("poly-predicate-A", local_predicate_a)?; + cs.register_predicate("poly-predicate-B", local_predicate_b)?; + cs.register_predicate("poly-predicate-C", local_predicate_c)?; + + // Enforing constraints to the predicates + + let predicate_a_constraint_1 = vec![lc!() + x1, lc!() + x2, lc!() + x3, lc!() + w4]; + let predicate_b_constraint_1 = vec![lc!() + x4, lc!() + w1, lc!() + w5]; + let predicate_c_constraint_1 = vec![lc!() + w2, lc!() + w3, lc!() + w6]; + let predicate_b_constraint_2 = vec![lc!() + w5, lc!() + w6, lc!() + w8]; + let predicate_c_constraint_2 = vec![lc!() + w5 + w4, lc!() + w8, lc!() + x5]; + + cs.enforce_constraint("poly-predicate-A", predicate_a_constraint_1)?; + cs.enforce_constraint("poly-predicate-B", predicate_b_constraint_1)?; + cs.enforce_constraint("poly-predicate-C", predicate_c_constraint_1)?; + cs.enforce_constraint("poly-predicate-B", predicate_b_constraint_2)?; + cs.enforce_constraint("poly-predicate-C", predicate_c_constraint_2)?; + Ok(()) + } +} diff --git a/relations/src/gr1cs/tests/circuit2.rs b/relations/src/gr1cs/tests/circuit2.rs new file mode 100644 index 000000000..d637fe887 --- /dev/null +++ b/relations/src/gr1cs/tests/circuit2.rs @@ -0,0 +1,75 @@ +use ark_ff::Field; +use ark_poly::{ + multivariate::{SparsePolynomial, SparseTerm, Term}, + DenseMVPolynomial, +}; +use ark_std::{ + collections::BTreeMap, + string::ToString, + vec::{self, Vec}, +}; + +use crate::{ + gr1cs::{ + local_predicate::{self, ConstraintType, LocalPredicate}, + ConstraintSynthesizer, ConstraintSystemRef, + }, + lc, +}; + +use super::{ + local_predicate::polynomial_constraint::R1CS_PREDICATE_LABEL, Label, Matrix, Variable, +}; + +#[derive(Debug, Clone)] +pub struct Circuit2 { + pub a: F, + pub b: F, + pub c: F, +} + +impl Circuit2 { + pub fn get_matrices() -> BTreeMap>> { + let two = F::one() + F::one(); + let mut map: BTreeMap>> = BTreeMap::new(); + map.insert( + R1CS_PREDICATE_LABEL.to_string(), + vec![ + vec![ + vec![(F::one(), 1)], + vec![(F::one(), 1)], + vec![(F::one(), 0)], + ], + vec![ + vec![(two, 2)], + vec![(F::one(), 1), (F::one(), 2)], + vec![(two, 1), (two, 2)], + ], + vec![ + vec![(F::one(), 3)], + vec![(F::one(), 1), (F::one(), 2)], + vec![(two, 1), (two, 2)], + ], + ], + ); + + map + } +} +impl> ConstraintSynthesizer for Circuit2 { + fn generate_constraints(self, mut cs: ConstraintSystemRef) -> crate::utils::Result<()> { + // Variable declarations -> Instance variables + Witness variables + let two = F::one() + F::one(); + + let a = cs.new_input_variable(|| Ok(self.a)).unwrap(); + let b = cs.new_witness_variable(|| Ok(self.b)).unwrap(); + let c = cs.new_witness_variable(|| Ok(self.c)).unwrap(); + cs.enforce_r1cs_constraint(lc!() + a, lc!() + (two, b), lc!() + c)?; + let d = cs.new_lc(lc!() + a + b)?; + cs.enforce_r1cs_constraint(lc!() + a, lc!() + d, lc!() + d)?; + let e = cs.new_lc(lc!() + d + d)?; + cs.enforce_r1cs_constraint(lc!() + Variable::One, lc!() + e, lc!() + e)?; + + Ok(()) + } +} diff --git a/relations/src/gr1cs/tests/mod.rs b/relations/src/gr1cs/tests/mod.rs new file mode 100644 index 000000000..a52254f37 --- /dev/null +++ b/relations/src/gr1cs/tests/mod.rs @@ -0,0 +1,104 @@ +mod circuit1; +mod circuit2; +use super::*; +use ark_ff::{One, Zero}; +use ark_test_curves::bls12_381::Fr; +use circuit1::Circuit1; +use circuit2::Circuit2; +use constraint_system::ConstraintSystem; + +#[test] +fn test_circuit1_sat() { + let c = Circuit1 { + x1: Fr::from(1u8), + x2: Fr::from(2u8), + x3: Fr::from(3u8), + x4: Fr::from(0u8), + x5: Fr::from(1255254u32), + w1: Fr::from(4u8), + w2: Fr::from(2u8), + w3: Fr::from(5u8), + w4: Fr::from(29u8), + w5: Fr::from(28u8), + w6: Fr::from(10u8), + w7: Fr::from(57u8), + w8: Fr::from(22022u32), + }; + let cs = ConstraintSystem::::new_ref(); + c.clone().generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert!(cs.borrow().unwrap().is_satisfied().unwrap()); + + let cs = ConstraintSystem::::new_ref(); + cs.set_optimization_goal(OptimizationGoal::Constraints); + c.clone().generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert!(cs.borrow().unwrap().is_satisfied().unwrap()); + + let cs = ConstraintSystem::::new_ref(); + cs.set_optimization_goal(OptimizationGoal::Weight); + c.clone().generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert!(cs.borrow().unwrap().is_satisfied().unwrap()); +} + +/// Test the circuit with non-satisfying inputs +/// The first input is changed comparing to sat test +#[test] +fn test_circuit1_non_sat() { + let c = Circuit1 { + x1: Fr::from(4u8), + x2: Fr::from(2u8), + x3: Fr::from(3u8), + x4: Fr::from(0u8), + x5: Fr::from(1255254u32), + w1: Fr::from(4u8), + w2: Fr::from(2u8), + w3: Fr::from(5u8), + w4: Fr::from(29u8), + w5: Fr::from(28u8), + w6: Fr::from(10u8), + w7: Fr::from(57u8), + w8: Fr::from(22022u32), + }; + let cs = ConstraintSystem::::new_ref(); + c.generate_constraints(cs.clone()).unwrap(); + assert!(!cs.borrow().unwrap().is_satisfied().unwrap()); +} + +#[test] +fn test_circuit1_matrices() { + let c = Circuit1 { + x1: Fr::zero(), + x2: Fr::zero(), + x3: Fr::zero(), + x4: Fr::zero(), + x5: Fr::zero(), + w1: Fr::zero(), + w2: Fr::zero(), + w3: Fr::zero(), + w4: Fr::zero(), + w5: Fr::zero(), + w6: Fr::zero(), + w7: Fr::zero(), + w8: Fr::zero(), + }; + let cs = ConstraintSystem::::new_ref(); + c.clone().generate_constraints(cs.clone()).unwrap(); + assert_eq!(Circuit1::get_matrices(), cs.clone().to_matrices().unwrap()); +} + + +/// This is the legacy test for R1CS from the previous version of the library +#[test] +fn test_circuit2_matrices() { + let c = Circuit2 { + a: Fr::one(), + b: Fr::one(), + c: Fr::one()+Fr::one(), + }; + let cs = ConstraintSystem::::new_ref(); + c.clone().generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert_eq!(Circuit2::get_matrices(), cs.clone().to_matrices().unwrap()); +} diff --git a/relations/src/r1cs/trace.rs b/relations/src/gr1cs/trace.rs similarity index 92% rename from relations/src/r1cs/trace.rs rename to relations/src/gr1cs/trace.rs index a5ce11be6..cc2831c9b 100644 --- a/relations/src/r1cs/trace.rs +++ b/relations/src/gr1cs/trace.rs @@ -11,7 +11,7 @@ use tracing_subscriber::{ registry::LookupSpan, }; -/// A subscriber [`Layer`] that enables capturing a trace of R1CS constraint +/// A subscriber [`Layer`] that enables capturing a trace of GR1CS constraint /// generation. /// /// [`Layer`]: https://docs.rs/tracing-subscriber/0.2.10/tracing_subscriber/layer/trait.Layer.html @@ -29,10 +29,10 @@ pub struct ConstraintLayer { #[derive(PartialEq, Eq, Ord, PartialOrd, Hash, Debug)] pub enum TracingMode { /// Instructs `ConstraintLayer` to filter out any spans that *do not* have - /// `target == "r1cs"`. + /// `target == "gr1cs"`. OnlyConstraints, /// Instructs `ConstraintLayer` to filter out any spans that *do* have - /// `target == "r1cs"`. + /// `target == "gr1cs"`. NoConstraints, /// Instructs `ConstraintLayer` to not filter out any spans. All, @@ -51,8 +51,8 @@ where { fn enabled(&self, metadata: &Metadata<'_>, _ctx: layer::Context<'_, S>) -> bool { match self.mode { - TracingMode::OnlyConstraints => metadata.target() == "r1cs", - TracingMode::NoConstraints => metadata.target() != "r1cs", + TracingMode::OnlyConstraints => metadata.target() == "gr1cs", + TracingMode::NoConstraints => metadata.target() != "gr1cs", TracingMode::All => true, } } @@ -81,10 +81,10 @@ where /// Returns a new `ConstraintLayer`. /// /// If `mode == TracingMode::OnlyConstraints`, the resulting layer will - /// filter out any spans whose `target != "r1cs"`. + /// filter out any spans whose `target != "gr1cs"`. /// /// If `mode == TracingMode::NoConstraints`, the resulting layer will - /// filter out any spans whose `target == "r1cs"`. + /// filter out any spans whose `target == "gr1cs"`. /// /// Finally, if `mode == TracingMode::All`, the resulting layer will /// not filter out any spans. @@ -156,14 +156,14 @@ macro_rules! try_bool { }}; } -/// A captured trace of [`tracing`] spans that have `target = "r1cs"`. +/// A captured trace of [`tracing`] spans that have `target = "gr1cs"`. /// /// This type can be thought of as a relative of /// [`std::backtrace::Backtrace`][`Backtrace`]. /// However, rather than capturing the current call stack when it is /// constructed, a `ConstraintTrace` instead captures the current [span] and its /// [parents]. It allows inspection of the constraints that are left unsatisfied -/// by a particular witness assignment to an R1CS instance. +/// by a particular witness assignment to an GR1CS instance. /// /// # Formatting /// @@ -171,10 +171,10 @@ macro_rules! try_bool { /// trace similarly to how Rust formats panics. For example: /// /// ```text -/// 0: r1cs-std::bits::something -/// at r1cs-std/src/bits/test.rs:42 -/// 1: r1cs-std::bits::another_thing -/// at r1cs-std/src/bits/test.rs:15 +/// 0: gr1cs-std::bits::something +/// at gr1cs-std/src/bits/test.rs:42 +/// 1: gr1cs-std::bits::another_thing +/// at gr1cs-std/src/bits/test.rs:15 /// ``` /// /// [`tracing`]: https://docs.rs/tracing @@ -193,7 +193,7 @@ impl ConstraintTrace { /// /// # Examples /// ```rust - /// use ark_relations::r1cs::ConstraintTrace; + /// use ark_relations::gr1cs::ConstraintTrace; /// /// pub struct MyError { /// trace: Option, @@ -203,7 +203,7 @@ impl ConstraintTrace { /// # fn some_error_condition() -> bool { true } /// /// pub fn my_function(arg: &str) -> Result<(), MyError> { - /// let _span = tracing::info_span!(target: "r1cs", "In my_function"); + /// let _span = tracing::info_span!(target: "gr1cs", "In my_function"); /// let _guard = _span.enter(); /// if some_error_condition() { /// return Err(MyError { @@ -254,7 +254,7 @@ impl ConstraintTrace { pub fn path(&self) -> Vec { let mut path = Vec::new(); self.with_spans(|metadata, _| { - if metadata.target() == "r1cs" { + if metadata.target() == "gr1cs" { let n = metadata.name(); let step = metadata .module_path() @@ -286,7 +286,7 @@ impl fmt::Display for ConstraintTrace { let mut span = 0; self.with_spans(|metadata, _| { - if metadata.target() != "r1cs" { + if metadata.target() != "gr1cs" { return true; } if span > 0 { diff --git a/relations/src/lib.rs b/relations/src/lib.rs index cf249f777..9b6bf9921 100644 --- a/relations/src/lib.rs +++ b/relations/src/lib.rs @@ -15,4 +15,5 @@ #[macro_use] extern crate ark_std; -pub mod r1cs; +pub mod gr1cs; +pub mod utils; diff --git a/relations/src/r1cs/constraint_system.rs b/relations/src/r1cs/constraint_system.rs deleted file mode 100644 index 1b0d54922..000000000 --- a/relations/src/r1cs/constraint_system.rs +++ /dev/null @@ -1,1171 +0,0 @@ -#[cfg(feature = "std")] -use crate::r1cs::ConstraintTrace; -use crate::r1cs::{LcIndex, LinearCombination, Matrix, SynthesisError, Variable}; -use ark_ff::Field; -use ark_std::{ - any::{Any, TypeId}, - boxed::Box, - cell::{Ref, RefCell, RefMut}, - collections::BTreeMap, - format, - rc::Rc, - string::String, - vec, - vec::Vec, -}; - -/// Computations are expressed in terms of rank-1 constraint systems (R1CS). -/// The `generate_constraints` method is called to generate constraints for -/// both CRS generation and for proving. -// TODO: Think: should we replace this with just a closure? -pub trait ConstraintSynthesizer { - /// Drives generation of new constraints inside `cs`. - fn generate_constraints(self, cs: ConstraintSystemRef) -> crate::r1cs::Result<()>; -} - -/// An Rank-One `ConstraintSystem`. Enforces constraints of the form -/// `⟨a_i, z⟩ ⋅ ⟨b_i, z⟩ = ⟨c_i, z⟩`, where `a_i`, `b_i`, and `c_i` are linear -/// combinations over variables, and `z` is the concrete assignment to these -/// variables. -#[derive(Debug, Clone)] -pub struct ConstraintSystem { - /// The mode in which the constraint system is operating. `self` can either - /// be in setup mode (i.e., `self.mode == SynthesisMode::Setup`) or in - /// proving mode (i.e., `self.mode == SynthesisMode::Prove`). If we are - /// in proving mode, then we have the additional option of whether or - /// not to construct the A, B, and C matrices of the constraint system - /// (see below). - pub mode: SynthesisMode, - /// The number of variables that are "public inputs" to the constraint - /// system. - pub num_instance_variables: usize, - /// The number of variables that are "private inputs" to the constraint - /// system. - pub num_witness_variables: usize, - /// The number of constraints in the constraint system. - pub num_constraints: usize, - /// 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, - /// Assignments to the private input variables. This is empty if `self.mode - /// == SynthesisMode::Setup`. - pub witness_assignment: Vec, - - /// Map for gadgets to cache computation results. - pub cache_map: Rc>>>, - - lc_map: BTreeMap>, - - #[cfg(feature = "std")] - constraint_traces: Vec>, - - a_constraints: Vec, - b_constraints: Vec, - c_constraints: Vec, - - lc_assignment_cache: Rc>>, -} - -impl Default for ConstraintSystem { - fn default() -> Self { - Self::new() - } -} - -/// Defines the mode of operation of a `ConstraintSystem`. -#[derive(Copy, Clone, Debug, Eq, PartialEq, Ord, PartialOrd)] -pub enum SynthesisMode { - /// Indicate to the `ConstraintSystem` that it should only generate - /// constraint matrices and not populate the variable assignments. - Setup, - /// Indicate to the `ConstraintSystem` that it populate the variable - /// assignments. If additionally `construct_matrices == true`, then generate - /// the matrices as in the `Setup` case. - Prove { - /// If `construct_matrices == true`, then generate - /// the matrices as in the `Setup` case. - construct_matrices: bool, - }, -} - -/// Defines the parameter to optimize for a `ConstraintSystem`. -#[derive(Copy, Clone, Debug, Eq, PartialEq, Ord, PartialOrd)] -pub enum OptimizationGoal { - /// 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 ConstraintSystem { - #[inline] - fn make_row(&self, l: &LinearCombination) -> Vec<(F, usize)> { - let num_input = self.num_instance_variables; - l.0.iter() - .filter_map(|(coeff, var)| { - if coeff.is_zero() { - None - } else { - Some(( - *coeff, - var.get_index_unchecked(num_input).expect("no symbolic LCs"), - )) - } - }) - .collect() - } - - /// Construct an empty `ConstraintSystem`. - pub fn new() -> Self { - Self { - num_instance_variables: 1, - num_witness_variables: 0, - num_constraints: 0, - num_linear_combinations: 0, - a_constraints: Vec::new(), - b_constraints: Vec::new(), - c_constraints: Vec::new(), - instance_assignment: vec![F::one()], - witness_assignment: Vec::new(), - cache_map: Rc::new(RefCell::new(BTreeMap::new())), - #[cfg(feature = "std")] - constraint_traces: Vec::new(), - - lc_map: BTreeMap::new(), - lc_assignment_cache: Rc::new(RefCell::new(BTreeMap::new())), - - mode: SynthesisMode::Prove { - construct_matrices: true, - }, - - optimization_goal: OptimizationGoal::Constraints, - } - } - - /// Create a new `ConstraintSystemRef`. - pub fn new_ref() -> ConstraintSystemRef { - ConstraintSystemRef::new(Self::new()) - } - - /// Set `self.mode` to `mode`. - pub fn set_mode(&mut self, mode: SynthesisMode) { - self.mode = mode; - } - - /// Check whether `self.mode == SynthesisMode::Setup`. - pub fn is_in_setup_mode(&self) -> bool { - 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) { - // `set_optimization_goal` should only be executed before any constraint or value is created. - assert_eq!(self.num_instance_variables, 1); - assert_eq!(self.num_witness_variables, 0); - assert_eq!(self.num_constraints, 0); - assert_eq!(self.num_linear_combinations, 0); - - self.optimization_goal = goal; - } - - /// Check whether or not `self` will construct matrices. - pub fn should_construct_matrices(&self) -> bool { - match self.mode { - SynthesisMode::Setup => true, - SynthesisMode::Prove { construct_matrices } => construct_matrices, - } - } - - /// Return a variable representing the constant "zero" inside the constraint - /// system. - #[inline] - pub fn zero() -> Variable { - Variable::Zero - } - - /// Return a variable representing the constant "one" inside the constraint - /// system. - #[inline] - pub fn one() -> Variable { - Variable::One - } - - /// Obtain a variable representing a new public instance input. - #[inline] - pub fn new_input_variable(&mut self, f: Func) -> crate::r1cs::Result - where - Func: FnOnce() -> crate::r1cs::Result, - { - let index = self.num_instance_variables; - self.num_instance_variables += 1; - - if !self.is_in_setup_mode() { - self.instance_assignment.push(f()?); - } - Ok(Variable::Instance(index)) - } - - /// Obtain a variable representing a new private witness input. - #[inline] - pub fn new_witness_variable(&mut self, f: Func) -> crate::r1cs::Result - where - Func: FnOnce() -> crate::r1cs::Result, - { - let index = self.num_witness_variables; - self.num_witness_variables += 1; - - if !self.is_in_setup_mode() { - self.witness_assignment.push(f()?); - } - Ok(Variable::Witness(index)) - } - - /// Obtain a variable representing a linear combination. - #[inline] - pub fn new_lc(&mut self, lc: LinearCombination) -> crate::r1cs::Result { - let index = LcIndex(self.num_linear_combinations); - let var = Variable::SymbolicLc(index); - - self.lc_map.insert(index, lc); - - self.num_linear_combinations += 1; - Ok(var) - } - - /// Enforce a R1CS constraint with the name `name`. - #[inline] - pub fn enforce_constraint( - &mut self, - a: LinearCombination, - b: LinearCombination, - c: LinearCombination, - ) -> crate::r1cs::Result<()> { - if self.should_construct_matrices() { - let a_index = self.new_lc(a)?.get_lc_index().unwrap(); - let b_index = self.new_lc(b)?.get_lc_index().unwrap(); - let c_index = self.new_lc(c)?.get_lc_index().unwrap(); - self.a_constraints.push(a_index); - self.b_constraints.push(b_index); - self.c_constraints.push(c_index); - } - self.num_constraints += 1; - #[cfg(feature = "std")] - { - let trace = ConstraintTrace::capture(); - self.constraint_traces.push(trace); - } - Ok(()) - } - - /// 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 { - let mut num_times_used = vec![0; self.lc_map.len()]; - - // Iterate over every lc in constraint system - for (index, lc) in self.lc_map.iter() { - num_times_used[index.0] += count_sinks as usize; - - // Increment the counter for each lc that this lc has a direct dependency on. - for &(_, var) in lc.iter() { - if var.is_lc() { - let lc_index = var.get_lc_index().expect("should be lc"); - num_times_used[lc_index.0] += 1; - } - } - } - num_times_used - } - - /// 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, usize, &mut LinearCombination) - /// - /// 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>) - pub fn transform_lc_map( - &mut self, - transformer: &mut dyn FnMut( - &ConstraintSystem, - usize, - &mut LinearCombination, - ) -> (usize, Option>), - ) { - // `transformed_lc_map` stores the transformed linear combinations. - let mut transformed_lc_map = BTreeMap::<_, LinearCombination>::new(); - let mut num_times_used = self.lc_num_times_used(false); - - // This loop goes through all the LCs in the map, starting from - // the early ones. The transformer function is applied to the - // inlined LC, where new witness variables can be created. - for (&index, lc) in &self.lc_map { - let mut transformed_lc = LinearCombination::new(); - - // Inline the LC, unwrapping symbolic LCs that may constitute it, - // and updating them according to transformations in prior iterations. - for &(coeff, var) in lc.iter() { - if var.is_lc() { - let lc_index = var.get_lc_index().expect("should be lc"); - - // If `var` is a `SymbolicLc`, fetch the corresponding - // inlined LC, and substitute it in. - // - // We have the guarantee that `lc_index` must exist in - // `new_lc_map` since a LC can only depend on other - // LCs with lower indices, which we have transformed. - // - let lc = transformed_lc_map - .get(&lc_index) - .expect("should be inlined"); - transformed_lc.extend((lc * coeff).0.into_iter()); - - // 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. - // - // * 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 { - // This lc is not used any more, so remove it. - transformed_lc_map.remove(&lc_index); - } - } else { - // Otherwise, it's a concrete variable and so we - // substitute it in directly. - transformed_lc.push((coeff, var)); - } - } - transformed_lc.compactify(); - - // Call the transformer function. - let (num_new_witness_variables, new_witness_assignments) = - transformer(&self, num_times_used[index.0], &mut transformed_lc); - - // Insert the transformed LC. - transformed_lc_map.insert(index, transformed_lc); - - // Update the witness counter. - self.num_witness_variables += num_new_witness_variables; - - // Supply additional witness assignments if not in the - // setup mode and if new witness variables are created. - if !self.is_in_setup_mode() && num_new_witness_variables > 0 { - assert!(new_witness_assignments.is_some()); - if let Some(new_witness_assignments) = new_witness_assignments { - assert_eq!(new_witness_assignments.len(), num_new_witness_variables); - self.witness_assignment - .extend_from_slice(&new_witness_assignments); - } - } - } - // Replace the LC map. - self.lc_map = transformed_lc_map; - } - - /// Naively inlines symbolic linear combinations into the linear - /// combinations that use them. - /// - /// Useful for standard pairing-based SNARKs where addition gates are cheap. - /// For example, in the SNARKs such as [\[Groth16\]](https://eprint.iacr.org/2016/260) and - /// [\[Groth-Maller17\]](https://eprint.iacr.org/2017/540), addition gates - /// do not contribute to the size of the multi-scalar multiplication, which - /// is the dominating cost. - pub fn inline_all_lcs(&mut self) { - // Only inline when a matrix representing R1CS is needed. - if !self.should_construct_matrices() { - return; - } - - // A dummy closure is used, which means that - // - it does not modify the inlined LC. - // - it does not add new witness variables. - self.transform_lc_map(&mut |_, _, _| (0, None)); - } - - /// If a `SymbolicLc` is used in more than one location and has sufficient - /// length, this method makes a new variable for that `SymbolicLc`, adds - /// a constraint ensuring the equality of the variable and the linear - /// combination, and then uses that variable in every location the - /// `SymbolicLc` is used. - /// - /// 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. - fn outline_lcs(&mut self) { - // Only inline when a matrix representing R1CS is needed. - if !self.should_construct_matrices() { - return; - } - - // Store information about new witness variables created - // for outlining. New constraints will be added after the - // transformation of the LC map. - let mut new_witness_linear_combinations = Vec::new(); - let mut new_witness_indices = Vec::new(); - - // It goes through all the LCs in the map, starting from - // the early ones, and decides whether or not to dedicate a witness - // variable for this LC. - // - // 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. - // - self.transform_lc_map(&mut |cs, num_times_used, inlined_lc| { - let mut should_dedicate_a_witness_variable = false; - let mut new_witness_index = None; - let mut new_witness_assignment = Vec::new(); - - // Check if it is worthwhile to dedicate a witness variable. - let this_used_times = num_times_used + 1; - let this_len = inlined_lc.len(); - - // Cost with no outlining = `lc_len * number of usages` - // Cost with outlining is one constraint for `(lc_len) * 1 = {new variable}` and - // using that single new variable in each of the prior usages. - // This has total cost `number_of_usages + lc_len + 2` - if this_used_times * this_len > this_used_times + 2 + this_len { - should_dedicate_a_witness_variable = true; - } - - // If it is worthwhile to dedicate a witness variable, - if should_dedicate_a_witness_variable { - // Add a new witness (the value of the linear combination). - // This part follows the same logic of `new_witness_variable`. - let witness_index = cs.num_witness_variables; - new_witness_index = Some(witness_index); - - // Compute the witness assignment. - if !cs.is_in_setup_mode() { - let mut acc = F::zero(); - for (coeff, var) in inlined_lc.iter() { - acc += *coeff * &cs.assigned_value(*var).unwrap(); - } - new_witness_assignment.push(acc); - } - - // Add a new constraint for this new witness. - new_witness_linear_combinations.push(inlined_lc.clone()); - new_witness_indices.push(witness_index); - - // Replace the linear combination with (1 * this new witness). - *inlined_lc = LinearCombination::from(Variable::Witness(witness_index)); - } - // Otherwise, the LC remains unchanged. - - // Return information about new witness variables. - if new_witness_index.is_some() { - (1, Some(new_witness_assignment)) - } else { - (0, None) - } - }); - - // Add the constraints for the newly added witness variables. - for (new_witness_linear_combination, new_witness_variable) in - new_witness_linear_combinations - .iter() - .zip(new_witness_indices.iter()) - { - // Add a new constraint - self.enforce_constraint( - new_witness_linear_combination.clone(), - LinearCombination::from(Self::one()), - LinearCombination::from(Variable::Witness(*new_witness_variable)), - ) - .unwrap(); - } - } - - /// 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 => self.inline_all_lcs(), - 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. - pub fn to_matrices(&self) -> Option> { - if let SynthesisMode::Prove { - construct_matrices: false, - } = self.mode - { - None - } else { - let a: Vec<_> = self - .a_constraints - .iter() - .map(|index| self.make_row(self.lc_map.get(index).unwrap())) - .collect(); - let b: Vec<_> = self - .b_constraints - .iter() - .map(|index| self.make_row(self.lc_map.get(index).unwrap())) - .collect(); - let c: Vec<_> = self - .c_constraints - .iter() - .map(|index| self.make_row(self.lc_map.get(index).unwrap())) - .collect(); - - let a_num_non_zero: usize = a.iter().map(|lc| lc.len()).sum(); - let b_num_non_zero: usize = b.iter().map(|lc| lc.len()).sum(); - let c_num_non_zero: usize = c.iter().map(|lc| lc.len()).sum(); - let matrices = ConstraintMatrices { - num_instance_variables: self.num_instance_variables, - num_witness_variables: self.num_witness_variables, - num_constraints: self.num_constraints, - - a_num_non_zero, - b_num_non_zero, - c_num_non_zero, - - a, - b, - c, - }; - Some(matrices) - } - } - - fn eval_lc(&self, lc: LcIndex) -> Option { - let lc = self.lc_map.get(&lc)?; - let mut acc = F::zero(); - for (coeff, var) in lc.iter() { - acc += *coeff * self.assigned_value(*var)?; - } - Some(acc) - } - - /// If `self` is satisfied, outputs `Ok(true)`. - /// If `self` is unsatisfied, outputs `Ok(false)`. - /// If `self.is_in_setup_mode()`, outputs `Err(())`. - pub fn is_satisfied(&self) -> crate::r1cs::Result { - self.which_is_unsatisfied().map(|s| s.is_none()) - } - - /// If `self` is satisfied, outputs `Ok(None)`. - /// If `self` is unsatisfied, outputs `Some(i)`, where `i` is the index of - /// the first unsatisfied constraint. If `self.is_in_setup_mode()`, outputs - /// `Err(())`. - pub fn which_is_unsatisfied(&self) -> crate::r1cs::Result> { - if self.is_in_setup_mode() { - Err(SynthesisError::AssignmentMissing) - } else { - for i in 0..self.num_constraints { - let a = self - .eval_lc(self.a_constraints[i]) - .ok_or(SynthesisError::AssignmentMissing)?; - let b = self - .eval_lc(self.b_constraints[i]) - .ok_or(SynthesisError::AssignmentMissing)?; - let c = self - .eval_lc(self.c_constraints[i]) - .ok_or(SynthesisError::AssignmentMissing)?; - if a * b != c { - let trace; - #[cfg(feature = "std")] - { - trace = self.constraint_traces[i].as_ref().map_or_else( - || { - eprintln!("Constraint trace requires enabling `ConstraintLayer`"); - format!("{}", i) - }, - |t| format!("{}", t), - ); - } - #[cfg(not(feature = "std"))] - { - trace = format!("{}", i); - } - return Ok(Some(trace)); - } - } - Ok(None) - } - } - - /// Obtain the assignment corresponding to the `Variable` `v`. - pub fn assigned_value(&self, v: Variable) -> Option { - match v { - Variable::One => Some(F::one()), - Variable::Zero => Some(F::zero()), - Variable::Witness(idx) => self.witness_assignment.get(idx).copied(), - Variable::Instance(idx) => self.instance_assignment.get(idx).copied(), - Variable::SymbolicLc(idx) => { - let value = self.lc_assignment_cache.borrow().get(&idx).copied(); - if value.is_some() { - value - } else { - let value = self.eval_lc(idx)?; - self.lc_assignment_cache.borrow_mut().insert(idx, value); - Some(value) - } - }, - } - } -} -/// The A, B and C matrices of a Rank-One `ConstraintSystem`. -/// Also contains metadata on the structure of the constraint system -/// and the matrices. -#[derive(Debug, Clone, PartialEq, Eq)] -pub struct ConstraintMatrices { - /// The number of variables that are "public instances" to the constraint - /// system. - pub num_instance_variables: usize, - /// The number of variables that are "private witnesses" to the constraint - /// system. - pub num_witness_variables: usize, - /// The number of constraints in the constraint system. - pub num_constraints: usize, - /// The number of non_zero entries in the A matrix. - pub a_num_non_zero: usize, - /// The number of non_zero entries in the B matrix. - pub b_num_non_zero: usize, - /// The number of non_zero entries in the C matrix. - pub c_num_non_zero: usize, - - /// The A constraint matrix. This is empty when - /// `self.mode == SynthesisMode::Prove { construct_matrices = false }`. - pub a: Matrix, - /// The B constraint matrix. This is empty when - /// `self.mode == SynthesisMode::Prove { construct_matrices = false }`. - pub b: Matrix, - /// The C constraint matrix. This is empty when - /// `self.mode == SynthesisMode::Prove { construct_matrices = false }`. - pub c: Matrix, -} - -/// A shared reference to a constraint system that can be stored in high level -/// variables. -#[derive(Debug, Clone)] -pub enum ConstraintSystemRef { - /// Represents the case where we *don't* need to allocate variables or - /// enforce constraints. Encountered when operating over constant - /// values. - None, - /// Represents the case where we *do* allocate variables or enforce - /// constraints. - CS(Rc>>), -} - -impl PartialEq for ConstraintSystemRef { - fn eq(&self, other: &Self) -> bool { - match (self, other) { - (Self::None, Self::None) => true, - (..) => false, - } - } -} - -impl Eq for ConstraintSystemRef {} - -/// A namespaced `ConstraintSystemRef`. -#[derive(Debug, Clone)] -pub struct Namespace { - inner: ConstraintSystemRef, - id: Option, -} - -impl From> for Namespace { - fn from(other: ConstraintSystemRef) -> Self { - Self { - inner: other, - id: None, - } - } -} - -impl Namespace { - /// Construct a new `Namespace`. - pub fn new(inner: ConstraintSystemRef, id: Option) -> Self { - Self { inner, id } - } - - /// Obtain the inner `ConstraintSystemRef`. - pub fn cs(&self) -> ConstraintSystemRef { - self.inner.clone() - } - - /// Manually leave the namespace. - pub fn leave_namespace(self) { - drop(self) - } -} - -impl Drop for Namespace { - fn drop(&mut self) { - if let Some(id) = self.id.as_ref() { - tracing::dispatcher::get_default(|dispatch| dispatch.exit(id)) - } - let _ = self.inner; - } -} - -impl ConstraintSystemRef { - /// Returns `self` if `!self.is_none()`, otherwise returns `other`. - pub fn or(self, other: Self) -> Self { - match self { - ConstraintSystemRef::None => other, - _ => self, - } - } - - /// Returns `true` is `self == ConstraintSystemRef::None`. - pub fn is_none(&self) -> bool { - matches!(self, ConstraintSystemRef::None) - } - - /// Construct a `ConstraintSystemRef` from a `ConstraintSystem`. - #[inline] - pub fn new(inner: ConstraintSystem) -> Self { - Self::CS(Rc::new(RefCell::new(inner))) - } - - fn inner(&self) -> Option<&Rc>>> { - match self { - Self::CS(a) => Some(a), - Self::None => None, - } - } - - /// Consumes self to return the inner `ConstraintSystem`. Returns - /// `None` if `Self::CS` is `None` or if any other references to - /// `Self::CS` exist. - pub fn into_inner(self) -> Option> { - match self { - Self::CS(a) => Rc::try_unwrap(a).ok().map(|s| s.into_inner()), - Self::None => None, - } - } - - /// Obtain an immutable reference to the underlying `ConstraintSystem`. - /// - /// # Panics - /// This method panics if `self` is already mutably borrowed. - #[inline] - pub fn borrow(&self) -> Option>> { - self.inner().map(|cs| cs.borrow()) - } - - /// Obtain a mutable reference to the underlying `ConstraintSystem`. - /// - /// # Panics - /// This method panics if `self` is already mutably borrowed. - #[inline] - pub fn borrow_mut(&self) -> Option>> { - self.inner().map(|cs| cs.borrow_mut()) - } - - /// Set `self.mode` to `mode`. - pub fn set_mode(&self, mode: SynthesisMode) { - self.inner().map_or((), |cs| cs.borrow_mut().set_mode(mode)) - } - - /// Check whether `self.mode == SynthesisMode::Setup`. - #[inline] - pub fn is_in_setup_mode(&self) -> bool { - self.inner() - .map_or(false, |cs| cs.borrow().is_in_setup_mode()) - } - - /// Returns the number of constraints. - #[inline] - pub fn num_constraints(&self) -> usize { - self.inner().map_or(0, |cs| cs.borrow().num_constraints) - } - - /// Returns the number of instance variables. - #[inline] - pub fn num_instance_variables(&self) -> usize { - self.inner() - .map_or(0, |cs| cs.borrow().num_instance_variables) - } - - /// Returns the number of witness variables. - #[inline] - pub fn num_witness_variables(&self) -> usize { - self.inner() - .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 { - self.inner() - .map_or(false, |cs| cs.borrow().should_construct_matrices()) - } - - /// Obtain a variable representing a new public instance input. - #[inline] - pub fn new_input_variable(&self, f: Func) -> crate::r1cs::Result - where - Func: FnOnce() -> crate::r1cs::Result, - { - self.inner() - .ok_or(SynthesisError::MissingCS) - .and_then(|cs| { - if !self.is_in_setup_mode() { - // This is needed to avoid double-borrows, because `f` - // might itself mutably borrow `cs` (eg: `f = || g.value()`). - let value = f(); - cs.borrow_mut().new_input_variable(|| value) - } else { - cs.borrow_mut().new_input_variable(f) - } - }) - } - - /// Obtain a variable representing a new private witness input. - #[inline] - pub fn new_witness_variable(&self, f: Func) -> crate::r1cs::Result - where - Func: FnOnce() -> crate::r1cs::Result, - { - self.inner() - .ok_or(SynthesisError::MissingCS) - .and_then(|cs| { - if !self.is_in_setup_mode() { - // This is needed to avoid double-borrows, because `f` - // might itself mutably borrow `cs` (eg: `f = || g.value()`). - let value = f(); - cs.borrow_mut().new_witness_variable(|| value) - } else { - cs.borrow_mut().new_witness_variable(f) - } - }) - } - - /// Obtain a variable representing a linear combination. - #[inline] - pub fn new_lc(&self, lc: LinearCombination) -> crate::r1cs::Result { - self.inner() - .ok_or(SynthesisError::MissingCS) - .and_then(|cs| cs.borrow_mut().new_lc(lc)) - } - - /// Enforce a R1CS constraint with the name `name`. - #[inline] - pub fn enforce_constraint( - &self, - a: LinearCombination, - b: LinearCombination, - c: LinearCombination, - ) -> crate::r1cs::Result<()> { - self.inner() - .ok_or(SynthesisError::MissingCS) - .and_then(|cs| cs.borrow_mut().enforce_constraint(a, b, c)) - } - - /// Naively inlines symbolic linear combinations into the linear - /// combinations that use them. - /// - /// Useful for standard pairing-based SNARKs where addition gates are cheap. - /// For example, in the SNARKs such as [\[Groth16\]](https://eprint.iacr.org/2016/260) and - /// [\[Groth-Maller17\]](https://eprint.iacr.org/2017/540), addition gates - /// do not contribute to the size of the multi-scalar multiplication, which - /// is the dominating cost. - pub fn inline_all_lcs(&self) { - if let Some(cs) = self.inner() { - cs.borrow_mut().inline_all_lcs() - } - } - - /// 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().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. - #[inline] - pub fn to_matrices(&self) -> Option> { - self.inner().and_then(|cs| cs.borrow().to_matrices()) - } - - /// If `self` is satisfied, outputs `Ok(true)`. - /// If `self` is unsatisfied, outputs `Ok(false)`. - /// If `self.is_in_setup_mode()` or if `self == None`, outputs `Err(())`. - pub fn is_satisfied(&self) -> crate::r1cs::Result { - self.inner() - .map_or(Err(SynthesisError::AssignmentMissing), |cs| { - cs.borrow().is_satisfied() - }) - } - - /// If `self` is satisfied, outputs `Ok(None)`. - /// If `self` is unsatisfied, outputs `Some(i)`, where `i` is the index of - /// the first unsatisfied constraint. - /// If `self.is_in_setup_mode()` or `self == None`, outputs `Err(())`. - pub fn which_is_unsatisfied(&self) -> crate::r1cs::Result> { - self.inner() - .map_or(Err(SynthesisError::AssignmentMissing), |cs| { - cs.borrow().which_is_unsatisfied() - }) - } - - /// Obtain the assignment corresponding to the `Variable` `v`. - pub fn assigned_value(&self, v: Variable) -> Option { - self.inner().and_then(|cs| cs.borrow().assigned_value(v)) - } - - /// Get trace information about all constraints in the system - pub fn constraint_names(&self) -> Option> { - #[cfg(feature = "std")] - { - self.inner().and_then(|cs| { - cs.borrow() - .constraint_traces - .iter() - .map(|trace| { - let mut constraint_path = String::new(); - let mut prev_module_path = ""; - let mut prefixes = ark_std::collections::BTreeSet::new(); - for step in trace.as_ref()?.path() { - let module_path = if prev_module_path == step.module_path { - prefixes.insert(step.module_path.to_string()); - String::new() - } else { - let mut parts = step - .module_path - .split("::") - .filter(|&part| part != "r1cs_std" && part != "constraints"); - let mut path_so_far = String::new(); - for part in parts.by_ref() { - if path_so_far.is_empty() { - path_so_far += part; - } else { - path_so_far += &["::", part].join(""); - } - if prefixes.contains(&path_so_far) { - continue; - } else { - prefixes.insert(path_so_far.clone()); - break; - } - } - parts.collect::>().join("::") + "::" - }; - prev_module_path = step.module_path; - constraint_path += &["/", &module_path, step.name].join(""); - } - Some(constraint_path) - }) - .collect::>>() - }) - } - #[cfg(not(feature = "std"))] - { - None - } - } -} - -#[cfg(test)] -mod tests { - use crate::r1cs::*; - use ark_ff::One; - use ark_test_curves::bls12_381::Fr; - - #[test] - fn matrix_generation() -> crate::r1cs::Result<()> { - let cs = ConstraintSystem::::new_ref(); - let two = Fr::one() + Fr::one(); - let a = cs.new_input_variable(|| Ok(Fr::one()))?; - let b = cs.new_witness_variable(|| Ok(Fr::one()))?; - let c = cs.new_witness_variable(|| Ok(two))?; - cs.enforce_constraint(lc!() + a, lc!() + (two, b), lc!() + c)?; - let d = cs.new_lc(lc!() + a + b)?; - cs.enforce_constraint(lc!() + a, lc!() + d, lc!() + d)?; - let e = cs.new_lc(lc!() + d + d)?; - cs.enforce_constraint(lc!() + Variable::One, lc!() + e, lc!() + e)?; - cs.inline_all_lcs(); - let matrices = cs.to_matrices().unwrap(); - assert_eq!(matrices.a[0], vec![(Fr::one(), 1)]); - assert_eq!(matrices.b[0], vec![(two, 2)]); - assert_eq!(matrices.c[0], vec![(Fr::one(), 3)]); - - assert_eq!(matrices.a[1], vec![(Fr::one(), 1)]); - assert_eq!(matrices.b[1], vec![(Fr::one(), 1), (Fr::one(), 2)]); - assert_eq!(matrices.c[1], vec![(Fr::one(), 1), (Fr::one(), 2)]); - - assert_eq!(matrices.a[2], vec![(Fr::one(), 0)]); - assert_eq!(matrices.b[2], vec![(two, 1), (two, 2)]); - assert_eq!(matrices.c[2], vec![(two, 1), (two, 2)]); - Ok(()) - } - - #[test] - fn matrix_generation_outlined() -> crate::r1cs::Result<()> { - let cs = ConstraintSystem::::new_ref(); - cs.set_optimization_goal(OptimizationGoal::Weight); - let two = Fr::one() + Fr::one(); - let a = cs.new_input_variable(|| Ok(Fr::one()))?; - let b = cs.new_witness_variable(|| Ok(Fr::one()))?; - let c = cs.new_witness_variable(|| Ok(two))?; - cs.enforce_constraint(lc!() + a, lc!() + (two, b), lc!() + c)?; - - let d = cs.new_lc(lc!() + a + b)?; - cs.enforce_constraint(lc!() + a, lc!() + d, lc!() + d)?; - - let e = cs.new_lc(lc!() + d + d)?; - cs.enforce_constraint(lc!() + Variable::One, lc!() + e, lc!() + e)?; - - cs.finalize(); - assert!(cs.is_satisfied().unwrap()); - let matrices = cs.to_matrices().unwrap(); - assert_eq!(matrices.a[0], vec![(Fr::one(), 1)]); - assert_eq!(matrices.b[0], vec![(two, 2)]); - assert_eq!(matrices.c[0], vec![(Fr::one(), 3)]); - - assert_eq!(matrices.a[1], vec![(Fr::one(), 1)]); - // Notice here how the variable allocated for d is outlined - // compared to the example in previous test case. - // We are optimising for weight: there are less non-zero elements. - assert_eq!(matrices.b[1], vec![(Fr::one(), 4)]); - assert_eq!(matrices.c[1], vec![(Fr::one(), 4)]); - - assert_eq!(matrices.a[2], vec![(Fr::one(), 0)]); - assert_eq!(matrices.b[2], vec![(two, 4)]); - assert_eq!(matrices.c[2], vec![(two, 4)]); - Ok(()) - } - - /// Example meant to follow as closely as possible the excellent R1CS - /// write-up by [Vitalik Buterin](https://vitalik.eth.limo/general/2016/12/10/qap.html) - /// and demonstrate how to construct such matrices in arkworks. - #[test] - fn matrix_generation_example() -> crate::r1cs::Result<()> { - let cs = ConstraintSystem::::new_ref(); - // helper definitions - let three = Fr::from(3u8); - let five = Fr::from(5u8); - let nine = Fr::from(9u8); - // There will be six variables in the system, in the order governed by adding - // them to the constraint system (Note that the CS is initialised with - // `Variable::One` in the first position implicitly). - // Note also that the all public variables will always be placed before all witnesses - // - // Variable::One - // Variable::Instance(35) - // Variable::Witness(3) ( == x ) - // Variable::Witness(9) ( == sym_1 ) - // Variable::Witness(27) ( == y ) - // Variable::Witness(30) ( == sym_2 ) - - // let one = Variable::One; // public input, implicitly defined - let out = cs.new_input_variable(|| Ok(nine * three + three + five))?; // public input - let x = cs.new_witness_variable(|| Ok(three))?; // explicit witness - let sym_1 = cs.new_witness_variable(|| Ok(nine))?; // intermediate witness variable - let y = cs.new_witness_variable(|| Ok(nine * three))?; // intermediate witness variable - let sym_2 = cs.new_witness_variable(|| Ok(nine * three + three))?; // intermediate witness variable - - cs.enforce_constraint(lc!() + x, lc!() + x, lc!() + sym_1)?; - cs.enforce_constraint(lc!() + sym_1, lc!() + x, lc!() + y)?; - cs.enforce_constraint(lc!() + y + x, lc!() + Variable::One, lc!() + sym_2)?; - cs.enforce_constraint( - lc!() + sym_2 + (five, Variable::One), - lc!() + Variable::One, - lc!() + out, - )?; - - cs.finalize(); - assert!(cs.is_satisfied().unwrap()); - let matrices = cs.to_matrices().unwrap(); - // There are four gates(constraints), each generating a row. - // Resulting matrices: - // (Note how 2nd & 3rd columns are swapped compared to the online example. - // This results from an implementation detail of placing all Variable::Instances(_) first. - // - // A - // [0, 0, 1, 0, 0, 0] - // [0, 0, 0, 1, 0, 0] - // [0, 0, 1, 0, 1, 0] - // [5, 0, 0, 0, 0, 1] - // B - // [0, 0, 1, 0, 0, 0] - // [0, 0, 1, 0, 0, 0] - // [1, 0, 0, 0, 0, 0] - // [1, 0, 0, 0, 0, 0] - // C - // [0, 0, 0, 1, 0, 0] - // [0, 0, 0, 0, 1, 0] - // [0, 0, 0, 0, 0, 1] - // [0, 1, 0, 0, 0, 0] - assert_eq!(matrices.a[0], vec![(Fr::one(), 2)]); - assert_eq!(matrices.b[0], vec![(Fr::one(), 2)]); - assert_eq!(matrices.c[0], vec![(Fr::one(), 3)]); - - assert_eq!(matrices.a[1], vec![(Fr::one(), 3)]); - assert_eq!(matrices.b[1], vec![(Fr::one(), 2)]); - assert_eq!(matrices.c[1], vec![(Fr::one(), 4)]); - - assert_eq!(matrices.a[2], vec![(Fr::one(), 2), (Fr::one(), 4)]); - assert_eq!(matrices.b[2], vec![(Fr::one(), 0)]); - assert_eq!(matrices.c[2], vec![(Fr::one(), 5)]); - - assert_eq!(matrices.a[3], vec![(five, 0), (Fr::one(), 5)]); - assert_eq!(matrices.b[3], vec![(Fr::one(), 0)]); - assert_eq!(matrices.c[3], vec![(Fr::one(), 1)]); - Ok(()) - } -} diff --git a/relations/src/r1cs/error.rs b/relations/src/utils/error.rs similarity index 72% rename from relations/src/r1cs/error.rs rename to relations/src/utils/error.rs index 3a4136966..2906d9e25 100644 --- a/relations/src/r1cs/error.rs +++ b/relations/src/utils/error.rs @@ -21,6 +21,11 @@ pub enum SynthesisError { MalformedVerifyingKey, /// During CRS generation, we observed an unconstrained auxiliary variable UnconstrainedVariable, + + PredicateNotFound, + ArityMismatch, + LcNotFound, + UnexpectedVariable } impl ark_std::error::Error for SynthesisError {} @@ -42,6 +47,24 @@ impl fmt::Display for SynthesisError { SynthesisError::UnconstrainedVariable => { write!(f, "auxiliary variable was unconstrained") }, + SynthesisError::ArityMismatch => { + write!(f, "The Arity for the predicate does not match the input") + }, + SynthesisError::PredicateNotFound => { + write!(f, "The predicate was not found in the constraint system") + }, + SynthesisError::LcNotFound => { + write!( + f, + "The LcIndex provided does not correspond to any Linear Combination" + ) + }, + SynthesisError::UnexpectedVariable => { + write!( + f, + "Variable type is not expected for the operation" + ) + }, } } } diff --git a/relations/src/r1cs/impl_lc.rs b/relations/src/utils/linear_combination.rs similarity index 96% rename from relations/src/r1cs/impl_lc.rs rename to relations/src/utils/linear_combination.rs index c56abce5e..438e04019 100644 --- a/relations/src/r1cs/impl_lc.rs +++ b/relations/src/utils/linear_combination.rs @@ -1,6 +1,5 @@ #![allow(clippy::suspicious_arithmetic_impl)] -use crate::r1cs::{LinearCombination, Variable}; use ark_ff::Field; use ark_std::{ ops::{Add, AddAssign, Deref, DerefMut, Mul, MulAssign, Neg, Sub}, @@ -8,12 +7,22 @@ use ark_std::{ vec::Vec, }; +use super::variable::Variable; + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Debug)] +/// An opaque counter for symbolic linear combinations. +pub struct LcIndex(pub usize); + +/// A linear combination of variables according to associated coefficients. +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct LinearCombination(pub Vec<(F, Variable)>); + /// Generate a `LinearCombination` from arithmetic expressions involving /// `Variable`s. #[macro_export] macro_rules! lc { () => { - $crate::r1cs::LinearCombination::zero() + $crate::gr1cs::LinearCombination::zero() }; } diff --git a/relations/src/utils/matrix.rs b/relations/src/utils/matrix.rs new file mode 100644 index 000000000..690f7cbe0 --- /dev/null +++ b/relations/src/utils/matrix.rs @@ -0,0 +1,30 @@ +use ark_ff::Field; +use ark_std::vec::Vec; +/// A sparse representation of constraint matrices. +pub type Matrix = Vec>; + +/// Transpose a matrix of field elements. +pub fn transpose(matrix: &Matrix) -> Matrix { + // First, find the maximum column index to know the size of the transposed + // matrix + let max_cols = matrix + .iter() + .flat_map(|row| row.iter().map(|&(_, col)| col + 1)) + .max() + .unwrap_or(0); + + // Initialize the transposed matrix with empty vectors + let mut transposed: Matrix = vec![Vec::new(); max_cols]; + + // Iterate through each row and each element in the row + for (row_index, row) in matrix.iter().enumerate() { + for &(value, col_index) in row { + // Add the element to the new row (which is originally a column) in the + // transposed matrix + transposed[col_index].push((value, row_index)); + } + } + + // Return the transposed matrix + transposed +} diff --git a/relations/src/utils/mod.rs b/relations/src/utils/mod.rs new file mode 100644 index 000000000..d7e924d9c --- /dev/null +++ b/relations/src/utils/mod.rs @@ -0,0 +1,11 @@ +use ark_std::vec::Vec; +use error::SynthesisError; +use linear_combination::LcIndex; + +pub mod error; +pub mod linear_combination; +pub mod matrix; +pub mod variable; + +/// A result type specialized to `SynthesisError`. +pub type Result = core::result::Result; diff --git a/relations/src/r1cs/mod.rs b/relations/src/utils/variable.rs similarity index 64% rename from relations/src/r1cs/mod.rs rename to relations/src/utils/variable.rs index 69adfa3f5..39309421b 100644 --- a/relations/src/r1cs/mod.rs +++ b/relations/src/utils/variable.rs @@ -1,37 +1,6 @@ -//! Core interface for working with Rank-1 Constraint Systems (R1CS). - -use ark_std::vec::Vec; - -/// A result type specialized to `SynthesisError`. -pub type Result = core::result::Result; - -#[macro_use] -mod impl_lc; -mod constraint_system; -mod error; -#[cfg(feature = "std")] -mod trace; - -#[cfg(feature = "std")] -pub use crate::r1cs::trace::{ConstraintLayer, ConstraintTrace, TraceStep, TracingMode}; - -pub use tracing::info_span; - -pub use ark_ff::{Field, ToConstraintField}; -pub use constraint_system::{ - ConstraintMatrices, ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, - OptimizationGoal, SynthesisMode, -}; -pub use error::SynthesisError; - use core::cmp::Ordering; -/// A sparse representation of constraint matrices. -pub type Matrix = Vec>; - -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Debug)] -/// An opaque counter for symbolic linear combinations. -pub struct LcIndex(usize); +use super::linear_combination::LcIndex; /// Represents the different kinds of variables present in a constraint system. #[derive(Copy, Clone, PartialEq, Debug, Eq)] @@ -48,25 +17,16 @@ pub enum Variable { SymbolicLc(LcIndex), } -/// A linear combination of variables according to associated coefficients. -#[derive(Debug, Clone, PartialEq, Eq, Default)] -pub struct LinearCombination(pub Vec<(F, Variable)>); +impl Variable { + pub fn zero() -> Variable { + Variable::Zero + } -/// Generate a `Namespace` with name `name` from `ConstraintSystem` `cs`. -/// `name` must be a `&'static str`. -#[macro_export] -macro_rules! ns { - ($cs:expr, $name:expr) => {{ - let span = $crate::r1cs::info_span!(target: "r1cs", $name); - let id = span.id(); - let _enter_guard = span.enter(); - core::mem::forget(_enter_guard); - core::mem::forget(span); - $crate::r1cs::Namespace::new($cs.clone(), id) - }}; -} + #[inline] + pub fn one() -> Variable { + Variable::One + } -impl Variable { /// Is `self` the zero variable? #[inline] pub fn is_zero(&self) -> bool { diff --git a/rustfmt.toml b/rustfmt.toml index 71712138c..1a5934611 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -6,4 +6,4 @@ match_block_trailing_comma = true use_field_init_shorthand = true edition = "2018" condense_wildcard_suffixes = true -merge_imports = true +imports_granularity="Crate" \ No newline at end of file diff --git a/snark/src/lib.rs b/snark/src/lib.rs index 6003837ed..757fe1680 100644 --- a/snark/src/lib.rs +++ b/snark/src/lib.rs @@ -11,10 +11,12 @@ #![forbid(unsafe_code)] use ark_ff::PrimeField; -use ark_relations::r1cs::ConstraintSynthesizer; +use ark_relations::gr1cs::ConstraintSynthesizer; use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; -use ark_std::fmt::Debug; -use ark_std::rand::{CryptoRng, RngCore}; +use ark_std::{ + fmt::Debug, + rand::{CryptoRng, RngCore}, +}; /// The basic functionality for a SNARK. pub trait SNARK { @@ -52,8 +54,8 @@ pub trait SNARK { ) -> Result; /// Checks that `proof` is a valid proof of the satisfaction of circuit - /// encoded in `circuit_vk`, with respect to the public input `public_input`, - /// specified as R1CS constraints. + /// encoded in `circuit_vk`, with respect to the public input + /// `public_input`, specified as R1CS constraints. fn verify( circuit_vk: &Self::VerifyingKey, public_input: &[F], @@ -69,8 +71,8 @@ pub trait SNARK { ) -> Result; /// Checks that `proof` is a valid proof of the satisfaction of circuit - /// encoded in `circuit_pvk`, with respect to the public input `public_input`, - /// specified as R1CS constraints. + /// encoded in `circuit_pvk`, with respect to the public input + /// `public_input`, specified as R1CS constraints. fn verify_with_processed_vk( circuit_pvk: &Self::ProcessedVerifyingKey, public_input: &[F],