bellpepper

According to repo:

bellpepper is a crate for building zk-SNARK arithmetic circuits and generating witnesses for those circuits. It provides circuit traits and primitive structures, as well as basic gadget implementations such as booleans and number abstractions.

└── src
    ├── constraint_system.rs
    ├── gadgets
    │   ├── boolean.rs
    │   ├── mod.rs
    │   └── num.rs
    ├── lc.rs
    ├── lib.rs
    └── util_cs
        ├── mod.rs
        └── test_cs.rs

lc.rs

Structures

Index
Variable
Indexer
LinearCombination





















pub enum Index {
    Input(usize),
    Aux(usize),
}

pub struct Variable(pub Index);

struct Indexer<T> {
    /// Stores a list of `T` indexed by the number in the first slot of the tuple.
    values: Vec<(usize, T)>,
    /// `(index, key)` of the last insertion operation. Used to optimize consecutive operations
    last_inserted: Option<(usize, usize)>,
}

/// This represents a linear combination of some variables, with coefficients
/// in the scalar field of a pairing-friendly elliptic curve group.
#[derive(Clone, Debug, PartialEq)]
pub struct LinearCombination<Scalar: PrimeField> {
    inputs: Indexer<Scalar>,
    aux: Indexer<Scalar>,
}

Methods

Indexer:

















































impl<T> Indexer<T> {
    pub fn from_value(key: usize, value: T) -> Self {
        Indexer {
            values: vec![(key, value)],
            last_inserted: Some((0, key)),
        }
    }
    
    pub fn insert_or_update<F, G>(&mut self, key: usize, insert: F, update: G)
    where
        F: FnOnce() -> T,
        G: FnOnce(&mut T),
    {
        if let Some((last_index, last_key)) = self.last_inserted {
            // Optimization to avoid doing binary search on inserts & updates that are linear, meaning
            // they are adding a consecutive values.
            if last_key == key {
                // update the same key again
                update(&mut self.values[last_index].1);
                return;
            } else if last_key + 1 == key {
                // optimization for follow on updates
                let i = last_index + 1;
                if i >= self.values.len() {
                    // insert at the end
                    self.values.push((key, insert()));
                    self.last_inserted = Some((i, key));
                } else if self.values[i].0 == key {
                    // update
                    update(&mut self.values[i].1);
                } else {
                    // insert
                    self.values.insert(i, (key, insert()));
                    self.last_inserted = Some((i, key));
                }
                return;
            }
        }
        match self.values.binary_search_by_key(&key, |(k, _)| *k) {
            Ok(i) => {
                update(&mut self.values[i].1);
            }
            Err(i) => {
                self.values.insert(i, (key, insert()));
                self.last_inserted = Some((i, key));
            }
        }
    }
}

The Indexer stores a k-v pair, the values to store the entries and the last_inserted to improve efficiency when inserting, because the entries should be sorted according to key.

from_value, init the Indexer with given (key, value), and set the last_inserted to (0, key)
insert_or_update, insert a entry if the key is new, or update the entry under given key

LinearCombination:






















































































impl<Scalar: PrimeField> LinearCombination<Scalar> {
    pub fn from_coeff(var: Variable, coeff: Scalar) -> Self {
        match var {
            Variable(Index::Input(i)) => Self {
                inputs: Indexer::from_value(i, coeff),
                aux: Default::default(),
            },
            Variable(Index::Aux(i)) => Self {
                inputs: Default::default(),
                aux: Indexer::from_value(i, coeff),
            },
        }
    }
    
    pub fn from_variable(var: Variable) -> Self {
        Self::from_coeff(var, Scalar::ONE)
    }
    
