diff --git a/src/witness_generator/generator.rs b/src/witness_generator/generator.rs index 72cc3a038..77c2dba44 100644 --- a/src/witness_generator/generator.rs +++ b/src/witness_generator/generator.rs @@ -8,9 +8,10 @@ use crate::number::{AbstractNumberType, DegreeType}; use super::affine_expression::AffineExpression; use super::bit_constraints::{BitConstraint, BitConstraintSet}; use super::eval_error::EvalError; -use super::expression_evaluator::{ExpressionEvaluator, SymbolicVariables}; +use super::expression_evaluator::ExpressionEvaluator; use super::machines::Machine; -use super::util::contains_next_witness_ref; +use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator}; +use super::util::{contains_next_witness_ref, WitnessColumnNamer}; use super::{Constraint, EvalResult, FixedData, WitnessColumn}; pub struct Generator<'a, QueryCallback> @@ -250,6 +251,8 @@ where // If there is no "next" reference in the expression, // we just evaluate it directly on the "next" row. let row = if contains_next_witness_ref(identity, self.fixed_data) { + // 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 @@ -349,13 +352,22 @@ where expr: &Expression, evaluate_row: EvaluationRow, ) -> Result { - ExpressionEvaluator::new(EvaluationData { - fixed_data: self.fixed_data, - current_witnesses: &self.current, - next_witnesses: &self.next, - next_row: self.next_row, - evaluate_row, - }) + let degree = self.fixed_data.degree; + 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 { + fixed_data: self.fixed_data, + current_witnesses: &self.current, + next_witnesses: &self.next, + evaluate_row, + }, + )) .evaluate(expr) } @@ -392,62 +404,43 @@ struct EvaluationData<'a> { pub current_witnesses: &'a Vec>, /// Values of the witness polynomials in the next row pub next_witnesses: &'a Vec>, - pub next_row: DegreeType, pub evaluate_row: EvaluationRow, } -impl<'a> SymbolicVariables for EvaluationData<'a> { - fn constant(&self, name: &str) -> Result { - Ok(self.fixed_data.constants[name].clone().into()) - } - +impl<'a> WitnessColumnEvaluator for EvaluationData<'a> { fn value(&self, name: &str, next: bool) -> Result { - // TODO arrays - if let Some(id) = self.fixed_data.witness_ids.get(name) { - // TODO we could also work with both p and p' as symbolic variables and only eliminate them at the end. - - match (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.clone().into()) - .ok_or_else(|| EvalError::PreviousValueUnknown(name.to_string())) - } - (false, EvaluationRow::Next) | (true, EvaluationRow::Current) => { - Ok(if let Some(value) = &self.next_witnesses[*id] { - // We already computed the concrete value - value.clone().into() - } else { - // We continue with a symbolic value - AffineExpression::from_witness_poly_value(*id) - }) - } - (true, EvaluationRow::Next) => { - // "double next" or evaluation of a witness on a specific row - Err(format!( - "{name}' references the next-next row when evaluating on the current row.", - ) - .into()) - } + let id = self.fixed_data.witness_ids[name]; + match (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.clone().into()) + .ok_or_else(|| EvalError::PreviousValueUnknown(name.to_string())) } - } else { - // Constant polynomial (or something else) - let values = self.fixed_data.fixed_cols[name]; - let degree = values.len() as DegreeType; - let mut row = match self.evaluate_row { - EvaluationRow::Current => (self.next_row + degree - 1) % degree, - EvaluationRow::Next => self.next_row, - }; - if next { - row = (row + 1) % degree; + (false, EvaluationRow::Next) | (true, EvaluationRow::Current) => { + Ok(if let Some(value) = &self.next_witnesses[id] { + // We already computed the concrete value + value.clone().into() + } else { + // We continue with a symbolic value + AffineExpression::from_witness_poly_value(id) + }) + } + (true, EvaluationRow::Next) => { + // "double next" or evaluation of a witness on a specific row + Err(format!( + "{name}' references the next-next row when evaluating on the current row.", + ) + .into()) } - Ok(values[row as usize].clone().into()) } } +} - fn format(&self, expr: AffineExpression) -> String { - expr.format(self.fixed_data) +impl<'a> WitnessColumnNamer for EvaluationData<'a> { + fn name(&self, i: usize) -> String { + self.fixed_data.name(i) } } diff --git a/src/witness_generator/mod.rs b/src/witness_generator/mod.rs index e7dd78602..2a62353a5 100644 --- a/src/witness_generator/mod.rs +++ b/src/witness_generator/mod.rs @@ -15,6 +15,7 @@ pub mod fixed_evaluator; mod generator; mod machines; pub mod symbolic_evaluator; +mod symbolic_witness_evaluator; mod util; /// Generates the committed polynomial values diff --git a/src/witness_generator/symbolic_witness_evaluator.rs b/src/witness_generator/symbolic_witness_evaluator.rs new file mode 100644 index 000000000..294ee68c4 --- /dev/null +++ b/src/witness_generator/symbolic_witness_evaluator.rs @@ -0,0 +1,68 @@ +use crate::number::DegreeType; + +use super::{ + affine_expression::AffineExpression, eval_error::EvalError, + expression_evaluator::SymbolicVariables, util::WitnessColumnNamer, FixedData, +}; + +pub trait WitnessColumnEvaluator { + /// Returns a symbolic or concrete value for the given witness column and next flag. + /// This function defines the mapping to IDs. + /// It should be used together with a matching reverse mapping in WitnessColumnNamer. + fn value(&self, name: &str, next: bool) -> Result; +} + +/// An evaluator (to be used together with ExpressionEvaluator) that performs concrete +/// evaluation of all fixed columns but falls back to a generic WitnessColumnEvaluator +/// to evaluate the witness columns either symbolically or concretely. +pub struct SymoblicWitnessEvaluator<'a, WA: WitnessColumnEvaluator + WitnessColumnNamer> { + fixed_data: &'a FixedData<'a>, + row: DegreeType, + witness_access: WA, +} + +impl<'a, WA> SymoblicWitnessEvaluator<'a, WA> +where + WA: WitnessColumnEvaluator + WitnessColumnNamer, +{ + /// 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>, row: DegreeType, witness_access: WA) -> Self { + Self { + fixed_data, + row, + witness_access, + } + } +} + +impl<'a, WA> SymbolicVariables for SymoblicWitnessEvaluator<'a, WA> +where + WA: WitnessColumnEvaluator + WitnessColumnNamer, +{ + fn constant(&self, name: &str) -> Result { + Ok(self.fixed_data.constants[name].clone().into()) + } + + fn value(&self, name: &str, next: bool) -> Result { + // TODO arrays + if self.fixed_data.witness_ids.contains_key(name) { + self.witness_access.value(name, next) + } else { + // Constant polynomial (or something else) + let values = self.fixed_data.fixed_cols[name]; + let row = if next { + let degree = values.len() as DegreeType; + (self.row + 1) % degree + } else { + self.row + }; + Ok(values[row as usize].clone().into()) + } + } + + fn format(&self, expr: AffineExpression) -> String { + expr.format(&self.witness_access) + } +}