Skip to content

Commit

Permalink
Block machines: Skip complete identities (#1528)
Browse files Browse the repository at this point in the history
Just like the `VmProcessor`, with this PR the `BlockProcessor` never
processes an identity again that has been completed.

This should be a slight performance optimization (when the "default"
sequence iterator is used), but more importantly it:
- Fixes #1385 
- Allows us to remove error-prone code (see below)
- Helps with witgen for stateful machines, like those who access memory
  • Loading branch information
georgwiese committed Jul 3, 2024
1 parent 5691d6e commit c4ded73
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 57 deletions.
16 changes: 12 additions & 4 deletions executor/src/witgen/block_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,17 +67,25 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> BlockProcessor<'a, 'b, 'c
) -> Result<EvalValue<&'a AlgebraicReference, T>, EvalError<T>> {
let mut outer_assignments = vec![];

let mut is_identity_complete =
vec![vec![false; self.identities.len()]; self.processor.len()];

while let Some(SequenceStep { row_delta, action }) = sequence_iterator.next() {
let row_index = (1 + row_delta) as usize;
let progress = match action {
Action::InternalIdentity(identity_index) => {
self.processor
.process_identity(
if is_identity_complete[row_index][identity_index] {
// The identity has been completed already, there is no point in processing it again.
false
} else {
let res = self.processor.process_identity(
row_index,
self.identities[identity_index],
UnknownStrategy::Unknown,
)?
.progress
)?;
is_identity_complete[row_index][identity_index] = res.is_complete;
res.progress
}
}
Action::OuterQuery => {
let (progress, new_outer_assignments) =
Expand Down
52 changes: 1 addition & 51 deletions executor/src/witgen/machines/block_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,8 @@ use super::{EvalResult, FixedData, FixedLookup};

use crate::witgen::block_processor::BlockProcessor;
use crate::witgen::data_structures::finalizable_data::FinalizableData;
use crate::witgen::identity_processor::IdentityProcessor;
use crate::witgen::processor::{OuterQuery, Processor};
use crate::witgen::rows::{Row, RowIndex, RowPair, UnknownStrategy};
use crate::witgen::rows::{Row, RowIndex, RowPair};
use crate::witgen::sequence_iterator::{
DefaultSequenceIterator, ProcessingSequenceCache, ProcessingSequenceIterator,
};
Expand Down Expand Up @@ -464,17 +463,6 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
RowIndex::from_i64(self.rows() as i64 - 1, self.fixed_data.degree)
}

fn last_latch_row_index(&self) -> Option<RowIndex> {
if self.rows() > self.block_size as DegreeType {
Some(RowIndex::from_degree(
self.rows() - self.block_size as DegreeType + self.latch_row as DegreeType,
self.fixed_data.degree,
))
} else {
None
}
}

fn get_row(&self, row: RowIndex) -> &Row<T> {
// The first block is a dummy block corresponding to rows (-block_size, 0),
// so we have to add the block size to the row index.
Expand All @@ -495,44 +483,6 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
log::trace!(" {}", l);
}

// First check if we already store the value.
// This can happen in the loop detection case, where this function is just called
// to validate the constraints.
if outer_query.left.iter().all(|v| v.is_constant()) {
// All values on the left hand side are known, check if this is a query
// to the last row.
if let Some(row_index) = self.last_latch_row_index() {
let current = &self.get_row(row_index);
let fresh_row = Row::fresh(self.fixed_data, row_index + 1);
let next = if self.latch_row == self.block_size - 1 {
// We don't have the next row, because it would be the first row of the next block.
// We'll use a fresh row instead.
&fresh_row
} else {
self.get_row(row_index + 1)
};

let row_pair = RowPair::new(
current,
next,
row_index,
self.fixed_data,
UnknownStrategy::Unknown,
);

let mut identity_processor = IdentityProcessor::new(self.fixed_data, mutable_state);
if let Ok(result) = identity_processor.process_link(&outer_query, &row_pair) {
if result.is_complete() && result.constraints.is_empty() {
log::trace!(
"End processing block machine '{}' (already solved)",
self.name()
);
return Ok(result);
}
}
}
}

// TODO this assumes we are always using the same lookup for this machine.
let mut sequence_iterator = self
.processing_sequence_cache
Expand Down
2 changes: 0 additions & 2 deletions pipeline/tests/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -450,9 +450,7 @@ fn permutation_to_vm() {
}

#[test]
#[should_panic = "Verifier did not say 'PIL OK'."]
fn permutation_to_block_to_block() {
// TODO: witgen issue (https://github.com/powdr-labs/powdr/issues/1385)
let f = "asm/permutations/block_to_block.asm";
verify_asm(f, Default::default());
test_halo2(f, Default::default());
Expand Down

0 comments on commit c4ded73

Please sign in to comment.