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 , then if and only if .
In our code above is a binary value. It's value is either or . We make use of this fact by the following:
- when . If then the expression is .
So we can rewrite
foo(w, a, b) as the mathematical function
We now can convert this expression to a constraint system.
ZK statements take the form of:
More succinctly as:
These statements are converted into polynomials of the form:
is the target polynomial and in our case will be . is the cofactor polynomial. The statement says that the polynomial has roots (is equal to zero) at the points when .
Earlier we wrote our mathematical statement which we will now convert to constraints.
Rearranging the equation, we note that:
Swapping and rearranging, our final statement becomes . Represented in ZK as:
The last line is a boolean constraint that is either or by enforcing that (re-arranged this is ).
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 (line 1), (line 2) and (line 3).
Each one of , and is supplied a list of (constant coefficient, variable value) pairs.
In bellman library, the constant is a fixed value of type
The variable is a type called
Variable. These are the values fed
lc0 (the 'left' polynomial),
lc1 (the 'right' polynomial),
lc2 (the 'out' polynomial).
In our example we had a function where for example .
The verifier does not know the variables ,
and which are allocated by the prover as variables. However
the verifier does know the coefficients (which are of the
type) shown in the table above. In our example they only either
or , 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 to
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
, getting back
Variable objects which we then add to
the left lc, right lc or output lc.