Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Refactor constraint system #131

Merged
merged 27 commits into from
Feb 4, 2022
Merged
Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
f88b7c7
Implementation of ConstraintSystemImpl
lgiussan Sep 28, 2021
abe2565
Update groth16 and gm17 to use ConstraintSystemImpl
lgiussan Sep 28, 2021
376ebdc
Implement test functionality for ConstraintSystemImpl
lgiussan Sep 30, 2021
6dc70ea
Remove TestConstraintSystem and update tests to use ConstraintSystemI…
lgiussan Sep 30, 2021
1edac58
Add variables to named_objects during alloc
lgiussan Sep 30, 2021
0a3364b
Panic when trying to get or set variables during setup
lgiussan Sep 30, 2021
45ff1e9
Bugfix: building constraint matrices when not required
lgiussan Sep 30, 2021
7d24190
Fix Cargo.toml files
lgiussan Sep 30, 2021
aa6ce0b
Fix Cargo.toml files (hopefully)
lgiussan Oct 1, 2021
23739ca
fix failing proof-systems tests
lgiussan Oct 4, 2021
0bd1bc3
rename ConstraintSystemImpl and ConstraintSystem
lgiussan Oct 18, 2021
d5a8399
Add debugging functions to ConstraintSystem trait
lgiussan Oct 18, 2021
8881671
Merge branch 'development_tmp' into refactor_constraint_system
lgiussan Oct 18, 2021
d2dc6cc
Remove print_named_objects function
lgiussan Oct 19, 2021
d2c83e0
Remove unnecessary override
lgiussan Oct 19, 2021
e5c45a0
Delete commented out code
lgiussan Oct 19, 2021
5ecf4e6
Introduce Debug mode in ConstraintSystem
lgiussan Oct 21, 2021
420256d
Merge remote-tracking branch 'origin/refactor_constraint_system' into…
lgiussan Oct 21, 2021
555ec1f
Changes after code review
lgiussan Oct 25, 2021
6b79526
Changes after code review
lgiussan Oct 26, 2021
04926c8
cargo-fmt
lgiussan Oct 28, 2021
f15ebb4
Merge branch 'development' into refactor_constraint_system
lgiussan Oct 28, 2021
7ab5a5b
Update Cargo.toml files
lgiussan Oct 29, 2021
e25730f
Merge branch 'endo' into refactor_constraint_system
lgiussan Oct 29, 2021
d41aef6
Merge remote-tracking branch 'origin/development' into refactor_const…
lgiussan Nov 16, 2021
a61fc10
Merge branch 'development' into refactor_constraint_system
DanieleDiBenedetto Jan 12, 2022
6ac16de
Fix compilation error
DanieleDiBenedetto Jan 12, 2022
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 0 additions & 39 deletions proof-systems/src/gm17/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,50 +11,11 @@ use crate::gm17::r1cs_to_sap::R1CStoSAP;

use r1cs_core::{ConstraintSynthesizer, SynthesisError, ConstraintSystem, SynthesisMode};

// use smallvec::SmallVec;

use std::{
ops::AddAssign,
sync::Arc,
};

// type CoeffVec<T> = SmallVec<[T; 2]>;
//
// #[inline]
// fn eval<E: PairingEngine>(
// lc: &LinearCombination<E::Fr>,
// constraints: &mut [CoeffVec<(E::Fr, Index)>],
// input_assignment: &[E::Fr],
// aux_assignment: &[E::Fr],
// this_constraint: usize,
// ) -> E::Fr {
// let mut acc = E::Fr::zero();
//
// for &(index, coeff) in lc.as_ref() {
// let mut tmp;
//
// match index.get_unchecked() {
// Index::Input(i) => {
// constraints[this_constraint].push((coeff, Index::Input(i)));
// tmp = input_assignment[i];
// },
// Index::Aux(i) => {
// constraints[this_constraint].push((coeff, Index::Aux(i)));
// tmp = aux_assignment[i];
// },
// }
//
// if coeff.is_one() {
// acc.add_assign(&tmp);
// } else {
// tmp.mul_assign(&coeff);
// acc.add_assign(&tmp);
// }
// }
//
// acc
// }

