Contiguity of Memory-Pointer Regions
Contiguity for Op Stack Table
In each cycle, the memory pointer for the Op Stack Table, op_stack_pointer
, can only ever increase by one, remain the same, or decrease by one.
As a result, it is easy to enforce that the entire table is sorted for memory pointer using one initial constraint and one transition constraint.
- Initial constraint:
op_stack_pointer
starts with 161, so in terms of polynomials the constraint isop_stack_pointer - 16
. - Transition constraint: the new
op_stack_pointer
is either the same as the previous or one larger. The polynomial representation for this constraint is(op_stack_pointer' - op_stack_pointer - 1) · (op_stack_pointer' - op_stack_pointer)
.
Contiguity for Jump Stack Table
Analogously to the Op Stack Table, the Jump Stack's memory pointer jsp
can only ever decrease by one, remain the same, or increase by one, within each cycle. As a result, similar constraints establish that the entire table is sorted for memory pointer.
- Initial constraint:
jsp
starts with zero, so in terms of polynomials the constraint isjsp
. - Transition constraint: the new
jsp
is either the same as the previous or one larger. The polynomial representation for this constraint is(jsp' - jsp - 1) * (jsp' - jsp)
.
Contiguity for RAM Table
The Contiguity Argument for the RAM table establishes that all RAM pointer regions start with distinct values. It is easy to ignore consecutive duplicates in the list of all RAM pointers using one additional main column. This allows identification of the RAM pointer values at the regions' boundaries, . The Contiguity Argument then shows that the list contains no duplicates. For this, it uses Bézout's identity for univariate polynomials. Concretely, the prover shows that for the polynomial with all elements of as roots, i.e., and its formal derivative , there exist and with appropriate degrees such that In other words, the Contiguity Argument establishes that the greatest common divisor of and is 1. This implies that all roots of have multiplicity 1, which holds if and only if there are no duplicate elements in list .
The following columns and constraints are needed for the Contiguity Argument:
- Main column
iord
and two deterministic transition constraints enable conditioning on a changed memory pointer. - Main columns
bcpc0
andbcpc1
and two deterministic transition constraints contain and constrain the symbolic Bézout coefficient polynomials' coefficients. - Auxiliary column
rpp
is a running product similar to that of a conditioned permutation argument. A randomized transition constraint verifies the correct accumulation of factors for updating this column. - Auxiliary column
fd
is the formal derivative ofrpp
. A randomized transition constraint verifies the correct application of the product rule of differentiation to update this column. - Auxiliary columns
bc0
andbc1
build up the Bézout coefficient polynomials based on the corresponding main columns,bcpc0
andbcpc1
. Two randomized transition constraints enforce the correct build-up of the Bézout coefficient polynomials. - A terminal constraint takes the weighted sum of the running product and the formal derivative, where the weights are the Bézout coefficient polynomials, and equates it to one. This equation asserts the Bézout relation.
The following table illustrates the idea. Columns not needed for establishing memory consistency are not displayed.
ramp | iord | bcpc0 | bcpc1 | rpp | fd | bc0 | bc1 |
---|---|---|---|---|---|---|---|
0 | |||||||
0 | |||||||
0 | |||||||
0 | |||||||
- |
The values contained in the auxiliary columns are undetermined until the verifier's challenge is known; before that happens it is worthwhile to present the polynomial expressions in , anticipating the substitution . The constraints are articulated relative to α
.
The inverse of RAMP difference iord
takes the inverse of the difference between the current and next ramp
values if that difference is non-zero, and zero else. This constraint corresponds to two transition constraint polynomials:
(ramp' - ramp) ⋅ ((ramp' - ramp) ⋅ iord - 1)
iord ⋅ (ramp' - ramp) ⋅ iord - 1)
The running product rpp
starts with initially, which is enforced by an initial constraint.
It accumulates a factor in every pair of rows where ramp ≠ ramp'
. This evolution corresponds to one transition constraint: (ramp' - ramp) ⋅ (rpp' - rpp ⋅ (α - ramp')) + (1 - (ramp' - ramp) ⋅ di) ⋅ (rpp' - rp)
Denote by the polynomial that accumulates all factors in every pair of rows where .
The column fd
contains the “formal derivative” of the running product with respect to .
The formal derivative is initially , which is enforced by an initial constraint.
The transition constraint applies the product rule of differentiation conditioned upon the difference in ramp
being nonzero; in other words, if then the same value persists; but if then is mapped as
This update rule is called the product rule of differentiation because, assuming , then
The transition constraint for fd
is (ramp' - ramp) ⋅ (fd' - rp - (α - ramp') ⋅ fd) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (fd' - fd)
.
The polynomials and are the Bézout coefficient polynomials satisfying the relation The prover finds and as the minimal-degree Bézout coefficients as returned by the extended Euclidean algorithm. Concretely, the degree of is smaller than the degree of , and the degree of is smaller than the degree of .
The (scalar) coefficients of the Bézout coefficient polynomials are recorded in main columns bcpc0
and bcpc1
, respectively.
The transition constraints for these columns enforce that the value in one such column can only change if the memory pointer ramp
changes.
However, unlike the conditional update rule enforced by the transition constraints of rp
and fd
, the new value is unconstrained.
Concretely, the two transition constraints are:
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc0' - bcpc0)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc1' - bcpc1)
Additionally, bcpc0
must initially be zero, which is enforced by an initial constraint.
This upper-bounds the degrees of the Bézout coefficient polynomials, which are built from main columns bcpc0
and bcpc1
.
Two transition constraints enforce the correct build-up of the Bézout coefficient polynomials:
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc0' - bc0) + (ramp' - ramp) ⋅ (bc0' - α ⋅ bc0 - bcpc0')
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc1' - bc1) + (ramp' - ramp) ⋅ (bc1' - α ⋅ bc1 - bcpc1')
Additionally, bc0
must initially be zero, and bc1
must initially equal bcpc1
.
This is enforced by initial constraints bc0
and bc1 - bcpc1
.
Lastly, the verifier verifies the randomized AIR terminal constraint bc0 ⋅ rpp + bc1 ⋅ fd - 1
.
Completeness.
For honest provers, the gcd is guaranteed to be one. As a result, the protocol has perfect completeness.
Soundness.
If the table has at least one non-contiguous region, then and share at least one factor. As a result, no Bézout coefficients and can exist such that . The verifier therefore probes unequal polynomials of degree at most , where is the length of the execution trace, which is upper bounded by . According to the Schwartz-Zippel lemma, the false positive probability is at most .
Zero-Knowledge.
Since the contiguity argument is constructed using only AET and AIR, zero-knowledge follows from Triton VM's zk-STNARK engine.
Summary of constraints
We present a summary of all constraints.
Initial
bcpc0
bc0
bc1 - bcpc1
fd - 1
rpp - (α - ramp)
Consistency
None.
Transition
(ramp' - ramp) ⋅ ((ramp' - ramp) ⋅ iord - 1)
iord ⋅ ((ramp' - ramp) ⋅ iord - 1)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc0' - bcpc0)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc1' - bcpc1)
(ramp' - ramp) ⋅ (rpp' - rpp ⋅ (α - ramp')) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (rpp' - rpp)
(ramp' - ramp) ⋅ (fd' - rp - (α - ramp') ⋅ fd) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (fd' - fd)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc0' - bc0) + (ramp' - ramp) ⋅ (bc0' - α ⋅ bc0 - bcpc0')
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc1' - bc1) + (ramp' - ramp) ⋅ (bc1' - α ⋅ bc1 - bcpc1')
Terminal
bc0 ⋅ rpp + bc1 ⋅ fd - 1
See data structures and registers for explanations of the specific value 16.