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