# Zero knowledge proofs using Bulletproofs

*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

I assume that you are already familiar with utilizing arithmetic circuits for proving arbitrary statements. It has been described in several papers but the library this post talks about it built on the paper “Efficient zero-knowledge arguments for arithmetic circuits in the discrete log setting”. The technique was made more efficient by the Bulletproofs paper and dalek-cryptography published their implementation of this. The idea is to represent the statement as an arithmetic circuit, i.e a set of equations where the allowed operators are addition, subtraction and multiplication and convert these equations to a Rank-1 Constraint System (R1CS). A constraint system is a collection of arithmetic constraints over a set of variables. To understand more about this process and R1CS, see this post. Proving systems utilizing R1CS have gained popularity recently, ZK-SNARKs being the most popular one. The disadvantage of ZK-SNARKs is the presence of a trusted setup, i.e one time generation of protocol parameters which involves knowledge of or learning of some secrets that can be used to break the guarantees of the protocol. This is challenging as now the setup has to be done in such a way that such secrets cannot be learned (completely), Zcash does it using a multi-party computation. Another challenge is the trusted setup has to be done for each circuit, eg. if you want to prove knowledge of 2 factors then you do a trusted setup. Now if you have to prove knowledge of 3 factors, you have to do the trusted setup again since the constraints have changed. The R1CS system built with Bulletproofs does not have a trusted setup and hence the above 2 problems are avoided.

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

Let’s explore the Bulletproofs API in the context of an example. Let’s say the prover wants to prove the knowledge of factors of a public number `r`

The prover knows the factors `p`

and `q`

but the verifier does not. Thus the prover will create proof for the statement `p * q = r`

where `r`

is known by both prover and verifier but `p`

and `q`

are known only to the prover.

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

represents the linear constraint with value equal to *One*(), r.into())`r`

, i.e. multiply the variable with value 1 (`Variable::`

) with the scalar *One*()`r`

. If the prover wanted to create a variable with value p+q+r, he could create by `vec![(Variable::`

or by *One*(), (p+q+r).into())]`vec![(Variable::`

the terms of the vector are added.*One*(), p.into()), (Variable::*One*(), q.into()), (Variable::*One*(), r.into())]

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

**Range proof**To prove that a committed value

`x`

satisfies *min ≤ x ≤ max*for some public

`min`

and `max`

, the prover has to satisfy 2 statements, *x ≥ min*and

*x ≤ max*.

*x ≥ min*is equivalent to proving

*x - min ≥ 0*and

*x ≤ max*is equivalent to proving

*max - x ≥ 0*. Now if the prover that for some committed

`v`

, `v`

≥ 0, he can prove both *x - min ≥ 0*and

*max - x ≥ 0*and giving commitements to

*x - min*and

*max - x.*Lets focus on proving

`v`

≥ 0 and less than the maximum allowed value to avoid overflows for some committed `v`

, i.e. `v`

in *[0, MAX_VALUE]*. If the prover created a bit-representation of

`v`

and the bit-representation contained `n`

bits, its clear that `v`

is in [0, 2ⁿ). Once the prover creates this `n`

-bit vector, it still cannot reveal this bit-vector to verifier since that will `v`

to the verifier. But if the prover can prove to the verifier that each element of this vector is indeed a bit and the bits are set at the “right index”, it can convince the verifier that `v`

is in the range.Say the n-bit vector is [bₙ₋₁, bₙ₋₂, …b₁, b₀]. To prove each bᵢ is a bit, it is sufficient to prove bᵢ*(1-bᵢ)=0. The following snippet shows this idea

`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

Frequently there is a need to prove that some value is non-zero without revealing it but only committing to it, we will see its usage in the proof of set non-membership below. Another usage is proving some value is not equal to a certain value since to prove `x`

is not equal to `c`

, it is sufficient to prove that `x-c`

is not equal to 0.

The proof is based on the following observation (not mine). Say you want to prove `x`

not equal to 0. Calculate inverse of `x`

, call it `inv`

. Let `y = if x!=0 then 1 else 0`

. `inv`

= 0 when `x`

=0 else `inv`

=`x`

⁻¹. Now the following 2 equations hold

i) x*(1-y) = 0

ii) x*inv = y

The prover first commits to both `x`

and its inverse `inv`

and then satisfies the above 2 constraints.

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

Proving that your value `v`

is not equal to a given `c`

is same as proving that `v — c != 0`

. So we utilize the above `is_nonzero_gadget`

. The complete code is here.

## Set non-membership

The prover might need to prove that his committed value does not lie in a set, eg. Say there is a public set `S`

as [2, 9, 78, 44, 55] and prover’s committed value `v`

is 12, he does not want the verifier to know that his value is 12 but only that his value is not in the set. The idea is that the prover can subtract his value from each set element and prove that each result is non-zero, i.e `S[i] — v != 0`

for each set index `i`

. So the prover first commits to his value, then commits to the difference of each set element and his value and also to the inverse of each difference, `2*n+1`

commitments in total where `n`

is number of elements in the set. The commitment to the inverse of the difference is needed to prove that the difference is *non-zero* as shown in previous example.

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 might need to prove that his committed value lies in a set `S`

but without revealing his value `v`

. This is the idea (taken from ethsnarks repo)

1. Prover creates a bit-vector corresponding to the set with 1 bit per element of the set. All bits are 0.

2. Prover sets the bit in the bit-vector at the index of his value `v`

. eg. if set `S`

was [5, 9, 1, 100, 200] and prover’s value was 100, the bit-vector will be [0, 0, 0, 1, 0].

3. Prover then proves that

i) each element of the bit-vector is in-fact a bit,

ii) there is only 1 bit set in the bit vector by adding all the bits and proving the sum is 1.

iii) for each set index `i`

, this relation holds `set[i] * bitvec[i] = bitvec[i] * v`

. This should hold since `bitvec[i]`

is 0 for all `i`

except the index of `v`

.

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*(())

}