Add PhantomBusInteraction (#2183)

This PR adds a `Constr:: PhantomBusInteraction` variant. For now, it is ignored - if users want to use a bus, they need to express this in terms of phantom lookups / permutations as before this PR. I added a few `TODO(bus_interaction)` and opened #2184 to track support for phantom bus interactions. One use-case this could have before though is to trigger a "hand-written" witness generation for the bus, as discussed in the chat.
powdr-labs · Dec 6, 2024 · 3b45173 · 3b45173
1 parent 58a5c03
commit 3b45173
Show file tree

Hide file tree

Showing 16 changed files with 140 additions and 21 deletions.
diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs
@@ -427,6 +427,17 @@ impl<T: Display> Display for ConnectIdentity<T> {
     }
 }
 
+impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
+        write!(
+            f,
+            "Constr::PhantomBusInteraction({}, [{}]);",
+            self.multiplicity,
+            self.tuple.0.iter().map(ToString::to_string).format(", "),
+        )
+    }
+}
+
 impl Display for Reference {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {

diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs
@@ -949,7 +949,7 @@ impl<T> Children<AlgebraicExpression<T>> for SelectedExpressions<T> {
 
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
 pub struct PolynomialIdentity<T> {
-    // The ID is globally unique among identitites.
+    // The ID is globally unique among identities.
     pub id: u64,
     pub source: SourceRef,
     pub expression: AlgebraicExpression<T>,
@@ -966,7 +966,7 @@ impl<T> Children<AlgebraicExpression<T>> for PolynomialIdentity<T> {
 
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
 pub struct LookupIdentity<T> {
-    // The ID is globally unique among identitites.
+    // The ID is globally unique among identities.
     pub id: u64,
     pub source: SourceRef,
     pub left: SelectedExpressions<T>,
@@ -1017,7 +1017,7 @@ impl<T> Children<AlgebraicExpression<T>> for PhantomLookupIdentity<T> {
 
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
 pub struct PermutationIdentity<T> {
-    // The ID is globally unique among identitites.
+    // The ID is globally unique among identities.
     pub id: u64,
     pub source: SourceRef,
     pub left: SelectedExpressions<T>,
@@ -1035,11 +1035,11 @@ impl<T> Children<AlgebraicExpression<T>> for PermutationIdentity<T> {
 
 /// A witness generation helper for a permutation identity.
 ///
-/// This identity is used as a replactement for a permutation identity which has been turned into challenge-based polynomial identities.
+/// This identity is used as a replacement for a permutation identity which has been turned into challenge-based polynomial identities.
 /// This is ignored by the backend.
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
 pub struct PhantomPermutationIdentity<T> {
-    // The ID is globally unique among identitites.
+    // The ID is globally unique among identities.
     pub id: u64,
     pub source: SourceRef,
     pub left: SelectedExpressions<T>,
@@ -1057,7 +1057,7 @@ impl<T> Children<AlgebraicExpression<T>> for PhantomPermutationIdentity<T> {
 
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
 pub struct ConnectIdentity<T> {
-    // The ID is globally unique among identitites.
+    // The ID is globally unique among identities.
     pub id: u64,
     pub source: SourceRef,
     pub left: Vec<AlgebraicExpression<T>>,
@@ -1073,6 +1073,36 @@ impl<T> Children<AlgebraicExpression<T>> for ConnectIdentity<T> {
     }
 }
 
+#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema, PartialOrd, Ord)]
+pub struct ExpressionList<T>(pub Vec<AlgebraicExpression<T>>);
+
+impl<T> Children<AlgebraicExpression<T>> for ExpressionList<T> {
+    fn children_mut(&mut self) -> Box<dyn Iterator<Item = &mut AlgebraicExpression<T>> + '_> {
+        Box::new(self.0.iter_mut())
+    }
+    fn children(&self) -> Box<dyn Iterator<Item = &AlgebraicExpression<T>> + '_> {
+        Box::new(self.0.iter())
+    }
+}
+
+#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
+pub struct PhantomBusInteractionIdentity<T> {
+    // The ID is globally unique among identities.
+    pub id: u64,
+    pub source: SourceRef,
+    pub multiplicity: AlgebraicExpression<T>,
+    pub tuple: ExpressionList<T>,
+}
+
+impl<T> Children<AlgebraicExpression<T>> for PhantomBusInteractionIdentity<T> {
+    fn children_mut(&mut self) -> Box<dyn Iterator<Item = &mut AlgebraicExpression<T>> + '_> {
+        Box::new(once(&mut self.multiplicity).chain(self.tuple.children_mut()))
+    }
+    fn children(&self) -> Box<dyn Iterator<Item = &AlgebraicExpression<T>> + '_> {
+        Box::new(once(&self.multiplicity).chain(self.tuple.children()))
+    }
+}
+
 #[derive(
     Debug,
     PartialEq,
@@ -1092,6 +1122,7 @@ pub enum Identity<T> {
     Permutation(PermutationIdentity<T>),
     PhantomPermutation(PhantomPermutationIdentity<T>),
     Connect(ConnectIdentity<T>),
+    PhantomBusInteraction(PhantomBusInteractionIdentity<T>),
 }
 
 impl<T> Identity<T> {
@@ -1111,6 +1142,7 @@ impl<T> Identity<T> {
             Identity::Permutation(i) => i.id,
             Identity::PhantomPermutation(i) => i.id,
             Identity::Connect(i) => i.id,
+            Identity::PhantomBusInteraction(i) => i.id,
         }
     }
 
@@ -1122,6 +1154,7 @@ impl<T> Identity<T> {
             Identity::Permutation(_) => IdentityKind::Permutation,
             Identity::PhantomPermutation(_) => IdentityKind::PhantomPermutation,
             Identity::Connect(_) => IdentityKind::Connect,
+            Identity::PhantomBusInteraction(_) => IdentityKind::PhantomBusInteraction,
         }
     }
 }
@@ -1135,6 +1168,7 @@ impl<T> SourceReference for Identity<T> {
             Identity::Permutation(i) => &i.source,
             Identity::PhantomPermutation(i) => &i.source,
             Identity::Connect(i) => &i.source,
+            Identity::PhantomBusInteraction(i) => &i.source,
         }
     }
 
@@ -1146,6 +1180,7 @@ impl<T> SourceReference for Identity<T> {
             Identity::Permutation(i) => &mut i.source,
             Identity::PhantomPermutation(i) => &mut i.source,
             Identity::Connect(i) => &mut i.source,
+            Identity::PhantomBusInteraction(i) => &mut i.source,
         }
     }
 }
@@ -1159,6 +1194,7 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
             Identity::Permutation(i) => i.children_mut(),
             Identity::PhantomPermutation(i) => i.children_mut(),
             Identity::Connect(i) => i.children_mut(),
+            Identity::PhantomBusInteraction(i) => i.children_mut(),
         }
     }
 
