Zero knowledge proofs using Bulletproofs

Lovesh Harchandani
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.

The code in this post has been refactored, updated with more examples and moved to a new repo.

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 duringcommit.

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 ith 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.

Proof that a committed value is not equal to a given value

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] * value
pub 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(())
}

Coinmonks

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

Lovesh Harchandani

Written by

Coinmonks

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