# Zero knowledge proofs using Bulletproofs

Feb 23 · 17 min read

Here i will show how to create various zero knowledge proofs using the Bulletproofs implementation from dalek-cryptography. The examples will be i) proving knowledge of factors of a given number without revealing the factors, ii) a range proof, i.e. prove that you know a value x such that a ≤ x ≤ b without revealing x, iii) prove that the value you have is non-zero without revealing it (without using above range proof), iv) prove that the value is not equal to a given value without revealing your own, v) Set membership, i.e given a set S, prove that you know an element contained in the set without revealing the element, vi) Similarly, set non-membership without revealing the value of the absent element. The examples can be adapted with little effort such that they can be used in ZK-SNARK implementations like libsnark or bellman. To directly browse the code, go here.

# Overview

The high level idea of this proving system is that
1. The prover commits to a value(s) that he wants to prove knowledge of
2. The prover generates the proof by enforcing the constraints over the committed values and any additional public values. The constraints might require the prover to commit to some additional variables.
3. Prover sends the verifier all the commitments he made in step 1 and step 2 along with the proof from step 2.
4. The verifier now verifies the proof by enforcing the same constraints over the commitments plus any public values.

# Bulletproofs API

1. Create some generators that will be used by both the prover and verifier

`let pc_gens = PedersenGens::default();let bp_gens = BulletproofGens::new(128, 1);`

The above code creates 2 sets of generators, `pc_gens` are a pair of 2 generators and `bp_gens` are a pair of 2 vectors (list) of generators. The argument 128 indicates that each vector will have 128 generators. So in total you create 2*128=256 generators in `bp_gens`. `pc` and `bp` stand for Pedersen and Bulletproofs respectively.

2. Instantiate a prover

`let mut prover_transcript = Transcript::new(b"Factors");let mut prover = Prover::new(&bp_gens, &pc_gens, &mut prover_transcript);`

`prover_transcript` is a transcript for the prover. A transcript is the record of messages exchanged between prover and verifier like the commitments sent by the prover to the verifier or the challenges sent by the verifier to prover. Since this Bulletproofs implementation is non-interactive, challenges are generated by Fiat-Shamir heuristic, i.e hashing the current state of the transcript. `Factors` is the label of the transcript and is used to differentiate between different transcripts or sub transcripts when the protocol is composed of sub protocols.

3. Prover commits to variables

`let x1 = Scalar::random(&mut rng);let (com_p, var_p) = prover.commit(p.into(), x1);let x2 = Scalar::random(&mut rng);let (com_q, var_q) = prover.commit(q.into(), x2);`

In above, the prover commits to the factor `p` using randomness `x1` and the 2 generators `g` and `h` of `pc_gens`. This is a Pedersen commitment, hence `com_p = gᵖhˣ¹`. Similarly `com_q` is commitment to `q` with `x2`. In addition to creating the commitment, the `commit` method also creates corresponding variables for the constraint system, `var_p` and `var_q` are variables for `p` and `q` respectively. Additionally the 2 commitments are added to the transcript during`commit`.

4. Prover constrains the variables

`let (_, _, o) =  prover.multiply(var_p.into(), var_q.into());`

With the `multiply` function the prover specifies that variables `var_p` and `var_q` are to be multiplied together and the result be captured in the variable `o`. Also this function will result in the allocation of the variables corresponding to `var_p`, `var_q` and `o`. Additionally `multiply` evaluates the input variables and constraints them to be equal to the corresponding allocated variables.

`let r_lc: LinearCombination = vec![(Variable::One(),      r.into())].iter().collect();prover.constrain(o -  r_lc);`

Now the prover wants to enforce that the product of `p` and `q` is equal to `r`. Since the product of variables for `p` and `q`, i.e. `var_p` and `var_q` is captured in variable `o`, the prover can allocate a variable for `r` and then ensure that the subtraction for the r-variable and `o` is 0. The prover creates this r-variable by creating a linear constraint, i.e. a variable multiplied with a scalar. The tuple `(Variable::One(), r.into())` represents the linear constraint with value equal to `r`, i.e. multiply the variable with value 1 (`Variable::One()`) with the scalar `r`. If the prover wanted to create a variable with value p+q+r, he could create by `vec![(Variable::One(), (p+q+r).into())]` or by `vec![(Variable::One(), p.into()), (Variable::One(), q.into()), (Variable::One(), r.into())]` the terms of the vector are added.
Since linear combinations can be added or subtracted from each other to give another linear combination, the prover ensures that the linear combination `o — lc` is 0, this is done by calling `constrain`. The method `constrain` ensures that the linear combination passed to it is equal to 0.