@@ -1170,6 +1206,7 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
             Identity::Permutation(i) => i.children(),
             Identity::PhantomPermutation(i) => i.children(),
             Identity::Connect(i) => i.children(),
+            Identity::PhantomBusInteraction(i) => i.children(),
         }
     }
 }
@@ -1184,6 +1221,7 @@ pub enum IdentityKind {
     Permutation,
     PhantomPermutation,
     Connect,
+    PhantomBusInteraction,
 }
 
 impl<T> SelectedExpressions<T> {

diff --git a/backend/src/estark/json_exporter/expression_counter.rs b/backend/src/estark/json_exporter/expression_counter.rs
@@ -60,7 +60,9 @@ impl<T: FieldElement> ExpressionCounter for Identity<T> {
                 connect_identity.left.len() + connect_identity.right.len()
             }
             // phantom identities are not relevant in this context
-            Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => 0,
+            Identity::PhantomLookup(..)
+            | Identity::PhantomPermutation(..)
+            | Identity::PhantomBusInteraction(..) => 0,
         }
     }
 }

diff --git a/backend/src/estark/json_exporter/mod.rs b/backend/src/estark/json_exporter/mod.rs
@@ -135,7 +135,9 @@ pub fn export<T: FieldElement>(analyzed: &Analyzed<T>) -> PIL {
                             line,
                         });
                     }
-                    Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => {
+                    Identity::PhantomLookup(..)
+                    | Identity::PhantomPermutation(..)
+                    | Identity::PhantomBusInteraction(..) => {
                         // These are not relevant for the PIL
                     }
                 }

diff --git a/backend/src/halo2/circuit_builder.rs b/backend/src/halo2/circuit_builder.rs
@@ -320,7 +320,9 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
                             .collect()
                     });
                 }
-                Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => {
+                Identity::PhantomLookup(..)
+                | Identity::PhantomPermutation(..)
+                | Identity::PhantomBusInteraction(..) => {
                     // Phantom identities are only used in witness generation
                 }
             }

