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,
ClockPrevious InstructionRAM PointerRAM ValueInverse of RAM Pointer DifferenceBézout coefficient polynomial's coefficients 0Bézout coefficient polynomial's coefficients 1
-------

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 and row is 0, then iord in row is 0. Otherwise, iord in row is the multiplicative inverse of the difference between ramp in row and ramp in row . 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:

clkpiciniast0st1st2st3rampramv
0-push5000000
1pushpush6500000
2pushwrite_mempop650000
3write_mempoppush500056
4poppush15000056
5pushpush161500056
6pushwrite_mempop16150056
7write_mempoppush150001516
8poppush500001516
9pushread_mempop50001516
10read_mempoppop650056
11poppoppush500056
12poppush15000056
13pushread_mempop1500056
14read_mempoppop1615001516
15poppoppush150001516
16poppush500001516
17pushpush750001516
18pushwrite_mempop75001516
19write_mempoppush500057
20poppush15000057
21pushread_mempush1500057
22read_mempush51615001516
23pushread_memhalt5161501516
24read_memhalthalt75161557

RAM Table:

clkpirampramviord
7write_mem15160
8pop15160
9push15160
14read_mem15160
15pop15160
16pop15160
17push15160
18push15160
22read_mem15160
23push1516-10
3write_mem560
4pop560
5push560
6push560
10read_mem560
11pop560
12pop560
13push560
19write_mem570
20pop570
21push570
24read_mem57-5
0-000
1push000
2push000

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 :

  • The running product polynomial rpp, which accumulates a factor 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 .
  • The Bézout coefficient 1 bc1, which is the evaluation of the polynomial defined by the coefficients of bcpc1 in .

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

holds for any . However, if rp is not square-free, indicating a malicious prover, then the above relation holds in a negligible fraction of possible '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 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 in every row. In this expression, , , , and 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 .

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')
    • 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