# Proof of Memory Consistency

Whenever the Processor Table reads a value "from" a memory-like table, this value appears nondeterministically and is unconstrained by the base table AIR constraints. However, there is a permutation argument that links the Processor Table to the memory-like table in question. *The construction satisfies memory consistency if it guarantees that whenever a memory cell is read, its value is consistent with the last time that cell was written.*

The above is too informal to provide a meaningful proof for. Let's put formal meanings on the proposition and premises, before reducing the former to the latter.

Let $P$ denote the Processor Table and $M$ denote the memory-like table. Both have height $T$. Both have columns `clk`

, `mp`

, and `val`

. For $P$ the column `clk`

coincides with the index of the row. $P$ has another column `ci`

, which contains the current instruction, which is `write`

, `read`

, or `any`

. Obviously, `mp`

and `val`

are abstract names that depend on the particular memory-like table, just like `write`

, `read`

, and `any`

are abstract instructions that depend on the type of memory being accessed. In the following math notation we use $col$ to denote the column name and $col$ to denote the value that the column might take in a given row.

**Definition 1 (contiguity):** The memory-like table is *contiguous* iff all sublists of rows with the same memory pointer `mp`

are contiguous. Specifically, for any given memory pointer $mp$, there are no rows with a different memory pointer $mp_{′}$ in between rows with memory pointer $mp$.

$∀i<j<k∈{0,…,T−1}:mp=△M[i][mp]=M[k][mp]⇒M[j][mp]=mp$

**Definition 2 (regional sorting):** The memory-like table is *regionally sorted* iff for every contiguous region of constant memory pointer, the clock cycle increases monotonically.

$∀i<j∈{0,…,T−1}:M[i][mp]=M[j][mp]⇒M[i][clk]<_{Z}M[j][clk]$

The symbol $<_{Z}$ denotes the integer less than operator, after lifting the operands from the finite field to the integers.

**Definition 3 (memory consistency):** A Processor Table $P$ has *memory consistency* if whenever a memory cell at location $mp$ is read, its value corresponds to the previous time the memory cell at location $mp$ was written. Specifically, there are no writes in between the write and the read, that give the cell a different value.

$∀k∈{0,…,T−1}:P[k][ci]=read⇒((1)⇒(2))$

$(1)∃i∈{0,…,k}:P[i][ci]=write∧P[i+1][val]=P[k][val]∧P[i][mp]=P[k][mp]$

$(2)∄j∈{i+1,…,k−1}:P[j][ci]=write∧P[i][mp]=P[k][mp]$

**Theorem 1 (memory consistency):** Let $P$ be a Processor Table. If there exists a memory-like table $M$ such that

- selecting for the columns
`clk`

,`mp`

,`val`

, the two tables' lists of rows are permutations of each other; and - $M$ is contiguous and regionally sorted; and
- $M$ has no changes in
`val`

that coincide with clock jumps;

then $P$ has memory consistency.

*Proof.* For every memory pointer value $mp$, select the sublist of rows $P_{mp}=△{P[k]∣P[k][mp]=mp}$ in order. The way this sublist is constructed guarantees that it coincides with the contiguous region of $M$ where the memory pointer is also $mp$.

Iteratively apply the following procedure to $P_{mp}$: remove the bottom-most row if it does not correspond to a row $k$ that constitutes a counter-example to memory consistency. Specifically, let $i$ be the clock cycle of the previous row in $P_{mp}$.

- If $i$ satisfies $(1)$ then by construction it also satisfies $(2)$. As a result, row $k$ is not part of a counter-example to memory consistency. We can therefore remove the bottom-most row and proceed to the next iteration of the outermost loop.
- If $P[i][ci]=write$ then we can safely ignore this row: if there is no clock jump, then the absence of a $write$-instruction guarantees that $val$ cannot change; and if there is a clock jump, then by assumption on $M$, $val$ cannot change. So set $i$ to the clock cycle of the row above it in $P_{mp}$ and proceed to the next iteration of the inner loop. If there are no rows left for $i$ to index, then there is no possible counterexample for $k$ and so remove the bottom-most row of $P_{mp}$ and proceed to the next iteration of the outermost loop.
- The case $P[i+1][val]=P[k][val]$ cannot occur because by construction of $i$, $val$ cannot change.
- The case $P[i][mp]=P[k][mp]$ cannot occur because the list was constructed by selecting only elements with the same memory pointer.
- This list exhausts the possibilities of condition (1).

When $P_{mp}$ consists of only two rows, it can contain no counter-examples. By applying the above procedure, we can reduce every correctly constructed sublist $P_{mp}$ to a list consisting of two rows. Therefore, for every $mp$, the sublist $P_{mp}$ is free of counter-examples to memory consistency. Equivalently, $P$ is memory consistent. $□$