Module starky::cross_table_lookup

This crate provides support for cross-table lookups.

If a STARK S_1 calls an operation that is carried out by another STARK S_2, S_1 provides the inputs to S_2 and reads the output from S_1. To ensure that the operation was correctly carried out, we must check that the provided inputs and outputs are correctly read. Cross-table lookups carry out that check.

To achieve this, smaller CTL tables are created on both sides: looking and looked tables. In our example, we create a table S_1’ comprised of columns – or linear combinations of columns – of S_1, and rows that call operations carried out in S_2. We also create a table S_2’ comprised of columns – or linear combinations od columns – of S_2 and rows that carry out the operations needed by other STARKs. Then, S_1’ is a looking table for the looked S_2’, since we want to check that the operation outputs in S_1’ are indeeed in S_2’. Furthermore, the concatenation of all tables looking into S_2’ must be equal to S_2’.

To achieve this, we construct, for each table, a permutation polynomial Z(x). Z(x) is computed as the product of all its column combinations. To check it was correctly constructed, we check:

• Z(gw) = Z(w) * combine(w) where combine(w) is the column combination at point w.
• Z(g^(n-1)) = combine(1).
• The verifier also checks that the product of looking table Z polynomials is equal to the associated looked table Z polynomial. Note that the first two checks are written that way because Z polynomials are computed upside down for convenience.

Additionally, we support cross-table lookups over two rows. The permutation principle is similar, but we provide not only local_values but also next_values – corresponding to the current and next row values – when computing the linear combinations.

Modules

• debug_utils
  Debugging module used to assert correctness of the different CTLs of a multi-STARK system, that can be used during the proof generation process.

Structs

• CrossTableLookup
  Cross-table lookup data consisting in the lookup table (looked_table) and all the tables that look into looked_table (looking_tables). Each looking_table corresponds to a STARK’s table whose rows have been filtered out and whose columns have been through a linear combination (see eval_table). The concatenation of those smaller tables should result in the looked_table.
• CtlCheckVars
  Data necessary to check the cross-table lookups of a given table.
• CtlCheckVarsTarget
  Circuit version of CtlCheckVars. Data necessary to check the cross-table lookups of a given table.
• CtlData
  Cross-table lookup data for one table.
• CtlZData
  Cross-table lookup data associated with one Z(x) polynomial. One Z(x) polynomial can be associated to multiple tables, built from the same STARK.
• TableWithColumns
  A table index with a linear combination of columns and a filter. filter is used to determine the rows to select in table. columns represents linear combinations of the columns of table.

Functions

• get_ctl_data
  Outputs a tuple of (challenges, data) of CTL challenges and all the CTL data necessary to prove a multi-STARK system.
• get_ctl_vars_from_proofs
  Outputs all the CTL data necessary to prove a multi-STARK system.
• verify_cross_table_lookups
  Verifies all cross-table lookups.
• verify_cross_table_lookups_circuit
  Circuit version of verify_cross_table_lookups. Verifies all cross-table lookups.

Type Aliases

• TableIdx
  An alias for usize, to represent the index of a STARK table in a multi-STARK setting.