5. Prover creates the proof

`let proof = prover.prove().unwrap();`

6. Instantiate the verifier

`let mut verifier_transcript = Transcript::new(b"Factors");let mut verifier = Verifier::new(&bp_gens, &pc_gens, &mut verifier_transcript);`

Here the verifier is instantiated and it creates it own transcript. Note that the name of the transcript is same as that in case of prover. This is important since the name is part of the transcript content and the challenges between the prover and verifier are hash of the transcript content. Different names will result in different transcript content and hence different challenges for prover and verifier which will result in failure of proof verification.

7. Verifier using the commitments.

`let var_p = verifier.commit(commitments.0);let var_q = verifier.commit(commitments.1);`

The verifier records the commitments for p and q sent by the prover in the transcript and creates variables for these commitments similar to the prover. The difference is the prover had access to the value being committed to and the randomness whereas the verifier doesn’t.

8. Verifier constrains the variables

`let (_, _, o) =  verifier.multiply(var_p.into(), var_q.into());let r_lc: LinearCombination = vec![(Variable::One(), r.into())].iter().collect();verifier.constrain(o -  r_lc);`

Similar to the prover, the verifer also constrains the variables corresponding to commitment. Notice that the constraints are exactly the same as that of the prover.

9. Finally the verifier verifies the proof.

`verifier.verify(&proof)`

This example is missing a constrain for ensuring that neither `p` nor `q` can be 1 (unless `r` is 1), this can be done using range proof (which is expenve) or proving not equal to 1 as shown in example below. The complete example is here.

# More examples

`for i in 0..n {    // Create low-level variables and add them to constraints    let (a, b, o) = cs.allocate(|| {        let q: u64 = v.assignment.ok_or(R1CSError::MissingAssignment)?;        let bit: u64 = (q >> i) & 1;        Ok(((1 - bit).into(), bit.into(), Scalar::zero()))    })?;    // Enforce a * b = 0, so one of (a,b) is zero    cs.constrain(o.into());    // Enforce that a = 1 - b, so they both are 1 or 0.    cs.constrain(a + (b - 1u64));}`

The above example iterates over the n bits of `v`. `cs` is constraint system. Both the prover and verifier from previous examples are constraint systems and both will run the above code block. `allocate` will allocate 3 variables, `a`, `b` and `o` with the constraint that `a * b = o`. Also variables `a` and `b` are assigned values `1-bit` and `bit` respectively. Hence, for each bit `bit` of `v` (`(q >> i) & 1` returns the `i`th least significant bit), the prover will satify the constaint `(1-bit)*bit=o` and will constrain `o` to be 0 in `cs.constrain(o.into())`. But if you notice the closure passed to `allocate` has access to value of `v` which cannot be the case for the verifier, and indeed its not. The closure is only executed for the prover and not for the verifier. But this means that can put assign arbitrary values to `a` and `b` since only `o` is constrained to be 0, eg a=3 and b=0 still result in a*b=0. Thus the need of an additional constraint that `a = 1 - b` =>` cs.constrain(a + (b — 1u64))`
The above example proves the that element of the vector is a bit but still does not prove that the bit-vector is for `v`. eg the above constraint system will be satisfied for all 0’s or all 1’s but that might not be the correct representation of `v`. We need more constraints to prove that the bit vector is for `v`.

`pub fn positive_no_gadget<CS: ConstraintSystem>(    cs: &mut CS,    v: AllocatedQuantity,    n: usize    ,) -> Result<(), R1CSError> {    let mut constraint_v = vec![(v.variable, -Scalar::one())];    let mut exp_2 = Scalar::one();    for i in 0..n {        // Create low-level variables and add them to constraints        let (a, b, o) = cs.allocate(|| {            ....        })?;        // Enforce a * b = 0, so one of (a,b) is zero        // Enforce that a = 1 - b, so they both are 1 or 0.        ....        constraint_v.push((b, exp_2)  );        exp_2 = exp_2 + exp_2;    }    // Enforce that -v + Sum(b_i * 2^i, i = 0..n-1) = 0 => Sum(b_i * 2^i, i = 0..n-1) = v    cs.constrain(constraint_v.iter().collect());    Ok(())}`

