Skip to content

Commit 6440b72

Browse files
qwang98qwang98
authored
Native bus interaction (#2508)
WIP. For Stwo native logup use.
1 parent d81f8bd commit 6440b72

File tree

12 files changed

+105
-10
lines changed

12 files changed

+105
-10
lines changed

‎ast/src/analyzed/display.rs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -427,6 +427,19 @@ impl<T: Display> Display for ConnectIdentity<T> {
427427
}
428428
}
429429

430+
impl<T: Display> Display for BusInteractionIdentity<T> {
431+
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
432+
write!(
433+
f,
434+
"Constr::BusInteraction({}, {}, [{}], {});",
435+
self.multiplicity,
436+
self.bus_id,
437+
self.payload.0.iter().map(ToString::to_string).format(", "),
438+
self.latch
439+
)
440+
}
441+
}
442+
430443
impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
431444
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
432445
write!(

‎ast/src/analyzed/mod.rs

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1024,6 +1024,39 @@ impl<T> Children<AlgebraicExpression<T>> for ExpressionList<T> {
10241024
}
10251025
}
10261026

1027+
#[derive(
1028+
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Serialize, Deserialize, JsonSchema, Hash,
1029+
)]
1030+
/// For documentation, see the equivalent `Constr` variant in std/prelude.asm.
1031+
pub struct BusInteractionIdentity<T> {
1032+
// The ID is globally unique among identities.
1033+
pub id: u64,
1034+
pub source: SourceRef,
1035+
pub multiplicity: AlgebraicExpression<T>,
1036+
pub bus_id: AlgebraicExpression<T>,
1037+
pub payload: ExpressionList<T>,
1038+
pub latch: AlgebraicExpression<T>,
1039+
}
1040+
1041+
impl<T> Children<AlgebraicExpression<T>> for BusInteractionIdentity<T> {
1042+
fn children_mut(&mut self) -> Box<dyn Iterator<Item = &mut AlgebraicExpression<T>> + '_> {
1043+
Box::new(
1044+
once(&mut self.multiplicity)
1045+
.chain(once(&mut self.bus_id))
1046+
.chain(self.payload.children_mut())
1047+
.chain(once(&mut self.latch)),
1048+
)
1049+
}
1050+
fn children(&self) -> Box<dyn Iterator<Item = &AlgebraicExpression<T>> + '_> {
1051+
Box::new(
1052+
once(&self.multiplicity)
1053+
.chain(once(&self.bus_id))
1054+
.chain(self.payload.children())
1055+
.chain(once(&self.latch)),
1056+
)
1057+
}
1058+
}
1059+
10271060
#[derive(
10281061
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Serialize, Deserialize, JsonSchema, Hash,
10291062
)]
@@ -1086,6 +1119,7 @@ pub enum Identity<T> {
10861119
Permutation(PermutationIdentity<T>),
10871120
PhantomPermutation(PhantomPermutationIdentity<T>),
10881121
Connect(ConnectIdentity<T>),
1122+
BusInteraction(BusInteractionIdentity<T>),
10891123
PhantomBusInteraction(PhantomBusInteractionIdentity<T>),
10901124
}
10911125

@@ -1109,6 +1143,7 @@ impl<T> Identity<T> {
11091143
Identity::Permutation(i) => i.id,
11101144
Identity::PhantomPermutation(i) => i.id,
11111145
Identity::Connect(i) => i.id,
1146+
Identity::BusInteraction(i) => i.id,
11121147
Identity::PhantomBusInteraction(i) => i.id,
11131148
}
11141149
}
@@ -1121,6 +1156,7 @@ impl<T> Identity<T> {
11211156
Identity::Permutation(_) => IdentityKind::Permutation,
11221157
Identity::PhantomPermutation(_) => IdentityKind::PhantomPermutation,
11231158
Identity::Connect(_) => IdentityKind::Connect,
1159+
Identity::BusInteraction(_) => IdentityKind::BusInteraction,
11241160
Identity::PhantomBusInteraction(_) => IdentityKind::PhantomBusInteraction,
11251161
}
11261162
}
@@ -1135,6 +1171,7 @@ impl<T> SourceReference for Identity<T> {
11351171
Identity::Permutation(i) => &i.source,
11361172
Identity::PhantomPermutation(i) => &i.source,
11371173
Identity::Connect(i) => &i.source,
1174+
Identity::BusInteraction(i) => &i.source,
11381175
Identity::PhantomBusInteraction(i) => &i.source,
11391176
}
11401177
}
@@ -1147,6 +1184,7 @@ impl<T> SourceReference for Identity<T> {
11471184
Identity::Permutation(i) => &mut i.source,
11481185
Identity::PhantomPermutation(i) => &mut i.source,
11491186
Identity::Connect(i) => &mut i.source,
1187+
Identity::BusInteraction(i) => &mut i.source,
11501188
Identity::PhantomBusInteraction(i) => &mut i.source,
11511189
}
11521190
}
@@ -1161,6 +1199,7 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
11611199
Identity::Permutation(i) => i.children_mut(),
11621200
Identity::PhantomPermutation(i) => i.children_mut(),
11631201
Identity::Connect(i) => i.children_mut(),
1202+
Identity::BusInteraction(i) => i.children_mut(),
11641203
Identity::PhantomBusInteraction(i) => i.children_mut(),
11651204
}
11661205
}
@@ -1173,6 +1212,7 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
11731212
Identity::Permutation(i) => i.children(),
11741213
Identity::PhantomPermutation(i) => i.children(),
11751214
Identity::Connect(i) => i.children(),
1215+
Identity::BusInteraction(i) => i.children(),
11761216
Identity::PhantomBusInteraction(i) => i.children(),
11771217
}
11781218
}
@@ -1188,6 +1228,7 @@ pub enum IdentityKind {
11881228
Permutation,
11891229
PhantomPermutation,
11901230
Connect,
1231+
BusInteraction,
11911232
PhantomBusInteraction,
11921233
}
11931234

