diff --git a/specification/cheatsheet.pdf b/specification/cheatsheet.pdf index 06ba4a89c..f242007b3 100644 Binary files a/specification/cheatsheet.pdf and b/specification/cheatsheet.pdf differ diff --git a/specification/cheatsheet.tex b/specification/cheatsheet.tex index 2762ce398..f5f5a0578 100644 --- a/specification/cheatsheet.tex +++ b/specification/cheatsheet.tex @@ -87,14 +87,14 @@ \rowcolors{2}{row2}{row1} \begin{tabular}{lllllllllllllllllllllll} \toprule - Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule - Program & \multicolumn{3}{l}{Address} & & \multicolumn{2}{l}{Instruction} & \multicolumn{4}{l}{LookupMultiplicity} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & \\ - Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\ - OpStack & \texttt{CLK} & \texttt{clk\_di} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\ - RAM & \texttt{CLK} & \texttt{clk\_di} & & \texttt{PI} & & \texttt{bcpc0} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\ - JumpStack & \texttt{CLK} & \texttt{clk\_di} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\ - Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\ - U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule + Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule + Program & \multicolumn{3}{l}{Address} & & \multicolumn{3}{l}{Instruction} & \multicolumn{4}{l}{LookupMultiplicity} & \multicolumn{3}{l}{IsPadding} & & & & & & & & \\ + Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\ + OpStack & \texttt{CLK} & & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\ + RAM & \texttt{CLK} & & & \texttt{PI} & & & \multicolumn{2}{l}{\texttt{bcpc0}} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\ + JumpStack & \texttt{CLK} & & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\ + Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\ + U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule \end{tabular} } %end scalebox \begin{tikzpicture}[remember picture, overlay] @@ -119,12 +119,12 @@ & base & ext & $\sum$ \\ \midrule Program & 4 & 1 & 5 \\ Processor & 44 & 13 & 57 \\ - OpStack & 5 & 2 & 7 \\ - RAM & 8 & 6 & 14 \\ - JumpStack & 6 & 2 & 8 \\ + OpStack & 4 & 2 & 6 \\ + RAM & 7 & 6 & 13 \\ + JumpStack & 5 & 2 & 7 \\ Hash & 50 & 3 & 53 \\ U32 & 14 & 1 & 15 \\ \bottomrule\bottomrule - $\sum$ & 131 & 28 & 159 + $\sum$ & 128 & 28 & 156 \end{tabular} \end{minipage}% \hfill% @@ -148,14 +148,14 @@ \toprule & init & cons & trans & term & $\sum$ \\ \midrule Program & 2 & 1 & 3 & & 6 \\ - Processor & 39 & 12 & 77 & 2 & 130 \\ - OpStack & 5 & & 6 & & 11 \\ - Ram & 8 & & 14 & 1 & 23 \\ - JumpStack & 6 & & 8 & & 14 \\ + Processor & 39 & 13 & 75 & 1 & 128 \\ + OpStack & 5 & & 4 & & 9 \\ + Ram & 8 & & 12 & 1 & 21 \\ + JumpStack & 6 & & 6 & & 12 \\ Hash & 5 & 40 & 26 & & 71 \\ U32 & 2 & 14 & 22 & 2 & 40 \\ Cross-Table & & & & 1 & 1 \\ \bottomrule\bottomrule - $\sum$ & 67 & 67 & 156 & 6 & 296 + $\sum$ & 67 & 68 & 148 & 5 & 288 \end{tabular} \end{minipage} diff --git a/specification/src/img/aet-relations.ipe b/specification/src/img/aet-relations.ipe index 656d4b244..18306f154 100644 --- a/specification/src/img/aet-relations.ipe +++ b/specification/src/img/aet-relations.ipe @@ -1,7 +1,7 @@ - + \usepackage{lmodern} \renewcommand*\familydefault{\sfdefault} \usepackage[T1]{fontenc} @@ -318,119 +318,74 @@ h - + - + -80 188 m -80 44 l -280 44 l -280 188 l +120 172 m +120 60 l +272 60 l +272 172 l h - + +158.864 117.909 m +164.993 121.995 l + + +168 124 m +156 116 l + + +158.864 117.909 m +164.993 121.995 l + + 192 138 m 192 154 l processor program -output -input - -176 120 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 96 l - -jumpStack +output +input +RAM opStack -RAM -hash - -128 154 m -128 134 l -128 130 -132 130 c -168 130 l - - -256 154 m -256 134 l -256 130 -252 130 c -216 130 l - - +jumpStack + +144 152 m +144 132 l +144 128 +148 128 c +168 128 l + + +240 152 m +240 132 l +240 128 +236 128 c +216 128 l + + 192 124 m 192 92 l - -200 124 m -200 104 l -200 100 -204 100 c -228 100 l -232 100 -232 96 c -232 92 l - - -184 124 m -184 104 l -184 100 -180 100 c -148 100 l -144 100 -144 96 c + +180 124 m +180 108 l +180 104 +176 104 c +148 104 l +144 104 +144 100 c 144 92 l 1.20123 0 0 1.20123 176 176 e - + 1.20123 0 0 1.20123 176 176 e - -176 124 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 92 l - - -208 124 m -208 120 l -208 116 -212 116 c -252 116 l -256 116 -256 112 c -256 64 l - - -240 76 m -240 64 l - - -192 76 m -192 64 l - - -144 76 m -144 64 l - - -140 64 m -260 64 l - - + 160 100 m 8 0 0 -8 160 92 152 92 a @@ -438,26 +393,45 @@ h 160 100 m 8 0 0 -8 160 92 152 92 a -u32 - -176 120 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 96 l - +u32 -168 124 m -164 120 l -160 116 -156 116 c -100 116 l -96 116 -96 120 c -96 124 l +216 124 m +228 116 l + +hash + +184 124 m +184 104 l +184 100 +180 100 c +152 100 l +148 100 +148 96 c +148 92 l + + +180 124 m +180 108 l +180 104 +176 104 c +148 104 l +144 104 +144 100 c +144 92 l + + +184 124 m +184 104 l +184 100 +180 100 c +152 100 l +148 100 +148 96 c +148 92 l + + +192 124 m +192 92 l diff --git a/specification/src/img/aet-relations.pdf b/specification/src/img/aet-relations.pdf index 6ddb3f710..b0dd76df0 100644 Binary files a/specification/src/img/aet-relations.pdf and b/specification/src/img/aet-relations.pdf differ diff --git a/specification/src/img/aet-relations.png b/specification/src/img/aet-relations.png index 94e8b12ce..4016831fc 100644 Binary files a/specification/src/img/aet-relations.png and b/specification/src/img/aet-relations.png differ diff --git a/specification/src/jump-stack-table.md b/specification/src/jump-stack-table.md index 48dac940c..b5d8be6bd 100644 --- a/specification/src/jump-stack-table.md +++ b/specification/src/jump-stack-table.md @@ -4,17 +4,16 @@ The Jump Stack Memory contains the underflow from the Jump Stack. ## Base Columns -The Jump Stack Table consists of 6 columns: +The Jump Stack Table consists of 5 columns: 1. the cycle counter `clk` -1. the inverse-or-zero of the difference between two consecutive `clk` values minus one, `clk_di`, 1. current instruction `ci`, 1. the jump stack pointer `jsp`, 1. the last jump's origin `jso`, and 1. the last jump's destination `jsd`. -| Clock | Inverse of Clock Difference Minus One | Current Instruction | Jump Stack Pointer | Jump Stack Origin | Jump Stack Destination | -|:------|:--------------------------------------|:--------------------|:-------------------|:------------------|:-----------------------| -| - | - | - | - | - | - | +| Clock | Current Instruction | Jump Stack Pointer | Jump Stack Origin | Jump Stack Destination | +|:------|:--------------------|:-------------------|:------------------|:-----------------------| +| - | - | - | - | - | The rows are sorted by jump stack pointer `jsp`, then by cycle counter `clk`. The column `jsd` contains the destination of stack-extending jump (`call`) as well as of the no-stack-change jump (`recurse`); @@ -83,35 +82,35 @@ Execution trace: Jump Stack Table: -| `clk` | `clk_di` | `ci` | `jsp` | `jso` | `jsd` | -|------:|-----------------------:|:---------|------:|-------:|-------:| -| 0 | 0 | `foo` | 0 | `0x00` | `0x00` | -| 1 | 0 | `bar` | 0 | `0x00` | `0x00` | -| 2 | (7 - 2 - 1)${}^{-1}$ | `call` | 0 | `0x00` | `0x00` | -| 7 | 0 | `buzz` | 0 | `0x00` | `0x00` | -| 8 | 0 | `bar` | 0 | `0x00` | `0x00` | -| 9 | (17 - 9 - 1)${}^{-1}$ | `call` | 0 | `0x00` | `0x00` | -| 17 | (3 - 17 - 1)${}^{-1}$ | `foo` | 0 | `0x00` | `0x00` | -| 3 | 0 | `buzz` | 1 | `0x04` | `0xA0` | -| 4 | 0 | `foo` | 1 | `0x04` | `0xA0` | -| 5 | 0 | `bar` | 1 | `0x04` | `0xA0` | -| 6 | (10 - 6 - 1)${}^{-1}$ | `return` | 1 | `0x04` | `0xA0` | -| 10 | 0 | `foo` | 1 | `0x08` | `0xB0` | -| 11 | (16 - 11 - 1)${}^{-1}$ | `call` | 1 | `0x08` | `0xB0` | -| 16 | (12 - 16 - 1)${}^{-1}$ | `return` | 1 | `0x08` | `0xB0` | -| 12 | 0 | `buzz` | 2 | `0xB3` | `0xC0` | -| 13 | 0 | `foo` | 2 | `0xB3` | `0xC0` | -| 14 | 0 | `bar` | 2 | `0xB3` | `0xC0` | -| 15 | 0 | `return` | 2 | `0xB3` | `0xC0` | +| `clk` | `ci` | `jsp` | `jso` | `jsd` | +|------:|:---------|------:|-------:|-------:| +| 0 | `foo` | 0 | `0x00` | `0x00` | +| 1 | `bar` | 0 | `0x00` | `0x00` | +| 2 | `call` | 0 | `0x00` | `0x00` | +| 7 | `buzz` | 0 | `0x00` | `0x00` | +| 8 | `bar` | 0 | `0x00` | `0x00` | +| 9 | `call` | 0 | `0x00` | `0x00` | +| 17 | `foo` | 0 | `0x00` | `0x00` | +| 3 | `buzz` | 1 | `0x04` | `0xA0` | +| 4 | `foo` | 1 | `0x04` | `0xA0` | +| 5 | `bar` | 1 | `0x04` | `0xA0` | +| 6 | `return` | 1 | `0x04` | `0xA0` | +| 10 | `foo` | 1 | `0x08` | `0xB0` | +| 11 | `call` | 1 | `0x08` | `0xB0` | +| 16 | `return` | 1 | `0x08` | `0xB0` | +| 12 | `buzz` | 2 | `0xB3` | `0xC0` | +| 13 | `foo` | 2 | `0xB3` | `0xC0` | +| 14 | `bar` | 2 | `0xB3` | `0xC0` | +| 15 | `return` | 2 | `0xB3` | `0xC0` | ## Extension Columns -The Jump Stack Table has 2 extension columns, `rppa` and `rpcjd`. +The Jump Stack Table has 2 extension columns, `rppa` and `ClockJumpDifferenceLookupClientLogDerivative`. 1. A Permutation Argument establishes that the rows of the Jump Stack Table match with the rows in the [Processor Table](processor-table.md). The running product for this argument is contained in the `rppa` column. -1. In order to achieve [memory consistency](memory-consistency.md), a [multi-table Permutation Argument](memory-consistency.md#memory-like-tables) shows that all clock jump differences greater than one, from all memory-like tables (i.e., including the [RAM Table](random-access-memory-table.md) and the [OpStack Table](operational-stack-table.md)), are contained in the `cjd` column of the Processor Table. - The running product for this argument is contained in the `rpcjd` column. +1. In order to achieve [memory consistency](memory-consistency.md), a [Lookup Argument](lookup-argument.md) shows that all clock jump differences are contained in the `clk` column of the [Processor Table](processor-table.md). + The logarithmic derivative for this argument is contained in the `ClockJumpDifferenceLookupClientLogDerivative` column. ## Padding @@ -125,8 +124,12 @@ In total, above steps ensure that the Permutation Argument between the Jump Stac Memory-consistency follows from two more primitive properties: - 1. Contiguity of regions of constant memory pointer. Since the memory pointer for the JumpStack table, `jsp` can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints. - 2. Correct inner-sorting within contiguous regions. Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. This property is established by the clock jump difference lookup argument. In a nutshell, every difference of consecutive clock cycles that a) occurs within one contiguous block of constant memory pointer, and b) is greater than 1, is shown itself to be a valid clock cycle through a separate cross-table argument. The construction is described in more details in [Memory Consistency](memory-consistency.md). +1. Contiguity of regions of constant memory pointer. + Since the memory pointer for the JumpStack table, `jsp` can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints. +2. Correct inner-sorting within contiguous regions. + Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. + This property is established by the clock jump difference [Lookup Argument](lookup-argument.md). + In a nutshell, every difference of consecutive clock cycles that occurs within one contiguous block of constant memory pointer is shown itself to be a valid clock cycle through a separate cross-table argument. # Arithmetic Intermediate Representation @@ -141,7 +144,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. Jump Stack Origin `jso` is 0. 1. Jump Stack Destination `jsd` is 0. 1. The running product for the permutation argument with the Processor Table `rppa` has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴. -1. The running product of clock jump differences `rpcjd` starts off with 1. +1. The running product of clock jump differences `ClockJumpDifferenceLookupClientLogDerivative` is 0. ### Initial Constraints as Polynomials @@ -150,7 +153,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `jso` 1. `jsd` 1. `rppa - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)` -1. `rpcjd - 1` +1. `ClockJumpDifferenceLookupClientLogDerivative` ## Consistency Constraints @@ -162,24 +165,18 @@ None. 1. (`jsp` does not change and `jso` does not change and `jsd` does not change and the cycle counter `clk` increases by 1), *or* 1. (`jsp` does not change and `jso` does not change and `jsd` does not change and the current instruction `ci` is `call`), *or* 1. (`jsp` does not change and the current instruction `ci` is `return`). -1. The clock jump difference inverse column `clk_di` is the inverse of the clock jump difference minus one if a) the clock jump difference is greater than 1, and b) the jump stack pointer remains the same. -1. If the memory pointer `jsp` does not change, then `clk_di` is the inverse-or-zero of the clock jump difference minus one. 1. The running product for the permutation argument `rppa` absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴. -1. The running product for clock jump differences `rpcjd` accumulates a factor `(clk' - clk - 1)` (relative to indeterminate `🚿`) if - a) the clock jump difference is greater than 1, and if - b) the jump stack pointer does not change; - and remains the same otherwise. +1. If the jump stack pointer `jsp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🧺. + Otherwise, it remains the same. Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. The jump stack pointer `jsp` increases by 1 or the jump stack pointer `jsp` does not change 1. The jump stack pointer `jsp` increases by 1 or the jump stack origin `jso` does not change or current instruction `ci` is `return` 1. The jump stack pointer `jsp` increases by 1 or the jump stack destination `jsd` does not change or current instruction `ci` is `return` 1. The jump stack pointer `jsp` increases by 1 or the cycle count `clk` increases by 1 or current instruction `ci` is `call` or current instruction `ci` is `return` -1. Either `jsp' - jsp = 1` or `clk_di` is the inverse of `clk' - clk - 1` (or 0 if no inverse exists). -1. `rppa' = rppa·(🧴 - a·clk' - b·ci' - c·jsp' - d·jsp' - e·jsd)` -1. `rpcjd' = rpcjd` and `(clk' - clk - 1) = 0`; - or `rpcjd' = rpcjd` and `jsp' ≠ jsp`; - or `rpcjd' = rpcjd·(🚿 - clk' + clk)` and `(clk' - clk - 1)·clk_di = 1` and `jsp' = jsp`. +1. `rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')` +1. - the `jsp` changes or the logarithmic derivative accumulates a summand, and + - the `jsp` does not change or the logarithmic derivative does not change. ### Transition Constraints as Polynomials @@ -189,8 +186,9 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. `(jsp' - (jsp + 1))·(clk' - (clk + 1))·(ci - op_code(call))·(ci - op_code(return))` 1. `clk_di·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))` 1. `(clk' - clk - one)·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))` -1. `rppa' - rppa·(🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)` -1. `(clk' - clk - 1)·(rpcjd' - rpcjd) + (jsp' - jsp - 1)·(rpcjd' - rpcjd) + (1 - (clk' - clk - 1)·clk_di)·(jsp' - jsp)·(rpcjd' - rpcjd·(🚿 - clk' + clk))` +1. `rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')` +1. `(jsp' - (jsp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🧺 - clk' + clk) - 1)`
+ `+ (jsp' - jsp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/operational-stack-table.md b/specification/src/operational-stack-table.md index dbee0e07c..07f202257 100644 --- a/specification/src/operational-stack-table.md +++ b/specification/src/operational-stack-table.md @@ -8,19 +8,18 @@ It is initially empty. ## Base Columns -The Operational Stack Table consists of 5 columns: +The Operational Stack Table consists of 4 columns: 1. the cycle counter `clk` -1. the inverse-or-zero of the difference between two consecutive `clk` values minus one, `clk_di`, 1. the shrink stack indicator `shrink_stack` 1. the operational stack value `osv`, and 1. the operational stack pointer `osp`. -| Clock | Inverse of Clock Difference Minus One | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value | -|:------|:--------------------------------------|:-----------------------|:-----------------|:---------------| -| - | - | - | - | - | +| Clock | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value | +|:------|:-----------------------|:-----------------|:---------------| +| - | - | - | - | Columns `clk`, `shrink_stack`, `osp`, and `osv` correspond to columns `clk`, `ib1`, `osp`, and `osv` in the [Processor Table](processor-table.md), respectively. -A Permutation Argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. +A [Permutation Argument](permutation-argument.md) with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. In order to guarantee [memory consistency](memory-consistency.md), the rows of the operational stack table are sorted by operational stack pointer `osp` first, cycle count `clk` second. The mechanics are best illustrated by an example. @@ -64,41 +63,41 @@ Execution trace: Operational Stack Table: -| `clk` | `clk_di` | `shrink_stack` | (comment) | `osp` | `osv` | -|------:|-----------------------:|---------------:|:----------|------:|------:| -| 0 | (23 - 0 - 1)${}^{-1}$ | 0 | (`push`) | 4 | 0 | -| 23 | (1 - 23 - 1)${}^{-1}$ | 1 | (`pop`) | 4 | 0 | -| 1 | (22 - 1 - 1)${}^{-1}$ | 0 | (`push`) | 5 | 0 | -| 22 | (2 - 22 - 1)${}^{-1}$ | 1 | (`pop`) | 5 | 0 | -| 2 | (21 - 2 - 1)${}^{-1}$ | 0 | (`push`) | 6 | 0 | -| 21 | (3 - 21 - 1)${}^{-1}$ | 1 | (`pop`) | 6 | 0 | -| 3 | (12 - 3 - 1)${}^{-1}$ | 0 | (`push`) | 7 | 0 | -| 12 | (20 - 12 - 1)${}^{-1}$ | 0 | (`push`) | 7 | 0 | -| 20 | (4 - 20 - 1)${}^{-1}$ | 1 | (`pop`) | 7 | 0 | -| 4 | (11 - 4 - 1)${}^{-1}$ | 0 | (`push`) | 8 | 0 | -| 11 | (13 - 11 - 1)${}^{-1}$ | 1 | (`pop`) | 8 | 0 | -| 13 | (14 - 13 - 1)${}^{-1}$ | 0 | (`swap`) | 8 | 0 | -| 14 | (19 - 14 - 1)${}^{-1}$ | 0 | (`push`) | 8 | 0 | -| 19 | (5 - 19 - 1)${}^{-1}$ | 1 | (`pop`) | 8 | 0 | -| 5 | (10 - 5 - 1)${}^{-1}$ | 0 | (`push`) | 9 | 42 | -| 10 | (15 - 10 - 1)${}^{-1}$ | 1 | (`pop`) | 9 | 99 | -| 15 | (16 - 15 - 1)${}^{-1}$ | 0 | (`swap`) | 9 | 77 | -| 16 | (18 - 16 - 1)${}^{-1}$ | 0 | (`push`) | 9 | 77 | -| 18 | (6 - 18 - 1)${}^{-1}$ | 1 | (`pop`) | 9 | 77 | -| 6 | (9 - 6 - 1)${}^{-1}$ | 0 | (`push`) | 10 | 43 | -| 9 | (17 - 9 - 1)${}^{-1}$ | 1 | (`pop`) | 10 | 43 | -| 17 | (7 - 17 - 1)${}^{-1}$ | 1 | (`pop`) | 10 | 78 | -| 7 | (8 - 7 - 1)${}^{-1}$ | 0 | (`nop`) | 11 | 44 | -| 8 | 0 | 1 | (`pop`) | 11 | 44 | +| `clk` | `shrink_stack` | (comment) | `osp` | `osv` | +|------:|---------------:|:----------|------:|------:| +| 0 | 0 | (`push`) | 4 | 0 | +| 23 | 1 | (`pop`) | 4 | 0 | +| 1 | 0 | (`push`) | 5 | 0 | +| 22 | 1 | (`pop`) | 5 | 0 | +| 2 | 0 | (`push`) | 6 | 0 | +| 21 | 1 | (`pop`) | 6 | 0 | +| 3 | 0 | (`push`) | 7 | 0 | +| 12 | 0 | (`push`) | 7 | 0 | +| 20 | 1 | (`pop`) | 7 | 0 | +| 4 | 0 | (`push`) | 8 | 0 | +| 11 | 1 | (`pop`) | 8 | 0 | +| 13 | 0 | (`swap`) | 8 | 0 | +| 14 | 0 | (`push`) | 8 | 0 | +| 19 | 1 | (`pop`) | 8 | 0 | +| 5 | 0 | (`push`) | 9 | 42 | +| 10 | 1 | (`pop`) | 9 | 99 | +| 15 | 0 | (`swap`) | 9 | 77 | +| 16 | 0 | (`push`) | 9 | 77 | +| 18 | 1 | (`pop`) | 9 | 77 | +| 6 | 0 | (`push`) | 10 | 43 | +| 9 | 1 | (`pop`) | 10 | 43 | +| 17 | 1 | (`pop`) | 10 | 78 | +| 7 | 0 | (`nop`) | 11 | 44 | +| 8 | 1 | (`pop`) | 11 | 44 | ## Extension Columns -The Op Stack Table has 2 extension columns, `rppa` and `rpcjd`. +The Op Stack Table has 2 extension columns, `rppa` and `ClockJumpDifferenceLookupClientLogDerivative`. 1. A Permutation Argument establishes that the rows of the Op Stack Table correspond to the rows of the [Processor Table](processor-table.md). The running product for this argument is contained in the `rppa` column. -1. In order to achieve [memory consistency](memory-consistency.md), a [multi-table Permutation Argument](memory-consistency.md#memory-like-tables) shows that all clock jump differences greater than one, from all memory-like tables (i.e., including the [RAM Table](random-access-memory-table.md) and the [JumpStack Table](jump-stack-table.md)), are contained in the `cjd` column of the [Processor Table](processor-table.md). - The running product for this argument is contained in the `rpcjd` column. +1. In order to achieve [memory consistency](memory-consistency.md), a [Lookup Argument](lookup-argument.md) shows that all clock jump differences are contained in the `clk` column of the [Processor Table](processor-table.md). + The logarithmic derivative for this argument is contained in the `ClockJumpDifferenceLookupClientLogDerivative` column. ## Padding @@ -116,11 +115,8 @@ Memory-consistency follows from two more primitive properties: Since the memory pointer for the Op Stack table, `osp` can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints. 2. Correct inner-sorting within contiguous regions. Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. - This property is established by the clock jump difference lookup argument. - In a nutshell, every difference of consecutive clock cycles that - a) occurs within one contiguous block of constant memory pointer, and - b) is greater than 1, is shown itself to be a valid clock cycle through a separate cross-table argument. - The construction is described in more details in [Memory Consistency](memory-consistency.md#memory-like-tables). + This property is established by the clock jump difference [Lookup Argument](lookup-argument.md). + In a nutshell, every difference of consecutive clock cycles that occurs within one contiguous block of constant memory pointer is shown itself to be a valid clock cycle through a separate cross-table argument. # Arithmetic Intermediate Representation @@ -134,7 +130,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `osv` is 0. 1. `osp` is the number of available stack registers, _i.e._, 16. 1. The running product for the permutation argument with the Processor Table `rppa` starts off having accumulated the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. -1. The running product of clock jump differences `rpcjd` starts off with 1. +1. The logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` is 0. ### Initial Constraints as Polynomials @@ -142,7 +138,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `osv` 1. `osp - 16` 1. `rppa - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒osv)` -1. `rpcjd - 1` +1. `ClockJumpDifferenceLookupClientLogDerivative` ## Consistency Constraints @@ -154,32 +150,26 @@ None. - the `osp` increases by 1, *or* - the `osp` does not change AND the `osv` does not change, *or* - the `osp` does not change AND the shrink stack indicator `shrink_stack` is 1. -1. The clock jump difference inverse column `clk_di` is the inverse of the clock jump difference minus one if a) the clock jump difference is greater than 1, and b) the op stack pointer remains the same. 1. The running product for the permutation argument with the Processor Table `rppa` absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. -1. The running product for clock jump differences `rpcjd` accumulates a factor `(clk' - clk)` (relative to indeterminate `🚿`) if - a) the clock jump difference is greater than 1, and if - b) the op stack pointer does not change; - and remains the same otherwise. +1. If the op stack pointer `osp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🪞. + Otherwise, it remains the same. Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. - the `osp` increases by 1 or the `osp` does not change - the `osp` increases by 1 or the `osv` does not change or the shrink stack indicator `shrink_stack` is 1 -1. `osp' - osp = 1` or `clk_di` is the multiplicative inverse of `(clk' - clk - 1)` or `0` if that inverse does not exist. 1. `rppa' = rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')` -1. `rpcjd' = rpcjd` and `(clk' - clk - 1) = 0`; - or `rpcjd' = rpcjd` and `osp' ≠ osp`; - or `rpcjd' = rpcjd·(🚿 - clk' + clk)` and `(clk' - clk - 1)·clk_di = 1` and `osp' = osp`. +1. - the `osp` changes or the logarithmic derivative accumulates a summand, and + - the `osp` does not change or the logarithmic derivative does not change. ### Transition Constraints as Polynomials 1. `(osp' - (osp + 1))·(osp' - osp)` 1. `(osp' - (osp + 1))·(osv' - osv)·(1 - shrink_stack)` -1. `clk_di·(osp' - osp - 1)·(1 - clk_di·(clk' - clk - one))` -1. `(clk' - clk - one)·(osp' - osp - 1)·(1 - clk_di·(clk' - clk - one))` 1. `rppa' - rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')` -1. `(clk' - clk - 1)·(rpcjd' - rpcjd) + (osp' - osp - 1)·(rpcjd' - rpcjd) + (1 - (clk' - clk - 1)·clk_di)·(osp' - osp)·(rpcjd' - rpcjd·(🚿 - clk' + clk))` +1. `(osp' - (osp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)`
+ `+ (osp' - osp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/processor-table.md b/specification/src/processor-table.md index b50c438c1..cef75e856 100644 --- a/specification/src/processor-table.md +++ b/specification/src/processor-table.md @@ -7,7 +7,7 @@ Each register is assigned a column in the processor table. ## Extension Colums -The Processor Table has 15 extension columns, corresponding to Evaluation Arguments and Permutation Arguments. +The Processor Table has 13 extension columns, corresponding to Evaluation Arguments and Permutation Arguments. Namely: 1. `RunningEvaluationStandardInput` for the Evaluation Argument with the input symbols. 1. `RunningEvaluationStandardOutput` for the Evaluation Argument with the output symbols. @@ -19,32 +19,25 @@ Namely: 1. `RunningEvaluationHashDigest` for the Evaluation Argument with the [Hash Table](hash-table.md) for copying the hash digest from the hash coprocessor to the processor. 1. `RunningEvaluationSponge` for the Evaluation Argument with the [Hash Table](hash-table.md) for copying the 10 next to-be-absorbed elements from the processor to the hash coprocessor or the 10 next squeezed elements from the hash coprocessor to the processor, depending on the instruction. 1. `RunningProductU32Table` for the Permutation Argument with the [U32 Table](u32-table.md). -1. `RunningProductAllClockJumpDifferences` for the [Multi-Table Set Equality argument](memory-consistency.md#clock-jump-differences-with-multiplicities-in-the-processor-table) with the [RAM Table](random-access-memory-table.md), the [JumpStack Table](jump-stack-table.md), and the [OpStack Table](operational-stack-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [OpStack Table](operational-stack-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [RAM Table](random-access-memory-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [JumpStack Table](jump-stack-table.md). -Lastly, extension columns `RunningEvaluationSelectedClockCycles` and `RunningEvaluationUniqueClockJumpDifferences` help achieving [memory consistency](memory-consistency.md#unique-clock-jump-differences-in-the-processor-table). ## Padding A padding row is a copy of the Processor Table's last row with the following modifications: -1. column `clk` is increased by 1, and -1. column `IsPadding` is set to 1. - -## Memory Consistency: Inner Sorting Argument - -In order to satisfy [Memory-Consistency](memory-consistency.md), the rows of memory-like tables (*i.e.*, [RAM Table](random-access-memory-table.md), [JumpStack Table](jump-stack-table.md), [OpStack Table](operational-stack-table.md)), need to be sorted in a special way. -In particular, the regions of constant memory pointer need to be contiguous; -and the rows in each such contiguous region must be sorted for clock cycle. -The contiguity of regions is trivial for the JumpStack and OpStack Table, and for the RAM Table the [Contiguity Argument](memory-consistency.md#contiguity-for-ram-table) establishes this fact. - -The [Inner Sorting Argument via Clock Jump Differences](memory-consistency.md#clock-jump-differences-and-inner-sorting) impacts the Processor Table quite substantially. -Concretely, the following 3 base columns and 3 extension columns only help achieving memory consistency. - -- Base column `cjd`, the list of all clock jump differences greater than 1 in all memory-like tables. -- Base column `invm`, the list of inverses of clock jump differences, counting multiplicities. This column helps to select all nonzero `cjd`'s. -- Base column `invu`, the list of inverses of unique clock jump differences, *i.e.*, without counting multiplicities. This column helps to select the unique nonzero `cjd`'s. -- Extension column `rer`, the running evaluation of relevant clock cycles. -- Extension column `reu`, the running evaluation of unique clock cycle differences. -- Extension column `rpm`, the running product of all clock jump differences, with multiplicities. +1. column `clk` is increased by 1, +1. column `IsPadding` is set to 1, +1. column `cjd_mul_op_stack` is set to 0, +1. column `cjd_mul_ram` is set to 0, and +1. column `cjd_mul_jump_stack` is set to 0. + +A notable exception: +if the row with `clk` equal to 1 is a padding row, then the values of `cjd_mul_op_stack`, `cjd_mul_ram`, and `cjd_mul_jump_stack` are not constrained in that row. +The reason for this exception is the lack of “awareness” of padding rows in the three memory-like tables. +In fact, all memory-like tables keep looking up clock jump differences in their padding section. +All these clock jumps are guaranteed to have magnitude 1 due to the [Permutation Arguments](permutation-argument.md) with the respective memory-like tables. # Arithmetic Intermediate Representation @@ -102,11 +95,9 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th 1. `RunningEvaluationHashDigest` is 1. 1. `RunningEvaluationSponge` is 1. 1. `RunningProductU32Table` is 1. -1. The running evaluation of relevant clock cycles is 1. -1. The running evaluation of unique clock jump differences starts off having applied one evaluation step with the clock jump difference with respect to indeterminate 🛒, if the `cjd` column does not start with zero. -1. The running product of all clock jump differences starts starts off having accumulated the first factor with respect to indeterminate 🚿, but only if the `cjd` column does not start with zero. - -(Note that the `cjd` column can start with a zero, but only if all other elements of this column are zero. This event indicates the absence of clock jumps.) +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` is 0. +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` is 0. +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` is 0. ### Initial Constraints as Polynomials @@ -147,28 +138,46 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th 1. `RunningEvaluationHashDigest - 1` 1. `RunningEvaluationSponge - 1` 1. `RunningProductU32Table - 1` -1. `rer - 1` -1. `cjd · (reu - 🛒 - cjd)) + (1 - cjd · invm) · (reu - 1)` -1. `cjd · (rpm - (🚿 - cjd)) + (1 - cjd · invm) · (rpm - 1)` +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` ## Consistency Constraints -1. The composition of instruction buckets `ib0` through `ib7` corresponds to the current instruction `ci`. -1. The inverse of clock jump difference with multiplicity `invm` is the inverse-or-zero of the the clock jump difference `cjd`. (Results in 2 polynomials.) +1. The composition of instruction bits `ib0` through `ib7` corresponds to the current instruction `ci`. +1. The instruction bit `ib0` is a bit. +1. The instruction bit `ib1` is a bit. +1. The instruction bit `ib2` is a bit. +1. The instruction bit `ib3` is a bit. +1. The instruction bit `ib4` is a bit. +1. The instruction bit `ib5` is a bit. +1. The instruction bit `ib6` is a bit. +1. The instruction bit `ib7` is a bit. 1. The padding indicator `IsPadding` is either 0 or 1. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Op Stack Table is 0. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Ram Table is 0. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Jump Stack Table is 0. ### Consistency Constraints as Polynomials 1. `ci - (2^7·ib7 + 2^6·ib6 + 2^5·ib5 + 2^4·ib4 + 2^3·ib3 + 2^2·ib2 + 2^1·ib1 + 2^0·ib0)` -1. `invm·(invm·cjd - 1)` -1. `cjd·(invm·cjd - 1)` +1. `ib0·(ib0 - 1)` +1. `ib1·(ib1 - 1)` +1. `ib2·(ib2 - 1)` +1. `ib3·(ib3 - 1)` +1. `ib4·(ib4 - 1)` +1. `ib5·(ib5 - 1)` +1. `ib6·(ib6 - 1)` +1. `ib7·(ib7 - 1)` 1. `IsPadding·(IsPadding - 1)` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeOpStack` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeRam` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeJumpStack` ## Transition Constraints Due to their complexity, instruction-specific constraints are defined [in their own section](instruction-specific-transition-constraints.md). - -The following constraints apply to every pair of rows. +The following additional constraints also apply to every pair of rows. 1. The cycle counter `clk` increases by 1. 1. The padding indicator `IsPadding` is 0 or remains unchanged. @@ -189,11 +198,9 @@ The following constraints apply to every pair of rows. 1. `st0` in the next row and `st1` in the current row as well as the constants `opcode(lt)` and `1` with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷. 1. `st0` in the current row and `st1` in the next row as well as `opcode(split)` with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷. 1. Else, _i.e._, if the current instruction is not a u32 instruction, the running product with the U32 Table remains unchanged. -1. The unique inverse column `invu'` holds the inverse-or-zero of the difference of consecutive `cjd`'s, if `cjd'` is nonzero. - (Results in 2 constraint polynomials.) -1. The running evaluation `reu` of unique `cjd`'s is updated relative to indeterminate 🛒 whenever the difference of `cjd`'s is nonzero *and* the next `cjd` is nonzero. -1. The running evaluation `rer` or relevant clock cycles is updated relative to indeterminate 🛒 or not at all. -1. The running product `rpm` of `cjd`'s with multiplicities is accumulates a factor `🚿 - cjd'` in every row, provided that `cjd'` is nonzero. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Op Stack Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🪞. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Ram Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🪑. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Jump Stack Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🧺. ### Transition Constraints as Polynomials @@ -224,18 +231,17 @@ The following constraints apply to every pair of rows. 1. `+ log_2_floor_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0'))` 1. `+ div_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split)))` 1. `+ (1 - ib2)·(RunningProductU32Table' - RunningProductU32Table)` -1. `invu'·(invu'·(cjd' - cjd) - 1)·cjd'` -1. `(cjd' - cjd)·(invu'·(cjd' - cjd) - 1)·cjd'` -1. `(1 - (cjd' - cjd)·invu)·(reu' - reu) + (1 - cjd'·invm)·(reu' - reu) + cjd'·(cjd' - cjd)·(reu' - 🛒·reu - cjd')` -1. `(rer' - rer·🛒 - clk')·(rer' - rer)` -1. `cjd'·(rpm' - rpm·(🚿 - cjd')) + (cjd'·invm' - 1)·(rpm' - rpm)` +1. `(ClockJumpDifferenceLookupServerLogDerivativeOpStack' - ClockJumpDifferenceLookupServerLogDerivativeOpStack)`
+ `·(🪞 - clk') - cjd_mul_op_stack'` +1. `(ClockJumpDifferenceLookupServerLogDerivativeRam' - ClockJumpDifferenceLookupServerLogDerivativeRam)`
+ `·(🪑 - clk') - cjd_mul_ram'` +1. `(ClockJumpDifferenceLookupServerLogDerivativeJumpStack' - ClockJumpDifferenceLookupServerLogDerivativeJumpStack)`
+ `·(🧺 - clk') - cjd_mul_jump_stack'` ## Terminal Constraints 1. In the last row, register “current instruction” `ci` is 0, corresponding to instruction `halt`. -1. In the last row, the running evaluations `rer` and `reu` are equal. ### Terminal Constraints as Polynomials 1. `ci` -1. `rer - reu` diff --git a/specification/src/random-access-memory-table.md b/specification/src/random-access-memory-table.md index 72a6816d5..ca8240b57 100644 --- a/specification/src/random-access-memory-table.md +++ b/specification/src/random-access-memory-table.md @@ -4,9 +4,8 @@ The RAM is accessible through `read_mem` and `write_mem` commands. ## Base Columns -The RAM Table has 8 columns: +The RAM Table has 7 columns: 1. the cycle counter `clk`, -1. the inverse-or-zero of clock cycle differences minus 1 `clk_di`, 1. the instruction executed in the previous clock cycle `previous_instruction`, 1. RAM address pointer `ramp`, 1. the value of the memory at that address `ramv`, @@ -14,9 +13,9 @@ The RAM Table has 8 columns: 1. Bézout coefficient polynomial coefficient 0 `bcpc0`, 1. Bézout coefficient polynomial coefficient 1 `bcpc1`, -| Clock | Inverse of Clock Difference Minus One | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bézout coefficient polynomial's coefficients 1 | -|:------|:--------------------------------------|:---------------------|:------------|:----------|:----------------------------------|:-----------------------------------------------|:-----------------------------------------------| -| - | - | - | - | - | - | - | - | +| Clock | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bézout coefficient polynomial's coefficients 1 | +|:------|:---------------------|:------------|:----------|:----------------------------------|:-----------------------------------------------|:-----------------------------------------------| +| - | - | - | - | - | - | - | Columns `clk`, `previous_instruction`, `ramp`, and `ramv` correspond to the columns of the same name in the [Processor Table](processor-table.md). A permutation argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. @@ -27,17 +26,14 @@ The function of `iord` is best explained in the context of sorting the RAM Table The Bézout coefficient polynomial coefficients `bcpc0` and `bcpc1` represent the coefficients of polynomials that are needed for the [contiguity argument](memory-consistency.md#contiguity-for-ram-table). This argument establishes that all regions of constant `ramp` are contiguous. -Column `clk_di` is used to discount clock cycle differences that are equal to one. -It is necessary to establish the [inner sorting](memory-consistency.md#clock-jump-differences-and-inner-sorting) by `clk` within contiguous regions of constant `ramp`. - ## Extension Columns -The RAM Table has 2 extension columns, `rppa` and `rpcjd`. +The RAM Table has 2 extension columns, `rppa` and `ClockJumpDifferenceLookupClientLogDerivative`. 1. A Permutation Argument establishes that the rows in the RAM Table correspond to the rows of the [Processor Table](processor-table.md), after selecting for columns `clk`, `ramp`, `ramv` in both tables. The running product for this argument is contained in the `rppa` column. -1. In order to achieve [memory consistency](memory-consistency.md), a [multi-table Permutation Argument](memory-consistency.md#memory-like-tables) shows that all clock jump differences greater than one, from all memory-like tables (i.e., including the [OpStack Table](operational-stack-table.md) and the [JumpStack Table](jump-stack-table.md)), are contained in the `cjd` column of the [Processor Table](processor-table.md). - The running product for this argument is contained in the `rpcjd` column. +1. In order to achieve [memory consistency](memory-consistency.md), a [Lookup Argument](lookup-argument.md) shows that all clock jump differences are contained in the `clk` column of the [Processor Table](processor-table.md). + The logarithmic derivative for this argument is contained in the `ClockJumpDifferenceLookupClientLogDerivative` column. ## Sorting Rows @@ -183,8 +179,8 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. The Bézout coefficient 1 `bc1` is equal to the first coefficient of the Bézout coefficient polynomial `bcpc1`. 1. The running product polynomial `rpp` starts with `🧼 - ramp`. 1. The formal derivative `fd` starts with 1. -1. The running product for clock jump differences `rpcjd` starts with 1. 1. The running product for the permutation argument with the Processor Table `rppa` has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. +1. The logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` is 0. ### Initial Constraints as Polynomials @@ -194,8 +190,8 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `bc1 - bcpc1` 1. `rpp - 🧼 + ramp` 1. `fd - 1` -1. `rpcjd - 1` 1. `rppa - 🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction` +1. `ClockJumpDifferenceLookupClientLogDerivative` ## Consistency Constraints @@ -208,9 +204,9 @@ None. 1. If the `ramp` does not change and `previous_instruction` in the next row is not `write_mem`, then the RAM value `ramv` does not change. 1. The Bézout coefficient polynomial coefficients are allowed to change only when the `ramp` changes. 1. The running product polynomial `rpp` accumulates a factor `(🧼 - ramp)` whenever `ramp` changes. -1. The clock difference inverse `clk_di` is the inverse-or-zero of the clock difference minus 1. -1. The running product for clock jump differences `rpcjd` accumulates a factor `(🚿 - clk' + clk)` whenever that difference is greater than one and `ramp` is the same. 1. The running product for the permutation argument with the Processor Table `rppa` absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. +1. If the RAM pointer `ramp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🪑. + Otherwise, it remains the same. Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. `iord` is 0 or `iord` is the inverse of `(ramp' - ramp)`. @@ -223,12 +219,9 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. the formal derivative `fd` applies the product rule of differentiation (as necessary). 1. Bézout coefficient 0 is evaluated correctly. 1. Bézout coefficient 1 is evaluated correctly. -1. `clk_di` is zero or the inverse of `(clk' - clk - 1)`. -1. `(clk' - clk - 1)` is zero or the inverse of `clk_di`. -1. `(clk' - clk - 1) ≠ 0` and `rpcjd' = rpcjd`; - or `ramp' - ramp ≠ 0` and `rpcjd' = rpcjd`; - or `(clk' - clk - 1) = 0` and `ramp' - ramp = 0` and `rpcjd' = rpcjd·(🚿 - clk' + clk)`. 1. `rppa' = rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')` +1. - the `ramp` changes or the logarithmic derivative accumulates a summand, and + - the `ramp` does not change or the logarithmic derivative does not change. ### Transition Constraints as Polynomials @@ -242,10 +235,9 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. `(iord·(ramp' - ramp) - 1)·(fd' - fd) + (ramp' - ramp)·(fd' - fd·(ramp'-🧼) - rpp)` 1. `(iord·(ramp' - ramp) - 1)·(bc0' - bc0) + (ramp' - ramp)·(bc0' - bc0·🧼 - bcpc0')` 1. `(iord·(ramp' - ramp) - 1)·(bc1' - bc1) + (ramp' - ramp)·(bc1' - bc1·🧼 - bcpc1')` -1. `clk_di·(clk_di·(clk' - clk - 1) - 1)` -1. `(clk' - clk - 1)·(clk_di·(clk' - clk - 1) - 1)` -1. `(clk' - clk - 1)·(rpcjd' - rpcjd) + (1 - (ramp' - ramp)·iord)·(rpcjd' - rpcjd) + (1 - (clk' - clk - 1)·clk_di)·ramp·(rpcjd' - rpcjd·(🚿 - clk' + clk))` 1. `rppa' - rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')` +1. `(iord·(ramp' - ramp) - 1)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪑 - clk' + clk) - 1)`
+ `+ (ramp' - ramp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/registers.md b/specification/src/registers.md index 228d40679..1bc155af0 100644 --- a/specification/src/registers.md +++ b/specification/src/registers.md @@ -4,24 +4,27 @@ This section covers all columns in the Protocol Table. Only a subset of these registers relate to the instruction set; the remaining registers exist only to enable an efficient arithmetization and are marked with an asterisk (\*). -| Register | Name | Purpose | -|:-----------------------|:-----------------------------|:-------------------------------------------------------------------------------------------------------------------| -| *`clk` | cycle counter | counts the number of cycles the program has been running for | -| *`IsPadding` | padding indicator | indicates whether current state is only recorded to improve on STARK's computational runtime | -| *`PreviousInstruction` | previous instruction | holds the opcode of the instruction executed in the previous clock cycle (or 0 if such cycle exists) | -| `ip` | instruction pointer | contains the memory address (in Program Memory) of the instruction | -| `ci` | current instruction register | contains the current instruction | -| `nia` | next instruction register | contains either the instruction at the next address in Program Memory, or the argument for the current instruction | -| *`ib0` through `ib7` | instruction bit | decomposition of the instruction's opcode used to keep the AIR degree low | -| `jsp` | jump stack pointer | contains the memory address (in jump stack memory) of the top of the jump stack | -| `jso` | jump stack origin | contains the value of the instruction pointer of the last `call` | -| `jsd` | jump stack destination | contains the argument of the last `call` | -| `st0` through `st15` | operational stack registers | contain explicit operational stack values | -| *`osp` | operational stack pointer | contains the OpStack address of the top of the operational stack | -| *`osv` | operational stack value | contains the (stack) memory value at the given address | -| *`hv0` through `hv3` | helper variable registers | helper variables for some arithmetic operations | -| *`ramp` | RAM pointer | contains an address pointing into the RAM | -| *`ramv` | RAM value | contains the value of the RAM element at the address currently held in `ramp` | +| Register | Name | Purpose | +|:-----------------------|:-----------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------| +| *`clk` | cycle counter | counts the number of cycles the program has been running for | +| *`IsPadding` | padding indicator | indicates whether current state is only recorded to improve on STARK's computational runtime | +| *`PreviousInstruction` | previous instruction | holds the opcode of the instruction executed in the previous clock cycle (or 0 if such cycle exists) | +| `ip` | instruction pointer | contains the memory address (in Program Memory) of the instruction | +| `ci` | current instruction register | contains the current instruction | +| `nia` | next instruction register | contains either the instruction at the next address in Program Memory, or the argument for the current instruction | +| *`ib0` through `ib7` | instruction bit | decomposition of the instruction's opcode used to keep the AIR degree low | +| `jsp` | jump stack pointer | contains the memory address (in jump stack memory) of the top of the jump stack | +| `jso` | jump stack origin | contains the value of the instruction pointer of the last `call` | +| `jsd` | jump stack destination | contains the argument of the last `call` | +| `st0` through `st15` | operational stack registers | contain explicit operational stack values | +| *`osp` | operational stack pointer | contains the OpStack address of the top of the operational stack | +| *`osv` | operational stack value | contains the (stack) memory value at the given address | +| *`hv0` through `hv3` | helper variable registers | helper variables for some arithmetic operations | +| *`ramp` | RAM pointer | contains an address pointing into the RAM | +| *`ramv` | RAM value | contains the value of the RAM element at the address currently held in `ramp` | +| *`cjd_mul_op_stack` | clock jump difference lookup multiplicity Op Stack | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [Op Stack Table](operational-stack-table.md) | +| *`cjd_mul_ram` | clock jump difference lookup multiplicity Ram | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [RAM Table](random-access-memory-table.md) | +| *`cjd_mul_jump_stack` | clock jump difference lookup multiplicity Jump Stack | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [Jump Stack Table](jump-stack-table.md) | ## Instruction