diff --git a/CHANGELOG.md b/CHANGELOG.md index 618262432..1339a32a5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ #### Fixes - Fixed an issue with formatting of blocks in Miden Assembly syntax +- Fixed the construction of the block hash table (#1506) #### Fixes diff --git a/docs/src/design/decoder/constraints.md b/docs/src/design/decoder/constraints.md index 4067c41da..8c38a8652 100644 --- a/docs/src/design/decoder/constraints.md +++ b/docs/src/design/decoder/constraints.md @@ -287,10 +287,10 @@ Graphically, this looks like so: In a similar manner, we define a value representing the result of hash computation as follows: $$ -bh = \alpha_0 + \alpha_1 \cdot a + \sum_{i=0}^3(\alpha_{i+2} \cdot h_i) + \alpha_7 \cdot h_4 \text{ | degree} = 1 +bh = \alpha_0 + \alpha_1 \cdot a' + \sum_{i=0}^3(\alpha_{i+2} \cdot h_i) + \alpha_7 \cdot f_{is\_loop\_body} \text{ | degree} = 1 $$ -Note that in the above we use $a$ (block address from the current row) rather than $a'$ (block address from the next row) as we did for for values of $ch_1$ and $ch_2$. Also, note that we are not adding a flag indicating whether the block is the first child of a join block (i.e., $\alpha_6$ term is missing). It will be added later on. +Above, $f_{is\_loop\_body}$ refers to the value in the `IS_LOOP_BODY` column (already constrained to be 0 or 1), located in $h_4$. Also, note that we are not adding a flag indicating whether the block is the first child of a join block (i.e., $\alpha_6$ term is missing). It will be added later on. Using the above variables, we define row values to be added to and removed from the block hash table as follows. @@ -326,17 +326,23 @@ $$ v_{dyn} = f_{dyn} \cdot ch_{dyn} \text{ | degree} = 6 $$ -When `END` operation is executed, hash of the completed block is removed from the block hash table. However, we also need to differentiate between removing the first and the second child of a *join* block. We do this by looking at the next operation. Specifically, if the next operation is neither `END` nor `REPEAT` we know that another block is about to be executed, and thus, we have just finished executing the first child of a *join* block. Thus, if the next operation is neither `END` nor `REPEAT` we need to set the term for $\alpha_6$ coefficient to $1$ as shown below: +When the `CALL` or `SYSCALL` operation is executed, the hash of the callee is added to the block hash table. $$ -u_{end} = f_{end} \cdot (bh + \alpha_6 \cdot (1 - (f_{end}' + f_{repeat}'))) \text{ | } \text{degree} = 8 +v_{call\_or\_syscall} = (f_{call} + f_{syscall}) \cdot ch_1 \text{ | degree} = 5 +$$ + +When `END` operation is executed, hash of the completed block is removed from the block hash table. However, we also need to differentiate between removing the first and the second child of a *join* block. We do this by looking at the next operation. Specifically, if the next operation is neither `END` nor `REPEAT` nor `HALT`, we know that another block is about to be executed, and thus, we have just finished executing the first child of a *join* block. Thus, if the next operation is neither `END` nor `REPEAT` nor `HALT` we need to set the term for $\alpha_6$ coefficient to $1$ as shown below: + +$$ +u_{end} = f_{end} \cdot (bh + \alpha_6 \cdot (1 - (f_{end}' + f_{repeat}' + f_{halt}'))) \text{ | } \text{degree} = 8 $$ Using the above definitions, we can describe the constraint for updating the block hash table as follows: > $$ p_2' \cdot (u_{end} + 1 - f_{end}) = \\ -p_2 \cdot (v_{join} + v_{split} + v_{loop} + v_{repeat} + v_{dyn} + 1 - (f_{join} + f_{split} + f_{loop} + f_{repeat} + f_{dyn})) +p_2 \cdot (v_{join} + v_{split} + v_{loop} + v_{repeat} + v_{dyn} + v_{call\_or\_syscall} + 1 - (f_{join} + f_{split} + f_{loop} + f_{repeat} + f_{dyn} + f_{call} + f_{syscall})) $$ We need to add $1$ and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to $1$, the above constraint reduces to $p_2' = p_2$. diff --git a/processor/src/decoder/aux_trace/block_hash_table.rs b/processor/src/decoder/aux_trace/block_hash_table.rs index cba054d0b..818df3512 100644 --- a/processor/src/decoder/aux_trace/block_hash_table.rs +++ b/processor/src/decoder/aux_trace/block_hash_table.rs @@ -1,7 +1,7 @@ use miden_air::RowIndex; use vm_core::{ - Word, OPCODE_DYN, OPCODE_END, OPCODE_HALT, OPCODE_JOIN, OPCODE_LOOP, OPCODE_REPEAT, - OPCODE_SPLIT, ZERO, + Word, OPCODE_CALL, OPCODE_DYN, OPCODE_END, OPCODE_HALT, OPCODE_JOIN, OPCODE_LOOP, + OPCODE_REPEAT, OPCODE_SPLIT, OPCODE_SYSCALL, ZERO, }; use super::{AuxColumnBuilder, Felt, FieldElement, MainTrace, ONE}; @@ -56,6 +56,9 @@ impl> AuxColumnBuilder for BlockHashTableCo .unwrap_or(E::ONE), OPCODE_REPEAT => BlockHashTableRow::from_repeat(main_trace, row).collapse(alphas), OPCODE_DYN => BlockHashTableRow::from_dyn(main_trace, row).collapse(alphas), + OPCODE_CALL | OPCODE_SYSCALL => { + BlockHashTableRow::from_call_or_syscall(main_trace, row).collapse(alphas) + }, _ => E::ONE, } } @@ -226,6 +229,15 @@ impl BlockHashTableRow { } } + pub fn from_call_or_syscall(main_trace: &MainTrace, row: RowIndex) -> Self { + Self { + parent_block_id: main_trace.addr(row + 1), + child_block_hash: main_trace.decoder_hasher_state_first_half(row), + is_first_child: false, + is_loop_body: false, + } + } + // COLLAPSE // ---------------------------------------------------------------------------------------------- diff --git a/processor/src/decoder/aux_trace/mod.rs b/processor/src/decoder/aux_trace/mod.rs index c81618ede..fe2ff5c30 100644 --- a/processor/src/decoder/aux_trace/mod.rs +++ b/processor/src/decoder/aux_trace/mod.rs @@ -41,6 +41,9 @@ impl AuxTraceBuilder { let p2 = block_hash_column_builder.build_aux_column(main_trace, rand_elements); let p3 = op_group_table_column_builder.build_aux_column(main_trace, rand_elements); + debug_assert_eq!(*p2.last().unwrap(), E::ONE); + debug_assert_eq!(*p3.last().unwrap(), E::ONE); + vec![p1, p2, p3] } }