From c2f5ce27460d1855be7e7b34c6fb6308304d3c08 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Mon, 14 Aug 2023 09:36:16 +0000 Subject: [PATCH] Refactor Main Machine Witness Generation #470 --- ast/src/analyzed/mod.rs | 15 + executor/src/witgen/column_map.rs | 22 - executor/src/witgen/eval_result.rs | 2 - executor/src/witgen/generator.rs | 900 +++++++----------- executor/src/witgen/identity_processor.rs | 133 +++ executor/src/witgen/machines/block_machine.rs | 2 +- executor/src/witgen/mod.rs | 31 +- executor/src/witgen/query_processor.rs | 94 ++ executor/src/witgen/rows.rs | 339 +++++++ .../src/witgen/symbolic_witness_evaluator.rs | 4 +- halo2/src/mock_prover.rs | 2 +- 11 files changed, 944 insertions(+), 600 deletions(-) create mode 100644 executor/src/witgen/identity_processor.rs create mode 100644 executor/src/witgen/query_processor.rs create mode 100644 executor/src/witgen/rows.rs diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index 30a349f33..c7565505e 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -310,6 +310,10 @@ impl Identity { assert_eq!(self.kind, IdentityKind::Polynomial); self.left.selector.as_ref().unwrap() } + + pub fn contains_next_ref(&self) -> bool { + self.left.contains_next_ref() || self.right.contains_next_ref() + } } #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash)] @@ -326,6 +330,17 @@ pub struct SelectedExpressions { pub expressions: Vec>, } +impl SelectedExpressions { + /// @returns true if the expression contains a reference to a next value of a + /// (witness or fixed) column + pub fn contains_next_ref(&self) -> bool { + self.selector + .iter() + .chain(self.expressions.iter()) + .any(|e| e.contains_next_ref()) + } +} + #[derive(Debug, PartialEq, Eq, Clone)] pub enum Expression { Constant(String), diff --git a/executor/src/witgen/column_map.rs b/executor/src/witgen/column_map.rs index c83de7d11..337e7791f 100644 --- a/executor/src/witgen/column_map.rs +++ b/executor/src/witgen/column_map.rs @@ -56,28 +56,6 @@ impl ColumnMap { } } -impl ColumnMap> { - pub fn unwrap_or_default(self) -> ColumnMap { - ColumnMap { - values: self - .values - .into_iter() - .map(|v| v.unwrap_or_default()) - .collect(), - ptype: self.ptype, - } - } -} - -impl ColumnMap { - pub fn wrap_some(self) -> ColumnMap> { - ColumnMap { - values: self.values.into_iter().map(|v| Some(v)).collect(), - ptype: self.ptype, - } - } -} - impl Index<&PolyID> for ColumnMap { type Output = V; diff --git a/executor/src/witgen/eval_result.rs b/executor/src/witgen/eval_result.rs index c893762eb..d06fcb7ae 100644 --- a/executor/src/witgen/eval_result.rs +++ b/executor/src/witgen/eval_result.rs @@ -7,8 +7,6 @@ use super::range_constraints::RangeConstraint; #[derive(Clone, Debug, PartialEq, Eq)] pub enum IncompleteCause { - /// Previous value of witness column not known when trying to derive a value in the next row. Example: `x' = x` where `x` is unknown - PreviousValueUnknown(K), /// Some parts of an expression are not bit constrained. Example: `x + y == 0x3` with `x | 0x1`. Arguments: the indices of the unconstrained variables. BitUnconstrained(Vec), /// Some bit constraints are overlapping. Example: `x + y == 0x3` with `x | 0x3` and `y | 0x3` diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index ec3f95334..fa956a946 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -1,66 +1,72 @@ -use ast::analyzed::{Expression, Identity, IdentityKind, PolyID, PolynomialReference}; +use ast::analyzed::{Identity, PolyID}; use itertools::Itertools; use number::{DegreeType, FieldElement}; use parser_util::lines::indent; -use std::collections::{BTreeSet, HashMap}; +use std::collections::{BTreeMap, BTreeSet, HashMap}; use std::time::Instant; -use super::affine_expression::{AffineExpression, AffineResult}; +use crate::witgen::identity_processor::IdentityProcessor; +use crate::witgen::rows::RowUpdater; + use super::column_map::ColumnMap; -use super::global_constraints::RangeConstraintSet; +use super::query_processor::QueryProcessor; use super::range_constraints::RangeConstraint; -use super::expression_evaluator::ExpressionEvaluator; use super::machines::{FixedLookup, Machine}; -use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator}; -use super::{ - Constraint, EvalError, EvalResult, EvalValue, FixedData, IncompleteCause, WitnessColumn, -}; +use super::rows::{Row, RowFactory, RowPair}; +use super::{EvalError, EvalResult, FixedData}; + +/// Phase in which [Generator::compute_next_row_or_initialize] 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)>, +} + +impl<'a, T: FieldElement> CompletableIdentities<'a, T> { + fn new(identities: impl Iterator>) -> Self { + Self { + identities_with_complete: identities.map(|identity| (identity, false)).collect(), + } + } + + /// Yields immutable references to the identity and mutable references to the complete flag. + fn iter_mut(&mut self) -> impl Iterator, &mut bool)> { + self.identities_with_complete + .iter_mut() + .map(|(identity, complete)| (*identity, complete)) + } +} pub struct Generator<'a, T: FieldElement, QueryCallback: Send + Sync> { - fixed_data: &'a FixedData<'a, T>, - fixed_lookup: &'a mut FixedLookup, - identities: &'a [&'a Identity], + /// The witness columns belonging to this machine witnesses: BTreeSet, - machines: Vec>>, - query_callback: Option, - global_range_constraints: ColumnMap>>, + row_factory: RowFactory<'a, T>, + identity_processor: IdentityProcessor<'a, T>, + query_processor: Option>, + fixed_data: &'a FixedData<'a, T>, + /// The subset of identities that contains a reference to the next row + /// (precomputed once for performance reasons) + identities_with_next_ref: Vec<&'a Identity>, + /// The subset of identities that does not contain a reference to the next row + /// (precomputed once for performance reasons) + identities_without_next_ref: Vec<&'a Identity>, + /// Values of the witness polynomials in the previous row (needed to check proposed rows) + previous: Row, /// Values of the witness polynomials - current: ColumnMap>, + current: Row, /// Values of the witness polynomials in the next row - next: ColumnMap>, - /// Range constraints on the witness polynomials in the next row. - next_range_constraints: ColumnMap>>, - next_row: DegreeType, - failure_reasons: Vec>, + next: Row, + current_row_index: DegreeType, last_report: DegreeType, last_report_time: Instant, } -#[derive(PartialEq, Eq, Clone, Copy)] -enum EvaluationRow { - /// p is p[next_row - 1], p' is p[next_row] - Current, - /// p is p[next_row], p' is p[next_row + 1] - Next, -} - -#[derive(PartialEq, Eq, Clone, Copy, Debug)] -enum SolvingStrategy { - /// Only solve expressions that are affine in a single variable - /// (and use range constraints). - SingleVariableAffine, - /// Assume that all unknown values are zero and check that this does not generate - /// a conflict (but do not store the values as fixed zero to avoid relying on nondeterminism). - AssumeZero, -} - -#[derive(PartialEq, Eq, Clone, Copy)] -enum EvaluateUnknown { - Symbolic, - AssumeZero, -} - impl<'a, T: FieldElement, QueryCallback> Generator<'a, T, QueryCallback> where QueryCallback: FnMut(&str) -> Option + Send + Sync, @@ -74,149 +80,236 @@ where machines: Vec>>, query_callback: Option, ) -> Self { - Generator { - fixed_data, - fixed_lookup, - identities, + let query_processor = + query_callback.map(|query_callback| QueryProcessor::new(fixed_data, query_callback)); + let identity_processor = IdentityProcessor::new(fixed_data, fixed_lookup, machines); + let row_factory = RowFactory::new(fixed_data, global_range_constraints); + let default_row = row_factory.fresh_row(); + + let (identities_with_next, identities_without_next): (Vec<_>, Vec<_>) = identities + .iter() + .partition(|identity| identity.contains_next_ref()); + + let mut generator = Generator { + row_factory, witnesses, - machines, - query_callback, - global_range_constraints, - current: fixed_data.witness_map_with(None), - next: fixed_data.witness_map_with(None), - next_range_constraints: fixed_data.witness_map_with(None), - next_row: 0, - failure_reasons: vec![], + query_processor, + identity_processor, + fixed_data, + identities_with_next_ref: identities_with_next, + identities_without_next_ref: identities_without_next, + previous: default_row.clone(), + current: default_row.clone(), + next: default_row, + current_row_index: fixed_data.degree - 1, last_report: 0, last_report_time: Instant::now(), - } + }; + // For identities like `pc' = (1 - first_step') * <...>`, we need to process the last + // row before processing the first row. + generator + .compute_next_row_or_initialize(generator.last_row(), ProcessingPhase::Initialization); + generator + } + + fn last_row(&self) -> DegreeType { + self.fixed_data.degree - 1 } pub fn compute_next_row(&mut self, next_row: DegreeType) -> ColumnMap { - self.set_next_row_and_log(next_row); + self.compute_next_row_or_initialize(next_row, ProcessingPhase::Regular) + } - let mut complete_identities = vec![false; self.identities.len()]; - - log::trace!("Row: {}", next_row); - - let mut identity_failed = false; - for strategy in [ - SolvingStrategy::SingleVariableAffine, - SolvingStrategy::AssumeZero, - ] { - if identity_failed { - break; - } - log::trace!(" Strategy: {:?}", strategy); - loop { - identity_failed = false; - let mut progress = false; - self.failure_reasons.clear(); - - for (identity, complete) in self - .identities - .iter() - .zip(complete_identities.iter_mut()) - .filter(|(_, complete)| !**complete) - { - let result = self.process_identity(identity, strategy).map_err(|err| { - let msg = match strategy { - SolvingStrategy::SingleVariableAffine => "Solving failed on", - SolvingStrategy::AssumeZero => { - "Assuming zero for unknown columns failed in" - } - }; - format!("{msg} {identity}:\n{}", indent(&format!("{err}"), " ")).into() - }); - - match &result { - Ok(e) => { - *complete = e.is_complete(); - } - Err(_) => { - identity_failed = true; - } - }; - - progress |= - self.handle_eval_result(result, strategy, || format!("{}", identity)); - } - - if self.query_callback.is_some() - && strategy == SolvingStrategy::SingleVariableAffine - { - for (poly_id, column) in self.fixed_data.witness_cols.iter() { - if !self.has_known_next_value(&poly_id) && column.query.is_some() { - let result = self.process_witness_query(&column); - progress |= - self.handle_eval_result(result, strategy, || "".into()); - } - } - } - - if !progress || identity_failed { - break; - } - } + fn compute_next_row_or_initialize( + &mut self, + next_row: DegreeType, + phase: ProcessingPhase, + ) -> ColumnMap { + if phase == ProcessingPhase::Initialization { + assert_eq!(next_row, self.last_row()); + self.current_row_index = next_row; + } else { + self.set_next_row_and_log(next_row); } - if identity_failed { - let list_undetermined = |values: &ColumnMap>| { - values - .iter() - .filter_map(|(p, v)| { - if v.is_none() && self.is_relevant_witness(&p) { - Some(self.fixed_data.column_name(&p).to_string()) - } else { - None - } - }) - .collect::>() - .join(", ") - }; - log::error!( - "\nError: Row {next_row}: Identity check failed or unable to derive values for some witness columns.\nSet RUST_LOG=debug for more information."); - log::debug!( - "\nThe following columns were undetermined in the previous row and might have been needed to derive this row's values:\n{}", - list_undetermined(&self.current) + log::trace!("Row: {}", self.current_row_index); + + log::trace!(" Going over all identities until no more progress is made"); + // First, go over identities that don't reference the next row, + // Second, propagate values to the next row by going over identities that do reference the next row. + let mut identities_without_next_ref = + CompletableIdentities::new(self.identities_without_next_ref.iter().cloned()); + let mut identities_with_next_ref = + CompletableIdentities::new(self.identities_with_next_ref.iter().cloned()); + self.loop_until_no_progress(&mut identities_without_next_ref) + .and_then(|_| self.loop_until_no_progress(&mut identities_with_next_ref)) + .map_err(|e| self.report_failure_and_panic_unsatisfiable(e)) + .unwrap(); + + // 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::debug!( - "\nThe following columns are still undetermined in the current row:\n{}", - list_undetermined(&self.next) - ); - log::debug!( - "\nReasons:\n{}\n", - self.failure_reasons - .iter() - .map(|r| r.to_string()) - .join("\n\n") - ); - log::debug!( - "Determined range constraints for this row:\n{}", - self.next_range_constraints - .iter() - .filter_map(|(id, cons)| { - cons.as_ref() - .map(|cons| format!(" {}: {cons}", self.fixed_data.column_name(&id))) - }) - .join("\n") - ); - log::debug!( - "Current values (known nonzero first, then zero, unknown omitted):\n{}", - indent(&self.format_next_known_values().join("\n"), " ") - ); - panic!("Witness generation failed."); + self.process_identities(&mut identities_without_next_ref, true) + .and_then(|_| self.process_identities(&mut identities_with_next_ref, true)) + .map_err(|e| self.report_failure_and_panic_underconstrained(e)) + .unwrap(); } log::trace!( - "===== Row {next_row}:\n{}", - indent(&self.format_next_values().join("\n"), " ") + "{}", + self.current + .render(&format!("===== Row {}", self.current_row_index), true) ); - std::mem::swap(&mut self.next, &mut self.current); - self.next = self.fixed_data.witness_map_with(None); - self.next_range_constraints = self.fixed_data.witness_map_with(None); - self.current.clone().unwrap_or_default() + self.shift_rows(); + + self.previous.clone().into() + } + + /// Loops over all identities and queries, until no further progress is made. + /// @returns the "incomplete" identities, i.e. identities that contain unknown values. + fn loop_until_no_progress( + &mut self, + identities: &mut CompletableIdentities<'a, T>, + ) -> Result<(), Vec>> { + loop { + let mut progress = self.process_identities(identities, false)?; + if let Some(ref mut query_processor) = self.query_processor { + let row_pair = RowPair::new( + &self.current, + &self.next, + self.current_row_index, + self.fixed_data, + false, + ); + let updates = query_processor.process_queries_on_current_row(&row_pair); + let mut row_updater = + RowUpdater::new(&mut self.current, &mut self.next, self.current_row_index); + progress |= row_updater.apply_updates(&updates, || "query".to_string()); + } + + if !progress { + break; + } + } + Ok(()) + } + + /// Loops over all identities once and updates the current row and next row. + /// Arguments: + /// * `identities`: Identities to process. Completed identities are removed from the list. + /// * `frozen`: If true, the identities are processed assuming that all unknown values are 0. + /// Also, no updates are applied to the current row. + /// Returns: + /// * `Ok(true)`: If progress was made. + /// * `Ok(false)`: If no progress was made. + /// * `Err(errors)`: If an error occurred. + fn process_identities( + &mut self, + identities: &mut CompletableIdentities<'a, T>, + frozen: bool, + ) -> Result>> { + let mut progress = false; + let mut errors = vec![]; + + for (identity, is_complete) in identities.iter_mut() { + if *is_complete { + continue; + } + + let row_pair = RowPair::new( + &self.current, + &self.next, + self.current_row_index, + self.fixed_data, + frozen, + ); + let result: EvalResult<'a, T> = self + .identity_processor + .process_identity(identity, &row_pair) + .map_err(|err| { + format!("{identity}:\n{}", indent(&format!("{err}"), " ")).into() + }); + + match result { + Ok(eval_value) => { + if frozen { + assert!(eval_value.constraints.is_empty()) + } else { + *is_complete = eval_value.is_complete(); + let mut row_updater = RowUpdater::new( + &mut self.current, + &mut self.next, + self.current_row_index, + ); + progress |= + row_updater.apply_updates(&eval_value, || format!("{identity}")); + } + } + Err(e) => { + errors.push(e); + } + }; + } + + if errors.is_empty() { + Ok(progress) + } else { + Err(errors) + } + } + + /// Shifts rows: fresh row -> next -> current -> previous + fn shift_rows(&mut self) { + let mut fresh_row = self.row_factory.fresh_row(); + std::mem::swap(&mut self.previous, &mut fresh_row); + std::mem::swap(&mut self.current, &mut self.previous); + std::mem::swap(&mut self.next, &mut self.current); + } + + fn report_failure_and_panic_unsatisfiable(&self, failures: Vec>) -> ! { + log::error!( + "\nError: Row {} failed. Set RUST_LOG=debug for more information.\n", + self.current_row_index + ); + log::debug!("Some identities where not satisfiable after the following values were uniquely determined (known nonzero first, then zero, unknown omitted):"); + log::debug!("{}", self.current.render("Current Row", false)); + log::debug!("{}", self.next.render("Next Row", false)); + log::debug!("Set RUST_LOG=trace to understand why these values were chosen."); + log::debug!( + "Assuming these values are correct, the following identities fail:\n{}\n", + failures + .iter() + .map(|r| indent(&r.to_string(), " ")) + .join("\n") + ); + panic!("Witness generation failed."); + } + + fn report_failure_and_panic_underconstrained(&self, failures: Vec>) -> ! { + log::error!( + "\nError: Row {} failed. Set RUST_LOG=debug for more information.\n", + self.current_row_index + ); + + log::debug!("Some columns could not be determined, but setting them to zero does not satisfy the constraints. This typically means that the system is underconstrained!"); + log::debug!("{}", self.current.render("Current Row", true)); + log::debug!("{}", self.next.render("Next Row", true)); + log::debug!("\nSet RUST_LOG=trace to understand why these values were (not) chosen."); + log::debug!( + "Assuming zero for unknown values, the following identities fail:\n{}\n", + failures + .iter() + .map(|r| indent(&r.to_string(), " ")) + .join("\n") + ); + panic!("Witness generation failed."); } /// Verifies the proposed values for the next row. @@ -224,28 +317,84 @@ where /// not used. pub fn propose_next_row(&mut self, next_row: DegreeType, values: &ColumnMap) -> bool { self.set_next_row_and_log(next_row); - self.next = values.clone().wrap_some(); - for identity in self.identities { + let proposed_row = self.row_factory.row_from_known_values(values); + + let constraints_valid = + self.check_row_pair(&proposed_row, false) && self.check_row_pair(&proposed_row, true); + + if constraints_valid { + self.previous = proposed_row; + } else { + // Note that we never update `current` 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. + std::mem::swap(&mut self.current, &mut self.previous); + self.next = self.row_factory.fresh_row(); + self.compute_next_row(next_row - 1); + } + constraints_valid + } + + fn check_row_pair(&mut self, proposed_row: &Row, previous: bool) -> bool { + let row_pair = match previous { + // Check whether identities with a reference to the next row are satisfied + // when applied to the previous row and the proposed row. + true => RowPair::new( + &self.previous, + proposed_row, + self.current_row_index - 1, + self.fixed_data, + true, + ), + // 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( + proposed_row, + &self.next, + self.current_row_index, + self.fixed_data, + true, + ), + }; + + // Check identities depending on whether or not they have a reference to the next row: + // - Those that do should be checked on the previous and proposed row + // - All others should be checked on the proposed row + let identities = match previous { + true => &self.identities_with_next_ref, + false => &self.identities_without_next_ref, + }; + + for identity in identities.iter() { if self - .process_identity(identity, SolvingStrategy::AssumeZero) + .identity_processor + .process_identity(identity, &row_pair) .is_err() { - self.next = self.fixed_data.witness_map_with(None); - self.next_range_constraints = self.fixed_data.witness_map_with(None); + log::debug!("Previous {:?}", self.previous); + log::debug!("Proposed {:?}", proposed_row); + log::debug!("Failed on identity: {}", identity); + return false; } } - std::mem::swap(&mut self.next, &mut self.current); - self.next = self.fixed_data.witness_map_with(None); - self.next_range_constraints = self.fixed_data.witness_map_with(None); true } - pub fn machine_witness_col_values(&mut self) -> HashMap> { + pub fn machine_witness_col_values(&mut self) -> HashMap> { let mut result: HashMap<_, _> = Default::default(); - for m in &mut self.machines { - result.extend(m.witness_col_values(self.fixed_data)); + let name_to_id = self + .fixed_data + .witness_column_names + .iter() + .map(|(poly_id, &name)| (name, poly_id)) + .collect::>(); + for m in &mut self.identity_processor.machines { + for (col_name, col) in m.witness_col_values(self.fixed_data) { + result.insert(*name_to_id.get(col_name.as_str()).unwrap(), col); + } } result } @@ -263,392 +412,11 @@ where ); self.last_report = next_row; } - self.next_row = next_row; - } - - fn format_next_values(&self) -> Vec { - self.format_next_values_iter( - self.next - .iter() - .filter(|(i, _)| self.is_relevant_witness(i)), - ) - } - - fn format_next_known_values(&self) -> Vec { - self.format_next_values_iter(self.next.iter().filter(|(_, v)| v.is_some())) - } - - fn format_next_values_iter<'b>( - &self, - values: impl IntoIterator)>, - ) -> Vec { - let mut values = values.into_iter().collect::>(); - values.sort_by_key(|(i, v1)| { - ( - match v1 { - Some(v) if v.is_zero() => 1, - Some(_) => 0, - None => 2, - }, - *i, - ) - }); - values - .into_iter() - .map(|(i, v)| { - format!( - "{} = {}", - self.fixed_data.column_name(&i), - v.as_ref() - .map(ToString::to_string) - .unwrap_or_else(|| "".to_string()) - ) - }) - .collect() - } - - fn process_witness_query(&mut self, column: &&'a WitnessColumn) -> EvalResult<'a, T> { - let query = column.query.as_ref().unwrap(); - let query_string = match self.interpolate_query(query.expr) { - Ok(query) => query, - Err(incomplete) => return Ok(EvalValue::incomplete(incomplete)), - }; - if let Some(value) = self - .query_callback - .as_mut() - .and_then(|c| (c)(&query_string)) - { - Ok(EvalValue::complete(vec![( - &query.poly, - Constraint::Assignment(value), - )])) - } else { - Ok(EvalValue::incomplete(IncompleteCause::NoQueryAnswer( - query_string, - column.name.to_string(), - ))) - } - } - - fn interpolate_query<'b>( - &self, - query: &'b Expression, - ) -> Result> { - // TODO combine that with the constant evaluator and the commit evaluator... - match query { - Expression::Tuple(items) => Ok(items - .iter() - .map(|i| self.interpolate_query(i)) - .collect::, _>>()? - .join(", ")), - Expression::LocalVariableReference(i) => { - assert!(*i == 0); - Ok(format!("{}", self.next_row)) - } - Expression::String(s) => Ok(format!( - "\"{}\"", - s.replace('\\', "\\\\").replace('"', "\\\"") - )), - Expression::MatchExpression(scrutinee, arms) => { - self.interpolate_match_expression_for_query(scrutinee.as_ref(), arms) - } - _ => self - .evaluate(query, EvaluationRow::Next, EvaluateUnknown::Symbolic)? - .constant_value() - .map(|c| c.to_string()) - .ok_or(IncompleteCause::NonConstantQueryElement), - } - } - - fn interpolate_match_expression_for_query<'b>( - &self, - scrutinee: &'b Expression, - arms: &'b [(Option, Expression)], - ) -> Result> { - let v = self - .evaluate(scrutinee, EvaluationRow::Next, EvaluateUnknown::Symbolic)? - .constant_value() - .ok_or(IncompleteCause::NonConstantQueryMatchScrutinee)?; - let (_, expr) = arms - .iter() - .find(|(n, _)| n.is_none() || n.as_ref() == Some(&v)) - .ok_or(IncompleteCause::NoMatchArmFound)?; - self.interpolate_query(expr) - } - - fn process_identity<'b>( - &mut self, - identity: &'b Identity, - strategy: SolvingStrategy, - ) -> EvalResult<'b, T> { - match identity.kind { - IdentityKind::Polynomial => { - self.process_polynomial_identity(identity.expression_for_poly_id(), strategy) - } - IdentityKind::Plookup | IdentityKind::Permutation => { - self.process_plookup(identity, strategy) - } - kind => { - unimplemented!("Identity of kind {kind:?} is not supported in the executor") - } - } - } - - fn process_polynomial_identity<'b>( - &self, - identity: &'b Expression, - strategy: SolvingStrategy, - ) -> EvalResult<'b, T> { - // If there is no "next" reference in the expression, - // we just evaluate it directly on the "next" row. - let row = if identity.contains_next_witness_ref() { - // TODO this is the only situation where we use "current" - // TODO this is the only that actually uses a window. - EvaluationRow::Current - } else { - EvaluationRow::Next - }; - let evaluate_unknown = if strategy == SolvingStrategy::AssumeZero { - EvaluateUnknown::AssumeZero - } else { - EvaluateUnknown::Symbolic - }; - let evaluated = match self.evaluate(identity, row, evaluate_unknown) { - Ok(evaluated) => evaluated, - Err(cause) => { - return Ok(EvalValue::incomplete(cause)); - } - }; - if evaluated.constant_value() == Some(0.into()) { - Ok(EvalValue::complete(vec![])) - } else { - evaluated.solve_with_range_constraints(&self.range_constraint_set()) - } - } - - fn process_plookup<'b>( - &mut self, - identity: &'b Identity, - strategy: SolvingStrategy, - ) -> EvalResult<'b, T> { - let evaluate_unknown = if strategy == SolvingStrategy::AssumeZero { - EvaluateUnknown::AssumeZero - } else { - EvaluateUnknown::Symbolic - }; - if let Some(left_selector) = &identity.left.selector { - let value = match self.evaluate(left_selector, EvaluationRow::Next, evaluate_unknown) { - Ok(value) => value, - Err(cause) => return Ok(EvalValue::incomplete(cause)), - }; - match value.constant_value() { - Some(v) if v.is_zero() => { - return Ok(EvalValue::complete(vec![])); - } - Some(v) if v.is_one() => {} - _ => { - return Ok(EvalValue::incomplete( - IncompleteCause::NonConstantLeftSelector, - )) - } - }; - } - - let left = identity - .left - .expressions - .iter() - .map(|e| self.evaluate(e, EvaluationRow::Next, evaluate_unknown)) - .collect::>(); - - // Now query the machines. - // Note that we should always query all machines that match, because they might - // update their internal data, even if all values are already known. - // TODO could it be that multiple machines match? - - // query the fixed lookup "machine" - if let Some(result) = self.fixed_lookup.process_plookup( - self.fixed_data, - identity.kind, - &left, - &identity.right, - ) { - return result; - } - - for m in &mut self.machines { - // TODO also consider the reasons above. - if let Some(result) = m.process_plookup( - self.fixed_data, - self.fixed_lookup, - identity.kind, - &left, - &identity.right, - ) { - return result; - } - } - - unimplemented!("No executor machine matched identity `{identity}`") - } - - /// Processes the evaluation result: Stores failure reasons and updates next values. - /// Returns true if a new value or constraint was determined. - fn handle_eval_result( - &mut self, - result: EvalResult, - strategy: SolvingStrategy, - source_name: impl Fn() -> String, - ) -> bool { - let mut first = true; - match result { - Ok(constraints) => { - let progress = !constraints.is_empty(); - // If we assume unknown variables to be zero, we cannot learn anything new. - if strategy == SolvingStrategy::AssumeZero { - assert!(!progress); - } - for (id, c) in constraints.constraints { - if first { - log::trace!(" Processing: {}", source_name()); - first = false; - } - match c { - Constraint::Assignment(value) => { - log::trace!(" => {id} = {value}"); - self.next[&id.poly_id()] = Some(value); - } - Constraint::RangeConstraint(cons) => { - log::trace!(" => Adding range constraint for {id}: {cons}"); - let old = &mut self.next_range_constraints[&id.poly_id()]; - let new = match old { - Some(c) => Some(cons.conjunction(c)), - None => Some(cons), - }; - log::trace!(" (the conjunction is {})", new.as_ref().unwrap()); - *old = new; - } - } - } - progress - } - Err(reason) => { - self.failure_reasons.push(reason); - false - } - } - } - - fn has_known_next_value(&self, id: &PolyID) -> bool { - self.next[id].is_some() + self.current_row_index = next_row; } /// Returns true if this is a witness column we care about (instead of a sub-machine witness). pub fn is_relevant_witness(&self, id: &PolyID) -> bool { self.witnesses.contains(id) } - - /// Tries to evaluate the expression to an expression affine in the witness polynomials, - /// taking current values of polynomials into account. - /// @returns an expression affine in the witness polynomials - fn evaluate<'b>( - &self, - expr: &'b Expression, - evaluate_row: EvaluationRow, - evaluate_unknown: EvaluateUnknown, - ) -> AffineResult<&'b PolynomialReference, T> { - let degree = self.fixed_data.degree; - - // We want to determine the values of next_row, but if the expression contains - // references to the next row, we want to evaluate the expression for the current row - // in order to determine values for next_row. - // Otherwise, we want to evaluate the expression on next_row directly. - let fixed_row = match evaluate_row { - EvaluationRow::Current => (self.next_row + degree - 1) % degree, - EvaluationRow::Next => self.next_row, - }; - - ExpressionEvaluator::new(SymoblicWitnessEvaluator::new( - self.fixed_data, - fixed_row, - EvaluationData { - current_witnesses: &self.current, - next_witnesses: &self.next, - evaluate_row, - evaluate_unknown, - }, - )) - .evaluate(expr) - } - - fn range_constraint_set(&'a self) -> WitnessRangeConstraintSet<'a, T> { - WitnessRangeConstraintSet { - global_range_constraints: &self.global_range_constraints, - next_range_constraints: &self.next_range_constraints, - } - } -} - -struct WitnessRangeConstraintSet<'a, T: FieldElement> { - /// Global constraints on witness and fixed polynomials. - global_range_constraints: &'a ColumnMap>>, - /// Range constraints on the witness polynomials in the next row. - next_range_constraints: &'a ColumnMap>>, -} - -impl<'a, T: FieldElement> RangeConstraintSet<&PolynomialReference, T> - for WitnessRangeConstraintSet<'a, T> -{ - fn range_constraint(&self, poly: &PolynomialReference) -> Option> { - // Combine potential global range constraints with local range constraints. - let global = self.global_range_constraints[&poly.poly_id()].as_ref(); - let local = self.next_range_constraints[&poly.poly_id()].as_ref(); - - match (global, local) { - (None, None) => None, - (None, Some(con)) | (Some(con), None) => Some(con.clone()), - (Some(g), Some(l)) => Some(g.conjunction(l)), - } - } -} - -struct EvaluationData<'a, T> { - /// Values of the witness polynomials in the current / last row - pub current_witnesses: &'a ColumnMap>, - /// Values of the witness polynomials in the next row - pub next_witnesses: &'a ColumnMap>, - pub evaluate_row: EvaluationRow, - pub evaluate_unknown: EvaluateUnknown, -} - -impl<'a, T: FieldElement> WitnessColumnEvaluator for EvaluationData<'a, T> { - fn value<'b>(&self, poly: &'b PolynomialReference) -> AffineResult<&'b PolynomialReference, T> { - let id = poly.poly_id(); - match (poly.next, self.evaluate_row) { - (false, EvaluationRow::Current) => { - // All values in the "current" row should usually be known. - // The exception is when we start the analysis on the first row. - self.current_witnesses[&id] - .as_ref() - .map(|value| (*value).into()) - .ok_or(IncompleteCause::PreviousValueUnknown(poly)) - } - (false, EvaluationRow::Next) | (true, EvaluationRow::Current) => { - Ok(if let Some(value) = &self.next_witnesses[&id] { - // We already computed the concrete value - (*value).into() - } else if self.evaluate_unknown == EvaluateUnknown::AssumeZero { - T::from(0).into() - } else { - // We continue with a symbolic value - AffineExpression::from_variable_id(poly) - }) - } - (true, EvaluationRow::Next) => { - unimplemented!( - "{poly} references the next-next row when evaluating on the current row." - ); - } - } - } } diff --git a/executor/src/witgen/identity_processor.rs b/executor/src/witgen/identity_processor.rs new file mode 100644 index 000000000..29b5ac0dc --- /dev/null +++ b/executor/src/witgen/identity_processor.rs @@ -0,0 +1,133 @@ +use ast::analyzed::{Expression, Identity, IdentityKind, PolynomialReference}; +use number::FieldElement; + +use super::{ + machines::{FixedLookup, Machine}, + rows::RowPair, + EvalResult, EvalValue, FixedData, IncompleteCause, +}; + +/// Computes (value or range constraint) updates given a [RowPair] and [Identity]. +pub struct IdentityProcessor<'a, T: FieldElement> { + fixed_data: &'a FixedData<'a, T>, + fixed_lookup: &'a mut FixedLookup, + pub machines: Vec>>, +} + +impl<'a, T: FieldElement> IdentityProcessor<'a, T> { + pub fn new( + fixed_data: &'a FixedData<'a, T>, + fixed_lookup: &'a mut FixedLookup, + machines: Vec>>, + ) -> Self { + Self { + fixed_data, + fixed_lookup, + machines, + } + } + + /// Given an identity and a row pair, tries to figure out additional values / range constraints + /// for the given cells. + /// Fails if any constraint was not satisfiable. + /// Returns the updates. + pub fn process_identity<'b>( + &mut self, + identity: &'b Identity, + rows: &RowPair, + ) -> EvalResult<'b, T> { + match identity.kind { + IdentityKind::Polynomial => self.process_polynomial_identity(identity, rows), + IdentityKind::Plookup | IdentityKind::Permutation => { + self.process_plookup(identity, rows) + } + kind => { + unimplemented!( + "Identity of kind {kind:?} is not supported by the identity processor." + ) + } + } + } + + fn process_polynomial_identity<'b>( + &self, + identity: &'b Identity, + rows: &RowPair, + ) -> EvalResult<'b, T> { + let expression = identity.expression_for_poly_id(); + let evaluated = match rows.evaluate(expression) { + Err(inclomplete_cause) => return Ok(EvalValue::incomplete(inclomplete_cause)), + Ok(evaluated) => evaluated, + }; + + evaluated.solve_with_range_constraints(rows) + } + + fn process_plookup<'b>( + &mut self, + identity: &'b Identity, + rows: &RowPair, + ) -> EvalResult<'b, T> { + if let Some(left_selector) = &identity.left.selector { + if let Some(status) = self.handle_left_selector(left_selector, rows) { + return Ok(status); + } + } + + let left = identity + .left + .expressions + .iter() + .map(|e| rows.evaluate(e)) + .collect::>(); + + // Now query the machines. + // Note that we should always query all machines that match, because they might + // update their internal data, even if all values are already known. + // TODO could it be that multiple machines match? + + // query the fixed lookup "machine" + if let Some(result) = self.fixed_lookup.process_plookup( + self.fixed_data, + identity.kind, + &left, + &identity.right, + ) { + return result; + } + + for m in &mut self.machines { + // TODO also consider the reasons above. + if let Some(result) = m.process_plookup( + self.fixed_data, + self.fixed_lookup, + identity.kind, + &left, + &identity.right, + ) { + return result; + } + } + + unimplemented!("No executor machine matched identity `{identity}`") + } + + /// Returns updates of the left selector cannot be evaluated to 1, otherwise None. + fn handle_left_selector<'b>( + &mut self, + left_selector: &'b Expression, + rows: &RowPair, + ) -> Option> { + let value = match rows.evaluate(left_selector) { + Err(inclomplete_cause) => return Some(EvalValue::incomplete(inclomplete_cause)), + Ok(value) => value, + }; + match value.constant_value() { + Some(v) if v.is_zero() => Some(EvalValue::complete(vec![])), + Some(v) if v.is_one() => None, + _ => Some(EvalValue::incomplete( + IncompleteCause::NonConstantLeftSelector, + )), + } + } +} diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 1a11a5486..3fac52c6a 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -596,7 +596,7 @@ impl BlockMachine { ExpressionEvaluator::new(SymoblicWitnessEvaluator::new( fixed_data, self.row, - WitnessData { + &WitnessData { fixed_data, data: &self.data, row: self.row, diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index f22fd5d2c..418e64dad 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -21,12 +21,24 @@ mod expression_evaluator; pub mod fixed_evaluator; mod generator; mod global_constraints; +mod identity_processor; mod machines; +mod query_processor; mod range_constraints; +mod rows; pub mod symbolic_evaluator; mod symbolic_witness_evaluator; mod util; +// TODO: This is done once for the witness column names, so that they can be referenced +// by the `Cell`. The reason is that we want machines (e.g. `BlockMachine`) to own +// their rows, but because they live in a `Box`, they can't have a non-static lifetime +// parameter. #488 prototypes solving this, so this can be removed in the future. +/// Leaks a string and returns a reference with static lifetime. +fn leak_string(s: String) -> &'static str { + Box::leak(s.into_boxed_str()) +} + /// Generates the committed polynomial values /// @returns the values (in source order) and the degree of the polynomials. pub fn generate<'a, T: FieldElement, QueryCallback>( @@ -139,11 +151,7 @@ where } // Overwrite all machine witness columns - for (name, data) in generator.machine_witness_col_values() { - let poly_id = *poly_ids - .iter() - .find(|&p| fixed.column_name(p) == name) - .unwrap(); + for (poly_id, data) in generator.machine_witness_col_values() { columns[&poly_id] = data; } @@ -197,20 +205,31 @@ fn rows_are_repeating( /// Data that is fixed for witness generation. pub struct FixedData<'a, T> { degree: DegreeType, + witness_column_names: ColumnMap<&'static str>, fixed_cols: ColumnMap>, witness_cols: ColumnMap>, } -impl<'a, T> FixedData<'a, T> { +impl<'a, T: FieldElement> FixedData<'a, T> { pub fn new( degree: DegreeType, fixed_cols: ColumnMap>, witness_cols: ColumnMap>, ) -> Self { + // Leak the column names once, so that they can be referenced without + // having to worry about lifetimes. + let witness_column_names = ColumnMap::from( + witness_cols + .values() + .map(|witness_col| leak_string(witness_col.name.clone())), + PolynomialType::Committed, + ); + FixedData { degree, fixed_cols, witness_cols, + witness_column_names, } } diff --git a/executor/src/witgen/query_processor.rs b/executor/src/witgen/query_processor.rs new file mode 100644 index 000000000..467c58fb5 --- /dev/null +++ b/executor/src/witgen/query_processor.rs @@ -0,0 +1,94 @@ +use ast::analyzed::{Expression, PolynomialReference}; +use number::FieldElement; + +use super::{rows::RowPair, Constraint, EvalValue, FixedData, IncompleteCause, Query}; + +/// Computes value updates that result from a query. +pub struct QueryProcessor<'a, T: FieldElement, QueryCallback: Send + Sync> { + fixed_data: &'a FixedData<'a, T>, + query_callback: QueryCallback, +} + +impl<'a, T: FieldElement, QueryCallback> QueryProcessor<'a, T, QueryCallback> +where + QueryCallback: FnMut(&str) -> Option + Send + Sync, +{ + pub fn new(fixed_data: &'a FixedData<'a, T>, query_callback: QueryCallback) -> Self { + Self { + fixed_data, + query_callback, + } + } + + pub fn process_queries_on_current_row( + &mut self, + rows: &RowPair, + ) -> EvalValue<&'a PolynomialReference, T> { + let mut eval_value = EvalValue::complete(vec![]); + for column in self.fixed_data.witness_cols.values() { + if let Some(query) = column.query.as_ref() { + if rows.get_value(&query.poly).is_none() { + eval_value.combine(self.process_witness_query(query, rows)); + } + } + } + eval_value + } + + fn process_witness_query( + &mut self, + query: &'a Query<'_, T>, + rows: &RowPair, + ) -> EvalValue<&'a PolynomialReference, T> { + let query_str = match interpolate_query(query.expr, rows) { + Ok(query) => query, + Err(incomplete) => return EvalValue::incomplete(incomplete), + }; + if let Some(value) = (self.query_callback)(&query_str) { + EvalValue::complete(vec![(&query.poly, Constraint::Assignment(value))]) + } else { + EvalValue::incomplete(IncompleteCause::NoQueryAnswer( + query_str, + query.poly.name.to_string(), + )) + } + } +} + +fn interpolate_query<'b, T: FieldElement>( + query: &'b Expression, + rows: &RowPair, +) -> Result> { + // TODO combine that with the constant evaluator and the commit evaluator... + match query { + Expression::Tuple(items) => Ok(items + .iter() + .map(|i| interpolate_query(i, rows)) + .collect::, _>>()? + .join(", ")), + Expression::LocalVariableReference(i) => { + assert!(*i == 0); + Ok(format!("{}", rows.current_row_index)) + } + Expression::String(s) => Ok(format!( + "\"{}\"", + s.replace('\\', "\\\\").replace('"', "\\\"") + )), + Expression::MatchExpression(scrutinee, arms) => { + let v = rows + .evaluate(scrutinee)? + .constant_value() + .ok_or(IncompleteCause::NonConstantQueryMatchScrutinee)?; + let (_, expr) = arms + .iter() + .find(|(n, _)| n.is_none() || n.as_ref() == Some(&v)) + .ok_or(IncompleteCause::NoMatchArmFound)?; + interpolate_query(expr, rows) + } + _ => rows + .evaluate(query)? + .constant_value() + .map(|c| c.to_string()) + .ok_or(IncompleteCause::NonConstantQueryElement), + } +} diff --git a/executor/src/witgen/rows.rs b/executor/src/witgen/rows.rs new file mode 100644 index 000000000..57075d4a0 --- /dev/null +++ b/executor/src/witgen/rows.rs @@ -0,0 +1,339 @@ +use std::fmt::Debug; + +use ast::analyzed::{Expression, PolynomialReference, PolynomialType}; +use itertools::Itertools; +use number::{DegreeType, FieldElement}; + +use crate::witgen::Constraint; + +use super::{ + affine_expression::{AffineExpression, AffineResult}, + column_map::ColumnMap, + expression_evaluator::ExpressionEvaluator, + global_constraints::RangeConstraintSet, + range_constraints::RangeConstraint, + symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator}, + EvalValue, FixedData, +}; + +#[derive(Clone)] +enum CellValue { + Known(T), + RangeConstraint(RangeConstraint), + Unknown, +} + +impl CellValue { + fn is_known(&self) -> bool { + matches!(self, CellValue::Known(_)) + } + + fn unwrap_or_default(&self) -> T { + match self { + CellValue::Known(v) => *v, + _ => Default::default(), + } + } +} + +/// A single cell, holding an optional value and range constraint. +#[derive(Clone)] +pub struct Cell { + /// The column name, for debugging purposes. + pub name: &'static str, + value: CellValue, +} + +impl Debug for Cell { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let debug_str = match &self.value { + CellValue::Known(v) => format!("{} = {}", self.name, v), + CellValue::RangeConstraint(rc) => { + format!("{} = \n (range constraint: {})", self.name, rc) + } + CellValue::Unknown => format!("{} = ", self.name), + }; + f.write_str(&debug_str) + } +} + +/// A row of cells, indexed by polynomial ID. +pub type Row = ColumnMap>; + +impl Debug for Row { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.write_str(&self.render("Row:", true)) + } +} + +impl Row { + /// Builds a string representing the current row + pub fn render(&self, title: &str, include_unknown: bool) -> String { + format!("{}:\n{}", title, self.render_values(include_unknown)) + } + + /// Builds a string listing all values, one by row. Nonzero entries are + /// first, then zero, then unknown (if `include_unknown == true`). + pub fn render_values(&self, include_unknown: bool) -> String { + let mut cells = self + .iter() + .filter(|(_, cell)| cell.value.is_known() || include_unknown) + .collect::>(); + + // Nonzero first, then zero, then unknown + cells.sort_by_key(|(i, cell)| { + ( + match cell.value { + CellValue::Known(v) if v.is_zero() => 1, + CellValue::Known(_) => 0, + _ => 2, + }, + *i, + ) + }); + + cells + .into_iter() + .map(|(_, cell)| format!(" {:?}", cell)) + .join("\n") + } +} + +/// A factory for rows, which knows the global range constraints and has pointers to column names. +pub struct RowFactory<'a, T: FieldElement> { + fixed_data: &'a FixedData<'a, T>, + global_range_constraints: ColumnMap>>, +} + +impl<'a, T: FieldElement> RowFactory<'a, T> { + pub fn new( + fixed_data: &'a FixedData<'a, T>, + global_range_constraints: ColumnMap>>, + ) -> Self { + Self { + fixed_data, + global_range_constraints, + } + } + + pub fn fresh_row(&self) -> Row { + ColumnMap::from( + self.global_range_constraints + .iter() + .map(|(poly_id, range_constraint)| Cell { + name: self.fixed_data.witness_column_names[&poly_id], + value: match range_constraint.as_ref() { + Some(rc) => CellValue::RangeConstraint(rc.clone()), + None => CellValue::Unknown, + }, + }), + PolynomialType::Committed, + ) + } + + pub fn row_from_known_values(&self, values: &ColumnMap) -> Row { + ColumnMap::from( + values.iter().map(|(poly_id, &v)| Cell { + name: self.fixed_data.witness_column_names[&poly_id], + value: CellValue::Known(v), + }), + PolynomialType::Committed, + ) + } +} + +impl From> for ColumnMap { + /// Builds a map from polynomial ID to value. Unknown values are set to zero. + fn from(val: Row) -> Self { + ColumnMap::from( + val.into_iter() + .map(|(_, cell)| cell.value.unwrap_or_default()), + PolynomialType::Committed, + ) + } +} + +/// A pair of mutable row references which knows how to apply updates. +pub struct RowUpdater<'row, T: FieldElement> { + current: &'row mut Row, + next: &'row mut Row, + current_row_index: DegreeType, +} + +impl<'row, T: FieldElement> RowUpdater<'row, T> { + pub fn new( + current: &'row mut Row, + next: &'row mut Row, + current_row_index: DegreeType, + ) -> Self { + Self { + current, + next, + current_row_index, + } + } + + /// Applies the updates to the underlying rows. Returns true if any updates + /// were applied. + /// + /// # Panics + /// Panics if any updates are redundant, as this indicates a bug that would + /// potentially cause infinite loops otherwise. + pub fn apply_updates( + &mut self, + updates: &EvalValue<&PolynomialReference, T>, + source_name: impl Fn() -> String, + ) -> bool { + if updates.constraints.is_empty() { + return false; + } + + log::trace!(" Updates from: {}", source_name()); + for (poly, c) in &updates.constraints { + match c { + Constraint::Assignment(value) => { + self.set_value(poly, *value); + } + Constraint::RangeConstraint(constraint) => { + self.update_range_constraint(poly, constraint); + } + } + } + true + } + + fn get_cell_mut<'b>(&'b mut self, poly: &PolynomialReference) -> &'b mut Cell { + match poly.next { + false => &mut self.current[&poly.poly_id()], + true => &mut self.next[&poly.poly_id()], + } + } + + fn row_number(&self, poly: &PolynomialReference) -> DegreeType { + match poly.next { + false => self.current_row_index, + true => self.current_row_index + 1, + } + } + + fn set_value(&mut self, poly: &PolynomialReference, value: T) { + log::trace!( + " => {} (Row {}) = {}", + poly.name, + self.row_number(poly), + value + ); + let cell = self.get_cell_mut(poly); + // Note that this is a problem even if the value that was set is the same, + // because we would return that progress was made when it wasn't. + assert!(!cell.value.is_known(), "Value was already set"); + cell.value = CellValue::Known(value); + } + + fn update_range_constraint( + &mut self, + poly: &PolynomialReference, + constraint: &RangeConstraint, + ) { + log::trace!( + " => Adding range constraint for {} (Row {}): {}", + poly.name, + self.row_number(poly), + constraint + ); + let cell = self.get_cell_mut(poly); + let new = match &cell.value { + CellValue::RangeConstraint(c) => constraint.conjunction(c), + _ => constraint.clone(), + }; + if let CellValue::RangeConstraint(old) = &cell.value { + assert!(*old != new, "Range constraint was already set"); + } + assert!( + !cell.value.is_known(), + "Range constraint was updated but value is already known" + ); + log::trace!(" (the conjunction is {})", new); + cell.value = CellValue::RangeConstraint(new); + } +} + +/// A pair of row references which knows which value / range constraint +/// to return for a given [PolynomialReference]. +pub struct RowPair<'row, 'a, T: FieldElement> { + pub current: &'row Row, + pub next: &'row Row, + pub current_row_index: DegreeType, + fixed_data: &'a FixedData<'a, T>, + evaluate_unknown_to_zero: bool, +} +impl<'row, 'a, T: FieldElement> RowPair<'row, 'a, T> { + pub fn new( + current: &'row Row, + next: &'row Row, + current_row_index: DegreeType, + fixed_data: &'a FixedData<'a, T>, + evaluate_unknown_to_zero: bool, + ) -> Self { + Self { + current, + next, + current_row_index, + fixed_data, + evaluate_unknown_to_zero, + } + } + + fn get_cell(&self, poly: &PolynomialReference) -> &Cell { + match poly.next { + false => &self.current[&poly.poly_id()], + true => &self.next[&poly.poly_id()], + } + } + + pub fn get_value(&self, poly: &PolynomialReference) -> Option { + match self.get_cell(poly).value { + CellValue::Known(value) => Some(value), + _ => { + if self.evaluate_unknown_to_zero { + Some(T::zero()) + } else { + None + } + } + } + } + + /// Tries to evaluate the expression to an expression affine in the witness polynomials, + /// taking current values of polynomials into account. + /// @returns an expression affine in the witness polynomials + pub fn evaluate<'b>( + &self, + expr: &'b Expression, + ) -> AffineResult<&'b PolynomialReference, T> { + ExpressionEvaluator::new(SymoblicWitnessEvaluator::new( + self.fixed_data, + self.current_row_index, + self, + )) + .evaluate(expr) + } +} + +impl WitnessColumnEvaluator for RowPair<'_, '_, T> { + fn value<'b>(&self, poly: &'b PolynomialReference) -> AffineResult<&'b PolynomialReference, T> { + Ok(match self.get_value(poly) { + Some(v) => v.into(), + None => AffineExpression::from_variable_id(poly), + }) + } +} + +impl RangeConstraintSet<&PolynomialReference, T> for RowPair<'_, '_, T> { + fn range_constraint(&self, poly: &PolynomialReference) -> Option> { + match self.get_cell(poly).value { + CellValue::RangeConstraint(ref c) => Some(c.clone()), + _ => None, + } + } +} diff --git a/executor/src/witgen/symbolic_witness_evaluator.rs b/executor/src/witgen/symbolic_witness_evaluator.rs index 7c70d3c7d..fd2f151ef 100644 --- a/executor/src/witgen/symbolic_witness_evaluator.rs +++ b/executor/src/witgen/symbolic_witness_evaluator.rs @@ -16,7 +16,7 @@ pub trait WitnessColumnEvaluator { pub struct SymoblicWitnessEvaluator<'a, T, WA: WitnessColumnEvaluator> { fixed_data: &'a FixedData<'a, T>, row: DegreeType, - witness_access: WA, + witness_access: &'a WA, } impl<'a, T, WA> SymoblicWitnessEvaluator<'a, T, WA> @@ -26,7 +26,7 @@ where /// Constructs a new SymbolicWitnessEvaluator /// @param row the row on which to evaluate plain fixed /// columns ("next columns" - f' - are evaluated on row + 1). - pub fn new(fixed_data: &'a FixedData<'a, T>, row: DegreeType, witness_access: WA) -> Self { + pub fn new(fixed_data: &'a FixedData<'a, T>, row: DegreeType, witness_access: &'a WA) -> Self { Self { fixed_data, row, diff --git a/halo2/src/mock_prover.rs b/halo2/src/mock_prover.rs index 85bd89acf..64fd26ae5 100644 --- a/halo2/src/mock_prover.rs +++ b/halo2/src/mock_prover.rs @@ -103,7 +103,7 @@ mod test { #[test] fn secondary_block_machine_add2() { - mock_prove_asm("../test_data/asm/secondary_block_machine_add2.asm", &vec![]); + mock_prove_asm("../test_data/asm/secondary_block_machine_add2.asm", &[]); } #[test]