From 34f8f1c04ccf0506a02547a1d935658e3e48f44d Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 2 May 2023 11:05:30 +0200 Subject: [PATCH] Use poly ref in expression evaluator. --- executor/src/witgen/eval_result.rs | 2 +- executor/src/witgen/expression_evaluator.rs | 6 +++--- executor/src/witgen/fixed_evaluator.rs | 8 ++++---- executor/src/witgen/generator.rs | 12 ++++++------ executor/src/witgen/machines/block_machine.rs | 10 +++++----- executor/src/witgen/symbolic_evaluator.rs | 15 ++++++++++----- executor/src/witgen/symbolic_witness_evaluator.rs | 15 ++++++++------- 7 files changed, 37 insertions(+), 31 deletions(-) diff --git a/executor/src/witgen/eval_result.rs b/executor/src/witgen/eval_result.rs index 59c2f2c5d..b45e39d21 100644 --- a/executor/src/witgen/eval_result.rs +++ b/executor/src/witgen/eval_result.rs @@ -7,7 +7,7 @@ use super::bit_constraints::BitConstraint; #[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(String), + PreviousValueUnknown(u64), /// 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/expression_evaluator.rs b/executor/src/witgen/expression_evaluator.rs index 0fa8e1688..ee3f02d21 100644 --- a/executor/src/witgen/expression_evaluator.rs +++ b/executor/src/witgen/expression_evaluator.rs @@ -1,5 +1,5 @@ use number::FieldElement; -use pil_analyzer::{BinaryOperator, Expression, UnaryOperator}; +use pil_analyzer::{BinaryOperator, Expression, PolynomialReference, UnaryOperator}; use super::{ affine_expression::{AffineExpression, AffineResult}, @@ -10,7 +10,7 @@ pub trait SymbolicVariables { /// Acutal constant, not fixed polynomial fn constant(&self, name: &str) -> AffineResult; /// Value of a polynomial (fixed or witness). - fn value(&self, name: &str, next: bool) -> AffineResult; + fn value(&self, poly: &PolynomialReference) -> AffineResult; fn format(&self, expr: AffineExpression) -> String; } @@ -30,7 +30,7 @@ impl ExpressionEvaluator { // we could store the simplified values. match expr { Expression::Constant(name) => self.variables.constant(name), - Expression::PolynomialReference(poly) => self.variables.value(&poly.name, poly.next), + Expression::PolynomialReference(poly) => self.variables.value(poly), Expression::Number(n) => Ok((*n).into()), Expression::BinaryOperation(left, op, right) => { self.evaluate_binary_operation(left, op, right) diff --git a/executor/src/witgen/fixed_evaluator.rs b/executor/src/witgen/fixed_evaluator.rs index d444c143e..21d76c4c4 100644 --- a/executor/src/witgen/fixed_evaluator.rs +++ b/executor/src/witgen/fixed_evaluator.rs @@ -1,7 +1,7 @@ use super::affine_expression::{AffineExpression, AffineResult}; - use super::expression_evaluator::SymbolicVariables; use super::FixedData; +use pil_analyzer::PolynomialReference; /// Evaluates only fixed columns on a specific row. pub struct FixedEvaluator<'a> { @@ -20,11 +20,11 @@ impl<'a> SymbolicVariables for FixedEvaluator<'a> { Ok(self.fixed_data.constants[name].into()) } - fn value(&self, name: &str, next: bool) -> AffineResult { + fn value(&self, poly: &PolynomialReference) -> AffineResult { // TODO arrays - if let Some(col_data) = self.fixed_data.fixed_cols.get(name) { + if let Some(col_data) = self.fixed_data.fixed_cols.get(poly.name.as_str()) { let degree = col_data.len(); - let row = if next { + let row = if poly.next { (self.row + 1) % degree } else { self.row diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index ad29ac0ce..f22d81544 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -1,5 +1,5 @@ use parser_util::lines::indent; -use pil_analyzer::{Expression, Identity, IdentityKind}; +use pil_analyzer::{Expression, Identity, IdentityKind, PolynomialReference}; use std::collections::{BTreeMap, HashMap}; use std::time::Instant; // TODO should use finite field instead of abstract number @@ -495,16 +495,16 @@ struct EvaluationData<'a> { } impl<'a> WitnessColumnEvaluator for EvaluationData<'a> { - fn value(&self, name: &str, next: bool) -> AffineResult { - let id = self.fixed_data.witness_ids[name]; - match (next, self.evaluate_row) { + fn value(&self, poly: &PolynomialReference) -> AffineResult { + let id = poly.poly_id() as usize; + 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_else(|| IncompleteCause::PreviousValueUnknown(name.to_string())) + .ok_or(IncompleteCause::PreviousValueUnknown(id as u64)) } (false, EvaluationRow::Next) | (true, EvaluationRow::Current) => { Ok(if let Some(value) = &self.next_witnesses[id] { @@ -517,7 +517,7 @@ impl<'a> WitnessColumnEvaluator for EvaluationData<'a> { } (true, EvaluationRow::Next) => { unimplemented!( - "{name}' references the next-next row when evaluating on the current row." + "{poly} references the next-next row when evaluating on the current row." ); } } diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 7172820a4..bf5577cee 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -14,7 +14,7 @@ use crate::witgen::{ Constraint, EvalError, }; use number::{DegreeType, FieldElement}; -use pil_analyzer::{Expression, Identity, IdentityKind, SelectedExpressions}; +use pil_analyzer::{Expression, Identity, IdentityKind, PolynomialReference, SelectedExpressions}; /// A machine that produces multiple rows (one block) per query. /// TODO we do not actually "detect" the machine yet, we just check if @@ -458,9 +458,9 @@ struct WitnessData<'a> { } impl<'a> WitnessColumnEvaluator for WitnessData<'a> { - fn value(&self, name: &str, next: bool) -> AffineResult { - let id = self.fixed_data.witness_ids[name]; - let row = if next { + fn value(&self, poly: &PolynomialReference) -> AffineResult { + let id = poly.poly_id() as usize; + let row = if poly.next { (self.row + 1) % self.fixed_data.degree } else { self.row @@ -471,7 +471,7 @@ impl<'a> WitnessColumnEvaluator for WitnessData<'a> { Some(value) => Ok(value.into()), None => { let witness_count = self.fixed_data.witness_cols.len(); - let symbolic_id = if next { id + witness_count } else { id }; + let symbolic_id = if poly.next { id + witness_count } else { id }; Ok(AffineExpression::from_variable_id(symbolic_id)) } } diff --git a/executor/src/witgen/symbolic_evaluator.rs b/executor/src/witgen/symbolic_evaluator.rs index 45082d561..1f013e7da 100644 --- a/executor/src/witgen/symbolic_evaluator.rs +++ b/executor/src/witgen/symbolic_evaluator.rs @@ -1,10 +1,10 @@ use std::collections::HashMap; use super::affine_expression::{AffineExpression, AffineResult}; - use super::expression_evaluator::SymbolicVariables; use super::util::WitnessColumnNamer; use super::FixedData; +use pil_analyzer::PolynomialReference; /// A purely symbolic evaluator. /// Note: The affine expressions it returns will contain variables @@ -75,15 +75,20 @@ impl<'a> SymbolicVariables for SymbolicEvaluator<'a> { Ok(self.fixed_data.constants[name].into()) } - fn value(&self, name: &str, next: bool) -> AffineResult { + fn value(&self, poly: &PolynomialReference) -> AffineResult { // TODO arrays - if self.fixed_data.witness_ids.get(name).is_some() { + if self + .fixed_data + .witness_ids + .get(poly.name.as_str()) + .is_some() + { Ok(AffineExpression::from_variable_id( - self.id_for_witness_poly(name, next), + self.id_for_witness_poly(&poly.name, poly.next), )) } else { Ok(AffineExpression::from_variable_id( - self.id_for_fixed_poly(name, next), + self.id_for_fixed_poly(&poly.name, poly.next), )) } } diff --git a/executor/src/witgen/symbolic_witness_evaluator.rs b/executor/src/witgen/symbolic_witness_evaluator.rs index 6b31d6726..1df473d14 100644 --- a/executor/src/witgen/symbolic_witness_evaluator.rs +++ b/executor/src/witgen/symbolic_witness_evaluator.rs @@ -1,4 +1,5 @@ use number::DegreeType; +use pil_analyzer::PolynomialReference; use super::{ affine_expression::{AffineExpression, AffineResult}, @@ -11,7 +12,7 @@ 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) -> AffineResult; + fn value(&self, poly: &PolynomialReference) -> AffineResult; } /// An evaluator (to be used together with ExpressionEvaluator) that performs concrete @@ -47,18 +48,18 @@ where Ok(self.fixed_data.constants[name].into()) } - fn value(&self, name: &str, next: bool) -> AffineResult { + fn value(&self, poly: &PolynomialReference) -> AffineResult { // TODO arrays - if self.fixed_data.witness_ids.contains_key(name) { - self.witness_access.value(name, next) + if poly.is_witness() { + self.witness_access.value(poly) } else { // Constant polynomial (or something else) let values = self .fixed_data .fixed_cols - .get(name) - .unwrap_or_else(|| panic!("unknown col: {name}")); - let row = if next { + .get(poly.name.as_str()) // TODO we need those accessible by ID instead of by name. + .unwrap_or_else(|| panic!("unknown col: {}", poly.name)); + let row = if poly.next { let degree = values.len() as DegreeType; (self.row + 1) % degree } else {