Random Access Memory Table

The RAM is accessible through read_mem and write_mem commands.

Base Columns

The RAM Table has 7 columns:

1. the cycle counter clk,
2. the instruction executed in the previous clock cycle previous_instruction,
3. RAM address pointer ramp,
4. the value of the memory at that address ramv,
5. helper variable iord ("inverse of ramp difference", but elsewhere also "difference inverse" and di for short),
6. Bézout coefficient polynomial coefficient 0 bcpc0,
7. Bézout coefficient polynomial coefficient 1 bcpc1,

Columns clk, previous_instruction, ramp, and ramv correspond to the columns of the same name in the Processor Table. A permutation argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical.

Column iord helps with detecting a change of ramp across two RAM Table rows. The function of iord is best explained in the context of sorting the RAM Table's rows, which is what the next section is about.

The Bézout coefficient polynomial coefficients bcpc0 and bcpc1 represent the coefficients of polynomials that are needed for the contiguity argument. This argument establishes that all regions of constant ramp are contiguous.

Extension Columns

The RAM Table has 2 extension columns, rppa and ClockJumpDifferenceLookupClientLogDerivative.

1. A Permutation Argument establishes that the rows in the RAM Table correspond to the rows of the Processor Table, after selecting for columns clk, ramp, ramv in both tables. The running product for this argument is contained in the rppa column.
2. In order to achieve memory consistency, a Lookup Argument shows that all clock jump differences are contained in the clk column of the Processor Table. The logarithmic derivative for this argument is contained in the ClockJumpDifferenceLookupClientLogDerivative column.

Sorting Rows

Up to order, the rows of the Hash Table in columns clk, ramp, ramv are identical to the rows in the Processor Table in columns clk, ramp, and ramv. In the Hash Table, the rows are arranged such that they

1. form contiguous regions of ramp, and
2. are sorted by cycle counter clk within each such region.

One way to achieve this is to sort by ramp first, clk second.

Coming back to iord: if the difference between ramp in row $i$ and row $i+1$ is 0, then iord in row $i$ is 0. Otherwise, iord in row $i$ is the multiplicative inverse of the difference between ramp in row $i+1$ and ramp in row $i$. In the last row, there being no next row, iord is 0.

An example of the mechanics can be found below. For reasons of display width, we abbreviate previous_instruction by pi. For illustrative purposes only, we use four stack registers st0 through st3 in the example. Triton VM has 16 stack registers, st0 through st15.

Processor Table:

RAM Table:

Padding

A padding row is a direct copy of the RAM Table's row with the highest value for column clk, called template row, with the exception of the cycle count column clk. In a padding row, the value of column clk is 1 greater than the value of column clk in the template row. The padding row is inserted right below the template row. Finally, the value of column iord is set to 0 in the template row. These steps are repeated until the desired padded height is reached. In total, above steps ensure that the Permutation Argument between the RAM Table and the Processor Table holds up.

Contiguity Argument

As a stepping stone to proving memory-consistency, it is necessary to prove that all regions of constant ramp are contiguous. In simpler terms, this condition stipulates that after filtering the rows in the RAM Table for any given ramp value, the resulting sublist of rows forms a contiguous sublist with no gaps. The contiguity establishes this property. What follows here is a summary of the Contiguity Argument for RAM Consistency.

The contiguity argument is a Randomized AIR without Preprocessing (RAP). In particular, there are 4 extension columns whose values depend on the verifier's challenge $\alpha$:

• The running product polynomial rpp, which accumulates a factor $(\alpha -\mathsf{ramp})$ in every consecutive pair of rows (including the first) where the current row's ramp value is different from the previous row's ramp value.
• The formal derivative fd, which is updated according to the product rule of differentiation and therefore tracks the formal derivative of rpp.
• The Bézout coefficient 0 bc0, which is the evaluation of the polynomial defined by the coefficients of bcpc0 in $\alpha$.
• The Bézout coefficient 1 bc1, which is the evaluation of the polynomial defined by the coefficients of bcpc1 in $\alpha$.

The contiguity of regions of constant ramp is implied by the square-freeness (as a polynomial in $\alpha$) of rpp. If rpp is square-free, then the Bézout relation

$$bc0\cdot \mathsf{rpp}+bc1\cdot \mathsf{fd}=1$$

holds for any $\alpha$. However, if rp is not square-free, indicating a malicious prover, then the above relation holds in a negligible fraction of possible $\alpha$'s. Therefore, the AIR enforces the Bézout relation as a terminal boundary constraint.

Inner Sorting

