Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?

Proving gadgets

This is a collection of fun algebraic tricks to prove various boolean and arithmetic statements inside zero knowledge proofs.

We are going to use Bulletproofs interface, but won't go into detail how Bulletproofs actually work.

Bulletproofs interface

Bulletproofs is a framework to create arbitrary proofs using a "Rank-1 Constraint System" interface. In simple terms, "rank-1" means that in our system we can express statements where secret values ("variables") can be added and multiplied.

All the arithmetic is done modulo group order q. So all additions and multiplications wrap around over some large ≈256-bit integer q.

Using these two operations (addition and multiplication) we can express "constraints": requirements that the secret values must satisfy.

Linear constraints: a set of statements "sum of secrets weighted by non-secret integers equals some non-secret integer"

Multiplicative constraints: multiplication of two variables is equal to some other secret variable. These are also called "multiplication gates".

How do they look like? Let's say we have a statement (2x + y)*z == 100, where letter indicate secret numbers.

To represent it in Bulletproofs we need one multiplier and three linear constraints:

# Multiplication gate:
a*b == c

# Linear constraints:
2x + y - a == 0   # left input of the multiplier is 2x+y
z - b == 0        # right input of the multiplier is z
c == 100          # output of the multiplier is 100

Notice that each secret can be weighted by a non-secret integer. In the example above we assign weight 2 to x and weight 1 to y and z.

We can represent secrets in two ways:

High-level variables: those are individual numbers encrypted using Pedersen commitments. You use these for various "external facts". E.g. if you want to prove something about a payment amount, then the amount (A) and the currency (C) would be represented as two high level variables A and C.

Low-level variables: those are simply inputs and outputs of the "multiplication gates". These are also encrypted, but in bulk, so they occupy very small and fixed space in the proof.

Bulletproofs also permit generating constraints on the fly, so we can use not just constants for weights, but also random challenges: when the weight is generated pseudo-randomly as a hash of all the previously committed secrets. This feature allows us to express some constraints very efficiently.

Examples

Equality check

Expression X == Y is very simple: it's just a single linear constraint X - Y == 0.

Inequality check

Expression X ≠ Y is a bit tricky. Let's rephrase it as X-Y ≠ 0 and look at the following constraint: (X-Y)*W == 1.

To make the statement compatible with the logical operators, let's rephrase it as (X-Y)*W - 1 == 0.

From the perspective of the verifier, the additional secret variable W may have any value, and the constraint would not be satisfied if either term is zero.

So the prover must use secrets X≠Y and also use the inverse of their difference as W: W = (X-Y)^-1 mod q.

The constraint system looks like this:

# One multiplier:
a*b==c

# Linear constraints:
X-Y-a = 0
c = 1

We do not need constrain b to anything: it is indirectly constrained to be the inverse of a because c is constrained to be 1.

Logical OR

Let's say we have a collection of expressions in the form "must equal zero", and we need one of them to be true: A = 0 || B == 0 || C == 0.

This can easily be expressed as a multiplicative constraint: A*B*C == 0. In general, for N statements we'd need N-1 multipliers.

Logical AND

Let's say we have a collection of expressions in the form "must equal zero", that all need to be true simultaneously: A = 0 && B == 0 && C == 0.

Construct the polynomial over an additional non-secret variable: A + x*B + (x^2)*C. In other words, we'd use every statement in canonical form as a term of the polynomial. Then, if all statements are true, then the polynomial will be zero for all values of x.

The cryptographic trick then, is to make the prover commit to the values A, B, C and then sample a random value of x using a hash function. If the prover was dishonest, they have a negligible chance that x falls on the root of the polynomial and satisfies the check. Therefore, the verifier is easily convinced that, if for random value of x the polynomial evaluates to zero, then the original statements were correct.

The constraint system in such case uses just one linear constraint, where cleartext weights on secrets A, B and C are powers (0,1,2) of the non-secret random number x.

Logical NOT

Say, you have an arithmetized statement "X = 0" and you need a statement "Y = 0" to be true when "X ≠ 0". For this we'd need a trick similar to "not equals" constraint, but make it composable with other logical operations (AND, OR).

This uses two multipliers:

X*Y == 0       # either X or Y is 0
X*W == 1 - Y   # if X = 0, Y must be 1; if Y = 0, X must be non-zero.

Right wire W is freely chosen by the prover. If X is non-zero (the original statement X==0 is false), then W must be set to its inverse, and Y must be 0, making the statement Y==0 true. If the original statement is true (X==0), then Y must be assigned 1, and W can be assigned an arbitrary value. The resulting statement Y==0 is then false.

Set membership

To prove that an integer X belongs to a set of (possibly secret) integers {a, b, c...}, use the statement about a polynomial, where the roots are formed by the set:

(x - a) * (x - b) * (x - c) * ... == 0

This requires N-1 multiplication gates.

Set equality / Shuffling / Sorting / Permutation proof

To prove that two lists of numbers {a0, a1, a2...} and {b0, b1, b2, ...} are equal up to a permutation (in order to shuffle secret list randomly, or sort it by some criteria), use equality of two polynomials sampled by a random challenge x:

(x-a0)*(x-a1)*(x-a2)*... == (x-b0)*(x-b1)*(x-b2)*...

The challenge x is a cleartext value, sampled randomly after the input lists are committed.

The proof requires 2*(N-1) multiplication gates, where N is the size of each list.

Tuple compression

To use tuples of numbers in the proofs about sets and lists, they must be compressed in single integers. This can be done with the same trick as logical AND described above:

Commit each variable in a tuple (a,b,c) and sample a random challenge x. Then, form a polynomial a + b*x + c*x^2 using the tuple members as terms.

If two compressed tuples (using the same challenge) are equal, it means that the probability that the original tuples are equal is overwhelmingly high. Obviously, if the tuples are different, then the resulting evaluations are also overwhelmingly likely to be different.

Bits

To perform bitwise operations we need to prove that a number is, in fact, a bit (zero or one). Like a boolean OR, it is done with a multiplicative constraint:

X = 0 || X = 1    =>  X * (X-1) == 0

Bitwise NOT

If we know that a variable X is in range {0,1}, its negation Y is a linear constraint Y = 1-X.

Bitwise AND

If we know that two variables contain values in range {0,1}, expressing their bitwise AND is really simple:

Z == X*Y  #  if either is 0, the Z is zero, otherwise Z = 1*1 = 1

Note: this spends one multiplier while boolean AND does not. This is because this also guarantees that Z will be in {0,1} as a result of the operation, not simply checks whether one of the input bits is set.

Bitwise OR

This can be constructed using negations and bitwise AND:

Z = X | Y   =>  1-Z == (1-X)*(1-Y)

Binary decomposition

To break the number into N individual bits, one needs N multipliers, for each bit, and a linear constraint to add all the bits to a given number:

bit_0 * (1-bit_0) == 0
...
bit_k * (1-bit_k) == 0

bit_0 + bit_1*2 + bit_2*(2^2) + ... + bit_k * (2^k) - X == 0

This also works as a simple range proof, where one needs to prove that a number is in range [0, 2^n).

Arbitrary range proof

To prove that X is in range [min, max], we can simply do two proofs that X-min in [0, 2^n] and max-X in [0, 2^n]. Where n is rounded up log2(max-min).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment