Skip to content

Commit

Permalink
Process pc lookup first. (powdr-labs#1427)
Browse files Browse the repository at this point in the history
  • Loading branch information
chriseth authored Jun 10, 2024
1 parent 15f6208 commit 4ab45dc
Showing 1 changed file with 62 additions and 30 deletions.
92 changes: 62 additions & 30 deletions executor/src/witgen/vm_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -314,9 +314,29 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T
identities: &mut CompletableIdentities<'a, T>,
) -> Result<Constraints<&'a AlgebraicReference, T>, Vec<EvalError<T>>> {
let mut outer_assignments = vec![];

// The PC lookup fills most of the columns and enables hints thus it should be run first.
// We find it as largest plookup identity.
let pc_lookup_index = identities
.iter_mut()
.enumerate()
.filter(|(_, (ident, _))| ident.kind == IdentityKind::Plookup)
.max_by_key(|(_, (ident, _))| ident.left.expressions.len())
.map(|(i, _)| i);
loop {
let mut progress =
self.process_identities(row_index, identities, UnknownStrategy::Unknown)?;
let mut progress = false;
if let Some(pc_lookup_index) = pc_lookup_index {
let (identity, is_complete) =
&mut identities.identities_with_complete[pc_lookup_index];
let result = self
.process_identity(row_index, identity, is_complete, UnknownStrategy::Unknown)
.map_err(|e| vec![e])?;
if result == Some(true) {
progress |= true;
}
}

progress |= self.process_identities(row_index, identities, UnknownStrategy::Unknown)?;
let row_index = row_index as usize;
if let Some(true) = self.processor.latch_value(row_index) {
let (outer_query_progress, new_outer_assignments) = self
Expand Down Expand Up @@ -358,35 +378,11 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T
let mut errors = vec![];

for (identity, is_complete) in identities.iter_mut() {
if *is_complete {
continue;
}

let is_machine_call = matches!(
identity.kind,
IdentityKind::Plookup | IdentityKind::Permutation
);
if is_machine_call && unknown_strategy == UnknownStrategy::Zero {
// The fact that we got to the point where we assume 0 for unknown cells, but this identity
// is still not complete, means that either the inputs or the machine is under-constrained.
errors.push(format!("{identity}:\n{}",
indent("This machine call could not be completed. Either some inputs are missing or the machine is under-constrained.", 1)).into());
continue;
match self.process_identity(row_index, identity, is_complete, unknown_strategy) {
Ok(Some(result)) => progress |= result,
Ok(None) => (),
Err(e) => errors.push(e),
}

let result =
self.processor
.process_identity(row_index as usize, identity, unknown_strategy);

match result {
Ok(res) => {
*is_complete = res.is_complete;
progress |= res.progress;
}
Err(e) => {
errors.push(e);
}
};
}

if errors.is_empty() {
Expand All @@ -396,6 +392,42 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T
}
}

/// Processes a single identity and updates the "is_complete" flag.
/// Returns:
/// * `Ok(Some(true)`: If progress was made.
/// * `Ok(Some(false)`: If no progress was made.
/// * `Ok(None)`: If the identity has been complete already.
/// * `Err(e)`: If an error occurred.
fn process_identity(
&mut self,
row_index: DegreeType,
identity: &'a Identity<Expression<T>>,
is_complete: &mut bool,
unknown_strategy: UnknownStrategy,
) -> Result<Option<bool>, EvalError<T>> {
if *is_complete {
return Ok(None);
}

let is_machine_call = matches!(
identity.kind,
IdentityKind::Plookup | IdentityKind::Permutation
);
if is_machine_call && unknown_strategy == UnknownStrategy::Zero {
// The fact that we got to the point where we assume 0 for unknown cells, but this identity
// is still not complete, means that either the inputs or the machine is under-constrained.
return Err(format!(
"{identity}:\n This machine call could not be completed. Either some inputs are missing or the machine is under-constrained."
).into());
}

let result =
self.processor
.process_identity(row_index as usize, identity, unknown_strategy)?;
*is_complete = result.is_complete;
Ok(Some(result.progress))
}

fn report_failure_and_panic_unsatisfiable(
&self,
row_index: DegreeType,
Expand Down

0 comments on commit 4ab45dc

Please sign in to comment.