    pub fn iter_mut(&mut self) -> impl Iterator<Item = (Variable, &mut Scalar)> + '_ {
        self.inputs
            .iter_mut()
            .map(|(k, v)| (Variable(Index::Input(*k)), v))
            .chain(
                self.aux
                    .iter_mut()
                    .map(|(k, v)| (Variable(Index::Aux(*k)), v)),
            )
    }

    #[inline]
    fn add_assign_unsimplified_input(&mut self, new_var: usize, coeff: Scalar) {
        self.inputs
            .insert_or_update(new_var, || coeff, |val| *val += coeff);
    }
    
    #[inline]
    fn add_assign_unsimplified_aux(&mut self, new_var: usize, coeff: Scalar) {
        self.aux
            .insert_or_update(new_var, || coeff, |val| *val += coeff);
    } 
    
    pub fn add_unsimplified(
        mut self,
        (coeff, var): (Scalar, Variable),
    ) -> LinearCombination<Scalar> {
        match var.0 {
            Index::Input(new_var) => {
                self.add_assign_unsimplified_input(new_var, coeff);
            }
            Index::Aux(new_var) => {
                self.add_assign_unsimplified_aux(new_var, coeff);
            }
        }

        self
    }
    
    pub fn len(&self) -> usize {
        self.inputs.len() + self.aux.len()
    }
    

    pub fn eval(&self, input_assignment: &[Scalar], aux_assignment: &[Scalar]) -> Scalar {
        let mut acc = Scalar::ZERO;

        let one = Scalar::ONE;

        for (index, coeff) in self.iter_inputs() {
            let mut tmp = input_assignment[*index];
            if coeff != &one {
                tmp *= coeff;
            }
            acc += tmp;
        }

        for (index, coeff) in self.iter_aux() {
            let mut tmp = aux_assignment[*index];
            if coeff != &one {
                tmp *= coeff;
            }
            acc += tmp;
        }

        acc
    }
}

from_coeff, given a Variable and a Scalar, init a Indexer according to the value of the Variable, and set the Indexer to LinearCombination according to the type of the Variable.
from_variable, use the Scalar::ONE.
iter_mut, return the mut Iterator, which merges inputs and aux.
add_assign_unsimplified_input, given the (new_var, coeff), update the inputs: insert or add the coeff under the new_var
add_assign_unsimplified_aux, given the (new_var: usize, coeff), update the aux: insert or add the coeff under the new_var
add_unsimplified, given the (coeff, var: Variable), update the inputs or aux according to the type of Variable.
sub_assign_unsimplified_input, sub_assign_unsimplified_aux, sub_unsimplified is the same to add, just use the -coeff
len, sum of inputs' and aux's len.
eval, given input_assignment: &[Scalar], aux_assignment: &[Scalar], Suppose \(f(x_1, x_2, \dots, x_n) = a_1x_1+ a_2x_2+ \cdots + a_nx_n\) and \(g(x_1, x_2, \dots, x_n) = b_1x_1 + b_2x_2 + \cdots + b_nx_n\), so \((a_1, \dots, a_n)\) is stored in the LinearCombination's inputs, and \((b_1, \dots, b_n)\) is stored in LinearCombination's aux. the self.eval(input_assignment, aux_assignment) means that in \(f(x)\), the \((x_1, x_2, \dots, x_n) = \text{input_assignment}\), and in \(g(x)\), the \((x_1, x_2, \dots, x_n) = \text{aux_assignment}\), the eval will return \(f(\text{input_assignment}) + g(\text{aux_assignment})\)

constraint_system.rs

Trait

















































































































pub trait Circuit<Scalar: PrimeField> {
    /// Synthesize the circuit into a rank-1 quadratic constraint system.
    fn synthesize<CS: ConstraintSystem<Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError>;
}

pub trait ConstraintSystem<Scalar: PrimeField>: Sized + Send {
    type Root: ConstraintSystem<Scalar>;

    fn new() -> Self {
        unimplemented!(
            "ConstraintSystem::new must be implemented for extensible types implementing ConstraintSystem"
        );
    }
    
