Skip to content

Commit

Permalink
Master Tables
Browse files Browse the repository at this point in the history
A Master Table is, in some sense, a top-level table of Triton VM. It
contains all the data but little logic beyond bookkeeping and presenting
the data in a useful way. Conversely, the individual tables contain no
data but all of the respective logic. Master Tables are responsible for
managing the individual tables and for presenting the right data to the
right tables, serving as a clean interface between the VM and the
individual tables.

As a mental model, it is perfectly fine to think of the data for the
individual tables as completely separate from each other. Only the
cross-table argument links all tables together.

Conceptually, there are three Master Tables: the Master Base Table, the
Master Extension Table, and the Master Quotient Table. The lifecycle of
the Master Tables is as follows:

1. The Master Base Table is instantiated and filled using the Algebraic
    Execution Trace. This is the first time a Master Base Table is
    instantiated. It is in column-major form.
2. The Master Base Table is padded using logic from the individual
    tables.
3. The still-empty entries in the Master Base Table are filled with
    random elements. This step is also known as “trace randomization.”
4. Each column of the Master Base Table is low-degree extended. The
    result is the Master Base Table over the FRI domain. This is the
    second and last time a Master Base Table is instantiated. It is in
    row-major form.
5. The Master Base Table and the Master Base Table over the FRI domain
    are used to derive the Master Extension Table using logic from the
    individual tables. This is the first time a Master Extension Table
    is instantiated. It is in column-major form.
6. The Master Extension Table is trace-randomized.
7. Each column of the Master Extension Table is low-degree extended.
    The result is the Master Extension Table over the FRI domain. This
    is the second and last time a Master Extension Table is
    instantiated. It is in row-major form.
8. Using the Master Base Table over the FRI domain and the Master
    Extension Table over the FRI domain, the Quotient Master Table is
    derived using the AIR. Each individual table defines that part of
    the AIR that is relevant to it.

The following points are of note:
- The Master Extension Table's rightmost columns are the randomizer
    codewords. These are necessary for zero-knowledge.
- The terminal quotient of the cross-table argument, which links the
    individual tables together, is also stored in the Master Quotient
    Table. Even though the cross-table argument is not a table, it does
    define part of the AIR. Hence, the cross-table argument does not
    contribute to padding or extending the Master Tables, but is
    incorporated when deriving the Master Qoutient Table.
- For better performance, it is possible to derive the Master Quotient
    Table (step 8) from the Master Base Table and Master Extension Table
    over a smaller domain than the FRI domain – the “quotient domain.”
    The quotient domain is a subset of the FRI domain. This performance
    improvement changes nothing conceptually.

- global indexing into master tables
- fill in trace for individual tables
- pad individual tables
- extend individual tables
- remove old logic for trace filling, padding, and extending
- add randomizer polynomials to master extension table
- trace-randomize master tables
- perform low-degree extension in parallel
- build Merkle trees from master tables
- get quotient degree bounds of individual tables
- compute quotient codewords using master tables
- avoid recomputing zerofiers by building quotients by type, not table
- one place to store all quotients – “master quotient table”
    - including `GrandCrossTableArg` as a first-class citizen
- adapt multicircuits to use master tables
    - adapt code generator correspondingly
    - remove multivariate polynomials from multicircuits
- use type layout `#[repr(usize)]` for `*Table*Column` to safely allow
    indexing with compile-time known indices
- update specification:
    - remove unenforceable Ram Table constraints
    - add new column “previous instruction”
    - with the necessary constraints
    - don't require the Ram Table to be sorted by `ramp`
- documentation, tests, cheatsheet, …

Fix #11, fix #119, fix #120, fix #139, fix #148, fix #155.
  • Loading branch information
jan-ferdinand committed Dec 20, 2022
2 parents aded2d2 + 78d2a78 commit 4477d75
Show file tree
Hide file tree
Showing 42 changed files with 8,397 additions and 7,630 deletions.
237 changes: 125 additions & 112 deletions constraint-evaluation-generator/src/main.rs

