Avoid redundant computation in Protogalaxy

Cargo.toml

@@ -15,6 +15,8 @@ members = [
     "asm_to_pil",
     "halo2",
     "backend",
+    "bberg",
+    "bberg_pil_cli",
     "ast",
     "analysis",
     "linker",

asm_to_pil/src/vm_to_constrained.rs

@@ -144,6 +144,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
                                     ),
                                     PilStatement::PolynomialIdentity(
                                         0,
+                                        None,
                                         lhs - (Expression::from(T::one())
                                             - next_reference("first_step"))
                                             * direct_reference(pc_update_name),
@@ -154,10 +155,14 @@ impl<T: FieldElement> ASMPILConverter<T> {
                             ReadOnly => {
                                 let not_reset: Expression<T> =
                                     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)]
                             }
                         }
                     })
@@ -175,6 +180,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
 
         self.pil.push(PilStatement::PlookupIdentity(
             0,
+            None,
             SelectedExpressions {
                 selector: None,
                 expressions: self
@@ -389,7 +395,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
                 });
 
                 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,13 +412,14 @@ impl<T: FieldElement> ASMPILConverter<T> {
                             }
                             (None, expr) => self.pil.push(PilStatement::PolynomialIdentity(
                                 0,
+                                None,
                                 direct_reference(&instruction_flag) * expr.clone(),
                             )),
                         }
                     } else {
                         match &mut statement {
-                            PilStatement::PermutationIdentity(_, left, _)
-                            | PilStatement::PlookupIdentity(_, left, _) => {
+                            PilStatement::PermutationIdentity(_, _attr, left, _)
+                            | PilStatement::PlookupIdentity(_, _attr, left, _) => {
                                 assert!(
                                     left.selector.is_none(),
                                     "LHS selector not supported, could and-combine with instruction flag later."
@@ -715,6 +722,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
             .sum();
         self.pil.push(PilStatement::PolynomialIdentity(
             0,
+            None,
             direct_reference(register) - assign_constraint,
         ));
     }

ast/src/analyzed/display.rs

@@ -149,7 +149,13 @@ impl<T: Display> Display for Identity<Expression<T>> {
                 }
             }
             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),
         }
     }

ast/src/analyzed/mod.rs