    fn one() -> Variable {
        Variable::new_unchecked(Index::Input(0))
    }

    fn alloc<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
    where
        F: FnOnce() -> Result<Scalar, SynthesisError>,
        A: FnOnce() -> AR,
        AR: Into<String>;

    fn alloc_input<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
    where
        F: FnOnce() -> Result<Scalar, SynthesisError>,
        A: FnOnce() -> AR,
        AR: Into<String>;
        
    fn enforce<A, AR, LA, LB, LC>(&mut self, annotation: A, a: LA, b: LB, c: LC)
    where
        A: FnOnce() -> AR,
        AR: Into<String>,
        LA: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar>,
        LB: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar>,
        LC: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar>;
        
    fn push_namespace<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;
        
    fn pop_namespace(&mut self);

    fn get_root(&mut self) -> &mut Self::Root;

    fn namespace<NR, N>(&mut self, name_fn: N) -> Namespace<'_, Scalar, Self::Root>
    where
        NR: Into<String>,
        N: FnOnce() -> NR,
    {
        self.get_root().push_namespace(name_fn);

        Namespace(self.get_root(), Default::default())
    }
    
    fn is_extensible() -> bool {
        false
    }
    
    fn extend(&mut self, _other: &Self) {
        unimplemented!(
            "ConstraintSystem::extend must be implemented for types implementing ConstraintSystem"
        );
    }
    
    fn is_witness_generator(&self) -> bool {
        false
    }
    
    fn extend_inputs(&mut self, _new_inputs: &[Scalar]) {
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::extend_inputs must be implemented for witness generators implementing ConstraintSystem")
    }

    fn extend_aux(&mut self, _new_aux: &[Scalar]) {
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::extend_aux must be implemented for witness generators implementing ConstraintSystem")
    }

    fn allocate_empty(
        &mut self,
        _aux_n: usize,
        _inputs_n: usize,
    ) -> (&mut [Scalar], &mut [Scalar]) {
        // This method should only ever be called on witness generators.
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::allocate_empty must be implemented for witness generators implementing ConstraintSystem")
    }

    fn allocate_empty_inputs(&mut self, _n: usize) -> &mut [Scalar] {
        // This method should only ever be called on witness generators.
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::allocate_empty_inputs must be implemented for witness generators implementing ConstraintSystem")
    }

    fn allocate_empty_aux(&mut self, _n: usize) -> &mut [Scalar] {
        // This method should only ever be called on witness generators.
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::allocate_empty_aux must be implemented for witness generators implementing ConstraintSystem")
    }

    fn inputs_slice(&self) -> &[Scalar] {
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::inputs_slice must be implemented for witness generators implementing ConstraintSystem")
    }

    fn aux_slice(&self) -> &[Scalar] {
        assert!(self.is_witness_generator());
        unimplemented!("ConstraintSystem::aux_slice must be implemented for witness generators implementing ConstraintSystem")
    }
}

Circuit
The synthesize method has become a universal method of the zkp library, at least the same in Halo2: whenever it comes to converting computations(various gates) into constraints, we call synthesize.

ConstraintSystem
the ConstraintSystem trait has many methods, which I plan to introduce in detail when a struct implements it.

Structures





#[derive(Debug)]
pub struct Namespace<'a, Scalar: PrimeField, CS: ConstraintSystem<Scalar>>(
    &'a mut CS,
    PhantomData<Scalar>,
);

Namespace wraps a &mut CS structure, and CS needs to implement the ConstraintSystem trait, the lifetime of &mut CS in a Namespace instance should be the same with the Namespace instance.

Methods



impl<'cs, Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
    for Namespace<'cs, Scalar, CS>
{}

Implementations for almost all of ConstraintSystem's methods are provided by the wrapping CS structure, except push_namespace, pop_namespace, because Namespace it self is not the root.

Drop for Namespace





