From 4beb28280c8aa3e7fbf797afc60bc94185cb0191 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 20 Oct 2023 17:26:07 +0200 Subject: [PATCH 1/2] Use global constraints in fixed lookup. --- compiler/tests/pil.rs | 5 +++ executor/src/witgen/global_constraints.rs | 12 +++++ .../witgen/machines/fixed_lookup_machine.rs | 45 ++++++++++++------- .../src/witgen/machines/machine_extractor.rs | 2 +- executor/src/witgen/processor.rs | 8 ++-- .../pil/conditional_fixed_constraints.pil | 31 +++++++++++++ 6 files changed, 83 insertions(+), 20 deletions(-) create mode 100644 test_data/pil/conditional_fixed_constraints.pil diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs index 9d0d013cd..a7c5befd8 100644 --- a/compiler/tests/pil.rs +++ b/compiler/tests/pil.rs @@ -239,3 +239,8 @@ fn test_fixed_columns() { fn test_witness_via_let() { verify_pil("witness_via_let.pil", None); } + +#[test] +fn conditional_fixed_constraints() { + verify_pil("conditional_fixed_constraints.pil", None); +} diff --git a/executor/src/witgen/global_constraints.rs b/executor/src/witgen/global_constraints.rs index 6d516b37c..2ef992c5b 100644 --- a/executor/src/witgen/global_constraints.rs +++ b/executor/src/witgen/global_constraints.rs @@ -41,6 +41,18 @@ pub struct GlobalConstraints { pub fixed_constraints: FixedColumnMap>>, } +impl<'a, T: FieldElement> RangeConstraintSet<&PolynomialReference, T> for GlobalConstraints { + fn range_constraint(&self, id: &PolynomialReference) -> Option> { + assert!(!id.next); + let poly_id = id.poly_id.unwrap(); + match poly_id.ptype { + PolynomialType::Constant => self.fixed_constraints[&poly_id].clone(), + PolynomialType::Committed => self.witness_constraints[&poly_id].clone(), + PolynomialType::Intermediate => None, + } + } +} + /// Determines global constraints on witness and fixed columns. /// Removes identities that only serve to create range constraints from /// the identities vector and returns the remaining identities. diff --git a/executor/src/witgen/machines/fixed_lookup_machine.rs b/executor/src/witgen/machines/fixed_lookup_machine.rs index fc06f9fad..0e5f10964 100644 --- a/executor/src/witgen/machines/fixed_lookup_machine.rs +++ b/executor/src/witgen/machines/fixed_lookup_machine.rs @@ -2,12 +2,13 @@ use std::collections::{BTreeMap, HashMap, HashSet}; use std::mem; use std::num::NonZeroUsize; -use ast::analyzed::{Expression, Identity, IdentityKind, PolyID, PolynomialReference}; +use ast::analyzed::{Expression, IdentityKind, PolyID, PolynomialReference}; use ast::parsed::SelectedExpressions; use itertools::Itertools; use number::FieldElement; use crate::witgen::affine_expression::AffineExpression; +use crate::witgen::global_constraints::{GlobalConstraints, SimpleRangeConstraintSet}; use crate::witgen::util::try_to_simple_poly_ref; use crate::witgen::{EvalError, EvalValue, IncompleteCause}; use crate::witgen::{EvalResult, FixedData}; @@ -155,21 +156,16 @@ impl IndexedColumns { } /// Machine to perform a lookup in fixed columns only. -#[derive(Default)] -pub struct FixedLookup { +pub struct FixedLookup { + global_constraints: GlobalConstraints, indices: IndexedColumns, } impl FixedLookup { - pub fn try_new( - _fixed_data: &FixedData, - identities: &[&Identity>], - witness_names: &HashSet<&str>, - ) -> Option { - if identities.is_empty() && witness_names.is_empty() { - Some(Default::default()) - } else { - None + pub fn new(global_constraints: GlobalConstraints) -> Self { + Self { + global_constraints, + indices: Default::default(), } } @@ -188,6 +184,8 @@ impl FixedLookup { return None; } + println!("Processing {{ {} }} in {}", left.iter().format(", "), right); + // get the values of the fixed columns let right = right .expressions @@ -202,18 +200,22 @@ impl FixedLookup { &mut self, fixed_data: &FixedData, left: &[AffineExpression<&'b PolynomialReference, T>], - right: Vec<&PolynomialReference>, + right: Vec<&'b PolynomialReference>, ) -> EvalResult<'b, T> { // split the fixed columns depending on whether their associated lookup variable is constant or not. Preserve the value of the constant arguments. // {1, 2, x} in {A, B, C} -> [[(A, 1), (B, 2)], [C, x]] + if left.len() == 1 && !left.first().unwrap().is_constant() { + // Lookup of the form "c { X } in { B }". Might be a conditional range check. + return self.process_range_check(left.first().unwrap(), right.first().unwrap()); + } + let mut input_assignment = vec![]; let mut output_columns = vec![]; let mut output_expressions = vec![]; left.iter().zip(right).for_each(|(l, r)| { - let left_value = l.constant_value(); - if let Some(value) = left_value { + if let Some(value) = l.constant_value() { input_assignment.push((r, value)); } else { output_columns.push(r.poly_id()); @@ -274,4 +276,17 @@ impl FixedLookup { Ok(result) } + + fn process_range_check<'b>( + &self, + lhs: &AffineExpression<&'b PolynomialReference, T>, + rhs: &'b PolynomialReference, + ) -> EvalResult<'b, T> { + let equation = lhs.clone() - AffineExpression::from_variable_id(rhs); + // TODO this is kind of unusual because we use symbolic fixed columns. + // we should better filter out the fixed column from the result. + let r = equation.solve_with_range_constraints(&self.global_constraints); + println!("{r:?}"); + r + } } diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs index c2b6f39e4..8860fd419 100644 --- a/executor/src/witgen/machines/machine_extractor.rs +++ b/executor/src/witgen/machines/machine_extractor.rs @@ -29,7 +29,7 @@ pub fn split_out_machines<'a, T: FieldElement>( identities: Vec<&'a Identity>>, global_range_constraints: &GlobalConstraints, ) -> ExtractionOutput<'a, T> { - let fixed_lookup = FixedLookup::try_new(fixed, &[], &Default::default()).unwrap(); + let fixed_lookup = FixedLookup::new(global_range_constraints.clone()); let mut machines: Vec> = vec![]; diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 16bea4be9..a34ceea86 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -334,16 +334,16 @@ mod tests { let (constants, degree) = generate(&analyzed); let fixed_data = FixedData::new(&analyzed, degree, &constants, vec![]); - // No submachines - let mut fixed_lookup = FixedLookup::default(); - let mut machines = vec![]; - // No global range constraints let global_range_constraints = GlobalConstraints { witness_constraints: fixed_data.witness_map_with(None), fixed_constraints: FixedColumnMap::new(None, fixed_data.fixed_cols.len()), }; + // No submachines + let mut fixed_lookup = FixedLookup::new(global_range_constraints.clone()); + let mut machines = vec![]; + let row_factory = RowFactory::new(&fixed_data, global_range_constraints); let data = (0..fixed_data.degree) .map(|i| row_factory.fresh_row(i)) diff --git a/test_data/pil/conditional_fixed_constraints.pil b/test_data/pil/conditional_fixed_constraints.pil new file mode 100644 index 000000000..5daa4f425 --- /dev/null +++ b/test_data/pil/conditional_fixed_constraints.pil @@ -0,0 +1,31 @@ +constant %N = 1024; + +namespace Main(%N); + let first = |i| match i { 0 => 1, _ => 0 }; + let Y; + let Z; + let bytes = |i| i % 256; + let wrap_bit; + wrap_bit * (1 - wrap_bit) = 0; + let X_b4; + let X_b3; + let X_b2; + let X_b1; + { X_b4 } in { bytes }; + { X_b3 } in { bytes }; + { X_b2 } in { bytes }; + { X_b1 } in { bytes }; + + let cond; + + cond { Z } in { two_bits }; + let two_bits = |i| i % 4; + + 0 = cond * (Y - wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z); + let six_bits = |i| i % 2**6; + cond { X_b1 } in { six_bits }; + + let odd = |i| i % 2; + cond = odd; + + Y' = (1 - first') * (Y + 1); From c1d6d04b4e888240d28e810ccc2cccd6a9a5dc45 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Wed, 25 Oct 2023 15:31:56 +0000 Subject: [PATCH 2/2] Fix test by giving FixedLookup access to RowPair --- executor/src/witgen/global_constraints.rs | 2 +- executor/src/witgen/identity_processor.rs | 1 + .../witgen/machines/fixed_lookup_machine.rs | 68 +++++++++++++++---- .../pil/conditional_fixed_constraints.pil | 2 +- 4 files changed, 56 insertions(+), 17 deletions(-) diff --git a/executor/src/witgen/global_constraints.rs b/executor/src/witgen/global_constraints.rs index 2ef992c5b..fed9454f4 100644 --- a/executor/src/witgen/global_constraints.rs +++ b/executor/src/witgen/global_constraints.rs @@ -41,7 +41,7 @@ pub struct GlobalConstraints { pub fixed_constraints: FixedColumnMap>>, } -impl<'a, T: FieldElement> RangeConstraintSet<&PolynomialReference, T> for GlobalConstraints { +impl RangeConstraintSet<&PolynomialReference, T> for GlobalConstraints { fn range_constraint(&self, id: &PolynomialReference) -> Option> { assert!(!id.next); let poly_id = id.poly_id.unwrap(); diff --git a/executor/src/witgen/identity_processor.rs b/executor/src/witgen/identity_processor.rs index beaa19efd..a6277505c 100644 --- a/executor/src/witgen/identity_processor.rs +++ b/executor/src/witgen/identity_processor.rs @@ -158,6 +158,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> IdentityProcessor<'a, 'b, // query the fixed lookup "machine" if let Some(result) = self.mutable_state.fixed_lookup.process_plookup( self.fixed_data, + rows, identity.kind, &left, &identity.right, diff --git a/executor/src/witgen/machines/fixed_lookup_machine.rs b/executor/src/witgen/machines/fixed_lookup_machine.rs index 0e5f10964..eb2c593c8 100644 --- a/executor/src/witgen/machines/fixed_lookup_machine.rs +++ b/executor/src/witgen/machines/fixed_lookup_machine.rs @@ -2,13 +2,15 @@ use std::collections::{BTreeMap, HashMap, HashSet}; use std::mem; use std::num::NonZeroUsize; -use ast::analyzed::{Expression, IdentityKind, PolyID, PolynomialReference}; +use ast::analyzed::{Expression, IdentityKind, PolyID, PolynomialReference, PolynomialType}; use ast::parsed::SelectedExpressions; use itertools::Itertools; use number::FieldElement; use crate::witgen::affine_expression::AffineExpression; -use crate::witgen::global_constraints::{GlobalConstraints, SimpleRangeConstraintSet}; +use crate::witgen::global_constraints::{GlobalConstraints, RangeConstraintSet}; +use crate::witgen::range_constraints::RangeConstraint; +use crate::witgen::rows::RowPair; use crate::witgen::util::try_to_simple_poly_ref; use crate::witgen::{EvalError, EvalValue, IncompleteCause}; use crate::witgen::{EvalResult, FixedData}; @@ -172,6 +174,7 @@ impl FixedLookup { pub fn process_plookup<'b>( &mut self, fixed_data: &FixedData, + rows: &RowPair<'_, '_, T>, kind: IdentityKind, left: &[AffineExpression<&'b PolynomialReference, T>], right: &'b SelectedExpressions>, @@ -184,8 +187,6 @@ impl FixedLookup { return None; } - println!("Processing {{ {} }} in {}", left.iter().format(", "), right); - // get the values of the fixed columns let right = right .expressions @@ -193,23 +194,27 @@ impl FixedLookup { .map(try_to_simple_poly_ref) .collect::>>()?; - Some(self.process_plookup_internal(fixed_data, left, right)) + Some(self.process_plookup_internal(fixed_data, rows, left, right)) } fn process_plookup_internal<'b>( &mut self, fixed_data: &FixedData, + rows: &RowPair<'_, '_, T>, left: &[AffineExpression<&'b PolynomialReference, T>], right: Vec<&'b PolynomialReference>, ) -> EvalResult<'b, T> { + if left.len() == 1 + && !left.first().unwrap().is_constant() + && right.first().unwrap().poly_id().ptype == PolynomialType::Constant + { + // Lookup of the form "c { X } in { B }". Might be a conditional range check. + return self.process_range_check(rows, left.first().unwrap(), right.first().unwrap()); + } + // split the fixed columns depending on whether their associated lookup variable is constant or not. Preserve the value of the constant arguments. // {1, 2, x} in {A, B, C} -> [[(A, 1), (B, 2)], [C, x]] - if left.len() == 1 && !left.first().unwrap().is_constant() { - // Lookup of the form "c { X } in { B }". Might be a conditional range check. - return self.process_range_check(left.first().unwrap(), right.first().unwrap()); - } - let mut input_assignment = vec![]; let mut output_columns = vec![]; let mut output_expressions = vec![]; @@ -279,14 +284,47 @@ impl FixedLookup { fn process_range_check<'b>( &self, + rows: &RowPair<'_, '_, T>, lhs: &AffineExpression<&'b PolynomialReference, T>, rhs: &'b PolynomialReference, ) -> EvalResult<'b, T> { + // Use AffineExpression::solve_with_range_constraints to transfer range constraints + // from the rhs to the lhs. let equation = lhs.clone() - AffineExpression::from_variable_id(rhs); - // TODO this is kind of unusual because we use symbolic fixed columns. - // we should better filter out the fixed column from the result. - let r = equation.solve_with_range_constraints(&self.global_constraints); - println!("{r:?}"); - r + let range_constraints = UnifiedRangeConstraints { + witness_constraints: rows, + global_constraints: &self.global_constraints, + }; + let updates = equation.solve_with_range_constraints(&range_constraints)?; + + // Filter out any updates to the fixed columns + Ok(EvalValue::incomplete_with_constraints( + updates + .constraints + .into_iter() + .filter(|(poly, _)| poly.poly_id().ptype == PolynomialType::Committed), + IncompleteCause::NotConcrete, + )) + } +} + +/// Combines witness constraints on a concrete row with global range constraints +/// (used for fixed columns). +/// This is useful in order to transfer range constraints from fixed columns to +/// witness columns (see [FixedLookup::process_range_check]). +pub struct UnifiedRangeConstraints<'a, T: FieldElement> { + witness_constraints: &'a RowPair<'a, 'a, T>, + global_constraints: &'a GlobalConstraints, +} + +impl RangeConstraintSet<&PolynomialReference, T> + for UnifiedRangeConstraints<'_, T> +{ + fn range_constraint(&self, poly: &PolynomialReference) -> Option> { + match poly.poly_id().ptype { + PolynomialType::Committed => self.witness_constraints.range_constraint(poly), + PolynomialType::Constant => self.global_constraints.range_constraint(poly), + PolynomialType::Intermediate => unimplemented!(), + } } } diff --git a/test_data/pil/conditional_fixed_constraints.pil b/test_data/pil/conditional_fixed_constraints.pil index 5daa4f425..f6003101b 100644 --- a/test_data/pil/conditional_fixed_constraints.pil +++ b/test_data/pil/conditional_fixed_constraints.pil @@ -21,7 +21,7 @@ namespace Main(%N); cond { Z } in { two_bits }; let two_bits = |i| i % 4; - 0 = cond * (Y - wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z); + 0 = cond * (Y - (wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z)); let six_bits = |i| i % 2**6; cond { X_b1 } in { six_bits };