Technical Design: Prover

The Valida zk-VM has various parameters, including but not limited to: the base finite field, the extension field which challenges are drawn from, the polynomial commitment scheme, the challenger implementation, and the set of chips.

The prover first needs to run the program and generate execution traces: one execution trace per chip. These execution traces are encoded as univariate polynomials over a finite field, as are any preprocessed execution traces (i.e., traces whose contents are known at chip definition time). The polynomials encoding the execution traces are generated by Barycentric Lagrange interpolation, with the X coordinates used in this interpolation being the multiplicative subgroup generated by a primitive root of unity. Call that primitive root of unity ω. Commitments to these polynomials are generated, as well as these polynomials with their inputs shifted by one (i.e., multiplied by ω). Next, the prover generates and commits to trace polynomials for the permutation argument, as well as these polynomials with their inputs shifted by one.

The goal of the Valida proof is to show that the execution trace is valid. This goal is expressed as a finite set of polynomial functions of the trace polynomials, each of which must be equal to zero for the execution trace to be valid, such that if all of them are equal to zero for the trace polynomials of a particular trace, then that execution trace is valid. These polynomial functions of the trace polynomials are called the polynomial constraints.

The trace polynomials are plugged into the polynomial constraints, resulting in a collection of univari6 ate polynomials. A linear combination is taken of these polynomials, with the coefficients being successive powers of a challenge value. The goal is then to show that this linear combination, this univariate polynomial, call it P(x), is equal to zero whenever x is in the multiplicative subgroup of the finite field generated by the aforementioned primitive root of unity, ω. If this is true, then with high probability, the polynomial constraints are satisfied (i.e., equal to zero in this case). In other words, the goal is to show that P(x) is divisible by Z(x), where Z(x) is the zerofier polynomial of the subgroup generated by ω, or in other words Z(x) is the product of the set of monomials of the form (x − ω^i), for i an integer. Since the subgroup generated by ω is a subgroup of a finite field, it is finite, and Z(x) is well defined this way as a finite product of monomials.

The prover computes the quotient Q(x) = P(x) / Z(x) . The prover commits to Q(x). The prover generates succinct proofs of the evaluations of the trace polynomials and Q(x) at a challenge point α. The verifier will later use these evaluations to check the equation P(x) = Q(x) × Z(x).

There is one sub-argument of the proof for each chip. This process is repeated for each sub-argument of the proof: plugging the trace polynomials into the polynomial constraints, taking a linear combination, taking a quotient by the zerofier polynomial, committing to the linear combination and quotient polynomial, and proving the openings at a challenge point.

The proof output by the prover consists of all of the challenges, commitments to the execution trace polynomials, commitments to the preprocessed trace polynomials, commitments to the permutation trace polynomials, commitments to all of the aforementioned polynomials shifted by one row, commitments to the quotient polynomials, evaluations of all of the aforementioned polynomials at the challenge point α, and proofs of those evaluations.

The Valida verifier recomputes the commitments to the preprocessed traces. (This verifier step can be avoided easily enough by moving this step to the setup phase.) The verifier recomputes the permutation argument challenges and the challenge α. The verifier verifies the proofs of the evaluations of the committed polynomials at α. The verifier verifies that P(α) = Q(α)×Z(α). The verifier verifies that the permutation argument is satisfied by checking that the sum of the cumulative sums of the linear combinations of permutation trace rows is equal to zero.

Permutation Arguments

The goal of the Valida permutation arguments is to show that in a trace of interactions between chips, there is a one to one correspondence between sends and receives: that is, everything sent is received, and everything received is sent. A Valida permutation argument takes as input a permutation trace. A permutation trace contains whatever values are sent and received by the interactions being checked in the permutation argument: call these columns “the interaction trace.” A permutation trace consists of its interaction trace, and some additional columns containing values derived from the interaction trace.

In a Valida permutation argument, the prover takes the multiplicative inverse of a linear combination of the elements of each row of each interaction in the interaction trace. The coefficients of these linear combinations are generated from challenges. As a result, each row is reduced to one nonzero field element. The coefficients of the linear combinations are devised such that a send and a receive will be reduced to each other’s additive inverses, meaning they sum to zero. As a result, if the sends and receives are correctly in a one to one correspondence, then the sum of all of the multiplicative inverses of linear combinations of the interaction rows will be equal to zero. The permutation argument essentially works by checking this, based on the premise that if the sum of the multiplicative inverses of linear combinations of the interaction rows is zero, then probably, the sends and receives are correctly in a one to one correspondence.

The derived columns of permutation trace hold the multiplicative inverses of the linear combinations of the interaction rows (one column per interaction). The final derived column of the permutation trace is a running sum column, which is used to check that the sum of the multiplicative inverses of the linear combinations of the interaction rows is zero.

Each permutation argument has reciprocal constraints, which check that the derived values of the multiplicative inverses of linear combinations of interaction rows are in fact the multiplicative inverses of the appropriate linear combinations. These have the effect that all of the linear combinations of interaction rows are constrained to be non-zero. The value of the running sum column is constrained to be equal to its previous value plus the multiplicative inverses of linear combinations on the current row, for every row except the first row. On the first row and the last row, the running sum is expected to be zero.

Permutation arguments can also be used to check an interaction of a chip with itself: a so-called local interaction. Currently this only occurs in the argument for the memory chip.

Challenges

Challenges are pseudo-randomly chosen elements of a finite field. The process of selecting challenges is deterministic: given the same input data, the same challenges will result. The input data which is used to select each challenge needs to be carefully chosen. If this is not done, it may compromise the soundness of the proof system. The Fiat-Shamir heuristic describes how to choose the input data used to select each challenge. Basically, each challenge in the proof needs to depend on all of the public inputs to the prover, and all of the elements of the proof up to but not including that challenge.

In order to check that the prover correctly generated each challenge, the verifier re-generates each challenge, by following the same process the prover followed to generate the challenges, using the inputs provided by the prover in the proof. This is why the process of selecting the challenges needs to be deterministic and can only depend on information provided to the verifier. The verifier needs to check that the prover followed the prescribed process to pick the challenges, because otherwise the prover could try to pick a special challenge which results in the prover being able to trick the verifier into accepting a proof of a false statement.

Polynomial commitment schemes

In general, a commitment scheme is a protocol for reducing a piece of information to a fingerprint (called a commitment), and proving facts about the underlying information used to generate the commitment, typically without revealing the underlying information. The latter step, which proves facts about the committed information, is called an “opening proof.”

In a polynomial commitment scheme (PCS), the committed pieces of information are polynomials or collections of polynomials. Valida specifically uses univariate polynomial commitment schemes, where the committed pieces of information are univariate polynomials with coefficients drawn from a finite field. The opening proofs in a polynomial commitment scheme prove the evaluations of the committed polynomial(s) at specified point(s).

The Valida zk-VM is polymorphic in the PCS. By default, Valida uses a FRI PCS. This is a polynomial commitment scheme for polynomials over a 2-adic field, which is based on the Fast Reed-Solomon IOP of Proximity (FRI). There was some experimenting with using a Brakedown PCS early on. This results in more efficient proving, but substantially larger proofs. Using a FRI-PCS seems to strike a good balance between proving efficiency and succinctness.