impl<'a, Scalar: PrimeField, CS: ConstraintSystem<Scalar>> Drop for Namespace<'a, Scalar, CS> {
    fn drop(&mut self) {
        self.get_root().pop_namespace()
    }
}

Rust features, mutable references and primitive types need to implement the same traits respectively.



impl<'cs, Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
    for &'cs mut CS
{}

util_cs/mod.rs

Structures






































































pub type Constraint<Scalar> = (
    LinearCombination<Scalar>,
    LinearCombination<Scalar>,
    LinearCombination<Scalar>,
    String,
);


pub trait Comparable<Scalar: PrimeField> {
    /// Example usage:
    ///
    /// ```ignore
    /// let delta = cs.delta(&cs_blank, false);
    /// assert!(delta == Delta::Equal);
    /// ```
    fn num_inputs(&self) -> usize;
    fn num_constraints(&self) -> usize;
    fn inputs(&self) -> Vec<String>;
    fn aux(&self) -> Vec<String>;
    fn constraints(&self) -> &[Constraint<Scalar>];

    fn delta<C: Comparable<Scalar>>(&self, other: &C, ignore_counts: bool) -> Delta<Scalar>
    where
        Scalar: PrimeField,
    {
        let input_count_matches = self.num_inputs() == other.num_inputs();
        let constraint_count_matches = self.num_constraints() == other.num_constraints();

        let inputs_match = self.inputs() == other.inputs();
        let constraints_match = self.constraints() == other.constraints();

        let equal =
            input_count_matches && constraint_count_matches && inputs_match && constraints_match;

        if !ignore_counts && !input_count_matches {
            Delta::InputCountMismatch(self.num_inputs(), other.num_inputs())
        } else if !ignore_counts && !constraint_count_matches {
            Delta::ConstraintCountMismatch(self.num_constraints(), other.num_constraints())
        } else if !constraints_match {
            let c = self.constraints();
            let o = other.constraints();

            let mismatch = c
                .iter()
                .zip(o)
                .enumerate()
                .filter(|(_, (a, b))| a != b)
                .map(|(i, (a, b))| (i, a, b))
                .next();

            let m = mismatch.unwrap();

            Delta::ConstraintMismatch(m.0, m.1.clone(), m.2.clone())
        } else if equal {
            Delta::Equal
        } else {
            Delta::Different
        }
    }
}

#[allow(clippy::large_enum_variant)]
#[derive(Clone, Debug, PartialEq)]
pub enum Delta<Scalar: PrimeField> {
    Equal,
    Different,
    InputCountMismatch(usize, usize),
    ConstraintCountMismatch(usize, usize),
    ConstraintMismatch(usize, Constraint<Scalar>, Constraint<Scalar>),
}

type Constraint<Scalar> is a tuple of 3 LinearCombination and a String.

the trait Comparable is used to compare 2 constrait system's difference.

Note the aux does not participate in comparison, it is really just a temporary, auxiliary variable

util_cs/test_cs.rs

Structures

























#[derive(Debug)]
enum NamedObject {
    Constraint(usize),
    Var(Variable),
    Namespace,
}

#[derive(Debug)]
pub struct TestConstraintSystem<Scalar: PrimeField> {
    named_objects: HashMap<String, NamedObject>,
    current_namespace: Vec<String>,
    #[allow(clippy::type_complexity)]
    constraints: Vec<(
        LinearCombination<Scalar>,
        LinearCombination<Scalar>,
        LinearCombination<Scalar>,
        String,
    )>,
    inputs: Vec<(Scalar, String)>,
    aux: Vec<(Scalar, String)>,
}

#[derive(Clone, Copy)]
struct OrderedVariable(Variable);

Methods

OrderedVariable










