From 01e6e0f6fd92d8ab1cc99466086b74c2d4aef86d Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 10 Oct 2023 09:23:47 +0000 Subject: [PATCH] Witgen Refactoring: Pull out wrapping handling into Generator --- executor/src/witgen/generator.rs | 85 +++++++++++-- executor/src/witgen/processor.rs | 4 + executor/src/witgen/rows.rs | 33 +++++- executor/src/witgen/sequence_iterator.rs | 3 +- .../src/witgen/symbolic_witness_evaluator.rs | 8 +- executor/src/witgen/vm_processor.rs | 112 ++++++++---------- 6 files changed, 164 insertions(+), 81 deletions(-) diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index c511e4420..a211b1781 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -1,16 +1,20 @@ use ast::analyzed::{Expression, Identity, IdentityKind, PolyID, PolynomialReference}; use ast::parsed::SelectedExpressions; -use number::FieldElement; +use number::{DegreeType, FieldElement}; use std::collections::{HashMap, HashSet}; +use crate::witgen::rows::CellValue; + use super::affine_expression::AffineExpression; use super::column_map::WitnessColumnMap; -use super::identity_processor::Machines; +use super::identity_processor::{IdentityProcessor, Machines}; use super::machines::Machine; +use super::processor::Processor; use super::range_constraints::RangeConstraint; use super::machines::FixedLookup; use super::rows::{transpose_rows, Row, RowFactory}; +use super::sequence_iterator::{DefaultSequenceIterator, ProcessingSequenceIterator}; use super::vm_processor::VmProcessor; use super::{EvalResult, FixedData, MutableState}; @@ -68,20 +72,85 @@ impl<'a, T: FieldElement> Generator<'a, T> { where Q: FnMut(&str) -> Option + Send + Sync, { - // For now, run the VM Processor on an empty block of the size of the degree - // In the future, we'll instantate a processor for each block and then stitch them together here. - let row_factory = RowFactory::new(self.fixed_data, self.global_range_constraints.clone()); - let default_row = row_factory.fresh_row(); - let data = vec![default_row; self.fixed_data.degree as usize]; + let first_row = self.compute_partial_first_row(mutable_state); + self.data = self.process(first_row, mutable_state); + self.fix_first_row(); + } + /// Runs the solver on the row pair (degree - 1, 0) in order to partially compute the first + /// row from identities like `pc' = (1 - first_step') * <...>`. + fn compute_partial_first_row(&self, mutable_state: &mut MutableState<'a, T, Q>) -> Row<'a, T> + where + Q: FnMut(&str) -> Option + Send + Sync, + { + // Use `Processor` + `DefaultSequenceIterator` using a "block size" of 0. Because `Processor` + // expects `data` to include the row before and after the block, this means we'll run the + // solver on exactly one row pair. + // Note that using `Processor` instead of `VmProcessor` is more convenient here because + // it does not assert that the row is "complete" afterwards (i.e., that all identities + // are satisfied assuming 0 for unknown values). + let mut identity_processor = IdentityProcessor::new( + self.fixed_data, + &mut mutable_state.fixed_lookup, + mutable_state.machines.iter_mut().into(), + ); + let row_factory = RowFactory::new(self.fixed_data, self.global_range_constraints.clone()); + let data = vec![row_factory.fresh_row(); 2]; + let mut processor = Processor::new( + self.fixed_data.degree - 1, + data, + &mut identity_processor, + &self.identities, + self.fixed_data, + row_factory, + &self.witnesses, + ); + let mut sequence_iterator = ProcessingSequenceIterator::Default( + DefaultSequenceIterator::new(0, self.identities.len(), None), + ); + processor.solve(&mut sequence_iterator).unwrap(); + let first_row = processor.finish().remove(1); + + first_row + } + + fn process( + &self, + first_row: Row<'a, T>, + mutable_state: &mut MutableState<'a, T, Q>, + ) -> Vec> + where + Q: FnMut(&str) -> Option + Send + Sync, + { + log::trace!("{}", first_row.render("first row", false, &self.witnesses)); + let data = vec![first_row]; + let row_factory = RowFactory::new(self.fixed_data, self.global_range_constraints.clone()); let mut processor = VmProcessor::new( self.fixed_data, &self.identities, self.witnesses.clone(), data, + row_factory, ); processor.run(mutable_state); + processor.finish() + } - self.data = processor.finish(); + /// At the end of the solving algorithm, we'll have computed the first row twice + /// (as row 0 and as row ). This function merges the two versions. + fn fix_first_row(&mut self) { + assert_eq!(self.data.len() as DegreeType, self.fixed_data.degree + 1); + + let last_row = self.data.pop().unwrap(); + self.data[0] = WitnessColumnMap::from(self.data[0].values().zip(last_row.values()).map( + |(cell1, cell2)| match (&cell1.value, &cell2.value) { + (CellValue::Known(v1), CellValue::Known(v2)) => { + assert_eq!(v1, v2); + cell1.clone() + } + (CellValue::Known(_), _) => cell1.clone(), + _ => cell2.clone(), + }, + )); } } diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 6e067314d..3e169d59f 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -102,6 +102,10 @@ impl<'a, 'b, 'c, T: FieldElement> Processor<'a, 'b, 'c, T, WithoutCalldata> { witness_cols: self.witness_cols, } } + + pub fn finish(self) -> Vec> { + self.data + } } impl<'a, 'b, T: FieldElement> Processor<'a, 'b, '_, T, WithCalldata> { diff --git a/executor/src/witgen/rows.rs b/executor/src/witgen/rows.rs index 05c2dab82..e011184d8 100644 --- a/executor/src/witgen/rows.rs +++ b/executor/src/witgen/rows.rs @@ -307,12 +307,13 @@ pub enum UnknownStrategy { /// to return for a given [PolynomialReference]. pub struct RowPair<'row, 'a, T: FieldElement> { pub current: &'row Row<'a, T>, - pub next: &'row Row<'a, T>, + pub next: Option<&'row Row<'a, T>>, pub current_row_index: DegreeType, fixed_data: &'a FixedData<'a, T>, unknown_strategy: UnknownStrategy, } impl<'row, 'a, T: FieldElement> RowPair<'row, 'a, T> { + /// Creates a new row pair. pub fn new( current: &'row Row<'a, T>, next: &'row Row<'a, T>, @@ -322,17 +323,39 @@ impl<'row, 'a, T: FieldElement> RowPair<'row, 'a, T> { ) -> Self { Self { current, - next, + next: Some(next), current_row_index, fixed_data, unknown_strategy, } } + /// Creates a new row pair from a single row, setting the next row to None. + pub fn from_single_row( + current: &'row Row<'a, T>, + current_row_index: DegreeType, + fixed_data: &'a FixedData<'a, T>, + unknown_strategy: UnknownStrategy, + ) -> Self { + Self { + current, + next: None, + current_row_index, + fixed_data, + unknown_strategy, + } + } + + /// Gets the cell corresponding to the given polynomial reference. + /// + /// # Panics + /// Panics if the next row is accessed but the row pair has been constructed with + /// [RowPair::from_single_row]. fn get_cell(&self, poly: &PolynomialReference) -> &Cell { - match poly.next { - false => &self.current[&poly.poly_id()], - true => &self.next[&poly.poly_id()], + match (poly.next, self.next.as_ref()) { + (false, _) => &self.current[&poly.poly_id()], + (true, Some(next)) => &next[&poly.poly_id()], + (true, None) => panic!("Tried to access next row, but it is not available."), } } diff --git a/executor/src/witgen/sequence_iterator.rs b/executor/src/witgen/sequence_iterator.rs index 6a9b6bc86..e763202b8 100644 --- a/executor/src/witgen/sequence_iterator.rs +++ b/executor/src/witgen/sequence_iterator.rs @@ -38,7 +38,6 @@ const MAX_ROUNDS_PER_ROW_DELTA: usize = 100; impl DefaultSequenceIterator { pub fn new(block_size: usize, identities_count: usize, outer_query_row: Option) -> Self { - assert!(block_size >= 1); let max_row = block_size as i64 - 1; DefaultSequenceIterator { identities_count, @@ -113,7 +112,7 @@ impl DefaultSequenceIterator { pub fn next(&mut self) -> Option { self.update_state(); - if self.cur_row_delta_index == self.row_deltas.len() { + if self.cur_row_delta_index == self.row_deltas.len() || self.identities_count == 0 { // Done! return None; } diff --git a/executor/src/witgen/symbolic_witness_evaluator.rs b/executor/src/witgen/symbolic_witness_evaluator.rs index fd2f151ef..93753f144 100644 --- a/executor/src/witgen/symbolic_witness_evaluator.rs +++ b/executor/src/witgen/symbolic_witness_evaluator.rs @@ -46,12 +46,8 @@ where } else { // Constant polynomial (or something else) let values = self.fixed_data.fixed_cols[&poly.poly_id()].values; - let row = if poly.next { - let degree = values.len() as DegreeType; - (self.row + 1) % degree - } else { - self.row - }; + let row = + if poly.next { self.row + 1 } else { self.row } % (values.len() as DegreeType); Ok(values[row as usize].into()) } } diff --git a/executor/src/witgen/vm_processor.rs b/executor/src/witgen/vm_processor.rs index 25542d9eb..7f843c215 100644 --- a/executor/src/witgen/vm_processor.rs +++ b/executor/src/witgen/vm_processor.rs @@ -11,16 +11,9 @@ use crate::witgen::rows::RowUpdater; use super::query_processor::QueryProcessor; -use super::rows::{Row, RowPair, UnknownStrategy}; +use super::rows::{Row, RowFactory, RowPair, UnknownStrategy}; use super::{EvalError, EvalResult, EvalValue, FixedData, MutableState}; -/// Phase in which [VmProcessor::compute_row] is called. -#[derive(Debug, PartialEq)] -enum ProcessingPhase { - Initialization, - Regular, -} - /// A list of identities with a flag whether it is complete. struct CompletableIdentities<'a, T: FieldElement> { identities_with_complete: Vec<(&'a Identity>, bool)>, @@ -54,6 +47,7 @@ pub struct VmProcessor<'a, T: FieldElement> { data: Vec>, last_report: DegreeType, last_report_time: Instant, + row_factory: RowFactory<'a, T>, } impl<'a, T: FieldElement> VmProcessor<'a, T> { @@ -62,6 +56,7 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { identities: &[&'a Identity>], witnesses: HashSet, data: Vec>, + row_factory: RowFactory<'a, T>, ) -> Self { let (identities_with_next, identities_without_next): (Vec<_>, Vec<_>) = identities .iter() @@ -73,6 +68,7 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { identities_with_next_ref: identities_with_next, identities_without_next_ref: identities_without_next, data, + row_factory, last_report: 0, last_report_time: Instant::now(), } @@ -82,26 +78,19 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { self.data } - fn last_row(&self) -> DegreeType { - self.fixed_data.degree - 1 - } - + /// Starting out with a single row, iteratively append rows until we have degree + 1 rows + /// (i.e., we have the first row twice). pub fn run(&mut self, mutable_state: &mut MutableState<'a, T, Q>) where Q: FnMut(&str) -> Option + Send + Sync, { - // For identities like `pc' = (1 - first_step') * <...>`, we need to process the last - // row before processing the first row. - self.compute_row( - self.last_row(), - ProcessingPhase::Initialization, - mutable_state, - ); + assert!(self.data.len() == 1); // Are we in an infinite loop and can just re-use the old values? let mut looping_period = None; let mut loop_detection_log_level = log::Level::Info; - for row_index in 0..self.fixed_data.degree as DegreeType { + let rows_left = self.fixed_data.degree + 1; + for row_index in 0..rows_left { self.maybe_log_performance(row_index); // Check if we are in a loop. if looping_period.is_none() && row_index % 100 == 0 && row_index > 0 { @@ -126,10 +115,16 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { loop_detection_log_level = log::Level::Debug; } } - if looping_period.is_none() { - self.compute_row(row_index, ProcessingPhase::Regular, mutable_state); + // Note that we exit one iteration early in the non-loop case, + // because ensure_has_next_row() + compute_row() will already + // add and compute some values for the next row as well. + if looping_period.is_none() && row_index != rows_left - 1 { + self.ensure_has_next_row(row_index); + self.compute_row(row_index, mutable_state); }; } + + assert_eq!(self.data.len() as DegreeType, self.fixed_data.degree + 1); } /// Checks if the last rows are repeating and returns the period. @@ -152,16 +147,18 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { // Returns a reference to a given row fn row(&self, row_index: DegreeType) -> &Row<'a, T> { - let row_index = (row_index + self.fixed_data.degree) % self.fixed_data.degree; &self.data[row_index as usize] } - fn compute_row( - &mut self, - row_index: DegreeType, - phase: ProcessingPhase, - mutable_state: &mut MutableState<'a, T, Q>, - ) where + fn ensure_has_next_row(&mut self, row_index: DegreeType) { + assert!(self.data.len() as DegreeType > row_index); + if row_index == self.data.len() as DegreeType - 1 { + self.data.push(self.row_factory.fresh_row()); + } + } + + fn compute_row(&mut self, row_index: DegreeType, mutable_state: &mut MutableState<'a, T, Q>) + where Q: FnMut(&str) -> Option + Send + Sync, { log::trace!("Row: {}", row_index); @@ -202,30 +199,23 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { // Check that the computed row is "final" by asserting that all unknown values can // be set to 0. - // This check is skipped in the initialization phase (run on the last row), - // because its only purpose is to transfer values to the first row, - // not to finalize the last row. - if phase == ProcessingPhase::Regular { - log::trace!( - " Checking that remaining identities hold when unknown values are set to 0" - ); + log::trace!(" Checking that remaining identities hold when unknown values are set to 0"); + self.process_identities( + row_index, + &mut identities_without_next_ref, + UnknownStrategy::Zero, + &mut identity_processor, + ) + .and_then(|_| { self.process_identities( row_index, - &mut identities_without_next_ref, + &mut identities_with_next_ref, UnknownStrategy::Zero, &mut identity_processor, ) - .and_then(|_| { - self.process_identities( - row_index, - &mut identities_with_next_ref, - UnknownStrategy::Zero, - &mut identity_processor, - ) - }) - .map_err(|e| self.report_failure_and_panic_underconstrained(row_index, e)) - .unwrap(); - } + }) + .map_err(|e| self.report_failure_and_panic_underconstrained(row_index, e)) + .unwrap(); log::trace!( "{}", @@ -349,13 +339,7 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { updates: &EvalValue<&PolynomialReference, T>, source_name: impl Fn() -> String, ) -> bool { - let (before, after) = if row_index == self.last_row() { - // Last row is current, first row is next - let (after, before) = self.data.split_at_mut(row_index as usize); - (before, after) - } else { - self.data.split_at_mut(row_index as usize + 1) - }; + let (before, after) = self.data.split_at_mut(row_index as usize + 1); let current = before.last_mut().unwrap(); let next = after.first_mut().unwrap(); let mut row_updater = RowUpdater::new(current, next, row_index); @@ -447,12 +431,21 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { && self.check_row_pair(row_index, &proposed_row, true, &mut identity_processor); if constraints_valid { - self.data[row_index as usize] = proposed_row; + if row_index as usize == self.data.len() - 1 { + // We might already have added the row in [VmProcessor::ensure_has_next_row] + self.data[row_index as usize] = proposed_row; + } else { + // If the previous row was also added by [VmProcessor::try_propose_row], we won't have an entry + // for the current row yet. + assert_eq!(row_index as usize, self.data.len()); + self.data.push(proposed_row); + } } else { // Note that we never update the next row if proposing a row succeeds (the happy path). // If it doesn't, we re-run compute_next_row on the previous row in order to // correctly forward-propagate values via next references. - self.compute_row(row_index - 1, ProcessingPhase::Regular, mutable_state); + self.ensure_has_next_row(row_index - 1); + self.compute_row(row_index - 1, mutable_state); } constraints_valid } @@ -476,10 +469,9 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { ), // Check whether identities without a reference to the next row are satisfied // when applied to the proposed row. - // Note that we also provide the next row here, but it is not used. - false => RowPair::new( + // Because we never access the next row, we can use [RowPair::from_single_row] here. + false => RowPair::from_single_row( proposed_row, - self.row(row_index + 1), row_index, self.fixed_data, UnknownStrategy::Zero,