diff --git a/src/asm_compiler/mod.rs b/src/asm_compiler/mod.rs index a6a10a831..f4c1a001e 100644 --- a/src/asm_compiler/mod.rs +++ b/src/asm_compiler/mod.rs @@ -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> { - // 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> { + // 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()); } } diff --git a/src/bin/compiler.rs b/src/bin/compiler.rs index 1f492e5ec..50c76b767 100644 --- a/src/bin/compiler.rs +++ b/src/bin/compiler.rs @@ -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, diff --git a/src/commit_evaluator/affine_expression.rs b/src/commit_evaluator/affine_expression.rs index 830feb836..5dcef410d 100644 --- a/src/commit_evaluator/affine_expression.rs +++ b/src/commit_evaluator/affine_expression.rs @@ -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> { + // 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::>(); + 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::::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); + impl BitConstraintSet for TestBitConstraints { + fn bit_constraint(&self, id: usize) -> Option { + 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!(), + }; + } } diff --git a/src/commit_evaluator/bit_constraints.rs b/src/commit_evaluator/bit_constraints.rs new file mode 100644 index 000000000..87d65e208 --- /dev/null +++ b/src/commit_evaluator/bit_constraints.rs @@ -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 { + 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 { + 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; +} + +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 { + 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::>(); + + 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 { + 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 { + 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::>(); + assert_eq!(process_fixed_column(&fixed), None); + } + + #[test] + fn zero_one() { + let fixed = [0, 1, 0, 1, 0] + .iter() + .map(|v| (*v).into()) + .collect::>(); + 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::>(); + 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::>(); + 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 = 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 + } + ); + } +} diff --git a/src/commit_evaluator/double_sorted_witness_machine.rs b/src/commit_evaluator/double_sorted_witness_machine.rs index a6d189cd6..e8b5fd946 100644 --- a/src/commit_evaluator/double_sorted_witness_machine.rs +++ b/src/commit_evaluator/double_sorted_witness_machine.rs @@ -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], right: &SelectedExpressions, - ) -> LookupResult { + ) -> Option { 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], + 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) + } +} diff --git a/src/commit_evaluator/eval_error.rs b/src/commit_evaluator/eval_error.rs index 69757e144..864f2d7a3 100644 --- a/src/commit_evaluator/eval_error.rs +++ b/src/commit_evaluator/eval_error.rs @@ -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), } @@ -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![]), diff --git a/src/commit_evaluator/evaluator.rs b/src/commit_evaluator/evaluator.rs index 49406a65a..38c0f8955 100644 --- a/src/commit_evaluator/evaluator.rs +++ b/src/commit_evaluator/evaluator.rs @@ -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>, query_callback: Option, + 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>, /// Values of the witness polynomials in the next row next: Vec>, + /// Bit constraints on the witness polynomials in the next row. + next_bit_constraints: Vec>, next_row: DegreeType, failure_reasons: Vec, 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>, query_callback: Option, ) -> 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 { + 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, 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>, +} + +impl<'a> BitConstraintSet for WitnessBitConstraintSet<'a> { + fn bit_constraint(&self, id: usize) -> Option { + 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> { diff --git a/src/commit_evaluator/fixed_lookup_machine.rs b/src/commit_evaluator/fixed_lookup_machine.rs index 6f76c86a4..67c437d30 100644 --- a/src/commit_evaluator/fixed_lookup_machine.rs +++ b/src/commit_evaluator/fixed_lookup_machine.rs @@ -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], right: &SelectedExpressions, - ) -> LookupResult { + ) -> Option { // 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> { + Default::default() + } +} + +impl FixedLookup { + fn process_plookup_internal( + &mut self, + fixed_data: &FixedData, + left: &[Result], + 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> { - 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() } - } + }) } } diff --git a/src/commit_evaluator/machine.rs b/src/commit_evaluator/machine.rs index 2d75ee9ed..30ea29a9a 100644 --- a/src/commit_evaluator/machine.rs +++ b/src/commit_evaluator/machine.rs @@ -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], right: &SelectedExpressions, - ) -> LookupResult; + ) -> Option; /// Returns the final values of the witness columns. fn witness_col_values( @@ -33,13 +37,3 @@ pub trait Machine { fixed_data: &FixedData, ) -> HashMap>; } - -pub type LookupResult = Result; - -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)>), -} diff --git a/src/commit_evaluator/mod.rs b/src/commit_evaluator/mod.rs index 091052abf..350491e21 100644 --- a/src/commit_evaluator/mod.rs +++ b/src/commit_evaluator/mod.rs @@ -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)> = 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, EvalError>; +/// Result of evaluating an expression / lookup. +/// New assignments or constraints for witness columns identified by an ID. +type EvalResult = Result, EvalError>; + +#[derive(Debug, Clone, PartialEq)] +pub enum Constraint { + Assignment(AbstractNumberType), + BitConstraint(BitConstraint), +} /// Data that is fixed for witness generation. pub struct FixedData<'a> { diff --git a/src/commit_evaluator/sorted_witness_machine.rs b/src/commit_evaluator/sorted_witness_machine.rs index baea6e03a..9ffe14975 100644 --- a/src/commit_evaluator/sorted_witness_machine.rs +++ b/src/commit_evaluator/sorted_witness_machine.rs @@ -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], right: &SelectedExpressions, - ) -> LookupResult { + ) -> Option { 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::>(); if rhs.iter().any(|e| e.is_none()) { - return Ok(LookupReturn::NotApplicable); + return None; } let rhs = rhs.iter().map(|x| x.unwrap()).collect::>(); + Some(self.process_plookup_internal(fixed_data, left, right, rhs)) + } + fn witness_col_values( + &mut self, + fixed_data: &FixedData, + ) -> HashMap> { + 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::>(); + 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], + 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> { - 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::>(); - col_values.resize(fixed_data.degree as usize, 0.into()); - result.insert(col_name.clone(), col_values); - } - - result + Ok(assignments) } } diff --git a/src/commit_evaluator/symbolic_evaluator.rs b/src/commit_evaluator/symbolic_evaluator.rs index 9b8e68a0b..33de52890 100644 --- a/src/commit_evaluator/symbolic_evaluator.rs +++ b/src/commit_evaluator/symbolic_evaluator.rs @@ -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::>(); + 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 { // 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() } } } diff --git a/src/commit_evaluator/util.rs b/src/commit_evaluator/util.rs index f9f080158..4cb24a3c9 100644 --- a/src/commit_evaluator/util.rs +++ b/src/commit_evaluator/util.rs @@ -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()) diff --git a/src/compiler.rs b/src/compiler.rs index a8977ccfa..9c99b05dd 100644 --- a/src/compiler.rs +++ b/src/compiler.rs @@ -54,6 +54,7 @@ pub fn compile_pil_ast( pub fn compile_asm( file_name: &str, inputs: Vec, + 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, + 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( diff --git a/src/number.rs b/src/number.rs index 055fd9c34..757c497b2 100644 --- a/src/number.rs +++ b/src/number.rs @@ -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}") } diff --git a/tests/bit_access.asm b/tests/bit_access.asm new file mode 100644 index 000000000..0ae15a93c --- /dev/null +++ b/tests/bit_access.asm @@ -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; diff --git a/tests/integration.rs b/tests/integration.rs index bf0823df3..f860f22aa 100644 --- a/tests/integration.rs +++ b/tests/integration.rs @@ -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 Option>) { let input_file = Path::new(&format!("./tests/{file_name}")) @@ -18,9 +18,10 @@ fn verify_pil(file_name: &str, query_callback: Option Option) { +fn verify_asm(file_name: &str, inputs: Vec, row_count: Option) { 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), + ); }