We begin by vector of linear combinations `constraint_v`, negative `v` being its first term. Then for each bit of `v`, we multiply the bit with an appropriate power of 2 and add the result to the above linear combination in `constraint_v.push((b, exp_2))`. Finally summing all the terms of the linear combination results in 0. `cs.constrain(constraint_v.iter().collect())` means add all terms of `constraint_v` and ensure that the sum is 0. The type `AllocatedQuantity` is a wrapper over the committed variable. The complete code is here.
Now we can use the above `positive_no_gadget` to prove that both `x-min` and `max — x` are in [0, 2ⁿ). This looks fine but the prover can still cheat. Since the prover is only giving commitments to `x-min` and `max-x`, he can cheat by using different `x` in the commitment, so one commitment is over `x-min` and other over `max-y`. This can be fixed by ensuring that adding both committed value leads to the result `max-min`. Let a = x-min and b=max-x. The prover commits to `v`, `a` and `b`.

`let (com_v, var_v) = prover.commit(v.into(), Scalar::random(&mut rng));let quantity_v = AllocatedQuantity {    variable: var_v,    assignment: Some(v),};let (com_a, var_a) = prover.commit(a.into(), Scalar::random(&mut rng));let quantity_a = AllocatedQuantity {    variable: var_a,    assignment: Some(a),};let (com_b, var_b) = prover.commit(b.into(), Scalar::random(&mut rng));let quantity_b = AllocatedQuantity {    variable: var_b,    assignment: Some(b),};`

The prover passes the variables for `v`, `a` and `b` to the `bound_check_gadget` which ensure that `v` is in [`min`, `max`]. He then creates the proof.

`assert!(bound_check_gadget(&mut prover, quantity_v, quantity_a, quantity_b, max, min, n).is_ok());let proof = prover.prove()?;`

The `bound_check_gadget` ensures that a+b = max-min and both a and b are in [0, 2ⁿ). The complete code is here.

`pub fn bound_check_gadget<CS: ConstraintSystem>(    cs: &mut CS,    v: AllocatedQuantity,    a: AllocatedQuantity,    b: AllocatedQuantity,    max: u64,    min: u64,    n: usize) -> Result<(), R1CSError> {    // a + b = max - min    let lc_max_minus_min: LinearCombination = vec![(Variable::One(), Scalar::from(max-min))].iter().collect();    // Constrain a + b to be same as max - min.    cs.constrain(a.variable + b.variable - lc_max_minus_min);    // Constrain a in [0, 2^n)    assert!(positive_no_gadget(cs, a, n).is_ok());    // Constrain b in [0, 2^n)    assert!(positive_no_gadget(cs, b, n).is_ok());    Ok(())}`

## Proof that a committed value is non-zero

`let (com_val, var_val) = prover.commit(value.clone(), Scalar::random(&mut rng));let alloc_scal = AllocatedScalar {    variable: var_val,    assignment: Some(value),};let inv = value.invert();let (com_val_inv, var_val_inv) = prover.commit(inv.clone(), Scalar::random(&mut rng));let alloc_scal_inv = AllocatedScalar {    variable: var_val_inv,    assignment: Some(inv),};assert!(is_nonzero_gadget(&mut prover, alloc_scal, alloc_scal_inv).is_ok());`

The following are the constraints

`pub fn is_nonzero_gadget<CS: ConstraintSystem>(    cs: &mut CS,    x: AllocatedScalar,    x_inv: AllocatedScalar,) -> Result<(), R1CSError> {    let y: u32 = 1;    let x_lc: LinearCombination = vec![(x.variable, Scalar::one())].iter().collect();    let one_minus_y_lc: LinearCombination = vec![(Variable::One(), Scalar::from(1-y))].iter().collect();    let y_lc: LinearCombination = vec![(Variable::One(), Scalar::from(y))].iter().collect();    // x * (1-y) = 0    let (_, _, o1) = cs.multiply(x_lc.clone(), one_minus_y_lc);    cs.constrain(o1.into());    // x * x_inv = y    let inv_lc: LinearCombination = vec![(x_inv.variable, Scalar::one())].iter().collect();    let (_, _, o2) = cs.multiply(x_lc.clone(), inv_lc.clone());    // Output wire should have value `y`    cs.constrain(o2 - y_lc);    // Ensure x_inv is the really the inverse of x by ensuring x*x_inv = 1    let (_, x_inv_var, o3) = cs.multiply(x_lc, inv_lc);    // Output wire should be 1    let one_lc: LinearCombination = vec![(Variable::One(), Scalar::one())].iter().collect();    cs.constrain(o3 - one_lc);    Ok(())}`

Notice the first 2 constraints `cs.constrain(o1.into())` and `cs.constrain(o2 — y_lc)` correspond to the 2 equations above but there is a third constraint that checks whether `inv` is actually the inverse of `x`. This is necessary since the prover only gives the commitment of `x` and `inv` (`x`⁻¹) to the verifier and prover could cheat by not giving the inverse but some other value. So the verifier makes sure that `inv` is actually the inverse. The complete code is here.