‎backend/src/estark/json_exporter/expression_counter.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,9 @@ impl<T: FieldElement> ExpressionCounter for Identity<T> {
5959
Identity::Connect(connect_identity) => {
6060
connect_identity.left.len() + connect_identity.right.len()
6161
}
62+
Identity::BusInteraction(bus_interaction_identity) => {
63+
3 + bus_interaction_identity.payload.0.len() // multiplicity/latch/bus_id + payload
64+
}
6265
// phantom identities are not relevant in this context
6366
Identity::PhantomLookup(..)
6467
| Identity::PhantomPermutation(..)

‎backend/src/estark/json_exporter/mod.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,9 @@ pub fn export<T: FieldElement>(analyzed: &Analyzed<T>) -> PIL {
135135
line,
136136
});
137137
}
138+
Identity::BusInteraction(..) => {
139+
// Native bus interactions are not relevant in estark, which supports native lookup/permutations
140+
}
138141
Identity::PhantomLookup(..)
139142
| Identity::PhantomPermutation(..)
140143
| Identity::PhantomBusInteraction(..) => {

‎backend/src/halo2/circuit_builder.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -332,6 +332,9 @@ impl<T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCircui
332332
.collect()
333333
});
334334
}
335+
Identity::BusInteraction(..) => {
336+
// Native bus interactions are not relevant in halo2, which supports native lookup/permutations
337+
}
335338
Identity::PhantomLookup(..)
336339
| Identity::PhantomPermutation(..)
337340
| Identity::PhantomBusInteraction(..) => {

‎backend/src/mock/connection_constraint_checker.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ impl<F: FieldElement> Connection<F> {
7878
None,
7979
)),
8080
// Handled by bus constraint checker
81-
Identity::PhantomBusInteraction(_) => Err(()),
81+
Identity::BusInteraction(_) | Identity::PhantomBusInteraction(_) => Err(()),
8282
}?;
8383

8484
// This connection is not localized yet: Its expression's PolyIDs point to the global PIL, not the local PIL.

‎backend/src/stwo/circuit_builder.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,8 @@ impl FrameworkEval for PowdrEval {
300300
Identity::Permutation(..) => {
301301
unimplemented!("Permutation is not implemented in stwo yet")
302302
}
303-
Identity::PhantomPermutation(..)
303+
Identity::BusInteraction(..)
304+
| Identity::PhantomPermutation(..)
304305
| Identity::PhantomLookup(..)
305306
| Identity::PhantomBusInteraction(..) => {}
306307
}

‎executor/src/witgen/data_structures/identity.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -249,6 +249,7 @@ fn convert_identity<T: FieldElement>(
249249
identity.clone(),
250250
))]
251251
}
252+
AnalyzedIdentity::BusInteraction(_) => vec![],
252253
AnalyzedIdentity::PhantomBusInteraction(bus_interaction) => {
253254
vec![convert_phantom_bus_interaction(bus_interaction)]
254255
}

‎pil-analyzer/src/condenser.rs

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,11 @@ use std::{
1010
};
1111