diff --git a/backend/src/mock/connection_constraint_checker.rs b/backend/src/mock/connection_constraint_checker.rs
@@ -68,6 +68,8 @@ impl<F: FieldElement> Connection<F> {
             | Identity::PhantomPermutation(PhantomPermutationIdentity { left, right, .. }) => {
                 Ok((left.clone(), right.clone(), ConnectionKind::Permutation))
             }
+            // TODO(bus_interaction)
+            Identity::PhantomBusInteraction(_) => Err(()),
         }?;
 
         // This connection is not localized yet: Its expression's PolyIDs point to the global PIL, not the local PIL.

diff --git a/backend/src/stwo/circuit_builder.rs b/backend/src/stwo/circuit_builder.rs
@@ -108,8 +108,9 @@ impl<T: FieldElement> FrameworkEval for PowdrEval<T> {
                 Identity::Permutation(..) => {
                     unimplemented!("Permutation is not implemented in stwo yet")
                 }
-                Identity::PhantomPermutation(..) => {}
-                Identity::PhantomLookup(..) => {}
+                Identity::PhantomPermutation(..)
+                | Identity::PhantomLookup(..)
+                | Identity::PhantomBusInteraction(..) => {}
             }
         }
         eval

diff --git a/executor/src/witgen/global_constraints.rs b/executor/src/witgen/global_constraints.rs
@@ -332,6 +332,11 @@ fn propagate_constraints<T: FieldElement>(
             // permutation identities are stronger than just range constraints, so we do nothing
             false
         }
+        Identity::PhantomBusInteraction(..) => {
+            // TODO(bus_interaction): If we can statically match sends & receives, we could extract
+            // range constraints from them.
+            false
+        }
     }
 }
 

diff --git a/executor/src/witgen/identity_processor.rs b/executor/src/witgen/identity_processor.rs
@@ -55,6 +55,8 @@ impl<'a, 'c, T: FieldElement, Q: QueryCallback<T>> IdentityProcessor<'a, 'c, T,
                 //     "Identity of kind {kind:?} is not supported by the identity processor."
                 // )
             }
+            // TODO(bus_interaction)
+            Identity::PhantomBusInteraction(..) => Ok(EvalValue::complete(Vec::new())),
         };
         report_identity_solving(identity, &result);
         result

diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs
@@ -284,6 +284,8 @@ impl<'a, T: FieldElement> MachineExtractor<'a, T> {
                     Identity::Connect(..) => {
                         unimplemented!()
                     }
+                    // TODO(bus_interaction)
+                    Identity::PhantomBusInteraction(..) => {}
                 };
             }
             if witnesses.len() == count {
@@ -312,6 +314,12 @@ impl<'a, T: FieldElement> MachineExtractor<'a, T> {
             }
             Identity::Polynomial(i) => self.fixed.polynomial_references(i),
             Identity::Connect(i) => self.fixed.polynomial_references(i),
+            Identity::PhantomBusInteraction(i) => self
+                .fixed
+                .polynomial_references(&i.tuple)
+                .into_iter()
+                .chain(self.fixed.polynomial_references(&i.multiplicity))
+                .collect(),
         }
     }
 }

diff --git a/executor/src/witgen/machines/write_once_memory.rs b/executor/src/witgen/machines/write_once_memory.rs
@@ -3,7 +3,7 @@ use std::collections::{BTreeMap, HashMap};
 use itertools::{Either, Itertools};
 
 use num_traits::One;
-use powdr_ast::analyzed::{PolyID, PolynomialType};
+use powdr_ast::analyzed::{Identity, PolyID, PolynomialType};
 use powdr_number::{DegreeType, FieldElement};
 
 use crate::witgen::data_structures::mutable_state::MutableState;
