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