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 #97 from chriseth/bit_constraints

Browse Source 
Bit Constraints
This commit is contained in:
chriseth
2023-03-23 11:52:54 +01:00
committed by GitHub
parent 69993acfef ea1adcbd02
commit 04a1f00e6c
17 changed files with 1142 additions and 233 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
src/asm_compiler/mod.rs
View File

@@ -1,14 +1,18 @@
use std::collections::{BTreeMap, HashMap};
use crate::number::AbstractNumberType;
use crate::number::DegreeType;
use crate::parser::asm_ast::*;
use crate::parser::ast::*;
use crate::parser::{self, ParseError};
pub fn compile<'a>(file_name: Option<&str>, input: &'a str) -> Result<PILFile, ParseError<'a>> {
// TODO configure the degree
let max_steps = 1024;
parser::parse_asm(file_name, input).map(|ast| ASMPILConverter::new().convert(ast, max_steps))
pub fn compile<'a>(
file_name: Option<&str>,
input: &'a str,
row_count: DegreeType,
) -> Result<PILFile, ParseError<'a>> {
// TODO define the row count / poly degree in the assembly file.
parser::parse_asm(file_name, input).map(|ast| ASMPILConverter::new().convert(ast, row_count))
}
#[derive(Default)]
@@ -29,7 +33,7 @@ impl ASMPILConverter {
Default::default()
}
fn convert(&mut self, input: ASMFile, max_steps: usize) -> PILFile {
fn convert(&mut self, input: ASMFile, max_steps: DegreeType) -> PILFile {
self.pil.push(Statement::Namespace(
0,
"Assembly".to_string(),
@@ -791,7 +795,7 @@ pol constant p_reg_write_X_CNT = [1, 0, 0, 0, 0, 0, 0, 0, 0];
"#;
let file_name = "tests/simple_sum.asm";
let contents = fs::read_to_string(file_name).unwrap();
let pil = compile(Some(file_name), &contents).unwrap();
let pil = compile(Some(file_name), &contents, 1024).unwrap();
assert_eq!(format!("{pil}").trim(), expectation.trim());
}
}

7
src/bin/compiler.rs
View File

@@ -22,6 +22,11 @@ enum Commands {
#[arg(default_value_t = String::new())]
inputs: String,
/// Number of rows (degree of the polynomials).
#[arg(short, long)]
#[arg(default_value_t = 1024)]
rows: u64,
/// Output directory for PIL file, json file and fixed and witness column data.
#[arg(short, long)]
#[arg(default_value_t = String::from("."))]
@@ -60,6 +65,7 @@ fn main() {
Commands::Asm {
file,
inputs,
rows,
output_directory,
force,
verbose,
@@ -73,6 +79,7 @@ fn main() {
powdr::compiler::compile_asm(
&file,
inputs,
rows,
Path::new(&output_directory),
force,
verbose,

283
src/commit_evaluator/affine_expression.rs
View File

@@ -1,7 +1,13 @@
use std::{collections::HashSet, ops::Not};
// TODO this should probably rather be a finite field element.
use crate::number::{format_number, is_zero, AbstractNumberType, GOLDILOCKS_MOD};
use super::bit_constraints::{BitConstraint, BitConstraintSet};
use super::eval_error::EvalError::ConflictingBitConstraints;
use super::util::WitnessColumnNamer;
use super::Constraint;
use super::EvalResult;
/// An expression affine in the committed polynomials.
#[derive(Debug, Clone)]
@@ -72,31 +78,175 @@ impl AffineExpression {
/// If the affine expression has only a single variable (with nonzero coefficient),
/// returns the index of the variable and the assignment that evaluates the
/// affine expression to zero.
pub fn solve(&self) -> Option<(usize, AbstractNumberType)> {
pub fn solve(&self) -> EvalResult {
let mut nonzero = self.nonzero_coefficients();
nonzero.next().and_then(|(i, c)| {
if nonzero.next().is_none() {
// c * a + o = 0 <=> a = -o/c
if *c == 1.into() {
Some((i, clamp(-self.offset.clone())))
} else if *c == (-1).into() || *c == (GOLDILOCKS_MOD - 1).into() {
Some((i, self.offset.clone()))
} else {
Some((
nonzero
.next()
.and_then(|(i, c)| {
if nonzero.next().is_none() {
// c * a + o = 0 <=> a = -o/c
Some(vec![(
i,
clamp(-clamp(
self.offset.clone() * inv(c.clone(), GOLDILOCKS_MOD.into()),
)),
))
Constraint::Assignment(if *c == 1.into() {
clamp(-self.offset.clone())
} else if *c == (-1).into() || *c == (GOLDILOCKS_MOD - 1).into() {
self.offset.clone()
} else {
clamp(-clamp(
self.offset.clone() * inv(c.clone(), GOLDILOCKS_MOD.into()),
))
}),
)])
} else {
None
}
} else {
})
.ok_or_else(|| "Cannot solve affine expression.".to_string().into())
}
/// Tries to solve "self = 0", or at least propagate a bit constraint:
/// If we know that some components can only have certain bits set and the offset is zero,
/// this property might transfer to another component.
/// Furthermore, if we know that all components are bit-constrained and do not overlap,
/// we can deduce the values of all components from the offset part.
pub fn solve_with_bit_constraints(
&self,
known_constraints: &impl BitConstraintSet,
) -> EvalResult {
// Try to solve directly.
if let Ok(result) = self.solve() {
return Ok(result);
}
let new_constraints: Option<_> = if self
.nonzero_coefficients()
.all(|(i, _coeff)| known_constraints.bit_constraint(i).is_some())
{
// We might be able to solve for one or more variables, if all
// bit constraints are disjoint.
// Try positive and negative. We might also experiment with other strategies.
let result = self
.try_solve_through_constraints(known_constraints)
.and_then(|new_constraints| {
if new_constraints.is_empty() {
(-self.clone()).try_solve_through_constraints(known_constraints)
} else {
Ok(new_constraints)
}
})?;
if result.is_empty() {
None
} else {
Some(result)
}
} else if self.offset == 0.into() {
// We might be able to deduce bit constraints on one varaible.
self.try_transfer_constraints(known_constraints)
} else {
None
};
new_constraints.ok_or_else(|| {
"Unable to solve or determine constraints."
.to_string()
.into()
})
}
fn try_transfer_constraints(
&self,
known_constraints: &impl BitConstraintSet,
) -> Option<Vec<(usize, Constraint)>> {
// We need the form X = a * Y + b * Z + ...
// where X is unconstrained and all others are bit-constrained.
let mut unconstrained = self
.nonzero_coefficients()
.filter(|(i, _c)| known_constraints.bit_constraint(*i).is_none());
let solve_for = unconstrained.next()?;
if unconstrained.next().is_some() {
return None;
}
if *solve_for.1 == 1.into() {
return (-self.clone()).try_transfer_constraints(known_constraints);
} else if *solve_for.1 != clamp((-1).into()) {
// We could try to divide by this in the future.
return None;
}
// We can assume that nonzero coefficients is not empty, otherwise we could have solved
// the affine expression directly.
let parts = self
.nonzero_coefficients()
.filter(|(i, _)| *i != solve_for.0)
.map(|(i, coeff)| {
known_constraints
.bit_constraint(i)
.and_then(|con| con.multiple(coeff.clone()))
});
parts
.reduce(|c1, c2| match (c1, c2) {
(Some(c1), Some(c2)) => c1.try_combine(&c2),
_ => None,
})
.flatten()
.map(|con| vec![(solve_for.0, Constraint::BitConstraint(con))])
}
/// Tries to assign values to all variables through their bit constraints.
/// This can also determine if the equation is not satsifiable,
/// if the bit-constraints do not cover all the bits of the offset.
/// Returns an empty vector if it is not able to solve the equation.
fn try_solve_through_constraints(
&self,
known_constraints: &impl BitConstraintSet,
) -> EvalResult {
let parts = self
.nonzero_coefficients()
.map(|(i, coeff)| {
(
i,
known_constraints
.bit_constraint(i)
.unwrap()
.multiple(coeff.clone()),
)
})
.collect::<Vec<_>>();
if parts.iter().any(|(_i, con)| con.is_none()) {
return Ok(vec![]);
}
// Check if they are mutually exclusive and compute assignments.
let mut covered_bits = HashSet::<u64>::new();
let mut assignments = vec![];
let mut offset = clamp(-self.offset.clone());
for (i, con) in parts {
let con = con.clone().unwrap();
let BitConstraint { min_bit, max_bit } = con;
for bit in min_bit..=max_bit {
if !covered_bits.insert(bit) {
return Ok(vec![]);
}
}
let mask: AbstractNumberType = con.mask();
assignments.push((
i,
Constraint::Assignment((offset.clone() & mask.clone()) >> min_bit),
));
offset &= mask.not();
}
if offset != 0.into() {
// We were not able to cover all of the offset, so this equation cannot be solved.
Err(ConflictingBitConstraints)
} else {
Ok(assignments)
}
}
/// Returns true if it can be determined that this expression can never be zero.
pub fn is_invalid(&self) -> bool {
// TODO add constraint invalidness.
self.constant_value().map(|v| v != 0.into()) == Some(true)
}
@@ -106,7 +256,7 @@ impl AffineExpression {
let name = namer.name(i);
if *c == 1.into() {
name
} else if *c == (-1).into() {
} else if *c == clamp((-1).into()) {
format!("-{name}")
} else {
format!("{} * {name}", format_number(c))
@@ -177,9 +327,9 @@ impl std::ops::Neg for AffineExpression {
type Output = AffineExpression;
fn neg(mut self) -> Self::Output {
self.coefficients
.iter_mut()
.for_each(|v| *v = clamp(-v.clone()));
self.coefficients.iter_mut().for_each(|v| {
*v = clamp(-v.clone());
});
self.offset = clamp(-self.offset);
self
}
@@ -195,8 +345,13 @@ impl std::ops::Sub for AffineExpression {
#[cfg(test)]
mod test {
use std::collections::BTreeMap;
use super::*;
use crate::number::AbstractNumberType;
use crate::{
commit_evaluator::{bit_constraints::BitConstraint, eval_error::EvalError},
number::AbstractNumberType,
};
use super::{AffineExpression, GOLDILOCKS_MOD};
@@ -259,4 +414,92 @@ mod test {
1
);
}
struct TestBitConstraints(BTreeMap<usize, BitConstraint>);
impl BitConstraintSet for TestBitConstraints {
fn bit_constraint(&self, id: usize) -> Option<BitConstraint> {
self.0.get(&id).cloned()
}
}
#[test]
pub fn derive_constraints() {
let expr = AffineExpression::from_witness_poly_value(1)
- AffineExpression::from_witness_poly_value(2).mul(16.into())
- AffineExpression::from_witness_poly_value(3);
let known_constraints = TestBitConstraints(
vec![
(2, BitConstraint::from_max(7)),
(3, BitConstraint::from_max(3)),
]
.into_iter()
.collect(),
);
assert_eq!(
expr.solve_with_bit_constraints(&known_constraints).unwrap(),
vec![(1, Constraint::BitConstraint(BitConstraint::from_max(11)))]
);
assert_eq!(
(-expr)
.solve_with_bit_constraints(&known_constraints)
.unwrap(),
vec![(1, Constraint::BitConstraint(BitConstraint::from_max(11)))]
);
// Replace factor 16 by 32.
let expr = AffineExpression::from_witness_poly_value(1)
- AffineExpression::from_witness_poly_value(2).mul(32.into())
- AffineExpression::from_witness_poly_value(3);
assert!(expr.solve_with_bit_constraints(&known_constraints).is_err());
// Replace factor 16 by 8.
let expr = AffineExpression::from_witness_poly_value(1)
- AffineExpression::from_witness_poly_value(2).mul(8.into())
- AffineExpression::from_witness_poly_value(3);
assert!(expr.solve_with_bit_constraints(&known_constraints).is_err());
}
#[test]
pub fn solve_through_constraints_success() {
let value = 0x1504u32;
let expr = AffineExpression::from(value)
- AffineExpression::from_witness_poly_value(2).mul(256.into())
- AffineExpression::from_witness_poly_value(3);
let known_constraints = TestBitConstraints(
vec![
(2, BitConstraint::from_max(7)),
(3, BitConstraint::from_max(3)),
]
.into_iter()
.collect(),
);
assert_eq!(value, 0x15 * 256 + 0x4);
assert_eq!(
expr.solve_with_bit_constraints(&known_constraints).unwrap(),
vec![
(2, Constraint::Assignment(0x15.into())),
(3, Constraint::Assignment(0x4.into()))
]
);
}
#[test]
pub fn solve_through_constraints_conflict() {
let value = 0x1554u32;
let expr = AffineExpression::from(value)
- AffineExpression::from_witness_poly_value(2).mul(256.into())
- AffineExpression::from_witness_poly_value(3);
let known_constraints = TestBitConstraints(
vec![
(2, BitConstraint::from_max(7)),
(3, BitConstraint::from_max(3)),
]
.into_iter()
.collect(),
);
match expr.solve_with_bit_constraints(&known_constraints) {
Err(EvalError::ConflictingBitConstraints) => {}
_ => panic!(),
};
}
}

434
src/commit_evaluator/bit_constraints.rs Normal file
View File

@@ -0,0 +1,434 @@
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::{Display, Formatter};
use crate::analyzer::{BinaryOperator, Expression, Identity, IdentityKind, PolynomialReference};
use crate::commit_evaluator::util::{contains_next_ref, WitnessColumnNamer};
use crate::number::{AbstractNumberType, GOLDILOCKS_MOD};
use super::expression_evaluator::ExpressionEvaluator;
use super::symbolic_evaluator::SymbolicEvaluator;
use super::{Constraint, FixedData};
/// Constraint on the bit values of a variable X.
/// All bits smaller than min_bit have to be zero
/// and all bits larger than max_bit have to be zero.
/// The least significant bit is bit zero.
#[derive(PartialEq, Debug, Clone)]
pub struct BitConstraint {
pub min_bit: u64,
pub max_bit: u64,
}
impl BitConstraint {
pub fn from_max(max_bit: u64) -> Self {
BitConstraint {
min_bit: 0,
max_bit,
}
}
/// The bit constraint of the sum of two expressions.
pub fn try_combine(&self, other: &BitConstraint) -> Option<BitConstraint> {
if self.max_bit + 1 == other.min_bit {
Some(BitConstraint {
min_bit: self.min_bit,
max_bit: other.max_bit,
})
} else if other.max_bit + 1 == self.min_bit {
Some(BitConstraint {
min_bit: other.min_bit,
max_bit: self.max_bit,
})
} else {
None
}
}
/// The bit constraint of an integer multiple of an expression.
/// TODO this assumes goldilocks
pub fn multiple(&self, factor: AbstractNumberType) -> Option<BitConstraint> {
if factor.clone() * (1 << self.max_bit) >= GOLDILOCKS_MOD.into() {
None
} else {
// TODO use binary logarithm
(0..64).find_map(|i| {
if factor.clone() == (1u64 << i).into() {
Some(BitConstraint {
min_bit: self.min_bit + i,
max_bit: self.max_bit + i,
})
} else {
None
}
})
}
}
pub fn mask(&self) -> AbstractNumberType {
((AbstractNumberType::from(1) << (1 + self.max_bit - self.min_bit)) - 1) << self.min_bit
}
}
impl Display for BitConstraint {
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
write!(f, "0x{:x}", self.mask())
}
}
/// Trait that provides a bit constraint on a symbolic variable if given by ID.
pub trait BitConstraintSet {
fn bit_constraint(&self, id: usize) -> Option<BitConstraint>;
}
pub struct SimpleBitConstraintSet<'a, Namer: WitnessColumnNamer> {
bit_constraints: &'a BTreeMap<&'a str, BitConstraint>,
names: &'a Namer,
}
impl<'a, Namer: WitnessColumnNamer> BitConstraintSet for SimpleBitConstraintSet<'a, Namer> {
fn bit_constraint(&self, id: usize) -> Option<BitConstraint> {
self.bit_constraints
.get(self.names.name(id).as_str())
.cloned()
}
}
/// Determines global constraints on witness and fixed columns.
/// Removes identities that only serve to create bit constraints from
/// the identities vector.
/// TODO at some point, we should check that they still hold.
pub fn determine_global_constraints<'a>(
fixed_data: &'a FixedData,
identities: Vec<&'a Identity>,
) -> (BTreeMap<&'a str, BitConstraint>, Vec<&'a Identity>) {
let mut known_constraints = BTreeMap::new();
for (&name, &values) in &fixed_data.fixed_cols {
if let Some(cons) = process_fixed_column(values) {
known_constraints.insert(name, cons);
}
}
// For these columns, we know that they are not only constrained to those bits
// but also have one row for each possible value.
let full_span = known_constraints.keys().copied().collect::<BTreeSet<_>>();
let mut reduced_identities = vec![];
for identity in identities {
let remove;
(known_constraints, remove) =
propagate_constraints(fixed_data, known_constraints, identity, &full_span);
if !remove {
reduced_identities.push(identity)
}
}
(known_constraints, reduced_identities)
}
/// Analyzes a fixed column and checks if its values correspond exactly
/// to a certain bit pattern.
/// TODO do this on the symbolic definition instead of the values.
fn process_fixed_column(fixed: &[AbstractNumberType]) -> Option<BitConstraint> {
if let Some(bit) = smallest_period_candidate(fixed) {
let mask: u64 = (1 << bit) - 1;
for (i, v) in fixed.iter().enumerate() {
if *v != (i as u64 & mask).into() {
return None;
}
}
Some(BitConstraint {
min_bit: 0,
max_bit: bit - 1,
})
} else {
None
}
}
/// Deduces new bit constraints on witness columns from constraints on fixed columns
/// and identities. Note that these constraints hold globaly, i.e. for all rows.
/// If the returned flag is true, the identity can be removed, because it contains
/// no further information than the bit constraint.
fn propagate_constraints<'a>(
fixed_data: &'a FixedData,
mut known_constraints: BTreeMap<&'a str, BitConstraint>,
identity: &'a Identity,
full_span: &BTreeSet<&'a str>,
) -> (BTreeMap<&'a str, BitConstraint>, bool) {
let mut remove = false;
match identity.kind {
IdentityKind::Polynomial => {
if let Some(p) =
is_binary_constraint(fixed_data, identity.left.selector.as_ref().unwrap())
{
assert!(known_constraints
.insert(p, BitConstraint::from_max(0))
.is_none());
remove = true;
} else if let Some((p, c)) = try_transfer_constraints(
fixed_data,
identity.left.selector.as_ref().unwrap(),
&known_constraints,
) {
assert!(known_constraints.insert(p, c).is_none());
}
}
IdentityKind::Plookup | IdentityKind::Permutation | IdentityKind::Connect => {
if identity.left.selector.is_some() || identity.right.selector.is_some() {
return (known_constraints, false);
}
for (left, right) in identity
.left
.expressions
.iter()
.zip(identity.right.expressions.iter())
{
if let (Some(left), Some(right)) = (is_simple_poly(left), is_simple_poly(right)) {
if let Some(constraint) = known_constraints.get(right).cloned() {
assert!(known_constraints.insert(left, constraint).is_none());
}
}
}
if identity.kind == IdentityKind::Plookup && identity.right.expressions.len() == 1 {
// We can only remove the lookup if the RHS is a fixed polynomial that
// provides all values in the span.
if let Some(name) = is_simple_poly(&identity.right.expressions[0]) {
if full_span.contains(name) {
remove = true;
}
}
}
}
}
(known_constraints, remove)
}
/// Tries to find "X * (1 - X) = 0"
fn is_binary_constraint<'a>(fixed_data: &'a FixedData, expr: &Expression) -> Option<&'a str> {
// TODO Write a proper pattern matching engine.
if let Expression::BinaryOperation(left, BinaryOperator::Sub, right) = expr {
if let Expression::Number(n) = right.as_ref() {
if *n == 0.into() {
return is_binary_constraint(fixed_data, left.as_ref());
}
}
} else if let Expression::BinaryOperation(left, BinaryOperator::Mul, right) = expr {
let symbolic_ev = SymbolicEvaluator::new(fixed_data);
let left_root = ExpressionEvaluator::new(symbolic_ev.clone())
.evaluate(left)
.ok()
.and_then(|l| l.solve().ok())?;
let right_root = ExpressionEvaluator::new(symbolic_ev.clone())
.evaluate(right)
.ok()
.and_then(|r| r.solve().ok())?;
if let ([(id1, Constraint::Assignment(value1))], [(id2, Constraint::Assignment(value2))]) =
(&left_root[..], &right_root[..])
{
let poly1 = symbolic_ev.poly_from_id(*id1);
let poly2 = symbolic_ev.poly_from_id(*id2);
if poly1 != poly2 || !fixed_data.witness_ids.contains_key(poly1.0) {
return None;
}
if (*value1 == 0.into() && *value2 == 1.into())
|| (*value1 == 1.into() && *value2 == 0.into())
{
return Some(poly1.0);
}
}
}
None
}
/// Tries to transfer constraints in a linear expression.
fn try_transfer_constraints<'a>(
fixed_data: &'a FixedData,
expr: &'a Expression,
known_constraints: &BTreeMap<&str, BitConstraint>,
) -> Option<(&'a str, BitConstraint)> {
if contains_next_ref(expr) {
return None;
}
let symbolic_ev = SymbolicEvaluator::new(fixed_data);
let aff_expr = ExpressionEvaluator::new(symbolic_ev.clone())
.evaluate(expr)
.ok()?;
let result = aff_expr
.solve_with_bit_constraints(&SimpleBitConstraintSet {
bit_constraints: known_constraints,
names: &symbolic_ev,
})
.ok()?;
assert!(result.len() <= 1);
result.get(0).map(|(id, cons)| {
if let Constraint::BitConstraint(cons) = cons {
let (poly, next) = symbolic_ev.poly_from_id(*id);
assert!(!next);
(poly, cons.clone())
} else {
panic!();
}
})
}
fn is_simple_poly(expr: &Expression) -> Option<&str> {
if let Expression::PolynomialReference(PolynomialReference {
name,
index: None,
next: false,
}) = expr
{
Some(name)
} else {
None
}
}
fn smallest_period_candidate(fixed: &[AbstractNumberType]) -> Option<u64> {
if fixed.first() != Some(&0.into()) {
return None;
}
(1..63).find(|bit| fixed.get(1 << bit) == Some(&0.into()))
}
#[cfg(test)]
mod test {
use std::collections::BTreeMap;
use crate::commit_evaluator::bit_constraints::{propagate_constraints, BitConstraint};
use crate::commit_evaluator::{FixedData, WitnessColumn};
use super::process_fixed_column;
#[test]
fn all_zeros() {
let fixed = [0, 0, 0, 0].iter().map(|v| (*v).into()).collect::<Vec<_>>();
assert_eq!(process_fixed_column(&fixed), None);
}
#[test]
fn zero_one() {
let fixed = [0, 1, 0, 1, 0]
.iter()
.map(|v| (*v).into())
.collect::<Vec<_>>();
assert_eq!(
process_fixed_column(&fixed),
Some(BitConstraint {
min_bit: 0,
max_bit: 0
})
);
}
#[test]
fn zero_one_two_three() {
let fixed = [0, 1, 2, 3, 0]
.iter()
.map(|v| (*v).into())
.collect::<Vec<_>>();
assert_eq!(
process_fixed_column(&fixed),
Some(BitConstraint {
min_bit: 0,
max_bit: 1
})
);
}
#[test]
fn test_propagate_constraints() {
let pil_source = r"
namespace Global(2**20);
col fixed BYTE(i) { i & 0xff };
col fixed BYTE2(i) { i & 0xffff };
col witness A;
// A bit more complicated to see that the 'pattern matcher' works properly.
(1 - A + 0) * (A + 1 - 1) = 0;
col witness B;
{ B } in { BYTE };
col witness C;
C = A * 2**8 + B;
";
let analyzed = crate::analyzer::analyze_string(pil_source);
let (constants, degree) = crate::constant_evaluator::generate(&analyzed);
let mut known_constraints = constants
.iter()
.filter_map(|(name, values)| {
process_fixed_column(values).map(|constraint| (*name, constraint))
})
.collect::<BTreeMap<_, _>>();
assert_eq!(
known_constraints,
vec![
("Global.BYTE", BitConstraint::from_max(7)),
("Global.BYTE2", BitConstraint::from_max(15)),
]
.into_iter()
.collect()
);
// TODO write some test code to generate FixedData directly from `analyzed`
let witness_cols: Vec<WitnessColumn> = analyzed
.committed_polys_in_source_order()
.iter()
.enumerate()
.map(|(i, (poly, value))| {
if poly.length.is_some() {
unimplemented!("Committed arrays not implemented.")
}
WitnessColumn::new(i, &poly.absolute_name, value)
})
.collect();
let fixed_data = FixedData {
degree,
constants: &analyzed.constants,
fixed_cols: constants.iter().map(|(n, v)| (*n, v)).collect(),
witness_cols: &witness_cols,
witness_ids: witness_cols.iter().map(|w| (w.name, w.id)).collect(),
verbose: false,
};
for identity in &analyzed.identities {
(known_constraints, _) = propagate_constraints(
&fixed_data,
known_constraints,
identity,
&Default::default(),
);
}
assert_eq!(
known_constraints,
vec![
("Global.A", BitConstraint::from_max(0)),
("Global.B", BitConstraint::from_max(7)),
("Global.C", BitConstraint::from_max(8)),
("Global.BYTE", BitConstraint::from_max(7)),
("Global.BYTE2", BitConstraint::from_max(15)),
]
.into_iter()
.collect()
);
}
#[test]
fn combinations() {
let a = BitConstraint::from_max(7);
let b = a.multiple(256.into()).unwrap();
assert_eq!(
b,
BitConstraint {
min_bit: 8,
max_bit: 15
}
);
assert_eq!(
b.try_combine(&a).unwrap(),
BitConstraint {
min_bit: 0,
max_bit: 15
}
);
}
}

166
src/commit_evaluator/double_sorted_witness_machine.rs
View File

@@ -6,13 +6,12 @@ use itertools::{Either, Itertools};
use crate::analyzer::PolynomialReference;
use crate::analyzer::{Expression, Identity, IdentityKind, SelectedExpressions};
use crate::commit_evaluator::eval_error;
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;
use super::machine::Machine;
use super::{EvalResult, FixedData};
/// TODO make this generic
@@ -69,7 +68,7 @@ impl Machine for DoubleSortedWitnesses {
kind: IdentityKind,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult {
) -> Option<EvalResult> {
if kind != IdentityKind::Permutation
|| (right.selector
!= Some(Expression::PolynomialReference(PolynomialReference {
@@ -84,82 +83,10 @@ impl Machine for DoubleSortedWitnesses {
next: false,
})))
{
return Ok(LookupReturn::NotApplicable);
return None;
}
// We blindly assume the lookup is of the form
// OP { ADDR, STEP, X } is m_is_write { m_addr, m_step, m_value }
// or
// OP { ADDR, STEP, X } is m_is_read { m_addr, m_step, m_value }
// Fail if the LHS has an error.
let (left, errors): (Vec<_>, Vec<_>) = left.iter().partition_map(|x| match x {
Ok(x) => Either::Left(x),
Err(x) => Either::Right(x),
});
if !errors.is_empty() {
return Err(errors
.into_iter()
.cloned()
.reduce(eval_error::combine)
.unwrap());
}
let is_write = match &right.selector {
Some(Expression::PolynomialReference(p)) => p.name == "Assembly.m_is_write",
_ => panic!(),
};
let addr = left[0].constant_value().ok_or_else(|| {
format!(
"Address must be known: {} = {}",
left[0].format(fixed_data),
right.expressions[0]
)
})?;
let step = left[1].constant_value().ok_or_else(|| {
format!(
"Step must be known: {} = {}",
left[1].format(fixed_data),
right.expressions[1]
)
})?;
println!(
"Query addr={addr}, step={step}, write: {is_write}, left: {}",
left[2].format(fixed_data)
);
// TODO this does not check any of the failure modes
let mut assignments = vec![];
if is_write {
let value = match left[2].constant_value() {
Some(v) => v,
None => return Ok(LookupReturn::Assignments(vec![])),
};
if fixed_data.verbose {
println!("Memory write: addr={addr}, step={step}, value={value}");
}
self.data.insert(addr.clone(), value.clone());
self.trace
.insert((addr, step), Operation { is_write, value });
} else {
let value = self.data.entry(addr.clone()).or_default();
self.trace.insert(
(addr.clone(), step.clone()),
Operation {
is_write,
value: value.clone(),
},
);
if fixed_data.verbose {
println!("Memory read: addr={addr}, step={step}, value={value}");
}
assignments.push(match (left[2].clone() - value.clone().into()).solve() {
Some(ass) => ass,
None => return Ok(LookupReturn::Assignments(vec![])),
});
}
Ok(LookupReturn::Assignments(assignments))
Some(self.process_plookup_internal(fixed_data, left, right))
}
fn witness_col_values(
@@ -216,3 +143,86 @@ impl Machine for DoubleSortedWitnesses {
.collect()
}
}
impl DoubleSortedWitnesses {
fn process_plookup_internal(
&mut self,
fixed_data: &FixedData,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> EvalResult {
// We blindly assume the lookup is of the form
// OP { ADDR, STEP, X } is m_is_write { m_addr, m_step, m_value }
// or
// OP { ADDR, STEP, X } is m_is_read { m_addr, m_step, m_value }
// Fail if the LHS has an error.
let (left, errors): (Vec<_>, Vec<_>) = left.iter().partition_map(|x| match x {
Ok(x) => Either::Left(x),
Err(x) => Either::Right(x),
});
if !errors.is_empty() {
return Err(errors
.into_iter()
.cloned()
.reduce(eval_error::combine)
.unwrap());
}
let is_write = match &right.selector {
Some(Expression::PolynomialReference(p)) => p.name == "Assembly.m_is_write",
_ => panic!(),
};
let addr = left[0].constant_value().ok_or_else(|| {
format!(
"Address must be known: {} = {}",
left[0].format(fixed_data),
right.expressions[0]
)
})?;
let step = left[1].constant_value().ok_or_else(|| {
format!(
"Step must be known: {} = {}",
left[1].format(fixed_data),
right.expressions[1]
)
})?;
println!(
"Query addr={addr}, step={step}, write: {is_write}, left: {}",
left[2].format(fixed_data)
);
// TODO this does not check any of the failure modes
let mut assignments = vec![];
if is_write {
let value = match left[2].constant_value() {
Some(v) => v,
None => return Ok(vec![]),
};
if fixed_data.verbose {
println!("Memory write: addr={addr}, step={step}, value={value}");
}
self.data.insert(addr.clone(), value.clone());
self.trace
.insert((addr, step), Operation { is_write, value });
} else {
let value = self.data.entry(addr.clone()).or_default();
self.trace.insert(
(addr.clone(), step.clone()),
Operation {
is_write,
value: value.clone(),
},
);
if fixed_data.verbose {
println!("Memory read: addr={addr}, step={step}, value={value}");
}
assignments.extend(match (left[2].clone() - value.clone().into()).solve() {
Ok(ass) => ass,
Err(_) => return Ok(vec![]),
});
}
Ok(assignments)
}
}

5
src/commit_evaluator/eval_error.rs
View File

@@ -4,6 +4,8 @@ use std::fmt::{Display, Formatter, Result};
pub enum EvalError {
/// Previous value of witness column not known when trying to derive a value in the next row.
PreviousValueUnknown(String),
/// Conflicting bit-constraints in an equation, i.e. for X = 0x100, where X is known to be at most 0xff.
ConflictingBitConstraints,
Generic(String),
Multiple(Vec<EvalError>),
}
@@ -34,6 +36,9 @@ impl Display for EvalError {
f,
"Previous value of the following column(s) is not (yet) known: {names}.",
),
EvalError::ConflictingBitConstraints => {
write!(f, "Bit constraints in the expression are conflicting or do not match the constant / offset.",)
}
EvalError::Multiple(errors) => {
let (previous_unknown, mut others) = errors.iter().fold(
(vec![], vec![]),

105
src/commit_evaluator/evaluator.rs
View File

@@ -6,11 +6,12 @@ use std::collections::{BTreeMap, HashMap};
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::machine::{LookupReturn, Machine};
use super::util::contains_next_ref;
use super::{EvalResult, FixedData, WitnessColumn};
use super::machine::Machine;
use super::util::contains_next_witness_ref;
use super::{Constraint, EvalResult, FixedData, WitnessColumn};
pub struct Evaluator<'a, QueryCallback>
where
@@ -20,15 +21,19 @@ where
identities: Vec<&'a Identity>,
machines: Vec<Box<dyn Machine>>,
query_callback: Option<QueryCallback>,
global_bit_constraints: BTreeMap<&'a str, BitConstraint>,
/// Maps the witness polynomial names to optional parameter and query string.
witness_cols: BTreeMap<&'a str, &'a WitnessColumn<'a>>,
/// Values of the witness polynomials
current: Vec<Option<AbstractNumberType>>,
/// Values of the witness polynomials in the next row
next: Vec<Option<AbstractNumberType>>,
/// Bit constraints on the witness polynomials in the next row.
next_bit_constraints: Vec<Option<BitConstraint>>,
next_row: DegreeType,
failure_reasons: Vec<String>,
progress: bool,
last_report: DegreeType,
}
#[derive(PartialEq, Eq, Clone, Copy)]
@@ -46,6 +51,7 @@ where
pub fn new(
fixed_data: &'a FixedData<'a>,
identities: Vec<&'a Identity>,
global_bit_constraints: BTreeMap<&'a str, BitConstraint>,
machines: Vec<Box<dyn Machine>>,
query_callback: Option<QueryCallback>,
) -> Self {
@@ -56,16 +62,27 @@ where
identities,
machines,
query_callback,
global_bit_constraints,
witness_cols: witness_cols.iter().map(|p| (p.name, p)).collect(),
current: vec![None; witness_cols.len()],
next: vec![None; witness_cols.len()],
next_bit_constraints: vec![None; witness_cols.len()],
next_row: 0,
failure_reasons: vec![],
progress: true,
last_report: 0,
}
}
pub fn compute_next_row(&mut self, next_row: DegreeType) -> Vec<AbstractNumberType> {
if next_row >= self.last_report + 1000 {
println!(
"{next_row} of {} rows ({} %)",
self.fixed_data.degree,
next_row * 100 / self.fixed_data.degree
);
self.last_report = next_row;
}
self.next_row = next_row;
// TODO maybe better to generate a dependency graph than looping multiple times.
@@ -135,6 +152,18 @@ where
.join(", ")
);
eprintln!("Reasons:\n{}\n", self.failure_reasons.join("\n\n"));
eprintln!("Known bit constraints:");
eprintln!("Global:");
for (name, cons) in &self.global_bit_constraints {
eprintln!(" {name}: {cons}");
}
eprintln!("For this row:");
for (id, cons) in self.next_bit_constraints.iter().enumerate() {
if let Some(cons) = cons {
eprintln!(" {}: {cons}", self.fixed_data.witness_cols[id].name);
}
}
eprintln!();
eprintln!(
"Current values:\n{}",
indent(&self.format_next_values().join("\n"), " ")
@@ -149,6 +178,7 @@ where
}
std::mem::swap(&mut self.next, &mut self.current);
self.next = vec![None; self.current.len()];
self.next_bit_constraints = vec![None; self.current.len()];
// TODO check a bit better that "None" values do not
// violate constraints.
self.current
@@ -182,13 +212,10 @@ where
.collect()
}
fn process_witness_query(
&mut self,
column: &&WitnessColumn,
) -> Result<Vec<(usize, AbstractNumberType)>, EvalError> {
fn process_witness_query(&mut self, column: &&WitnessColumn) -> EvalResult {
let query = self.interpolate_query(column.query.unwrap())?;
if let Some(value) = self.query_callback.as_mut().and_then(|c| (c)(&query)) {
Ok(vec![(column.id, value)])
Ok(vec![(column.id, Constraint::Assignment(value))])
} else {
Err(format!("No query answer for {} query: {query}.", column.name).into())
}
@@ -222,7 +249,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 contains_next_ref(identity, self.fixed_data) {
let row = if contains_next_witness_ref(identity, self.fixed_data) {
EvaluationRow::Current
} else {
EvaluationRow::Next
@@ -231,17 +258,16 @@ where
if evaluated.constant_value() == Some(0.into()) {
Ok(vec![])
} else {
match evaluated.solve() {
Some((id, value)) => Ok(vec![(id, value)]),
None => {
evaluated
.solve_with_bit_constraints(&self.bit_constraint_set())
.map_err(|_| {
let formatted = evaluated.format(self.fixed_data);
Err(if evaluated.is_invalid() {
if evaluated.is_invalid() {
format!("Constraint is invalid ({formatted} != 0).").into()
} else {
format!("Could not solve expression {formatted} = 0.").into()
})
}
}
}
})
}
}
@@ -276,10 +302,10 @@ where
// 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) =
m.process_plookup(self.fixed_data, identity.kind, &left, &identity.right)?
if let Some(result) =
m.process_plookup(self.fixed_data, identity.kind, &left, &identity.right)
{
return Ok(assignments);
return result;
}
}
@@ -290,11 +316,20 @@ where
fn handle_eval_result(&mut self, result: EvalResult) {
match result {
Ok(assignments) => {
for (id, value) in assignments {
self.next[id] = Some(value);
Ok(constraints) => {
if !constraints.is_empty() {
self.progress = true;
}
for (id, c) in constraints {
match c {
Constraint::Assignment(value) => {
self.next[id] = Some(value);
}
Constraint::BitConstraint(cons) => {
self.next_bit_constraints[id] = Some(cons);
}
}
}
}
Err(reason) => {
self.failure_reasons.push(format!("{reason}"));
@@ -323,6 +358,32 @@ where
})
.evaluate(expr)
}
fn bit_constraint_set(&'a self) -> WitnessBitConstraintSet<'a> {
WitnessBitConstraintSet {
fixed_data: self.fixed_data,
global_bit_constraints: &self.global_bit_constraints,
next_bit_constraints: &self.next_bit_constraints,
}
}
}
struct WitnessBitConstraintSet<'a> {
fixed_data: &'a FixedData<'a>,
/// Global constraints on witness and fixed polynomials.
global_bit_constraints: &'a BTreeMap<&'a str, BitConstraint>,
/// Bit constraints on the witness polynomials in the next row.
next_bit_constraints: &'a Vec<Option<BitConstraint>>,
}
impl<'a> BitConstraintSet for WitnessBitConstraintSet<'a> {
fn bit_constraint(&self, id: usize) -> Option<BitConstraint> {
let name = self.fixed_data.witness_cols[id].name;
self.global_bit_constraints
.get(name)
.or_else(|| self.next_bit_constraints[id].as_ref())
.cloned()
}
}
struct EvaluationData<'a> {

60
src/commit_evaluator/fixed_lookup_machine.rs
View File

@@ -3,14 +3,13 @@ use std::collections::{HashMap, HashSet};
use crate::analyzer::{Expression, Identity, IdentityKind, 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::machine::Machine;
use super::{EvalResult, FixedData};
/// Machine to perform a lookup in fixed columns only.
@@ -38,7 +37,7 @@ impl Machine for FixedLookup {
kind: IdentityKind,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult {
) -> Option<EvalResult> {
// This is a matching machine if it is a plookup and the RHS is fully constant.
if kind != IdentityKind::Plookup
|| right.selector.is_some()
@@ -47,7 +46,7 @@ impl Machine for FixedLookup {
.iter()
.any(|e| contains_witness_ref(e, fixed_data))
{
return Ok(LookupReturn::NotApplicable);
return None;
}
// If we already know the LHS, skip it.
@@ -55,9 +54,27 @@ impl Machine for FixedLookup {
.iter()
.all(|v| v.is_ok() && v.as_ref().unwrap().is_constant())
{
return Ok(LookupReturn::Assignments(vec![]));
return Some(Ok(vec![]));
}
Some(self.process_plookup_internal(fixed_data, left, right))
}
fn witness_col_values(
&mut self,
_fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>> {
Default::default()
}
}
impl FixedLookup {
fn process_plookup_internal(
&mut self,
fixed_data: &FixedData,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> EvalResult {
let left_key = match left[0].clone() {
Ok(v) => match v.constant_value() {
Some(v) => Ok(v),
@@ -90,12 +107,14 @@ impl Machine for FixedLookup {
// - 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 in the other cases, we could at least return some improved bit constraints.
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),
Ok(constraints) => result.extend(constraints),
Err(err) => reasons.push(err),
},
Err(err) => {
@@ -106,18 +125,9 @@ impl Machine for FixedLookup {
if result.is_empty() {
Err(reasons.into_iter().reduce(eval_error::combine).unwrap())
} else {
Ok(LookupReturn::Assignments(result))
Ok(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,
@@ -138,17 +148,15 @@ impl FixedLookup {
})?;
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()
})
// TODO we could use bit constraints here
evaluated.solve().map_err(|_| {
let formatted = l.format(fixed_data);
if evaluated.is_invalid() {
format!("Constraint is invalid ({formatted} != {r}).",).into()
} else {
format!("Could not solve expression {formatted} = {r}.",).into()
}
}
})
}
}

16
src/commit_evaluator/machine.rs
View File

@@ -3,6 +3,7 @@ use std::collections::HashMap;
use crate::analyzer::{IdentityKind, SelectedExpressions};
use crate::number::AbstractNumberType;
use super::EvalResult;
use super::{affine_expression::AffineExpression, eval_error::EvalError, FixedData};
/// A machine is a set of witness columns and identities where the columns
@@ -19,13 +20,16 @@ pub trait Machine {
/// Process a plookup. Not all values on the LHS need to be available.
/// Can update internal data.
/// Only return an error if this machine is able to handle the query and
/// it results in a constraint failure.
/// If this is not the right machine for the query, return `None`.
fn process_plookup(
&mut self,
fixed_data: &FixedData,
kind: IdentityKind,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult;
) -> Option<EvalResult>;
/// Returns the final values of the witness columns.
fn witness_col_values(
@@ -33,13 +37,3 @@ pub trait Machine {
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)>),
}

24
src/commit_evaluator/mod.rs
View File

@@ -3,10 +3,12 @@ use std::collections::HashMap;
use crate::analyzer::{Analyzed, Expression, FunctionValueDefinition};
use crate::number::{AbstractNumberType, DegreeType};
use self::bit_constraints::BitConstraint;
use self::eval_error::EvalError;
use self::util::WitnessColumnNamer;
mod affine_expression;
mod bit_constraints;
mod double_sorted_witness_machine;
mod eval_error;
mod evaluator;
@@ -49,7 +51,15 @@ pub fn generate<'a>(
};
let (machines, identities) =
machine_extractor::split_out_machines(&fixed, &analyzed.identities, &witness_cols);
let mut evaluator = evaluator::Evaluator::new(&fixed, identities, machines, query_callback);
let (global_bit_constraints, identities) =
bit_constraints::determine_global_constraints(&fixed, identities);
let mut evaluator = evaluator::Evaluator::new(
&fixed,
identities,
global_bit_constraints,
machines,
query_callback,
);
let mut values: Vec<(&str, Vec<AbstractNumberType>)> =
witness_cols.iter().map(|p| (p.name, Vec::new())).collect();
@@ -72,9 +82,15 @@ pub fn generate<'a>(
values
}
/// Result of evaluating an expression / lookup:
/// A new assignment to a witness column identified by an ID or an error.
type EvalResult = Result<Vec<(usize, AbstractNumberType)>, EvalError>;
/// Result of evaluating an expression / lookup.
/// New assignments or constraints for witness columns identified by an ID.
type EvalResult = Result<Vec<(usize, Constraint)>, EvalError>;
#[derive(Debug, Clone, PartialEq)]
pub enum Constraint {
Assignment(AbstractNumberType),
BitConstraint(BitConstraint),
}
/// Data that is fixed for witness generation.
pub struct FixedData<'a> {

105
src/commit_evaluator/sorted_witness_machine.rs
View File

@@ -4,16 +4,15 @@ use itertools::{Either, Itertools};
use crate::analyzer::{Expression, Identity, IdentityKind, SelectedExpressions};
use crate::commit_evaluator::eval_error;
use crate::commit_evaluator::machine::LookupReturn;
use crate::number::AbstractNumberType;
use super::affine_expression::AffineExpression;
use super::eval_error::EvalError;
use super::expression_evaluator::ExpressionEvaluator;
use super::fixed_evaluator::FixedEvaluator;
use super::machine::{LookupResult, Machine};
use super::machine::Machine;
use super::symbolic_evaluator::SymbolicEvaluator;
use super::FixedData;
use super::{EvalResult, FixedData};
/// A machine that can support a lookup in a set of columns that are sorted
/// by one specific column and values in that column have to be unique.
@@ -97,8 +96,8 @@ fn check_identity<'a>(fixed_data: &'a FixedData, id: &Identity) -> Option<&'a st
/// Checks that the identity has a constraint of the form `a' - a` as the first expression
/// on the left hand side and returns the name of the witness column.
fn check_constraint<'a>(fixed_data: &'a FixedData, constraint: &Expression) -> Option<&'a str> {
let symbolic_ev = ExpressionEvaluator::new(SymbolicEvaluator::new(fixed_data));
let sort_constraint = match symbolic_ev.evaluate(constraint) {
let symbolic_ev = SymbolicEvaluator::new(fixed_data);
let sort_constraint = match ExpressionEvaluator::new(symbolic_ev.clone()).evaluate(constraint) {
Ok(c) => c,
Err(_) => return None,
};
@@ -106,14 +105,21 @@ fn check_constraint<'a>(fixed_data: &'a FixedData, constraint: &Expression) -> O
[key, _] => *key,
_ => return None,
};
let witness_count = fixed_data.witness_cols.len();
let pattern = AffineExpression::from_witness_poly_value(key_column_id + witness_count)
- AffineExpression::from_witness_poly_value(key_column_id);
let (poly, next) = symbolic_ev.poly_from_id(key_column_id);
if next || fixed_data.witness_ids.get(poly).is_none() {
// Either next-witness or fixed column.
return None;
}
let pattern =
AffineExpression::from_witness_poly_value(symbolic_ev.id_for_witness_poly(poly, true))
- AffineExpression::from_witness_poly_value(
symbolic_ev.id_for_witness_poly(poly, false),
);
if sort_constraint != pattern {
return None;
}
Some(fixed_data.witness_cols[key_column_id].name)
Some(poly)
}
impl Machine for SortedWitnesses {
@@ -123,9 +129,9 @@ impl Machine for SortedWitnesses {
kind: IdentityKind,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
) -> LookupResult {
) -> Option<EvalResult> {
if kind != IdentityKind::Plookup || right.selector.is_some() {
return Ok(LookupReturn::NotApplicable);
return None;
}
let rhs = right
.expressions
@@ -143,10 +149,49 @@ impl Machine for SortedWitnesses {
})
.collect::<Vec<_>>();
if rhs.iter().any(|e| e.is_none()) {
return Ok(LookupReturn::NotApplicable);
return None;
}
let rhs = rhs.iter().map(|x| x.unwrap()).collect::<Vec<_>>();
Some(self.process_plookup_internal(fixed_data, left, right, rhs))
}
fn witness_col_values(
&mut self,
fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>> {
let mut result = HashMap::new();
let (mut keys, mut values): (Vec<_>, Vec<_>) =
std::mem::take(&mut self.data).into_iter().unzip();
let mut last_key = keys.last().cloned().unwrap_or_default();
while keys.len() < fixed_data.degree as usize {
last_key += 1;
keys.push(last_key.clone());
}
result.insert(self.key_col.clone(), keys);
for (col_name, &i) in &self.witness_positions {
let mut col_values = values
.iter_mut()
.map(|row| std::mem::take(&mut row[i]).unwrap_or_default())
.collect::<Vec<_>>();
col_values.resize(fixed_data.degree as usize, 0.into());
result.insert(col_name.clone(), col_values);
}
result
}
}
impl SortedWitnesses {
fn process_plookup_internal(
&mut self,
fixed_data: &FixedData,
left: &[Result<AffineExpression, EvalError>],
right: &SelectedExpressions,
rhs: Vec<&String>,
) -> EvalResult {
// Fail if the LHS has an error.
let (left, errors): (Vec<_>, Vec<_>) = left.iter().partition_map(|x| match x {
Ok(x) => Either::Left(x),
@@ -194,13 +239,13 @@ impl Machine for SortedWitnesses {
// Just a repeated lookup.
} else {
match constraint.solve() {
Some(assignment) => {
Ok(ass) => {
if fixed_data.verbose {
println!("Read {} = {key_value} -> {r} = {v}", self.key_col);
}
assignments.push(assignment);
assignments.extend(ass);
}
None => {
Err(_) => {
return Err(
format!("Cannot solve {} = {v}", l.format(fixed_data)).into()
)
@@ -226,34 +271,6 @@ impl Machine for SortedWitnesses {
},
}
}
Ok(LookupReturn::Assignments(assignments))
}
fn witness_col_values(
&mut self,
fixed_data: &FixedData,
) -> HashMap<String, Vec<AbstractNumberType>> {
let mut result = HashMap::new();
let (mut keys, mut values): (Vec<_>, Vec<_>) =
std::mem::take(&mut self.data).into_iter().unzip();
let mut last_key = keys.last().cloned().unwrap_or_default();
while keys.len() < fixed_data.degree as usize {
last_key += 1;
keys.push(last_key.clone());
}
result.insert(self.key_col.clone(), keys);
for (col_name, &i) in &self.witness_positions {
let mut col_values = values
.iter_mut()
.map(|row| std::mem::take(&mut row[i]).unwrap_or_default())
.collect::<Vec<_>>();
col_values.resize(fixed_data.degree as usize, 0.into());
result.insert(col_name.clone(), col_values);
}
result
Ok(assignments)
}
}

74
src/commit_evaluator/symbolic_evaluator.rs
View File

@@ -1,21 +1,68 @@
use std::collections::HashMap;
use super::affine_expression::AffineExpression;
use super::eval_error::EvalError;
use super::expression_evaluator::SymbolicVariables;
use super::util::WitnessColumnNamer;
use super::FixedData;
/// A purely symbolic evaluator. It wil fail on fixed columns.
/// A purely symbolic evaluator.
/// Note: The affine expressions it returns will contain variables
/// for both the "current" and the "next" row, and they are different!
/// for both the "current" and the "next" row, and for fixed columns as well,
/// and they are all different!
/// This means these AffineExpressions should not be confused with those
/// returned by the EvaluationData struct.
/// The only IDs are allocated in the following order:
/// witness columns, next witness columns, fixed columns, next fixed columns.
#[derive(Clone)]
pub struct SymbolicEvaluator<'a> {
fixed_data: &'a FixedData<'a>,
fixed_ids: HashMap<&'a str, usize>,
fixed_names: Vec<&'a str>,
}
impl<'a> SymbolicEvaluator<'a> {
pub fn new(fixed_data: &'a FixedData<'a>) -> Self {
SymbolicEvaluator { fixed_data }
let mut fixed_names = fixed_data.fixed_cols.keys().cloned().collect::<Vec<_>>();
fixed_names.sort();
let fixed_ids = fixed_names
.iter()
.enumerate()
.map(|(i, n)| (*n, i))
.collect();
SymbolicEvaluator {
fixed_data,
fixed_ids,
fixed_names,
}
}
pub fn poly_from_id(&self, id: usize) -> (&'a str, bool) {
let witness_count = self.fixed_data.witness_ids.len();
if id < 2 * witness_count {
(
self.fixed_data.witness_cols[id % witness_count].name,
id >= witness_count,
)
} else {
let fixed_count = self.fixed_ids.len();
let fixed_id = id - 2 * witness_count;
(
self.fixed_names[fixed_id % fixed_count],
fixed_id >= fixed_count,
)
}
}
pub fn id_for_fixed_poly(&self, name: &str, next: bool) -> usize {
let witness_count = self.fixed_data.witness_ids.len();
let fixed_count = self.fixed_ids.len();
2 * witness_count + self.fixed_ids[name] + if next { fixed_count } else { 0 }
}
pub fn id_for_witness_poly(&self, name: &str, next: bool) -> usize {
let witness_count = self.fixed_data.witness_ids.len();
self.fixed_data.witness_ids[name] + if next { witness_count } else { 0 }
}
}
@@ -26,15 +73,14 @@ impl<'a> SymbolicVariables for SymbolicEvaluator<'a> {
fn value(&self, name: &str, next: bool) -> Result<AffineExpression, EvalError> {
// TODO arrays
if let Some(id) = self.fixed_data.witness_ids.get(name) {
let witness_count = self.fixed_data.witness_ids.len();
if self.fixed_data.witness_ids.get(name).is_some() {
Ok(AffineExpression::from_witness_poly_value(
*id + if next { witness_count } else { 0 },
self.id_for_witness_poly(name, next),
))
} else {
Err("Cannot access fixed columns in the symoblic evaluator."
.to_string()
.into())
Ok(AffineExpression::from_witness_poly_value(
self.id_for_fixed_poly(name, next),
))
}
}
@@ -44,12 +90,12 @@ impl<'a> SymbolicVariables for SymbolicEvaluator<'a> {
}
impl<'a> WitnessColumnNamer for SymbolicEvaluator<'a> {
fn name(&self, i: usize) -> String {
let witness_count = self.fixed_data.witness_ids.len();
if i < witness_count {
self.fixed_data.name(i)
fn name(&self, id: usize) -> String {
let (name, next) = self.poly_from_id(id);
if next {
format!("{name}'")
} else {
format!("{}'", self.fixed_data.name(i - witness_count))
name.to_string()
}
}
}

11
src/commit_evaluator/util.rs
View File

@@ -6,8 +6,17 @@ pub trait WitnessColumnNamer {
fn name(&self, i: usize) -> String;
}
/// @returns true if the expression contains a reference to a next value of a
/// (witness or fixed) column
pub fn contains_next_ref(expr: &Expression) -> bool {
expr_any(expr, &mut |e| match e {
Expression::PolynomialReference(poly) => poly.next,
_ => false,
})
}
/// @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 {
pub fn contains_next_witness_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())

7
src/compiler.rs
View File

@@ -54,6 +54,7 @@ pub fn compile_pil_ast(
pub fn compile_asm(
file_name: &str,
inputs: Vec<AbstractNumberType>,
rows: u64,
output_dir: &Path,
force_overwrite: bool,
verbose: bool,
@@ -63,6 +64,7 @@ pub fn compile_asm(
file_name,
&contents,
inputs,
rows,
output_dir,
force_overwrite,
verbose,
@@ -75,11 +77,12 @@ pub fn compile_asm_string(
file_name: &str,
contents: &str,
inputs: Vec<AbstractNumberType>,
rows: u64,
output_dir: &Path,
force_overwrite: bool,
verbose: bool,
) {
let pil = asm_compiler::compile(Some(file_name), contents).unwrap_or_else(|err| {
let pil = asm_compiler::compile(Some(file_name), contents, rows).unwrap_or_else(|err| {
eprintln!("Error parsing .asm file:");
err.output_to_stderr();
panic!();
@@ -129,6 +132,7 @@ fn compile(
verbose: bool,
) -> bool {
let mut success = true;
println!("Evaluating fixed columns...");
let (constants, degree) = constant_evaluator::generate(analyzed);
if analyzed.constant_count() == constants.len() {
write_polys_file(
@@ -137,6 +141,7 @@ fn compile(
&constants,
);
println!("Wrote constants.bin.");
println!("Deducing witness columns...");
let commits =
commit_evaluator::generate(analyzed, degree, &constants, query_callback, verbose);
write_polys_file(

2
src/number.rs
View File

@@ -23,7 +23,7 @@ pub const GOLDILOCKS_MOD: u64 = 0xffffffff00000001u64;
pub fn format_number(x: &AbstractNumberType) -> String {
if *x > (GOLDILOCKS_MOD / 2).into() {
format!("{}", GOLDILOCKS_MOD - x)
format!("-{}", GOLDILOCKS_MOD - x)
} else {
format!("{x}")
}

34
tests/bit_access.asm Normal file
View File

@@ -0,0 +1,34 @@
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg A;
reg B;
pil{
col witness XInv;
col witness XIsZero;
XIsZero = 1 - X * XInv;
XIsZero * X = 0;
XIsZero * (1 - XIsZero) = 0;
}
// Wraps a value in Y to 32 bits.
// Requires 0 <= Y < 2**33
// TODO we need better syntax for defining instructions that are functions.
// Maybe like instr wrap <=Y= v -> X { Y = X + wrap_bit * 2**32, X = Xhi * 2**16 + Xlo }
instr wrap <=Y= v, x <=X= { Y = X + wrap_bit * 2**32, X = Xhi * 2**16 + Xlo }
pil{
col fixed BYTES2(i) { i & 0xffff };
col witness Xlo;
col witness Xhi;
{ Xlo } in { BYTES2 };
{ Xhi } in { BYTES2 };
col commit wrap_bit;
wrap_bit * (1 - wrap_bit) = 0;
}
instr assert_zero <=X= a { XIsZero = 1 }
B <=X= ${ ("input", 0) };
wrap B + 0xffffffec, A;
assert_zero A;

26
tests/integration.rs
View File

@@ -2,7 +2,7 @@ use std::{fs, path::Path, process::Command};
use itertools::Itertools;
use powdr::compiler;
use powdr::number::AbstractNumberType;
use powdr::number::{AbstractNumberType, DegreeType};
fn verify_pil(file_name: &str, query_callback: Option<fn(&str) -> Option<AbstractNumberType>>) {
let input_file = Path::new(&format!("./tests/{file_name}"))
@@ -18,9 +18,10 @@ fn verify_pil(file_name: &str, query_callback: Option<fn(&str) -> Option<Abstrac
verify(file_name, &temp_dir);
}
fn verify_asm(file_name: &str, inputs: Vec<AbstractNumberType>) {
fn verify_asm(file_name: &str, inputs: Vec<AbstractNumberType>, row_count: Option<DegreeType>) {
let contents = fs::read_to_string(format!("./tests/{file_name}")).unwrap();
let pil = powdr::asm_compiler::compile(Some(file_name), &contents).unwrap();
let pil = powdr::asm_compiler::compile(Some(file_name), &contents, row_count.unwrap_or(1024))
.unwrap();
let pil_file_name = "asm.pil";
let temp_dir = mktemp::Temp::new_dir().unwrap();
assert!(compiler::compile_pil_ast(
@@ -131,6 +132,7 @@ fn simple_sum_asm() {
verify_asm(
"simple_sum.asm",
[16, 4, 1, 2, 8, 5].iter().map(|&x| x.into()).collect(),
None,
);
}
@@ -139,15 +141,29 @@ fn palindrome() {
verify_asm(
"palindrome.asm",
[7, 1, 7, 3, 9, 3, 7, 1].iter().map(|&x| x.into()).collect(),
None,
);
}
#[test]
fn test_mem_read_write() {
verify_asm("mem_read_write.asm", Default::default());
verify_asm("mem_read_write.asm", Default::default(), None);
}
#[test]
fn test_multi_assign() {
verify_asm("multi_assign.asm", [7].iter().map(|&x| x.into()).collect());
verify_asm(
"multi_assign.asm",
[7].iter().map(|&x| x.into()).collect(),
None,
);
}
#[test]
fn test_bit_access() {
verify_asm(
"bit_access.asm",
[20].iter().map(|&x| x.into()).collect(),
Some(0x20000),
);
}