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

Abstract machine.

Browse Source
This commit is contained in:
chriseth
2023-03-07 16:01:18 +01:00
parent f71c5705e1
commit cf5ced091a
5 changed files with 183 additions and 132 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
src/commit_evaluator/evaluator.rs
View File

@@ -7,7 +7,7 @@ use crate::number::{AbstractNumberType, DegreeType};
use super::affine_expression::AffineExpression;
use super::eval_error::{self, EvalError};
use super::machine::Machine;
use super::machine::{LookupReturn, Machine};
use super::{EvalResult, FixedData, WitnessColumn};
pub struct Evaluator<'a, QueryCallback>
@@ -16,7 +16,7 @@ where
{
fixed_data: &'a FixedData<'a>,
identities: Vec<&'a Identity>,
machines: Vec<Machine<'a>>,
machines: Vec<Box<dyn Machine>>,
query_callback: Option<QueryCallback>,
/// Maps the witness polynomial names to their IDs internal to this component
/// and optional parameter and query string.
@@ -48,7 +48,7 @@ where
pub fn new(
fixed_data: &'a FixedData<'a>,
identities: Vec<&'a Identity>,
machines: Vec<Machine<'a>>,
machines: Vec<Box<dyn Machine>>,
query_callback: Option<QueryCallback>,
) -> Self {
let witness_cols = fixed_data.witness_cols;
@@ -162,7 +162,7 @@ where
pub fn machine_witness_col_values(&mut self) -> HashMap<String, Vec<AbstractNumberType>> {
let mut result: HashMap<_, _> = Default::default();
for m in &mut self.machines {
result.extend(m.witness_col_values());
result.extend(m.witness_col_values(self.fixed_data));
}
result
}
@@ -293,9 +293,10 @@ where
// Try to see if it's a query to a machine.
for m in &mut self.machines {
// TODO also consider the reasons above.
let result = m.process_plookup(&left, &identity.right)?;
if !result.is_empty() {
return Ok(result);
if let LookupReturn::Assignments(assignments) =
m.process_plookup(self.fixed_data, &left, &identity.right)?
{
return Ok(assignments);
}
}

153
src/commit_evaluator/machine.rs
View File

@@ -1,130 +1,43 @@
use std::collections::{btree_map::Entry, BTreeMap, HashMap, HashSet};
use std::collections::HashMap;
use crate::{
analyzer::{Identity, SelectedExpressions},
number::AbstractNumberType,
};
use crate::{analyzer::SelectedExpressions, number::AbstractNumberType};
use super::{affine_expression::AffineExpression, EvalResult, FixedData};
use super::{affine_expression::AffineExpression, eval_error::EvalError, FixedData};
/// A machine is a set of witness columns and identities where the columns
/// are used on the righ-hand-side
pub struct Machine<'a> {
fixed_data: &'a FixedData<'a>,
/// These are the identities only concerning the machine columns.
_identities: Vec<&'a Identity>,
/// Maps the witness polynomial names to their IDs internal to this component
/// and optional parameter and query string.
//witness_cols: BTreeMap<&'a String, &'a WitnessColumn<'a>>,
witness_names: HashSet<&'a String>,
/// are used on the righ-hand-side of lookups. It can process plookups.
pub trait Machine {
// /// Tries to construct a new machine with the given subset of
// /// witness columns and identities. If the identities do not
// /// fit the pattern of the machine type, it can return None.
// fn try_new(
// fixed_data: &'a FixedData<'a>,
// identities: Vec<&'a Identity>,
// witness_names: HashSet<&'a String>,
// ) -> Option<Box<Self>>;
// TODO this is specific to the sorted write-once memory machine.
data: BTreeMap<AbstractNumberType, AbstractNumberType>,
}
impl<'a> Machine<'a> {
pub fn new(
fixed_data: &'a FixedData<'a>,
identities: Vec<&'a Identity>,
witness_names: HashSet<&'a String>,
) -> Machine<'a> {
// TODO we should check the identities and select certain machines
// based on patterns (and just return an object that implements a trait).
// Now we just assume that we have two columns
// that are sorted by a column called "m_addr"
Machine {
_identities: identities,
fixed_data,
witness_names,
data: Default::default(),
}
}
/// Process a plookup. The convention is to return an empty assignment
/// if this is not a query to this machine and only return an error
/// if the identity is violated.
pub fn process_plookup(
/// Process o plookup. Not all values on the LHS need to be available.
/// Can update internal data.
fn process_plookup(
&mut self,
fixed_data: &FixedData,
left: &[Option<AffineExpression>],
right: &SelectedExpressions,
) -> EvalResult {
assert!(right.selector.is_none());
let rhs = right
.expressions
.iter()
.map(|e| match e {
crate::analyzer::Expression::PolynomialReference(p) => {
if self.witness_names.contains(&p.name) {
Some(&p.name)
} else {
None
}
}
_ => None,
})
.collect::<Vec<_>>();
if rhs.iter().any(|e| e.is_none()) {
return Ok(vec![]);
}
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()) {
(Some(a), Some(v)) => match self.data.entry(a.clone()) {
Entry::Vacant(e) => {
if self.fixed_data.verbose {
println!("Stored in memory: {a}: {v}");
}
e.insert(v);
Ok(vec![])
}
Entry::Occupied(e) => {
if e.get() != &v {
Err(format!(
"Lookup mismatch: There is already a unique row {a}, {} (new value: {v})", e.get()).into())
} else {
Ok(vec![])
}
}
},
(Some(a), None) => {
if let Some(value) = self.data.get(&a) {
if let Some(assignment) = (v.clone() - value.clone().into()).solve() {
if self.fixed_data.verbose {
println!("Read from memory: {a}: {value}");
}
Ok(vec![assignment])
} else {
Err("Cannot solve".to_string().into())
}
} else {
Err(format!("Value at address {a} not known").into())
}
}
(None, _) => Err("Address must be known: <format affin eexpr> TODO"
.to_string()
.into()),
},
) -> LookupResult;
_ => Ok(vec![]),
}
}
pub fn witness_col_values(&mut self) -> HashMap<String, Vec<AbstractNumberType>> {
let (mut addr, mut values): (Vec<_>, Vec<_>) =
std::mem::take(&mut self.data).into_iter().unzip();
values.resize(self.fixed_data.degree as usize, 0.into());
let mut last_addr = addr.last().cloned().unwrap_or_default();
while addr.len() < self.fixed_data.degree as usize {
last_addr += 1;
addr.push(last_addr.clone());
}
[
("Assembly.m_value".to_string(), values),
("Assembly.m_addr".to_string(), addr),
]
.into_iter()
.collect()
}
/// Returns the final values of the witness columns.
fn witness_col_values(
&mut self,
fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>>;
}
pub type LookupResult = Result<LookupReturn, EvalError>;
pub enum LookupReturn {
/// The query is not applicable to this machine type.
NotApplicable,
/// The machne type can fully handle this query and it is
/// (partially) satisfied with the given assignments.
Assignments(Vec<(usize, AbstractNumberType)>),
}

13
src/commit_evaluator/machine_extractor.rs
View File

@@ -2,7 +2,10 @@ use std::collections::HashSet;
use crate::analyzer::{Expression, Identity, SelectedExpressions};
use super::{machine::Machine, FixedData, WitnessColumn};
use super::machine::Machine;
use super::sorted_witness_machine::SortedWitnesses;
use super::{FixedData, WitnessColumn};
/// Finds machines in the witness columns and identities
/// and returns a list of machines and the identities
@@ -11,7 +14,7 @@ pub fn split_out_machines<'a>(
fixed: &'a FixedData<'a>,
identities: &'a [Identity],
witness_cols: &'a [WitnessColumn],
) -> (Vec<Machine<'a>>, Vec<&'a Identity>) {
) -> (Vec<Box<dyn Machine>>, Vec<&'a Identity>) {
// TODO we only split out one machine for now.
// We could also split the machine into independent sub-machines.
@@ -31,7 +34,7 @@ pub fn split_out_machines<'a>(
// Split identities into those that only concern the machine
// witnesses and those that concern any other witness.
let (machine_identities, identities) = identities.iter().partition(|i| {
let (machine_identities, identities): (Vec<_>, _) = identities.iter().partition(|i| {
// The identity has at least one a machine witness, but
// all referenced witnesses are machine witnesses.
let mw = machine_witness_extractor.in_identity(i);
@@ -41,9 +44,9 @@ pub fn split_out_machines<'a>(
// TODO we probably nede to check that machine witnesses do not appear
// in any identity among `identities` except on the RHS.
let machine = Machine::new(fixed, machine_identities, machine_witnesses);
let machine = SortedWitnesses::try_new(fixed, &machine_identities, &machine_witnesses);
(vec![machine], identities)
(vec![machine.unwrap()], identities)
}
/// Extracts all references to any of the given names

1
src/commit_evaluator/mod.rs
View File

@@ -10,6 +10,7 @@ mod eval_error;
mod evaluator;
mod machine;
mod machine_extractor;
mod sorted_witness_machine;
/// Generates the committed polynomial values
/// @returns the values (in source order) and the degree of the polynomials.

133
src/commit_evaluator/sorted_witness_machine.rs Normal file
View File

@@ -0,0 +1,133 @@
use std::collections::{btree_map::Entry, BTreeMap, HashMap, HashSet};
use crate::analyzer::{Identity, SelectedExpressions};
use crate::commit_evaluator::machine::LookupReturn;
use crate::number::AbstractNumberType;
use super::affine_expression::AffineExpression;
use super::machine::{LookupResult, Machine};
use super::FixedData;
pub struct SortedWitnesses {
/// These are the identities only concerning the machine columns.
_identities: Vec<Identity>,
/// Maps the witness polynomial names to their IDs internal to this component
/// and optional parameter and query string.
//witness_cols: BTreeMap<&'a String, &'a WitnessColumn<'a>>,
witness_names: HashSet<String>,
// TODO this is specific to the sorted write-once memory machine.
data: BTreeMap<AbstractNumberType, AbstractNumberType>,
}
impl SortedWitnesses {
pub fn try_new(
_fixed_data: &FixedData,
identities: &[&Identity],
witness_names: &HashSet<&String>,
) -> Option<Box<Self>> {
// TODO we should check the identities and select certain machines
// based on patterns (and just return an object that implements a trait).
// Now we just assume that we have two columns
// that are sorted by a column called "m_addr"
Some(Box::new(SortedWitnesses {
_identities: identities.iter().map(|&i| i.clone()).collect(),
witness_names: witness_names.iter().map(|&w| w.clone()).collect(),
data: Default::default(),
}))
}
}
impl Machine for SortedWitnesses {
/// Process a plookup. The convention is to return an empty assignment
/// if this is not a query to this machine and only return an error
/// if the identity is violated.
fn process_plookup(
&mut self,
fixed_data: &FixedData,
left: &[Option<AffineExpression>],
right: &SelectedExpressions,
) -> LookupResult {
assert!(right.selector.is_none());
let rhs = right
.expressions
.iter()
.map(|e| match e {
crate::analyzer::Expression::PolynomialReference(p) => {
if self.witness_names.contains(&p.name) {
Some(&p.name)
} else {
None
}
}
_ => None,
})
.collect::<Vec<_>>();
if rhs.iter().any(|e| e.is_none()) {
return Ok(LookupReturn::NotApplicable);
}
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()) {
(Some(a), Some(v)) => match self.data.entry(a.clone()) {
Entry::Vacant(e) => {
if fixed_data.verbose {
println!("Stored in memory: {a}: {v}");
}
e.insert(v);
Ok(LookupReturn::Assignments(vec![]))
}
Entry::Occupied(e) => {
if e.get() != &v {
Err(format!(
"Lookup mismatch: There is already a unique row {a}, {} (new value: {v})", e.get()).into())
} else {
Ok(LookupReturn::Assignments(vec![]))
}
}
},
(Some(a), None) => {
if let Some(value) = self.data.get(&a) {
if let Some(assignment) = (v.clone() - value.clone().into()).solve() {
if fixed_data.verbose {
println!("Read from memory: {a}: {value}");
}
Ok(LookupReturn::Assignments(vec![assignment]))
} else {
Err("Cannot solve".to_string().into())
}
} else {
Err(format!("Value at address {a} not known").into())
}
}
(None, _) => Err("Address must be known: <format affin eexpr> TODO"
.to_string()
.into()),
},
_ => Ok(LookupReturn::Assignments(vec![])),
}
}
fn witness_col_values(
&mut self,
fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>> {
let (mut addr, mut values): (Vec<_>, Vec<_>) =
std::mem::take(&mut self.data).into_iter().unzip();
values.resize(fixed_data.degree as usize, 0.into());
let mut last_addr = addr.last().cloned().unwrap_or_default();
while addr.len() < fixed_data.degree as usize {
last_addr += 1;
addr.push(last_addr.clone());
}
[
("Assembly.m_value".to_string(), values),
("Assembly.m_addr".to_string(), addr),
]
.into_iter()
.collect()
}
}