ACE wire bus constraints

constraints/ace.air

@@ -33,12 +33,12 @@
 # │ v1_0        │ First operand value (extension field element, coefficient 0)               │
 # │ v1_1        │ First operand value (extension field element, coefficient 1)               │
 # │ id2 / n_eval│ Dual use: 2nd operand node ID (EVAL) / #evaluations in section (READ)      │
-# │ v2_0        │ Second operand value (extension field element, coefficient 0)              │
-# │ v2_1        │ Second operand value (extension field element, coefficient 1)              │
-# │ m0          │ Wire bus multiplicity (for node tracking, not yet implemented)             │
+# │ v2_0        │ Second operand value, coefficient 0 (EVAL only)                            │
+# │ v2_1 / m1   │ Dual use: 2nd operand value (EVAL) / node 1 multiplicity (READ)            │
+# │ m0          │ Wire bus multiplicity for node 0 (both READ and EVAL)                      │
 # └─────────────┴────────────────────────────────────────────────────────────────────────────┘
 #
-# STATUS: Core constraints implemented, wire bus constraints not implemented
+# STATUS: Fully implemented
 #
 # REFERENCES:
 # - ACE Design: https://0xmiden.github.io/miden-vm/design/chiplets/ace.html
@@ -67,11 +67,12 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) {
     let id1 = ace[9];       # Second node identifier
     let v1_0 = ace[10];     # Second node value (element 0)
     let v1_1 = ace[11];     # Second node value (element 1)
-    let id2 = ace[12];      # Third node identifier (result node in EVAL)
-    let n_eval = ace[12];   # Total number of arithmetic operations
-    let v2_0 = ace[13];     # Third node value (element 0)
-    let v2_1 = ace[14];     # Third node value (element 1)
-    let m0 = ace[15];       # Multiplicity for wire bus operations
+    let id2 = ace[12];      # Third node identifier (EVAL only)
+    let n_eval = ace[12];   # Total number of arithmetic operations (READ only, same column as id2)
+    let v2_0 = ace[13];     # Third node value (element 0, EVAL only)
+    let v2_1 = ace[14];     # Third node value (element 1, EVAL only)
+    let m1 = ace[14];       # Multiplicity for node 1 wire bus (READ only, same column as v2_1)
+    let m0 = ace[15];       # Multiplicity for node 0 wire bus (both READ and EVAL)
 
     let flag_ace_next = flag_ace_current_and_next(s3');
     let flag_ace_last = flag_ace_last(s3');
@@ -136,6 +137,39 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) {
 
     let instruction = id1 + id2 * ACEINSTRUCTIONIDONEOFFSET + (op + 1) * ACEINSTRUCTIONIDTWOOFFSET;
     bus_5_v_table.remove(MEMREADELEMENT, ctx, ptr, clk, instruction) when is_eval_block;
+
+    ####################################################################################
+    # WIRE BUS
+    ####################################################################################
+    # The wire bus (bus_7_wiring_bus) ensures that every node ID used as an operand
+    # in EVAL blocks was previously defined in READ blocks or earlier EVAL blocks.
+    #
+    # The LogUp protocol tracks node definitions and consumptions:
+    # - READ blocks: Define 2 nodes (id0, id1) with multiplicities (m0, m1)
+    # - EVAL blocks: Consume 2 nodes (id1, id2), define 1 node (id0) with multiplicity m0
+    #
+    # Each node is tracked with: (ctx, clk, id, v0, v1)
+    ####################################################################################
+
+    # READ block: Insert two nodes being loaded from memory
+    # Node 0: (id0, v0) with fan-out multiplicity m0
+    # Node 1: (id1, v1) with fan-out multiplicity m1
+    # Use conditional multiplicity: m * is_read_block (multiplicity if READ, 0 if EVAL)
+    let m0_read = m0 * is_read_block;
+    let m1_read = m1 * is_read_block;
+    bus_7_wiring_bus.insert(ctx, clk, id0, v0_0, v0_1) with m0_read;
+    bus_7_wiring_bus.insert(ctx, clk, id1, v1_0, v1_1) with m1_read;
+
+    # EVAL block: Consume two input nodes, insert one result node
+    # Consume input node 1: (id1, v1)
+    # Consume input node 2: (id2, v2)
+    # Insert result node 0: (id0, v0) with fan-out multiplicity m0
+    # Use conditional multiplicity: 1 * is_eval_block (consume if EVAL, 0 if READ)
+    let consume = is_eval_block;
+    let m0_eval = m0 * is_eval_block;
+    bus_7_wiring_bus.remove(ctx, clk, id1, v1_0, v1_1) with consume;
+    bus_7_wiring_bus.remove(ctx, clk, id2, v2_0, v2_1) with consume;
+    bus_7_wiring_bus.insert(ctx, clk, id0, v0_0, v0_1) with m0_eval;
 }
 
 # Enforces that on the first row of ACE chiplet we should have sstart' = 1

constraints/miden_vm.air

@@ -150,7 +150,7 @@ boundary_constraints {
     enf bus_3_stack_p1.first = unconstrained;
     enf bus_3_stack_p1.last = unconstrained;
 
-    # Range checker bus - LogUp protocol requires null initialization/finalization
+    # Range checker bus
     enf bus_4_range_checker.first = null;
     enf bus_4_range_checker.last = null;
 
@@ -163,9 +163,10 @@ boundary_constraints {
     enf bus_6_chiplets_bus.first = kernel_digests;
     enf bus_6_chiplets_bus.last = unconstrained;
 
-    # ACE (Algebraic Circuit Elements) wiring bus
-    enf bus_7_wiring_bus.first = unconstrained;
-    enf bus_7_wiring_bus.last = unconstrained;
+    # ACE wiring bus
+    # Ensures all nodes inserted are consumed exactly as many times as their multiplicity
+    enf bus_7_wiring_bus.first = null;
+    enf bus_7_wiring_bus.last = null;
 }
 
 ##########################################################################################