darkfi/doc/src/crypto/zk_explainer.md

Zero-knowledge explainer

We start with this algorithm as an example:

def foo(w, a, b):
    if w:
        return a * b
    else:
        return a + b

ZK code consists of lines of constraints. It has no concept of branching conditionals or loops.

So our first task is to flatten (convert) the above code to a linear equation that can be evaluated in ZK.

Consider an interesting fact. For any value \mathbb{x}, then (1 - w) = 0 if and only if x = 1.

In our code above w is a binary value. It's value is either 1 or 0. We make use of this fact by the following:

1. w = 1 when w = 1
2. (1 - w) = 1 when w = 0. If w = 1 then the expression is 0.

So we can rewrite foo(w, a, b) as the mathematical function

f(w, a, b) = w(ab) + (1 - w)(a + b)

We now can convert this expression to a constraint system.

ZK statements take the form of:

(c_{l,1} \cdot v_{l,1} + c_{a,2} \cdot v_{l,2} + \dots) \times (c_{b,1} \cdot v_{r,1} + c_{b,2} \cdot v_{r,2} + \dots) = (c_{o,1} \cdot v_{o,1} + c_{o,2} v_{o,2} + \dots)

More succinctly as:

\sum_{i = 1}^n c_{l,i} \cdot v_{l,i} \times \sum_{i = 1}^n c_{r,i} v_{r, i} = \sum_{i = 1}^n c_{o, i} v_{o, i}

These statements are converted into polynomials of the form:

L(x) \times R(x) - O(x) = t(x)h(x)

t(x) is the target polynomial and in our case will be (x - 1)(x - 2)(x - 3). h(x) is the cofactor polynomial. The statement says that the polynomial L(x) \times R(x) - O(x) has roots (is equal to zero) at the points when x \in {1, 2, 3}.

Earlier we wrote our mathematical statement which we will now convert to constraints.

f(w, a, b) = w(ab) + (1 - w)(a + b)

Rearranging the equation, we note that:

v = w(ab) + (1 - w)(a + b) = w(ab) + a + b - w(a + b)

Swapping and rearranging, our final statement becomes w(ab - a - b) = v - a - b. Represented in ZK as:

ab = m w(m - a - b) = v - a - b w^2 = w

The last line is a boolean constraint that w is either 0 or 1 by enforcing that w(w - 1) = 0 (re-arranged this is w \cdot w = w).

Line	L(x)	R(x)	O(x)
1	(1\cdot a)	(1 \cdot b)	(1 \cdot m)
2	(1 \cdot w)	(1 \cdot m + (-1) \cdot a + (-1) \cdot b)	(1 \cdot v + (-1) \cdot a + (-1) \cdot b)
3	(1 \cdot w)	(1 \cdot w)	(1 \cdot w)

Because of how the polynomials are created during the setup phase, you must supply them with the correct variables that satisfy these constraints, so that L(1) \times R(1) - O(1) = 0 (line 1), L(2) \times R(2) - O(2) = 0 (line 2) and L(3) \times R(3) - O(3) = 0 (line 3).

Each one of L(x), R(x) and O(x) is supplied a list of (constant coefficient, variable value) pairs.

In bellman library, the constant is a fixed value of type Scalar. The variable is a type called Variable. These are the values fed into lc0 (the 'left' polynomial), lc1 (the 'right' polynomial), and lc2 (the 'out' polynomial).

In our example we had a function f(w, a, b) where for example f(1, 4, 2) = 8. The verifier does not know the variables w = 1, a = 4 and b = 2 which are allocated by the prover as variables. However the verifier does know the coefficients (which are of the Scalar type) shown in the table above. In our example they only either 1 or -1, but can also be other constant values.

pub struct LinearCombination<Scalar: PrimeField>(Vec<(Variable, Scalar)>);

It is important to note that each one of the left, right and out registers is simply a list of tuples of (constant coefficient, variable value).

When we wish to add a constant value, we use the variable called ~one (which is always the first automatically allocated variable in bellman at index 0). Therefore we end up adding our constant c to the LinearCombination as (c, ~one).

Any other non-constant value, we wish to add to our constraint system must be allocated as a variable. Then the variable is added to the LinearCombination. So in our example, we will allocate w, a, b, m, v, getting back Variable objects which we then add to the left lc, right lc or output lc.