Large diffs are not rendered by default.

Binary file modified specification/cheatsheet.pdf
Binary file not shown.
186 changes: 94 additions & 92 deletions specification/cheatsheet.tex

Large diffs are not rendered by default.

16 changes: 0 additions & 16 deletions specification/src/instruction-specific-transition-constraints.md
Original file line number Diff line number Diff line change
Expand Up @@ -390,14 +390,6 @@ Additionally, it defines the following transition constraints.
1. If `hv0` is 1, then `st2` is copied to `st7`.
1. If `hv0` is 1, then `st3` is copied to `st8`.
1. If `hv0` is 1, then `st4` is copied to `st9`.
1. The stack element in `st11` does not change.
1. The stack element in `st12` does not change.
1. The stack element in `st13` does not change.
1. The stack element in `st14` does not change.
1. The stack element in `st15` does not change.
1. The top of the OpStack underflow, i.e., `osv`, does not change.
1. The OpStack pointer does not change.
1. If `hv0` is 0, then the RAM value `ramv` does not change.

### Polynomials

Expand All @@ -408,14 +400,6 @@ Additionally, it defines the following transition constraints.
1. `(1 - hv0)·(st2' - st2) + hv0·(st7' - st2)`
1. `(1 - hv0)·(st3' - st3) + hv0·(st8' - st3)`
1. `(1 - hv0)·(st4' - st4) + hv0·(st9' - st4)`
1. `st11' - st11`
1. `st12' - st12`
1. `st13' - st13`
1. `st14' - st14`
1. `st15' - st15`
1. `osv' - osv`
1. `osp' - osp`
1. `(1 - hv0)·(ramv' - ramv)`

### Helper variable definitions for `divine_sibling`

Expand Down
12 changes: 8 additions & 4 deletions specification/src/processor-table.md
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ However, in order to verify the correctness of `RunningEvaluationFromHashTable`,
## Initial Constraints

1. The cycle counter `clk` is 0.
1. The previous instruction `previous_instruction` is 0.
1. The instruction pointer `ip` is 0.
1. The jump address stack pointer `jsp` is 0.
1. The jump address origin `jso` is 0.
Expand Down Expand Up @@ -93,7 +94,7 @@ However, in order to verify the correctness of `RunningEvaluationFromHashTable`,
1. `RunningEvaluationStandardOutput` is 1.
1. `RunningProductInstructionTable` has absorbed the first row with respect to challenges 🍓, 🍒, and 🥭 and indeterminate 🛁.
1. `RunningProductOpStackTable` has absorbed the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
1. `RunningProductRamTable` has absorbed the first row with respect to challenges 🍍, 🍈, and 🍎 and indeterminate 🛋.
1. `RunningProductRamTable` has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
1. `RunningProductJumpStackTable` has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
1. `RunningEvaluationToHashTable` has absorbed the first row with respect to challenges 🧄0 through 🧄9 and indeterminate 🪣 if the current instruction is `hash`. Otherwise, it is 1.
1. `RunningEvaluationFromHashTable` is 1.
Expand All @@ -106,6 +107,7 @@ However, in order to verify the correctness of `RunningEvaluationFromHashTable`,
### Initial Constraints as Polynomials

1. `clk`
1. `previous_instruction`
1. `ip`
1. `jsp`
1. `jso`
Expand Down Expand Up @@ -134,7 +136,7 @@ However, in order to verify the correctness of `RunningEvaluationFromHashTable`,
1. `RunningEvaluationStandardOutput - 1`
1. `RunningProductInstructionTable - (🛁 - 🍓·ip - 🍒·ci - 🥭·nia)`
1. `RunningProductOpStackTable - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒·osv)`
1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv)`
1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction)`
1. `RunningProductJumpStackTable - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)`
1. `(ci - opcode(hash))·(RunningEvaluationToHashTable - 1) + hash_deselector·(RunningEvaluationToHashTable - 🪣 - 🧄0·st0 - 🧄1·st1 - 🧄2·st2 - 🧄3·st3 - 🧄4·st4 - 🧄5·st5 - 🧄6·st6 - 🧄7·st7 - 🧄8·st8 - 🧄9·st9)`
1. `RunningEvaluationFromHashTable - 1`
Expand Down Expand Up @@ -163,11 +165,12 @@ The following constraints apply to every pair of rows.

