mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-05-13 03:00:26 -04:00
Merge pull request #126 from chriseth/generalize_evaluator
Generalize witness evaluator.
This commit is contained in:
@@ -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<AffineExpression, EvalError> {
|
||||
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<Option<AbstractNumberType>>,
|
||||
/// Values of the witness polynomials in the next row
|
||||
pub next_witnesses: &'a Vec<Option<AbstractNumberType>>,
|
||||
pub next_row: DegreeType,
|
||||
pub evaluate_row: EvaluationRow,
|
||||
}
|
||||
|
||||
impl<'a> SymbolicVariables for EvaluationData<'a> {
|
||||
fn constant(&self, name: &str) -> Result<AffineExpression, EvalError> {
|
||||
Ok(self.fixed_data.constants[name].clone().into())
|
||||
}
|
||||
|
||||
impl<'a> WitnessColumnEvaluator for EvaluationData<'a> {
|
||||
fn value(&self, name: &str, next: bool) -> Result<AffineExpression, EvalError> {
|
||||
// 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)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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
|
||||
|
||||
68
src/witness_generator/symbolic_witness_evaluator.rs
Normal file
68
src/witness_generator/symbolic_witness_evaluator.rs
Normal file
@@ -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<AffineExpression, EvalError>;
|
||||
}
|
||||
|
||||
/// 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<AffineExpression, EvalError> {
|
||||
Ok(self.fixed_data.constants[name].clone().into())
|
||||
}
|
||||
|
||||
fn value(&self, name: &str, next: bool) -> Result<AffineExpression, EvalError> {
|
||||
// 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)
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user