---
# System prepended metadata

title: Note for bellpepper
tags: [zkSNARK, circuit]

---

# bellpepper

According to [repo](https://github.com/lurk-lab/bellpepper):
> 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


```rs=
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:**

```rs=
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:**

```rs=
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
```rs=
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
```rs=
#[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
```rs=
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`
```rs=
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.
```rs=
impl<'cs, Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
    for &'cs mut CS
{}
```

## util_cs/mod.rs

### Structures
```rs=
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
```rs=
#[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**
```rs=
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**


```rs=
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`:
    ```rs=
    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

```rs=
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
```rs=
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:
```rs=
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
```rs=
#[derive(Debug, Clone)]
pub struct AllocatedBit {
    variable: Variable,
    value: Option<bool>,
}

```

### Methods

**AllocatedBit**
```rs=
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,
        })
    }
}
```




