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 #228 from chriseth/use_refs_in_eval

Browse Source 
Use poly ref in expression evaluator.
This commit is contained in:
chriseth
2023-05-04 17:31:06 +02:00
committed by GitHub
parent b6aca7eca2 34f8f1c04c
commit 225c20aa25
7 changed files with 37 additions and 31 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
executor/src/witgen/eval_result.rs
View File

@@ -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<usize>),
/// Some bit constraints are overlapping. Example: `x + y == 0x3` with `x | 0x3` and `y | 0x3`

6
executor/src/witgen/expression_evaluator.rs
View File

@@ -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<SV: SymbolicVariables> ExpressionEvaluator<SV> {
// 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)

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

@@ -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

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

@@ -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."
);
}
}

10
executor/src/witgen/machines/block_machine.rs
View File

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

15
executor/src/witgen/symbolic_evaluator.rs
View File

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

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

@@ -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 {