@@ -226,6 +226,7 @@ impl<T> Analyzed<T> {
         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,11 +505,16 @@ pub struct Identity<Expr> {
     /// The ID is specific to the identity kind.
     pub id: u64,
     pub kind: IdentityKind,
+    pub attribute: Option<String>,
     pub source: SourceRef,
     /// For a simple polynomial identity, the selector contains
     /// the actual expression (see expression_for_poly_id).
-    pub left: SelectedExpressions<Expr>,
-    pub right: SelectedExpressions<Expr>,
+    //
+    //
+    // NTS(Md) Both left and right are only used in the case of perm / plookup
+    //
+    pub left: SelectedExpressions<Expr>, // left is selector expressions  - for an arithmetic gate, the entire relation is in SL
+    pub right: SelectedExpressions<Expr>, // right is the overall expressions
 }
 
 impl<Expr> Identity<Expr> {
@@ -530,7 +536,7 @@ pub enum IdentityKind {
     Polynomial,
     Plookup,
     Permutation,
-    Connect,
+    Connect, // not used
 }
 
 impl<T> SelectedExpressions<AlgebraicExpression<T>> {

ast/src/parsed/display.rs

@@ -383,15 +383,20 @@ impl<T: Display> Display for PilStatement<T> {
                     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 {
                     write!(f, "{expression} = 0;")
                 }
             }
-            PilStatement::PlookupIdentity(_, left, right) => write!(f, "{left} in {right};"),
-            PilStatement::PermutationIdentity(_, left, right) => write!(f, "{left} is {right};"),
+            PilStatement::PlookupIdentity(_, _, left, right) => write!(f, "{left} in {right};"),
+            PilStatement::PermutationIdentity(
+                _, //
+                _, //
+                left,
+                right,
+            ) => write!(f, "{left} is {right};"), //
             PilStatement::ConnectIdentity(_, left, right) => write!(
                 f,
                 "{{ {} }} connect {{ {} }};",

ast/src/parsed/mod.rs

@@ -34,14 +34,16 @@ pub enum PilStatement<T> {
     PolynomialConstantDeclaration(usize, Vec<PolynomialName<T>>),
     PolynomialConstantDefinition(usize, String, FunctionDefinition<T>),
     PolynomialCommitDeclaration(usize, Vec<PolynomialName<T>>, Option<FunctionDefinition<T>>),
-    PolynomialIdentity(usize, Expression<T>),
+    PolynomialIdentity(usize, Option<String>, Expression<T>),
     PlookupIdentity(
         usize,
+        Option<String>,
         SelectedExpressions<Expression<T>>,
         SelectedExpressions<Expression<T>>,
     ),
     PermutationIdentity(
         usize,
+        Option<String>,
         SelectedExpressions<Expression<T>>,
         SelectedExpressions<Expression<T>>,
     ),
@@ -50,6 +52,11 @@ pub enum PilStatement<T> {
     Expression(usize, Expression<T>),
 }
 
+#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
+pub struct Attribute {
+    pub name: Option<String>,
+}
+
 #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
 pub struct SelectedExpressions<Expr> {
     pub selector: Option<Expr>,

ast/src/parsed/visitor.rs

@@ -192,8 +192,13 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> for Pi
     {
         match self {
             PilStatement::Expression(_, e) => e.visit_expressions_mut(f, o),
-            PilStatement::PlookupIdentity(_, left, right)
-            | PilStatement::PermutationIdentity(_, left, right) => [left, right]
+            PilStatement::PlookupIdentity(_, _, 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
@@ -203,7 +208,7 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> 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),
@@ -229,8 +234,13 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> for Pi
     {
         match self {
             PilStatement::Expression(_, e) => e.visit_expressions(f, o),
-            PilStatement::PlookupIdentity(_, left, right)
-            | PilStatement::PermutationIdentity(_, left, right) => [left, right]
+            PilStatement::PlookupIdentity(_, _, 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
@@ -240,7 +250,7 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> 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),

backend/Cargo.toml

@@ -5,9 +5,13 @@ edition = "2021"
 
 [features]
 halo2 = ["dep:halo2"]
+# TODO: enable feature flag for bberg backend
+# bberg = ["dep:bberg"]
 
 [dependencies]
 halo2 = { path = "../halo2", optional = true }
+bberg = { path = "../bberg"}
+
 pil_analyzer = { path = "../pil_analyzer" }
 number = { path = "../number" }
 ast = { path = "../ast" }

backend/src/bberg_impl.rs

@@ -0,0 +1,68 @@
+use std::io::{self};
+
+use crate::{BackendImpl, BackendImplWithSetup, Proof};
+use ast::analyzed::Analyzed;
+
+// We do not directly have a bberg prover at the moment
+// however we can just perform codegen
+use bberg::bberg_codegen::BBergCodegen;
+use number::{DegreeType, FieldElement};
+
+impl<T: FieldElement> BackendImpl<T> for BBergCodegen {
+    fn new(degree: DegreeType) -> Self {
+        BBergCodegen::assert_field_is_compatible::<T>();
+        BBergCodegen::new(degree)
+    }
+
+    fn prove(
+        &self,
+        pil: &Analyzed<T>,
+        fixed: &[(String, Vec<T>)],
+        witness: &[(String, Vec<T>)],
+        _prev_proof: Option<Proof>,
+        bname: Option<String>,
+    ) -> (Option<Proof>, Option<String>) {
+        self.build_ast(pil, fixed, witness, bname);
+
+        // Note(md): In the current bberg impl we do not produce proofs here
+        // as we do cpp code generation, and then create proofs with bberg
+        // This may change in the future when the library matures to be more pluggable
+        (None, None)
+    }
+}
+
+impl<T: FieldElement> BackendImplWithSetup<T> for BBergCodegen {
+    fn new_from_setup(mut input: &mut dyn io::Read) -> Result<Self, io::Error> {
+        BBergCodegen::assert_field_is_compatible::<T>();
+        BBergCodegen::new_from_setup(&mut input)
+    }
+
+    // TODO: implement this
+    fn write_setup(&self, _output: &mut dyn io::Write) -> Result<(), io::Error> {
+        Ok(())
+        // self.write_setup(&mut output)
+    }
+}
+
+pub struct BBergMock;
+impl<T: FieldElement> BackendImpl<T> for BBergMock {
+    fn new(_degree: DegreeType) -> Self {
+        Self
+    }
+
+    fn prove(
+        &self,
+        _pil: &Analyzed<T>,
+        _fixed: &[(String, Vec<T>)],
+        _witness: &[(String, Vec<T>)],
+        prev_proof: Option<Proof>,
+        _bname: Option<String>,
+    ) -> (Option<Proof>, Option<String>) {
+        if prev_proof.is_some() {
+            unimplemented!("BBergMock backend does not support aggregation");
+        }
+
+        // TODO: mock prover
+        unimplemented!("BBergMock backend is not implemented");
+    }
+}

backend/src/halo2_impl.rs

@@ -17,6 +17,7 @@ impl<T: FieldElement> BackendImpl<T> for Halo2Prover {
         fixed: &[(String, Vec<T>)],
         witness: &[(String, Vec<T>)],
         prev_proof: Option<Proof>,
+        _name: Option<String>,
     ) -> (Option<Proof>, Option<String>) {
         let proof = match prev_proof {
             Some(proof) => self.prove_aggr(pil, fixed, witness, proof),
@@ -27,7 +28,7 @@ impl<T: FieldElement> BackendImpl<T> for Halo2Prover {
     }
 }
 
-impl<T: FieldElement> BackendImplWithSetup<T> for halo2::Halo2Prover {
+impl<T: FieldElement> BackendImplWithSetup<T> for Halo2Prover {
     fn new_from_setup(mut input: &mut dyn io::Read) -> Result<Self, io::Error> {
         Halo2Prover::assert_field_is_compatible::<T>();
         Halo2Prover::new_from_setup(&mut input)
@@ -50,6 +51,7 @@ impl<T: FieldElement> BackendImpl<T> for Halo2Mock {
         fixed: &[(String, Vec<T>)],
         witness: &[(String, Vec<T>)],
         prev_proof: Option<Proof>,
+        _name: Option<String>,
     ) -> (Option<Proof>, Option<String>) {
         if prev_proof.is_some() {
             unimplemented!("Halo2Mock backend does not support aggregation");