fix: fix block hash table construction and docs (#1509)

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
 

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$.

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<E: FieldElement<BaseField = Felt>> AuxColumnBuilder<E> 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
     // ----------------------------------------------------------------------------------------------
 

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]
     }
 }