CTL protocol
Since each STARK module is like a small state machine where its state transition can be uniquely captured in the form of a table, called the execution trace
, the STARK modules are henceforth also referred to as STARK tables. See the repo for further details of each table here.
For each STARK table, ordinary STARK proof and verification are used to check if all state transitions occurring in the module satisfies stipulated constraints.
However, there are input and output values shared among the tables. These values need to be checked for possible alterations while being shared among tables. For this purpose, crosstable lookups (CTLs) are used in verifying that the shared values are not tampered with.
How CTLs work¶
The CTL protocol is based on the logUP argment, which works similar to how rangechecks work. Rangechecks are discussed in a subsequent document to this one.
Example (CTL)¶
Consider the following scenario as an example. Suppose STARK \(S_2\) requires an operation – say \(Op\) – that is carried out by another STARK \(S_1\).
Then \(S_1\) writes input and output values of \(Op\) in its own table, and provides these two values as inputs to STARK \(S_2\).
Now, STARK \(S_2\) also writes the input and output values in its rows, and the table’s constraints check if \(Op\) is carried out correctly.
However, one still needs to ensure that the input and output values in \(S_1\) are the same as those shared with \(S_2\).
In other words, and in cases where the \(S_1\) and \(S_2\) tables have many rows individually, one needs to ensure that all the rows of the \(S_1\) table involving \(Op\) appear amongst the rows of the \(S_2\) table.
Note that, for the sake of efficiency, the \(S_1\) and \(S_2\) tables are first reduced to the input and output columns.
And thus, this check is tantamount to ensuring that the rows of the \(S_1\) table involving \(Op\) are but permutations of the rows of \(S_2\) that carry out \(Op\).
How the CTL proof works¶
As outlined in the above example, verifying that shared values among STARK tables are not tampered with amounts to proving that rows of reduced STARK tables are permutations of each other.
The proof therefore is achieved in three steps;

Filtering rows of interest in both STARK tables.

Computing columnwise ‘running sums’.

Checking correct construction and equality of ‘running sums’.
Table filtering¶
Define filters \(f^1\) and \(f^2\) for STARK tables \(S_1\) and \(S_2\) , respectively, such that
for \(i \in \{ 0, 1 \}\) and \(0 < j < n_i\), where \(n_i\) is \(S_i\)’s number of rows. So, each filter \(f^i\) evaluates to either \(0\) or \(1\).
Next create subtables \(S_1'\) and \(S_2'\) of STARK tables \(S_1\) and \(S_2\) , respectively, such that \(f^i(row_j) = 1\) for all \(row_j\) of \(S_i'\).
Note
Columns \(\{ c^{i,j} \}\) of the filtered subtables \(S_i'\) only contains values that must be identical (these are shared input and output values.)
Let \(\alpha\) and \(\beta\) be random challenges which in an interactive setting the verifier sends to the prover.
Filters are limited to (at most) degree 2 combinations of columns.
Computing running sums¶
For each \(i \in \{0,1\}\), let \(\{ c^{i,j} \}\) denote the columns of \(S_i'\).
Define a running sum \(Z_i^{S_i}\) for \(S_i'\) as follows,
and
for \(0 < l < n1\).
Note that \(Z_l^{S_i}\) is computed backwards. i.e., It starts with \(Z_{n1}^{S_i}\) and goes down to \(Z_0^{S_i}\) as the final sum.
Checking running sums¶
After computing running sums, check equality of the final sums \(Z_0^{S_1} =?\ Z_0^{S_2}\) and whether the running sums were correctly constructed.
The above three steps turn the CTL argument into a LogUp lookup argument, where
 the STARK table \(S_1'\) is the looking table
 the STARK table \(S_2'\) is the looked table
which checks for equality between \(S_1'\) and \(S_2'\).
CTL protocol summary¶
The crosstable protocol can be summarized as follows.
For any STARK table \(S\), the prover:
 Constructs the
looking sums
, which are the running sums \(\{Z_j^l\}\) for each table looking into \(S\).  Constructs the
looked sum
, which is the running sum \(Z^S\) for \(S\).  Sends all the final values \(\{Z_{j,0}^l\}\) and \(Z_0^S\) to the verifier.
 Sends a commitment to the
looking sums
\(\{Z_{j}^l\}\) and thelooked sum
\(Z^S\) to the verifier.
On the other side, and for the same STARK table \(S\), the verifier:
 Computes the sum \(Z = \sum_j Z_{j}^l\).
 Checks equality, \(Z =?\ Z_0^S\).
 Checks whether each of the running sums \(Z_{j}^l\) and \(Z^S\) were correctly constructed.