impl Ord for OrderedVariable {
    fn cmp(&self, other: &Self) -> Ordering {
        match (self.0.get_unchecked(), other.0.get_unchecked()) {
            (Index::Input(ref a), Index::Input(ref b)) => a.cmp(b),
            (Index::Aux(ref a), Index::Aux(ref b)) => a.cmp(b),
            (Index::Input(_), Index::Aux(_)) => Ordering::Less,
            (Index::Aux(_), Index::Input(_)) => Ordering::Greater,
        }
    }
}

Note:
Index::Input < Index::Aux

proc_lc, transform a LinearCombination to a BTreeMap<OrderedVariable, Scalar>, and will delete the entry whose'value is Scalar::ZERO.

hash_lc, hash a LinearCombination with Blake2s

eval_lc, the same with LinearCombination.eval(&inputs, &aux), see before for detail.

TestConstraintSystem

















impl<Scalar: PrimeField> Default for TestConstraintSystem<Scalar> {
    fn default() -> Self {
        let mut map = HashMap::new();
        map.insert(
            "ONE".into(),
            NamedObject::Var(TestConstraintSystem::<Scalar>::one()),
        );

        TestConstraintSystem {
            named_objects: map,
            current_namespace: vec![],
            constraints: vec![],
            inputs: vec![(Scalar::ONE, "ONE".into())],
            aux: vec![],
        }
    }
}

TestConstraintSystem's default will init the map and inputs.

scalar_inputs, return TestConstraintSystem's inputs field
scalar_aux, return the TestConstraintSystem's aux field.
pretty_print_list, return the strings in TestConstraintSystem's inputs, aux, constraints field.
pretty_print, merge the list from pretty_print_list with \n.
hash, Blake2s hash, only the inputs, aux, constraints's len() and constraints' internal 3 LinearCombination will effect the hash.

which_is_unsatisfied:















pub fn which_is_unsatisfied(&self) -> Option<&str> {
    for (a, b, c, path) in &self.constraints {
        let mut a = eval_lc::<Scalar>(a, &self.inputs, &self.aux);
        let b = eval_lc::<Scalar>(b, &self.inputs, &self.aux);
        let c = eval_lc::<Scalar>(c, &self.inputs, &self.aux);

        a.mul_assign(&b);

        if a != c {
            return Some(path);
        }
    }

    None
}

\(f(x_1, x_2, \dots, x_n) = a_1x_1 + a_2x_2 + \cdots + a_nx_n\)
\(g(x_1, x_2, \dots, x_n) = b_1x_1 + b_2x_2 + \cdots + b_nx_n\)

\(a, b, c\) are the LinearCombination type, which contains the \(f, g\).

if there is any \((a, b, c)\) in constraints, that \(\begin{pmatrix}f_a(\text{self.inputs}) + g_a(\text{self.aux})\end{pmatrix} \cdot \begin{pmatrix}f_b(\text{self.inputs}) + g_b(\text{self.aux})\end{pmatrix} \\ \neq f_c(\text{self.inputs}) + g_c(\text{self.aux})\), that means the inputs and aux are unsatisfied to the constraints, return the constraint's path.

is_satisfied, for all \((a, b, c)\) in constraints, \(\begin{pmatrix}f_a(\text{self.inputs}) + g_a(\text{self.aux})\end{pmatrix} \cdot \begin{pmatrix}f_b(\text{self.inputs}) + g_b(\text{self.aux})\end{pmatrix} = f_c(\text{self.inputs}) + g_c(\text{self.aux})\)
num_constraints, the len of constraints
set, given (path: &str, to: Scalar), get the index in named_objects of the path, set the inputs[index] or aux[index] = to
verify, given (expected: &[Scalar]), if expected = self.inputs[1..], true, else, false.
num_inputs, inputs' len


impl<Scalar: PrimeField> ConstraintSystem<Scalar> for TestConstraintSystem<Scalar> {
}

