Clock Jump Differences and Inner Sorting

The previous sections show how it is proven that in the Jump Stack, Op Stack, and RAM Tables, the regions of constant memory pointer are contiguous. The next step is to prove that within each contiguous region of constant memory pointer, the rows are sorted for clock cycle. That is the topic of this section.

The problem arises from clock jumps, which describes the phenomenon when the clock cycle increases even though the memory pointer does not change. If arbitrary jumps were allowed, nothing would prevent the cheating prover from using a table where higher rows correspond to later states, giving rise to an exploitable attack. So it must be shown that every clock jump is directed forward and not backward.

Our strategy is to show that the difference, i.e., the next clock cycle minus the current clock cycle, is itself a clock cycle. Recall that the Processor Table's clock cycles run from 0 to . Therefore, a forward directed clock jump difference is in , whereas a backward directed clock jump's difference is in . No other clock jump difference can occur. If , there is no overlap between sets and . As a result, in this regime, showing that a clock jump difference is in guarantees that the jump is forward-directed.

The set of values in the Processor Table's clock cycle column is . A standard Lookup Argument can show that the clock jump differences are elements of that column. Since all three memory-like tables look up the same property, the Processor Table acts as a single server as opposed to three distinct servers. Concretely, the lookup multiplicities of the three clients, i.e., the memory-like tables, are recorded in a single column cjd_mul. It contains the element-wise sum of the three distinct lookup multiplicities.