Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Block machines: Skip complete identities #1528

Merged
merged 4 commits into from
Jul 3, 2024
Merged

Block machines: Skip complete identities #1528

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
58d23b2
Block machines: Skip complete identities
georgwiese Jul 3, 2024
9b042b2
Assert that no block machine is called twice
georgwiese Jul 3, 2024
38f27a1
Remove test if machine has been called
georgwiese Jul 3, 2024
6890731
Add comment
georgwiese Jul 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions executor/src/witgen/block_processor.rs
View file
Open in desktop
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
View file
Open in desktop
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);
}
}
}
}

Comment on lines -498 to -535
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Finally, we can remove this trouble maker! It is very error prone and had to be adjusted many times in the past.

Commit 9b042b2 asserts that it would never reach the return with the new changes (you can see the CI passes on this commit).

Basically, this code checks if the LHS we are getting happens to be exactly what is in the latch row of the last block that was added. But that only happens in practice if the identity is processed even though it was completed already. The VmProcessor already makes sure not to do that, and with this PR the BlockProcessor does too.

// 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
View file
Open in desktop
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
Loading