feat: introduce instruction for dot product

The new instructions `xxdotstep` and `xbdotstep` simplify computing
the dot product of two vectors.

The `xx` variant reads two extension field elements from RAM located at
the addresses corresponding to the two top stack elements, multiplies
the extension field elements, and adds the product to an accumulator
located on stack immediately below the two pointers.

The `xb` variant reads one base field element from RAM located at the
addresses corresponding to the top of the stack, one extension field
element from RAM located at the address of the second stack element,
multiplies the field elements, and adds the product to an accumulator
located on stack immediately below the two pointers.

Both instructions increases the respective pointers by the number of
words read.

constraint-evaluation-generator/src/constraints.rs

@@ -108,13 +108,6 @@ impl Constraints {
         .concat()
     }
 
-    pub fn fold_constants(&mut self) {
-        ConstraintCircuitMonad::constant_folding(&mut self.init);
-        ConstraintCircuitMonad::constant_folding(&mut self.cons);
-        ConstraintCircuitMonad::constant_folding(&mut self.tran);
-        ConstraintCircuitMonad::constant_folding(&mut self.term);
-    }
-
     pub fn lower_to_target_degree_through_substitutions(&mut self) -> AllSubstitutions {
         // Subtract the degree lowering table's width from the total number of columns to guarantee
         // the same number of columns even for repeated runs of the constraint evaluation generator.

constraint-evaluation-generator/src/main.rs

@@ -13,7 +13,6 @@ mod substitution;
 
 fn main() {
     let mut constraints = Constraints::all();
-    constraints.fold_constants();
     let substitutions = constraints.lower_to_target_degree_through_substitutions();
     let degree_lowering_table_code = substitutions.generate_degree_lowering_table_code();
 
@@ -45,7 +44,6 @@ mod tests {
     #[test]
     fn degree_lowering_tables_code_can_be_generated_for_test_constraints() {
         let mut constraints = Constraints::test_constraints();
-        constraints.fold_constants();
         let substitutions = constraints.lower_to_target_degree_through_substitutions();
         let _ = substitutions.generate_degree_lowering_table_code();
     }
@@ -58,15 +56,13 @@ mod tests {
     #[test]
     fn degree_lowering_tables_code_can_be_generated_from_all_constraints() {
         let mut constraints = Constraints::all();
-        constraints.fold_constants();
         let substitutions = constraints.lower_to_target_degree_through_substitutions();
         let _ = substitutions.generate_degree_lowering_table_code();
     }
 
     #[test]
     fn constraints_and_substitutions_can_be_combined() {
         let mut constraints = Constraints::test_constraints();
-        constraints.fold_constants();
         let substitutions = constraints.lower_to_target_degree_through_substitutions();
         let _ = constraints.combine_with_substitution_induced_constraints(substitutions);
     }

specification/src/instruction-specific-transition-constraints.md

@@ -796,7 +796,6 @@ In addition to its [instruction groups](instruction-groups.md), this instruction
 ### Description
 
 1. Numerator is quotient times denominator plus remainder: `n == q·d + r`.
-1. Stack element `st2` does not change.
 
 ### Polynomials
 
@@ -991,3 +990,25 @@ In addition to its [instruction groups](instruction-groups.md), this instruction
     `+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2)`<br />
     `+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3)`<br />
     `+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3) - st4)`
+
+## Instruction `xxdotstep`
+
+In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.
+
+### Description
+
+1. Store `(RAM[st0], RAM[st0+1], RAM[st0+2])` in `(hv0, hv1, hv2)`.
+1. Store `(RAM[st1], RAM[st1+1], RAM[st1+2])` in `(hv3, hv4, hv5)`.
+1. Add `(hv0 + hv1·x + hv2·x²) · (hv3 + hv4·x + hv5·x²)` into `(st2, st3, st4)`
+1. Increase the pointers: `st0` and `st1` by 3 each.
+
+## Instruction `xbdotstep`
+
+In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.
+
+### Description
+
+1. Store `RAM[st0]` in `hv0`.
+1. Store `(RAM[st1], RAM[st1+1], RAM[st1+2])` in `(hv1, hv2, hv3)`.
+1. Add `hv0 · (hv1 + hv2·x + hv3·x²)` into `(st1, st2, st3)`
+1. Increase the pointers: `st0` and `st1` by 1 and 3, respectively.

specification/src/instructions.md

@@ -146,3 +146,10 @@ Triton VM cannot know the number of elements that will be absorbed.
 |:-----------------|-------:|:----------------|:----------------|:-----------------------------------------------------------------------------------------|
 | `read_io` + `n`  |     49 | e.g., `_`       | e.g., `_ c b a` | Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5 |
 | `write_io` + `n` |     19 | e.g., `_ c b a` | e.g., `_`       | Pops `n` elements from the stack and writes them to standard output. 1 ⩽ `n` ⩽ 5         |
+
+## Many-In-One
+
+| Instruction | Opcode | old op stack    | new op stack                 | Description |
+|:------------|--------|:----------------|:-----------------------------|-------------|
+| `xxdotstep` | 72     | `_ z y x *b *a` | `_ z+p2 y+p1 x+p0 *b+3 *a+3` | Reads two extension field elements from RAM located at the addresses corresponding to the two top stack elements, multiplies the extension field elements, and adds the product `(p0, p1, p2)` to an accumulator located on stack immediately below the two pointers. Also, increase the pointers by the number of words read. |
+| `xxdotstep` | 80     | `_ z y x *b *a` | `_ z+p2 y+p1 x+p0 *b+3 *a+1` | Reads one base field element from RAM located at the addresses corresponding to the top of the stack, one extension field element from RAM located at the address of the second stack element, multiplies the field elements, and adds the product `(p0, p1, p2)` to an accumulator located on stack immediately below the two pointers. Also, increase the pointers by the number of words read. |

specification/src/isa.md

@@ -5,6 +5,8 @@ It is a [Harvard architecture](https://en.wikipedia.org/wiki/Harvard_architectur
 The arithmetization of the VM is defined over the *B-field* $\mathbb{F}_p$ where $p$ is the Oxfoi prime, _i.e._, $2^{64}-2^{32}+1$.[^oxfoi]
 This means the registers and memory elements take values from $\mathbb{F}_p$, and the transition function gives rise to low-degree transition verification polynomials from the ring of multivariate polynomials over $\mathbb{F}_p$.
 
+At certain points in the course of arithmetization we need an extension field over $\mathbb{F}_p$ to ensure sufficient soundness. To this end we use $\mathbb{F}_{p^3} = \frac{\mathbb{F}_p[X]}{\langle X^3 -X +1 \rangle}$, _i.e._, the quotient ring of remainders of polynomials after division by the *Shah* polynomial, $X^3 -X +1$. We refer to this field as the *X-field* for short, and its elements as *X-field elements*.
+
 Instructions have variable width:
 they either consist of one word, i.e., one B-field element, or of two words, i.e., two B-field elements.
 An example for a single-word instruction is `add`, adding the two elements on top of the stack, leaving the result as the new top of the stack.

specification/src/processor-table.md

@@ -26,7 +26,7 @@ The Processor Table has the following extension columns, corresponding to [Evalu
 1. `RunningEvaluationStandardOutput` for the Evaluation Argument with the output symbols.
 1. `InstructionLookupClientLogDerivative` for the Lookup Argument with the [Program Table](program-table.md)
 1. `RunningProductOpStackTable` for the Permutation Argument with the [Op Stack Table](operational-stack-table.md).
-1. `RunningProductRamTable` for the Permutation Argument with the [RAM Table](random-access-memory-table.md).
+1. `RunningProductRamTable` for the Permutation Argument with the [RAM Table](random-access-memory-table.md). Note that virtual column `instruction_type` holds value 1 for reads and 0 for writes.
 1. `RunningProductJumpStackTable` for the Permutation Argument with the [Jump Stack Table](jump-stack-table.md).
 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.
@@ -112,7 +112,7 @@ See [program attestation](program-attestation.md) for more details.
 1. `RunningEvaluationHashDigest` is 1.
 1. `RunningEvaluationSponge` is 1.
 1. `U32LookupClientLogDerivative` is 0.
-1. `ClockJumpDifferenceLookupServerLogDerivative` is 0.
+1. `ClockJumpDifferenceLookupServerLogDerivative` starts having accumulated the first contribution.
 
 ### Initial Constraints as Polynomials
 
@@ -138,14 +138,14 @@ See [program attestation](program-attestation.md) for more details.
 1. `RunningEvaluationStandardOutput - 1`
 1. `InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1`
 1. `RunningProductOpStackTable - 1`
-1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction)`
+1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·instruction_type)`
 1. `RunningProductJumpStackTable - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)`
 1. `(ci - opcode(hash))·(RunningEvaluationHashInput - 1)`<br />
     `+ hash_deselector·(RunningEvaluationHashInput - 🚪 - 🧄₀·st0 - 🧄₁·st1 - 🧄₂·st2 - 🧄₃·st3 - 🧄₄·st4 - 🧄₅·st5 - 🧄₆·st6 - 🧄₇·st7 - 🧄₈·st8 - 🧄₉·st9)`
 1. `RunningEvaluationHashDigest - 1`
 1. `RunningEvaluationSponge - 1`
 1. `U32LookupClientLogDerivative`
-1. `ClockJumpDifferenceLookupServerLogDerivative`
+1. `ClockJumpDifferenceLookupServerLogDerivative · 🪞 - cjd_mul` (Recall that `(🪞 - clk) = 🪞` because `clk = 0`.)
 
 ## Consistency Constraints
 

specification/src/random-access-memory-table.md

@@ -166,7 +166,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{
 1. `bc1 - bcpc1`
 1. `RunningProductOfRAMP - 🧼 + ram_pointer`
 1. `FormalDerivative - 1`
-1. `(RunningProductPermArg - 🛋 - 🍍·clk - 🍈·ram_pointer - 🍎·ram_value - 🌽·previous_instruction)·(instruction_type - 2)`<br />
+1. `(RunningProductPermArg - 🛋 - 🍍·clk - 🍈·ram_pointer - 🍎·ram_value - 🌽·instruction_type)·(instruction_type - 2)`<br />
     `(RunningProductPermArg - 1)·(instruction_type - 1)·(instruction_type - 0)`
 1. `ClockJumpDifferenceLookupClientLogDerivative`
 
@@ -211,7 +211,7 @@ None.
      `+ (ram_pointer' - ram_pointer)·(bc0' - bc0·🧼 - bcpc0')`
 1. `(iord·(ram_pointer' - ram_pointer) - 1)·(bc1' - bc1)`<br />
      `+ (ram_pointer' - ram_pointer)·(bc1' - bc1·🧼 - bcpc1')`
-1. `(RunningProductPermArg' - RunningProductPermArg·(🛋 - 🍍·clk' - 🍈·ram_pointer' - 🍎·ram_value' - 🌽·previous_instruction'))·(instruction_type' - 2)`<br />
+1. `(RunningProductPermArg' - RunningProductPermArg·(🛋 - 🍍·clk' - 🍈·ram_pointer' - 🍎·ram_value' - 🌽·instruction_type'))·(instruction_type' - 2)`<br />
     `(RunningProductPermArg' - RunningProductPermArg)·(instruction_type - 1)·(instruction_type - 0))`
 1. `(iord·(ram_pointer' - ram_pointer) - 1)·(instruction_type' - 2)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)`<br />
     `+ (ram_pointer' - ram_pointer)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)`<br />

specification/src/registers.md

@@ -55,6 +55,8 @@ Because they are only needed for some instructions, the helper variables are not
 For instruction group [`decompose_arg`](instruction-groups.md#group-decompose_arg) and instructions
 [`skiz`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-skiz),
 [`divine_sibling`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-divine_sibling),
-[`split`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-split), and
+[`split`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-split),
 [`eq`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-eq),
+[`xxdotstep`](instruction-specific-transition-constraints.md#instruction-xxdotstep), and
+[`xbdotstep`](instruction-specific-transition-constraints.md#instruction-xbdotstep),
 the behavior is defined in the respective sections.

triton-vm/src/instruction.rs

@@ -209,6 +209,10 @@ pub enum AnInstruction<Dest: PartialEq + Default> {
     // Read/write
     ReadIo(NumberOfWords),
     WriteIo(NumberOfWords),
+
+    // Many-in-One
+    XxDotStep,
+    XbDotStep,
 }
 
 impl<Dest: PartialEq + Default> AnInstruction<Dest> {
@@ -253,6 +257,8 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             XbMul => 82,
             ReadIo(_) => 49,
             WriteIo(_) => 19,
+            XxDotStep => 72,
+            XbDotStep => 80,
         }
     }
 
@@ -296,6 +302,8 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             XbMul => "xbmul",
             ReadIo(_) => "read_io",
             WriteIo(_) => "write_io",
+            XxDotStep => "xxdotstep",
+            XbDotStep => "xbdotstep",
         }
     }
 
@@ -367,6 +375,8 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             XbMul => XbMul,
             ReadIo(x) => ReadIo(*x),
             WriteIo(x) => WriteIo(*x),
+            XxDotStep => XxDotStep,
+            XbDotStep => XbDotStep,
         }
     }
 
@@ -410,6 +420,8 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             XbMul => -1,
             ReadIo(n) => n.num_words() as i32,
             WriteIo(n) => -(n.num_words() as i32),
+            XxDotStep => 0,
+            XbDotStep => 0,
         }
     }
 
@@ -560,6 +572,8 @@ const fn all_instructions_without_args() -> [AnInstruction<BFieldElement>; Instr
         XbMul,
         ReadIo(N1),
         WriteIo(N1),
+        XxDotStep,
+        XbDotStep,
     ]
 }
 

triton-vm/src/parser.rs

@@ -285,6 +285,12 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
 
     let read_write = alt((read_io, write_io));
 
+    // Many-in-One
+    let xxdotstep = instruction("xxdotstep", XxDotStep);
+    let xbdotstep = instruction("xbdotstep", XbDotStep);
+
+    let many_to_one = alt((xxdotstep, xbdotstep));
+
     // Because of common prefixes, the following parsers are sensitive to order:
     //
     // Successfully parsing "assert" before trying "assert_vector" can lead to
@@ -300,6 +306,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
         arithmetic_on_stack,
         read_write,
         syntax_ambiguous,
+        many_to_one,
     ))(s)
 }
 

