turn link between Processor Table and U32 Table into Lookup Argument

specification/src/processor-table.md

@@ -18,7 +18,7 @@ The Processor Table has the following extension columns, corresponding to [Evalu
 1. `RunningEvaluationHashInput` for the Evaluation Argument with the [Hash Table](hash-table.md) for copying the input to the hash function from the processor to the hash coprocessor.
 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. `U32LookupClientLogDerivative` for the Lookup Argument with the [U32 Table](u32-table.md).
 1. `ClockJumpDifferenceLookupServerLogDerivative` for the Lookup Argument of clock jump differences with the [OpStack Table](operational-stack-table.md), the [RAM Table](random-access-memory-table.md), and the [JumpStack Table](jump-stack-table.md).
 
 ## Padding
@@ -89,7 +89,7 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th
 1. `RunningEvaluationHashInput` has absorbed the first row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪 if the current instruction is `hash`. Otherwise, it is 1.
 1. `RunningEvaluationHashDigest` is 1.
 1. `RunningEvaluationSponge` is 1.
-1. `RunningProductU32Table` is 1.
+1. `U32LookupClientLogDerivative` is 0.
 1. `ClockJumpDifferenceLookupServerLogDerivative` is 0.
 
 ### Initial Constraints as Polynomials
@@ -130,7 +130,7 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th
     `+ hash_deselector·(RunningEvaluationHashInput - 🚪 - 🧄₀·st0 - 🧄₁·st1 - 🧄₂·st2 - 🧄₃·st3 - 🧄₄·st4 - 🧄₅·st5 - 🧄₆·st6 - 🧄₇·st7 - 🧄₈·st8 - 🧄₉·st9)`
 1. `RunningEvaluationHashDigest - 1`
 1. `RunningEvaluationSponge - 1`
-1. `RunningProductU32Table - 1`
+1. `U32LookupClientLogDerivative`
 1. `ClockJumpDifferenceLookupServerLogDerivative`
 
 ## Consistency Constraints
@@ -178,13 +178,13 @@ The following additional constraints also apply to every pair of rows.
 1. If the current instruction in the next row is `hash`, the running evaluation “Hash Input” absorbs the next row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪. Otherwise, it remains unchanged.
 1. If the current instruction is `hash`, the running evaluation “Hash Digest” absorbs the next row with respect to challenges 🧄₀ through 🧄₄ and indeterminate 🪟. Otherwise, it remains unchanged.
 1. If the current instruction is `absorb_init`, `absorb`, or `squeeze`, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, it remains unchanged.
-1.  1. If the current instruction is `split`, then the running product with the U32 Table absorbs `st0` and `st1` in the next row and `ci` in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
-    1. If the current instruction is `lt`, `and`, `xor`, or `pow`, then the running product with the U32 Table absorbs `st0`, `st1`, and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
-    1. If the current instruction is `log_2_floor`, then the running product with the U32 Table absorbs `st0` and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
-    1. If the current instruction is `div`, then the running product with the U32 Table absorbs both
+1.  1. If the current instruction is `split`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0` and `st1` in the next row and `ci` in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
+    1. If the current instruction is `lt`, `and`, `xor`, or `pow`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0`, `st1`, and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
+    1. If the current instruction is `log_2_floor`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0` and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
+    1. If the current instruction is `div`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates both
         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. Else, _i.e._, if the current instruction is not a u32 instruction, the logarithmic derivative for the Lookup Argument with the U32 Table remains unchanged.
 1. The running sum for the logarithmic derivative of the clock jump difference lookup argument accumulates the next row's `clk` with the appropriate multiplicity `cjd_mul` with respect to indeterminate 🪞.
 
 ### Transition Constraints as Polynomials
@@ -208,14 +208,18 @@ The following additional constraints also apply to every pair of rows.
 1. `(ci - opcode(absorb_init))·(ci - opcode(absorb)·(ci - opcode(squeeze))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)`<br />
     `+ (absorb_init_deselector + absorb_deselector + squeeze_deselector)`<br />
     `·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·ci - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')`
-1.  1. `split_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0' - 🌰·st1' - 🥑·ci))`
-    1. `+ lt_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0'))`
-    1. `+ and_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0'))`
-    1. `+ xor_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0'))`
-    1. `+ pow_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0'))`
-    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.  1. `split_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1' - 🥑·ci) - 1)`
+    1. `+ lt_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
+    1. `+ and_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
+    1. `+ xor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
+    1. `+ pow_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
+    1. `+ log_2_floor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)`
+    1. `+ div_deselector·(`<br />
+    &emsp;&emsp;`(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`<br />
+    &emsp;&emsp;`- (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)`<br />
+    &emsp;&emsp;`- (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`<br />
+    &emsp;`)`
+    1. `+ (1 - ib2)·(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)`
 1. `(ClockJumpDifferenceLookupServerLogDerivative' - ClockJumpDifferenceLookupServerLogDerivative)`<br />
     `·(🪞 - clk') - cjd_mul'`
 

specification/src/u32-table.md

@@ -14,17 +14,18 @@ Hence, the result of the instruction can be transferred into the processor withi
 
 ## Base Columns
 
-| name             | description                                                                                   |
-|:-----------------|:----------------------------------------------------------------------------------------------|
-| `CopyFlag`       | The row to be copied between processor and u32 coprocessor. Marks the beginning of a section. |
-| `CI`             | Current instruction, the instruction the processor is currently executing.                    |
-| `Bits`           | The number of bits that LHS and RHS have already been shifted by.                             |
-| `BitsMinus33Inv` | The inverse-or-zero of the difference between 33 and `Bits`.                                  |
-| `LHS`            | Left-hand side of the operation. Usually corresponds to the processor's `st0`.                |
-| `LhsInv`         | The inverse-or-zero of LHS. Needed to check whether `LHS` is unequal to 0.                    |
-| `RHS`            | Right-hand side of the operation. Usually corresponds to the processor's `st1`.               |
-| `RhsInv`         | The inverse-or-zero of RHS. Needed to check whether `RHS` is unequal to 0.                    |
-| `Result`         | The result (or intermediate result) of the instruction requested by the processor.            |
+| name                 | description                                                                                     |
+|:---------------------|:------------------------------------------------------------------------------------------------|
+| `CopyFlag`           | The row to be copied between processor and u32 coprocessor. Marks the beginning of a section.   |
+| `CI`                 | Current instruction, the instruction the processor is currently executing.                      |
+| `Bits`               | The number of bits that LHS and RHS have already been shifted by.                               |
+| `BitsMinus33Inv`     | The inverse-or-zero of the difference between 33 and `Bits`.                                    |
+| `LHS`                | Left-hand side of the operation. Usually corresponds to the processor's `st0`.                  |
+| `LhsInv`             | The inverse-or-zero of LHS. Needed to check whether `LHS` is unequal to 0.                      |
+| `RHS`                | Right-hand side of the operation. Usually corresponds to the processor's `st1`.                 |
+| `RhsInv`             | The inverse-or-zero of RHS. Needed to check whether `RHS` is unequal to 0.                      |
+| `Result`             | The result (or intermediate result) of the instruction requested by the processor.              |
+| `LookupMultiplicity` | The number of times the processor has executed the current instruction with the same arguments. |
 
 An example U32 Table follows.
 Some columns are omitted for presentation reasons.
@@ -98,8 +99,8 @@ It is impossible to create a valid proof of correct execution of Triton VM if `B
 
 ## Extension Columns
 
-The U32 Table has 1 extension column, `RunningProductProcessor`.
-It corresponds to the Permutation Argument with the [Processor Table](processor-table.md), establishing that whenever the processor executes a u32 instruction, the following holds:
+The U32 Table has 1 extension column, `U32LookupServerLogDerivative`.
+It corresponds to the [Lookup Argument](lookup-argument.md) with the [Processor Table](processor-table.md), establishing that whenever the processor executes a u32 instruction, the following holds:
 
 - the processor's requested left-hand side is copied into `LHS`,
 - the processor's requested right-hand side is copied into `RHS`,
@@ -123,13 +124,13 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{
 
 ## Initial Constraints
 
-1. If the `CopyFlag` is 0, then `RunningProductProcessor` is 1.
-Otherwise, the `RunningProductProcessor` has absorbed the first row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
+1. If the `CopyFlag` is 0, then `U32LookupServerLogDerivative` is 0.
+Otherwise, the `U32LookupServerLogDerivative` has accumulated the first row with multiplicity `LookupMultiplicity` and with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
 
 ### Initial Constraints as Polynomials
 
-1. `(CopyFlag - 1)·(RunningProductProcessor - 1)`<br />
-    `+ CopyFlag·(RunningProductProcessor - (🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result))`
+1. `(CopyFlag - 1)·U32LookupServerLogDerivative`<br />
+    `+ CopyFlag·(U32LookupServerLogDerivative·(🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result) - LookupMultiplicity)`
 
 ## Consistency Constraints
 
@@ -148,6 +149,7 @@ Otherwise, the `RunningProductProcessor` has absorbed the first row with respect
 1. If the current instruction is `log_2_floor`, then `RHS` is 0.
 1. If `CopyFlag` is 0 and the current instruction is `log_2_floor` and `LHS` is 0, then `Result` is -1.
 1. If `CopyFlag` is 1 and the current instruction is `log_2_floor` and `LHS` is 0, the VM crashes.
+1. If `CopyFlag` is 0, then `LookupMultiplicity` is 0.
 
 Written in Disjunctive Normal Form, the same constraints can be expressed as:
 
@@ -166,6 +168,7 @@ Written in Disjunctive Normal Form, the same constraints can be expressed as:
 1. `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `pow` or `RHS` is 0.
 1. `CopyFlag` is 1 or `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `pow` or `LHS` is not 0 or `Result` is -1.
 1. `CopyFlag` is 0 or `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `pow` or `LHS` is not 0.
+1. `CopyFlag` is 1 or `LookupMultiplicity` is 0.
 
 ### Consistency Constraints as Polynomials
 
@@ -184,6 +187,7 @@ Written in Disjunctive Normal Form, the same constraints can be expressed as:
 1. `(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(pow))·RHS`
 1. `(CopyFlag - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(pow))·(1 - LHS·LhsInv)·(Result + 1)`
 1. `CopyFlag·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(pow))·(1 - LHS·LhsInv)`
+1. `(CopyFlag - 1)·LookupMultiplicity`
 
 ## Transition Constraints
 
@@ -211,8 +215,8 @@ These aliases, _i.e._, `LhsLsb` := `LHS - 2·LHS'` and `RhsLsb` := `RHS - 2·RHS
 1. If the `CopyFlag` in the next row is 0 and the current instruction is `pow`, then `LHS` remains unchanged.
 1. If the `CopyFlag` in the next row is 0 and the current instruction is `pow` and `RhsLsb` in the current row is 0, then `Result` in the current row is `Result` in the next row squared.
 1. If the `CopyFlag` in the next row is 0 and the current instruction is `pow` and `RhsLsb` in the current row is 1, then `Result` in the current row is `Result` in the next row squared times `LHS` in the current row.
-1. If the `CopyFlag` in the next row is 0, then `RunningProductProcessor` in the next row is `RunningProductProcessor` in the current row.
-1. If the `CopyFlag` in the next row is 1, then `RunningProductProcessor` in the next row has absorbed the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
+1. If the `CopyFlag` in the next row is 0, then `U32LookupServerLogDerivative` in the next row is `U32LookupServerLogDerivative` in the current row.
+1. If the `CopyFlag` in the next row is 1, then `U32LookupServerLogDerivative` in the next row has accumulated the next row with multiplicity `LookupMultiplicity` and with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
 
 Written in Disjunctive Normal Form, the same constraints can be expressed as:
 
@@ -236,8 +240,8 @@ Written in Disjunctive Normal Form, the same constraints can be expressed as:
 1. `CopyFlag`' is 1 or `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `log_2_floor` or `LHS`' is `LHS`.
 1. `CopyFlag`' is 1 or `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `log_2_floor` or `RhsLsb` is 1 or `Result` is `Result`' times `Result`'.
 1. `CopyFlag`' is 1 or `CI` is the opcode of `split`, `lt`, `and`, `xor`, or `log_2_floor` or `RhsLsb` is 0 or `Result` is `Result`' times `Result`' times `LHS`.
-1. `CopyFlag`' is 1 or `RunningProductProcessor`' is `RunningProductProcessor`.
-1. `CopyFlag`' is 0 or `RunningProductProcessor`' is `RunningProductProcessor` times `(🧷 - 🥜·LHS' - 🌰·RHS' - 🥑·CI' - 🥕·Result')`.
+1. `CopyFlag`' is 1 or `U32LookupServerLogDerivative`' is `U32LookupServerLogDerivative`.
+1. `CopyFlag`' is 0 or the difference of `U32LookupServerLogDerivative`' and `U32LookupServerLogDerivative` times `(🧷 - 🥜·LHS' - 🌰·RHS' - 🥑·CI' - 🥕·Result')` is `LookupMultiplicity`'.
 
 ### Transition Constraints as Polynomials
 
@@ -261,8 +265,8 @@ Written in Disjunctive Normal Form, the same constraints can be expressed as:
 1. `(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(log_2_floor))·(LHS' - LHS)`
 1. `(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(log_2_floor))·(RhsLsb - 1)·(Result - Result'·Result')`
 1. `(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(xor))·(CI - opcode(log_2_floor))·(RhsLsb - 0)·(Result - Result'·Result'·LHS)`
-1. `(CopyFlag' - 1)·(RunningProductProcessor' - RunningProductProcessor)`
-1. `(CopyFlag' - 0)·(RunningProductProcessor' - RunningProductProcessor·(🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result))`
+1. `(CopyFlag' - 1)·(U32LookupServerLogDerivative' - U32LookupServerLogDerivative)`
+1. `(CopyFlag' - 0)·((U32LookupServerLogDerivative' - U32LookupServerLogDerivative)·(🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result) - LookupMultiplicity')`
 
 ## Terminal Constraints
 

triton-vm/src/table/cross_table_argument.rs

@@ -185,8 +185,8 @@ impl Evaluable for GrandCrossTableArg {
         let sponge = ext_row[ProcessorExtTableColumn::SpongeEvalArg.master_ext_table_index()]
             - ext_row[HashExtTableColumn::SpongeRunningEvaluation.master_ext_table_index()];
         let processor_to_u32 = ext_row
-            [ProcessorExtTableColumn::U32TablePermArg.master_ext_table_index()]
-            - ext_row[U32ExtTableColumn::ProcessorPermArg.master_ext_table_index()];
+            [ProcessorExtTableColumn::U32LookupClientLogDerivative.master_ext_table_index()]
+            - ext_row[U32ExtTableColumn::LookupServerLogDerivative.master_ext_table_index()];
         let clock_jump_difference_lookup = ext_row
             [ProcessorExtTableColumn::ClockJumpDifferenceLookupServerLogDerivative
                 .master_ext_table_index()]

triton-vm/src/table/master_table.rs

@@ -336,7 +336,8 @@ impl MasterBaseTable {
 
     pub fn u32_table_length(aet: &AlgebraicExecutionTrace) -> usize {
         aet.u32_entries
-            .iter()
+            .keys()
+            .into_iter()
             .map(|(instruction, lhs, rhs)| match instruction {
                 // for instruction `pow`, the left-hand side doesn't change between rows
                 Instruction::Pow => rhs.value(),