Witgen: Handle machine calls with side effects

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;
+    }
+}