From 073572aafad3fade804e2832f8a128fcbf2d40cc Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Mon, 4 Nov 2024 17:08:50 +0100 Subject: [PATCH] Rust phantom constr (#1945) Following #1934, adds these new variants to the rust side. A follow up PR by @georgwiese will actually compute multiplicities in witgen. --------- Co-authored-by: Georg Wiese --- ast/src/analyzed/display.rs | 42 ++++++ ast/src/analyzed/mod.rs | 91 +++++++++--- backend-utils/src/lib.rs | 10 +- .../json_exporter/expression_counter.rs | 2 + backend/src/estark/json_exporter/mod.rs | 3 + backend/src/halo2/circuit_builder.rs | 3 + executor/src/witgen/global_constraints.rs | 17 ++- executor/src/witgen/identity_processor.rs | 7 +- .../witgen/machines/fixed_lookup_machine.rs | 21 ++- .../src/witgen/machines/machine_extractor.rs | 16 ++- executor/src/witgen/machines/mod.rs | 10 ++ .../witgen/machines/sorted_witness_machine.rs | 21 +-- executor/src/witgen/vm_processor.rs | 17 ++- pil-analyzer/src/condenser.rs | 61 ++++++--- pilopt/src/lib.rs | 129 ++++++++++++------ pipeline/tests/powdr_std.rs | 36 +---- plonky3/src/circuit_builder.rs | 3 + std/protocols/lookup.asm | 8 +- test_data/std/lookup_via_challenges.asm | 31 ++--- test_data/std/lookup_via_challenges_ext.asm | 26 ---- .../std/lookup_via_challenges_ext_simple.asm | 19 --- ...lookup_via_challenges_range_constraint.asm | 19 +++ test_data/std/multiplicities.asm | 28 ---- 23 files changed, 386 insertions(+), 234 deletions(-) delete mode 100644 test_data/std/lookup_via_challenges_ext.asm delete mode 100644 test_data/std/lookup_via_challenges_ext_simple.asm create mode 100644 test_data/std/lookup_via_challenges_range_constraint.asm delete mode 100644 test_data/std/multiplicities.asm diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index b26df831f..0e9dfca33 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -350,12 +350,54 @@ impl Display for LookupIdentity { } } +fn format_selector(selector: &AlgebraicExpression) -> String { + match selector.to_string().as_str() { + "1" => "Option::None".to_string(), + s => format!("Option::Some({s})"), + } +} + +impl Display for PhantomLookupIdentity { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + write!( + f, + "Constr::PhantomLookup(({}, {}), [{}], {});", + format_selector(&self.left.selector), + format_selector(&self.right.selector), + self.left + .expressions + .iter() + .zip_eq(&self.right.expressions) + .map(|(left, right)| format!("({left}, {right})")) + .format(", "), + self.multiplicity + ) + } +} + impl Display for PermutationIdentity { fn fmt(&self, f: &mut Formatter<'_>) -> Result { write!(f, "{} is {};", self.left, self.right) } } +impl Display for PhantomPermutationIdentity { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + write!( + f, + "Constr::PhantomPermutation(({}, {}), [{}]);", + format_selector(&self.left.selector), + format_selector(&self.right.selector), + self.left + .expressions + .iter() + .zip_eq(&self.right.expressions) + .map(|(left, right)| format!("({left}, {right})")) + .format(", ") + ) + } +} + impl Display for ConnectIdentity { fn fmt(&self, f: &mut Formatter<'_>) -> Result { write!( diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index 066afe691..e7aa1d2b7 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -927,6 +927,39 @@ impl Children> for LookupIdentity { } } +/// A witness generation helper for a lookup identity. +/// +/// This identity is used as a replactement for a lookup identity which has been turned into challenge-based polynomial identities. +/// This is ignored by the backend. +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)] +pub struct PhantomLookupIdentity { + // The ID is globally unique among identities. + pub id: u64, + pub source: SourceRef, + pub left: SelectedExpressions, + pub right: SelectedExpressions, + pub multiplicity: AlgebraicExpression, +} + +impl Children> for PhantomLookupIdentity { + fn children_mut(&mut self) -> Box> + '_> { + Box::new( + self.left + .children_mut() + .chain(self.right.children_mut()) + .chain(self.multiplicity.children_mut()), + ) + } + fn children(&self) -> Box> + '_> { + Box::new( + self.left + .children() + .chain(self.right.children()) + .chain(self.multiplicity.children()), + ) + } +} + #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)] pub struct PermutationIdentity { // The ID is globally unique among identitites. @@ -945,6 +978,28 @@ impl Children> for PermutationIdentity { } } +/// A witness generation helper for a permutation identity. +/// +/// This identity is used as a replactement for a permutation identity which has been turned into challenge-based polynomial identities. +/// This is ignored by the backend. +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)] +pub struct PhantomPermutationIdentity { + // The ID is globally unique among identitites. + pub id: u64, + pub source: SourceRef, + pub left: SelectedExpressions, + pub right: SelectedExpressions, +} + +impl Children> for PhantomPermutationIdentity { + fn children_mut(&mut self) -> Box> + '_> { + Box::new(self.left.children_mut().chain(self.right.children_mut())) + } + fn children(&self) -> Box> + '_> { + Box::new(self.left.children().chain(self.right.children())) + } +} + #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)] pub struct ConnectIdentity { // The ID is globally unique among identitites. @@ -963,22 +1018,6 @@ impl Children> for ConnectIdentity { } } -impl ConnectIdentity { - pub fn new( - id: u64, - source: SourceRef, - left: Vec>, - right: Vec>, - ) -> Self { - Self { - id, - source, - left, - right, - } - } -} - #[derive( Debug, PartialEq, @@ -994,7 +1033,9 @@ impl ConnectIdentity { pub enum Identity { Polynomial(PolynomialIdentity), Lookup(LookupIdentity), + PhantomLookup(PhantomLookupIdentity), Permutation(PermutationIdentity), + PhantomPermutation(PhantomPermutationIdentity), Connect(ConnectIdentity), } @@ -1011,7 +1052,9 @@ impl Identity { match self { Identity::Polynomial(i) => i.id, Identity::Lookup(i) => i.id, + Identity::PhantomLookup(i) => i.id, Identity::Permutation(i) => i.id, + Identity::PhantomPermutation(i) => i.id, Identity::Connect(i) => i.id, } } @@ -1019,8 +1062,10 @@ impl Identity { pub fn kind(&self) -> IdentityKind { match self { Identity::Polynomial(_) => IdentityKind::Polynomial, - Identity::Lookup(_) => IdentityKind::Plookup, + Identity::Lookup(_) => IdentityKind::Lookup, + Identity::PhantomLookup(_) => IdentityKind::PhantomLookup, Identity::Permutation(_) => IdentityKind::Permutation, + Identity::PhantomPermutation(_) => IdentityKind::PhantomPermutation, Identity::Connect(_) => IdentityKind::Connect, } } @@ -1031,7 +1076,9 @@ impl SourceReference for Identity { match self { Identity::Polynomial(i) => &i.source, Identity::Lookup(i) => &i.source, + Identity::PhantomLookup(i) => &i.source, Identity::Permutation(i) => &i.source, + Identity::PhantomPermutation(i) => &i.source, Identity::Connect(i) => &i.source, } } @@ -1040,7 +1087,9 @@ impl SourceReference for Identity { match self { Identity::Polynomial(i) => &mut i.source, Identity::Lookup(i) => &mut i.source, + Identity::PhantomLookup(i) => &mut i.source, Identity::Permutation(i) => &mut i.source, + Identity::PhantomPermutation(i) => &mut i.source, Identity::Connect(i) => &mut i.source, } } @@ -1051,7 +1100,9 @@ impl Children> for Identity { match self { Identity::Polynomial(i) => i.children_mut(), Identity::Lookup(i) => i.children_mut(), + Identity::PhantomLookup(i) => i.children_mut(), Identity::Permutation(i) => i.children_mut(), + Identity::PhantomPermutation(i) => i.children_mut(), Identity::Connect(i) => i.children_mut(), } } @@ -1060,7 +1111,9 @@ impl Children> for Identity { match self { Identity::Polynomial(i) => i.children(), Identity::Lookup(i) => i.children(), + Identity::PhantomLookup(i) => i.children(), Identity::Permutation(i) => i.children(), + Identity::PhantomPermutation(i) => i.children(), Identity::Connect(i) => i.children(), } } @@ -1071,8 +1124,10 @@ impl Children> for Identity { )] pub enum IdentityKind { Polynomial, - Plookup, + Lookup, + PhantomLookup, Permutation, + PhantomPermutation, Connect, } diff --git a/backend-utils/src/lib.rs b/backend-utils/src/lib.rs index 15a49644d..1fc434c26 100644 --- a/backend-utils/src/lib.rs +++ b/backend-utils/src/lib.rs @@ -9,7 +9,7 @@ use itertools::Itertools; use powdr_ast::{ analyzed::{ AlgebraicExpression, Analyzed, Identity, LookupIdentity, PermutationIdentity, - StatementIdentifier, Symbol, SymbolKind, + PhantomLookupIdentity, PhantomPermutationIdentity, StatementIdentifier, Symbol, SymbolKind, }, parsed::{ asm::{AbsoluteSymbolPath, SymbolPath}, @@ -193,7 +193,13 @@ fn split_by_namespace( .then(|| (current_namespace.clone(), statement)), _ => match identity { Identity::Lookup(LookupIdentity { left, right, .. }) - | Identity::Permutation(PermutationIdentity { left, right, .. }) => { + | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) + | Identity::Permutation(PermutationIdentity { left, right, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { + left, + right, + .. + }) => { assert_eq!( referenced_namespaces(left).len(), 1, diff --git a/backend/src/estark/json_exporter/expression_counter.rs b/backend/src/estark/json_exporter/expression_counter.rs index 93e13f9e7..27c022e9e 100644 --- a/backend/src/estark/json_exporter/expression_counter.rs +++ b/backend/src/estark/json_exporter/expression_counter.rs @@ -59,6 +59,8 @@ impl ExpressionCounter for Identity { Identity::Connect(connect_identity) => { connect_identity.left.len() + connect_identity.right.len() } + // phantom identities are not relevant in this context + Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => 0, } } } diff --git a/backend/src/estark/json_exporter/mod.rs b/backend/src/estark/json_exporter/mod.rs index f43a4ce76..67b70e3d0 100644 --- a/backend/src/estark/json_exporter/mod.rs +++ b/backend/src/estark/json_exporter/mod.rs @@ -135,6 +135,9 @@ pub fn export(analyzed: &Analyzed) -> PIL { line, }); } + Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => { + // These are not relevant for the PIL + } } } StatementIdentifier::ProverFunction(_) diff --git a/backend/src/halo2/circuit_builder.rs b/backend/src/halo2/circuit_builder.rs index 2e1e74b79..b0a074698 100644 --- a/backend/src/halo2/circuit_builder.rs +++ b/backend/src/halo2/circuit_builder.rs @@ -320,6 +320,9 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi .collect() }); } + Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => { + // Phantom identities are only used in witness generation + } } } diff --git a/executor/src/witgen/global_constraints.rs b/executor/src/witgen/global_constraints.rs index 3fa46f2e9..3d8461ce5 100644 --- a/executor/src/witgen/global_constraints.rs +++ b/executor/src/witgen/global_constraints.rs @@ -3,9 +3,10 @@ use std::marker::PhantomData; use num_traits::Zero; +use num_traits::One; use powdr_ast::analyzed::{ AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression as Expression, - AlgebraicReference, LookupIdentity, PermutationIdentity, PolyID, PolynomialType, + AlgebraicReference, LookupIdentity, PhantomLookupIdentity, PolyID, PolynomialType, }; use powdr_number::FieldElement; @@ -237,10 +238,11 @@ fn propagate_constraints( } } Identity::Lookup(LookupIdentity { left, right, .. }) - | Identity::Permutation(PermutationIdentity { left, right, .. }) => { - if left.selector != T::one().into() || right.selector != T::one().into() { + | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) => { + if !left.selector.is_one() || !right.selector.is_one() { return (known_constraints, false); } + // We learn range constraints from both lookups and permutations for (left, right) in left.expressions.iter().zip(right.expressions.iter()) { if let (Some(left), Some(right)) = (try_to_simple_poly(left), try_to_simple_poly(right)) @@ -253,7 +255,11 @@ fn propagate_constraints( } } } - if right.expressions.len() == 1 { + + // We only remove lookups, since permutations hold more information than just range constraints. + if right.expressions.len() == 1 + && matches!(identity, Identity::Lookup(..) | Identity::PhantomLookup(..)) + { // We can only remove the lookup if the RHS is a fixed polynomial that // provides all values in the span. if let Some(name) = try_to_simple_poly(&right.expressions[0]) { @@ -268,6 +274,9 @@ fn propagate_constraints( Identity::Connect(..) => { // we do not handle connect identities yet, so we do nothing } + Identity::Permutation(..) | Identity::PhantomPermutation(..) => { + // permutation identities are stronger than just range constraints, so we do nothing + } } (known_constraints, remove) diff --git a/executor/src/witgen/identity_processor.rs b/executor/src/witgen/identity_processor.rs index 1332430e0..e5a76ac83 100644 --- a/executor/src/witgen/identity_processor.rs +++ b/executor/src/witgen/identity_processor.rs @@ -5,7 +5,8 @@ use std::{ use lazy_static::lazy_static; use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, LookupIdentity, PermutationIdentity, PolynomialIdentity, + AlgebraicExpression as Expression, LookupIdentity, PermutationIdentity, PhantomLookupIdentity, + PhantomPermutationIdentity, PolynomialIdentity, }; use powdr_number::FieldElement; @@ -152,7 +153,9 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> IdentityProcessor<'a, 'b, let result = match identity { Identity::Polynomial(identity) => self.process_polynomial_identity(identity, rows), Identity::Lookup(LookupIdentity { left, id, .. }) - | Identity::Permutation(PermutationIdentity { left, id, .. }) => { + | Identity::Permutation(PermutationIdentity { left, id, .. }) + | Identity::PhantomLookup(PhantomLookupIdentity { left, id, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { left, id, .. }) => { self.process_lookup_or_permutation(*id, left, rows) } Identity::Connect(..) => { diff --git a/executor/src/witgen/machines/fixed_lookup_machine.rs b/executor/src/witgen/machines/fixed_lookup_machine.rs index 3211dac39..f98838247 100644 --- a/executor/src/witgen/machines/fixed_lookup_machine.rs +++ b/executor/src/witgen/machines/fixed_lookup_machine.rs @@ -6,7 +6,9 @@ use std::num::NonZeroUsize; use std::str::FromStr; use itertools::Itertools; -use powdr_ast::analyzed::{AlgebraicReference, PolyID, PolynomialType}; +use powdr_ast::analyzed::{ + AlgebraicReference, LookupIdentity, PhantomLookupIdentity, PolyID, PolynomialType, +}; use powdr_ast::parsed::asm::SymbolPath; use powdr_number::{DegreeType, FieldElement}; @@ -199,18 +201,23 @@ impl<'a, T: FieldElement> FixedLookup<'a, T> { let connections = all_identities .into_iter() .filter_map(|i| match i { - Identity::Lookup(i) => (i.right.selector.is_one() - && i.right.expressions.iter().all(|e| { + Identity::Lookup(LookupIdentity { + id, left, right, .. + }) + | Identity::PhantomLookup(PhantomLookupIdentity { + id, left, right, .. + }) => (right.selector.is_one() + && right.expressions.iter().all(|e| { try_to_simple_poly_ref(e) .map(|poly| poly.poly_id.ptype == PolynomialType::Constant) .unwrap_or(false) }) - && !i.right.expressions.is_empty()) + && !right.expressions.is_empty()) .then_some(( - i.id, + *id, Connection { - left: &i.left, - right: &i.right, + left, + right, kind: ConnectionKind::Lookup, }, )), diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs index 9e53f190d..05ca9407e 100644 --- a/executor/src/witgen/machines/machine_extractor.rs +++ b/executor/src/witgen/machines/machine_extractor.rs @@ -3,6 +3,8 @@ use std::collections::{BTreeMap, BTreeSet, HashSet}; use itertools::Itertools; use powdr_ast::analyzed::LookupIdentity; use powdr_ast::analyzed::PermutationIdentity; +use powdr_ast::analyzed::PhantomLookupIdentity; +use powdr_ast::analyzed::PhantomPermutationIdentity; use super::block_machine::BlockMachine; use super::double_sorted_witness_machine_16::DoubleSortedWitnesses16; @@ -66,7 +68,9 @@ pub fn split_out_machines<'a, T: FieldElement>( // Extract all witness columns in the RHS of the lookup. let lookup_witnesses = match id { Identity::Lookup(LookupIdentity { right, .. }) - | Identity::Permutation(PermutationIdentity { right, .. }) => { + | Identity::PhantomLookup(PhantomLookupIdentity { right, .. }) + | Identity::Permutation(PermutationIdentity { right, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { right, .. }) => { &refs_in_selected_expressions(right) & (&remaining_witnesses) } _ => Default::default(), @@ -344,7 +348,11 @@ fn all_row_connected_witnesses( } } Identity::Lookup(LookupIdentity { left, right, .. }) - | Identity::Permutation(PermutationIdentity { left, right, .. }) => { + | Identity::Permutation(PermutationIdentity { left, right, .. }) + | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { + left, right, .. + }) => { // If we already have witnesses on the LHS, include the LHS, // and vice-versa, but not across the "sides". let in_lhs = &refs_in_selected_expressions(left) & all_witnesses; @@ -378,7 +386,9 @@ fn refs_in_selected_expressions(sel_expr: &SelectedExpressions) -> HashSet fn refs_in_identity_left(identity: &Identity) -> HashSet { match identity { Identity::Lookup(LookupIdentity { left, .. }) - | Identity::Permutation(PermutationIdentity { left, .. }) => { + | Identity::PhantomLookup(PhantomLookupIdentity { left, .. }) + | Identity::Permutation(PermutationIdentity { left, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { left, .. }) => { refs_in_selected_expressions(left) } Identity::Polynomial(i) => refs_in_expression(&i.expression).collect(), diff --git a/executor/src/witgen/machines/mod.rs b/executor/src/witgen/machines/mod.rs index b7f54efc6..10cf0c19c 100644 --- a/executor/src/witgen/machines/mod.rs +++ b/executor/src/witgen/machines/mod.rs @@ -186,11 +186,21 @@ impl<'a, T> TryFrom<&'a Identity> for Connection<'a, T> { right: &i.right, kind: ConnectionKind::Lookup, }), + Identity::PhantomLookup(i) => Ok(Connection { + left: &i.left, + right: &i.right, + kind: ConnectionKind::Lookup, + }), Identity::Permutation(i) => Ok(Connection { left: &i.left, right: &i.right, kind: ConnectionKind::Permutation, }), + Identity::PhantomPermutation(i) => Ok(Connection { + left: &i.left, + right: &i.right, + kind: ConnectionKind::Permutation, + }), _ => Err(identity), } } diff --git a/executor/src/witgen/machines/sorted_witness_machine.rs b/executor/src/witgen/machines/sorted_witness_machine.rs index 3cebbc6bc..ec1eca502 100644 --- a/executor/src/witgen/machines/sorted_witness_machine.rs +++ b/executor/src/witgen/machines/sorted_witness_machine.rs @@ -13,7 +13,10 @@ use crate::witgen::{EvalValue, IncompleteCause, MutableState, QueryCallback}; use crate::Identity; use itertools::Itertools; use num_traits::One; -use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, PolyID}; +use powdr_ast::analyzed::{ + AlgebraicExpression as Expression, AlgebraicReference, LookupIdentity, PhantomLookupIdentity, + PolyID, +}; use powdr_number::{DegreeType, FieldElement}; /// A machine that can support a lookup in a set of columns that are sorted @@ -109,22 +112,22 @@ fn check_identity( degree: DegreeType, ) -> Option { // Looking for a lookup - let id = if let Identity::Lookup(id) = id { - id - } else { - return None; + let (left, right) = match id { + Identity::Lookup(LookupIdentity { left, right, .. }) + | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) => (left, right), + _ => return None, }; // Looking for NOTLAST $ [ A' - A ] in [ POSITIVE ] - if !id.right.selector.is_one() || id.left.expressions.len() != 1 { + if !right.selector.is_one() || left.expressions.len() != 1 { return None; } // Check for A' - A in the LHS - let key_column = check_constraint(id.left.expressions.first().unwrap())?; + let key_column = check_constraint(left.expressions.first().unwrap())?; - let not_last = &id.left.selector; - let positive = id.right.expressions.first().unwrap(); + let not_last = &left.selector; + let positive = right.expressions.first().unwrap(); // TODO this could be rather slow. We should check the code for identity instead // of evaluating it. diff --git a/executor/src/witgen/vm_processor.rs b/executor/src/witgen/vm_processor.rs index 8d5620ae1..b6f993825 100644 --- a/executor/src/witgen/vm_processor.rs +++ b/executor/src/witgen/vm_processor.rs @@ -1,6 +1,6 @@ use indicatif::{ProgressBar, ProgressStyle}; use itertools::Itertools; -use powdr_ast::analyzed::DegreeRange; +use powdr_ast::analyzed::{DegreeRange, LookupIdentity, PhantomLookupIdentity}; use powdr_ast::indent; use powdr_number::{DegreeType, FieldElement}; use std::cmp::max; @@ -355,10 +355,13 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T .iter_mut() .enumerate() .filter_map(|(index, (ident, _))| match ident { - Identity::Lookup(i) => Some((index, i)), + Identity::Lookup(LookupIdentity { left, .. }) + | Identity::PhantomLookup(PhantomLookupIdentity { left, .. }) => { + Some((index, left)) + } _ => None, }) - .max_by_key(|(_, ident)| ident.left.expressions.len()) + .max_by_key(|(_, left)| left.expressions.len()) .map(|(i, _)| i); loop { let mut progress = false; @@ -447,7 +450,13 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T return Ok(None); } - let is_machine_call = matches!(identity, Identity::Lookup(..) | Identity::Permutation(..)); + let is_machine_call = matches!( + identity, + Identity::Lookup(..) + | Identity::Permutation(..) + | Identity::PhantomLookup(..) + | Identity::PhantomPermutation(..) + ); if is_machine_call && unknown_strategy == UnknownStrategy::Zero { // The fact that we got to the point where we assume 0 for unknown cells, but this identity // is still not complete, means that either the inputs or the machine is under-constrained. diff --git a/pil-analyzer/src/condenser.rs b/pil-analyzer/src/condenser.rs index 8898357cd..0b3afe19f 100644 --- a/pil-analyzer/src/condenser.rs +++ b/pil-analyzer/src/condenser.rs @@ -15,9 +15,10 @@ use powdr_ast::{ analyzed::{ self, AlgebraicBinaryOperation, AlgebraicExpression, AlgebraicReference, AlgebraicUnaryOperation, Analyzed, Challenge, ConnectIdentity, DegreeRange, Expression, - FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PolyID, - PolynomialIdentity, PolynomialReference, PolynomialType, PublicDeclaration, Reference, - SelectedExpressions, SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind, + FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, + PhantomLookupIdentity, PhantomPermutationIdentity, PolyID, PolynomialIdentity, + PolynomialReference, PolynomialType, PublicDeclaration, Reference, SelectedExpressions, + SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind, }, parsed::{ self, @@ -678,8 +679,12 @@ fn to_constraint( } .into() } - "Lookup" | "Permutation" => { - assert_eq!(fields.len(), 2); + "Lookup" | "Permutation" | "PhantomLookup" | "PhantomPermutation" => { + if variant == &"PhantomLookup" { + assert_eq!(fields.len(), 3); + } else { + assert_eq!(fields.len(), 2); + } let (sel_from, sel_to) = if let Value::Tuple(t) = fields[0].as_ref() { assert_eq!(t.len(), 2); @@ -703,22 +708,44 @@ fn to_constraint( unreachable!() }; - if variant == &"Lookup" { - LookupIdentity { - id: counters.dispense_identity_id(), + let id = counters.dispense_identity_id(); + let left = to_selected_exprs(sel_from, from); + let right = to_selected_exprs(sel_to, to); + + match *variant { + "Lookup" => LookupIdentity { + id, source, - left: to_selected_exprs(sel_from, from), - right: to_selected_exprs(sel_to, to), + left, + right, } - .into() - } else { - PermutationIdentity { - id: counters.dispense_identity_id(), + .into(), + "Permutation" => PermutationIdentity { + id, source, - left: to_selected_exprs(sel_from, from), - right: to_selected_exprs(sel_to, to), + left, + right, } - .into() + .into(), + "PhantomPermutation" => PhantomPermutationIdentity { + id, + source, + left, + right, + } + .into(), + "PhantomLookup" => { + let multiplicity = to_expr(&fields[2]); + PhantomLookupIdentity { + id, + source, + left, + right, + multiplicity, + } + .into() + } + _ => unreachable!(), } } "Connection" => { diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index bbd4998d5..59ad3c7a3 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -7,8 +7,9 @@ use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use powdr_ast::analyzed::{ AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, AlgebraicReference, AlgebraicUnaryOperation, AlgebraicUnaryOperator, Analyzed, ConnectIdentity, Expression, - FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PolyID, - PolynomialIdentity, PolynomialReference, PolynomialType, Reference, SymbolKind, + FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PhantomLookupIdentity, + PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialReference, PolynomialType, + Reference, SymbolKind, }; use powdr_ast::parsed::types::Type; use powdr_ast::parsed::visitor::{AllChildren, Children, ExpressionVisitable}; @@ -326,47 +327,55 @@ fn simplify_expression_single(e: &mut AlgebraicExpression) { fn extract_constant_lookups(pil_file: &mut Analyzed) { let mut new_identities = vec![]; for identity in &mut pil_file.identities.iter_mut() { - if let Identity::Lookup(LookupIdentity { - source, - left, - right, - .. - }) = identity - { - let mut extracted = HashSet::new(); - for (i, (l, r)) in left - .expressions - .iter() - .zip(&right.expressions) - .enumerate() - .filter_map(|(i, (l, r))| { - if let AlgebraicExpression::Number(n) = r { - Some((i, (l, n))) - } else { - None - } - }) - { - // TODO remove clones - let l_sel = left.selector.clone(); - let r_sel = right.selector.clone(); - let pol_id = (l_sel * l.clone()) - (r_sel * AlgebraicExpression::from(*r)); - new_identities.push((simplify_expression(pol_id), source.clone())); + match identity { + Identity::Lookup(LookupIdentity { + source, + left, + right, + .. + }) + | Identity::PhantomLookup(PhantomLookupIdentity { + source, + left, + right, + .. + }) => { + let mut extracted = HashSet::new(); + for (i, (l, r)) in left + .expressions + .iter() + .zip(&right.expressions) + .enumerate() + .filter_map(|(i, (l, r))| { + if let AlgebraicExpression::Number(n) = r { + Some((i, (l, n))) + } else { + None + } + }) + { + // TODO remove clones + let l_sel = left.selector.clone(); + let r_sel = right.selector.clone(); + let pol_id = (l_sel * l.clone()) - (r_sel * AlgebraicExpression::from(*r)); + new_identities.push((simplify_expression(pol_id), source.clone())); - extracted.insert(i); + extracted.insert(i); + } + // TODO rust-ize this. + let mut c = 0usize; + left.expressions.retain(|_i| { + c += 1; + !extracted.contains(&(c - 1)) + }); + let mut c = 0usize; + right.expressions.retain(|_i| { + c += 1; + + !extracted.contains(&(c - 1)) + }); } - // TODO rust-ize this. - let mut c = 0usize; - left.expressions.retain(|_i| { - c += 1; - !extracted.contains(&(c - 1)) - }); - let mut c = 0usize; - right.expressions.retain(|_i| { - c += 1; - - !extracted.contains(&(c - 1)) - }); + _ => {} } } for (identity, source) in new_identities { @@ -484,11 +493,13 @@ fn remove_trivial_identities(pil_file: &mut Analyzed) { } None } - Identity::Lookup(LookupIdentity { left, right, .. }) => { + Identity::Lookup(LookupIdentity { left, right, .. }) + | Identity::Permutation(PermutationIdentity { left, right, .. }) + | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) + | Identity::PhantomPermutation(PhantomPermutationIdentity { left, right, .. }) => { assert_eq!(left.expressions.len(), right.expressions.len()); left.expressions.is_empty().then_some(index) } - Identity::Permutation(..) => None, Identity::Connect(..) => None, }) .collect(); @@ -506,8 +517,10 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { let discriminant = |i: &CanonicalIdentity| match i.0 { Identity::Polynomial(..) => 0, Identity::Lookup(..) => 1, - Identity::Permutation(..) => 2, - Identity::Connect(..) => 3, + Identity::PhantomLookup(..) => 2, + Identity::Permutation(..) => 3, + Identity::PhantomPermutation(..) => 4, + Identity::Connect(..) => 5, }; discriminant(self) @@ -525,6 +538,20 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { left: c, right: d, .. }), ) => a.cmp(c).then_with(|| b.cmp(d)), + ( + Identity::PhantomLookup(PhantomLookupIdentity { + left: a, + right: b, + multiplicity: c, + .. + }), + Identity::PhantomLookup(PhantomLookupIdentity { + left: d, + right: e, + multiplicity: f, + .. + }), + ) => a.cmp(d).then_with(|| b.cmp(e)).then_with(|| c.cmp(f)), ( Identity::Permutation(PermutationIdentity { left: a, right: b, .. @@ -533,6 +560,18 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { left: c, right: d, .. }), ) => a.cmp(c).then_with(|| b.cmp(d)), + ( + Identity::PhantomPermutation(PhantomPermutationIdentity { + left: a, + right: b, + .. + }), + Identity::PhantomPermutation(PhantomPermutationIdentity { + left: c, + right: d, + .. + }), + ) => a.cmp(c).then_with(|| b.cmp(d)), ( Identity::Connect(ConnectIdentity { left: a, right: b, .. diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 5af9f4e93..30d13abfb 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -171,15 +171,11 @@ fn lookup_via_challenges() { } #[test] -fn lookup_via_challenges_ext() { - let f = "std/lookup_via_challenges_ext.asm"; - test_halo2(make_simple_prepared_pipeline(f)); - test_plonky3::(f, vec![]); -} - -#[test] -fn lookup_via_challenges_ext_simple() { - let f = "std/lookup_via_challenges_ext_simple.asm"; +#[should_panic = "Failed to merge the first and last row of the VM 'Main Machine'"] +fn lookup_via_challenges_range_constraint() { + // This test currently fails, because witness generation for the multiplicity column + // does not yet work for range constraints, so the lookup constraints are not satisfied. + let f = "std/lookup_via_challenges_range_constraint.asm"; test_halo2(make_simple_prepared_pipeline(f)); test_plonky3::(f, vec![]); } @@ -191,35 +187,17 @@ fn bus_permutation_via_challenges() { } #[test] -fn bus_permutation_via_challenges_ext() { +fn bus_permutation_via_challenges_ext_bn() { let f = "std/bus_permutation_via_challenges_ext.asm"; test_halo2(make_simple_prepared_pipeline(f)); - test_plonky3::(f, vec![]); } #[test] -fn test_multiplicities() { - let f = "std/multiplicities.asm"; - test_halo2(make_simple_prepared_pipeline(f)); - - // This test currently has a native lookup to aid witness generation, - // which is not supported by the Plonky3 backend. - // test_plonky3::(f, vec![]); -} - -#[test] -fn bus_lookup_via_challenges() { +fn bus_lookup_via_challenges_bn() { let f = "std/bus_lookup_via_challenges.asm"; test_halo2(make_simple_prepared_pipeline(f)); } -#[test] -fn bus_lookup_via_challenges_ext() { - let f = "std/bus_lookup_via_challenges_ext.asm"; - test_halo2(make_simple_prepared_pipeline(f)); - test_plonky3::(f, vec![]); -} - #[test] fn write_once_memory_test() { let f = "std/write_once_memory_test.asm"; diff --git a/plonky3/src/circuit_builder.rs b/plonky3/src/circuit_builder.rs index 6797f2406..4859788f7 100644 --- a/plonky3/src/circuit_builder.rs +++ b/plonky3/src/circuit_builder.rs @@ -466,6 +466,9 @@ where unimplemented!("Plonky3 does not support permutations") } Identity::Connect(..) => unimplemented!("Plonky3 does not support connections"), + Identity::PhantomPermutation(..) | Identity::PhantomLookup(..) => { + // phantom identities are only used in witgen + } } } } diff --git a/std/protocols/lookup.asm b/std/protocols/lookup.asm index fded98474..cbb2b4753 100644 --- a/std/protocols/lookup.asm +++ b/std/protocols/lookup.asm @@ -113,11 +113,9 @@ let lookup: Constr, expr -> () = constr |lookup_constraint, multiplicities| { is_first * acc_2 = 0; constrain_eq_ext(update_expr, from_base(0)); - // Build an annotation for witness generation - let witgen_annotation = to_phantom_lookup(lookup_constraint, multiplicities); - // TODO: Adding it to the constraint set currently fails - // witgen_annotation; - + // Add an annotation for witness generation + to_phantom_lookup(lookup_constraint, multiplicities); + // In the extension field, we need a prover function for the accumulator. if needs_extension() { // TODO: Helper columns, because we can't access the previous row in hints diff --git a/test_data/std/lookup_via_challenges.asm b/test_data/std/lookup_via_challenges.asm index 0c8535746..8992e6a12 100644 --- a/test_data/std/lookup_via_challenges.asm +++ b/test_data/std/lookup_via_challenges.asm @@ -1,25 +1,24 @@ -use std::prelude::Query; use std::convert::fe; use std::protocols::lookup::lookup; use std::math::fp2::from_base; use std::prover::challenge; machine Main with degree: 8 { - col fixed random_six = [1, 1, 1, 0, 1, 1, 1, 0]; - col fixed first_seven = [1, 1, 1, 1, 1, 1, 1, 0]; - col fixed a1 = [1, 2, 4, 3, 1, 1, 4, 1]; - col fixed a2 = [1, 2, 4, 1, 1, 1, 4, 1]; - col fixed a3 = [1, 2, 4, 1, 1, 1, 4, 3]; - col witness b1, b2, b3; - query |i| { - std::prover::provide_value(b1, i, fe(i + 1)); - std::prover::provide_value(b2, i, fe(i + 1)); - std::prover::provide_value(b3, i, fe(i + 1)); - }; - col fixed m = [3, 1, 0, 2, 0, 0, 0, 0]; + col fixed x = [1, 5, 2, 6, 4, 2, 6, 3]; + col witness y; - let lookup_constraint = random_six $ [a1, a2, a3] in first_seven $ [b1, b2, b3]; + // Pre-compute f(x) = x + 1 for all x in [1, 8] + col fixed INC_X = [1, 2, 3, 4, 5, 6, 7, 8]; + col fixed INC_Y = [2, 3, 4, 5, 6, 7, 8, 9]; - lookup(lookup_constraint, m); -} + // Machine extractor currently accepts the multiplicity column with exact the name of "m_logup_multiplicity" + col witness m_logup_multiplicity; + + // This would be the correct multiplicity values that would satisfy the constraints: + //col fixed m_logup_multiplicity = [1, 2, 1, 1, 1, 2, 0, 0]; + + let lookup_constraint = [x, y] in [INC_X, INC_Y]; + + lookup(lookup_constraint, m_logup_multiplicity); +} \ No newline at end of file diff --git a/test_data/std/lookup_via_challenges_ext.asm b/test_data/std/lookup_via_challenges_ext.asm deleted file mode 100644 index fcc1ffba4..000000000 --- a/test_data/std/lookup_via_challenges_ext.asm +++ /dev/null @@ -1,26 +0,0 @@ -use std::prelude::Query; -use std::convert::fe; -use std::protocols::lookup::lookup; -use std::protocols::lookup::compute_next_z; -use std::math::fp2::Fp2; -use std::prover::challenge; - -machine Main with degree: 8 { - col fixed a_sel = [0, 1, 1, 1, 0, 1, 0, 0]; - col fixed b_sel = [1, 1, 0, 1, 1, 1, 1, 0]; - - col fixed a1 = [16, 20, 22, 17, 16, 20, 4, 1]; - col fixed a2 = [12, 5, 7, 2, 5, 5, 4, 1]; - col fixed a3 = [20, 36, 38, 33, 36, 36, 4, 3]; - col witness b1, b2, b3; - query |i| { - std::prover::provide_value(b1, i, fe(i + 16)); - std::prover::provide_value(b2, i, fe(i + 1)); - std::prover::provide_value(b3, i, fe(i + 32)); - }; - col fixed m = [0, 1, 0, 0, 2, 0, 1, 0]; - - let lookup_constraint = a_sel $ [a1, a2, a3] in b_sel $ [b1, b2, b3]; - - lookup(lookup_constraint, m); -} \ No newline at end of file diff --git a/test_data/std/lookup_via_challenges_ext_simple.asm b/test_data/std/lookup_via_challenges_ext_simple.asm deleted file mode 100644 index 33194aa7f..000000000 --- a/test_data/std/lookup_via_challenges_ext_simple.asm +++ /dev/null @@ -1,19 +0,0 @@ -use std::prelude::Query; -use std::convert::fe; -use std::protocols::lookup::lookup; -use std::protocols::lookup::compute_next_z; -use std::math::fp2::Fp2; -use std::prover::challenge; - -machine Main with degree: 8 { - col fixed a = [1, 1, 4, 1, 1, 2, 1, 1]; - let b; - query |i| { - std::prover::provide_value(b, i, fe(i + 1)); - }; - col fixed m = [6, 1, 0, 1, 0, 0, 0, 0]; - - let lookup_constraint = [a] in [b]; - - lookup(lookup_constraint, m); -} \ No newline at end of file diff --git a/test_data/std/lookup_via_challenges_range_constraint.asm b/test_data/std/lookup_via_challenges_range_constraint.asm new file mode 100644 index 000000000..789da9c88 --- /dev/null +++ b/test_data/std/lookup_via_challenges_range_constraint.asm @@ -0,0 +1,19 @@ +use std::convert::fe; +use std::protocols::lookup::lookup; +use std::math::fp2::from_base; +use std::prover::challenge; + +machine Main with degree: 8 { + + // Prove a correct decomposition of x into 3-bit limbs + col fixed x = [1, 6, 23, 55, 63, 4, 1, 0]; + col witness x_low, x_high; + + col fixed BIT3 = [0, 1, 2, 3, 4, 5, 6, 7]; + + col witness m_low, m_high; + lookup([x_low] in [BIT3], m_low); + lookup([x_high] in [BIT3], m_high); + + x = x_low + 8 * x_high; +} \ No newline at end of file diff --git a/test_data/std/multiplicities.asm b/test_data/std/multiplicities.asm deleted file mode 100644 index 6438146ce..000000000 --- a/test_data/std/multiplicities.asm +++ /dev/null @@ -1,28 +0,0 @@ -use std::convert::fe; -use std::protocols::lookup::lookup; -use std::math::fp2::from_base; -use std::prover::challenge; - -machine Main with degree: 8 { - - col fixed x = [1, 5, 2, 6, 4, 2, 6, 3]; - col witness y; - - // Pre-compute f(x) = x + 1 for all x in [1, 8] - col fixed INC_X = [1, 2, 3, 4, 5, 6, 7, 8]; - col fixed INC_Y = [2, 3, 4, 5, 6, 7, 8, 9]; - - // Native lookup to implement y = f(x). From this, witgen should - // figure out the values in column y via FixedLookup. - [x, y] in [INC_X, INC_Y]; - - // Machine extractor currently accepts the multiplicity column with exact the name of "m_logup_multiplicity" - col witness m_logup_multiplicity; - - // This would be the correct multiplicity values that would satisfy the constraints: - //col fixed m_logup_multiplicity = [1, 2, 1, 1, 1, 2, 0, 0]; - - let lookup_constraint = [x, y] in [INC_X, INC_Y]; - - lookup(lookup_constraint, m_logup_multiplicity); -} \ No newline at end of file