github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #676 from powdr-labs/pull-out-wrapping-handling

Browse Source 
Witgen Refactoring: Pull out wrapping handling into Generator
This commit is contained in:
Georg Wiese
2023-10-10 14:04:40 +00:00
committed by GitHub
parent b4a7df22e3 01e6e0f6fd
commit 017fd44945
6 changed files with 164 additions and 81 deletions
Download Patch File Download Diff File Expand all files Collapse all files

85
executor/src/witgen/generator.rs
View File

@@ -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<T> + 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<Q>(&self, mutable_state: &mut MutableState<'a, T, Q>) -> Row<'a, T>
where
Q: FnMut(&str) -> Option<T> + 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<Q>(
&self,
first_row: Row<'a, T>,
mutable_state: &mut MutableState<'a, T, Q>,
) -> Vec<Row<'a, T>>
where
Q: FnMut(&str) -> Option<T> + 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 <degree>). 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(),
},
));
}
}

4
executor/src/witgen/processor.rs
View File

@@ -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<Row<'a, T>> {
self.data
}
}
impl<'a, 'b, T: FieldElement> Processor<'a, 'b, '_, T, WithCalldata> {

33
executor/src/witgen/rows.rs
View File

@@ -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<T> {
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."),
}
}

3
executor/src/witgen/sequence_iterator.rs
View File

@@ -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<i64>) -> 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<SequenceStep> {
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;
}

8
executor/src/witgen/symbolic_witness_evaluator.rs
View File

@@ -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())
}
}

112
executor/src/witgen/vm_processor.rs
View File

@@ -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<Expression<T>>, bool)>,
@@ -54,6 +47,7 @@ pub struct VmProcessor<'a, T: FieldElement> {
data: Vec<Row<'a, T>>,
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<Expression<T>>],
witnesses: HashSet<PolyID>,
data: Vec<Row<'a, T>>,
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<Q>(&mut self, mutable_state: &mut MutableState<'a, T, Q>)
where
Q: FnMut(&str) -> Option<T> + 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<Q>(
&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<Q>(&mut self, row_index: DegreeType, mutable_state: &mut MutableState<'a, T, Q>)
where
Q: FnMut(&str) -> Option<T> + 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,