Witgen: Handle machine calls with side effects (#1388)

Cherry-picked ef6a72f from #1380.

With this PR, we track whether a call to a machine led to some side
effect (e.g. added a block). In that case, the processed identity should
count has having led to some progress, even if no values were returned
to the calling machine. An example would be writing values to memory,
which does not return any values and hence does not change the state of
the caller.

executor/src/witgen/eval_result.rs

@@ -99,9 +99,14 @@ impl<K> EvalStatus<K> {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
+/// The result of solving a constraint (polynomial identity, lookup, or permutation).
 pub struct EvalValue<K, T: FieldElement> {
+    /// Assignments and range constraint updates resulting from the solving.
     pub constraints: Constraints<K, T>,
+    /// The status of the solving. If complete, all variables are known after applying the constraints.
     pub status: EvalStatus<K>,
+    /// Whether the solving had side effects. For example, a block might be added to another machine.
+    pub side_effect: bool,
 }
 
 impl<K, T: FieldElement> EvalValue<K, T> {
@@ -134,21 +139,22 @@ impl<K, T: FieldElement> EvalValue<K, T> {
     fn new(constraints: Vec<(K, Constraint<T>)>, status: EvalStatus<K>) -> Self {
         Self {
             constraints,
+            side_effect: false,
             status,
         }
     }
-}
 
-impl<K, T> EvalValue<K, T>
-where
-    K: Clone,
-    T: FieldElement,
-{
     pub fn combine(&mut self, other: Self) {
         // reserve more space?
         self.constraints.extend(other.constraints);
         self.status =
             std::mem::replace(&mut self.status, EvalStatus::Complete).combine(other.status);
+        self.side_effect |= other.side_effect;
+    }
+
+    pub fn report_side_effect(mut self) -> Self {
+        self.side_effect = true;
+        self
     }
 }
 

executor/src/witgen/generator.rs

@@ -70,15 +70,18 @@ impl<'a, T: FieldElement> Machine<'a, T> for Generator<'a, T> {
         let ProcessResult { eval_value, block } =
             self.process(first_row, 0, mutable_state, Some(outer_query), false);
 
-        if eval_value.is_complete() {
+        let eval_value = if eval_value.is_complete() {
             log::trace!("End processing VM '{}' (successfully)", self.name());
             // Remove the last row of the previous block, as it is the first row of the current
             // block.
             self.data.pop();
             self.data.extend(block);
+
+            eval_value.report_side_effect()
         } else {
             log::trace!("End processing VM '{}' (incomplete)", self.name());
-        }
+            eval_value
+        };
         Ok(eval_value)
     }
 

executor/src/witgen/machines/block_machine.rs

@@ -561,6 +561,11 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
                 );
                 self.append_block(new_block)?;
 
+                // TODO: This would be the right thing to do, but currently leads to failing tests
+                // due to #1385 ("Witgen: Block machines "forget" that they already completed a block"):
+                // https://github.com/powdr-labs/powdr/issues/1385
+                // let updates = updates.report_side_effect();
+
                 // We solved the query, so report it to the cache.
                 self.processing_sequence_cache
                     .report_processing_sequence(left, sequence_iterator);

executor/src/witgen/machines/double_sorted_witness_machine.rs

@@ -382,7 +382,7 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> {
 
         // TODO this does not check any of the failure modes
         let mut assignments = EvalValue::complete(vec![]);
-        if is_write {
+        let has_side_effect = if is_write {
             let value = match value_expr.constant_value() {
                 Some(v) => v,
                 None => {
@@ -398,34 +398,42 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> {
                 value
             );
             self.data.insert(addr, value);
-            self.trace.insert(
-                (addr, step),
-                Operation {
-                    is_normal_write,
-                    is_bootloader_write,
-                    value,
-                    selector_id,
-                },
-            );
+            self.trace
+                .insert(
+                    (addr, step),
+                    Operation {
+                        is_normal_write,
+                        is_bootloader_write,
+                        value,
+                        selector_id,
+                    },
+                )
+                .is_none()
         } else {
             let value = self.data.entry(addr).or_default();
-            self.trace.insert(
-                (addr, step),
-                Operation {
-                    is_normal_write,
-                    is_bootloader_write,
-                    value: *value,
-                    selector_id,
-                },
-            );
             log::trace!(
                 "Memory read: addr={:x}, step={step}, value={:x}",
                 addr,
                 value
             );
             let ass = (value_expr.clone() - (*value).into()).solve()?;
             assignments.combine(ass);
+            self.trace
+                .insert(
+                    (addr, step),
+                    Operation {
+                        is_normal_write,
+                        is_bootloader_write,
+                        value: *value,
+                        selector_id,
+                    },
+                )
+                .is_none()
+        };
+        if has_side_effect {
+            assignments = assignments.report_side_effect();
         }
+
         Ok(assignments)
     }
 }

executor/src/witgen/machines/sorted_witness_machine.rs

@@ -258,6 +258,7 @@ impl<'a, T: FieldElement> SortedWitnesses<'a, T> {
                             "Stored {} = {key_value} -> {r} = {v}",
                             self.fixed_data.column_name(&self.key_col)
                         );
+                        assignments = assignments.report_side_effect();
                         *stored_value = Some(v);
                     }
                     None => {

executor/src/witgen/machines/write_once_memory.rs

@@ -195,10 +195,17 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> {
 
         // Write values
         let is_complete = !values.contains(&None);
-        self.data.insert(index, values);
+        let side_effect = self.data.insert(index, values).is_none();
 
         match is_complete {
-            true => Ok(EvalValue::complete(updates)),
+            true => Ok({
+                let res = EvalValue::complete(updates);
+                if side_effect {
+                    res.report_side_effect()
+                } else {
+                    res
+                }
+            }),
             false => Ok(EvalValue::incomplete_with_constraints(
                 updates,
                 IncompleteCause::NonConstantRequiredArgument("value"),

executor/src/witgen/processor.rs

@@ -211,14 +211,16 @@ Known values in current row (local: {row_index}, global {global_row_index}):
 
         if unknown_strategy == UnknownStrategy::Zero {
             assert!(updates.constraints.is_empty());
+            assert!(!updates.side_effect);
             return Ok(IdentityResult {
                 progress: false,
                 is_complete: false,
             });
         }
 
         Ok(IdentityResult {
-            progress: self.apply_updates(row_index, &updates, || identity.to_string()),
+            progress: self.apply_updates(row_index, &updates, || identity.to_string())
+                || updates.side_effect,
             is_complete: updates.is_complete(),
         })
     }

pipeline/tests/asm.rs

@@ -384,6 +384,14 @@ fn enum_in_asm() {
     gen_estark_proof(f, Default::default());
 }
 
+#[test]
+fn side_effects() {
+    let f = "asm/side_effects.asm";
+    verify_asm(f, Default::default());
+    test_halo2(f, Default::default());
+    gen_estark_proof(f, Default::default());
+}
+
 #[test]
 fn permutation_simple() {
     let f = "asm/permutations/simple.asm";

test_data/asm/side_effects.asm

@@ -0,0 +1,48 @@
+// This tests whether side effects are counted as "progress" when processing identities.
+// The MemoryProxy writes values to memory. Processing the link to memory does not result
+// in any updates to the MemoryProxy witness, but it does have a side effect (adding an
+// entry to the memory machine). Because of this, processing the link should not be skipped.
+
+use std::machines::memory::Memory;
+
+machine MemoryProxy with
+    latch: latch,
+    operation_id: operation_id,
+    call_selectors: sel,
+{
+    operation mstore<0> addr, step, value ->;
+
+    col witness operation_id;
+    col fixed latch = [1]*;
+
+    Memory mem;
+
+    col witness addr, step, value;
+
+    col witness used;
+    used = std::array::sum(sel);
+    std::utils::force_bool(used);
+
+    link used ~> mem.mstore addr, step, value ->;
+}
+
+machine Main with degree: 1024 {
+    reg pc[@pc];
+    reg X[<=];
+    reg Y[<=];
+    reg Z[<=];
+
+    col fixed STEP(i) { i };
+    MemoryProxy mem;
+    instr mstore X, Y -> ~ mem.mstore X, STEP, Y ->;
+
+    function main {
+
+        mstore 1, 1;
+        mstore 2, 2;
+        mstore 3, 3;
+        mstore 4, 4;
+
+        return;
+    }
+}