The second stepping stone to proving memory-consistency is to establish that the rows in each region of constant ramp are correctly sorted for clk in ascending order. To prove this property, we show that all differences of clk values difference greater than 1 in consecutive rows with the same ramp value – the clock jump differences – are contained in the clk table of the Processor Table. What follows here is a summary of the construction reduced to the RAM Table; the bulk of the logic and constraints that make this argument work is located in the Processor Table. The entirety of this construction is motivated and explained in TIP-0003.

The inner sorting argument requires one extension column cjdrp, which contains a running product. Specifically, this column accumulates a factor $\beta -({\mathsf{clk}}^{\prime }-\mathsf{clk})$ in every pair of consecutive rows where a) the ramp value is the same, and b) the difference in clk values minus one is different from zero.

Row Permutation Argument

Selecting for the columns clk, ramp, and ramv, the set of rows of the RAM Table is identical to the set of rows of the Processor Table. This argument requires one extension column, rppa, short for "running product for Permutation Argument". This column accumulates a factor $(a\cdot \mathsf{clk}+b\cdot \mathsf{ramp}+c\cdot \mathsf{ramv}-\gamma )$ in every row. In this expression, $a$, $b$, $c$, and $\gamma$ are challenges from the verifier.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

1. The first coefficient of the Bézout coefficient polynomial 0 bcpc0 is 0.
2. The Bézout coefficient 0 bc0 is 0.
3. The Bézout coefficient 1 bc1 is equal to the first coefficient of the Bézout coefficient polynomial bcpc1.
4. The running product polynomial rpp starts with 🧼 - ramp.
5. The formal derivative fd starts with 1.
6. The running product for the permutation argument with the Processor Table rppa has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
7. The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. bcpc0
2. bc0
3. bc1 - bcpc1
4. rpp - 🧼 + ramp
5. fd - 1
6. rppa - 🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction
7. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. If (ramp - ramp') is 0, then iord is 0, else iord is the multiplicative inverse of (ramp' - ramp).
2. If the ramp does not change and previous_instruction in the next row is not write_mem, then the RAM value ramv does not change.
3. The Bézout coefficient polynomial coefficients are allowed to change only when the ramp changes.
4. The running product polynomial rpp accumulates a factor (🧼 - ramp) whenever ramp changes.
5. The running product for the permutation argument with the Processor Table rppa absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
6. If the RAM pointer ramp does not change, then the logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative accumulates a factor (clk' - clk) relative to indeterminate 🪞. Otherwise, it remains the same.

Written as Disjunctive Normal Form, the same constraints can be expressed as:

1. iord is 0 or iord is the inverse of (ramp' - ramp).
2. (ramp' - ramp) is zero or iord is the inverse of (ramp' - ramp).
3. (ramp' - ramp) non-zero or previous_instruction' is opcode(write_mem) or ramv' is ramv.
4. bcpc0' - bcpc0 is zero or (ramp' - ramp) is nonzero.
5. bcpc1' - bcpc1 is zero or (ramp' - ramp) is nonzero.
6. (ramp' - ramp) is zero and rpp' = rpp; or (ramp' - ramp) is nonzero and rpp' = rpp·(ramp'-🧼)) is zero.
7. the formal derivative fd applies the product rule of differentiation (as necessary).
8. Bézout coefficient 0 is evaluated correctly.
9. Bézout coefficient 1 is evaluated correctly.
10. rppa' = rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
11. • the ramp changes or the logarithmic derivative accumulates a summand, and
    • the ramp does not change or the logarithmic derivative does not change.

Transition Constraints as Polynomials

1. iord·(iord·(ramp' - ramp) - 1)
2. (ramp' - ramp)·(iord·(ramp' - ramp) - 1)
3. (1 - iord·(ramp' - ramp))·(previous_instruction - opcode(write_mem))·(ramv' - ramv)
4. (iord·(ramp' - ramp) - 1)·(bcpc0' - bcpc0)
5. (iord·(ramp' - ramp) - 1)·(bcpc1' - bcpc1)
6. (iord·(ramp' - ramp) - 1)·(rpp' - rpp) + (ramp' - ramp)·(rpp' - rpp·(ramp'-🧼))
7. (iord·(ramp' - ramp) - 1)·(fd' - fd) + (ramp' - ramp)·(fd' - fd·(ramp'-🧼) - rpp)
8. (iord·(ramp' - ramp) - 1)·(bc0' - bc0) + (ramp' - ramp)·(bc0' - bc0·🧼 - bcpc0')
9. (iord·(ramp' - ramp) - 1)·(bc1' - bc1) + (ramp' - ramp)·(bc1' - bc1·🧼 - bcpc1')
10. rppa' - rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
11. (iord·(ramp' - ramp) - 1)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (ramp' - ramp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

1. The Bézout relation holds between rp, fd, bc0, and bc1.

Terminal Constraints as Polynomials

1. rpp·bc0 + fd·bc1 - 1