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 $\mathtt{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}^{\prime }$ in between rows with memory pointer $mp$.

$$\forall i<j<k\in \{0,\dots ,T-1\}:mp\stackrel{△}{=}M[i][\mathtt{mp}]=M[k][\mathtt{mp}]\Rightarrow M[j][\mathtt{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.

$$\forall i<j\in \{0,\dots ,T-1\}:M[i][\mathtt{mp}]=M[j][\mathtt{mp}]\Rightarrow M[i][\mathtt{clk}]{<}_{\mathbb{Z}}M[j][\mathtt{clk}]$$

The symbol ${<}_{\mathbb{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.

$$\forall k\in \{0,\dots ,T-1\}:P[k][\mathtt{ci}]=read\Rightarrow \left((1)\Rightarrow (2)\right)$$

$$(1)\exists i\in \{0,\dots ,k\}:P[i][\mathtt{ci}]=write\wedge P[i+1][\mathtt{val}]=P[k][\mathtt{val}]\wedge P[i][\mathtt{mp}]=P[k][\mathtt{mp}]$$

$$(2)\nexists j\in \{i+1,\dots ,k-1\}:P[j][\mathtt{ci}]=write\wedge P[i][\mathtt{mp}]=P[k][\mathtt{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}\stackrel{△}{=}\{P[k]|P[k][\mathtt{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][\mathtt{ci}]\ne 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][\mathtt{val}]\ne P[k][\mathtt{val}]$ cannot occur because by construction of $i$, $val$ cannot change.
• The case $P[i][\mathtt{mp}]\ne P[k][\mathtt{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. $\square$