From dbf2d4c2ada4423138ef3ef3500c6e9987c054df Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Thu, 7 Dec 2023 15:25:46 +0000 Subject: [PATCH 01/10] temp --- bberg/src/vm_builder.rs | 183 ++++++++++++++++++++++++++++------------ 1 file changed, 129 insertions(+), 54 deletions(-) diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index bbd940369a..c79cd2b285 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -1,9 +1,11 @@ use std::collections::HashMap; -use ast::analyzed::AlgebraicExpression as Expression; +use ast::analyzed::AlgebraicExpression; use ast::analyzed::Analyzed; use ast::analyzed::Identity; +use ast::analyzed::IdentityKind; +use ast::parsed::SelectedExpressions; use itertools::Itertools; use number::FieldElement; @@ -42,8 +44,78 @@ pub(crate) fn analyzed_to_cpp( // Inlining step to remove the intermediate poly definitions let analyzed_identities = analyzed.identities_with_inlined_intermediate_polynomials(); + // ----------------------- Handle Standard Relation Identities ----------------------- + // We collect all references to shifts as we traverse all identities and create relation files + let shifted_polys = create_relation_files(&bb_files, file_name, &analyzed_identities); + + // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- + // We will likely need to create a new set of permutation identities for each lookup / permutation pair we come across + handle_permutations(analyzed); + // handle_lookups(); + + + + // TODO: hack - this can be removed with some restructuring + let shifted_polys: Vec = shifted_polys + .clone() + .iter() + .map(|s| s.replace("_shift", "")) + .collect(); + + // Collect all column names and determine if they need a shift or not + let ColumnGroups { + fixed, + witness, + all_cols, + unshifted, + to_be_shifted, + shifted, + all_cols_with_shifts, + } = get_all_col_names(fixed, witness, &shifted_polys); + + // bb_files.create_declare_views(file_name, &all_cols_with_shifts); + + // // ----------------------- Create the circuit builder file ----------------------- + // bb_files.create_circuit_builder_hpp( + // file_name, + // &relations, + // &all_cols, + // &to_be_shifted, + // &all_cols_with_shifts, + // ); + + // // ----------------------- Create the flavor file ----------------------- + // bb_files.create_flavor_hpp( + // file_name, + // &relations, + // &fixed, + // &witness, + // &all_cols, + // &to_be_shifted, + // &shifted, + // &all_cols_with_shifts, + // ); + + // // ----------------------- Create the composer files ----------------------- + // bb_files.create_composer_cpp(file_name, &all_cols); + // bb_files.create_composer_hpp(file_name); + + // // ----------------------- Create the Verifier files ----------------------- + // bb_files.create_verifier_cpp(file_name, &witness); + // bb_files.create_verifier_hpp(file_name); + + // // ----------------------- Create the Prover files ----------------------- + // bb_files.create_prover_cpp(file_name, &unshifted, &to_be_shifted); + // bb_files.create_prover_hpp(file_name); +} + + +/// TODO: MOVE THIS OUT OF THIS FILE???? +/// Does this need to return all of the shifted polys that it collects> +/// TODO: restructure this so that we do not have to pass in bb files abd the name at the top level +fn create_relation_files(bb_files: &BBFiles, file_name: &str, analyzed_identities: &Vec>>) -> Vec { // Group relations per file - let grouped_relations = group_relations_per_file(&analyzed_identities); + let grouped_relations: HashMap>>> = group_relations_per_file(&analyzed_identities); let relations = grouped_relations.keys().cloned().collect_vec(); // Contains all of the rows in each relation, will be useful for creating composite builder types @@ -74,60 +146,63 @@ pub(crate) fn analyzed_to_cpp( ); } - // TODO: hack - this can be removed with some restructuring - let shifted_polys: Vec = shifted_polys - .clone() - .iter() - .map(|s| s.replace("_shift", "")) - .collect(); + shifted_polys - // Collect all column names and determine if they need a shift or not - let ColumnGroups { - fixed, - witness, - all_cols, - unshifted, - to_be_shifted, - shifted, - all_cols_with_shifts, - } = get_all_col_names(fixed, witness, &shifted_polys); +} + + +// Maybe this is not the right thing to do? +#[derive(Debug)] +struct Permutation { + left: PermSide, + right: PermSide +} + +// TODO: rename +#[derive(Debug)] +struct PermSide { + selector: Option, + cols: Vec +} + +fn handle_permutations(analyzed: &Analyzed) -> Vec { + let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); + let new_perms = perms.iter().map(|perm| + Permutation { + left: get_perm_side(&perm.left), + right: get_perm_side(&perm.right) + }).collect_vec(); + + dbg!(&new_perms); + + // For every permutation set that we create, we will need to create an inverse column ( helper function ) + // TODO: how do we determine the name of this inverse column? + + + new_perms +} + +fn get_perm_side(def: &SelectedExpressions>) -> PermSide { + let get_name = |expr: &AlgebraicExpression| match expr { + AlgebraicExpression::Reference(a_ref) => sanitize_name(&a_ref.name), + _ => panic!("Expected reference") + }; - bb_files.create_declare_views(file_name, &all_cols_with_shifts); - - // ----------------------- Create the circuit builder file ----------------------- - bb_files.create_circuit_builder_hpp( - file_name, - &relations, - &all_cols, - &to_be_shifted, - &all_cols_with_shifts, - ); - - // ----------------------- Create the flavor file ----------------------- - bb_files.create_flavor_hpp( - file_name, - &relations, - &fixed, - &witness, - &all_cols, - &to_be_shifted, - &shifted, - &all_cols_with_shifts, - ); - - // ----------------------- Create the composer files ----------------------- - bb_files.create_composer_cpp(file_name, &all_cols); - bb_files.create_composer_hpp(file_name); - - // ----------------------- Create the Verifier files ----------------------- - bb_files.create_verifier_cpp(file_name, &witness); - bb_files.create_verifier_hpp(file_name); - - // ----------------------- Create the Prover files ----------------------- - bb_files.create_prover_cpp(file_name, &unshifted, &to_be_shifted); - bb_files.create_prover_hpp(file_name); + PermSide { + selector: def.selector.as_ref().map(|expr| get_name(&expr)), + cols: def.expressions.iter().map(|expr| get_name(&expr)).collect_vec() + } } + + +// pub struct SelectedExpressions { +// pub selector: Option, +// pub expressions: Vec, +// } + + + /// Group relations per file /// /// The compiler returns all relations in one large vector, however we want to distinguish @@ -149,8 +224,8 @@ pub(crate) fn analyzed_to_cpp( /// /// This allows us to generate a relation.hpp file containing ONLY the relations for that .pil file fn group_relations_per_file( - identities: &[Identity>], -) -> HashMap>>> { + identities: &[Identity>], +) -> HashMap>>> { identities .iter() .cloned() From a7ec94cbaeed949002f4c1cab4fb51f7da68822e Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Thu, 7 Dec 2023 19:09:06 +0000 Subject: [PATCH 02/10] feat: include attribute in permutation identities --- asm_to_pil/src/vm_to_constrained.rs | 2 +- ast/src/parsed/display.rs | 4 +++- ast/src/parsed/mod.rs | 7 +++++++ ast/src/parsed/visitor.rs | 8 ++++++-- bberg/src/vm_builder.rs | 17 ++++++++++++++--- parser/src/lib.rs | 24 ++++++++++++++++++++++++ parser/src/powdr.lalrpop | 6 +++++- pil_analyzer/src/statement_processor.rs | 3 ++- type_check/src/lib.rs | 4 +++- 9 files changed, 65 insertions(+), 10 deletions(-) diff --git a/asm_to_pil/src/vm_to_constrained.rs b/asm_to_pil/src/vm_to_constrained.rs index 68cf46dbc2..26ddd106ad 100644 --- a/asm_to_pil/src/vm_to_constrained.rs +++ b/asm_to_pil/src/vm_to_constrained.rs @@ -411,7 +411,7 @@ impl ASMPILConverter { } } else { match &mut statement { - PilStatement::PermutationIdentity(_, left, _) + PilStatement::PermutationIdentity(_, _, left, _) | PilStatement::PlookupIdentity(_, left, _) => { assert!( left.selector.is_none(), diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index ac23386dc4..361d667ec5 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -391,7 +391,9 @@ impl Display for PilStatement { } } PilStatement::PlookupIdentity(_, left, right) => write!(f, "{left} in {right};"), - PilStatement::PermutationIdentity(_, left, right) => write!(f, "{left} is {right};"), + PilStatement::PermutationIdentity(_, // + _, // + left, right) => write!(f, "{left} is {right};"), // PilStatement::ConnectIdentity(_, left, right) => write!( f, "{{ {} }} connect {{ {} }};", diff --git a/ast/src/parsed/mod.rs b/ast/src/parsed/mod.rs index 26657af854..fe0faad647 100644 --- a/ast/src/parsed/mod.rs +++ b/ast/src/parsed/mod.rs @@ -42,6 +42,7 @@ pub enum PilStatement { ), PermutationIdentity( usize, + Option, SelectedExpressions>, SelectedExpressions>, ), @@ -50,6 +51,12 @@ pub enum PilStatement { Expression(usize, Expression), } +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +pub struct Attribute { + pub name: Option, +} + + #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] pub struct SelectedExpressions { pub selector: Option, diff --git a/ast/src/parsed/visitor.rs b/ast/src/parsed/visitor.rs index 8fa9e7bfa2..55c9e95d62 100644 --- a/ast/src/parsed/visitor.rs +++ b/ast/src/parsed/visitor.rs @@ -193,7 +193,9 @@ impl ExpressionVisitable> for Pi match self { PilStatement::Expression(_, e) => e.visit_expressions_mut(f, o), PilStatement::PlookupIdentity(_, left, right) - | PilStatement::PermutationIdentity(_, left, right) => [left, right] + | PilStatement::PermutationIdentity(_, // + _, // + left, right) => [left, right] // .into_iter() .try_for_each(|e| e.visit_expressions_mut(f, o)), PilStatement::ConnectIdentity(_start, left, right) => left @@ -230,7 +232,9 @@ impl ExpressionVisitable> for Pi match self { PilStatement::Expression(_, e) => e.visit_expressions(f, o), PilStatement::PlookupIdentity(_, left, right) - | PilStatement::PermutationIdentity(_, left, right) => [left, right] + | PilStatement::PermutationIdentity(_, // + _, // + left, right) => [left, right] // .into_iter() .try_for_each(|e| e.visit_expressions(f, o)), PilStatement::ConnectIdentity(_start, left, right) => left diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index c79cd2b285..f0dfd9f8a4 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -46,7 +46,10 @@ pub(crate) fn analyzed_to_cpp( // ----------------------- Handle Standard Relation Identities ----------------------- // We collect all references to shifts as we traverse all identities and create relation files - let shifted_polys = create_relation_files(&bb_files, file_name, &analyzed_identities); + let RelationOutput { + relations, + shifted_polys + } = create_relation_files(&bb_files, file_name, &analyzed_identities); // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- // We will likely need to create a new set of permutation identities for each lookup / permutation pair we come across @@ -110,10 +113,15 @@ pub(crate) fn analyzed_to_cpp( } +struct RelationOutput { + relations: Vec, + shifted_polys: Vec, +} + /// TODO: MOVE THIS OUT OF THIS FILE???? /// Does this need to return all of the shifted polys that it collects> /// TODO: restructure this so that we do not have to pass in bb files abd the name at the top level -fn create_relation_files(bb_files: &BBFiles, file_name: &str, analyzed_identities: &Vec>>) -> Vec { +fn create_relation_files(bb_files: &BBFiles, file_name: &str, analyzed_identities: &Vec>>) -> RelationOutput { // Group relations per file let grouped_relations: HashMap>>> = group_relations_per_file(&analyzed_identities); let relations = grouped_relations.keys().cloned().collect_vec(); @@ -146,7 +154,10 @@ fn create_relation_files(bb_files: &BBFiles, file_name: &str, a ); } - shifted_polys + RelationOutput { + relations, + shifted_polys + } } diff --git a/parser/src/lib.rs b/parser/src/lib.rs index 311ab1f2c6..dbd5c5b3c1 100644 --- a/parser/src/lib.rs +++ b/parser/src/lib.rs @@ -110,6 +110,30 @@ mod test { ); } + #[test] + fn parse_permutation_attribute() { + let parsed = powdr::PILFileParser::new() + .parse::(" + #[attribute] + { f } is { g };") + .unwrap(); + assert_eq!( + parsed, + PILFile(vec![PilStatement::PermutationIdentity( + 13, + Some("attribute".to_string()), + SelectedExpressions { + selector: None, + expressions: vec![direct_reference("f")] + }, + SelectedExpressions { + selector: None, + expressions: vec![direct_reference("g")] + } + )]) + ); + } + fn parse_file(name: &str) -> PILFile { let file = std::path::PathBuf::from(format!( "{}/../test_data/{name}", diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index 4682c19661..1c61c131f8 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -147,8 +147,12 @@ SelectedExpressions: SelectedExpressions> = { Expression => SelectedExpressions{selector: None, expressions: vec![<>]}, } +Attribute: String = { + "#[" "]" => <>.to_string() +} + PermutationIdentity: PilStatement = { - <@L> "is" => PilStatement::PermutationIdentity(<>) + <@L> "is" => PilStatement::PermutationIdentity(<>) } ConnectIdentity: PilStatement = { diff --git a/pil_analyzer/src/statement_processor.rs b/pil_analyzer/src/statement_processor.rs index 42511d7b6f..50f1b11cda 100644 --- a/pil_analyzer/src/statement_processor.rs +++ b/pil_analyzer/src/statement_processor.rs @@ -215,7 +215,8 @@ where self.process_selected_expressions(key), self.process_selected_expressions(haystack), ), - PilStatement::PermutationIdentity(start, left, right) => ( + PilStatement::PermutationIdentity(start,// TODO: include the attribute in the PIL ITEM! + _, left, right) => ( start, IdentityKind::Permutation, self.process_selected_expressions(left), diff --git a/type_check/src/lib.rs b/type_check/src/lib.rs index 0616f93627..0faaf160af 100644 --- a/type_check/src/lib.rs +++ b/type_check/src/lib.rs @@ -319,7 +319,9 @@ impl TypeChecker { .iter() .filter_map(|s| match s { ast::parsed::PilStatement::PolynomialIdentity(_, _) => None, - ast::parsed::PilStatement::PermutationIdentity(_, l, _) + ast::parsed::PilStatement::PermutationIdentity(_, // + _, // + l, _) // | ast::parsed::PilStatement::PlookupIdentity(_, l, _) => l .selector .is_some() From 6b5e4d94aa40c12248b40868265d2bbfd56cbe4a Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Thu, 7 Dec 2023 21:22:47 +0000 Subject: [PATCH 03/10] temp: perms --- ast/src/analyzed/display.rs | 2 +- ast/src/analyzed/mod.rs | 2 + bberg/src/vm_builder.rs | 151 +++++++++++++++++++++++- pil_analyzer/src/condenser.rs | 2 + pil_analyzer/src/statement_processor.rs | 15 ++- 5 files changed, 164 insertions(+), 8 deletions(-) diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index 1218143de2..6c91bd1966 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -149,7 +149,7 @@ impl Display for Identity> { } } IdentityKind::Plookup => write!(f, "{} in {};", self.left, self.right), - IdentityKind::Permutation => write!(f, "{} is {};", self.left, self.right), + IdentityKind::Permutation => write!(f, "#[{}] {} is {};", self.attribute.clone().unwrap_or_default(), self.left, self.right), IdentityKind::Connect => write!(f, "{} connect {};", self.left, self.right), } } diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index 26ec1bf9d8..4fda5bbfb1 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -226,6 +226,7 @@ impl Analyzed { self.identities.push(Identity { id, kind: IdentityKind::Polynomial, + attribute: None, // TODO(md): None for the meantime as we do not have tagged identities, will be updated in following pr source, left: SelectedExpressions { selector: Some(identity), @@ -504,6 +505,7 @@ pub struct Identity { /// The ID is specific to the identity kind. pub id: u64, pub kind: IdentityKind, + pub attribute: Option, pub source: SourceRef, /// For a simple polynomial identity, the selector contains /// the actual expression (see expression_for_poly_id). diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index f0dfd9f8a4..759ea130c2 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -165,6 +165,10 @@ fn create_relation_files(bb_files: &BBFiles, file_name: &str, a // Maybe this is not the right thing to do? #[derive(Debug)] struct Permutation { + /// Attribute in this setting is used to determine what the name of the inverse column should be + /// TODO(md): Future implementations should use this to allow using the same inverse column multiple times, thus + /// allowing granularity in the logup trade-off + attribute: Option, left: PermSide, right: PermSide } @@ -176,21 +180,162 @@ struct PermSide { cols: Vec } -fn handle_permutations(analyzed: &Analyzed) -> Vec { +fn handle_permutations(analyzed: &Analyzed) { let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); let new_perms = perms.iter().map(|perm| Permutation { + attribute: perm.attribute.clone(), left: get_perm_side(&perm.left), right: get_perm_side(&perm.right) }).collect_vec(); - dbg!(&new_perms); // For every permutation set that we create, we will need to create an inverse column ( helper function ) // TODO: how do we determine the name of this inverse column? + create_permutations(new_perms); +} + +fn create_permutations(permutations: Vec) { + for permutation in permutations { + create_permutation_settings_file(permutation); + } +} + +fn create_permutation_settings_file(permutation: Permutation) -> String { + + println!("Permutation: {:?}", permutation); + let columns_per_set = permutation.left.cols.len(); + // TODO(md): Throw an error if no attribute is provided for the permutation + // TODO(md): In the future we will need to condense off the back of this - combining those with the same inverse column + let inverse_column_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here + + // NOTE: syntax is not flexible enough to enable the single row case right now :(:(:(:(:)))) + // This also will need to work for both sides of this ! + let selector = permutation.left.selector.clone().unwrap(); // TODO: deal with unwrap + let lhs_cols = permutation.left.cols.clone(); + let rhs_cols = permutation.right.cols.clone(); + + // 0. The polynomial containing the inverse products -> taken from the attributes + // 1. The polynomial enabling the relation (the selector) + // 2. lhs selector + // 3. rhs selector + // 4.. + columns per set. lhs cols + // 4 + columns per set.. . rhs cols + let mut perm_entities: Vec = [ + inverse_column_name, + selector.clone(), + selector.clone(), + selector.clone() // TODO: update this away from the simple example + ].to_vec(); + + perm_entities.extend(lhs_cols); + perm_entities.extend(rhs_cols); + + + // TODO: below here should really be in a new function as we have just got the settings extracted from the parsed type + let inverse_computed_at = create_inverse_computed_at(selector); + let const_entities = create_get_const_entities(&perm_entities); + let nonconst_entities = create_get_nonconst_entities(&perm_entities); + + + format!( + // TODO: replace with the inverse label name! + " + class ExampleTuplePermutationSettings {{ + public: + // This constant defines how many columns are bundled together to form each set. For example, in this case we are + // bundling tuples of (permutation_set_column_1, permutation_set_column_2) to be a permutation of + // (permutation_set_column_3,permutation_set_column_4). As the tuple has 2 elements, set the value to 2 + constexpr static size_t COLUMNS_PER_SET = {columns_per_set}; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the + * value needs to be set to zero. + * + * @details If this is true then permutation takes place in this row + * + */ + {inverse_computed_at} + + /** + * @brief Get all the entities for the permutation when we don't need to update them + * + * @details The entities are returned as a tuple of references in the following order: + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of + * the inverse polynomial + * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum + * subrelation + * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum + * subrelation + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) + * + * @return All the entities needed for the permutation + */ + {const_entities} + + /** + * @brief Get all the entities for the permutation when need to update them + * + * @details The entities are returned as a tuple of references in the following order: + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of + * the inverse polynomial + * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum + * subrelation + * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum + * subrelation + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) + * + * @return All the entities needed for the permutation + */ + {nonconst_entities} + }} + " + ) + +} + + - new_perms +// TODO: make this dynamic such that there can be more than one +fn create_inverse_computed_at(inverse_selector: String) -> String { + let inverse_computed_selector = format!("in.{inverse_selector}"); + format!(" + template static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in) {{ + return ({inverse_computed_selector} == 1); + }}") +} + +fn create_get_const_entities (settings: &[String]) -> String { + let forward = create_forward_as_tuple(settings); + format!(" + template static inline auto get_const_entities(const AllEntities& in) {{ + {forward} + }} + ") +} + +fn create_get_nonconst_entities (settings: &[String]) -> String { + let forward = create_forward_as_tuple(settings); + format!(" + template static inline auto get_nonconst_entities(AllEntities& in) {{ + {forward} + }} + ") +} + + +fn create_forward_as_tuple(settings: &[String]) -> String { + let adjusted = settings.iter().map(|col| format!("in.{col},\n")).join(""); + format!(" + return std::forward_as_tuple( + {} + ); + ", adjusted) } fn get_perm_side(def: &SelectedExpressions>) -> PermSide { diff --git a/pil_analyzer/src/condenser.rs b/pil_analyzer/src/condenser.rs index 0cd8c8edeb..6a8f56f677 100644 --- a/pil_analyzer/src/condenser.rs +++ b/pil_analyzer/src/condenser.rs @@ -119,6 +119,7 @@ impl Condenser { .map(|constraint| Identity { id: identity.id, kind: identity.kind, + attribute: identity.attribute.clone(), source: identity.source.clone(), left: SelectedExpressions { selector: Some(constraint), @@ -131,6 +132,7 @@ impl Condenser { vec![Identity { id: identity.id, kind: identity.kind, + attribute: identity.attribute.clone(), source: identity.source.clone(), left: self.condense_selected_expressions(&identity.left), right: self.condense_selected_expressions(&identity.right), diff --git a/pil_analyzer/src/statement_processor.rs b/pil_analyzer/src/statement_processor.rs index 50f1b11cda..23a0eff916 100644 --- a/pil_analyzer/src/statement_processor.rs +++ b/pil_analyzer/src/statement_processor.rs @@ -198,11 +198,12 @@ where } fn handle_identity_statement(&mut self, statement: PilStatement) -> Vec> { - let (start, kind, left, right) = match statement { + let (start, kind, attribute, left, right) = match statement { PilStatement::PolynomialIdentity(start, expression) | PilStatement::Expression(start, expression) => ( start, IdentityKind::Polynomial, + None, SelectedExpressions { selector: Some(self.process_expression(expression)), expressions: vec![], @@ -212,19 +213,24 @@ where PilStatement::PlookupIdentity(start, key, haystack) => ( start, IdentityKind::Plookup, + None, self.process_selected_expressions(key), self.process_selected_expressions(haystack), ), - PilStatement::PermutationIdentity(start,// TODO: include the attribute in the PIL ITEM! - _, left, right) => ( + PilStatement::PermutationIdentity(start, + attribute, left, right) => { + ( start, IdentityKind::Permutation, + attribute.clone(), self.process_selected_expressions(left), self.process_selected_expressions(right), - ), + ) + }, PilStatement::ConnectIdentity(start, left, right) => ( start, IdentityKind::Connect, + None, SelectedExpressions { selector: None, expressions: self.expression_processor().process_expressions(left), @@ -243,6 +249,7 @@ where vec![PILItem::Identity(Identity { id: self.counters.dispense_identity_id(kind), kind, + attribute, source: self.driver.source_position_to_source_ref(start), left, right, From 9756ad49cb15b04c3bf781bd5e31fa14da5bb326 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Fri, 8 Dec 2023 23:04:07 +0000 Subject: [PATCH 04/10] working --- bberg/src/circuit_builder.rs | 70 +++++++++++- bberg/src/flavor_builder.rs | 35 ++++-- bberg/src/permutation_builder.rs | 0 bberg/src/prover_builder.rs | 2 +- bberg/src/utils.rs | 5 +- bberg/src/vm_builder.rs | 177 ++++++++++++++++++++----------- 6 files changed, 214 insertions(+), 75 deletions(-) create mode 100644 bberg/src/permutation_builder.rs diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs index d868806898..66499f35a0 100644 --- a/bberg/src/circuit_builder.rs +++ b/bberg/src/circuit_builder.rs @@ -9,22 +9,26 @@ pub trait CircuitBuilder { &mut self, name: &str, relations: &[String], + permutations: &[String], fixed: &[String], shifted: &[String], all_cols_with_shifts: &[String], ); } -fn circuit_hpp_includes(name: &str, relations: &[String]) -> String { - let relation_imports = get_relations_imports(name, relations); +fn circuit_hpp_includes(name: &str, relations: &[String], permutations: &[String]) -> String { + let relation_imports = get_relations_imports(name, relations, permutations); format!( " // AUTOGENERATED FILE #pragma once + #include \"barretenberg/common/constexpr_utils.hpp\" #include \"barretenberg/common/throw_or_abort.hpp\" #include \"barretenberg/ecc/curves/bn254/fr.hpp\" #include \"barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp\" + #include \"barretenberg/relations/generic_permutation/generic_permutation_relation.hpp\" + #include \"barretenberg/honk/proof_system/logderivative_library.hpp\" #include \"barretenberg/flavor/generated/{name}_flavor.hpp\" {relation_imports} @@ -32,6 +36,23 @@ fn circuit_hpp_includes(name: &str, relations: &[String]) -> String { ) } +fn get_params() -> &'static str { + r#" + const FF gamma = FF::random_element(); + const FF beta = FF::random_element(); + proof_system::RelationParameters params{ + .eta = 0, + .beta = beta, + .gamma = gamma, + .public_input_delta = 0, + .lookup_grand_product_delta = 0, + .beta_sqr = 0, + .beta_cube = 0, + .eccvm_set_permutation_delta = 0, + }; + "# +} + impl CircuitBuilder for BBFiles { // Create circuit builder // Generate some code that can read a commits.bin and constants.bin into data structures that bberg understands @@ -39,11 +60,12 @@ impl CircuitBuilder for BBFiles { &mut self, name: &str, relations: &[String], + permutations: &[String], all_cols: &[String], to_be_shifted: &[String], all_cols_with_shifts: &[String], ) { - let includes = circuit_hpp_includes(name, relations); + let includes = circuit_hpp_includes(name, relations, permutations); let row_with_all_included = create_row_type(&format!("{name}Full"), all_cols_with_shifts); @@ -64,12 +86,23 @@ impl CircuitBuilder for BBFiles { relation_name = relation_name ) }; + let check_permutation_transformation = |permutation_name: &String| { + format!( + "if (!evaluate_permutation.template operator()>(\"{permutation_name}\")) {{ + return false; + }}", + permutation_name = permutation_name + ) + }; // Apply transformations + let params = get_params(); let compute_polys_assignemnt = map_with_newline(all_cols, compute_polys_transformation); let all_poly_shifts = map_with_newline(to_be_shifted, all_polys_transformation); let check_circuit_for_each_relation = map_with_newline(relations, check_circuit_transformation); + let check_circuit_for_each_permutation = + map_with_newline(permutations, check_permutation_transformation); let circuit_hpp = format!(" {includes} @@ -116,6 +149,8 @@ class {name}CircuitBuilder {{ [[maybe_unused]] bool check_circuit() {{ + {params} + auto polys = compute_polynomials(); const size_t num_rows = polys.get_polynomial_size(); @@ -144,8 +179,37 @@ class {name}CircuitBuilder {{ return true; }}; + const auto evaluate_permutation = [&](const std::string& permutation_name) {{ + + // Check the tuple permutation relation + proof_system::honk::logderivative_library::compute_logderivative_inverse< + Flavor, + PermutationSettings>( + polys, params, num_rows); + + typename PermutationSettings::SumcheckArrayOfValuesOverSubrelations + permutation_result; + + for (auto& r : permutation_result) {{ + r = 0; + }} + for (size_t i = 0; i < num_rows; ++i) {{ + PermutationSettings::accumulate(permutation_result, polys.get_row(i), params, 1); + }} + for (auto r : permutation_result) {{ + if (r != 0) {{ + info(\"Tuple\", permutation_name, \"failed.\"); + return false; + }} + }} + return true; + }}; + + {check_circuit_for_each_relation} + {check_circuit_for_each_permutation} + return true; }} diff --git a/bberg/src/flavor_builder.rs b/bberg/src/flavor_builder.rs index 4c42d8dbaf..d95d752092 100644 --- a/bberg/src/flavor_builder.rs +++ b/bberg/src/flavor_builder.rs @@ -1,6 +1,6 @@ use crate::{ file_writer::BBFiles, - utils::{get_relations_imports, map_with_newline}, + utils::{get_relations_imports, map_with_newline}, vm_builder::{Permutation, get_inverses_from_permutations}, }; pub trait FlavorBuilder { @@ -9,6 +9,7 @@ pub trait FlavorBuilder { &mut self, name: &str, relation_file_names: &[String], + permutations: &[Permutation], fixed: &[String], witness: &[String], all_cols: &[String], @@ -24,6 +25,7 @@ impl FlavorBuilder for BBFiles { &mut self, name: &str, relation_file_names: &[String], + permutations: &[Permutation], fixed: &[String], witness: &[String], all_cols: &[String], @@ -31,15 +33,18 @@ impl FlavorBuilder for BBFiles { shifted: &[String], all_cols_and_shifts: &[String], ) { + // TODO: move elsewhere and rename + let inverses = get_inverses_from_permutations(permutations); + let first_poly = &witness[0]; - let includes = flavor_includes(name, relation_file_names); + let includes = flavor_includes(name, relation_file_names, &inverses); let num_precomputed = fixed.len(); let num_witness = witness.len(); let num_all = all_cols_and_shifts.len(); // Top of file boilerplate let class_aliases = create_class_aliases(); - let relation_definitions = create_relation_definitions(name, relation_file_names); + let relation_definitions = create_relation_definitions(name, relation_file_names, permutations); let container_size_definitions = container_size_definitions(num_precomputed, num_witness, num_all); @@ -107,8 +112,8 @@ class {name}Flavor {{ } /// Imports located at the top of the flavor files -fn flavor_includes(name: &str, relation_file_names: &[String]) -> String { - let relation_imports = get_relations_imports(name, relation_file_names); +fn flavor_includes(name: &str, relation_file_names: &[String], permutations: &[String]) -> String { + let relation_imports = get_relations_imports(name, relation_file_names, permutations); format!( " @@ -119,6 +124,8 @@ fn flavor_includes(name: &str, relation_file_names: &[String]) -> String { #include \"barretenberg/polynomials/barycentric.hpp\" #include \"barretenberg/polynomials/univariate.hpp\" +#include \"barretenberg/relations/generic_permutation/generic_permutation_relation.hpp\" + #include \"barretenberg/flavor/flavor_macros.hpp\" #include \"barretenberg/transcript/transcript.hpp\" #include \"barretenberg/polynomials/evaluation_domain.hpp\" @@ -138,6 +145,18 @@ fn create_relations_tuple(master_name: &str, relation_file_names: &[String]) -> .join(", ") } +/// Creates comma separated relations tuple file +/// TODO(md): maybe need the filename in here too if we scope these +fn create_permutations_tuple(permutations: &[Permutation]) -> String { + permutations + .iter() + .map(|perm| + format!("sumcheck::{}", perm.attribute.clone().unwrap() + )) + .collect::>() + .join(", ") +} + /// Create Class Aliases /// /// Contains boilerplate defining key characteristics of the flavor class @@ -165,12 +184,14 @@ fn create_class_aliases() -> &'static str { /// definitions. /// /// We then also define some constants, making use of the preprocessor. -fn create_relation_definitions(name: &str, relation_file_names: &[String]) -> String { +fn create_relation_definitions(name: &str, relation_file_names: &[String], permutations: &[Permutation]) -> String { // Relations tuple = ns::relation_name_0, ns::relation_name_1, ... ns::relation_name_n (comma speratated) let comma_sep_relations = create_relations_tuple(name, relation_file_names); + let comma_sep_perms: String = create_permutations_tuple(permutations); + let all_relations = format!("{comma_sep_relations}, {comma_sep_perms}"); format!(" - using Relations = std::tuple<{comma_sep_relations}>; + using Relations = std::tuple<{all_relations}>; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); diff --git a/bberg/src/permutation_builder.rs b/bberg/src/permutation_builder.rs new file mode 100644 index 0000000000..e69de29bb2 diff --git a/bberg/src/prover_builder.rs b/bberg/src/prover_builder.rs index 9f35ecc8d9..b7eff21811 100644 --- a/bberg/src/prover_builder.rs +++ b/bberg/src/prover_builder.rs @@ -237,7 +237,7 @@ fn includes_cpp(name: &str) -> String { #include \"{name}_prover.hpp\" #include \"barretenberg/commitment_schemes/claim.hpp\" #include \"barretenberg/commitment_schemes/commitment_key.hpp\" - #include \"barretenberg/honk/proof_system/lookup_library.hpp\" + #include \"barretenberg/honk/proof_system/logderivative_library.hpp\" #include \"barretenberg/honk/proof_system/permutation_library.hpp\" #include \"barretenberg/honk/proof_system/power_polynomial.hpp\" #include \"barretenberg/polynomials/polynomial.hpp\" diff --git a/bberg/src/utils.rs b/bberg/src/utils.rs index 6bbb4e43db..676c3fac1d 100644 --- a/bberg/src/utils.rs +++ b/bberg/src/utils.rs @@ -4,12 +4,13 @@ use number::FieldElement; /// /// We may have multiple relation files in the generated foler /// This method will return all of the imports for the relation header files -pub fn get_relations_imports(name: &str, relations: &[String]) -> String { +pub fn get_relations_imports(name: &str, relations: &[String], permutations: &[String]) -> String { + let all_relations = flatten(&[relations.to_vec(), permutations.to_vec()]); let transformation = |relation_name: &_| { format!("#include \"barretenberg/relations/generated/{name}/{relation_name}.hpp\"") }; - map_with_newline(relations, transformation) + map_with_newline(&all_relations, transformation) } /// Sanitize Names diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index 759ea130c2..346b5b2173 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -14,6 +14,7 @@ use crate::composer_builder::ComposerBuilder; use crate::file_writer::BBFiles; use crate::flavor_builder::FlavorBuilder; use crate::prover_builder::ProverBuilder; +use crate::relation_builder; use crate::relation_builder::{create_identities, create_row_type, RelationBuilder}; use crate::utils::capitalize; use crate::utils::collect_col; @@ -52,11 +53,9 @@ pub(crate) fn analyzed_to_cpp( } = create_relation_files(&bb_files, file_name, &analyzed_identities); // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- - // We will likely need to create a new set of permutation identities for each lookup / permutation pair we come across - handle_permutations(analyzed); - // handle_lookups(); - - + let permutations = handle_permutations(&bb_files, file_name, analyzed); + let inverses = get_inverses_from_permutations(&permutations); + // TODO: may need to merge the perm_inverses for the flavor // TODO: hack - this can be removed with some restructuring let shifted_polys: Vec = shifted_polys @@ -74,42 +73,47 @@ pub(crate) fn analyzed_to_cpp( to_be_shifted, shifted, all_cols_with_shifts, - } = get_all_col_names(fixed, witness, &shifted_polys); - - // bb_files.create_declare_views(file_name, &all_cols_with_shifts); - - // // ----------------------- Create the circuit builder file ----------------------- - // bb_files.create_circuit_builder_hpp( - // file_name, - // &relations, - // &all_cols, - // &to_be_shifted, - // &all_cols_with_shifts, - // ); - - // // ----------------------- Create the flavor file ----------------------- - // bb_files.create_flavor_hpp( - // file_name, - // &relations, - // &fixed, - // &witness, - // &all_cols, - // &to_be_shifted, - // &shifted, - // &all_cols_with_shifts, - // ); - - // // ----------------------- Create the composer files ----------------------- - // bb_files.create_composer_cpp(file_name, &all_cols); - // bb_files.create_composer_hpp(file_name); - - // // ----------------------- Create the Verifier files ----------------------- - // bb_files.create_verifier_cpp(file_name, &witness); - // bb_files.create_verifier_hpp(file_name); - - // // ----------------------- Create the Prover files ----------------------- - // bb_files.create_prover_cpp(file_name, &unshifted, &to_be_shifted); - // bb_files.create_prover_hpp(file_name); + } = get_all_col_names(fixed, witness, &shifted_polys, &permutations); + + dbg!(&fixed); + dbg!(&witness); + + bb_files.create_declare_views(file_name, &all_cols_with_shifts); + + // ----------------------- Create the circuit builder file ----------------------- + bb_files.create_circuit_builder_hpp( + file_name, + &relations, + &inverses, + &all_cols, + &to_be_shifted, + &all_cols_with_shifts, + ); + + // ----------------------- Create the flavor file ----------------------- + bb_files.create_flavor_hpp( + file_name, + &relations, + &permutations, + &fixed, + &witness, + &all_cols, + &to_be_shifted, + &shifted, + &all_cols_with_shifts, + ); + + // ----------------------- Create the composer files ----------------------- + bb_files.create_composer_cpp(file_name, &all_cols); + bb_files.create_composer_hpp(file_name); + + // ----------------------- Create the Verifier files ----------------------- + bb_files.create_verifier_cpp(file_name, &witness); + bb_files.create_verifier_hpp(file_name); + + // ----------------------- Create the Prover files ----------------------- + bb_files.create_prover_cpp(file_name, &unshifted, &to_be_shifted); + bb_files.create_prover_hpp(file_name); } @@ -162,25 +166,30 @@ fn create_relation_files(bb_files: &BBFiles, file_name: &str, a } -// Maybe this is not the right thing to do? +// TODO(md): move permutation related code into its own home #[derive(Debug)] -struct Permutation { +pub struct Permutation { /// Attribute in this setting is used to determine what the name of the inverse column should be /// TODO(md): Future implementations should use this to allow using the same inverse column multiple times, thus /// allowing granularity in the logup trade-off - attribute: Option, - left: PermSide, - right: PermSide + pub attribute: Option, + pub left: PermSide, + pub right: PermSide +} + +/// The attributes of a permutation contain the name of the inverse, we collect all of these to create the inverse column +pub fn get_inverses_from_permutations(permutations: &[Permutation]) -> Vec { + permutations.iter().map(|perm| perm.attribute.clone().unwrap()).collect() } // TODO: rename #[derive(Debug)] -struct PermSide { +pub struct PermSide { selector: Option, cols: Vec } -fn handle_permutations(analyzed: &Analyzed) { +fn handle_permutations(bb_files: &BBFiles, project_name: &str, analyzed: &Analyzed) -> Vec { let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); let new_perms = perms.iter().map(|perm| Permutation { @@ -193,22 +202,57 @@ fn handle_permutations(analyzed: &Analyzed) { // For every permutation set that we create, we will need to create an inverse column ( helper function ) // TODO: how do we determine the name of this inverse column? - create_permutations(new_perms); + create_permutations(bb_files, &project_name, &new_perms); + new_perms } -fn create_permutations(permutations: Vec) { +fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Vec) { for permutation in permutations { - create_permutation_settings_file(permutation); + let perm_settings = create_permutation_settings_file(permutation); + + // TODO: temp this is not going to be the final configuration, maybe we use the trait construction again to have access to bb + let folder = format!("{}/{}", bb_files.rel, project_name); + let file_name = format!("{}{}", permutation.attribute.clone().unwrap_or("NONAME".to_owned()), ".hpp".to_owned()); + bb_files.write_file(&folder, &file_name, &perm_settings); } } -fn create_permutation_settings_file(permutation: Permutation) -> String { +/// All relation types eventually get wrapped in the relation type +/// This function creates the export for the relation type so that it can be added to the flavor +fn create_relation_exporter(permutation_name: &str) -> String { + let name = format!("{}_permutation_settings", permutation_name); + + let class_export = format!("template class GenericPermutationRelationImpl<{name}, barretenberg::fr>;"); + let template_export = format!("template using Generic{permutation_name} = GenericPermutationRelationImpl<{name}, FF_>;",); + let relation_export = format!("template using {permutation_name} = Relation>;"); + + format!(" + {class_export} + + {template_export} + + {relation_export} + ") +} + +fn permutation_settings_includes() -> &'static str { + r#" + #pragma once + + #include "barretenberg/relations/generic_permutation/generic_permutation_relation.hpp" + + #include + #include + "# +} + +fn create_permutation_settings_file(permutation: &Permutation) -> String { println!("Permutation: {:?}", permutation); let columns_per_set = permutation.left.cols.len(); // TODO(md): Throw an error if no attribute is provided for the permutation // TODO(md): In the future we will need to condense off the back of this - combining those with the same inverse column - let inverse_column_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here + let permutation_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here // NOTE: syntax is not flexible enough to enable the single row case right now :(:(:(:(:)))) // This also will need to work for both sides of this ! @@ -223,7 +267,7 @@ fn create_permutation_settings_file(permutation: Permutation) -> String { // 4.. + columns per set. lhs cols // 4 + columns per set.. . rhs cols let mut perm_entities: Vec = [ - inverse_column_name, + permutation_name.clone(), selector.clone(), selector.clone(), selector.clone() // TODO: update this away from the simple example @@ -234,19 +278,22 @@ fn create_permutation_settings_file(permutation: Permutation) -> String { // TODO: below here should really be in a new function as we have just got the settings extracted from the parsed type + let permutation_settings_includes = permutation_settings_includes(); let inverse_computed_at = create_inverse_computed_at(selector); let const_entities = create_get_const_entities(&perm_entities); let nonconst_entities = create_get_nonconst_entities(&perm_entities); - + let relation_exporter = create_relation_exporter(&permutation_name); format!( // TODO: replace with the inverse label name! " - class ExampleTuplePermutationSettings {{ + {permutation_settings_includes} + + namespace proof_system::honk::sumcheck {{ + + class {permutation_name}_permutation_settings {{ public: - // This constant defines how many columns are bundled together to form each set. For example, in this case we are - // bundling tuples of (permutation_set_column_1, permutation_set_column_2) to be a permutation of - // (permutation_set_column_3,permutation_set_column_4). As the tuple has 2 elements, set the value to 2 + // This constant defines how many columns are bundled together to form each set. constexpr static size_t COLUMNS_PER_SET = {columns_per_set}; /** @@ -254,7 +301,6 @@ fn create_permutation_settings_file(permutation: Permutation) -> String { * value needs to be set to zero. * * @details If this is true then permutation takes place in this row - * */ {inverse_computed_at} @@ -293,7 +339,10 @@ fn create_permutation_settings_file(permutation: Permutation) -> String { * @return All the entities needed for the permutation */ {nonconst_entities} - }} + }}; + + {relation_exporter} + }} " ) @@ -330,7 +379,7 @@ fn create_get_nonconst_entities (settings: &[String]) -> String { fn create_forward_as_tuple(settings: &[String]) -> String { - let adjusted = settings.iter().map(|col| format!("in.{col},\n")).join(""); + let adjusted = settings.iter().map(|col| format!("in.{col}")).join(",\n"); format!(" return std::forward_as_tuple( {} @@ -402,14 +451,18 @@ fn get_all_col_names( fixed: &[(String, Vec)], witness: &[(String, Vec)], to_be_shifted: &[String], + permutations: &[Permutation], ) -> ColumnGroups { // Transformations let sanitize = |(name, _): &(String, Vec)| sanitize_name(name).to_owned(); let append_shift = |name: &String| format!("{}_shift", *name); + let perm_inverses = get_inverses_from_permutations(permutations); + // Gather sanitized column names let fixed_names = collect_col(fixed, sanitize); let witness_names = collect_col(witness, sanitize); + let witness_names = flatten(&[witness_names, perm_inverses]); // Group columns by properties let shifted = transform_map(to_be_shifted, append_shift); From 543404af2eca48b69bc998f76519bcf1e851605c Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Mon, 11 Dec 2023 17:12:24 +0000 Subject: [PATCH 05/10] chore: permutation builder refactor --- bberg/src/flavor_builder.rs | 21 ++- bberg/src/lib.rs | 1 + bberg/src/permutation_builder.rs | 243 ++++++++++++++++++++++++++++ bberg/src/relation_builder.rs | 5 +- bberg/src/vm_builder.rs | 266 ++----------------------------- 5 files changed, 283 insertions(+), 253 deletions(-) diff --git a/bberg/src/flavor_builder.rs b/bberg/src/flavor_builder.rs index d95d752092..09b93046c9 100644 --- a/bberg/src/flavor_builder.rs +++ b/bberg/src/flavor_builder.rs @@ -1,6 +1,6 @@ use crate::{ file_writer::BBFiles, - utils::{get_relations_imports, map_with_newline}, vm_builder::{Permutation, get_inverses_from_permutations}, + utils::{get_relations_imports, map_with_newline}, permutation_builder::{Permutation, get_inverses_from_permutations}, }; pub trait FlavorBuilder { @@ -63,6 +63,8 @@ impl FlavorBuilder for BBFiles { let transcript = generate_transcript(witness); + let declare_permutation_sumcheck = create_permuation_sumcheck_declaration(&inverses, name); + let flavor_hpp = format!( " {includes} @@ -101,6 +103,10 @@ class {name}Flavor {{ }}; }} // namespace proof_system::honk::flavor + +namespace sumcheck {{ + {declare_permutation_sumcheck} +}} }} // namespace proof_system::honk @@ -545,3 +551,16 @@ fn generate_transcript(witness: &[String]) -> String { }}; ") } + + +fn create_permuation_sumcheck_declaration(permutations: &[String], name: &str) -> String { + let sumcheck_transformation = |perm: &String| { + format!( + " + DECLARE_SUMCHECK_RELATION_CLASS({perm}, flavor::{name}Flavor); + ", + ) + }; + + map_with_newline(permutations, sumcheck_transformation) +} \ No newline at end of file diff --git a/bberg/src/lib.rs b/bberg/src/lib.rs index ba9ac632dd..0682b25107 100644 --- a/bberg/src/lib.rs +++ b/bberg/src/lib.rs @@ -3,6 +3,7 @@ mod circuit_builder; mod composer_builder; mod file_writer; mod flavor_builder; +pub mod permutation_builder; mod prover_builder; mod relation_builder; mod utils; diff --git a/bberg/src/permutation_builder.rs b/bberg/src/permutation_builder.rs index e69de29bb2..774f837cb4 100644 --- a/bberg/src/permutation_builder.rs +++ b/bberg/src/permutation_builder.rs @@ -0,0 +1,243 @@ +use ast::{analyzed::{Analyzed, AlgebraicExpression, Identity, IdentityKind}, parsed::SelectedExpressions}; +use crate::file_writer::BBFiles; +use itertools::Itertools; +use number::FieldElement; + +use crate::utils::sanitize_name; + +#[derive(Debug)] +/// Permutation +/// +/// Contains the information required to produce a permutation relation +pub struct Permutation { + /// -> Attribute - the name given to the inverse helper column + pub attribute: Option, + /// -> PermSide - the left side of the permutation + pub left: PermutationSide, + /// -> PermSide - the right side of the permutation + pub right: PermutationSide +} + +#[derive(Debug)] +/// PermSide +/// +/// One side of a two sided permutation relationship +pub struct PermutationSide { + /// -> Option - the selector for the permutation ( on / off toggle ) + selector: Option, + /// The columns involved in this side of the permutation + cols: Vec +} + +pub trait PermutationBuilder { + /// Takes in an AST and works out what permutation relations are needed + /// Note: returns the name of the inverse columns, such that they can be added to he prover in subsequent steps + fn create_permutation_files(&self, name: &str, analyzed: &Analyzed)-> Vec; +} + +impl PermutationBuilder for BBFiles { + fn create_permutation_files(&self, project_name: &str, analyzed: &Analyzed) -> Vec { + let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); + let new_perms = perms.iter().map(|perm| + Permutation { + attribute: perm.attribute.clone(), + left: get_perm_side(&perm.left), + right: get_perm_side(&perm.right) + }).collect_vec(); + + create_permutations(self, project_name,&new_perms); + new_perms + } +} + +/// The attributes of a permutation contain the name of the inverse, we collect all of these to create the inverse column +pub fn get_inverses_from_permutations(permutations: &[Permutation]) -> Vec { + permutations.iter().map(|perm| perm.attribute.clone().unwrap()).collect() +} + +/// Write the permutation settings files to disk +fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Vec) { + for permutation in permutations { + let perm_settings = create_permutation_settings_file(permutation); + + // TODO: temp this is not going to be the final configuration, maybe we use the trait construction again to have access to bb + let folder = format!("{}/{}", bb_files.rel, project_name); + let file_name = format!("{}{}", permutation.attribute.clone().unwrap_or("NONAME".to_owned()), ".hpp".to_owned()); + bb_files.write_file(&folder, &file_name, &perm_settings); + } +} + +/// All relation types eventually get wrapped in the relation type +/// This function creates the export for the relation type so that it can be added to the flavor +fn create_relation_exporter(permutation_name: &str) -> String { + let settings_name = format!("{}_permutation_settings", permutation_name); + let relation_export = format!("template using {permutation_name} = GenericPermutationRelation<{settings_name}, FF_>;"); + + format!(" + {relation_export} + ") +} + +fn permutation_settings_includes() -> &'static str { + r#" + #pragma once + + #include "barretenberg/relations/generic_permutation/generic_permutation_relation.hpp" + + #include + #include + "# +} + +fn create_permutation_settings_file(permutation: &Permutation) -> String { + + println!("Permutation: {:?}", permutation); + let columns_per_set = permutation.left.cols.len(); + // TODO(md): Throw an error if no attribute is provided for the permutation + // TODO(md): In the future we will need to condense off the back of this - combining those with the same inverse column + let permutation_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here + + // NOTE: syntax is not flexible enough to enable the single row case right now :(:(:(:(:)))) + // This also will need to work for both sides of this ! + let selector = permutation.left.selector.clone().unwrap(); // TODO: deal with unwrap + let lhs_cols = permutation.left.cols.clone(); + let rhs_cols = permutation.right.cols.clone(); + + // 0. The polynomial containing the inverse products -> taken from the attributes + // 1. The polynomial enabling the relation (the selector) + // 2. lhs selector + // 3. rhs selector + // 4.. + columns per set. lhs cols + // 4 + columns per set.. . rhs cols + let mut perm_entities: Vec = [ + permutation_name.clone(), + selector.clone(), + selector.clone(), + selector.clone() // TODO: update this away from the simple example + ].to_vec(); + + perm_entities.extend(lhs_cols); + perm_entities.extend(rhs_cols); + + + // TODO: below here should really be in a new function as we have just got the settings extracted from the parsed type + let permutation_settings_includes = permutation_settings_includes(); + let inverse_computed_at = create_inverse_computed_at(selector); + let const_entities = create_get_const_entities(&perm_entities); + let nonconst_entities = create_get_nonconst_entities(&perm_entities); + let relation_exporter = create_relation_exporter(&permutation_name); + + format!( + // TODO: replace with the inverse label name! + " + {permutation_settings_includes} + + namespace proof_system::honk::sumcheck {{ + + class {permutation_name}_permutation_settings {{ + public: + // This constant defines how many columns are bundled together to form each set. + constexpr static size_t COLUMNS_PER_SET = {columns_per_set}; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the + * value needs to be set to zero. + * + * @details If this is true then permutation takes place in this row + */ + {inverse_computed_at} + + /** + * @brief Get all the entities for the permutation when we don't need to update them + * + * @details The entities are returned as a tuple of references in the following order: + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of + * the inverse polynomial + * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum + * subrelation + * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum + * subrelation + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) + * + * @return All the entities needed for the permutation + */ + {const_entities} + + /** + * @brief Get all the entities for the permutation when need to update them + * + * @details The entities are returned as a tuple of references in the following order: + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of + * the inverse polynomial + * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum + * subrelation + * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum + * subrelation + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) + * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) + * + * @return All the entities needed for the permutation + */ + {nonconst_entities} + }}; + + {relation_exporter} + }} + " + ) + +} + + + +// TODO: make this dynamic such that there can be more than one +fn create_inverse_computed_at(inverse_selector: String) -> String { + let inverse_computed_selector = format!("in.{inverse_selector}"); + format!(" + template static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in) {{ + return ({inverse_computed_selector} == 1); + }}") +} + +fn create_get_const_entities (settings: &[String]) -> String { + let forward = create_forward_as_tuple(settings); + format!(" + template static inline auto get_const_entities(const AllEntities& in) {{ + {forward} + }} + ") +} + +fn create_get_nonconst_entities (settings: &[String]) -> String { + let forward = create_forward_as_tuple(settings); + format!(" + template static inline auto get_nonconst_entities(AllEntities& in) {{ + {forward} + }} + ") +} + + +fn create_forward_as_tuple(settings: &[String]) -> String { + let adjusted = settings.iter().map(|col| format!("in.{col}")).join(",\n"); + format!(" + return std::forward_as_tuple( + {} + ); + ", adjusted) +} + +fn get_perm_side(def: &SelectedExpressions>) -> PermutationSide { + let get_name = |expr: &AlgebraicExpression| match expr { + AlgebraicExpression::Reference(a_ref) => sanitize_name(&a_ref.name), + _ => panic!("Expected reference") + }; + + PermutationSide { + selector: def.selector.as_ref().map(|expr| get_name(&expr)), + cols: def.expressions.iter().map(|expr| get_name(&expr)).collect_vec() + } +} \ No newline at end of file diff --git a/bberg/src/relation_builder.rs b/bberg/src/relation_builder.rs index 811c8d66f7..ba7aeb2a23 100644 --- a/bberg/src/relation_builder.rs +++ b/bberg/src/relation_builder.rs @@ -67,7 +67,7 @@ namespace proof_system::{root_name}_vm {{ let declare_views = format!( " - #define DECLARE_VIEWS(index) \\ + #define {name}_DECLARE_VIEWS(index) \\ using Accumulator = typename std::tuple_element::type; \\ using View = typename Accumulator::View; \\ {make_view_per_row} @@ -251,6 +251,7 @@ fn craft_expression( } pub(crate) fn create_identities( + file_name: &str, identities: &[Identity>], ) -> (Vec, Vec, Vec, Vec) { // We only want the expressions for now @@ -273,7 +274,7 @@ pub(crate) fn create_identities( for (i, expression) in expressions.iter().enumerate() { let relation_boilerplate = format!( - "DECLARE_VIEWS({i}); + "{file_name}_DECLARE_VIEWS({i}); ", ); // TODO: deal with unwrap diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index 346b5b2173..f0b1b2e963 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -4,8 +4,6 @@ use ast::analyzed::AlgebraicExpression; use ast::analyzed::Analyzed; use ast::analyzed::Identity; -use ast::analyzed::IdentityKind; -use ast::parsed::SelectedExpressions; use itertools::Itertools; use number::FieldElement; @@ -13,8 +11,10 @@ use crate::circuit_builder::CircuitBuilder; use crate::composer_builder::ComposerBuilder; use crate::file_writer::BBFiles; use crate::flavor_builder::FlavorBuilder; +use crate::permutation_builder::Permutation; +use crate::permutation_builder::PermutationBuilder; +use crate::permutation_builder::get_inverses_from_permutations; use crate::prover_builder::ProverBuilder; -use crate::relation_builder; use crate::relation_builder::{create_identities, create_row_type, RelationBuilder}; use crate::utils::capitalize; use crate::utils::collect_col; @@ -23,16 +23,27 @@ use crate::utils::sanitize_name; use crate::utils::transform_map; use crate::verifier_builder::VerifierBuilder; +/// All of the combinations of columns that are used in a bberg flavor file struct ColumnGroups { + /// fixed or constant columns in pil -> will be found in vk fixed: Vec, + /// witness or commit columns in pil -> will be found in proof witness: Vec, + /// fixed + witness columns all_cols: Vec, + /// Columns that will not be shifted unshifted: Vec, + /// Columns that will be shifted to_be_shifted: Vec, + /// The shifts of the columns that will be shifted shifted: Vec, + /// fixed + witness + shifted all_cols_with_shifts: Vec, } +/// Analyzed to cpp +/// +/// Converts an analyzed pil AST into a set of cpp files that can be used to generate a proof pub(crate) fn analyzed_to_cpp( analyzed: &Analyzed, fixed: &[(String, Vec)], @@ -53,9 +64,8 @@ pub(crate) fn analyzed_to_cpp( } = create_relation_files(&bb_files, file_name, &analyzed_identities); // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- - let permutations = handle_permutations(&bb_files, file_name, analyzed); + let permutations = bb_files.create_permutation_files(file_name, analyzed); let inverses = get_inverses_from_permutations(&permutations); - // TODO: may need to merge the perm_inverses for the flavor // TODO: hack - this can be removed with some restructuring let shifted_polys: Vec = shifted_polys @@ -75,9 +85,6 @@ pub(crate) fn analyzed_to_cpp( all_cols_with_shifts, } = get_all_col_names(fixed, witness, &shifted_polys, &permutations); - dbg!(&fixed); - dbg!(&witness); - bb_files.create_declare_views(file_name, &all_cols_with_shifts); // ----------------------- Create the circuit builder file ----------------------- @@ -139,7 +146,7 @@ fn create_relation_files(bb_files: &BBFiles, file_name: &str, a for (relation_name, analyzed_idents) in grouped_relations.iter() { // TODO: make this more granular instead of doing everything at once let (subrelations, identities, collected_polys, collected_shifts) = - create_identities(analyzed_idents); + create_identities(file_name,analyzed_idents); shifted_polys.extend(collected_shifts); @@ -166,247 +173,6 @@ fn create_relation_files(bb_files: &BBFiles, file_name: &str, a } -// TODO(md): move permutation related code into its own home -#[derive(Debug)] -pub struct Permutation { - /// Attribute in this setting is used to determine what the name of the inverse column should be - /// TODO(md): Future implementations should use this to allow using the same inverse column multiple times, thus - /// allowing granularity in the logup trade-off - pub attribute: Option, - pub left: PermSide, - pub right: PermSide -} - -/// The attributes of a permutation contain the name of the inverse, we collect all of these to create the inverse column -pub fn get_inverses_from_permutations(permutations: &[Permutation]) -> Vec { - permutations.iter().map(|perm| perm.attribute.clone().unwrap()).collect() -} - -// TODO: rename -#[derive(Debug)] -pub struct PermSide { - selector: Option, - cols: Vec -} - -fn handle_permutations(bb_files: &BBFiles, project_name: &str, analyzed: &Analyzed) -> Vec { - let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); - let new_perms = perms.iter().map(|perm| - Permutation { - attribute: perm.attribute.clone(), - left: get_perm_side(&perm.left), - right: get_perm_side(&perm.right) - }).collect_vec(); - dbg!(&new_perms); - - // For every permutation set that we create, we will need to create an inverse column ( helper function ) - // TODO: how do we determine the name of this inverse column? - - create_permutations(bb_files, &project_name, &new_perms); - new_perms -} - -fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Vec) { - for permutation in permutations { - let perm_settings = create_permutation_settings_file(permutation); - - // TODO: temp this is not going to be the final configuration, maybe we use the trait construction again to have access to bb - let folder = format!("{}/{}", bb_files.rel, project_name); - let file_name = format!("{}{}", permutation.attribute.clone().unwrap_or("NONAME".to_owned()), ".hpp".to_owned()); - bb_files.write_file(&folder, &file_name, &perm_settings); - } -} - -/// All relation types eventually get wrapped in the relation type -/// This function creates the export for the relation type so that it can be added to the flavor -fn create_relation_exporter(permutation_name: &str) -> String { - let name = format!("{}_permutation_settings", permutation_name); - - let class_export = format!("template class GenericPermutationRelationImpl<{name}, barretenberg::fr>;"); - let template_export = format!("template using Generic{permutation_name} = GenericPermutationRelationImpl<{name}, FF_>;",); - let relation_export = format!("template using {permutation_name} = Relation>;"); - - format!(" - {class_export} - - {template_export} - - {relation_export} - ") -} - -fn permutation_settings_includes() -> &'static str { - r#" - #pragma once - - #include "barretenberg/relations/generic_permutation/generic_permutation_relation.hpp" - - #include - #include - "# -} - -fn create_permutation_settings_file(permutation: &Permutation) -> String { - - println!("Permutation: {:?}", permutation); - let columns_per_set = permutation.left.cols.len(); - // TODO(md): Throw an error if no attribute is provided for the permutation - // TODO(md): In the future we will need to condense off the back of this - combining those with the same inverse column - let permutation_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here - - // NOTE: syntax is not flexible enough to enable the single row case right now :(:(:(:(:)))) - // This also will need to work for both sides of this ! - let selector = permutation.left.selector.clone().unwrap(); // TODO: deal with unwrap - let lhs_cols = permutation.left.cols.clone(); - let rhs_cols = permutation.right.cols.clone(); - - // 0. The polynomial containing the inverse products -> taken from the attributes - // 1. The polynomial enabling the relation (the selector) - // 2. lhs selector - // 3. rhs selector - // 4.. + columns per set. lhs cols - // 4 + columns per set.. . rhs cols - let mut perm_entities: Vec = [ - permutation_name.clone(), - selector.clone(), - selector.clone(), - selector.clone() // TODO: update this away from the simple example - ].to_vec(); - - perm_entities.extend(lhs_cols); - perm_entities.extend(rhs_cols); - - - // TODO: below here should really be in a new function as we have just got the settings extracted from the parsed type - let permutation_settings_includes = permutation_settings_includes(); - let inverse_computed_at = create_inverse_computed_at(selector); - let const_entities = create_get_const_entities(&perm_entities); - let nonconst_entities = create_get_nonconst_entities(&perm_entities); - let relation_exporter = create_relation_exporter(&permutation_name); - - format!( - // TODO: replace with the inverse label name! - " - {permutation_settings_includes} - - namespace proof_system::honk::sumcheck {{ - - class {permutation_name}_permutation_settings {{ - public: - // This constant defines how many columns are bundled together to form each set. - constexpr static size_t COLUMNS_PER_SET = {columns_per_set}; - - /** - * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the - * value needs to be set to zero. - * - * @details If this is true then permutation takes place in this row - */ - {inverse_computed_at} - - /** - * @brief Get all the entities for the permutation when we don't need to update them - * - * @details The entities are returned as a tuple of references in the following order: - * - The entity/polynomial used to store the product of the inverse values - * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of - * the inverse polynomial - * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum - * subrelation - * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum - * subrelation - * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) - * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) - * - * @return All the entities needed for the permutation - */ - {const_entities} - - /** - * @brief Get all the entities for the permutation when need to update them - * - * @details The entities are returned as a tuple of references in the following order: - * - The entity/polynomial used to store the product of the inverse values - * - The entity/polynomial that switches on the subrelation of the permutation relation that ensures correctness of - * the inverse polynomial - * - The entity/polynomial that enables adding a tuple-generated value from the first set to the logderivative sum - * subrelation - * - The entity/polynomial that enables adding a tuple-generated value from the second set to the logderivative sum - * subrelation - * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the first set (N.B. ORDER IS IMPORTANT!) - * - A sequence of COLUMNS_PER_SET entities/polynomials that represent the second set (N.B. ORDER IS IMPORTANT!) - * - * @return All the entities needed for the permutation - */ - {nonconst_entities} - }}; - - {relation_exporter} - }} - " - ) - -} - - - -// TODO: make this dynamic such that there can be more than one -fn create_inverse_computed_at(inverse_selector: String) -> String { - let inverse_computed_selector = format!("in.{inverse_selector}"); - format!(" - template static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in) {{ - return ({inverse_computed_selector} == 1); - }}") -} - -fn create_get_const_entities (settings: &[String]) -> String { - let forward = create_forward_as_tuple(settings); - format!(" - template static inline auto get_const_entities(const AllEntities& in) {{ - {forward} - }} - ") -} - -fn create_get_nonconst_entities (settings: &[String]) -> String { - let forward = create_forward_as_tuple(settings); - format!(" - template static inline auto get_nonconst_entities(AllEntities& in) {{ - {forward} - }} - ") -} - - -fn create_forward_as_tuple(settings: &[String]) -> String { - let adjusted = settings.iter().map(|col| format!("in.{col}")).join(",\n"); - format!(" - return std::forward_as_tuple( - {} - ); - ", adjusted) -} - -fn get_perm_side(def: &SelectedExpressions>) -> PermSide { - let get_name = |expr: &AlgebraicExpression| match expr { - AlgebraicExpression::Reference(a_ref) => sanitize_name(&a_ref.name), - _ => panic!("Expected reference") - }; - - PermSide { - selector: def.selector.as_ref().map(|expr| get_name(&expr)), - cols: def.expressions.iter().map(|expr| get_name(&expr)).collect_vec() - } -} - - - -// pub struct SelectedExpressions { -// pub selector: Option, -// pub expressions: Vec, -// } - - /// Group relations per file /// From c0bbea7000385a8a20a3be8fa0514f4ed6ab33ed Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Mon, 11 Dec 2023 17:27:31 +0000 Subject: [PATCH 06/10] fix: account for instances with no permutations --- bberg/src/circuit_builder.rs | 127 +++++++++++++++++++++-------------- bberg/src/flavor_builder.rs | 5 +- 2 files changed, 80 insertions(+), 52 deletions(-) diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs index 66499f35a0..1a9926ad3e 100644 --- a/bberg/src/circuit_builder.rs +++ b/bberg/src/circuit_builder.rs @@ -96,7 +96,6 @@ impl CircuitBuilder for BBFiles { }; // Apply transformations - let params = get_params(); let compute_polys_assignemnt = map_with_newline(all_cols, compute_polys_transformation); let all_poly_shifts = map_with_newline(to_be_shifted, all_polys_transformation); let check_circuit_for_each_relation = @@ -104,6 +103,17 @@ impl CircuitBuilder for BBFiles { let check_circuit_for_each_permutation = map_with_newline(permutations, check_permutation_transformation); + let (params,permutation_check_closure) = if permutations.len() > 0 { + (get_params(), get_permutation_check_closure()) + } else { + ("", "".to_owned()) + }; + let relation_check_closure = if relations.len() > 0 { + get_relation_check_closure() + } else { + "".to_owned() + }; + let circuit_hpp = format!(" {includes} @@ -154,57 +164,9 @@ class {name}CircuitBuilder {{ auto polys = compute_polynomials(); const size_t num_rows = polys.get_polynomial_size(); - const auto evaluate_relation = [&](const std::string& relation_name) {{ - typename Relation::SumcheckArrayOfValuesOverSubrelations result; - for (auto& r : result) {{ - r = 0; - }} - constexpr size_t NUM_SUBRELATIONS = result.size(); - - for (size_t i = 0; i < num_rows; ++i) {{ - Relation::accumulate(result, polys.get_row(i), {{}}, 1); - - bool x = true; - for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) {{ - if (result[j] != 0) {{ - throw_or_abort( - format(\"Relation \", relation_name, \", subrelation index \", j, \" failed at row \", i)); - x = false; - }} - }} - if (!x) {{ - return false; - }} - }} - return true; - }}; - - const auto evaluate_permutation = [&](const std::string& permutation_name) {{ - - // Check the tuple permutation relation - proof_system::honk::logderivative_library::compute_logderivative_inverse< - Flavor, - PermutationSettings>( - polys, params, num_rows); - - typename PermutationSettings::SumcheckArrayOfValuesOverSubrelations - permutation_result; - - for (auto& r : permutation_result) {{ - r = 0; - }} - for (size_t i = 0; i < num_rows; ++i) {{ - PermutationSettings::accumulate(permutation_result, polys.get_row(i), params, 1); - }} - for (auto r : permutation_result) {{ - if (r != 0) {{ - info(\"Tuple\", permutation_name, \"failed.\"); - return false; - }} - }} - return true; - }}; + {relation_check_closure} + {permutation_check_closure} {check_circuit_for_each_relation} @@ -236,3 +198,66 @@ class {name}CircuitBuilder {{ ); } } + + +fn get_permutation_check_closure() -> String { + + format!(" + const auto evaluate_permutation = [&](const std::string& permutation_name) {{ + + // Check the tuple permutation relation + proof_system::honk::logderivative_library::compute_logderivative_inverse< + Flavor, + PermutationSettings>( + polys, params, num_rows); + + typename PermutationSettings::SumcheckArrayOfValuesOverSubrelations + permutation_result; + + for (auto& r : permutation_result) {{ + r = 0; + }} + for (size_t i = 0; i < num_rows; ++i) {{ + PermutationSettings::accumulate(permutation_result, polys.get_row(i), params, 1); + }} + for (auto r : permutation_result) {{ + if (r != 0) {{ + info(\"Tuple\", permutation_name, \"failed.\"); + return false; + }} + }} + return true; + }}; + ") + +} + + +fn get_relation_check_closure() -> String { + format!(" + const auto evaluate_relation = [&](const std::string& relation_name) {{ + typename Relation::SumcheckArrayOfValuesOverSubrelations result; + for (auto& r : result) {{ + r = 0; + }} + constexpr size_t NUM_SUBRELATIONS = result.size(); + + for (size_t i = 0; i < num_rows; ++i) {{ + Relation::accumulate(result, polys.get_row(i), {{}}, 1); + + bool x = true; + for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) {{ + if (result[j] != 0) {{ + throw_or_abort( + format(\"Relation \", relation_name, \", subrelation index \", j, \" failed at row \", i)); + x = false; + }} + }} + if (!x) {{ + return false; + }} + }} + return true; + }}; + ") +} \ No newline at end of file diff --git a/bberg/src/flavor_builder.rs b/bberg/src/flavor_builder.rs index 09b93046c9..e826db31b0 100644 --- a/bberg/src/flavor_builder.rs +++ b/bberg/src/flavor_builder.rs @@ -194,7 +194,10 @@ fn create_relation_definitions(name: &str, relation_file_names: &[String], permu // Relations tuple = ns::relation_name_0, ns::relation_name_1, ... ns::relation_name_n (comma speratated) let comma_sep_relations = create_relations_tuple(name, relation_file_names); let comma_sep_perms: String = create_permutations_tuple(permutations); - let all_relations = format!("{comma_sep_relations}, {comma_sep_perms}"); + let mut all_relations = format!("{comma_sep_relations}"); + if permutations.len() > 0 { + all_relations = all_relations + &format!(", {comma_sep_perms}"); + } format!(" using Relations = std::tuple<{all_relations}>; From 92f59f20649b585815b6bdb5946fb841ed9f08bc Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Mon, 11 Dec 2023 18:46:53 +0000 Subject: [PATCH 07/10] fix: differentiate between perm and perm relation --- bberg/src/circuit_builder.rs | 2 +- bberg/src/flavor_builder.rs | 2 +- bberg/src/permutation_builder.rs | 4 +++- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs index 1a9926ad3e..8d1f0b35f1 100644 --- a/bberg/src/circuit_builder.rs +++ b/bberg/src/circuit_builder.rs @@ -88,7 +88,7 @@ impl CircuitBuilder for BBFiles { }; let check_permutation_transformation = |permutation_name: &String| { format!( - "if (!evaluate_permutation.template operator()>(\"{permutation_name}\")) {{ + "if (!evaluate_permutation.template operator()>(\"{permutation_name}\")) {{ return false; }}", permutation_name = permutation_name diff --git a/bberg/src/flavor_builder.rs b/bberg/src/flavor_builder.rs index e826db31b0..10bbab48e0 100644 --- a/bberg/src/flavor_builder.rs +++ b/bberg/src/flavor_builder.rs @@ -157,7 +157,7 @@ fn create_permutations_tuple(permutations: &[Permutation]) -> String { permutations .iter() .map(|perm| - format!("sumcheck::{}", perm.attribute.clone().unwrap() + format!("sumcheck::{}_relation", perm.attribute.clone().unwrap() )) .collect::>() .join(", ") diff --git a/bberg/src/permutation_builder.rs b/bberg/src/permutation_builder.rs index 774f837cb4..57dd9b860a 100644 --- a/bberg/src/permutation_builder.rs +++ b/bberg/src/permutation_builder.rs @@ -71,9 +71,11 @@ fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Ve /// This function creates the export for the relation type so that it can be added to the flavor fn create_relation_exporter(permutation_name: &str) -> String { let settings_name = format!("{}_permutation_settings", permutation_name); - let relation_export = format!("template using {permutation_name} = GenericPermutationRelation<{settings_name}, FF_>;"); + let permutation_export = format!("template using {permutation_name}_relation = GenericPermutationRelation<{settings_name}, FF_>;"); + let relation_export = format!("template using {permutation_name} = GenericPermutation<{settings_name}, FF_>;"); format!(" + {permutation_export} {relation_export} ") } From 9ea2a1c14ef2604f0b1ad4d734e6b1bd006240e7 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Tue, 12 Dec 2023 12:29:15 +0000 Subject: [PATCH 08/10] fix: move relation builder --- Cargo.lock | 22 +++++- bberg/src/permutation_builder.rs | 2 - bberg/src/relation_builder.rs | 123 +++++++++++++++++++++++++++++-- bberg/src/vm_builder.rs | 90 +--------------------- 4 files changed, 137 insertions(+), 100 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a7bb2c1a41..10b8938615 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -138,7 +138,7 @@ dependencies = [ [[package]] name = "algebraic" version = "0.0.1" -source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?branch=main#4b9d8d840f70995c0fe75ee5aed63ce3e171ae10" +source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?rev=4ed1da7#4ed1da7766f7aa8740f355d8c1f3d213411ccf4b" dependencies = [ "byteorder", "ff_ce 0.11.0", @@ -3462,7 +3462,6 @@ dependencies = [ name = "pil_analyzer" version = "0.1.0" dependencies = [ - "analysis 0.1.0", "ast 0.1.0", "env_logger", "itertools 0.10.5", @@ -3522,7 +3521,7 @@ dependencies = [ [[package]] name = "plonky" version = "0.0.2" -source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?branch=main#4b9d8d840f70995c0fe75ee5aed63ce3e171ae10" +source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?rev=4ed1da7#4ed1da7766f7aa8740f355d8c1f3d213411ccf4b" dependencies = [ "algebraic", "bellman_vk_codegen", @@ -3635,6 +3634,7 @@ dependencies = [ "parser 0.1.0", "pilopt", "riscv", + "riscv_executor", "strum", "tempfile", ] @@ -4271,10 +4271,24 @@ dependencies = [ "number 0.1.0", "parser_util 0.1.0", "regex-syntax 0.6.29", + "riscv_executor", "serde_json", "test-log", ] +[[package]] +name = "riscv_executor" +version = "0.1.0" +dependencies = [ + "analysis 0.1.0", + "ast 0.1.0", + "importer", + "itertools 0.11.0", + "log", + "number 0.1.0", + "parser 0.1.0", +] + [[package]] name = "rkyv" version = "0.7.42" @@ -4699,7 +4713,7 @@ checksum = "a8f112729512f8e442d81f95a8a7ddf2b7c6b8a1a6f509a95864142b30cab2d3" [[package]] name = "starky" version = "0.0.1" -source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?branch=main#4b9d8d840f70995c0fe75ee5aed63ce3e171ae10" +source = "git+https://github.com/0xEigenLabs/eigen-zkvm.git?rev=4ed1da7#4ed1da7766f7aa8740f355d8c1f3d213411ccf4b" dependencies = [ "algebraic", "array_tool", diff --git a/bberg/src/permutation_builder.rs b/bberg/src/permutation_builder.rs index 57dd9b860a..620096c06e 100644 --- a/bberg/src/permutation_builder.rs +++ b/bberg/src/permutation_builder.rs @@ -60,7 +60,6 @@ fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Ve for permutation in permutations { let perm_settings = create_permutation_settings_file(permutation); - // TODO: temp this is not going to be the final configuration, maybe we use the trait construction again to have access to bb let folder = format!("{}/{}", bb_files.rel, project_name); let file_name = format!("{}{}", permutation.attribute.clone().unwrap_or("NONAME".to_owned()), ".hpp".to_owned()); bb_files.write_file(&folder, &file_name, &perm_settings); @@ -122,7 +121,6 @@ fn create_permutation_settings_file(permutation: &Permutation) -> String { perm_entities.extend(rhs_cols); - // TODO: below here should really be in a new function as we have just got the settings extracted from the parsed type let permutation_settings_includes = permutation_settings_includes(); let inverse_computed_at = create_inverse_computed_at(selector); let const_entities = create_get_const_entities(&perm_entities); diff --git a/bberg/src/relation_builder.rs b/bberg/src/relation_builder.rs index ba7aeb2a23..cac1bcdc31 100644 --- a/bberg/src/relation_builder.rs +++ b/bberg/src/relation_builder.rs @@ -1,34 +1,113 @@ use ast::analyzed::Identity; +use ast::analyzed::AlgebraicExpression; use ast::analyzed::{ AlgebraicBinaryOperator, AlgebraicExpression as Expression, AlgebraicUnaryOperator, IdentityKind, }; use ast::parsed::SelectedExpressions; +use itertools::Itertools; +use std::collections::HashMap; use std::collections::HashSet; use number::{DegreeType, FieldElement}; use crate::file_writer::BBFiles; +use crate::utils::capitalize; use crate::utils::map_with_newline; +/// Returned back to the vm builder from the create_relations call +pub struct RelationOutput { + /// A list of the names of the created relations + pub relations: Vec, + /// A list of the names of all of the 'used' shifted polys + pub shifted_polys: Vec, +} + +/// Each created bb Identity is passed around with its degree so as needs to be manually +/// provided for sumcheck +type BBIdentity = (DegreeType, String); + pub trait RelationBuilder { - fn create_relations( + /// Create Relations + /// + /// Takes in the ast ( for relations ), groups each of them by file, and then + /// calls 'create relation' for each + /// + /// Relation output is passed back to the caller as the prover requires both: + /// - The shifted polys + /// - The names of the relations files created + fn create_relations( + &self, + root_name: &str, + identities: &[Identity>], + ) -> RelationOutput; + + /// Create Relation + /// + /// Name and root name are required to determine the file path, e.g. it will be in the bberg/relations/generated + /// followed by /root_name/name + /// - root name should be the name provided with the --name flag + /// - name will be a pil namespace + /// + /// - Identities are the identities that will be used to create the relations, they are generated within create_relations + /// - row_type contains all of the columns that the relations namespace touches. + fn create_relation( &self, root_name: &str, name: &str, sub_relations: &[String], identities: &[BBIdentity], - row_type: &str, - ); + row_type: &str); + /// Declare views + /// + /// Declare views is a macro that generates a reference for each of the columns + /// This reference will be a span into a sumcheck related object, it must be declared for EACH sub-relation + /// as the sumcheck object is sensitive to the degree of the relation. fn create_declare_views(&self, name: &str, all_cols_and_shifts: &[String]); } -// TODO: MOve -> to gen code we need to know the degree of each poly -type BBIdentity = (DegreeType, String); - impl RelationBuilder for BBFiles { - fn create_relations( + +fn create_relations(&self, file_name: &str, analyzed_identities: &[Identity>]) -> RelationOutput { + // Group relations per file + let grouped_relations: HashMap>>> = group_relations_per_file(&analyzed_identities); + let relations = grouped_relations.keys().cloned().collect_vec(); + + // Contains all of the rows in each relation, will be useful for creating composite builder types + let mut all_rows: HashMap = HashMap::new(); + let mut shifted_polys: Vec = Vec::new(); + + // ----------------------- Create the relation files ----------------------- + for (relation_name, analyzed_idents) in grouped_relations.iter() { + let (subrelations, identities, collected_polys, collected_shifts) = + create_identities(file_name,analyzed_idents); + + shifted_polys.extend(collected_shifts); + + // let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts); + // TODO: This can probably be moved into the create_identities function + let row_type = create_row_type(&capitalize(relation_name), &collected_polys); + + all_rows.insert(relation_name.to_owned(), row_type.clone()); + + self.create_relation( + file_name, + relation_name, + &subrelations, + &identities, + &row_type, + ); + } + + RelationOutput { + relations, + shifted_polys + } + +} + + fn create_relation( &self, root_name: &str, name: &str, @@ -84,6 +163,36 @@ namespace proof_system::{root_name}_vm {{ } } +/// Group relations per file +/// +/// The compiler returns all relations in one large vector, however we want to distinguish +/// which files .pil files the relations belong to for later code gen +/// +/// Say we have two files foo.pil and bar.pil +/// foo.pil contains the following relations: +/// - foo1 +/// - foo2 +/// bar.pil contains the following relations: +/// - bar1 +/// - bar2 +/// +/// This function will return a hashmap with the following structure: +/// { +/// "foo": [foo1, foo2], +/// "bar": [bar1, bar2] +/// } +/// +/// This allows us to generate a relation.hpp file containing ONLY the relations for that .pil file +fn group_relations_per_file( + identities: &[Identity>], +) -> HashMap>>> { + identities + .iter() + .cloned() + .into_group_map_by(|identity| identity.source.file.clone().replace(".pil", "")) +} + + fn relation_class_boilerplate( name: &str, sub_relations: &[String], diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index f0b1b2e963..8534af2def 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -1,10 +1,6 @@ -use std::collections::HashMap; -use ast::analyzed::AlgebraicExpression; use ast::analyzed::Analyzed; -use ast::analyzed::Identity; -use itertools::Itertools; use number::FieldElement; use crate::circuit_builder::CircuitBuilder; @@ -15,8 +11,8 @@ use crate::permutation_builder::Permutation; use crate::permutation_builder::PermutationBuilder; use crate::permutation_builder::get_inverses_from_permutations; use crate::prover_builder::ProverBuilder; -use crate::relation_builder::{create_identities, create_row_type, RelationBuilder}; -use crate::utils::capitalize; +use crate::relation_builder::RelationBuilder; +use crate::relation_builder::RelationOutput; use crate::utils::collect_col; use crate::utils::flatten; use crate::utils::sanitize_name; @@ -61,7 +57,7 @@ pub(crate) fn analyzed_to_cpp( let RelationOutput { relations, shifted_polys - } = create_relation_files(&bb_files, file_name, &analyzed_identities); + } = bb_files.create_relations(file_name, &analyzed_identities); // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- let permutations = bb_files.create_permutation_files(file_name, analyzed); @@ -124,85 +120,6 @@ pub(crate) fn analyzed_to_cpp( } -struct RelationOutput { - relations: Vec, - shifted_polys: Vec, -} - -/// TODO: MOVE THIS OUT OF THIS FILE???? -/// Does this need to return all of the shifted polys that it collects> -/// TODO: restructure this so that we do not have to pass in bb files abd the name at the top level -fn create_relation_files(bb_files: &BBFiles, file_name: &str, analyzed_identities: &Vec>>) -> RelationOutput { - // Group relations per file - let grouped_relations: HashMap>>> = group_relations_per_file(&analyzed_identities); - let relations = grouped_relations.keys().cloned().collect_vec(); - - // Contains all of the rows in each relation, will be useful for creating composite builder types - // TODO: this will change up - let mut all_rows: HashMap = HashMap::new(); - let mut shifted_polys: Vec = Vec::new(); - - // ----------------------- Create the relation files ----------------------- - for (relation_name, analyzed_idents) in grouped_relations.iter() { - // TODO: make this more granular instead of doing everything at once - let (subrelations, identities, collected_polys, collected_shifts) = - create_identities(file_name,analyzed_idents); - - shifted_polys.extend(collected_shifts); - - // let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts); - // TODO: This can probably be moved into the create_identities function - let row_type = create_row_type(&capitalize(relation_name), &collected_polys); - - all_rows.insert(relation_name.clone(), row_type.clone()); - - bb_files.create_relations( - file_name, - relation_name, - &subrelations, - &identities, - &row_type, - ); - } - - RelationOutput { - relations, - shifted_polys - } - -} - - - -/// Group relations per file -/// -/// The compiler returns all relations in one large vector, however we want to distinguish -/// which files .pil files the relations belong to for later code gen -/// -/// Say we have two files foo.pil and bar.pil -/// foo.pil contains the following relations: -/// - foo1 -/// - foo2 -/// bar.pil contains the following relations: -/// - bar1 -/// - bar2 -/// -/// This function will return a hashmap with the following structure: -/// { -/// "foo": [foo1, foo2], -/// "bar": [bar1, bar2] -/// } -/// -/// This allows us to generate a relation.hpp file containing ONLY the relations for that .pil file -fn group_relations_per_file( - identities: &[Identity>], -) -> HashMap>>> { - identities - .iter() - .cloned() - .into_group_map_by(|identity| identity.source.file.clone().replace(".pil", "")) -} - /// Get all col names /// /// In the flavor file, there are a number of different groups of columns that we need to keep track of @@ -241,7 +158,6 @@ fn get_all_col_names( let all_cols_with_shifts: Vec = flatten(&[fixed_names.clone(), witness_names.clone(), shifted.clone()]); - // TODO: remove dup ColumnGroups { fixed: fixed_names, witness: witness_names, From 5e3bffa25a17c0c0ff39c17ac5f8b777668cb926 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Tue, 12 Dec 2023 12:43:07 +0000 Subject: [PATCH 09/10] chore: clippy / fmt --- ast/src/analyzed/display.rs | 8 +- ast/src/parsed/display.rs | 9 +- ast/src/parsed/mod.rs | 1 - ast/src/parsed/visitor.rs | 16 +++- bberg/src/circuit_builder.rs | 64 ++++++------- bberg/src/flavor_builder.rs | 34 +++---- bberg/src/permutation_builder.rs | 121 ++++++++++++++++-------- bberg/src/relation_builder.rs | 99 +++++++++---------- bberg/src/verifier_builder.rs | 6 +- bberg/src/vm_builder.rs | 10 +- compiler/src/lib.rs | 10 +- parser/src/lib.rs | 6 +- pil_analyzer/src/statement_processor.rs | 7 +- riscv/tests/common/mod.rs | 1 + type_check/src/lib.rs | 9 +- 15 files changed, 228 insertions(+), 173 deletions(-) diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index 6c91bd1966..c5194b4992 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -149,7 +149,13 @@ impl Display for Identity> { } } IdentityKind::Plookup => write!(f, "{} in {};", self.left, self.right), - IdentityKind::Permutation => write!(f, "#[{}] {} is {};", self.attribute.clone().unwrap_or_default(), self.left, self.right), + IdentityKind::Permutation => write!( + f, + "#[{}] {} is {};", + self.attribute.clone().unwrap_or_default(), + self.left, + self.right + ), IdentityKind::Connect => write!(f, "{} connect {};", self.left, self.right), } } diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index 361d667ec5..d42f8fa4b4 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -391,9 +391,12 @@ impl Display for PilStatement { } } PilStatement::PlookupIdentity(_, left, right) => write!(f, "{left} in {right};"), - PilStatement::PermutationIdentity(_, // - _, // - left, right) => write!(f, "{left} is {right};"), // + PilStatement::PermutationIdentity( + _, // + _, // + left, + right, + ) => write!(f, "{left} is {right};"), // PilStatement::ConnectIdentity(_, left, right) => write!( f, "{{ {} }} connect {{ {} }};", diff --git a/ast/src/parsed/mod.rs b/ast/src/parsed/mod.rs index fe0faad647..b6a4b4c149 100644 --- a/ast/src/parsed/mod.rs +++ b/ast/src/parsed/mod.rs @@ -56,7 +56,6 @@ pub struct Attribute { pub name: Option, } - #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] pub struct SelectedExpressions { pub selector: Option, diff --git a/ast/src/parsed/visitor.rs b/ast/src/parsed/visitor.rs index 55c9e95d62..7bbec1f8f9 100644 --- a/ast/src/parsed/visitor.rs +++ b/ast/src/parsed/visitor.rs @@ -193,9 +193,12 @@ impl ExpressionVisitable> for Pi match self { PilStatement::Expression(_, e) => e.visit_expressions_mut(f, o), PilStatement::PlookupIdentity(_, left, right) - | PilStatement::PermutationIdentity(_, // + | PilStatement::PermutationIdentity( _, // - left, right) => [left, right] // + _, // + left, + right, + ) => [left, right] // .into_iter() .try_for_each(|e| e.visit_expressions_mut(f, o)), PilStatement::ConnectIdentity(_start, left, right) => left @@ -232,9 +235,12 @@ impl ExpressionVisitable> for Pi match self { PilStatement::Expression(_, e) => e.visit_expressions(f, o), PilStatement::PlookupIdentity(_, left, right) - | PilStatement::PermutationIdentity(_, // - _, // - left, right) => [left, right] // + | PilStatement::PermutationIdentity( + _, // + _, // + left, + right, + ) => [left, right] // .into_iter() .try_for_each(|e| e.visit_expressions(f, o)), PilStatement::ConnectIdentity(_start, left, right) => left diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs index 8d1f0b35f1..f7cfca2480 100644 --- a/bberg/src/circuit_builder.rs +++ b/bberg/src/circuit_builder.rs @@ -103,12 +103,12 @@ impl CircuitBuilder for BBFiles { let check_circuit_for_each_permutation = map_with_newline(permutations, check_permutation_transformation); - let (params,permutation_check_closure) = if permutations.len() > 0 { + let (params, permutation_check_closure) = if !permutations.is_empty() { (get_params(), get_permutation_check_closure()) } else { ("", "".to_owned()) }; - let relation_check_closure = if relations.len() > 0 { + let relation_check_closure = if !relations.is_empty() { get_relation_check_closure() } else { "".to_owned() @@ -199,11 +199,9 @@ class {name}CircuitBuilder {{ } } - fn get_permutation_check_closure() -> String { - - format!(" - const auto evaluate_permutation = [&](const std::string& permutation_name) {{ + " + const auto evaluate_permutation = [&](const std::string& permutation_name) { // Check the tuple permutation relation proof_system::honk::logderivative_library::compute_logderivative_inverse< @@ -214,50 +212,48 @@ fn get_permutation_check_closure() -> String { typename PermutationSettings::SumcheckArrayOfValuesOverSubrelations permutation_result; - for (auto& r : permutation_result) {{ + for (auto& r : permutation_result) { r = 0; - }} - for (size_t i = 0; i < num_rows; ++i) {{ + } + for (size_t i = 0; i < num_rows; ++i) { PermutationSettings::accumulate(permutation_result, polys.get_row(i), params, 1); - }} - for (auto r : permutation_result) {{ - if (r != 0) {{ + } + for (auto r : permutation_result) { + if (r != 0) { info(\"Tuple\", permutation_name, \"failed.\"); return false; - }} - }} + } + } return true; - }}; - ") - + }; + ".to_string() } - fn get_relation_check_closure() -> String { - format!(" - const auto evaluate_relation = [&](const std::string& relation_name) {{ + " + const auto evaluate_relation = [&](const std::string& relation_name) { typename Relation::SumcheckArrayOfValuesOverSubrelations result; - for (auto& r : result) {{ + for (auto& r : result) { r = 0; - }} + } constexpr size_t NUM_SUBRELATIONS = result.size(); - for (size_t i = 0; i < num_rows; ++i) {{ - Relation::accumulate(result, polys.get_row(i), {{}}, 1); + for (size_t i = 0; i < num_rows; ++i) { + Relation::accumulate(result, polys.get_row(i), {}, 1); bool x = true; - for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) {{ - if (result[j] != 0) {{ + for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) { + if (result[j] != 0) { throw_or_abort( format(\"Relation \", relation_name, \", subrelation index \", j, \" failed at row \", i)); x = false; - }} - }} - if (!x) {{ + } + } + if (!x) { return false; - }} - }} + } + } return true; - }}; - ") -} \ No newline at end of file + }; + ".to_string() +} diff --git a/bberg/src/flavor_builder.rs b/bberg/src/flavor_builder.rs index 10bbab48e0..0c10ea4f64 100644 --- a/bberg/src/flavor_builder.rs +++ b/bberg/src/flavor_builder.rs @@ -1,6 +1,7 @@ use crate::{ file_writer::BBFiles, - utils::{get_relations_imports, map_with_newline}, permutation_builder::{Permutation, get_inverses_from_permutations}, + permutation_builder::{get_inverses_from_permutations, Permutation}, + utils::{get_relations_imports, map_with_newline}, }; pub trait FlavorBuilder { @@ -44,7 +45,8 @@ impl FlavorBuilder for BBFiles { // Top of file boilerplate let class_aliases = create_class_aliases(); - let relation_definitions = create_relation_definitions(name, relation_file_names, permutations); + let relation_definitions = + create_relation_definitions(name, relation_file_names, permutations); let container_size_definitions = container_size_definitions(num_precomputed, num_witness, num_all); @@ -152,13 +154,11 @@ fn create_relations_tuple(master_name: &str, relation_file_names: &[String]) -> } /// Creates comma separated relations tuple file -/// TODO(md): maybe need the filename in here too if we scope these +/// TODO(md): maybe need the filename in here too if we scope these fn create_permutations_tuple(permutations: &[Permutation]) -> String { permutations .iter() - .map(|perm| - format!("sumcheck::{}_relation", perm.attribute.clone().unwrap() - )) + .map(|perm| format!("sumcheck::{}_relation", perm.attribute.clone().unwrap())) .collect::>() .join(", ") } @@ -190,12 +190,16 @@ fn create_class_aliases() -> &'static str { /// definitions. /// /// We then also define some constants, making use of the preprocessor. -fn create_relation_definitions(name: &str, relation_file_names: &[String], permutations: &[Permutation]) -> String { +fn create_relation_definitions( + name: &str, + relation_file_names: &[String], + permutations: &[Permutation], +) -> String { // Relations tuple = ns::relation_name_0, ns::relation_name_1, ... ns::relation_name_n (comma speratated) let comma_sep_relations = create_relations_tuple(name, relation_file_names); let comma_sep_perms: String = create_permutations_tuple(permutations); - let mut all_relations = format!("{comma_sep_relations}"); - if permutations.len() > 0 { + let mut all_relations = comma_sep_relations.to_string(); + if !permutations.is_empty() { all_relations = all_relations + &format!(", {comma_sep_perms}"); } @@ -475,12 +479,11 @@ fn generate_transcript(witness: &[String]) -> String { let declaration_transform = |c: &_| format!("Commitment {c};"); let deserialize_transform = |name: &_| { format!( - "{name} = deserialize_from_buffer(Transcript::proof_data, num_bytes_read);", - ) - }; - let serialize_transform = |name: &_| { - format!("serialize_to_buffer({name}, Transcript::proof_data);") + "{name} = deserialize_from_buffer(Transcript::proof_data, num_bytes_read);", + ) }; + let serialize_transform = + |name: &_| format!("serialize_to_buffer({name}, Transcript::proof_data);"); // Perform Transformations let declarations = map_with_newline(witness, declaration_transform); @@ -555,7 +558,6 @@ fn generate_transcript(witness: &[String]) -> String { ") } - fn create_permuation_sumcheck_declaration(permutations: &[String], name: &str) -> String { let sumcheck_transformation = |perm: &String| { format!( @@ -566,4 +568,4 @@ fn create_permuation_sumcheck_declaration(permutations: &[String], name: &str) - }; map_with_newline(permutations, sumcheck_transformation) -} \ No newline at end of file +} diff --git a/bberg/src/permutation_builder.rs b/bberg/src/permutation_builder.rs index 620096c06e..9d501461dd 100644 --- a/bberg/src/permutation_builder.rs +++ b/bberg/src/permutation_builder.rs @@ -1,5 +1,8 @@ -use ast::{analyzed::{Analyzed, AlgebraicExpression, Identity, IdentityKind}, parsed::SelectedExpressions}; use crate::file_writer::BBFiles; +use ast::{ + analyzed::{AlgebraicExpression, Analyzed, Identity, IdentityKind}, + parsed::SelectedExpressions, +}; use itertools::Itertools; use number::FieldElement; @@ -7,7 +10,7 @@ use crate::utils::sanitize_name; #[derive(Debug)] /// Permutation -/// +/// /// Contains the information required to produce a permutation relation pub struct Permutation { /// -> Attribute - the name given to the inverse helper column @@ -15,68 +18,91 @@ pub struct Permutation { /// -> PermSide - the left side of the permutation pub left: PermutationSide, /// -> PermSide - the right side of the permutation - pub right: PermutationSide + pub right: PermutationSide, } #[derive(Debug)] /// PermSide -/// +/// /// One side of a two sided permutation relationship pub struct PermutationSide { /// -> Option - the selector for the permutation ( on / off toggle ) selector: Option, /// The columns involved in this side of the permutation - cols: Vec + cols: Vec, } pub trait PermutationBuilder { /// Takes in an AST and works out what permutation relations are needed /// Note: returns the name of the inverse columns, such that they can be added to he prover in subsequent steps - fn create_permutation_files(&self, name: &str, analyzed: &Analyzed)-> Vec; + fn create_permutation_files( + &self, + name: &str, + analyzed: &Analyzed, + ) -> Vec; } impl PermutationBuilder for BBFiles { - fn create_permutation_files(&self, project_name: &str, analyzed: &Analyzed) -> Vec { - let perms: Vec<&Identity>> = analyzed.identities.iter().filter(|identity| matches!(identity.kind, IdentityKind::Permutation)).collect(); - let new_perms = perms.iter().map(|perm| - Permutation { + fn create_permutation_files( + &self, + project_name: &str, + analyzed: &Analyzed, + ) -> Vec { + let perms: Vec<&Identity>> = analyzed + .identities + .iter() + .filter(|identity| matches!(identity.kind, IdentityKind::Permutation)) + .collect(); + let new_perms = perms + .iter() + .map(|perm| Permutation { attribute: perm.attribute.clone(), left: get_perm_side(&perm.left), - right: get_perm_side(&perm.right) - }).collect_vec(); + right: get_perm_side(&perm.right), + }) + .collect_vec(); - create_permutations(self, project_name,&new_perms); + create_permutations(self, project_name, &new_perms); new_perms } } /// The attributes of a permutation contain the name of the inverse, we collect all of these to create the inverse column pub fn get_inverses_from_permutations(permutations: &[Permutation]) -> Vec { - permutations.iter().map(|perm| perm.attribute.clone().unwrap()).collect() + permutations + .iter() + .map(|perm| perm.attribute.clone().unwrap()) + .collect() } /// Write the permutation settings files to disk fn create_permutations(bb_files: &BBFiles, project_name: &str, permutations: &Vec) { for permutation in permutations { let perm_settings = create_permutation_settings_file(permutation); - + let folder = format!("{}/{}", bb_files.rel, project_name); - let file_name = format!("{}{}", permutation.attribute.clone().unwrap_or("NONAME".to_owned()), ".hpp".to_owned()); + let file_name = format!( + "{}{}", + permutation.attribute.clone().unwrap_or("NONAME".to_owned()), + ".hpp".to_owned() + ); bb_files.write_file(&folder, &file_name, &perm_settings); } } -/// All relation types eventually get wrapped in the relation type +/// All relation types eventually get wrapped in the relation type /// This function creates the export for the relation type so that it can be added to the flavor fn create_relation_exporter(permutation_name: &str) -> String { let settings_name = format!("{}_permutation_settings", permutation_name); let permutation_export = format!("template using {permutation_name}_relation = GenericPermutationRelation<{settings_name}, FF_>;"); let relation_export = format!("template using {permutation_name} = GenericPermutation<{settings_name}, FF_>;"); - format!(" + format!( + " {permutation_export} {relation_export} - ") + " + ) } fn permutation_settings_includes() -> &'static str { @@ -91,13 +117,15 @@ fn permutation_settings_includes() -> &'static str { } fn create_permutation_settings_file(permutation: &Permutation) -> String { - println!("Permutation: {:?}", permutation); let columns_per_set = permutation.left.cols.len(); // TODO(md): Throw an error if no attribute is provided for the permutation // TODO(md): In the future we will need to condense off the back of this - combining those with the same inverse column - let permutation_name = permutation.attribute.clone().expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here - + let permutation_name = permutation + .attribute + .clone() + .expect("Inverse column name must be provided"); // TODO(md): catch this earlier than here + // NOTE: syntax is not flexible enough to enable the single row case right now :(:(:(:(:)))) // This also will need to work for both sides of this ! let selector = permutation.left.selector.clone().unwrap(); // TODO: deal with unwrap @@ -114,13 +142,13 @@ fn create_permutation_settings_file(permutation: &Permutation) -> String { permutation_name.clone(), selector.clone(), selector.clone(), - selector.clone() // TODO: update this away from the simple example - ].to_vec(); + selector.clone(), // TODO: update this away from the simple example + ] + .to_vec(); perm_entities.extend(lhs_cols); perm_entities.extend(rhs_cols); - let permutation_settings_includes = permutation_settings_includes(); let inverse_computed_at = create_inverse_computed_at(selector); let const_entities = create_get_const_entities(&perm_entities); @@ -188,11 +216,8 @@ fn create_permutation_settings_file(permutation: &Permutation) -> String { }} " ) - } - - // TODO: make this dynamic such that there can be more than one fn create_inverse_computed_at(inverse_selector: String) -> String { let inverse_computed_selector = format!("in.{inverse_selector}"); @@ -202,42 +227,54 @@ fn create_inverse_computed_at(inverse_selector: String) -> String { }}") } -fn create_get_const_entities (settings: &[String]) -> String { +fn create_get_const_entities(settings: &[String]) -> String { let forward = create_forward_as_tuple(settings); - format!(" + format!( + " template static inline auto get_const_entities(const AllEntities& in) {{ {forward} }} - ") + " + ) } -fn create_get_nonconst_entities (settings: &[String]) -> String { +fn create_get_nonconst_entities(settings: &[String]) -> String { let forward = create_forward_as_tuple(settings); - format!(" + format!( + " template static inline auto get_nonconst_entities(AllEntities& in) {{ {forward} }} - ") + " + ) } - fn create_forward_as_tuple(settings: &[String]) -> String { let adjusted = settings.iter().map(|col| format!("in.{col}")).join(",\n"); - format!(" + format!( + " return std::forward_as_tuple( {} ); - ", adjusted) + ", + adjusted + ) } -fn get_perm_side(def: &SelectedExpressions>) -> PermutationSide { +fn get_perm_side( + def: &SelectedExpressions>, +) -> PermutationSide { let get_name = |expr: &AlgebraicExpression| match expr { AlgebraicExpression::Reference(a_ref) => sanitize_name(&a_ref.name), - _ => panic!("Expected reference") + _ => panic!("Expected reference"), }; PermutationSide { - selector: def.selector.as_ref().map(|expr| get_name(&expr)), - cols: def.expressions.iter().map(|expr| get_name(&expr)).collect_vec() + selector: def.selector.as_ref().map(|expr| get_name(expr)), + cols: def + .expressions + .iter() + .map(|expr| get_name(expr)) + .collect_vec(), } -} \ No newline at end of file +} diff --git a/bberg/src/relation_builder.rs b/bberg/src/relation_builder.rs index cac1bcdc31..2e932e0b55 100644 --- a/bberg/src/relation_builder.rs +++ b/bberg/src/relation_builder.rs @@ -1,5 +1,5 @@ -use ast::analyzed::Identity; use ast::analyzed::AlgebraicExpression; +use ast::analyzed::Identity; use ast::analyzed::{ AlgebraicBinaryOperator, AlgebraicExpression as Expression, AlgebraicUnaryOperator, IdentityKind, @@ -28,11 +28,11 @@ pub struct RelationOutput { type BBIdentity = (DegreeType, String); pub trait RelationBuilder { - /// Create Relations - /// - /// Takes in the ast ( for relations ), groups each of them by file, and then + /// Create Relations + /// + /// Takes in the ast ( for relations ), groups each of them by file, and then /// calls 'create relation' for each - /// + /// /// Relation output is passed back to the caller as the prover requires both: /// - The shifted polys /// - The names of the relations files created @@ -41,14 +41,14 @@ pub trait RelationBuilder { root_name: &str, identities: &[Identity>], ) -> RelationOutput; - + /// Create Relation - /// + /// /// Name and root name are required to determine the file path, e.g. it will be in the bberg/relations/generated /// followed by /root_name/name /// - root name should be the name provided with the --name flag /// - name will be a pil namespace - /// + /// /// - Identities are the identities that will be used to create the relations, they are generated within create_relations /// - row_type contains all of the columns that the relations namespace touches. fn create_relation( @@ -57,56 +57,60 @@ pub trait RelationBuilder { name: &str, sub_relations: &[String], identities: &[BBIdentity], - row_type: &str); + row_type: &str, + ); /// Declare views - /// - /// Declare views is a macro that generates a reference for each of the columns + /// + /// Declare views is a macro that generates a reference for each of the columns /// This reference will be a span into a sumcheck related object, it must be declared for EACH sub-relation /// as the sumcheck object is sensitive to the degree of the relation. fn create_declare_views(&self, name: &str, all_cols_and_shifts: &[String]); } impl RelationBuilder for BBFiles { + fn create_relations( + &self, + file_name: &str, + analyzed_identities: &[Identity>], + ) -> RelationOutput { + // Group relations per file + let grouped_relations: HashMap>>> = + group_relations_per_file(analyzed_identities); + let relations = grouped_relations.keys().cloned().collect_vec(); + + // Contains all of the rows in each relation, will be useful for creating composite builder types + let mut all_rows: HashMap = HashMap::new(); + let mut shifted_polys: Vec = Vec::new(); + + // ----------------------- Create the relation files ----------------------- + for (relation_name, analyzed_idents) in grouped_relations.iter() { + let (subrelations, identities, collected_polys, collected_shifts) = + create_identities(file_name, analyzed_idents); + + shifted_polys.extend(collected_shifts); + + // let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts); + // TODO: This can probably be moved into the create_identities function + let row_type = create_row_type(&capitalize(relation_name), &collected_polys); + + all_rows.insert(relation_name.to_owned(), row_type.clone()); + + self.create_relation( + file_name, + relation_name, + &subrelations, + &identities, + &row_type, + ); + } -fn create_relations(&self, file_name: &str, analyzed_identities: &[Identity>]) -> RelationOutput { - // Group relations per file - let grouped_relations: HashMap>>> = group_relations_per_file(&analyzed_identities); - let relations = grouped_relations.keys().cloned().collect_vec(); - - // Contains all of the rows in each relation, will be useful for creating composite builder types - let mut all_rows: HashMap = HashMap::new(); - let mut shifted_polys: Vec = Vec::new(); - - // ----------------------- Create the relation files ----------------------- - for (relation_name, analyzed_idents) in grouped_relations.iter() { - let (subrelations, identities, collected_polys, collected_shifts) = - create_identities(file_name,analyzed_idents); - - shifted_polys.extend(collected_shifts); - - // let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts); - // TODO: This can probably be moved into the create_identities function - let row_type = create_row_type(&capitalize(relation_name), &collected_polys); - - all_rows.insert(relation_name.to_owned(), row_type.clone()); - - self.create_relation( - file_name, - relation_name, - &subrelations, - &identities, - &row_type, - ); - } - - RelationOutput { - relations, - shifted_polys + RelationOutput { + relations, + shifted_polys, + } } -} - fn create_relation( &self, root_name: &str, @@ -192,7 +196,6 @@ fn group_relations_per_file( .into_group_map_by(|identity| identity.source.file.clone().replace(".pil", "")) } - fn relation_class_boilerplate( name: &str, sub_relations: &[String], diff --git a/bberg/src/verifier_builder.rs b/bberg/src/verifier_builder.rs index 8ac07514da..918231122a 100644 --- a/bberg/src/verifier_builder.rs +++ b/bberg/src/verifier_builder.rs @@ -10,9 +10,11 @@ impl VerifierBuilder for BBFiles { fn create_verifier_cpp(&mut self, name: &str, witness: &[String]) { let include_str = includes_cpp(name); - let wire_transformation = |n: &String| format!( + let wire_transformation = |n: &String| { + format!( "commitments.{n} = transcript->template receive_from_prover(commitment_labels.{n});" - ); + ) + }; let wire_commitments = map_with_newline(witness, wire_transformation); let ver_cpp = format!(" diff --git a/bberg/src/vm_builder.rs b/bberg/src/vm_builder.rs index 8534af2def..7bea6a6a37 100644 --- a/bberg/src/vm_builder.rs +++ b/bberg/src/vm_builder.rs @@ -1,4 +1,3 @@ - use ast::analyzed::Analyzed; use number::FieldElement; @@ -7,9 +6,9 @@ use crate::circuit_builder::CircuitBuilder; use crate::composer_builder::ComposerBuilder; use crate::file_writer::BBFiles; use crate::flavor_builder::FlavorBuilder; +use crate::permutation_builder::get_inverses_from_permutations; use crate::permutation_builder::Permutation; use crate::permutation_builder::PermutationBuilder; -use crate::permutation_builder::get_inverses_from_permutations; use crate::prover_builder::ProverBuilder; use crate::relation_builder::RelationBuilder; use crate::relation_builder::RelationOutput; @@ -38,7 +37,7 @@ struct ColumnGroups { } /// Analyzed to cpp -/// +/// /// Converts an analyzed pil AST into a set of cpp files that can be used to generate a proof pub(crate) fn analyzed_to_cpp( analyzed: &Analyzed, @@ -56,8 +55,8 @@ pub(crate) fn analyzed_to_cpp( // We collect all references to shifts as we traverse all identities and create relation files let RelationOutput { relations, - shifted_polys - } = bb_files.create_relations(file_name, &analyzed_identities); + shifted_polys, + } = bb_files.create_relations(file_name, &analyzed_identities); // ----------------------- Handle Lookup / Permutation Relation Identities ----------------------- let permutations = bb_files.create_permutation_files(file_name, analyzed); @@ -119,7 +118,6 @@ pub(crate) fn analyzed_to_cpp( bb_files.create_prover_hpp(file_name); } - /// Get all col names /// /// In the flavor file, there are a number of different groups of columns that we need to keep track of diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs index bb8d50c351..3396d33ee4 100644 --- a/compiler/src/lib.rs +++ b/compiler/src/lib.rs @@ -270,7 +270,7 @@ pub fn convert_analyzed_to_pil_with_callback( force_overwrite: bool, prove_with: Option, external_witness_values: Vec<(&str, Vec)>, - bname: Option + bname: Option, ) -> Result<(PathBuf, Option>), Vec> { let mut monitor = DiffMonitor::default(); let analyzed = compile_asm_string_to_analyzed_ast(file_name, contents, Some(&mut monitor))?; @@ -307,7 +307,7 @@ pub fn compile_asm_string( force_overwrite, prove_with, external_witness_values, - bname + bname, ) } @@ -321,7 +321,7 @@ pub fn compile_asm_string_with_callback>( force_overwrite: bool, prove_with: Option, external_witness_values: Vec<(&str, Vec)>, - bname: Option + bname: Option, ) -> Result<(PathBuf, Option>), Vec> { let mut monitor = DiffMonitor::default(); let analyzed = compile_asm_string_to_analyzed_ast(file_name, contents, Some(&mut monitor))?; @@ -337,7 +337,7 @@ pub fn compile_asm_string_with_callback>( force_overwrite, prove_with, external_witness_values, - bname + bname, ) } diff --git a/parser/src/lib.rs b/parser/src/lib.rs index dbd5c5b3c1..0909e43a4c 100644 --- a/parser/src/lib.rs +++ b/parser/src/lib.rs @@ -113,9 +113,11 @@ mod test { #[test] fn parse_permutation_attribute() { let parsed = powdr::PILFileParser::new() - .parse::(" + .parse::( + " #[attribute] - { f } is { g };") + { f } is { g };", + ) .unwrap(); assert_eq!( parsed, diff --git a/pil_analyzer/src/statement_processor.rs b/pil_analyzer/src/statement_processor.rs index 23a0eff916..8e8c4d9c36 100644 --- a/pil_analyzer/src/statement_processor.rs +++ b/pil_analyzer/src/statement_processor.rs @@ -217,16 +217,13 @@ where self.process_selected_expressions(key), self.process_selected_expressions(haystack), ), - PilStatement::PermutationIdentity(start, - attribute, left, right) => { - ( + PilStatement::PermutationIdentity(start, attribute, left, right) => ( start, IdentityKind::Permutation, attribute.clone(), self.process_selected_expressions(left), self.process_selected_expressions(right), - ) - }, + ), PilStatement::ConnectIdentity(start, left, right) => ( start, IdentityKind::Connect, diff --git a/riscv/tests/common/mod.rs b/riscv/tests/common/mod.rs index d34d062132..505b411f1f 100644 --- a/riscv/tests/common/mod.rs +++ b/riscv/tests/common/mod.rs @@ -29,6 +29,7 @@ pub fn verify_riscv_asm_string(file_name: &str, contents: &str, inputs: Vec TypeChecker { .iter() .filter_map(|s| match s { ast::parsed::PilStatement::PolynomialIdentity(_, _) => None, - ast::parsed::PilStatement::PermutationIdentity(_, // - _, // - l, _) // + ast::parsed::PilStatement::PermutationIdentity( + _, // + _, // + l, + _, + ) | ast::parsed::PilStatement::PlookupIdentity(_, l, _) => l .selector .is_some() From e3e8dfd8892877d8c92821e42a1699d82e759d0a Mon Sep 17 00:00:00 2001 From: Maddiaa <47148561+Maddiaa0@users.noreply.github.com> Date: Wed, 13 Dec 2023 18:25:17 +0000 Subject: [PATCH 10/10] feat(debug): tag relations with debug information (#33) * feat: add debug labels to check circuit * fmt * fix * fix: more than one file issue * inline fix --- asm_to_pil/src/vm_to_constrained.rs | 13 +++- ast/src/parsed/display.rs | 2 +- ast/src/parsed/mod.rs | 2 +- ast/src/parsed/visitor.rs | 4 +- bberg/src/circuit_builder.rs | 10 ++- bberg/src/relation_builder.rs | 97 ++++++++++++++++++++----- parser/src/powdr.lalrpop | 2 +- pil_analyzer/src/statement_processor.rs | 13 +++- type_check/src/lib.rs | 2 +- 9 files changed, 112 insertions(+), 33 deletions(-) diff --git a/asm_to_pil/src/vm_to_constrained.rs b/asm_to_pil/src/vm_to_constrained.rs index 26ddd106ad..e21b02d198 100644 --- a/asm_to_pil/src/vm_to_constrained.rs +++ b/asm_to_pil/src/vm_to_constrained.rs @@ -144,6 +144,7 @@ impl ASMPILConverter { ), PilStatement::PolynomialIdentity( 0, + None, lhs - (Expression::from(T::one()) - next_reference("first_step")) * direct_reference(pc_update_name), @@ -154,10 +155,14 @@ impl ASMPILConverter { ReadOnly => { let not_reset: Expression = Expression::from(T::one()) - direct_reference("instr__reset"); - vec![PilStatement::PolynomialIdentity(0, not_reset * (lhs - rhs))] + vec![PilStatement::PolynomialIdentity( + 0, + None, + not_reset * (lhs - rhs), + )] } _ => { - vec![PilStatement::PolynomialIdentity(0, lhs - rhs)] + vec![PilStatement::PolynomialIdentity(0, None, lhs - rhs)] } } }) @@ -389,7 +394,7 @@ impl ASMPILConverter { }); for mut statement in body { - if let PilStatement::PolynomialIdentity(_start, expr) = statement { + if let PilStatement::PolynomialIdentity(_start, _attr, expr) = statement { match extract_update(expr) { (Some(var), expr) => { let reference = direct_reference(&instruction_flag); @@ -406,6 +411,7 @@ impl ASMPILConverter { } (None, expr) => self.pil.push(PilStatement::PolynomialIdentity( 0, + None, direct_reference(&instruction_flag) * expr.clone(), )), } @@ -715,6 +721,7 @@ impl ASMPILConverter { .sum(); self.pil.push(PilStatement::PolynomialIdentity( 0, + None, direct_reference(register) - assign_constraint, )); } diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index d42f8fa4b4..27c435f543 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -383,7 +383,7 @@ impl Display for PilStatement { value.as_ref().map(|v| format!("{v}")).unwrap_or_default() ) } - PilStatement::PolynomialIdentity(_, expression) => { + PilStatement::PolynomialIdentity(_, _attr, expression) => { if let Expression::BinaryOperation(left, BinaryOperator::Sub, right) = expression { write!(f, "{left} = {right};") } else { diff --git a/ast/src/parsed/mod.rs b/ast/src/parsed/mod.rs index b6a4b4c149..3a588c7c76 100644 --- a/ast/src/parsed/mod.rs +++ b/ast/src/parsed/mod.rs @@ -34,7 +34,7 @@ pub enum PilStatement { PolynomialConstantDeclaration(usize, Vec>), PolynomialConstantDefinition(usize, String, FunctionDefinition), PolynomialCommitDeclaration(usize, Vec>, Option>), - PolynomialIdentity(usize, Expression), + PolynomialIdentity(usize, Option, Expression), PlookupIdentity( usize, SelectedExpressions>, diff --git a/ast/src/parsed/visitor.rs b/ast/src/parsed/visitor.rs index 7bbec1f8f9..831249137b 100644 --- a/ast/src/parsed/visitor.rs +++ b/ast/src/parsed/visitor.rs @@ -208,7 +208,7 @@ impl ExpressionVisitable> for Pi PilStatement::Namespace(_, _, e) | PilStatement::PolynomialDefinition(_, _, e) - | PilStatement::PolynomialIdentity(_, e) + | PilStatement::PolynomialIdentity(_, _, e) | PilStatement::PublicDeclaration(_, _, _, None, e) | PilStatement::ConstantDefinition(_, _, e) | PilStatement::LetStatement(_, _, Some(e)) => e.visit_expressions_mut(f, o), @@ -250,7 +250,7 @@ impl ExpressionVisitable> for Pi PilStatement::Namespace(_, _, e) | PilStatement::PolynomialDefinition(_, _, e) - | PilStatement::PolynomialIdentity(_, e) + | PilStatement::PolynomialIdentity(_, _, e) | PilStatement::PublicDeclaration(_, _, _, None, e) | PilStatement::ConstantDefinition(_, _, e) | PilStatement::LetStatement(_, _, Some(e)) => e.visit_expressions(f, o), diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs index f7cfca2480..2057851a5c 100644 --- a/bberg/src/circuit_builder.rs +++ b/bberg/src/circuit_builder.rs @@ -79,7 +79,7 @@ impl CircuitBuilder for BBFiles { |name: &String| format!("polys.{name}_shift = Polynomial(polys.{name}.shifted());"); let check_circuit_transformation = |relation_name: &String| { format!( - "if (!evaluate_relation.template operator()<{name}_vm::{relation_name}>(\"{relation_name}\")) {{ + "if (!evaluate_relation.template operator()<{name}_vm::{relation_name}>(\"{relation_name}\", {name}_vm::get_relation_label_{relation_name})) {{ return false; }}", name = name, @@ -220,7 +220,7 @@ fn get_permutation_check_closure() -> String { } for (auto r : permutation_result) { if (r != 0) { - info(\"Tuple\", permutation_name, \"failed.\"); + info(\"Tuple \", permutation_name, \" failed.\"); return false; } } @@ -231,7 +231,8 @@ fn get_permutation_check_closure() -> String { fn get_relation_check_closure() -> String { " - const auto evaluate_relation = [&](const std::string& relation_name) { + const auto evaluate_relation = [&](const std::string& relation_name, + std::string (*debug_label)(int)) { typename Relation::SumcheckArrayOfValuesOverSubrelations result; for (auto& r : result) { r = 0; @@ -244,8 +245,9 @@ fn get_relation_check_closure() -> String { bool x = true; for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) { if (result[j] != 0) { + std::string row_name = debug_label(static_cast(j)); throw_or_abort( - format(\"Relation \", relation_name, \", subrelation index \", j, \" failed at row \", i)); + format(\"Relation \", relation_name, \", subrelation index \", row_name, \" failed at row \", i)); x = false; } } diff --git a/bberg/src/relation_builder.rs b/bberg/src/relation_builder.rs index 2e932e0b55..bdfcde4973 100644 --- a/bberg/src/relation_builder.rs +++ b/bberg/src/relation_builder.rs @@ -58,6 +58,7 @@ pub trait RelationBuilder { sub_relations: &[String], identities: &[BBIdentity], row_type: &str, + labels_lookup: String, ); /// Declare views @@ -85,23 +86,30 @@ impl RelationBuilder for BBFiles { // ----------------------- Create the relation files ----------------------- for (relation_name, analyzed_idents) in grouped_relations.iter() { - let (subrelations, identities, collected_polys, collected_shifts) = - create_identities(file_name, analyzed_idents); + let IdentitiesOutput { + subrelations, + identities, + collected_cols, + collected_shifts, + expression_labels, + } = create_identities(file_name, analyzed_idents); - shifted_polys.extend(collected_shifts); - - // let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts); // TODO: This can probably be moved into the create_identities function - let row_type = create_row_type(&capitalize(relation_name), &collected_polys); + let row_type = create_row_type(&capitalize(relation_name), &collected_cols); + // Aggregate all shifted polys + shifted_polys.extend(collected_shifts); + // Aggregate all rows all_rows.insert(relation_name.to_owned(), row_type.clone()); + let labels_lookup = create_relation_labels(relation_name, expression_labels); self.create_relation( file_name, relation_name, &subrelations, &identities, &row_type, + labels_lookup, ); } @@ -118,6 +126,7 @@ impl RelationBuilder for BBFiles { sub_relations: &[String], identities: &[BBIdentity], row_type: &str, + labels_lookup: String, ) { let includes = relation_includes(); let class_boilerplate = relation_class_boilerplate(name, sub_relations, identities); @@ -129,6 +138,8 @@ namespace proof_system::{root_name}_vm {{ {row_type}; +{labels_lookup} + {class_boilerplate} {export} @@ -362,34 +373,45 @@ fn craft_expression( } } +pub struct IdentitiesOutput { + subrelations: Vec, + identities: Vec, + collected_cols: Vec, + collected_shifts: Vec, + expression_labels: HashMap, +} + pub(crate) fn create_identities( file_name: &str, identities: &[Identity>], -) -> (Vec, Vec, Vec, Vec) { +) -> IdentitiesOutput { // We only want the expressions for now // When we have a poly type, we only need the left side of it - let expressions = identities + let ids = identities .iter() - .filter_map(|identity| { - if identity.kind == IdentityKind::Polynomial { - Some(identity.left.clone()) - } else { - None - } - }) + .filter(|identity| identity.kind == IdentityKind::Polynomial) .collect::>(); let mut identities = Vec::new(); let mut subrelations = Vec::new(); + let mut expression_labels: HashMap = HashMap::new(); // Each relation can be given a label, this label can be assigned here let mut collected_cols: HashSet = HashSet::new(); let mut collected_public_identities: HashSet = HashSet::new(); + // Collect labels for each identity + // TODO: shite + for (i, id) in ids.iter().enumerate() { + if let Some(label) = &id.attribute { + expression_labels.insert(i, label.clone()); + } + } + + let expressions = ids.iter().map(|id| id.left.clone()).collect::>(); for (i, expression) in expressions.iter().enumerate() { let relation_boilerplate = format!( "{file_name}_DECLARE_VIEWS({i}); ", ); - // TODO: deal with unwrap // TODO: collected pattern is shit let mut identity = create_identity( @@ -424,6 +446,45 @@ pub(crate) fn create_identities( }) .collect(); - // Returning both for now - (subrelations, identities, collected_cols, collected_shifts) + IdentitiesOutput { + subrelations, + identities, + collected_cols, + collected_shifts, + expression_labels, + } +} + +/// Relation labels +/// +/// To view relation labels we create a sparse switch that contains all of the collected labels +/// Whenever there is a failure, we can lookup into this mapping +/// +/// Note: this mapping will never be that big, so we are quite naive in implementation +/// It should be able to be called from else where with relation_name::get_relation_label +fn create_relation_labels(relation_name: &str, labels: HashMap) -> String { + let label_transformation = |(index, label)| { + format!( + "case {index}: + return \"{label}\"; + " + ) + }; + + let switch_statement: String = labels + .into_iter() + .map(label_transformation) + .collect::>() + .join("\n"); + + format!( + " + inline std::string get_relation_label_{relation_name}(int index) {{ + switch (index) {{ + {switch_statement} + }} + return std::to_string(index); + }} + " + ) } diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index 1c61c131f8..fc1075aeb4 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -127,7 +127,7 @@ PolynomialCommitDeclaration: PilStatement = { } PolynomialIdentity: PilStatement = { - "=" => PilStatement::PolynomialIdentity(start, Expression::BinaryOperation(l, BinaryOperator::Sub, r)) + "=" => PilStatement::PolynomialIdentity(start, attr, Expression::BinaryOperation(l, BinaryOperator::Sub, r)) } PolynomialNameList: Vec> = { diff --git a/pil_analyzer/src/statement_processor.rs b/pil_analyzer/src/statement_processor.rs index 8e8c4d9c36..22c081f8e4 100644 --- a/pil_analyzer/src/statement_processor.rs +++ b/pil_analyzer/src/statement_processor.rs @@ -199,8 +199,17 @@ where fn handle_identity_statement(&mut self, statement: PilStatement) -> Vec> { let (start, kind, attribute, left, right) = match statement { - PilStatement::PolynomialIdentity(start, expression) - | PilStatement::Expression(start, expression) => ( + PilStatement::PolynomialIdentity(start, attr, expression) => ( + start, + IdentityKind::Polynomial, + attr, + SelectedExpressions { + selector: Some(self.process_expression(expression)), + expressions: vec![], + }, + SelectedExpressions::default(), + ), + PilStatement::Expression(start, expression) => ( start, IdentityKind::Polynomial, None, diff --git a/type_check/src/lib.rs b/type_check/src/lib.rs index 7ec16e043b..91d5496bea 100644 --- a/type_check/src/lib.rs +++ b/type_check/src/lib.rs @@ -318,7 +318,7 @@ impl TypeChecker { let errors: Vec<_> = statements .iter() .filter_map(|s| match s { - ast::parsed::PilStatement::PolynomialIdentity(_, _) => None, + ast::parsed::PilStatement::PolynomialIdentity(_, _, _) => None, ast::parsed::PilStatement::PermutationIdentity( _, // _, //