feat: introduce instruction sponge_absorb_mem

specification/src/arithmetization-overview.md

@@ -15,9 +15,9 @@
 | [CascadeTable](cascade-table.md)           |          6 |         2 |          12 |
 | [LookupTable](lookup-table.md)             |          4 |         2 |          10 |
 | [U32Table](u32-table.md)                   |         10 |         1 |          13 |
-| DegreeLowering                             |        217 |        36 |         325 |
+| DegreeLowering                             |        220 |        36 |         328 |
 | Randomizers                                |          0 |         1 |           3 |
-| **TOTAL**                                  |    **366** |    **86** |     **624** |
+| **TOTAL**                                  |    **369** |    **86** |     **627** |
 <!-- auto-gen info stop -->
 
 ## Constraints
@@ -50,7 +50,7 @@ After automatically lowering degree to 4:
 | table name                                     | #initial | #consistency | #transition | #terminal |
 |:-----------------------------------------------|---------:|-------------:|------------:|----------:|
 | [ProgramTable](program-table.md)               |        6 |            4 |          10 |         2 |
-| [ProcessorTable](processor-table.md)           |       31 |           10 |         252 |         1 |
+| [ProcessorTable](processor-table.md)           |       31 |           10 |         255 |         1 |
 | [OpStackTable](operational-stack-table.md)     |        3 |            0 |           5 |         0 |
 | [RamTable](random-access-memory-table.md)      |        7 |            0 |          13 |         1 |
 | [JumpStackTable](jump-stack-table.md)          |        6 |            0 |           6 |         0 |

specification/src/hash-table.md

@@ -5,6 +5,9 @@ Similarly, the Sponge instructions `sponge_init`, `sponge_absorb`, and `sponge_s
 The main processor achieves this by using a hash coprocessor.
 The Hash Table is part of the arithmetization of that coprocessor, the other two parts being the [Cascade Table](cascade-table.md) and the [Lookup Table](lookup-table.md).
 In addition to accelerating these [hashing instructions](instructions.md#hashing), the Hash Table helps with [program attestation](program-attestation.md) by hashing the [program](program-table.md).
+
+Note: the Hash Table is not “aware” of instruction `sponge_absorb_mem`.
+Instead, the processor requests a “regular” `sponge_absorb` from the Hash Table, fetching the to-be-absorbed elements from RAM instead of the stack.
 
 The arithmetization for instruction `hash`, the Sponge instructions `sponge_init`, `sponge_absorb`, and `sponge_squeeze`, and for program hashing are quite similar.
 The main differences are in updates to the `state` registers between executions of the pseudo-random permutation used in Triton VM, the permutation of [Tip5](https://eprint.iacr.org/2023/107.pdf).

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

@@ -587,6 +587,15 @@ Beyond that, correct transition is guaranteed by the [Hash Table](hash-table.md)
     `·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 8) - 🫒·st7')`<br/>
     `·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 9) - 🫒·st6')`
 
+## Instruction `sponge_absorb_mem`
+
+In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.
+Beyond that, correct transition is guaranteed by the [Hash Table](hash-table.md) and the [RAM Table](random-access-memory-table.md).
+
+### Description
+
+1. `st0` is incremented by 10.
+
 ## Instruction `sponge_squeeze`
 
 In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.

specification/src/instructions.md

@@ -75,21 +75,22 @@ For the benefit of clarity, the effect of every possible argument is given below
 
 ## Hashing
 
-| Instruction      | Opcode | old op stack    | new op stack   | Description                                                                                                                    |
-|:-----------------|-------:|:----------------|:---------------|:-------------------------------------------------------------------------------------------------------------------------------|
-| `hash`           |     18 | `_ jihgfedcba`  | `_ yxwvu`      | Hashes the stack's 10 top-most elements and puts their digest onto the stack, shrinking the stack by 5.                        |
-| `assert_vector`  |     26 | `_ edcba edcba` | `_ edcba`      | Assert equality of `st(i)` to `st(i+5)` for `0 <= i < 4`. Crashes the VM if any pair is unequal. Pops the 5 top-most elements. |
-| `sponge_init`    |     32 | `_`             | `_`            | Initializes (resets) the Sponge's state. Must be the first Sponge instruction executed.                                        |
-| `sponge_absorb`  |     34 | `_ _jihgfedcba` | `_`            | Absorbs the stack's ten top-most elements into the Sponge state.                                                               |
-| `sponge_squeeze` |     40 | `_`             | `_ zyxwvutsrq` | Squeezes the Sponge and pushes the 10 squeezed elements onto the stack.                                                        |
+| Instruction         | Opcode | old op stack    | new op stack    | Description                                                                                                                                                         |
+|:--------------------|-------:|:----------------|:----------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------|
+| `hash`              |     18 | `_ jihgfedcba`  | `_ yxwvu`       | Hashes the stack's 10 top-most elements and puts their digest onto the stack, shrinking the stack by 5.                                                             |
+| `assert_vector`     |     26 | `_ edcba edcba` | `_ edcba`       | Assert equality of `st(i)` to `st(i+5)` for `0 <= i < 4`. Crashes the VM if any pair is unequal. Pops the 5 top-most elements.                                      |
+| `sponge_init`       |     32 | `_`             | `_`             | Initializes (resets) the Sponge's state. Must be the first Sponge instruction executed.                                                                             |
+| `sponge_absorb`     |     34 | `_ jihgfedcba`  | `_`             | Absorbs the stack's ten top-most elements into the Sponge state.                                                                                                    |
+| `sponge_absorb_mem` |     40 | `_ dcba p`      | `_ hgfe (p+10)` | Absorbs the ten RAM elements at addresses `p`, `p+1`, … into the Sponge state. Overwrites stack elements `st1` through `st4` with the first four absorbed elements. |
+| `sponge_squeeze`    |     48 | `_`             | `_ zyxwvutsrq`  | Squeezes the Sponge and pushes the 10 squeezed elements onto the stack.                                                                                             |
 
 The instruction `hash` works as follows.
 The stack's 10 top-most elements (`jihgfedcba`) are popped from the stack, reversed, and concatenated with six zeros, resulting in `abcdefghij000000`.
 The Tip5 permutation is applied to `abcdefghij000000`, resulting in `αβγδεζηθικuvwxyz`.
 The first five elements of this result, i.e., `αβγδε`, are reversed and pushed to the stack.
 For example, the old stack was `_ jihgfedcba` and the new stack is `_ εδγβα`.
 