triton-vm/src/stark.rs

@@ -2053,6 +2053,34 @@ pub(crate) mod tests {
         triton_constraints_evaluate_to_zero(property_based_test_program_for_random_ram_access())
     }
 
+    #[test]
+    fn constraints_evaluate_to_zero_on_property_based_test_program_for_xxdotstep() {
+        triton_constraints_evaluate_to_zero(property_based_test_program_for_xxdotstep());
+    }
+
+    #[test]
+    fn constraints_evaluate_to_zero_on_property_based_test_program_for_xbdotstep() {
+        triton_constraints_evaluate_to_zero(property_based_test_program_for_xbdotstep());
+    }
+
+    #[test]
+    fn can_read_twice_from_same_ram_address_within_one_cycle() {
+        for i in 0..=2 {
+            // This program reads from the same address twice, even if the stack
+            // is not well-initialized.
+            let program = triton_program! {
+                dup 0
+                push {i} add
+                xxdotstep
+                halt
+            };
+            let result = program.run(PublicInput::default(), NonDeterminism::default());
+            assert!(result.is_ok());
+            let program_and_input = ProgramAndInput::new(program);
+            triton_constraints_evaluate_to_zero(program_and_input);
+        }
+    }
+
     #[test]
     fn claim_in_ram_corresponds_to_currently_running_program() {
         triton_constraints_evaluate_to_zero(