diff --git a/specification/src/instruction-groups.md b/specification/src/instruction-groups.md index c3ccf56c4..86931bf21 100644 --- a/specification/src/instruction-groups.md +++ b/specification/src/instruction-groups.md @@ -9,23 +9,23 @@ Continuing above example, instruction group `keep_jump_stack` contains all trans The next section treats each instruction group in detail. The following table lists and briefly explains all instruction groups. -| group name | description | -|:-------------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| `decompose_arg` | instruction's argument held in `nia` is binary decomposed into helper registers `hv0` through `hv3` | -| `prohibit_illegal_num_words` | constrain the instruction's argument `n` to 1 ⩽ `n` ⩽ 5 | -| `no_io` | the running evaluations for public input & output remain unchanged | -| `no_ram` | RAM is not being accessed, _i.e._, the running product of the [Permutation Argument](permutation-argument.md) with the RAM Table remains unchanged | -| `keep_jump_stack` | jump stack does not change, _i.e._, registers `jsp`, `jso`, and `jsd` do not change | -| `step_1` | jump stack does not change and instruction pointer `ip` increases by 1 | -| `step_2` | jump stack does not change and instruction pointer `ip` increases by 2 | -| `grow_op_stack` | op stack elements are shifted down by one position, top element of the resulting stack is unconstrained | -| `grow_op_stack_by_any_of` | op stack elements are shifted down by `n` positions, top `n` elements of the resulting stack are unconstrained, where `n` is the instruction's argument | -| `keep_op_stack_height` | the op stack height remains unchanged, and so in particular the running product of the [Permutation Argument](permutation-argument.md) with the Op Stack table remains unchanged | -| `op_stack_remains_except_top_n_elements_unconstrained` | all but the top `n` elements of the op stack remain unchanged | -| `keep_op_stack` | op stack remains entirely unchanged | -| `binary_operation` | op stack elements starting from `st2` are shifted up by one position, highest two elements of the resulting stack are unconstrained | -| `shrink_op_stack` | op stack elements starting from `st1` are shifted up by one position | -| `shrink_op_stack_by_any_of` | op stack elements starting from `stn` are shifted up by one position, where `n` is the instruction's argument | +| group name | description | +|:--------------------------------|:---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| `decompose_arg` | instruction's argument held in `nia` is binary decomposed into helper registers `hv0` through `hv3` | +| `prohibit_illegal_num_words` | constrain the instruction's argument `n` to 1 ⩽ `n` ⩽ 5 | +| `no_io` | the running evaluations for public input & output remain unchanged | +| `no_ram` | RAM is not being accessed, _i.e._, the running product of the [Permutation Argument](permutation-argument.md) with the RAM Table remains unchanged | +| `keep_jump_stack` | jump stack does not change, _i.e._, registers `jsp`, `jso`, and `jsd` do not change | +| `step_1` | jump stack does not change and instruction pointer `ip` increases by 1 | +| `step_2` | jump stack does not change and instruction pointer `ip` increases by 2 | +| `grow_op_stack` | op stack elements are shifted down by one position, top element of the resulting stack is unconstrained | +| `grow_op_stack_by_any_of` | op stack elements are shifted down by `n` positions, top `n` elements of the resulting stack are unconstrained, where `n` is the instruction's argument | +| `keep_op_stack_height` | the op stack height remains unchanged, and so in particular the running product of the [Permutation Argument](permutation-argument.md) with the Op Stack table remains unchanged | +| `op_stack_remains_except_top_n` | all but the top `n` elements of the op stack remain unchanged | +| `keep_op_stack` | op stack remains entirely unchanged | +| `binary_operation` | op stack elements starting from `st2` are shifted up by one position, highest two elements of the resulting stack are unconstrained | +| `shrink_op_stack` | op stack elements starting from `st1` are shifted up by one position | +| `shrink_op_stack_by_any_of` | op stack elements starting from `stn` are shifted up by one position, where `n` is the instruction's argument | The following instruction groups conceptually fit the category of 'instruction groups' but are not used or enforced through AIR constraints. @@ -35,48 +35,48 @@ The following instruction groups conceptually fit the category of 'instruction g A summary of all instructions and which groups they are part of is given in the following table. -| instruction | `decompose_arg` | `prohibit_illegal_num_words` | `no_io` | `no_ram` | `keep_jump_stack` | `step_1` | `step_2` | `grow_op_stack` | `grow_op_stack_by_any_of` | `keep_op_stack_height` | `op_stack_remains_except_top_n_elements_unconstrained` | `keep_op_stack` | `binary_operation` | `shrink_op_stack` | `shrink_op_stack_by_any_of` | -|:------------------|:---------------:|:----------------------------:|:-------:|:--------:|:-----------------:|:--------:|:--------:|:---------------:|:-------------------------:|:----------------------:|:------------------------------------------------------:|:---------------:|:------------------:|:-----------------:|:---------------------------:| -| `pop` + `n` | x | x | x | x | | | x | | | | | | | | x | -| `push` + `a` | | | x | x | | | x | x | | | | | | | | -| `divine` + `n` | x | x | x | x | | | x | | x | | | | | | | -| `dup` + `i` | x | | x | x | | | x | x | | | | | | | | -| `swap` + `i` | x | | x | x | | | x | | | x | | | | | | -| `nop` | | | x | x | | x | | | | x | 0 | x | | | | -| `skiz` | | | x | x | x | | | | | | | | | x | | -| `call` + `d` | | | x | x | | | | | | x | 0 | x | | | | -| `return` | | | x | x | | | | | | x | 0 | x | | | | -| `recurse` | | | x | x | x | | | | | x | 0 | x | | | | -| `assert` | | | x | x | | x | | | | | | | | x | | -| `halt` | | | x | x | | x | | | | x | 0 | x | | | | -| `read_mem` + `n` | x | x | x | | | | x | | | | | | | | | -| `write_mem` + `n` | x | x | x | | | | x | | | | | | | | | -| `hash` | | | x | x | | x | | | | | | | | | | -| `divine_sibling` | | | x | x | | x | | | | | | | | | | -| `assert_vector` | | | x | x | | x | | | | | | | | | | -| `sponge_init` | | | x | x | | x | | | | | | | | | | -| `sponge_absorb` | | | x | x | | x | | | | | | | | | | -| `sponge_squeeze` | | | x | x | | x | | | | | | | | | | -| `add` | | | x | x | | x | | | | | | | x | | | -| `mul` | | | x | x | | x | | | | | | | x | | | -| `invert` | | | x | x | | x | | | | x | 1 | | | | | -| `eq` | | | x | x | | x | | | | | | | x | | | -| `split` | | | x | x | | x | | | | | | | | | | -| `lt` | | | x | x | | x | | | | | | | x | | | -| `and` | | | x | x | | x | | | | | | | x | | | -| `xor` | | | x | x | | x | | | | | | | x | | | -| `log_2_floor` | | | x | x | | x | | | | x | 1 | | | | | -| `pow` | | | x | x | | x | | | | | | | x | | | -| `div_mod` | | | x | x | | x | | | | x | 2 | | | | | -| `pop_count` | | | x | x | | x | | | | x | 1 | | | | | -| `xx_add` | | | x | x | | x | | | | | | | | | | -| `xx_mul` | | | x | x | | x | | | | | | | | | | -| `x_invert` | | | x | x | | x | | | | x | 3 | | | | | -| `xb_mul` | | | x | x | | x | | | | | | | | | | -| `read_io` + `n` | x | x | | x | | | x | | x | | | | | | | -| `write_io` + `n` | x | x | | x | | | x | | | | | | | | x | -| `xx_dot_step` | | | x | | | | | | | x | 5 | | | | | -| `xb_dot_step` | | | x | | | | | | | x | 5 | | | | x | +| instruction | `decompose_arg` | `prohibit_illegal_num_words` | `no_io` | `no_ram` | `keep_jump_stack` | `step_1` | `step_2` | `grow_op_stack` | `grow_op_stack_by_any_of` | `keep_op_stack_height` | `op_stack_remains_except_top_n` | `keep_op_stack` | `binary_operation` | `shrink_op_stack` | `shrink_op_stack_by_any_of` | +|:------------------|:---------------:|:----------------------------:|:-------:|:--------:|:-----------------:|:--------:|:--------:|:---------------:|:-------------------------:|:----------------------:|:-------------------------------:|:---------------:|:------------------:|:-----------------:|:---------------------------:| +| `pop` + `n` | x | x | x | x | | | x | | | | | | | | x | +| `push` + `a` | | | x | x | | | x | x | | | | | | | | +| `divine` + `n` | x | x | x | x | | | x | | x | | | | | | | +| `dup` + `i` | x | | x | x | | | x | x | | | | | | | | +| `swap` + `i` | x | | x | x | | | x | | | x | | | | | | +| `nop` | | | x | x | | x | | | | x | 0 | x | | | | +| `skiz` | | | x | x | x | | | | | | | | | x | | +| `call` + `d` | | | x | x | | | | | | x | 0 | x | | | | +| `return` | | | x | x | | | | | | x | 0 | x | | | | +| `recurse` | | | x | x | x | | | | | x | 0 | x | | | | +| `assert` | | | x | x | | x | | | | | | | | x | | +| `halt` | | | x | x | | x | | | | x | 0 | x | | | | +| `read_mem` + `n` | x | x | x | | | | x | | | | | | | | | +| `write_mem` + `n` | x | x | x | | | | x | | | | | | | | | +| `hash` | | | x | x | | x | | | | | | | | | | +| `assert_vector` | | | x | x | | x | | | | | | | | | | +| `sponge_init` | | | x | x | | x | | | | | | | | | | +| `sponge_absorb` | | | x | x | | x | | | | | | | | | | +| `sponge_squeeze` | | | x | x | | x | | | | | | | | | | +| `add` | | | x | x | | x | | | | | | | x | | | +| `mul` | | | x | x | | x | | | | | | | x | | | +| `invert` | | | x | x | | x | | | | x | 1 | | | | | +| `eq` | | | x | x | | x | | | | | | | x | | | +| `split` | | | x | x | | x | | | | | | | | | | +| `lt` | | | x | x | | x | | | | | | | x | | | +| `and` | | | x | x | | x | | | | | | | x | | | +| `xor` | | | x | x | | x | | | | | | | x | | | +| `log_2_floor` | | | x | x | | x | | | | x | 1 | | | | | +| `pow` | | | x | x | | x | | | | | | | x | | | +| `div_mod` | | | x | x | | x | | | | x | 2 | | | | | +| `pop_count` | | | x | x | | x | | | | x | 1 | | | | | +| `xx_add` | | | x | x | | x | | | | | | | | | | +| `xx_mul` | | | x | x | | x | | | | | | | | | | +| `x_invert` | | | x | x | | x | | | | x | 3 | | | | | +| `xb_mul` | | | x | x | | x | | | | | | | | | | +| `read_io` + `n` | x | x | | x | | | x | | x | | | | | | | +| `write_io` + `n` | x | x | | x | | | x | | | | | | | | x | +| `merkle_step` | | | x | x | | x | | | | | 6 | | | | | +| `xx_dot_step` | | | x | | | | | | | x | 5 | | | | | +| `xb_dot_step` | | | x | | | | | | | x | 5 | | | | x | ## Indicator Polynomials `ind_i(hv3, hv2, hv1, hv0)` diff --git a/specification/src/instruction-specific-transition-constraints.md b/specification/src/instruction-specific-transition-constraints.md index 9278ce7a7..a79fe4a53 100644 --- a/specification/src/instruction-specific-transition-constraints.md +++ b/specification/src/instruction-specific-transition-constraints.md @@ -506,63 +506,6 @@ In addition to its [instruction groups](instruction-groups.md), this instruction `·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')`
`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')` -## Instruction `divine_sibling` - -Recall that in a Merkle tree, the indices of left (respectively right) leafs have 0 (respectively 1) as their least significant bit. -The first two polynomials achieve that helper variable `hv0` holds the result of `st10 mod 2`. -The third polynomial sets the new value of `st10` to `st10 div 2`. - -In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. - -### Description - -1. Helper variable `hv0` is either 0 or 1. -1. If `hv0` is 0, then `st0` does not change. -1. If `hv0` is 0, then `st1` does not change. -1. If `hv0` is 0, then `st2` does not change. -1. If `hv0` is 0, then `st3` does not change. -1. If `hv0` is 0, then `st4` does not change. -1. If `hv0` is 1, then `st0` is moved to `st5`. -1. If `hv0` is 1, then `st1` is moved to `st6`. -1. If `hv0` is 1, then `st2` is moved to `st7`. -1. If `hv0` is 1, then `st3` is moved to `st8`. -1. If `hv0` is 1, then `st4` is moved to `st9`. -1. `st5` is shifted by 1 bit to the right and moved into `st10`. -1. `st6` is moved into `st11` -1. `st7` is moved into `st12` -1. `st8` is moved into `st13` -1. `st9` is moved into `st14` -1. `st10` is moved into `st15` -1. The op stack pointer grows by 5. -1. The running product with the Op Stack Table accumulates `st11` through `st15`. - -### Polynomials - -1. `hv0·(hv0 - 1)` -1. `(1 - hv0)·(st0' - st0) + hv0·(st5' - st0)` -1. `(1 - hv0)·(st1' - st1) + hv0·(st6' - st1)` -1. `(1 - hv0)·(st2' - st2) + hv0·(st7' - st2)` -1. `(1 - hv0)·(st3' - st3) + hv0·(st8' - st3)` -1. `(1 - hv0)·(st4' - st4) + hv0·(st9' - st4)` -1. `st10'·2 + hv0 - st5` -1. `st11' - st6` -1. `st12' - st7` -1. `st13' - st8` -1. `st14' - st9` -1. `st15' - st10` -1. `op_stack_pointer' - op_stack_pointer - 5` -1. `RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍉·op_stack_pointer - 🫒·st15)`
- `·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 1) - 🫒·st14)`
- `·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 2) - 🫒·st13)`
- `·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 3) - 🫒·st12)`
- `·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 4) - 🫒·st11)` - -### Helper variable definitions for `divine_sibling` - -Since `st10` contains the Merkle tree node index, - -1. `hv0` holds the result of `st10 % 2` (the node index's least significant bit, indicating whether it is a left/right node). - ## Instruction `assert_vector` In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. @@ -991,6 +934,24 @@ In addition to its [instruction groups](instruction-groups.md), this instruction `+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3)`
`+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3) - st4)` +## Instruction `merkle_step` + +Recall that in a Merkle tree, the indices of left (respectively right) leaves have 0 (respectively 1) as their least significant bit. +This motivates the use of a helper variable to hold that least significant bit. + +In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. +The two [Evaluation Arguments also used for instruction hash](processor-table.md#transition-constraints) guarantee correct transition of the top of the stack. + +### Description + +1. Helper variable `hv5` is either 0 or 1. +1. `st5` is shifted by 1 bit to the right. In other words, twice `st5` in the next row plus `hv5` equals `st5` in the current row. + +### Helper variable definitions for `merkle_step` + +1. `hv0` through `hv4` hold the sibling digest of the node indicated by `st5`, as read from the interface for non-deterministic input. +1. `hv5` holds the result of `st5 % 2`, the Merkle tree node index's least significant bit, indicating whether it is a left or right node. + ## Instruction `xx_dot_step` In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. diff --git a/specification/src/instructions.md b/specification/src/instructions.md index 3398dd194..38f838a05 100644 --- a/specification/src/instructions.md +++ b/specification/src/instructions.md @@ -28,7 +28,7 @@ The third property allows efficient arithmetization of the running product for t | `dup` + `i` | 17 | e.g., `_ e d c b a` | e.g., `_ e d c b a d` | Duplicates the element `i` positions away from the top. 0 ⩽ `i` < 16 | | `swap` + `i` | 25 | e.g., `_ e d c b a` | e.g., `_ e a c b d` | Swaps the `i`th stack element with the top of the stack. 0 < `i` < 16 | -Instruction `divine n` (together with [`divine_sibling`](#hashing)) make Triton a virtual machine that can execute non-deterministic programs. +Instruction `divine n` (together with [`merkle_step`](#many-in-one)) make Triton a virtual machine that can execute non-deterministic programs. As programs go, this concept is somewhat unusual and benefits from additional explanation. The name of the instruction is the verb (not the adjective) meaning “to discover by intuition or insight.” @@ -75,14 +75,13 @@ 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. | -| `divine_sibling` | 32 | `_ i edcba` | e.g., `_ (i div 2) edcba zyxwv` | Helps traversing a Merkle tree during authentication path verification. See extended description below. | -| `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` | 40 | `_` | `_` | 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` | 48 | `_` | `_ 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_squeeze` | 40 | `_` | `_ 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`. @@ -90,17 +89,6 @@ The Tip5 permutation is applied to `abcdefghij000000`, resulting in `αβγδε 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 instruction `divine_sibling` 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`. -The sibling digest of `edcba` is `zyxwv` and is read from the input interface of secret data. -The least-significant bit of `i` indicates whether `edcba` is the digest of a left leaf or a right leaf of the Merkle tree's base level. -Depending on this least significant bit of `i`, `divine_sibling` either -1. (`i` = 0 mod 2, _i.e._, current node is left sibling) lets `edcba` remain in registers `st0` through `st4` and puts `zyxwv` into registers `st5` through `st9`, or -2. (`i` = 1 mod 2, _i.e._, current node is right sibling) moves `edcba` into registers `st5` through `st9` and puts `zyxwv` into registers `st0` through `st4`. - -In either case, 6th register `i` is shifted by 1 bit to the right, _i.e._, the least-significant bit is dropped, and moved into the 11th register. -In conjunction with instruction `hash` and `assert_vector`, the instruction `divine_sibling` allows to efficiently verify a Merkle authentication path. - 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 capacity is never accessible to the program that's being executed by Triton VM. At any given time, at most one Sponge state exists. @@ -115,7 +103,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` | 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. | +| `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. | | `eq` | 58 | `_ b a` | `_ (a == b)` | Tests the top two stack elements for equality. | ## Bitwise Arithmetic on Stack @@ -151,5 +139,20 @@ 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. | + +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`. +The sibling digest of `edcba` is `εδγβα` and is read from the input interface of secret data. +The least-significant bit of `i` indicates whether `edcba` is the digest of a left leaf or a right leaf of the Merkle tree's current level. +Depending on this least significant bit of `i`, `merkle_step` either +1. (`i` = 0 mod 2) interprets `edcba` as the left digest, `εδγβα` as the right digest, or +2. (`i` = 1 mod 2) interprets `εδγβα` as the left digest, `edcba` as the right digest. + +In either case, +1. the left and right digests are hashed, and the resulting digest `zyxwv` replaces the top of the stack, and +1. 6th register `i` is shifted by 1 bit to the right, _i.e._, the least-significant bit is dropped. + +In conjunction with instruction `assert_vector`, the instruction `merkle_step` allows to efficiently verify a Merkle authentication path. diff --git a/specification/src/processor-table.md b/specification/src/processor-table.md index d5f9eab10..7842fa0ea 100644 --- a/specification/src/processor-table.md +++ b/specification/src/processor-table.md @@ -114,39 +114,6 @@ See [program attestation](program-attestation.md) for more details. 1. `U32LookupClientLogDerivative` is 0. 1. `ClockJumpDifferenceLookupServerLogDerivative` starts having accumulated the first contribution. -### Initial Constraints as Polynomials - -1. `clk` -1. `ip` -1. `jsp` -1. `jso` -1. `jsd` -1. `st0` -1. `st1` -1. `st2` -1. `st3` -1. `st4` -1. `st5` -1. `st6` -1. `st7` -1. `st8` -1. `st9` -1. `st10` -1. `🥬^5 + st11·🥬^4 + st12·🥬^3 + st13·🥬^2 + st14·🥬 + st15 - 🫑` -1. `op_stack_pointer - 16` -1. `RunningEvaluationStandardInput - 1` -1. `RunningEvaluationStandardOutput - 1` -1. `InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1` -1. `RunningProductOpStackTable - 1` -1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·instruction_type)` -1. `RunningProductJumpStackTable - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)` -1. `(ci - opcode(hash))·(RunningEvaluationHashInput - 1)`
- `+ hash_deselector·(RunningEvaluationHashInput - 🚪 - 🧄₀·st0 - 🧄₁·st1 - 🧄₂·st2 - 🧄₃·st3 - 🧄₄·st4 - 🧄₅·st5 - 🧄₆·st6 - 🧄₇·st7 - 🧄₈·st8 - 🧄₉·st9)` -1. `RunningEvaluationHashDigest - 1` -1. `RunningEvaluationSponge - 1` -1. `U32LookupClientLogDerivative` -1. `ClockJumpDifferenceLookupServerLogDerivative · 🪞 - cjd_mul` (Recall that `(🪞 - clk) = 🪞` because `clk = 0`.) - ## Consistency Constraints 1. The composition of instruction bits `ib0` through `ib6` corresponds to the current instruction `ci`. @@ -160,19 +127,6 @@ See [program attestation](program-attestation.md) for more details. 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 is 0. -### Consistency Constraints as Polynomials - -1. `ci - (2^6·ib6 + 2^5·ib5 + 2^4·ib4 + 2^3·ib3 + 2^2·ib2 + 2^1·ib1 + 2^0·ib0)` -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. `IsPadding·(IsPadding - 1)` -1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivative` - ## Transition Constraints Due to their complexity, instruction-specific constraints are defined [in their own section](instruction-specific-transition-constraints.md). @@ -183,8 +137,13 @@ The following additional constraints also apply to every pair of rows. 1. If the next row is not a padding row, the logarithmic derivative for the Program Table absorbs the next row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥. Otherwise, it 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 🪞. 1. The running product for the Jump Stack Table absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴. -1. If the current instruction in the next row is `hash`, the running evaluation “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. 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 🚪. + 1. If the current instruction in the next row is `merkle_step` and helper variable `hv5`… + 1. …is 0, the running evaluation “Hash Input” absorbs next row's `st0` through `st4` and `hv0` through `hv4`… + 1. …is 1, the running evaluation “Hash Input” absorbs next row's `hv0` through `hv4` and `st0` through `st4`…
+ …with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪. + 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 🧽. Otherwise, the running evaluation remains unchanged. @@ -197,40 +156,6 @@ The following additional constraints also apply to every pair of rows. 1. If the current instruction is `pop_count`, 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. 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. -### Transition Constraints as Polynomials - -1. `clk' - (clk + 1)` -1. `IsPadding·(IsPadding' - IsPadding)` -1. `(1 - IsPadding') · ((InstructionLookupClientLogDerivative' - InstructionLookupClientLogDerivative) · (🛁 - 🥝·ip' - 🥥·ci' - 🫐·nia') - 1)`
- `+ IsPadding'·(RunningProductInstructionTable' - RunningProductInstructionTable)` -1. `(ClockJumpDifferenceLookupServerLogDerivative' - ClockJumpDifferenceLookupServerLogDerivative)`
- `·(🪞 - clk') - cjd_mul'` -1. `RunningProductJumpStackTable' - RunningProductJumpStackTable·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')` -1. `(ci' - opcode(hash))·(RunningEvaluationHashInput' - RunningEvaluationHashInput)`
- `+ hash_deselector'·(RunningEvaluationHashInput' - 🚪·RunningEvaluationHashInput - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')` -1. `(ci - opcode(hash))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)`
- `+ hash_deselector·(RunningEvaluationHashDigest' - 🪟·RunningEvaluationHashDigest - 🧄₀·st5' - 🧄₁·st6' - 🧄₂·st7' - 🧄₃·st8' - 🧄₄·st9')` -1. `(ci - opcode(sponge_init))·(ci - opcode(sponge_absorb)·(ci - opcode(sponge_squeeze))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)`
- `+ (sponge_init_deselector + sponge_absorb_deselector + sponge_squeeze_deselector)`
- `·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·ci - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')` -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_mod_deselector·(`
-   `(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`
-   `- (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)`
-   `- (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`
-  `)` - 1. `+ pop_count_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)` - 1. `+ (1 - ib2)·(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)` - ## Terminal Constraints 1. In the last row, register “current instruction” `ci` is 0, corresponding to instruction `halt`. - -### Terminal Constraints as Polynomials - -1. `ci` diff --git a/specification/src/registers.md b/specification/src/registers.md index 8fc6ed4a7..51ae022e6 100644 --- a/specification/src/registers.md +++ b/specification/src/registers.md @@ -54,9 +54,9 @@ These registers are part of the arithmetization of the architecture, but not nee Because they are only needed for some instructions, the helper variables are not generally defined. 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), [`eq`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-eq), +[`merkle_step`](instruction-specific-transition-constraints.md#helper-variable-definitions-for-merkle-step), [`xx_dot_step`](instruction-specific-transition-constraints.md#instruction-xx_dot_step), and [`xb_dot_step`](instruction-specific-transition-constraints.md#instruction-xb_dot_step), the behavior is defined in the respective sections. diff --git a/triton-vm/src/example_programs.rs b/triton-vm/src/example_programs.rs index 917bc0d1e..1efa69997 100644 --- a/triton-vm/src/example_programs.rs +++ b/triton-vm/src/example_programs.rs @@ -158,7 +158,7 @@ fn merkle_tree_authentication_path_verify() -> Program { // stack after: [* r4 r3 r2 r1 r0 1 d4 d3 d2 d1 d0] traverse_tree: dup 5 push 1 eq skiz return // break loop if node index is 1 - divine_sibling hash recurse // move up one level in the Merkle tree + merkle_step recurse // move up one level in the Merkle tree // subroutine: compare digests // stack before: [* r4 r3 r2 r1 r0 1 d4 d3 d2 d1 d0] diff --git a/triton-vm/src/instruction.rs b/triton-vm/src/instruction.rs index 805b0e35d..31aea711f 100644 --- a/triton-vm/src/instruction.rs +++ b/triton-vm/src/instruction.rs @@ -178,7 +178,6 @@ pub enum AnInstruction { // Hashing-related Hash, - DivineSibling, AssertVector, SpongeInit, SpongeAbsorb, @@ -211,6 +210,7 @@ pub enum AnInstruction { WriteIo(NumberOfWords), // Many-in-One + MerkleStep, XxDotStep, XbDotStep, } @@ -234,14 +234,13 @@ impl AnInstruction { ReadMem(_) => 41, WriteMem(_) => 11, Hash => 18, - DivineSibling => 32, AssertVector => 26, - SpongeInit => 40, + SpongeInit => 32, SpongeAbsorb => 34, - SpongeSqueeze => 48, + SpongeSqueeze => 40, Add => 42, Mul => 50, - Invert => 56, + Invert => 48, Eq => 58, Split => 4, Lt => 6, @@ -253,10 +252,11 @@ impl AnInstruction { PopCount => 28, XxAdd => 66, XxMul => 74, - XInvert => 64, + XInvert => 56, XbMul => 82, ReadIo(_) => 49, WriteIo(_) => 19, + MerkleStep => 64, XxDotStep => 72, XbDotStep => 80, } @@ -279,7 +279,6 @@ impl AnInstruction { ReadMem(_) => "read_mem", WriteMem(_) => "write_mem", Hash => "hash", - DivineSibling => "divine_sibling", AssertVector => "assert_vector", SpongeInit => "sponge_init", SpongeAbsorb => "sponge_absorb", @@ -302,13 +301,14 @@ impl AnInstruction { XbMul => "xb_mul", ReadIo(_) => "read_io", WriteIo(_) => "write_io", + MerkleStep => "merkle_step", XxDotStep => "xx_dot_step", XbDotStep => "xb_dot_step", } } - pub fn opcode_b(&self) -> BFieldElement { - self.opcode().into() + pub const fn opcode_b(&self) -> BFieldElement { + BFieldElement::new(self.opcode() as u64) } pub fn size(&self) -> usize { @@ -352,7 +352,6 @@ impl AnInstruction { ReadMem(x) => ReadMem(*x), WriteMem(x) => WriteMem(*x), Hash => Hash, - DivineSibling => DivineSibling, AssertVector => AssertVector, SpongeInit => SpongeInit, SpongeAbsorb => SpongeAbsorb, @@ -375,6 +374,7 @@ impl AnInstruction { XbMul => XbMul, ReadIo(x) => ReadIo(*x), WriteIo(x) => WriteIo(*x), + MerkleStep => MerkleStep, XxDotStep => XxDotStep, XbDotStep => XbDotStep, } @@ -397,7 +397,6 @@ impl AnInstruction { ReadMem(n) => n.num_words() as i32, WriteMem(n) => -(n.num_words() as i32), Hash => -5, - DivineSibling => 5, AssertVector => -5, SpongeInit => 0, SpongeAbsorb => -10, @@ -420,6 +419,7 @@ impl AnInstruction { XbMul => -1, ReadIo(n) => n.num_words() as i32, WriteIo(n) => -(n.num_words() as i32), + MerkleStep => 0, XxDotStep => 0, XbDotStep => 0, } @@ -549,7 +549,6 @@ const fn all_instructions_without_args() -> [AnInstruction; Instr ReadMem(N1), WriteMem(N1), Hash, - DivineSibling, AssertVector, SpongeInit, SpongeAbsorb, @@ -572,6 +571,7 @@ const fn all_instructions_without_args() -> [AnInstruction; Instr XbMul, ReadIo(N1), WriteIo(N1), + MerkleStep, XxDotStep, XbDotStep, ] diff --git a/triton-vm/src/parser.rs b/triton-vm/src/parser.rs index 3c7ddc1ef..47a5e23a2 100644 --- a/triton-vm/src/parser.rs +++ b/triton-vm/src/parser.rs @@ -222,7 +222,7 @@ fn an_instruction(s: &str) -> ParseResult> { let dup = dup_instruction(); let swap = swap_instruction(); - let opstack_manipulation = alt((pop, push, dup, swap)); + let opstack_manipulation = alt((pop, push, divine, dup, swap)); // Control flow let halt = instruction("halt", Halt); @@ -243,7 +243,6 @@ fn an_instruction(s: &str) -> ParseResult> { // Hashing-related instructions let hash = instruction("hash", Hash); - let divine_sibling = instruction("divine_sibling", DivineSibling); let assert_vector = instruction("assert_vector", AssertVector); let sponge_init = instruction("sponge_init", SpongeInit); let sponge_absorb = instruction("sponge_absorb", SpongeAbsorb); @@ -286,17 +285,18 @@ fn an_instruction(s: &str) -> ParseResult> { let read_write = alt((read_io, write_io)); // Many-in-One + let merkle_step = instruction("merkle_step", MerkleStep); let xx_dot_step = instruction("xx_dot_step", XxDotStep); let xb_dot_step = instruction("xb_dot_step", XbDotStep); - let many_to_one = alt((xx_dot_step, xb_dot_step)); + let many_to_one = alt((merkle_step, xx_dot_step, xb_dot_step)); // 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_, divine_sibling, divine)); + let syntax_ambiguous = alt((assert_vector, assert_)); alt(( opstack_manipulation, diff --git a/triton-vm/src/program.rs b/triton-vm/src/program.rs index be7785d37..858e6c82d 100644 --- a/triton-vm/src/program.rs +++ b/triton-vm/src/program.rs @@ -820,9 +820,9 @@ impl PublicInput { } } -/// All sources of non-determinism for a program. This includes elements that can be read using -/// instruction `divine`, digests that can be read using instruction `divine_sibling`, -/// and an initial state of random-access memory. +/// All sources of non-determinism for a program. This includes elements that +/// can be read using instruction `divine`, digests that can be read using +/// instruction `merkle_step`, and an initial state of random-access memory. #[derive(Debug, Default, Clone, Eq, PartialEq, Serialize, Deserialize, Arbitrary)] pub struct NonDeterminism { pub individual_tokens: Vec, diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index 9778bb887..031e33bd5 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -1423,13 +1423,13 @@ pub(crate) mod tests { } #[test] - fn check_grand_cross_table_argument_for_test_program_for_divine_sibling_no_switch() { - check_grand_cross_table_argument(test_program_for_divine_sibling_no_switch()) + fn check_grand_cross_table_argument_for_test_program_for_merkle_step_no_switch() { + check_grand_cross_table_argument(test_program_for_merkle_step_right_sibling()) } #[test] - fn check_grand_cross_table_argument_for_test_program_for_divine_sibling_switch() { - check_grand_cross_table_argument(test_program_for_divine_sibling_switch()) + fn check_grand_cross_table_argument_for_test_program_for_merkle_step_switch() { + check_grand_cross_table_argument(test_program_for_merkle_step_left_sibling()) } #[test] @@ -1864,13 +1864,13 @@ pub(crate) mod tests { } #[test] - fn constraints_evaluate_to_zero_on_program_for_divine_sibling_no_switch() { - triton_constraints_evaluate_to_zero(test_program_for_divine_sibling_no_switch()) + fn constraints_evaluate_to_zero_on_program_for_merkle_step_no_switch() { + triton_constraints_evaluate_to_zero(test_program_for_merkle_step_right_sibling()) } #[test] - fn constraints_evaluate_to_zero_on_program_for_divine_sibling_switch() { - triton_constraints_evaluate_to_zero(test_program_for_divine_sibling_switch()) + fn constraints_evaluate_to_zero_on_program_for_merkle_step_switch() { + triton_constraints_evaluate_to_zero(test_program_for_merkle_step_left_sibling()) } #[test] diff --git a/triton-vm/src/table/processor_table.rs b/triton-vm/src/table/processor_table.rs index 442cb06f5..4d6590ed4 100644 --- a/triton-vm/src/table/processor_table.rs +++ b/triton-vm/src/table/processor_table.rs @@ -187,36 +187,46 @@ impl ProcessorTable { jump_stack_running_product *= challenges[JumpStackIndeterminate] - compressed_row_for_jump_stack_table; - // Hash Table – Hash's input from Processor to Hash Coprocessor - let st_0_through_9 = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9]; + // Hash Table – `hash`'s or `merkle_step`'s input from Processor to Hash Coprocessor + let st0_through_st9 = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9]; let hash_state_weights = &challenges[HashStateWeight0..HashStateWeight10]; - let compressed_row_for_hash_input_and_sponge_squeeze: XFieldElement = st_0_through_9 - .map(|st| current_row[st.base_table_index()]) - .into_iter() - .zip_eq(hash_state_weights.iter()) - .map(|(st, &weight)| weight * st) - .sum(); - let hash_digest_weights = &challenges[HashStateWeight0..HashStateWeight5]; - let compressed_row_for_hash_digest: XFieldElement = st_0_through_9 - [0..tip5::DIGEST_LENGTH] - .iter() - .map(|st| current_row[st.base_table_index()]) - .zip_eq(hash_digest_weights.iter()) - .map(|(st, &weight)| weight * st) - .sum(); - if current_row[CI.base_table_index()] == Instruction::Hash.opcode_b() { + if ci == Instruction::Hash.opcode_b() || ci == Instruction::MerkleStep.opcode_b() { + let merkle_step_left_sibling = [ST0, ST1, ST2, ST3, ST4, HV0, HV1, HV2, HV3, HV4]; + let merkle_step_right_sibling = [HV0, HV1, HV2, HV3, HV4, ST0, ST1, ST2, ST3, ST4]; + let is_left_sibling = current_row[HV5.base_table_index()].value() % 2 == 0; + let hash_input = match Self::instruction_from_row(current_row) { + Some(Instruction::MerkleStep) if is_left_sibling => merkle_step_left_sibling, + Some(Instruction::MerkleStep) => merkle_step_right_sibling, + _ => st0_through_st9, + }; + let compressed_row: XFieldElement = hash_input + .map(|st| current_row[st.base_table_index()]) + .into_iter() + .zip_eq(hash_state_weights.iter()) + .map(|(st, &weight)| weight * st) + .sum(); hash_input_running_evaluation = hash_input_running_evaluation * challenges[HashInputIndeterminate] - + compressed_row_for_hash_input_and_sponge_squeeze; + + compressed_row; } - // Hash Table – Hash's output from Hash Coprocessor to Processor + // Hash Table – `hash`'s output from Hash Coprocessor to Processor if let Some(prev_row) = previous_row { - if prev_row[CI.base_table_index()] == Instruction::Hash.opcode_b() { + let prev_ci = prev_row[CI.base_table_index()]; + if prev_ci == Instruction::Hash.opcode_b() + || prev_ci == Instruction::MerkleStep.opcode_b() + { + let hash_digest_weights = &challenges[HashStateWeight0..HashStateWeight5]; + let compressed_row: XFieldElement = [ST0, ST1, ST2, ST3, ST4] + .map(|st| current_row[st.base_table_index()]) + .into_iter() + .zip_eq(hash_digest_weights) + .map(|(st, &weight)| weight * st) + .sum(); hash_digest_running_evaluation = hash_digest_running_evaluation * challenges[HashDigestIndeterminate] - + compressed_row_for_hash_digest; + + compressed_row; } } @@ -229,7 +239,7 @@ impl ProcessorTable { } if prev_row[CI.base_table_index()] == Instruction::SpongeAbsorb.opcode_b() { - let compressed_row: XFieldElement = st_0_through_9 + let compressed_row: XFieldElement = st0_through_st9 .map(|st| prev_row[st.base_table_index()]) .into_iter() .zip_eq(hash_state_weights.iter()) @@ -242,10 +252,16 @@ impl ProcessorTable { } if prev_row[CI.base_table_index()] == Instruction::SpongeSqueeze.opcode_b() { + let compressed_row: XFieldElement = st0_through_st9 + .map(|st| current_row[st.base_table_index()]) + .into_iter() + .zip_eq(hash_state_weights.iter()) + .map(|(st, &weight)| weight * st) + .sum(); sponge_running_evaluation = sponge_running_evaluation * challenges[SpongeIndeterminate] + challenges[HashCIWeight] * Instruction::SpongeSqueeze.opcode_b() - + compressed_row_for_hash_input_and_sponge_squeeze; + + compressed_row; } } @@ -1744,11 +1760,14 @@ impl ExtProcessorTable { .concat() } - /// Recall that in a Merkle tree, the indices of left (respectively right) leafs have 0 - /// (respectively 1) as their least significant bit. The first two polynomials achieve that - /// helper variable hv0 holds the result of st5 mod 2. The second polynomial sets the new value - /// of st10 to st5 div 2. - fn instruction_divine_sibling( + /// Recall that in a Merkle tree, the indices of left (respectively right) + /// leaves have 0 (respectively 1) as their least significant bit. The first two + /// polynomials achieve that helper variable hv5 holds the result of st5 mod 2. + /// The second polynomial sets the new value of st5 to st5 div 2. + /// + /// Two Evaluation Arguments with the Hash Table guarantee the rest of the + /// correct transition. + fn instruction_merkle_step( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); @@ -1760,49 +1779,14 @@ impl ExtProcessorTable { circuit_builder.input(NextBaseRow(col.master_base_table_index())) }; - let hv0_is_0_or_1 = curr_base_row(HV0) * (curr_base_row(HV0) - one()); - - let new_st10_is_previous_st5_div_2 = - next_base_row(ST10) * constant(2) + curr_base_row(HV0) - curr_base_row(ST5); - - let maybe_move_st0 = (one() - curr_base_row(HV0)) - * (next_base_row(ST0) - curr_base_row(ST0)) - + curr_base_row(HV0) * (next_base_row(ST5) - curr_base_row(ST0)); - let maybe_move_st1 = (one() - curr_base_row(HV0)) - * (next_base_row(ST1) - curr_base_row(ST1)) - + curr_base_row(HV0) * (next_base_row(ST6) - curr_base_row(ST1)); - let maybe_move_st2 = (one() - curr_base_row(HV0)) - * (next_base_row(ST2) - curr_base_row(ST2)) - + curr_base_row(HV0) * (next_base_row(ST7) - curr_base_row(ST2)); - let maybe_move_st3 = (one() - curr_base_row(HV0)) - * (next_base_row(ST3) - curr_base_row(ST3)) - + curr_base_row(HV0) * (next_base_row(ST8) - curr_base_row(ST3)); - let maybe_move_st4 = (one() - curr_base_row(HV0)) - * (next_base_row(ST4) - curr_base_row(ST4)) - + curr_base_row(HV0) * (next_base_row(ST9) - curr_base_row(ST4)); - - let maybe_shift_known_digest_down_the_stack = vec![ - hv0_is_0_or_1, - new_st10_is_previous_st5_div_2, - maybe_move_st0, - maybe_move_st1, - maybe_move_st2, - maybe_move_st3, - maybe_move_st4, - ]; + let hv5_is_0_or_1 = curr_base_row(HV5) * (curr_base_row(HV5) - one()); + let new_st5_is_previous_st5_div_2 = + next_base_row(ST5) * constant(2) + curr_base_row(HV5) - curr_base_row(ST5); - let op_stack_grows_by_5_and_top_11_elements_unconstrained = vec![ - next_base_row(ST11) - curr_base_row(ST6), - next_base_row(ST12) - curr_base_row(ST7), - next_base_row(ST13) - curr_base_row(ST8), - next_base_row(ST14) - curr_base_row(ST9), - next_base_row(ST15) - curr_base_row(ST10), - next_base_row(OpStackPointer) - curr_base_row(OpStackPointer) - constant(5), - Self::running_product_op_stack_accounts_for_growing_stack_by(circuit_builder, 5), - ]; + let update_merkle_tree_node_index = vec![hv5_is_0_or_1, new_st5_is_previous_st5_div_2]; [ - maybe_shift_known_digest_down_the_stack, - op_stack_grows_by_5_and_top_11_elements_unconstrained, + update_merkle_tree_node_index, + Self::instruction_group_op_stack_remains_except_top_n(circuit_builder, 6), Self::instruction_group_step_1(circuit_builder), Self::instruction_group_no_ram(circuit_builder), Self::instruction_group_no_io(circuit_builder), @@ -2491,7 +2475,6 @@ impl ExtProcessorTable { ReadMem(_) => ExtProcessorTable::instruction_read_mem(circuit_builder), WriteMem(_) => ExtProcessorTable::instruction_write_mem(circuit_builder), Hash => ExtProcessorTable::instruction_hash(circuit_builder), - DivineSibling => ExtProcessorTable::instruction_divine_sibling(circuit_builder), AssertVector => ExtProcessorTable::instruction_assert_vector(circuit_builder), SpongeInit => ExtProcessorTable::instruction_sponge_init(circuit_builder), SpongeAbsorb => ExtProcessorTable::instruction_sponge_absorb(circuit_builder), @@ -2509,12 +2492,12 @@ impl ExtProcessorTable { DivMod => ExtProcessorTable::instruction_div_mod(circuit_builder), PopCount => ExtProcessorTable::instruction_pop_count(circuit_builder), XxAdd => ExtProcessorTable::instruction_xx_add(circuit_builder), - XxMul => ExtProcessorTable::instruction_xx_mul(circuit_builder), XInvert => ExtProcessorTable::instruction_xinv(circuit_builder), XbMul => ExtProcessorTable::instruction_xb_mul(circuit_builder), ReadIo(_) => ExtProcessorTable::instruction_read_io(circuit_builder), WriteIo(_) => ExtProcessorTable::instruction_write_io(circuit_builder), + MerkleStep => ExtProcessorTable::instruction_merkle_step(circuit_builder), XxDotStep => ExtProcessorTable::instruction_xx_dot_step(circuit_builder), XbDotStep => ExtProcessorTable::instruction_xb_dot_step(circuit_builder), } @@ -3205,10 +3188,22 @@ impl ExtProcessorTable { * (challenge(JumpStackIndeterminate) - compressed_row) } + /// Deal with instructions `hash` and `merkle_step`. The registers from which + /// the preimage is loaded differs between the two instructions: + /// 1. `hash` always loads the stack's 10 top elements, + /// 1. `merkle_step` loads the stack's 5 top elements and helper variables 0 + /// through 4. The order of those two quintuplets depends on helper variable + /// hv5. + /// + /// The Hash Table does not “know” about instruction `merkle_step`. + /// + /// Note that using `next_row` might be confusing at first glance; See the + /// [specification](https://triton-vm.org/spec/processor-table.html). fn running_evaluation_hash_input_updates_correctly( circuit_builder: &ConstraintCircuitBuilder, ) -> ConstraintCircuitMonad { let constant = |c: u32| circuit_builder.b_constant(c); + let one = || constant(1); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let next_base_row = |col: ProcessorBaseTableColumn| { circuit_builder.input(NextBaseRow(col.master_base_table_index())) @@ -3222,7 +3217,11 @@ impl ExtProcessorTable { let hash_deselector = Self::instruction_deselector_next_row(circuit_builder, Instruction::Hash); - let hash_selector = next_base_row(CI) - constant(Instruction::Hash.opcode()); + let merkle_step_deselector = + Self::instruction_deselector_next_row(circuit_builder, Instruction::MerkleStep); + let hash_and_merkle_step_selector = (next_base_row(CI) + - constant(Instruction::Hash.opcode())) + * (next_base_row(CI) - constant(Instruction::MerkleStep.opcode())); let weights = [ HashStateWeight0, @@ -3237,20 +3236,50 @@ impl ExtProcessorTable { HashStateWeight9, ] .map(challenge); - let state = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9].map(next_base_row); - let compressed_row = weights + + // hash + let state_for_hash = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9].map(next_base_row); + let compressed_row_for_hash = weights + .iter() + .zip_eq(state_for_hash) + .map(|(weight, state)| weight.clone() * state) + .sum(); + + // merkle step + let is_left_sibling = || next_base_row(HV5); + let is_right_sibling = || one() - next_base_row(HV5); + let merkle_step_state_element = + |l, r| is_right_sibling() * next_base_row(l) + is_left_sibling() * next_base_row(r); + let state_for_merkle_step = [ + merkle_step_state_element(ST0, HV0), + merkle_step_state_element(ST1, HV1), + merkle_step_state_element(ST2, HV2), + merkle_step_state_element(ST3, HV3), + merkle_step_state_element(ST4, HV4), + merkle_step_state_element(HV0, ST0), + merkle_step_state_element(HV1, ST1), + merkle_step_state_element(HV2, ST2), + merkle_step_state_element(HV3, ST3), + merkle_step_state_element(HV4, ST4), + ]; + let compressed_row_for_merkle_step = weights .into_iter() - .zip_eq(state) + .zip_eq(state_for_merkle_step) .map(|(weight, state)| weight * state) .sum(); - let running_evaluation_updates = next_ext_row(HashInputEvalArg) + let running_evaluation_updates_for_hash = next_ext_row(HashInputEvalArg) - challenge(HashInputIndeterminate) * curr_ext_row(HashInputEvalArg) - - compressed_row; + - compressed_row_for_hash; + let running_evaluation_updates_for_merkle_step = next_ext_row(HashInputEvalArg) + - challenge(HashInputIndeterminate) * curr_ext_row(HashInputEvalArg) + - compressed_row_for_merkle_step; let running_evaluation_remains = next_ext_row(HashInputEvalArg) - curr_ext_row(HashInputEvalArg); - hash_selector * running_evaluation_remains + hash_deselector * running_evaluation_updates + hash_and_merkle_step_selector * running_evaluation_remains + + hash_deselector * running_evaluation_updates_for_hash + + merkle_step_deselector * running_evaluation_updates_for_merkle_step } fn running_evaluation_hash_digest_updates_correctly( @@ -3273,7 +3302,11 @@ impl ExtProcessorTable { let hash_deselector = Self::instruction_deselector_current_row(circuit_builder, Instruction::Hash); - let hash_selector = curr_base_row(CI) - constant(Instruction::Hash.opcode()); + let merkle_step_deselector = + Self::instruction_deselector_current_row(circuit_builder, Instruction::MerkleStep); + let hash_and_merkle_step_selector = (curr_base_row(CI) + - constant(Instruction::Hash.opcode())) + * (curr_base_row(CI) - constant(Instruction::MerkleStep.opcode())); let weights = [ HashStateWeight0, @@ -3296,7 +3329,8 @@ impl ExtProcessorTable { let running_evaluation_remains = next_ext_row(HashDigestEvalArg) - curr_ext_row(HashDigestEvalArg); - hash_selector * running_evaluation_remains + hash_deselector * running_evaluation_updates + hash_and_merkle_step_selector * running_evaluation_remains + + (hash_deselector + merkle_step_deselector) * running_evaluation_updates } fn running_evaluation_sponge_updates_correctly( @@ -3868,22 +3902,22 @@ pub(crate) mod tests { } #[test] - fn transition_constraints_for_instruction_divine_sibling() { + fn transition_constraints_for_instruction_merkle_step() { let programs = [ - triton_program!(push 2 swap 5 divine_sibling halt), - triton_program!(push 3 swap 5 divine_sibling halt), + triton_program!(push 2 swap 5 merkle_step halt), + triton_program!(push 3 swap 5 merkle_step halt), ]; - let dummy_digest = Digest::new([1, 2, 3, 4, 5].map(BFieldElement::new)); - let non_determinism = NonDeterminism::new(vec![]).with_digests(vec![dummy_digest]); + let dummy_digest = Digest::new(bfe_array![1, 2, 3, 4, 5]); + let non_determinism = NonDeterminism::default().with_digests(vec![dummy_digest]); let programs_with_input = programs.map(|program| { ProgramAndInput::new(program).with_non_determinism(non_determinism.clone()) }); let test_rows = programs_with_input.map(|p_w_i| test_row_from_program_with_input(p_w_i, 2)); let debug_info = TestRowsDebugInfo { - instruction: DivineSibling, - debug_cols_curr_row: vec![ST0, ST1, ST2, ST3, ST4, ST5], - debug_cols_next_row: vec![ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9, ST10], + instruction: MerkleStep, + debug_cols_curr_row: vec![ST0, ST1, ST2, ST3, ST4, ST5, HV0, HV1, HV2, HV3, HV4, HV5], + debug_cols_next_row: vec![ST0, ST1, ST2, ST3, ST4, ST5], }; assert_constraints_for_rows_with_debug_info(&test_rows, debug_info); } diff --git a/triton-vm/src/vm.rs b/triton-vm/src/vm.rs index afd5e9d96..d006f2adb 100644 --- a/triton-vm/src/vm.rs +++ b/triton-vm/src/vm.rs @@ -50,7 +50,7 @@ pub struct VMState { /// A list of [`BFieldElement`]s the program can read from using instruction `divine`. pub secret_individual_tokens: VecDeque, - /// A list of [`Digest`]s the program can read from using instruction `divine_sibling`. + /// A list of [`Digest`]s the program can use for instruction `merkle_step`. pub secret_digests: VecDeque, /// The read-write **random-access memory** allows Triton VM to store arbitrary data. @@ -154,9 +154,11 @@ impl VMState { let decomposition = decomposition.map(BFieldElement::new); hvs[1..6].copy_from_slice(&decomposition); } - DivineSibling => { + MerkleStep => { + let divined_digest = self.secret_digests.front().copied().unwrap_or_default(); let node_index = self.op_stack[ST5].value(); - hvs[0] = bfe!(node_index % 2); + hvs[..5].copy_from_slice(&divined_digest.values()); + hvs[5] = bfe!(node_index % 2); } Split => { let top_of_stack = self.op_stack[ST0].value(); @@ -230,7 +232,6 @@ impl VMState { SpongeInit => self.sponge_init(), SpongeAbsorb => self.sponge_absorb()?, SpongeSqueeze => self.sponge_squeeze()?, - DivineSibling => self.divine_sibling()?, AssertVector => self.assert_vector()?, Add => self.add()?, Mul => self.mul()?, @@ -250,6 +251,7 @@ impl VMState { XbMul => self.xb_mul()?, WriteIo(n) => self.write_io(n)?, ReadIo(n) => self.read_io(n)?, + MerkleStep => self.merkle_step()?, XxDotStep => self.xx_dot_step()?, XbDotStep => self.xb_dot_step()?, }; @@ -506,33 +508,6 @@ impl VMState { Ok(co_processor_calls) } - fn divine_sibling(&mut self) -> Result> { - if self.secret_digests.is_empty() { - return Err(EmptySecretDigestInput); - } - self.op_stack.is_u32(ST5)?; - - let known_digest = self.op_stack.pop_multiple()?; - let node_index = self.op_stack.pop_u32()?; - - let parent_node_index = node_index / 2; - self.op_stack.push(parent_node_index.into()); - - let sibling_digest = self.pop_secret_digest()?; - let (left_digest, right_digest) = - Self::put_known_digest_on_correct_side(node_index, known_digest, sibling_digest); - - for &digest_element in right_digest.iter().rev() { - self.op_stack.push(digest_element); - } - for &digest_element in left_digest.iter().rev() { - self.op_stack.push(digest_element); - } - - self.instruction_pointer += 1; - Ok(vec![]) - } - fn assert_vector(&mut self) -> Result> { for i in 0..tip5::DIGEST_LENGTH { if self.op_stack[i] != self.op_stack[i + tip5::DIGEST_LENGTH] { @@ -777,6 +752,43 @@ impl VMState { Ok(vec![]) } + fn merkle_step(&mut self) -> Result> { + if self.secret_digests.is_empty() { + return Err(EmptySecretDigestInput); + } + self.op_stack.is_u32(ST5)?; + + let accumulator_digest = self.op_stack.pop_multiple::<{ tip5::DIGEST_LENGTH }>()?; + let node_index = self.op_stack.pop_u32()?; + + let parent_node_index = node_index / 2; + self.op_stack.push(parent_node_index.into()); + + let stack_contains_left_node = node_index % 2 == 0; + let sibling_digest = self.pop_secret_digest()?; + let mut hash_input = Tip5::new(Domain::FixedLength); + if stack_contains_left_node { + hash_input.state[..tip5::DIGEST_LENGTH].copy_from_slice(&accumulator_digest); + hash_input.state[tip5::DIGEST_LENGTH..2 * tip5::DIGEST_LENGTH] + .copy_from_slice(&sibling_digest); + } else { + hash_input.state[..tip5::DIGEST_LENGTH].copy_from_slice(&sibling_digest); + hash_input.state[tip5::DIGEST_LENGTH..2 * tip5::DIGEST_LENGTH] + .copy_from_slice(&accumulator_digest); + } + let tip5_trace = hash_input.trace(); + let accumulator_digest = &tip5_trace[tip5_trace.len() - 1][0..tip5::DIGEST_LENGTH]; + + for i in (0..tip5::DIGEST_LENGTH).rev() { + self.op_stack.push(accumulator_digest[i]); + } + + let co_processor_calls = vec![Tip5Trace(Hash, Box::new(tip5_trace))]; + + self.instruction_pointer += 1; + Ok(co_processor_calls) + } + fn xx_dot_step(&mut self) -> Result> { self.start_recording_ram_calls(); let mut rhs_address = self.op_stack.pop()?; @@ -937,25 +949,6 @@ impl VMState { Ok(digest.values()) } - /// If the given node index indicates a left node, puts the known digest to the left. - /// Otherwise, puts the known digest to the right. - /// Returns the left and right digests in that order. - fn put_known_digest_on_correct_side( - node_index: u32, - known_digest: [BFieldElement; tip5::DIGEST_LENGTH], - sibling_digest: [BFieldElement; tip5::DIGEST_LENGTH], - ) -> ( - [BFieldElement; tip5::DIGEST_LENGTH], - [BFieldElement; tip5::DIGEST_LENGTH], - ) { - let is_left_node = node_index % 2 == 0; - if is_left_node { - (known_digest, sibling_digest) - } else { - (sibling_digest, known_digest) - } - } - /// Run Triton VM on this state to completion, or until an error occurs. pub fn run(&mut self) -> Result<()> { while !self.halting { @@ -1113,6 +1106,7 @@ pub(crate) mod tests { use crate::triton_asm; use crate::triton_instr; use crate::triton_program; + use crate::LabelledInstruction; use super::*; @@ -1211,50 +1205,51 @@ pub(crate) mod tests { hash read_io 1 eq assert halt ); - let hash_input = [3, 2, 1, 0, 0, 0, 0, 0, 0, 0].map(BFieldElement::new); + let hash_input = bfe_array![3, 2, 1, 0, 0, 0, 0, 0, 0, 0]; let digest = Tip5::hash_10(&hash_input); ProgramAndInput::new(program).with_input(&digest[..=0]) } - pub(crate) fn test_program_for_divine_sibling_no_switch() -> ProgramAndInput { - let program = triton_program!( - push 3 - push 4 push 2 push 2 push 2 push 1 - divine_sibling + /// Helper function that returns code to push a digest to the top of the stack + fn push_digest_to_stack_tasm(Digest([d0, d1, d2, d3, d4]): Digest) -> Vec { + triton_asm!(push {d4} push {d3} push {d2} push {d1} push {d0}) + } - push 4 push 3 push 2 push 1 push 0 - assert_vector pop 5 + pub(crate) fn test_program_for_merkle_step_right_sibling() -> ProgramAndInput { + let accumulator_digest = Digest::new(bfe_array![2, 12, 22, 32, 42]); + let divined_digest = Digest::new(bfe_array![10, 11, 12, 13, 14]); + let expected_digest = Tip5::hash_pair(divined_digest, accumulator_digest); + let merkle_tree_node_index = 3; + let program = triton_program!( + push {merkle_tree_node_index} + {&push_digest_to_stack_tasm(accumulator_digest)} + merkle_step - push 4 push 2 push 2 push 2 push 1 + {&push_digest_to_stack_tasm(expected_digest)} assert_vector pop 5 - assert halt ); - let dummy_digest = Digest([0, 1, 2, 3, 4].map(BFieldElement::new)); - let non_determinism = NonDeterminism::default().with_digests(vec![dummy_digest]); - + let non_determinism = NonDeterminism::default().with_digests(vec![divined_digest]); ProgramAndInput::new(program).with_non_determinism(non_determinism) } - pub(crate) fn test_program_for_divine_sibling_switch() -> ProgramAndInput { + pub(crate) fn test_program_for_merkle_step_left_sibling() -> ProgramAndInput { + let accumulator_digest = Digest::new(bfe_array![2, 12, 22, 32, 42]); + let divined_digest = Digest::new(bfe_array![10, 11, 12, 13, 14]); + let expected_digest = Tip5::hash_pair(accumulator_digest, divined_digest); + let merkle_tree_node_index = 2; let program = triton_program!( - push 2 - push 4 push 2 push 2 push 2 push 1 - divine_sibling + push {merkle_tree_node_index} + {&push_digest_to_stack_tasm(accumulator_digest)} + merkle_step - push 4 push 2 push 2 push 2 push 1 + {&push_digest_to_stack_tasm(expected_digest)} assert_vector pop 5 - - push 4 push 3 push 2 push 1 push 0 - assert_vector pop 5 - assert halt ); - let dummy_digest = Digest([0, 1, 2, 3, 4].map(BFieldElement::new)); - let non_determinism = NonDeterminism::default().with_digests(vec![dummy_digest]); - + let non_determinism = NonDeterminism::default().with_digests(vec![divined_digest]); ProgramAndInput::new(program).with_non_determinism(non_determinism) } @@ -2098,6 +2093,18 @@ pub(crate) mod tests { assert!(b_field_element::BFIELD_ZERO == vm_state.op_stack[ST0]); } + #[test] + fn run_tvm_merkle_step_right_sibling() { + let program_and_input = test_program_for_merkle_step_right_sibling(); + let_assert!(Ok(_) = program_and_input.run()); + } + + #[test] + fn run_tvm_merkle_step_left_sibling() { + let program_and_input = test_program_for_merkle_step_left_sibling(); + let_assert!(Ok(_) = program_and_input.run()); + } + #[test] fn run_tvm_halt_then_do_stuff() { let program = triton_program!(halt push 1 push 2 add invert write_io 5); @@ -2350,10 +2357,14 @@ pub(crate) mod tests { } fn instruction_does_not_change_vm_state_when_crashing_vm( - program: Program, + program_and_input: ProgramAndInput, num_preparatory_steps: usize, ) { - let mut vm_state = VMState::new(&program, [].into(), [].into()); + let mut vm_state = VMState::new( + &program_and_input.program, + program_and_input.public_input, + program_and_input.non_determinism, + ); for i in 0..num_preparatory_steps { assert!(let Ok(_) = vm_state.step(), "failed during step {i}"); } @@ -2365,124 +2376,134 @@ pub(crate) mod tests { #[test] fn instruction_pop_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 pop 2 halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_divine_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { divine 1 halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 0); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 0); } #[test] fn instruction_assert_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 assert halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] - fn instruction_divine_sibling_does_not_change_vm_state_when_crashing_vm() { + fn instruction_merkle_step_does_not_change_vm_state_when_crashing_vm_invalid_node_index() { let non_u32 = u64::from(u32::MAX) + 1; - let program = triton_program! { push {non_u32} swap 5 divine_sibling halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 2); + let program = triton_program! { push {non_u32} swap 5 merkle_step halt }; + let nondeterminism = NonDeterminism::default().with_digests([Digest::default()]); + let program_and_input = ProgramAndInput::new(program).with_non_determinism(nondeterminism); + instruction_does_not_change_vm_state_when_crashing_vm(program_and_input, 2); + } + + #[test] + fn instruction_merkle_step_does_not_change_vm_state_when_crashing_vm_no_nd_digests() { + let valid_u32 = u64::from(u32::MAX); + let program = triton_program! { push {valid_u32} swap 5 merkle_step halt }; + let program_and_input = ProgramAndInput::new(program); + instruction_does_not_change_vm_state_when_crashing_vm(program_and_input, 2); } #[test] fn instruction_assert_vector_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 push 1 push 0 push 0 push 0 assert_vector halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 5); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 5); } #[test] fn instruction_sponge_absorb_does_not_change_vm_state_when_crashing_vm() { let ten_pushes = triton_asm![push 0; 10]; let program = triton_program! { {&ten_pushes} sponge_absorb halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 10); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 10); } #[test] fn instruction_sponge_squeeze_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { sponge_squeeze halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 0); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 0); } #[test] fn instruction_invert_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 invert halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_lt_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} lt halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_and_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} and halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_xor_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} xor halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_log_2_floor_on_non_u32_operand_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} log_2_floor halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_log_2_floor_on_operand_0_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 log_2_floor halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_pow_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} push 0 pow halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 2); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 2); } #[test] fn instruction_div_mod_on_non_u32_operand_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} push 0 div_mod halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 2); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 2); } #[test] fn instruction_div_mod_on_denominator_0_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { push 0 push 1 div_mod halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 2); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 2); } #[test] fn instruction_pop_count_does_not_change_vm_state_when_crashing_vm() { let non_u32 = u64::from(u32::MAX) + 1; let program = triton_program! { push {non_u32} pop_count halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 1); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 1); } #[test] fn instruction_x_invert_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { x_invert halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 0); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 0); } #[test] fn instruction_read_io_does_not_change_vm_state_when_crashing_vm() { let program = triton_program! { read_io 1 halt }; - instruction_does_not_change_vm_state_when_crashing_vm(program, 0); + instruction_does_not_change_vm_state_when_crashing_vm(ProgramAndInput::new(program), 0); } #[proptest]