Patch outline, revert which_is_unsatisfied and more (#392)

* r1cs replaced with gr1cs

* addressed the PR comments

* instance assignment getter created

* instance assignment fixed outer

* nax_arity added

* predicate num constraints added

* bump version to 0.5.0 and update dependencies

* refactor: changed the constraint storage method in the predicates

* Fix: predicate weakly references to a constraint system

* polish

* feat: expose R1CS_PREDICATE_LABEL from gr1cs module

* refactor: move make_row method to ConstraintSystem and ConstraintSystemRef for matrix row creation

* refactor: update make_row method to improve error handling and clarity

* refactor: Replaced the weak reference with downstreaming constraint system reference

* tracing checked

* work

* works

* ready to review

* finalized

* Update

* Fix

* Fix

* Remove patches

* Bug Fix: Outline instances handling 'One'

* bug fix: Handling one in instance outline

* outline instance optimized

* path instance_outline

* Bug Fix: Outline instances handling 'One'

* bug fix: Handling one in instance outline

* outline instance optimized

* path instance_outline

* Fmt

* Fix

* Fix

* work

* fix

* which_is_unsatisfied reverted

* fmt

* Work

* Fix CI

* fmt

* Clean up

* Improve

* Tweak

---------

Co-authored-by: Pratyush Mishra <[email protected]>

Author: alireza-shirzad

.github/workflows/ci.yml

@@ -50,7 +50,7 @@ jobs:
           toolchain: ${{ matrix.rust }}
           override: true
 
-      - uses: actions/cache@v2
+      - uses: actions/cache@v4
         with:
           path: |
             ~/.cargo/registry
@@ -92,7 +92,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v2
 
-      - name: Install Rust (${{ matrix.rust }})
+      - name: Install Rust
         uses: actions-rs/toolchain@v1
         with:
           toolchain: stable

Cargo.toml

@@ -22,6 +22,7 @@ ark-serialize = { version = "0.5.0", default-features = false }
 tracing = { version = "0.1", default-features = false }
 tracing-subscriber = { version = "0.3", default-features = false }
 ark-test-curves = { version = "0.5.0", default-features = false }
+rayon = { version = "1" }
 
 [profile.release]
 opt-level = 3

relations/Cargo.toml

@@ -19,13 +19,15 @@ ark-poly.workspace = true
 ark-serialize.workspace = true
 tracing = { workspace = true, features = ["attributes"] }
 tracing-subscriber = { workspace = true, default-features = true, optional = true }
+rayon = { workspace = true, optional = true }
 
 [dev-dependencies]
 ark-test-curves = { workspace = true, default-features = false, features = [ "bls12_381_scalar_field" ] }
 
 [features]
 default = []
 std = [ "ark-std/std", "ark-ff/std", "tracing-subscriber", "tracing/std" ]
+parallel = [ "std", "ark-std/parallel", "ark-ff/parallel", "rayon" ]
 
 
 [[example]]

relations/src/gr1cs/constraint_system.rs

@@ -1,8 +1,9 @@
 //! This module contains the implementation of the `ConstraintSystem` struct.
 //! a constraint system contains multiple predicate constraint systems,
-//! each of which enforce have seperate predicates and constraints. For more infomation about the terminology and the structure of the constraint system, refer to section 3.3 of https://eprint.iacr.org/2024/1245
+//! each of which enforce have separate predicates and constraints. For more information about the terminology and the structure of the constraint system, refer to section 3.3 of https://eprint.iacr.org/2024/1245
 
 use super::{
+    instance_outliner::InstanceOutliner,
     predicate::{
         polynomial_constraint::R1CS_PREDICATE_LABEL, PredicateConstraintSystem, PredicateType,
     },
@@ -22,6 +23,7 @@ use ark_std::{
     string::{String, ToString},
     vec::Vec,
 };
+// TODO: Prayush's PR, Hashbrown, HAshmap for nostd
 ///////////////////////////////////////////////////////////////////////////////////////
 
 /// A GR1CS `ConstraintSystem`. Enforces constraints of the form  
@@ -55,7 +57,7 @@ pub struct ConstraintSystem<F: Field> {
     /// It assigns a witness variable to each instance variable and enforces the
     /// equality of the instance and witness variables. Then only uses the
     /// witness variables in the constraints.
-    outline_instances: bool,
+    instance_outliner: Option<InstanceOutliner<F>>,
 
     /// Assignments to the public input variables. This is empty if `self.mode
     /// == SynthesisMode::Setup`.
@@ -99,7 +101,7 @@ impl<F: Field> ConstraintSystem<F> {
             num_instance_variables: 1,
             num_witness_variables: 0,
             num_linear_combinations: 0,
-            outline_instances: false,
+            instance_outliner: None,
             predicate_constraint_systems: BTreeMap::new(),
             instance_assignment: vec![F::one()],
             witness_assignment: Vec::new(),
@@ -109,7 +111,7 @@ impl<F: Field> ConstraintSystem<F> {
             mode: SynthesisMode::Prove {
                 construct_matrices: true,
             },
-            optimization_goal: OptimizationGoal::Constraints,
+            optimization_goal: OptimizationGoal::None,
             #[cfg(feature = "std")]
             predicate_traces: BTreeMap::new(),
         };
@@ -361,6 +363,11 @@ impl<F: Field> ConstraintSystem<F> {
         Ok(())
     }
 
+    /// Remove the predicate with the given label from the constraint system.
+    pub fn remove_predicate(&mut self, predicate_label: &str) {
+        self.predicate_constraint_systems.remove(predicate_label);
+    }
+
     /// check if there is a predicate with the given label
     pub fn has_predicate(&self, predicate_label: &str) -> bool {
         self.predicate_constraint_systems
@@ -402,15 +409,15 @@ impl<F: Field> ConstraintSystem<F> {
     /// 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<bool> {
-        self.which_predicate_is_unsatisfied().map(|s| s.is_none())
+        self.which_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 prediacate and  `i` is the index of
     /// the first unsatisfied constraint in that predicate.
     /// If `self.is_in_setup_mode()` or `self == None`, outputs `Err(())`.
-    pub fn which_predicate_is_unsatisfied(&self) -> crate::utils::Result<Option<String>> {
+    pub fn which_is_unsatisfied(&self) -> crate::utils::Result<Option<String>> {
         if self.is_in_setup_mode() {
             Err(SynthesisError::AssignmentMissing)
         } else {
@@ -448,24 +455,35 @@ impl<F: Field> ConstraintSystem<F> {
     /// Finalize the constraint system (either by outlining or inlining,
     /// if an optimization goal is set).
     pub fn finalize(&mut self) {
+        let timer_finalize = start_timer!(|| "Finalize GR1CS");
+        let timer_inline_ouline_lcs = start_timer!(|| "Inline/Outline LCs");
         match self.optimization_goal {
-            OptimizationGoal::None => self.inline_all_lcs(),
             OptimizationGoal::Constraints => self.inline_all_lcs(),
             OptimizationGoal::Weight => self.outline_lcs(),
+            _ => self.inline_all_lcs(),
         };
-        if self.outline_instances {
-            let _ = self.do_outline_instances();
+        end_timer!(timer_inline_ouline_lcs);
+        // check if should outline instance or not
+        let timer_instance_outlining = start_timer!(|| "Instance Outlining");
+        if let Some(instance_outliner) = self.instance_outliner.take() {
+            // Check if the predicate to be outlined is in the constraint system
+            if self.has_predicate(&instance_outliner.pred_label) {
+                // Outline the instances
+                let _ = self.perform_instance_outlining(instance_outliner);
+            }
         }
+        end_timer!(timer_instance_outlining);
+        end_timer!(timer_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
+    /// 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.
+    /// 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() {
@@ -478,11 +496,11 @@ impl<F: Field> ConstraintSystem<F> {
         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.
+    /// 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
@@ -583,10 +601,10 @@ impl<F: Field> ConstraintSystem<F> {
     /// This method is used as a subroutine of `inline_all_lcs` and
     /// `outline_lcs`.
     ///
-    /// The transformer function is given a references of this constraint system
-    /// (&self), number of times used, and a mutable reference of the linear
-    /// combination to be transformed.     (&ConstraintSystem<F>, usize,
-    /// &mut LinearCombination<F>)
+    /// The transformer function is given a references of this constraint
+    /// system (&self), number of times used, and a mutable
+    /// reference of the linear combination to be transformed.
+    /// (&ConstraintSystem<F>, usize, &mut LinearCombination<F>)
     ///
     /// The transformer function returns the number of new witness variables
     /// needed and a vector of new witness assignments (if not in the setup
@@ -600,7 +618,8 @@ impl<F: Field> ConstraintSystem<F> {
         ) -> (usize, Option<Vec<F>>),
     ) {
         // `transformed_lc_map` stores the transformed linear combinations.
-        let mut transformed_lc_map = BTreeMap::<_, LinearCombination<F>>::new();
+        let mut transformed_lc_map: BTreeMap<LcIndex, LinearCombination<F>> =
+            BTreeMap::<_, LinearCombination<F>>::new();
         let mut num_times_used = self.lc_num_times_used(false);
 
         // This loop goes through all the LCs in the map, starting from
@@ -707,8 +726,8 @@ impl<F: Field> ConstraintSystem<F> {
     }
 
     /// 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.
+    /// 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<LinearCombination<F>> {
         self.lc_map
             .get(&lc_index)
@@ -735,24 +754,27 @@ impl<F: Field> ConstraintSystem<F> {
     }
 
     /// Sets the flag for outlining the instances
-    pub(crate) fn outline_instances(&mut self) {
-        self.outline_instances = true;
+    pub(crate) fn set_instance_outliner(&mut self, instance_outliner: InstanceOutliner<F>) {
+        self.instance_outliner = Some(instance_outliner);
     }
 
-    /// Returns the flag for outlining the instances, This is by default set to
-    /// false
+    /// Returns the flag for outlining the instances, This is by default set
+    /// to false
     pub(crate) fn should_outline_instances(&self) -> bool {
-        self.outline_instances
+        self.instance_outliner.is_some()
     }
 
     /// Outlines the instances in the constraint system
-    /// This function creates a new witness variable for each instance variable
-    /// and uses these witness variables in the constraints instead of instance
-    /// variables. This technique is useful for verifier succinctness in some
-    /// SNARKs like Garuda, Pari and PolyMath
-    /// After the function call, The instances are only used in the `c` matrix
-    /// of r1cs
-    pub(crate) fn do_outline_instances(&mut self) -> crate::gr1cs::Result<()> {
+    /// This function creates a new witness variable for each instance
+    /// variable and uses these witness variables in the constraints
+    /// instead of instance variables. This technique is useful for
+    /// verifier succinctness in some SNARKs like Garuda, Pari and
+    /// PolyMath After the function call, The instances are only
+    /// used in the `c` matrix of r1cs
+    pub fn perform_instance_outlining(
+        &mut self,
+        outliner: InstanceOutliner<F>,
+    ) -> crate::gr1cs::Result<()> {
         // First build a map from instance variables to witness variables
         let mut instance_to_witness_map = BTreeMap::<Variable, Variable>::new();
         // Initialize the map with the one variable, this is done manually because we
@@ -797,30 +819,7 @@ impl<F: Field> ConstraintSystem<F> {
                 self.witness_assignment[witness_index] = instance_value;
             }
         }
-
-        // Now, enforce the equality between the instance and the corresponding witness
-        // variable This is done by iterating over the instance-witness map
-        // which contains the unique instance-witness pairs The equality
-        // constraints are enforced with r1cs constraints, it is assumed that a
-        // constraint system has a default r1cs predicate registered
-        for (instance, witness) in instance_to_witness_map.iter() {
-            let r1cs_constraint = if instance.is_one() {
-                vec![
-                    LinearCombination::from(*witness),
-                    LinearCombination::from(*witness),
-                    LinearCombination::from(*instance),
-                ]
-            } else {
-                vec![
-                    LinearCombination::from(one_witt),
-                    LinearCombination::from(*witness),
-                    LinearCombination::from(*instance),
-                ]
-            };
-
-            self.enforce_constraint(R1CS_PREDICATE_LABEL, r1cs_constraint)?;
-        }
-
+        (outliner.func)(self, instance_to_witness_map)?;
         Ok(())
     }
 }