pub fn create_random_proof<E, C, R>(
circuit: C,
params: &Parameters<E>,
Expand Down
3 changes: 2 additions & 1 deletion r1cs/core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,5 @@ license = "MIT/Apache-2.0"
[dependencies]
algebra = { git = "https://github.com/HorizenOfficial/ginger-lib", branch = "sc_testnet_2" }
smallvec = { version = "1.6.1" }
radix_trie = {version = "0.2.1"}
radix_trie = { version = "0.2.1" }
rand = { version = "0.8.4" }
89 changes: 47 additions & 42 deletions r1cs/core/src/constraint_system.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use std::marker::PhantomData;
use algebra::Field;
use radix_trie::{Trie, TrieCommon};
use radix_trie::Trie;

use crate::{Index, Variable, LinearCombination, SynthesisError};

Expand Down Expand Up @@ -74,9 +74,6 @@ pub trait ConstraintSystemAbstract<F: Field>: Sized {
/// Output the number of constraints in the system.
fn num_constraints(&self) -> usize;

/// Prints the list of named object currently registered into the constraint system.
fn print_named_objects(&self);

/// Returns an Option containing the name of the first constraint which is not satisfied
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
/// or None if all the constraints are satisfied.
fn which_is_unsatisfied(&self) -> Option<&str>;
Expand All @@ -99,8 +96,9 @@ pub trait ConstraintSystemAbstract<F: Field>: Sized {
#[derive(Debug, Clone)]
pub struct ConstraintSystem<F: Field> {
/// 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
/// be in setup mode (i.e., `self.mode == SynthesisMode::Setup`), in
/// proving mode (i.e., `self.mode == SynthesisMode::Prove`), or in debug
/// mode (i.e. `self.mode == SynthesisMode::Debug`). 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).
Expand All @@ -125,8 +123,15 @@ pub struct ConstraintSystem<F: Field> {
pub bt: Vec<Vec<(F, Index)>>,
/// `C` matrix of the R1CS.
pub ct: Vec<Vec<(F, Index)>>,
/// A data structure for associating a name to variables, constraints and
/// namespaces registered into the constraint system. This is populated only
/// if `self.debug == true`.
named_objects: Trie<String, NamedObject>,
/// A stack keeping track of the current namespace. This is populated only if
/// `self.debug == true`.
current_namespace: Vec<String>,
/// A list of the constraint names. This is populated only if `self.debug
/// == true`.
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
constraint_names: Vec<String>,
}

Expand All @@ -144,6 +149,10 @@ pub enum SynthesisMode {
/// the matrices as in the `Setup` case.
construct_matrices: bool,
},
/// Indicate to `ConstraintSystem` that it populate variable assignments,
/// generate constraint matrices and register names of variables, constraints
/// and namespaces
Debug,
}

#[derive(Debug, Clone)]
Expand Down Expand Up @@ -189,9 +198,11 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
let index = self.num_aux;
self.num_aux += 1;

let path = compute_path(&self.current_namespace, annotation().into());
let var = Variable::new_unchecked(Index::Aux(index));
self.set_named_obj(path, NamedObject::Var(var));
if self.is_in_debug_mode() {
let path = compute_path(&self.current_namespace, annotation().into());
let var = Variable::new_unchecked(Index::Aux(index));
self.set_named_obj(path, NamedObject::Var(var));
}

if !self.is_in_setup_mode() {
self.aux_assignment.push(f()?);
Expand All @@ -208,9 +219,11 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
let index = self.num_inputs;
self.num_inputs += 1;

let path = compute_path(&self.current_namespace, annotation().into());
let var = Variable::new_unchecked(Index::Input(index));
self.set_named_obj(path, NamedObject::Var(var));
if self.is_in_debug_mode() {
let path = compute_path(&self.current_namespace, annotation().into());
let var = Variable::new_unchecked(Index::Input(index));
self.set_named_obj(path, NamedObject::Var(var));
}

if !self.is_in_setup_mode() {
self.input_assignment.push(f()?);
Expand All @@ -226,11 +239,12 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
LB: FnOnce(LinearCombination<F>) -> LinearCombination<F>,
LC: FnOnce(LinearCombination<F>) -> LinearCombination<F>,
{
let path = compute_path(&self.current_namespace, annotation().into());
let index = self.num_constraints;
self.set_named_obj(path.clone(), NamedObject::Constraint(index));

self.constraint_names.push(path.clone());
if self.is_in_debug_mode() {
let path = compute_path(&self.current_namespace, annotation().into());
let index = self.num_constraints;
self.set_named_obj(path.clone(), NamedObject::Constraint(index));
self.constraint_names.push(path.clone());
}

if self.should_construct_matrices() {
self.at.push(vec![]);
Expand Down Expand Up @@ -260,25 +274,24 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
NR: Into<String>,
N: FnOnce() -> NR
{
let name = name_fn().into();
let path = compute_path(&self.current_namespace, name.clone());
self.set_named_obj(path.clone(), NamedObject::Namespace);
self.current_namespace.push(name);
if self.is_in_debug_mode() {
let name = name_fn().into();
let path = compute_path(&self.current_namespace, name.clone());
self.set_named_obj(path.clone(), NamedObject::Namespace);
self.current_namespace.push(name);
}
}
fn pop_namespace(&mut self) {
assert!(self.current_namespace.pop().is_some());
if self.is_in_debug_mode() {
assert!(self.current_namespace.pop().is_some());
}
}
fn get_root(&mut self) -> &mut Self::Root {
self
}
fn num_constraints(&self) -> usize {
self.num_constraints
}
fn print_named_objects(&self) {
for (name, _) in self.named_objects.iter() {
println!("{}", name);
}
}
fn which_is_unsatisfied(&self) -> Option<&str> {
for i in 0..self.num_constraints {
let mut a = Self::eval_lc(&self.at[i], &self.input_assignment, &self.aux_assignment);
Expand All @@ -293,13 +306,7 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
None
}

fn is_satisfied(&self) -> bool {
self.which_is_unsatisfied().is_none()
}
fn set(&mut self, path: &str, to: F) {
if self.is_in_setup_mode() {
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
panic!("it is not possible to set the value of variables during setup.")
}
match self.named_objects.get(path) {
Some(&NamedObject::Var(ref v)) => match v.get_unchecked() {
Index::Input(index) => self.input_assignment[index] = to,
Expand All @@ -313,9 +320,6 @@ impl<F: Field> ConstraintSystemAbstract<F> for ConstraintSystem<F> {
}
}
fn get(&mut self, path: &str) -> F {
if self.is_in_setup_mode() {
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
panic!("it is not possible to get the value of variables during setup.")
}
match self.named_objects.get(path) {
Some(&NamedObject::Var(ref v)) => match v.get_unchecked() {
Index::Input(index) => self.input_assignment[index],
Expand Down Expand Up @@ -370,8 +374,15 @@ impl<F: Field> ConstraintSystem<F> {
match self.mode {
SynthesisMode::Setup => true,
SynthesisMode::Prove { construct_matrices } => construct_matrices,
SynthesisMode::Debug => true,
}
}

/// Check if the constraint system is in debug mode
pub fn is_in_debug_mode(&self) -> bool {
self.mode == SynthesisMode::Debug
}

fn push_constraints(
l: LinearCombination<F>,
constraints: &mut [Vec<(F, Index)>],
Expand Down Expand Up @@ -495,9 +506,6 @@ impl<F: Field, CS: ConstraintSystemAbstract<F>> ConstraintSystemAbstract<F> for
self.0.num_constraints()
}

#[inline]
fn print_named_objects(&self) { self.0.print_named_objects(); }

#[inline]
fn which_is_unsatisfied(&self) -> Option<&str> { self.0.which_is_unsatisfied() }

Expand Down Expand Up @@ -581,9 +589,6 @@ impl<F: Field, CS: ConstraintSystemAbstract<F>> ConstraintSystemAbstract<F> for
(**self).num_constraints()
}

#[inline]
fn print_named_objects(&self) { (**self).print_named_objects(); }

#[inline]
fn which_is_unsatisfied(&self) -> Option<&str> { (**self).which_is_unsatisfied() }

Expand Down
73 changes: 73 additions & 0 deletions r1cs/core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,3 +85,76 @@ pub enum ConstraintVar<F: Field> {
/// A wrapper around a `Variable`.
Var(Variable),
}

/// Debug a circuit by looking for unsatisfied constraints.
/// If the circuit is satisfied, return `Ok(None)`.
/// If there are unsatisfied constraints, return `Ok(Some(name))`,
/// where `name` is the name of the first unsatisfied constraint.
pub fn debug_circuit<F: Field, C: ConstraintSynthesizer<F>>(circuit: C) -> Result<Option<String>, SynthesisError> {
let mut cs = ConstraintSystem::<F>::new();
cs.set_mode(SynthesisMode::Debug);
circuit.generate_constraints(&mut cs)?;
let unsatisfied_constraint = cs.which_is_unsatisfied();
match unsatisfied_constraint {
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
None => Ok(None),
Some(name) => Ok(Some(name.into())),
}
}

#[cfg(test)]
mod test {
use algebra::Field;
use algebra::fields::tweedle::fr::Fr;
use crate::{ConstraintSynthesizer, ConstraintSystemAbstract, debug_circuit, SynthesisError};
use rand;

struct MyCircuit<F: Field> {
a: Option<F>,
b: Option<F>,
c: Option<F>,
}

impl<F: Field> ConstraintSynthesizer<F> for MyCircuit<F> {
fn generate_constraints<CS: ConstraintSystemAbstract<F>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
let a = cs.alloc(|| "a", || self.a.ok_or(SynthesisError::AssignmentMissing))?;
let b = cs.alloc(|| "b", || self.b.ok_or(SynthesisError::AssignmentMissing))?;
let c = cs.alloc(|| "c", || self.c.ok_or(SynthesisError::AssignmentMissing))?;
cs.enforce(||"multiplication constraint", |lc| lc + a, |lc| lc + b, |lc| lc + c);
Ok(())
}
}

#[test]
fn test_debug_circuit_satisfied() {
let a: Fr = rand::random();
let b: Fr = rand::random();
let mut c = a.clone();
c *= &b;
let circuit =
MyCircuit {
a: Some(a),
b: Some(b),
c: Some(c)
};
let unsatisfied_constraint = debug_circuit(circuit).unwrap();
assert!(unsatisfied_constraint.is_none());
}

#[test]
fn test_debug_circuit_unsatisfied() {
let a: Fr = rand::random();
let b: Fr = rand::random();
let mut c = a.clone();
c *= &b;
c += &b;
let circuit =
MyCircuit {
a: Some(a),
b: Some(b),
c: Some(c)
};
let unsatisfied_constraint = debug_circuit(circuit).unwrap();
assert!(unsatisfied_constraint.is_some());
assert_eq!(unsatisfied_constraint.unwrap(), "multiplication constraint");
}
DanieleDiBenedetto marked this conversation as resolved.
Show resolved Hide resolved
}
3 changes: 2 additions & 1 deletion r1cs/gadgets/crypto/src/commitment/blake2s/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -121,12 +121,13 @@ mod test {
},
*,
};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem, SynthesisMode};
use r1cs_std::prelude::*;

#[test]
fn commitment_gadget_test() {
let mut cs = ConstraintSystem::<Fr>::new();
cs.set_mode(SynthesisMode::Debug);

let input = [1u8; 32];

Expand Down
3 changes: 2 additions & 1 deletion r1cs/gadgets/crypto/src/commitment/pedersen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -201,14 +201,15 @@ mod test {
CommitmentGadget,
};
use algebra::curves::{jubjub::JubJubProjective as JubJub, ProjectiveCurve};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem, SynthesisMode};
use r1cs_std::{
instantiated::jubjub::JubJubGadget, prelude::*,
};

#[test]
fn commitment_gadget_test() {
let mut cs = ConstraintSystem::<Fq>::new();
cs.set_mode(SynthesisMode::Debug);

#[derive(Clone, PartialEq, Eq, Hash)]
pub(super) struct Window;
Expand Down
3 changes: 2 additions & 1 deletion r1cs/gadgets/crypto/src/crh/bowe_hopwood/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ mod test {
FixedLengthCRHGadget,
};
use algebra::{curves::edwards_sw6::EdwardsProjective as Edwards, ProjectiveCurve};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem};
use r1cs_core::{ConstraintSystemAbstract, ConstraintSystem, SynthesisMode};
use r1cs_std::{
alloc::AllocGadget, instantiated::edwards_sw6::EdwardsSWGadget, uint8::UInt8,
};
Expand Down Expand Up @@ -192,6 +192,7 @@ mod test {
fn crh_primitive_gadget_test() {
let rng = &mut thread_rng();
let mut cs = ConstraintSystem::<Fr>::new();
cs.set_mode(SynthesisMode::Debug);

let (input, input_bytes) = generate_input(&mut cs, rng);
println!("number of constraints for input: {}", cs.num_constraints());
Expand Down
Loading