github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-05-13 03:00:26 -04:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #87 from chriseth/extract_fixed_lookup

Browse Source 
Extract fixed column lookup.
This commit is contained in:
chriseth
2023-03-08 18:15:14 +01:00
committed by GitHub
parent b4de2da899 d3566345a2
commit b046d7d03c
7 changed files with 247 additions and 138 deletions
Download Patch File Download Diff File Expand all files Collapse all files

141
src/commit_evaluator/evaluator.rs
View File

@@ -6,9 +6,10 @@ use std::collections::{BTreeMap, HashMap};
use crate::number::{AbstractNumberType, DegreeType};
use super::affine_expression::AffineExpression;
use super::eval_error::{self, EvalError};
use super::eval_error::EvalError;
use super::expression_evaluator::{ExpressionEvaluator, SymbolicVariables};
use super::machine::{LookupReturn, Machine};
use super::util::contains_next_ref;
use super::{EvalResult, FixedData, WitnessColumn};
pub struct Evaluator<'a, QueryCallback>
@@ -36,8 +37,6 @@ enum EvaluationRow {
Current,
/// p is p[next_row], p' is p[next_row + 1]
Next,
/// p is p[arg], p' is p[arg + 1]
Specific(DegreeType),
}
impl<'a, QueryCallback> Evaluator<'a, QueryCallback>
@@ -221,7 +220,7 @@ where
fn process_polynomial_identity(&self, identity: &Expression) -> EvalResult {
// If there is no "next" reference in the expression,
// we just evaluate it directly on the "next" row.
let row = if self.contains_next_ref(identity) {
let row = if contains_next_ref(identity, self.fixed_data) {
EvaluationRow::Current
} else {
EvaluationRow::Next
@@ -265,26 +264,17 @@ where
return Err("Selectors at the RHS not yet supported.".to_string().into());
}
let mut reasons = vec![];
let left = identity
.left
.expressions
.iter()
.map(|e| self.evaluate(e, EvaluationRow::Next))
.map(|e| match e {
Ok(r) => Some(r),
Err(e) => {
reasons.push(e);
None
}
})
.collect::<Vec<_>>();
// TODO: We need to call the machine even if the LHS is already known.
// But then we also need a way to flag "progress" and we also need
// always call the machine, even if all witnesses are already known.
// Try to see if it's a query to a machine.
// 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?
for m in &mut self.machines {
// TODO also consider the reasons above.
if let LookupReturn::Assignments(assignments) =
@@ -294,97 +284,9 @@ where
}
}
// If we already know the LHS, skip it.
if left
.iter()
.all(|v| v.is_some() && v.as_ref().unwrap().is_constant())
{
return Ok(vec![]);
}
// TODO turn the rest of this code into a specialized machine that does
// lookups inside constants.
// TODO this ignores the error in `reasons` above.
let left_key = match left[0].clone() {
Some(v) => match v.constant_value() {
Some(v) => Ok(v),
None => Err(format!(
"First expression needs to be constant but is not: {}.",
v.format(self.fixed_data)
)),
},
// TODO this ignores the error in `reasons` above.
None => Err("First expression on the LHS is unknown.".to_string()),
}?;
let right_key = identity.right.expressions.first().unwrap();
let rhs_row = if let Expression::PolynomialReference(poly) = right_key {
// TODO we really need a search index on this.
self.fixed_data.fixed_cols
.get(poly.name.as_str())
.cloned()
.and_then(|values| values.iter().position(|v| *v == left_key))
.ok_or_else(|| {
format!(
"Unable to find matching row on the RHS where the first element is {left_key} - only fixed columns supported there."
)
})
.map(|i| i as DegreeType)
} else {
Err("First item on the RHS must be a polynomial reference.".to_string())
}?;
// TODO we only support the following case:
// - The first component on the LHS has to be known
// - The first component on the RHS has to be a direct fixed column reference
// - The first match of those uniquely determines the rest of the RHS.
//TODO there should be a shortcut to succeed if any of an iterator is "Ok" and combine the errors otherwise.
let mut result = vec![];
for (l, r) in left.iter().zip(&identity.right.expressions).skip(1) {
if let Some(l) = l {
match self.equate_to_constant_rhs(l, r, rhs_row) {
Ok(assignments) => result.extend(assignments),
Err(err) => reasons.push(err),
}
} // The error is already in "reasons"
}
if result.is_empty() {
Err(reasons.into_iter().reduce(eval_error::combine).unwrap())
} else {
Ok(result)
}
}
fn equate_to_constant_rhs(
&self,
l: &AffineExpression,
r: &Expression,
rhs_row: DegreeType,
) -> EvalResult {
// This needs to be a costant because symbolic variables
// would reference a different row!
let r = self
.evaluate(r, EvaluationRow::Specific(rhs_row))
.and_then(|r| {
r.constant_value().ok_or_else(|| {
format!("Constant value required: {}", r.format(self.fixed_data)).into()
})
})?;
let evaluated = l.clone() - r.clone().into();
match evaluated.solve() {
Some((id, value)) => Ok(vec![(id, value)]),
None => {
let formatted = l.format(self.fixed_data);
Err(if evaluated.is_invalid() {
format!("Constraint is invalid ({formatted} != {r}).",).into()
} else {
format!("Could not solve expression {formatted} = {r}.",).into()
})
}
}
Err("Could not find a matching machine for the lookup."
.to_string()
.into())
}
fn handle_eval_result(&mut self, result: EvalResult) {
@@ -422,25 +324,6 @@ where
})
.evaluate(expr)
}
/// @returns true if the expression contains a reference to a next value of a witness column.
fn contains_next_ref(&self, expr: &Expression) -> bool {
match expr {
Expression::PolynomialReference(poly) => {
poly.next && self.witness_cols.contains_key(poly.name.as_str())
}
Expression::Tuple(items) => items.iter().any(|e| self.contains_next_ref(e)),
Expression::BinaryOperation(l, _, r) => {
self.contains_next_ref(l) || self.contains_next_ref(r)
}
Expression::UnaryOperation(_, e) => self.contains_next_ref(e),
Expression::FunctionCall(_, args) => args.iter().any(|e| self.contains_next_ref(e)),
Expression::Constant(_)
| Expression::LocalVariableReference(_)
| Expression::PublicReference(_)
| Expression::Number(_)
| Expression::String(_) => false,
}
}
}
struct EvaluationData<'a> {
@@ -488,9 +371,6 @@ impl<'a> SymbolicVariables for EvaluationData<'a> {
)
.into())
}
(_, EvaluationRow::Specific(_)) => {
panic!("Witness polynomial {name} evaluated on specific row.")
}
}
} else {
// Constant polynomial (or something else)
@@ -499,7 +379,6 @@ impl<'a> SymbolicVariables for EvaluationData<'a> {
let mut row = match self.evaluate_row {
EvaluationRow::Current => (self.next_row + degree - 1) % degree,
EvaluationRow::Next => self.next_row,
EvaluationRow::Specific(r) => r,
};
if next {
row = (row + 1) % degree;

180
src/commit_evaluator/fixed_lookup_machine.rs Normal file
View File

@@ -0,0 +1,180 @@
use std::collections::{HashMap, HashSet};
use crate::analyzer::{Expression, Identity, SelectedExpressions};
use crate::commit_evaluator::eval_error;
use crate::commit_evaluator::expression_evaluator::ExpressionEvaluator;
use crate::commit_evaluator::machine::LookupReturn;
use crate::commit_evaluator::util::contains_witness_ref;
use crate::number::{AbstractNumberType, DegreeType};
use super::affine_expression::AffineExpression;
use super::eval_error::EvalError;
use super::expression_evaluator::SymbolicVariables;
use super::machine::{LookupResult, Machine};
use super::{EvalResult, FixedData};
/// Machine to perform a lookup in fixed columns only.
/// It only supports lookup in the first column of the query and will use the first match.
pub struct FixedLookup {}
impl FixedLookup {
pub fn try_new(
_fixed_data: &FixedData,
identities: &[&Identity],
witness_names: &HashSet<&str>,
) -> Option<Box<Self>> {
if identities.is_empty() && witness_names.is_empty() {
Some(Box::new(FixedLookup {}))
} else {
None
}
}
}
impl Machine for FixedLookup {
fn process_plookup(
&mut self,
fixed_data: &FixedData,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult {
// This is a matching machine if the RHS is fully constant.
assert!(right.selector.is_none());
if right
.expressions
.iter()
.any(|e| contains_witness_ref(e, fixed_data))
{
println!("NA");
return Ok(LookupReturn::NotApplicable);
}
// If we already know the LHS, skip it.
if left
.iter()
.all(|v| v.is_ok() && v.as_ref().unwrap().is_constant())
{
return Ok(LookupReturn::Assignments(vec![]));
}
let left_key = match left[0].clone() {
Ok(v) => match v.constant_value() {
Some(v) => Ok(v),
None => Err(format!(
"First expression needs to be constant but is not: {}.",
v.format(fixed_data)
)),
},
Err(err) => Err(format!("First expression on the LHS is unknown: {err}")),
}?;
let right_key = right.expressions.first().unwrap();
let rhs_row = if let Expression::PolynomialReference(poly) = right_key {
// TODO we really need a search index on this.
fixed_data.fixed_cols
.get(poly.name.as_str())
.and_then(|values| values.iter().position(|v| *v == left_key))
.ok_or_else(|| {
format!(
"Unable to find matching row on the RHS where the first element is {left_key} - only fixed columns supported there."
)
})
.map(|i| i as DegreeType)
} else {
Err("First item on the RHS must be a polynomial reference.".to_string())
}?;
// TODO we only support the following case:
// - The first component on the LHS has to be known
// - The first component on the RHS has to be a direct fixed column reference
// - The first match of those uniquely determines the rest of the RHS.
let mut reasons = vec![];
let mut result = vec![];
for (l, r) in left.iter().zip(right.expressions.iter()).skip(1) {
match l {
Ok(l) => match self.equate_to_constant_rhs(l, r, fixed_data, rhs_row) {
Ok(assignments) => result.extend(assignments),
Err(err) => reasons.push(err),
},
Err(err) => {
reasons.push(format!("Value of LHS component too complex: {err}").into());
}
}
}
if result.is_empty() {
Err(reasons.into_iter().reduce(eval_error::combine).unwrap())
} else {
Ok(LookupReturn::Assignments(result))
}
}
fn witness_col_values(
&mut self,
_fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>> {
Default::default()
}
}
impl FixedLookup {
fn equate_to_constant_rhs(
&self,
l: &AffineExpression,
r: &Expression,
fixed_data: &FixedData,
rhs_row: DegreeType,
) -> EvalResult {
let rhs_evaluator = ExpressionEvaluator::new(EvaluateFixedOnRow {
fixed_data,
row: rhs_row,
});
// This needs to be a costant because symbolic variables
// would reference a different row!
let r = rhs_evaluator.evaluate(r).and_then(|r| {
r.constant_value()
.ok_or_else(|| format!("Constant value required: {}", r.format(fixed_data)).into())
})?;
let evaluated = l.clone() - r.clone().into();
match evaluated.solve() {
Some((id, value)) => Ok(vec![(id, value)]),
None => {
let formatted = l.format(fixed_data);
Err(if evaluated.is_invalid() {
format!("Constraint is invalid ({formatted} != {r}).",).into()
} else {
format!("Could not solve expression {formatted} = {r}.",).into()
})
}
}
}
}
/// Evaluates references to fixed columns on a specific row.
struct EvaluateFixedOnRow<'a> {
pub fixed_data: &'a FixedData<'a>,
pub row: DegreeType,
}
impl<'a> SymbolicVariables for EvaluateFixedOnRow<'a> {
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
let values = self.fixed_data.fixed_cols[name];
let degree = values.len() as DegreeType;
let row = if next {
(self.row + 1) % degree
} else {
self.row
};
Ok(values[row as usize].clone().into())
}
fn format(&self, expr: AffineExpression) -> String {
expr.format(self.fixed_data)
}
}

2
src/commit_evaluator/machine.rs
View File

@@ -21,7 +21,7 @@ pub trait Machine {
fn process_plookup(
&mut self,
fixed_data: &FixedData,
left: &[Option<AffineExpression>],
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult;

7
src/commit_evaluator/machine_extractor.rs
View File

@@ -2,6 +2,7 @@ use std::collections::HashSet;
use crate::analyzer::{Expression, Identity, SelectedExpressions};
use super::fixed_lookup_machine::FixedLookup;
use super::machine::Machine;
use super::sorted_witness_machine::SortedWitnesses;
@@ -18,6 +19,8 @@ pub fn split_out_machines<'a>(
// TODO we only split out one machine for now.
// We could also split the machine into independent sub-machines.
// The lookup-in-fixed-columns machine, it always exists with an empty set of witnesses.
let fixed_lookup = FixedLookup::try_new(fixed, &[], &Default::default()).unwrap();
let witness_names = witness_cols.iter().map(|c| c.name).collect::<HashSet<_>>();
let all_witnesses = ReferenceExtractor::new(witness_names.clone());
// Extract all witness columns in the RHS of lookups.
@@ -27,7 +30,7 @@ pub fn split_out_machines<'a>(
.reduce(|l, r| &l | &r)
.unwrap_or_default();
if machine_witnesses.is_empty() {
return (vec![], identities.iter().collect());
return (vec![fixed_lookup], identities.iter().collect());
}
let machine_witness_extractor = ReferenceExtractor::new(machine_witnesses.clone());
@@ -46,7 +49,7 @@ pub fn split_out_machines<'a>(
let machine = SortedWitnesses::try_new(fixed, &machine_identities, &machine_witnesses);
(vec![machine.unwrap()], identities)
(vec![machine.unwrap(), fixed_lookup], identities)
}
/// Extracts all references to any of the given names

1
src/commit_evaluator/mod.rs
View File

@@ -10,6 +10,7 @@ mod affine_expression;
mod eval_error;
mod evaluator;
mod expression_evaluator;
mod fixed_lookup_machine;
mod machine;
mod machine_extractor;
mod sorted_witness_machine;

11
src/commit_evaluator/sorted_witness_machine.rs
View File

@@ -5,6 +5,7 @@ use crate::commit_evaluator::machine::LookupReturn;
use crate::number::AbstractNumberType;
use super::affine_expression::AffineExpression;
use super::eval_error::EvalError;
use super::machine::{LookupResult, Machine};
use super::FixedData;
@@ -46,7 +47,7 @@ impl Machine for SortedWitnesses {
fn process_plookup(
&mut self,
fixed_data: &FixedData,
left: &[Option<AffineExpression>],
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult {
assert!(right.selector.is_none());
@@ -70,7 +71,7 @@ impl Machine for SortedWitnesses {
assert_eq!(rhs[0].unwrap(), &"Assembly.m_addr".to_string());
assert_eq!(rhs[1].unwrap(), &"Assembly.m_value".to_string());
match (&left[0], &left[1]) {
(Some(a), Some(v)) => match (a.constant_value(), v.constant_value()) {
(Ok(a), Ok(v)) => match (a.constant_value(), v.constant_value()) {
(Some(a), Some(v)) => match self.data.entry(a.clone()) {
Entry::Vacant(e) => {
if fixed_data.verbose {
@@ -106,8 +107,10 @@ impl Machine for SortedWitnesses {
.to_string()
.into()),
},
_ => Ok(LookupReturn::Assignments(vec![])),
(Err(e), Ok(_)) | (Ok(_), Err(e)) => {
Err(format!("LHS value unknown for lookup: {e}").into())
}
(Err(e1), Err(e2)) => Err(format!("LHS values unknown for lookup: {e1}, {e2}").into()),
}
}

43
src/commit_evaluator/util.rs
View File

@@ -1,3 +1,46 @@
use crate::analyzer::Expression;
use super::FixedData;
pub trait WitnessColumnNamer {
fn name(&self, i: usize) -> &str;
}
/// @returns true if the expression contains a reference to a next value of a witness column.
pub fn contains_next_ref(expr: &Expression, fixed_data: &FixedData) -> bool {
expr_any(expr, &mut |e| match e {
Expression::PolynomialReference(poly) => {
poly.next && fixed_data.witness_ids.contains_key(poly.name.as_str())
}
_ => false,
})
}
/// @returns true if the expression contains a reference to a witness column.
pub fn contains_witness_ref(expr: &Expression, fixed_data: &FixedData) -> bool {
expr_any(expr, &mut |e| match e {
Expression::PolynomialReference(poly) => {
fixed_data.witness_ids.contains_key(poly.name.as_str())
}
_ => false,
})
}
pub fn expr_any(expr: &Expression, f: &mut impl FnMut(&Expression) -> bool) -> bool {
if f(expr) {
true
} else {
match expr {
Expression::Tuple(items) => items.iter().any(|e| expr_any(e, f)),
Expression::BinaryOperation(l, _, r) => expr_any(l, f) || expr_any(r, f),
Expression::UnaryOperation(_, e) => expr_any(e, f),
Expression::FunctionCall(_, args) => args.iter().any(|e| expr_any(e, f)),
Expression::Constant(_)
| Expression::PolynomialReference(_)
| Expression::LocalVariableReference(_)
| Expression::PublicReference(_)
| Expression::Number(_)
| Expression::String(_) => false,
}
}
}