1212
use powdr_ast::analyzed::{
13-
AlgebraicExpression, AlgebraicReference, Analyzed, ConnectIdentity, DegreeRange, Expression,
14-
ExpressionList, FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity,
15-
PhantomBusInteractionIdentity, PhantomLookupIdentity, PhantomPermutationIdentity, PolyID,
16-
PolynomialIdentity, PolynomialType, PublicDeclaration, SelectedExpressions, SolvedTraitImpls,
17-
StatementIdentifier, Symbol, SymbolKind,
13+
AlgebraicExpression, AlgebraicReference, Analyzed, BusInteractionIdentity, ConnectIdentity,
14+
DegreeRange, Expression, ExpressionList, FunctionValueDefinition, Identity, LookupIdentity,
15+
PermutationIdentity, PhantomBusInteractionIdentity, PhantomLookupIdentity,
16+
PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialType, PublicDeclaration,
17+
SelectedExpressions, SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind,
1818
};
1919
use powdr_ast::parsed::{
2020
asm::{AbsoluteSymbolPath, SymbolPath},
@@ -792,6 +792,18 @@ fn to_constraint<T: FieldElement>(
792792
}
793793
.into()
794794
}
795+
"BusInteraction" => BusInteractionIdentity {
796+
id: counters.dispense_identity_id(),
797+
source,
798+
multiplicity: to_expr(&fields[0]),
799+
bus_id: to_expr(&fields[1]),
800+
payload: ExpressionList(match fields[2].as_ref() {
801+
Value::Array(fields) => fields.iter().map(|f| to_expr(f)).collect(),
802+
_ => panic!("Expected array, got {:?}", fields[2]),
803+
}),
804+
latch: to_expr(&fields[3]),
805+
}
806+
.into(),
795807
"PhantomBusInteraction" => PhantomBusInteractionIdentity {
796808
id: counters.dispense_identity_id(),
797809
source,

‎pilopt/src/lib.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -717,6 +717,7 @@ fn remove_trivial_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
717717
left.expressions.is_empty().then_some(index)
718718
}
719719
Identity::Connect(..) => None,
720+
Identity::BusInteraction(..) => None,
720721
// Bus interactions send at least their bus ID, which needs to
721722
// be received for the bus argument to hold.
722723
Identity::PhantomBusInteraction(..) => None,
@@ -740,7 +741,8 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
740741
Identity::Permutation(..) => 3,
741742
Identity::PhantomPermutation(..) => 4,
742743
Identity::Connect(..) => 5,
743-
Identity::PhantomBusInteraction(..) => 6,
744+
Identity::BusInteraction(..) => 6,
745+
Identity::PhantomBusInteraction(..) => 7,
744746
};
745747

746748
discriminant(self)
@@ -800,7 +802,8 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
800802
left: c, right: d, ..
801803
}),
802804
) => a.cmp(c).then_with(|| b.cmp(d)),
803-
(Identity::PhantomBusInteraction(_), Identity::PhantomBusInteraction(_)) => {
805+
(Identity::BusInteraction(_), Identity::BusInteraction(_))
806+
| (Identity::PhantomBusInteraction(_), Identity::PhantomBusInteraction(_)) => {
804807
unimplemented!(
805808
"Bus interactions should have been removed before this point."
806809
)
@@ -834,6 +837,7 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
834837
.enumerate()
835838
.filter_map(|(index, identity)| match identity {
836839
// Duplicate bus interactions should not be removed, because that changes the statement.
840+
Identity::BusInteraction(_) => None,
837841
Identity::PhantomBusInteraction(_) => None,
838842
_ => match identity_expressions.insert(CanonicalIdentity(identity)) {
839843
false => Some(index),

‎plonky3/src/circuit_builder.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,8 @@ where
386386
unimplemented!("Plonky3 does not support permutations")
387387
}
388388
Identity::Connect(..) => unimplemented!("Plonky3 does not support connections"),
389-
Identity::PhantomPermutation(_)
389+
Identity::BusInteraction(_)
390+
| Identity::PhantomPermutation(_)
390391
| Identity::PhantomLookup(_)
391392
| Identity::PhantomBusInteraction(_) => {
392393
// phantom identities are only used in witgen

‎std/prelude.asm

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,19 @@ enum Constr {
4343
/// A connection constraint (copy constraint), result of the "connect" operator.
4444
Connection((expr, expr)[]),
4545

46+
/// A bus interaction with only stage 0 columns. Stage 1 columns are to be created in
47+
/// backends that support LogUp natively, i.e. Stwo.
48+
/// Contains:
49+
/// - An expression for the multiplicity. Negative for bus receives.
50+
/// - An expression for the bus ID. Each bus receive should have a static
51+
/// bus ID (i.e., just a number) that uniquely identifies the receive.
52+
/// - The tuple added to the bus.
53+
/// - An expression for the latch. This should be exactly what the RHS selector
54+
/// would be in an equivalent lookup or permutation:
55+
/// - It should always evaluate to a binary value.
56+
/// - If it evaluates to zero, the multiplicity must be zero.
57+
BusInteraction(expr, expr, expr[], expr),
58+
4659
/// A "phantom" bus interaction, i.e., an annotation for witness generation.
4760
/// The actual constraint should be enforced via other constraints.
4861
/// Contains:

0 commit comments

Comments
 (0)