## Set non-membership

`let mut comms: Vec<CompressedRistretto> = vec![];let mut diff_vars: Vec<AllocatedScalar> = vec![];let mut diff_inv_vars: Vec<AllocatedScalar> = vec![];let (com_value, var_value) = prover.commit(value.clone(), Scalar::random(&mut rng));let alloc_scal = AllocatedScalar {    variable: var_value,    assignment: Some(value),};for i in 0..set_length {    let elem = Scalar::from(set[i]);    let diff = elem - value;    let diff_inv = diff.invert();    // Take difference of set element and value, `set[i] - value`    let (com_diff, var_diff) = prover.commit(diff.clone(), Scalar::random(&mut rng));    let alloc_scal_diff = AllocatedScalar {        variable: var_diff,        assignment: Some(diff),    };    diff_vars.push(alloc_scal_diff);    comms.push(com_diff);    // Inverse needed to prove that difference `set[i] - value` is non-zero    let (com_diff_inv, var_diff_inv) = prover.commit(diff_inv.clone(), Scalar::random(&mut rng));    let alloc_scal_diff_inv = AllocatedScalar {        variable: var_diff_inv,        assignment: Some(diff_inv),    };    diff_inv_vars.push(alloc_scal_diff_inv);    comms.push(com_diff_inv);}assert!(set_non_membership_gadget(&mut prover, alloc_scal, diff_vars, diff_inv_vars, &set).is_ok());`

The variables corresponding to above commitments are then used in the following constraints

`pub fn set_non_membership_gadget<CS: ConstraintSystem>(    cs: &mut CS,    v: AllocatedScalar,    diff_vars: Vec<AllocatedScalar>,    diff_inv_vars: Vec<AllocatedScalar>,    set: &[u64]) -> Result<(), R1CSError> {    let set_length = set.len();    for i in 0..set_length {        // Take difference of value and each set element, `v - set[i]`        let elem_lc: LinearCombination = vec![(Variable::One(), Scalar::from(set[i]))].iter().collect();        let v_minus_elem = v.variable - elem_lc;        // Since `diff_vars[i]` is `set[i] - v`, `v - set[i]` + `diff_vars[i]` should be 0        cs.constrain(diff_vars[i].variable + v_minus_elem);        // Ensure `set[i] - v` is non-zero        is_nonzero_gadget(cs, diff_vars[i], diff_inv_vars[i])?;    }    Ok(())}`

Note that in the above constraints, apart from the non-zero constraints, there is additional constraint per set element. This constraint is needed to ensure that the prover uses the same `v` in `S[i] — v != 0` for each set index `i`. This is done by creating a variable for `v-S[i]` and adding it to above difference and constraining the result to 0. The complete code is here.

## Set membership proof

The prover first creates the bit-vector and commits to each bit.

`let bit_map: Vec<u64> = set.iter().map( | elem | {    if *elem == value { 1 } else { 0 }}).collect();let mut comms = vec![];let mut bit_vars = vec![];for b in bit_map {    let (com, var) = prover.commit(b.into(), Scalar::random(&mut rng));    let quantity = AllocatedQuantity {        variable: var,        assignment: Some(b),    };    assert!(bit_gadget(&mut prover, quantity).is_ok());    comms.push(com);    bit_vars.push(quantity);}`

To prove that some value is a bit the `bit_gadget` is used which is based on this relation `bit*(1-bit)=0`.

`pub fn bit_gadget<CS: ConstraintSystem>(    cs: &mut CS,    v: AllocatedQuantity) -> Result<(), R1CSError> {    let (a, b, o) = cs.allocate(|| {        let bit: u64 = v.assignment.ok_or(R1CSError::MissingAssignment)?;        Ok(((1 - bit).into(), bit.into(), Scalar::zero()))    })?;    // Variable b is same as v so b + (-v) = 0    let neg_v: LinearCombination = vec![(v.variable, -Scalar::one())].iter().collect();    cs.constrain(b + neg_v);    // Enforce a * b = 0, so one of (a,b) is zero    cs.constrain(o.into());    // Enforce that a = 1 - b, so they both are 1 or 0.    cs.constrain(a + (b - 1u64));    Ok(())}`

Note that `cs.constrain(b + neg_v)` is needed to ensure that the prover assigned the same value to variable `b` as committed in `v`.

The prover now ensures that there is only 1 bit set in the vector by summing the vector and comparing the result with 1.

`assert!(vector_sum_gadget(&mut prover, &bit_vars, 1).is_ok());`

The following is a vector sum gadget that can be used to compare the sum of a given vector to a given value.