@@ -49,7 +49,12 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> {
         fixed_data: &'a FixedData<'a, T>,
         parts: &MachineParts<'a, T>,
     ) -> Option<Self> {
-        if !parts.identities.is_empty() {
+        if parts
+            .identities
+            .iter()
+            // The only identity we'd expect is a PhantomBusInteraction
+            .any(|id| !matches!(id, Identity::PhantomBusInteraction(_)))
+        {
             return None;
         }
 

diff --git a/pil-analyzer/src/condenser.rs b/pil-analyzer/src/condenser.rs
@@ -11,9 +11,10 @@ use std::{
 
 use powdr_ast::analyzed::{
     AlgebraicExpression, AlgebraicReference, Analyzed, ConnectIdentity, DegreeRange, Expression,
-    FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PhantomLookupIdentity,
-    PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialType, PublicDeclaration,
-    SelectedExpressions, SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind,
+    ExpressionList, FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity,
+    PhantomBusInteractionIdentity, PhantomLookupIdentity, PhantomPermutationIdentity, PolyID,
+    PolynomialIdentity, PolynomialType, PublicDeclaration, SelectedExpressions, SolvedTraitImpls,
+    StatementIdentifier, Symbol, SymbolKind,
 };
 use powdr_ast::parsed::{
     asm::{AbsoluteSymbolPath, SymbolPath},
@@ -785,6 +786,16 @@ fn to_constraint<T: FieldElement>(
             }
             .into()
         }
+        "PhantomBusInteraction" => PhantomBusInteractionIdentity {
+            id: counters.dispense_identity_id(),
+            source,
+            multiplicity: to_expr(&fields[0]),
+            tuple: ExpressionList(match fields[1].as_ref() {
+                Value::Array(fields) => fields.iter().map(|f| to_expr(f)).collect(),
+                _ => panic!("Expected array, got {:?}", fields[1]),
+            }),
+        }
+        .into(),
         _ => panic!("Expected constraint but got {constraint}"),
     }
 }

diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs
@@ -556,6 +556,13 @@ fn remove_trivial_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
                 left.expressions.is_empty().then_some(index)
             }
             Identity::Connect(..) => None,
+            Identity::PhantomBusInteraction(id) => {
+                if id.tuple.0.is_empty() {
+                    unreachable!("Unexpected empty bus interaction: {}", id);
+                } else {
+                    None
+                }
+            }
         })
         .collect();
     pil_file.remove_identities(&to_remove);
@@ -576,6 +583,7 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
                 Identity::Permutation(..) => 3,
                 Identity::PhantomPermutation(..) => 4,
                 Identity::Connect(..) => 5,
+                Identity::PhantomBusInteraction(..) => 6,
             };
 
             discriminant(self)
@@ -635,6 +643,11 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
                             left: c, right: d, ..
                         }),
                     ) => a.cmp(c).then_with(|| b.cmp(d)),
+                    (Identity::PhantomBusInteraction(_), Identity::PhantomBusInteraction(_)) => {
+                        unimplemented!(
+                            "Bus interactions should have been removed before this point."
+                        )
+                    }
                     _ => {
                         unreachable!("Different identity types would have different discriminants.")
                     }
@@ -662,11 +675,13 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
         .identities
         .iter()
         .enumerate()
-        .filter_map(|(index, identity)| {
-            match identity_expressions.insert(CanonicalIdentity(identity)) {
+        .filter_map(|(index, identity)| match identity {
+            // Duplicate bus interactions should not be removed, because that changes the statement.
+            Identity::PhantomBusInteraction(_) => None,
+            _ => match identity_expressions.insert(CanonicalIdentity(identity)) {
                 false => Some(index),
                 true => None,
-            }
+            },
         })
         .collect();
     pil_file.remove_identities(&to_remove);

diff --git a/plonky3/src/circuit_builder.rs b/plonky3/src/circuit_builder.rs
@@ -459,7 +459,9 @@ where
                     unimplemented!("Plonky3 does not support permutations")
                 }
                 Identity::Connect(..) => unimplemented!("Plonky3 does not support connections"),
-                Identity::PhantomPermutation(..) | Identity::PhantomLookup(..) => {
+                Identity::PhantomPermutation(_)
+                | Identity::PhantomLookup(_)
+                | Identity::PhantomBusInteraction(_) => {
                     // phantom identities are only used in witgen
                 }
             }

diff --git a/std/prelude.asm b/std/prelude.asm
@@ -41,7 +41,16 @@ enum Constr {
     PhantomPermutation((Option<expr>, Option<expr>), (expr, expr)[]),
 
     /// A connection constraint (copy constraint), result of the "connect" operator.
-    Connection((expr, expr)[])
+    Connection((expr, expr)[]),
+
+    /// A "phantom" bus interaction, i.e., an annotation for witness generation.
+    /// The actual constraint should be enforced via other constraints.
+    /// Contains:
+    /// - An expression for the multiplicity.
+    /// - The tuple added to the bus.
+    /// WARNING: As of now, this annotation is largely ignored. When using the bus,
+    /// make sure that you also add phantom lookup / permutation constraints.
+    PhantomBusInteraction(expr, expr[])
 }
 
 /// This is the result of the "$" operator. It can be used as the left and