Random Access Memory Table
The RAM is accessible through read_mem
and write_mem
commands.
Base Columns
The RAM Table has 7 columns:
- the cycle counter
clk
, - the instruction executed in the previous clock cycle
previous_instruction
, - RAM address pointer
ramp
, - the value of the memory at that address
ramv
, - helper variable
iord
("inverse oframp
difference", but elsewhere also "difference inverse" anddi
for short), - Bézout coefficient polynomial coefficient 0
bcpc0
, - Bézout coefficient polynomial coefficient 1
bcpc1
,
Clock | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bé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
.
- 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 therppa
column. - 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 theClockJumpDifferenceLookupClientLogDerivative
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
- form contiguous regions of
ramp
, and - 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:
clk | pi | ci | nia | st0 | st1 | st2 | st3 | ramp | ramv |
---|---|---|---|---|---|---|---|---|---|
0 | - | push | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
1 | push | push | 6 | 5 | 0 | 0 | 0 | 0 | 0 |
2 | push | write_mem | pop | 6 | 5 | 0 | 0 | 0 | 0 |
3 | write_mem | pop | push | 5 | 0 | 0 | 0 | 5 | 6 |
4 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 6 |
5 | push | push | 16 | 15 | 0 | 0 | 0 | 5 | 6 |
6 | push | write_mem | pop | 16 | 15 | 0 | 0 | 5 | 6 |
7 | write_mem | pop | push | 15 | 0 | 0 | 0 | 15 | 16 |
8 | pop | push | 5 | 0 | 0 | 0 | 0 | 15 | 16 |
9 | push | read_mem | pop | 5 | 0 | 0 | 0 | 15 | 16 |
10 | read_mem | pop | pop | 6 | 5 | 0 | 0 | 5 | 6 |
11 | pop | pop | push | 5 | 0 | 0 | 0 | 5 | 6 |
12 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 6 |
13 | push | read_mem | pop | 15 | 0 | 0 | 0 | 5 | 6 |
14 | read_mem | pop | pop | 16 | 15 | 0 | 0 | 15 | 16 |
15 | pop | pop | push | 15 | 0 | 0 | 0 | 15 | 16 |
16 | pop | push | 5 | 0 | 0 | 0 | 0 | 15 | 16 |
17 | push | push | 7 | 5 | 0 | 0 | 0 | 15 | 16 |
18 | push | write_mem | pop | 7 | 5 | 0 | 0 | 15 | 16 |
19 | write_mem | pop | push | 5 | 0 | 0 | 0 | 5 | 7 |
20 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 7 |
21 | push | read_mem | push | 15 | 0 | 0 | 0 | 5 | 7 |
22 | read_mem | push | 5 | 16 | 15 | 0 | 0 | 15 | 16 |
23 | push | read_mem | halt | 5 | 16 | 15 | 0 | 15 | 16 |
24 | read_mem | halt | halt | 7 | 5 | 16 | 15 | 5 | 7 |
RAM Table:
clk | pi | ramp | ramv | iord |
---|---|---|---|---|
7 | write_mem | 15 | 16 | 0 |
8 | pop | 15 | 16 | 0 |
9 | push | 15 | 16 | 0 |
14 | read_mem | 15 | 16 | 0 |
15 | pop | 15 | 16 | 0 |
16 | pop | 15 | 16 | 0 |
17 | push | 15 | 16 | 0 |
18 | push | 15 | 16 | 0 |
22 | read_mem | 15 | 16 | 0 |
23 | push | 15 | 16 | -10 |
3 | write_mem | 5 | 6 | 0 |
4 | pop | 5 | 6 | 0 |
5 | push | 5 | 6 | 0 |
6 | push | 5 | 6 | 0 |
10 | read_mem | 5 | 6 | 0 |
11 | pop | 5 | 6 | 0 |
12 | pop | 5 | 6 | 0 |
13 | push | 5 | 6 | 0 |
19 | write_mem | 5 | 7 | 0 |
20 | pop | 5 | 7 | 0 |
21 | push | 5 | 7 | 0 |
24 | read_mem | 5 | 7 | -5 |
0 | - | 0 | 0 | 0 |
1 | push | 0 | 0 | 0 |
2 | push | 0 | 0 | 0 |
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'sramp
value is different from the previous row'sramp
value. - The formal derivative
fd
, which is updated according to the product rule of differentiation and therefore tracks the formal derivative ofrpp
. - The Bézout coefficient 0
bc0
, which is the evaluation of the polynomial defined by the coefficients ofbcpc0
in . - The Bézout coefficient 1
bc1
, which is the evaluation of the polynomial defined by the coefficients ofbcpc1
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
- The first coefficient of the Bézout coefficient polynomial 0
bcpc0
is 0. - The Bézout coefficient 0
bc0
is 0. - The Bézout coefficient 1
bc1
is equal to the first coefficient of the Bézout coefficient polynomialbcpc1
. - The running product polynomial
rpp
starts with🧼 - ramp
. - The formal derivative
fd
starts with 1. - The running product for the permutation argument with the Processor Table
rppa
has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. - The logarithmic derivative for the clock jump difference lookup
ClockJumpDifferenceLookupClientLogDerivative
is 0.
Initial Constraints as Polynomials
bcpc0
bc0
bc1 - bcpc1
rpp - 🧼 + ramp
fd - 1
rppa - 🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction
ClockJumpDifferenceLookupClientLogDerivative
Consistency Constraints
None.
Transition Constraints
- If
(ramp - ramp')
is 0, theniord
is 0, elseiord
is the multiplicative inverse of(ramp' - ramp)
. - If the
ramp
does not change andprevious_instruction
in the next row is notwrite_mem
, then the RAM valueramv
does not change. - The Bézout coefficient polynomial coefficients are allowed to change only when the
ramp
changes. - The running product polynomial
rpp
accumulates a factor(🧼 - ramp)
wheneverramp
changes. - The running product for the permutation argument with the Processor Table
rppa
absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. - If the RAM pointer
ramp
does not change, then the logarithmic derivative for the clock jump difference lookupClockJumpDifferenceLookupClientLogDerivative
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:
iord
is 0 oriord
is the inverse of(ramp' - ramp)
.(ramp' - ramp)
is zero oriord
is the inverse of(ramp' - ramp)
.(ramp' - ramp)
non-zero orprevious_instruction'
isopcode(write_mem)
orramv'
isramv
.bcpc0' - bcpc0
is zero or(ramp' - ramp)
is nonzero.bcpc1' - bcpc1
is zero or(ramp' - ramp)
is nonzero.(ramp' - ramp)
is zero andrpp' = rpp
; or(ramp' - ramp)
is nonzero andrpp' = rpp·(ramp'-🧼))
is zero.- the formal derivative
fd
applies the product rule of differentiation (as necessary). - Bézout coefficient 0 is evaluated correctly.
- Bézout coefficient 1 is evaluated correctly.
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.
- the
Transition Constraints as Polynomials
iord·(iord·(ramp' - ramp) - 1)
(ramp' - ramp)·(iord·(ramp' - ramp) - 1)
(1 - iord·(ramp' - ramp))·(previous_instruction - opcode(write_mem))·(ramv' - ramv)
(iord·(ramp' - ramp) - 1)·(bcpc0' - bcpc0)
(iord·(ramp' - ramp) - 1)·(bcpc1' - bcpc1)
(iord·(ramp' - ramp) - 1)·(rpp' - rpp) + (ramp' - ramp)·(rpp' - rpp·(ramp'-🧼))
(iord·(ramp' - ramp) - 1)·(fd' - fd) + (ramp' - ramp)·(fd' - fd·(ramp'-🧼) - rpp)
(iord·(ramp' - ramp) - 1)·(bc0' - bc0) + (ramp' - ramp)·(bc0' - bc0·🧼 - bcpc0')
(iord·(ramp' - ramp) - 1)·(bc1' - bc1) + (ramp' - ramp)·(bc1' - bc1·🧼 - bcpc1')
rppa' - rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
(iord·(ramp' - ramp) - 1)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (ramp' - ramp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
Terminal Constraints
- The Bézout relation holds between
rp
,fd
,bc0
, andbc1
.
Terminal Constraints as Polynomials
rpp·bc0 + fd·bc1 - 1