`// Ensure sum of items of `vector` is `sum`pub fn vector_sum_gadget<CS: ConstraintSystem>(    cs: &mut CS,    vector: &[AllocatedQuantity],    sum: u64) -> Result<(), R1CSError> {    let mut constraints: Vec<(Variable, Scalar)> = vec![(Variable::One(), -Scalar::from(sum))];    for i in vector {        constraints.push((i.variable, Scalar::one()));    }    cs.constrain(constraints.iter().collect());    Ok(())}`

Note that the first term of linear combination `constraints` is negative `sum` and the sum of all terms of this linear combination is constrained to be 0.

Now the prover satisfies the final product relation `set[i] * bitvec[i] = bitvec[i] * v` by committing to the value and using already allocated variables for the committed bit-vector `bit_vars`.

`let (com_value, var_value) = prover.commit(value.into(), Scalar::random(&mut rng));let quantity_value = AllocatedQuantity {    variable: var_value,    assignment: Some(value),};assert!(vector_product_gadget(&mut prover, &set, &bit_vars, &quantity_value).is_ok());`

The `vector_product_gadget`

`// Ensure items[i] * vector[i] = vector[i] * valuepub fn vector_product_gadget<CS: ConstraintSystem>(    cs: &mut CS,    items: &[u64],    vector: &[AllocatedQuantity],    value: &AllocatedQuantity) -> Result<(), R1CSError> {    let mut constraints = vec![(value.variable, -Scalar::one())];    for i in 0..items.len() {        let (a, b, o) = cs.allocate(|| {            let bit: u64 = vector[i].assignment.ok_or(R1CSError::MissingAssignment)?;            let val = value.assignment.ok_or(R1CSError::MissingAssignment)?;            Ok((items[i].into(), bit.into(), (bit*val).into()))        })?;        constraints.push((o, Scalar::one()));        let item_var: LinearCombination = vec![(Variable::One(), items[i].into())].iter().collect();        cs.constrain(a - item_var);        // Each `b` is already constrained to be 0 or 1    }    // Constrain the sum of output variables to be equal to the value of committed variable    cs.constrain(constraints.iter().collect());    Ok(())}`

Notice the constraint `cs.constrain(a — item_var)`. The verifier ensures that the value assigned by the prover to variable `a` is equal to value of the set item at that index. The complete code is here.
There is an alternate way of proving set membership. It relies on this idea: If an element is present in the set, then the vector constructed by taking the difference of each set item and this element will contain 1 zero value. So if we multiply all elements of this new vector, the product will be 0. The prover commits to the value and its difference with each set item and calls the new set membership gadget `set_membership_1_gadget`

`let (com_value, var_value) = prover.commit(value.clone(), Scalar::random(&mut rng));let alloc_scal = AllocatedScalar {    variable: var_value,    assignment: Some(value),};comms.push(com_value);for i in 0..set_length {    let elem = Scalar::from(set[i]);    let diff = elem - value;    // Take difference of set element and value, `set[i] - value`    let (com_diff, var_diff) = prover.commit(diff.clone(), Scalar::random(&mut rng));    let alloc_scal_diff = AllocatedScalar {        variable: var_diff,        assignment: Some(diff),    };    diff_vars.push(alloc_scal_diff);    comms.push(com_diff);}assert!(set_membership_1_gadget(&mut prover, alloc_scal, diff_vars, &set).is_ok());`

In the `set_membership_1_gadget`, the product of elements of `diff_vars` is constrained to be 0. The complete code is here.

`pub fn set_membership_1_gadget<CS: ConstraintSystem>(    cs: &mut CS,    v: AllocatedScalar,    diff_vars: Vec<AllocatedScalar>,    set: &[u64]) -> Result<(), R1CSError> {    let set_length = set.len();    // Accumulates product of elements in `diff_vars`    let mut product: LinearCombination = Variable::One().into();    for i in 0..set_length {        // Take difference of value and each set element, `v - set[i]`        let elem_lc: LinearCombination = vec![(Variable::One(), Scalar::from(set[i]))].iter().collect();        let v_minus_elem = v.variable - elem_lc;        // Since `diff_vars[i]` is `set[i] - v`, `v - set[i]` + `diff_vars[i]` should be 0        cs.constrain(diff_vars[i].variable + v_minus_elem);        let (_, _, o) = cs.multiply(product.clone(), diff_vars[i].variable.into());        product = o.into();    }    // Ensure product of elements if `diff_vars` is 0    cs.constrain(product);    Ok(())}`

Written by

## Coinmonks

#### Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project — https://coincodecap.com

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just \$5/month. Upgrade