Components of a proof system
Last updated
Was this helpful?
Last updated
Was this helpful?
Arithmetization is the process of turning a generic statement or question into a set of equations to be verified or solved.
Consider the following statement: “I am twice older than my youngest sibling”.
Can we write this mathematically? Let’s write a1, a2 ,…,an the ages of the siblings and x the age of the claimant. We can now rewrite the statement as: x=2∗min(a1, a2, …, an)
To verify the original statement for Alice (8) and her siblings Bob (9) and Charlie (4), we can just plug in the values to our equation.
We evaluate each side and determine whether the equation holds: if it holds the statement was true, if it does not the statement was false.
With this set of mathematical constraints, a verifier can run a small number of algebraic checks to show with high probability that the prover is not lying.
A “good” arithmetization is one in which the final mathematical expressions can be evaluated with minimal effort (computation). While our example was trivial, the process of arithmetization becomes more complex for abstract statements such as: “I have correctly shuffled a deck of cards” or “I know a secret value x such that running a public program P with x as input will output the public value y”.
Circuit constructions are utilized because they can easily be used for probabilistic checks by a verifier to ensure that the computations were correctly run. Because circuits can be defined as a series of polynomials, which are required for probabilistic checks, they have become the standard way to construct ZK proofs.
In order to visualize how a program could be turned into a circuit, we can take the following example. Imagine we have a variable in and want to check if in is equal to either 10, 15, or 25 and if so, return 1, otherwise return 0. Some pseudocode for this would look like:
In order to do the same thing in an arithmetic circuit, we can express this as an equation
(in - 10)(in - 15)(in - 25) ?= 0.
Essentially, what’s happening here is that the left hand side of the equation will evaluate to 0 if in is 10, 15, or 25, and nonzero otherwise. The isZero component is a circuit that returns 1 if its input is equal to 0, and 0 otherwise.
One way of displaying arithmetic circuits is the Rank-1 Constraint System, or R1CS.
By taking a circuit and transforming it into a series of matrices and vectors, we can eventually feed this into any proof system that supports R1CS to generate a zkSNARK.
To get an R1CS, we have to “flatten” our circuit into a series of mathematical constraints of the form left * right = output, or equivalently left * right — output = 0, where left is the left wire of an arithmetic circuit gate, right is the right wire, and output is the output wire.
