From a3087ea364a0821648e0db26f6704bb54f9f06f8 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 21 May 2024 18:09:06 +0200 Subject: [PATCH] Witgen: Handle machine calls with side effects (#1388) Cherry-picked ef6a72fcfab8a608f54b5e25cb173e51db953b69 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 | 18 ++++--- executor/src/witgen/generator.rs | 7 ++- executor/src/witgen/machines/block_machine.rs | 5 ++ .../machines/double_sorted_witness_machine.rs | 46 ++++++++++-------- .../witgen/machines/sorted_witness_machine.rs | 1 + .../src/witgen/machines/write_once_memory.rs | 11 ++++- executor/src/witgen/processor.rs | 4 +- pipeline/tests/asm.rs | 8 ++++ test_data/asm/side_effects.asm | 48 +++++++++++++++++++ 9 files changed, 118 insertions(+), 30 deletions(-) create mode 100644 test_data/asm/side_effects.asm diff --git a/executor/src/witgen/eval_result.rs b/executor/src/witgen/eval_result.rs index 40f53bb68..a03b46760 100644 --- a/executor/src/witgen/eval_result.rs +++ b/executor/src/witgen/eval_result.rs @@ -99,9 +99,14 @@ impl EvalStatus { } #[derive(Debug, Clone, PartialEq, Eq)] +/// The result of solving a constraint (polynomial identity, lookup, or permutation). pub struct EvalValue { + /// Assignments and range constraint updates resulting from the solving. pub constraints: Constraints, + /// The status of the solving. If complete, all variables are known after applying the constraints. pub status: EvalStatus, + /// Whether the solving had side effects. For example, a block might be added to another machine. + pub side_effect: bool, } impl EvalValue { @@ -134,21 +139,22 @@ impl EvalValue { fn new(constraints: Vec<(K, Constraint)>, status: EvalStatus) -> Self { Self { constraints, + side_effect: false, status, } } -} -impl EvalValue -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 } } diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index ce8cb4f33..980304bb3 100644 --- a/executor/src/witgen/generator.rs +++ b/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) } diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 740971874..c94355524 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/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); diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 7e0cdd4af..cf42d8baf 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/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,26 +398,19 @@ 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, @@ -425,7 +418,22 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { ); 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) } } diff --git a/executor/src/witgen/machines/sorted_witness_machine.rs b/executor/src/witgen/machines/sorted_witness_machine.rs index dfaeacc08..96deaadf4 100644 --- a/executor/src/witgen/machines/sorted_witness_machine.rs +++ b/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 => { diff --git a/executor/src/witgen/machines/write_once_memory.rs b/executor/src/witgen/machines/write_once_memory.rs index b7e74054b..c53cd3061 100644 --- a/executor/src/witgen/machines/write_once_memory.rs +++ b/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"), diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 23d4bff2b..0e230009f 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -211,6 +211,7 @@ 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, @@ -218,7 +219,8 @@ Known values in current row (local: {row_index}, global {global_row_index}): } 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(), }) } diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 4f44dc26d..1f76764fc 100644 --- a/pipeline/tests/asm.rs +++ b/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"; diff --git a/test_data/asm/side_effects.asm b/test_data/asm/side_effects.asm new file mode 100644 index 000000000..cf42e5c17 --- /dev/null +++ b/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; + } +}