-The instructions `sponge_init`, `sponge_absorb`, and `sponge_squeeze` are the interface for using the Tip5 permutation in a [Sponge](https://keccak.team/sponge_duplex.html) construction.
+The instructions `sponge_init`, `sponge_absorb`, `sponge_absorb_mem`, and `sponge_squeeze` are the interface for using the Tip5 permutation in a [Sponge](https://keccak.team/sponge_duplex.html) construction.
 The capacity is never accessible to the program that's being executed by Triton VM.
 At any given time, at most one Sponge state exists.
 Only instruction `sponge_init` resets the state of the Sponge, and only the three Sponge instructions influence the Sponge's state.
@@ -103,7 +104,7 @@ Triton VM cannot know the number of elements that will be absorbed.
 |:------------|-------:|:-------------|:-------------|:---------------------------------------------------------------------------------------------------------------------------|
 | `add`       |     42 | `_ b a`      | `_ c`        | Computes the sum (`c`) of the top two elements of the stack (`b` and `a`) over the field.                                  |
 | `mul`       |     50 | `_ b a`      | `_ c`        | Computes the product (`c`) of the top two elements of the stack (`b` and `a`) over the field.                              |
-| `invert`    |     48 | `_ a`        | `_ b`        | Computes the multiplicative inverse (over the field) of the top of the stack. Crashes the VM if the top of the stack is 0. |
+| `invert`    |     56 | `_ a`        | `_ b`        | Computes the multiplicative inverse (over the field) of the top of the stack. Crashes the VM if the top of the stack is 0. |
 | `eq`        |     58 | `_ b a`      | `_ (a == b)` | Tests the top two stack elements for equality.                                                                             |
 
 ## Bitwise Arithmetic on Stack
@@ -139,9 +140,9 @@ Triton VM cannot know the number of elements that will be absorbed.
 
 | Instruction   | Opcode | old op stack    | new op stack                 | Description                                                                                                                                                                                                                                                                                                                                                                                       |
 |:--------------|:-------|:----------------|:-----------------------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
-| `merkle_step` | 64     | `_ i edcba`     | `_ (i div 2) zyxwv`          | Helps traversing a Merkle tree during authentication path verification. See extended description below.                                                                                                                                                                                                                                                                                           |
-| `xx_dot_step` | 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.                                                                    |
-| `xx_dot_step` | 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. |
+| `merkle_step` | 72     | `_ i edcba`     | `_ (i div 2) zyxwv`          | Helps traversing a Merkle tree during authentication path verification. See extended description below.                                                                                                                                                                                                                                                                                           |
+| `xx_dot_step` | 80     | `_ 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.                                                                    |
+| `xx_dot_step` | 88     | `_ 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. |
 
 The instruction `merkle_step` works as follows.
 The 6th element of the stack `i` is taken as the node index for a Merkle tree that is claimed to include data whose digest is the content of stack registers `st4` through `st0`, i.e., `edcba`.

specification/src/processor-table.md

@@ -145,7 +145,9 @@ The following additional constraints also apply to every pair of rows.
     1. Otherwise, it remains unchanged.
 1. If the current instruction is `hash` or `merkle_step`, 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 `sponge_init`, then the running evaluation “Sponge” absorbs the current instruction and the Sponge's default initial state with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽.
-    Else if the current instruction is `sponge_absorb` or `sponge_squeeze`, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽.
+    Else if the current instruction is `sponge_absorb`, then the running evaluation “Sponge” absorbs the current instruction and the current row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽.
+    Else if the current instruction is `sponge_squeeze`, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽.
+    Else if the current instruction is `sponge_absorb_mem`, then the running evaluation “Sponge” absorbs the opcode of instruction `sponge_absorb` and stack elements `st1` through `st4` and all 6 helper variables with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽.
     Otherwise, the running evaluation remains unchanged.
 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 🧷.

triton-vm/src/aet.rs

@@ -61,8 +61,9 @@ pub struct AlgebraicExecutionTrace {
     /// permutation for each round.
     pub hash_trace: Array2<BFieldElement>,
 
-    /// For the Sponge instructions, i.e., `sponge_init`, `sponge_absorb`, and `sponge_squeeze`,
-    /// the Sponge trace records the internal state of the Tip5 permutation for each round.
+    /// For the Sponge instructions, i.e., `sponge_init`, `sponge_absorb`,
+    /// `sponge_absorb_mem`, and `sponge_squeeze`, the Sponge trace records the
+    /// internal state of the Tip5 permutation for each round.
     pub sponge_trace: Array2<BFieldElement>,
 
     /// The u32 entries hold all pairs of BFieldElements that were written to the U32 Table,

triton-vm/src/instruction.rs

@@ -181,6 +181,7 @@ pub enum AnInstruction<Dest: PartialEq + Default> {
     AssertVector,
     SpongeInit,
     SpongeAbsorb,
+    SpongeAbsorbMem,
     SpongeSqueeze,
 
     // Base field arithmetic on stack
@@ -237,10 +238,11 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             AssertVector => 26,
             SpongeInit => 32,
             SpongeAbsorb => 34,
-            SpongeSqueeze => 40,
+            SpongeAbsorbMem => 40,
+            SpongeSqueeze => 48,
             Add => 42,
             Mul => 50,
-            Invert => 48,
+            Invert => 56,
             Eq => 58,
             Split => 4,
             Lt => 6,
@@ -252,13 +254,13 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             PopCount => 28,
             XxAdd => 66,
             XxMul => 74,
-            XInvert => 56,
+            XInvert => 64,
             XbMul => 82,
             ReadIo(_) => 49,
             WriteIo(_) => 19,
-            MerkleStep => 64,
-            XxDotStep => 72,
-            XbDotStep => 80,
+            MerkleStep => 72,
+            XxDotStep => 80,
+            XbDotStep => 88,
         }
     }
 
@@ -282,6 +284,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             AssertVector => "assert_vector",
             SpongeInit => "sponge_init",
             SpongeAbsorb => "sponge_absorb",
+            SpongeAbsorbMem => "sponge_absorb_mem",
             SpongeSqueeze => "sponge_squeeze",
             Add => "add",
             Mul => "mul",
@@ -355,6 +358,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             AssertVector => AssertVector,
             SpongeInit => SpongeInit,
             SpongeAbsorb => SpongeAbsorb,
+            SpongeAbsorbMem => SpongeAbsorbMem,
             SpongeSqueeze => SpongeSqueeze,
             Add => Add,
             Mul => Mul,
@@ -400,6 +404,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             AssertVector => -5,
             SpongeInit => 0,
             SpongeAbsorb => -10,
+            SpongeAbsorbMem => 0,
             SpongeSqueeze => 10,
             Add => -1,
             Mul => -1,
@@ -552,6 +557,7 @@ const fn all_instructions_without_args() -> [AnInstruction<BFieldElement>; Instr
         AssertVector,
         SpongeInit,
         SpongeAbsorb,
+        SpongeAbsorbMem,
         SpongeSqueeze,
         Add,
         Mul,

triton-vm/src/parser.rs

@@ -231,7 +231,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
     let call = call_instruction();
     let return_ = instruction("return", Return);
     let recurse = instruction("recurse", Recurse);
-    let assert_ = instruction("assert", Assert);
+    let assert = instruction("assert", Assert);
 
     let control_flow = alt((nop, skiz, call, return_, recurse, halt));
 
@@ -246,9 +246,10 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
     let assert_vector = instruction("assert_vector", AssertVector);
     let sponge_init = instruction("sponge_init", SpongeInit);
     let sponge_absorb = instruction("sponge_absorb", SpongeAbsorb);
+    let sponge_absorb_mem = instruction("sponge_absorb_mem", SpongeAbsorbMem);
     let sponge_squeeze = instruction("sponge_squeeze", SpongeSqueeze);
 
-    let hashing_related = alt((hash, sponge_init, sponge_absorb, sponge_squeeze));
+    let hashing_related = alt((hash, sponge_init, sponge_squeeze));
 
     // Arithmetic on stack instructions
     let add = instruction("add", Add);
@@ -291,12 +292,11 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
 
     let many_to_one = alt((merkle_step, xx_dot_step, xb_dot_step));
 
-    // Because of common prefixes, the following parsers are sensitive to order:
-    //
+    // Because of common prefixes, the following parsers are sensitive to order.
     // Successfully parsing "assert" before trying "assert_vector" can lead to
     // picking the wrong one. By trying them in the order of longest first, less
     // backtracking is necessary.
-    let syntax_ambiguous = alt((assert_vector, assert_));
+    let syntax_ambiguous = alt((assert_vector, assert, sponge_absorb_mem, sponge_absorb));
 
     alt((
         opstack_manipulation,