1. The cycle counter `clk` increases by 1.
1. The padding indicator `IsPadding` is 0 or remains unchanged.
1. The current instruction `ci` in the current row is copied into `previous_instruction` in the next row or the next row is a padding row.
1. The running evaluation for standard input absorbs `st0` of the next row with respect to 🛏 if the current instruction is `read_io`, and remains unchanged otherwise.
1. The running evaluation for standard output absorbs `st0` of the next row with respect to 🧯 if the current instruction in the next row is `write_io`, and remains unchanged otherwise.
1. If the next row is not a padding row, the running product for the Instruction Table absorbs the next row with respect to challenges 🍓, 🍒, and 🥭 and indeterminate 🛁. Otherwise, it remains unchanged.
1. The running product for the OpStack Table absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
1. The running product for the RAM Table absorbs the next row with respect to challenges 🍍, 🍈, and 🍎 and indeterminate 🛋.
1. The running product for the RAM Table absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
1. The running product for the JumpStack Table absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
1. If the current instruction in the next row is `hash`, the running evaluation “to Hash Table” absorbs the next row with respect to challenges 🧄0 through 🧄9 and indeterminate 🪣. Otherwise, it remains unchanged.
1. If the current instruction is `hash`, the running evaluation “from Hash Table” absorbs the next row with respect to challenges 🫑0 through 🫑4 and indeterminate 🪟. Otherwise, it remains unchanged.
Expand All @@ -181,11 +184,12 @@ The following constraints apply to every pair of rows.

1. `clk' - (clk + 1)`
1. `IsPadding·(IsPadding' - IsPadding)`
1. `(1 - IsPadding')·(previous_instruction' - ci)`
1. `(ci - opcode(read_io))·(RunningEvaluationStandardInput' - RunningEvaluationStandardInput) + read_io_deselector·(RunningEvaluationStandardInput' - 🛏·RunningEvaluationStandardInput - st0')`
1. `(ci' - opcode(write_io))·(RunningEvaluationStandardOutput' - RunningEvaluationStandardOutput) + write_io_deselector'·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0')`
1. `(1 - IsPadding')·(RunningProductInstructionTable' - RunningProductInstructionTable(🛁 - 🍓·ip' - 🍒·ci' - 🥭·nia')) + IsPadding'·(RunningProductInstructionTable' - RunningProductInstructionTable)`
1. `RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒·osv')`
1. `RunningProductRamTable' - RunningProductRamTable·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv')`
1. `RunningProductRamTable' - RunningProductRamTable·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')`
1. `RunningProductJumpStackTable' - RunningProductJumpStackTable·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')`
1. `(ci' - opcode(hash))·(RunningEvaluationToHashTable' - RunningEvaluationToHashTable) + hash_deselector'·(RunningEvaluationToHashTable' - 🪣·RunningEvaluationToHashTable - 🧄0·st0' - 🧄1·st1' - 🧄2·st2' - 🧄3·st3' - 🧄4·st4' - 🧄5·st5' - 🧄6·st6' - 🧄7·st7' - 🧄8·st8' - 🧄9·st9')`
1. `(ci - opcode(hash))·(RunningEvaluationFromHashTable' - RunningEvaluationFromHashTable) + hash_deselector·(RunningEvaluationFromHashTable' - 🪟·RunningEvaluationFromHashTable - 🫑0·st5' - 🫑1·st6' - 🫑2·st7' - 🫑3·st8' - 🫑4·st9')`
Expand Down
Loading

0 comments on commit 4477d75

Please sign in to comment.