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( _, // _, //