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 denote the Processor Table and denote the memory-like table. Both have height . Both have columns clk, mp, and val. For the column clk coincides with the index of the row. 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 to denote the column name and 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 , there are no rows with a different memory pointer in between rows with memory pointer .

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.

The symbol denotes the integer less than operator, after lifting the operands from the finite field to the integers.

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

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

  • selecting for the columns clk, mp, val, the two tables' lists of rows are permutations of each other; and
  • is contiguous and regionally sorted; and
  • has no changes in val that coincide with clock jumps;

then has memory consistency.

Proof. For every memory pointer value , select the sublist of rows in order. The way this sublist is constructed guarantees that it coincides with the contiguous region of where the memory pointer is also .

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

  • If satisfies then by construction it also satisfies . As a result, row 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 then we can safely ignore this row: if there is no clock jump, then the absence of a -instruction guarantees that cannot change; and if there is a clock jump, then by assumption on , cannot change. So set to the clock cycle of the row above it in and proceed to the next iteration of the inner loop. If there are no rows left for to index, then there is no possible counterexample for and so remove the bottom-most row of and proceed to the next iteration of the outermost loop.
  • The case cannot occur because by construction of , cannot change.
  • The case 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 consists of only two rows, it can contain no counter-examples. By applying the above procedure, we can reduce every correctly constructed sublist to a list consisting of two rows. Therefore, for every , the sublist is free of counter-examples to memory consistency. Equivalently, is memory consistent.