Make latch semantic clearer (#2358)

Depends on #2360

Changes the semantics of the `PhantomBusInteraction.latch` field
slightly, to make my life easier with #2351. Basically, we want it to be
exactly what the RHS selector would have been in a lookup / permutation:
A fixed column latch for a lookup, and equal to the multiplicity for the
permutation. This way, witgen can treat it just like it treats selectors
now.

Eventually, I think we should remove the latch again. The permutation
latch is equal to the multiplicity anyway, and the lookup latch should
be detectable by looking for a constraint like `(1 - latch) *
multiplicity = 0;`.

Author: georgwiese

linker/src/lib.rs

@@ -330,26 +330,26 @@ fn receive(
     latch: Expression,
     interaction_id: u32,
 ) -> Expression {
-    let (function, identity) = match identity_type {
+    let (function, arguments) = match identity_type {
         InteractionType::Lookup => (
             SymbolPath::from_str("std::protocols::lookup_via_bus::lookup_receive")
                 .unwrap()
                 .into(),
-            lookup(lhs, rhs),
+            vec![interaction_id.into(), lookup(lhs, rhs), latch],
         ),
         InteractionType::Permutation => (
             SymbolPath::from_str("std::protocols::permutation_via_bus::permutation_receive")
                 .unwrap()
                 .into(),
-            permutation(lhs, rhs),
+            vec![interaction_id.into(), permutation(lhs, rhs)],
         ),
     };
 
     Expression::FunctionCall(
         SourceRef::unknown(),
         FunctionCall {
             function: Box::new(Expression::Reference(SourceRef::unknown(), function)),
-            arguments: vec![interaction_id.into(), identity, latch],
+            arguments,
         },
     )
 }

std/prelude.asm

@@ -46,9 +46,12 @@ enum Constr {
     /// 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.
+    /// - An expression for the multiplicity. Negative for bus receives.
     /// - The tuple added to the bus.
-    /// - An expression for the latch, a binary expression which indicates where the multiplicity can be non-zero.
+    /// - An expression for the latch. This should be exactly what the RHS selector
+    ///   would be in an equivalent lookup or permutation:
+    ///   - It should always evaluate to a binary value.
+    ///   - If it evaluates to zero, the multiplicity must be zero.
     /// 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[], expr)

std/protocols/bus.asm

@@ -125,10 +125,11 @@ let compute_next_z: expr, expr, expr[], expr, Ext<expr>, Ext<expr>, Ext<expr> ->
 
 /// Convenience function for bus interaction to send columns
 let bus_send: expr, expr[], expr -> () = constr |id, tuple, multiplicity| {
-    bus_interaction(id, tuple, multiplicity, 1);
+    // For bus sends, the multiplicity always equals the latch
+    bus_interaction(id, tuple, multiplicity, multiplicity);
 };
 
 /// Convenience function for bus interaction to receive columns
 let bus_receive: expr, expr[], expr, expr -> () = constr |id, tuple, multiplicity, latch| {
-    bus_interaction(id, tuple, -1 * multiplicity, latch);
+    bus_interaction(id, tuple, -multiplicity, latch);
 };

std/protocols/permutation_via_bus.asm

@@ -15,10 +15,10 @@ let permutation_send: expr, Constr -> () = constr |id, permutation_constraint| {
 /// Given an ID and permutation constraints, receives the (ID, permutation_constraint.rhs...) tuple from the bus
 /// with a prover-provided multiplicity if permutation_constraint.rhs_selector is 1.
 /// Also adds an annotation for witness generation.
-let permutation_receive: expr, Constr, expr -> () = constr |id, permutation_constraint, latch| {
+let permutation_receive: expr, Constr -> () = constr |id, permutation_constraint| {
     let (lhs_selector, lhs, rhs_selector, rhs) = unpack_permutation_constraint(permutation_constraint);
     
-    bus_receive(id, rhs, rhs_selector, latch);
+    bus_receive(id, rhs, rhs_selector, rhs_selector);
     
     // Add an annotation for witness generation
     to_phantom_permutation(permutation_constraint);

test_data/std/bus_permutation.asm

@@ -18,5 +18,5 @@ machine Main with degree: 8 {
     let ID = 123;
     let permutation_constraint = sel $ [x, y] is sub_sel $ [sub_x, sub_y];
     permutation_send(ID, permutation_constraint);
-    permutation_receive(ID, permutation_constraint, 1);
+    permutation_receive(ID, permutation_constraint);
 }