Contiguity of Memory-Pointer Regions

Contiguity for OpStack Table

In each cycle, the memory pointer for the OpStack Table, osp, 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: osp starts with zero, so in terms of polynomials the constraint is osp.
  • Transition constraint: the new osp is either the same as the previous or one larger. The polynomial representation for this constraint is (osp' - osp - 1) * (osp' - osp).

Contiguity for JumpStack Table

Analogously to the OpStack Table, the JumpStack'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 is jsp.
  • 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 base 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:

  • Base column iord and two deterministic transition constraints enable conditioning on a changed memory pointer.
  • Base columns bcpc0 and bcpc1 and two deterministic transition constraints contain and constrain the symbolic Bézout coefficient polynomials' coefficients.
  • Extension 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.
  • Extension column fd is the formal derivative of rpp. A randomized transition constraint verifies the correct application of the product rule of differentiation to update this column.
  • Extension columns bc0 and bc1 build up the Bézout coefficient polynomials based on the corresponding base columns, bcpc0 and bcpc1. 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.

rampiordbcpc0bcpc1rppfdbc0bc1
0
0
0
0
-

The values contained in the extension 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 base 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 base 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