alloc, push the val(Scalar) to self.aux
alloc_input, push the val(Scalar) to self.inputs
enforce, push the Constraint(a, b, c) to self.constraints
push_namespace, modify the named_objects, current_namespace
pop_namespace, pop current_namespace
get_root, return ``&mut self`

tests

















































fn test_cs() {
    let mut cs = TestConstraintSystem::<Fr>::new();
    assert!(cs.is_satisfied());
    assert_eq!(cs.num_constraints(), 0);
    // cs.aux = vec![(10, "var")];
    // a = Variable(0);
    let a = cs
        .namespace(|| "a")
        .alloc(|| "var", || Ok(Fr::from(10u64)))
        .unwrap();
    // cs.aux = vec![(10, "var"), (4, "var")];
    // b = Variable(1);
    let b = cs
        .namespace(|| "b")
        .alloc(|| "var", || Ok(Fr::from(4u64)))
        .unwrap();
    // cs.aux = vec![(10, "var"), (4, "var"), (40, "product")];
    // c = Variable(2)
    let c = cs.alloc(|| "product", || Ok(Fr::from(40u64))).unwrap();

    // cs.constraints = vec![(LC{inputs: vec![], aux: vec![(0, scalar::one)]}, LC{inputs: vec![], aux: vec![(1, scalar::one)]}, LC{inputs: vec![], aux: vec![(2, scalar::one)]})]
    cs.enforce(|| "mult", |lc| lc + a, |lc| lc + b, |lc| lc + c);
    // (1 * cs.aux[0].0) * (1 * cs.aux[1].0 == (1 * cs.aux[2].0))
    assert!(cs.is_satisfied());
    assert_eq!(cs.num_constraints(), 1);

    // cs.aux = vec![(4, "var"), (4, "var"), (40, "product")];
    cs.set("a/var", Fr::from(4u64));

    let one = TestConstraintSystem::<Fr>::one();
    cs.enforce(|| "eq", |lc| lc + a, |lc| lc + one, |lc| lc + b);

    assert!(!cs.is_satisfied());
    assert!(cs.which_is_unsatisfied() == Some("mult"));

    assert!(cs.get("product") == Fr::from(40u64));

    // cs.aux = vec![(4, "var"), (4, "var"), (16, "product")];
    cs.set("product", Fr::from(16u64));
    assert!(cs.is_satisfied());

    {
        let mut cs = cs.namespace(|| "test1");
        let mut cs = cs.namespace(|| "test2");
        cs.alloc(|| "hehe", || Ok(Fr::ONE)).unwrap();
    }

    assert!(cs.get("test1/test2/hehe") == Fr::ONE);
}

Note that:







impl<Scalar: PrimeField> Add<Variable> for LinearCombination<Scalar> {
    type Output = LinearCombination<Scalar>;

    fn add(self, other: Variable) -> LinearCombination<Scalar> {
        self + (Scalar::ONE, other)
    }
}

so, if LC + Variable, means, LC + Scalar::ONE in that variable index.

gadgets/boolean.rs

Structures






#[derive(Debug, Clone)]
pub struct AllocatedBit {
    variable: Variable,
    value: Option<bool>,
}

Methods

AllocatedBit


































impl AllocatedBit {
    pub fn alloc_conditionally<Scalar, CS>(
        mut cs: CS,
        value: Option<bool>,
        must_be_false: &AllocatedBit,
    ) -> Result<Self, SynthesisError>
    where
        Scalar: PrimeField,
        CS: ConstraintSystem<Scalar>,
    {
        let var = cs.alloc(
            || "boolean",
            || {
                if value.ok_or(SynthesisError::AssignmentMissing)? {
                    Ok(Scalar::ONE)
                } else {
                    Ok(Scalar::ZERO)
                }
            },
        )?;

        cs.enforce(
            || "boolean constraint",
            |lc| lc + CS::one() - must_be_false.variable - var,
            |lc| lc + var,
            |lc| lc,
        );

        Ok(AllocatedBit {
            variable: var,
            value,
        })
    }
}

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`	在筆記中貼入程式碼
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.