Chiplets bus constraints

constraints/ace.air

@@ -75,7 +75,11 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) {
 
     let flag_ace_next = flag_ace_current_and_next(s3');
     let flag_ace_last = flag_ace_last(s3');
-
+
+    ####################################################################################
+    # TRANSITION CONSTRAINTS
+    ####################################################################################
+
     # Section and block flags constraints
     enf section_block_flags_constraints([s3, sstart, sstart', sblock, id0, n_eval]);
 
@@ -91,10 +95,33 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) {
     # Finalization constraints
     let f_end = binary_or(binary_and(flag_ace_next, sstart'), flag_ace_last);
     enf finalization_constraints([id0, v0_0, v0_1]) when f_end;
+
+    ####################################################################################
+    # BUS RESPONSE - ACE INITIALIZATION
+    ####################################################################################
+    # The ACE chiplet provides a response to the decoder's ACE_INIT request via the
+    # chiplets bus. The response is sent when a new section starts (sstart = 1).
+    #
+    # Message format: (ACE_INIT, ctx, ptr, clk, nread, neval)
+    # where:
+    # - ctx, clk: Memory access context and clock cycle
+    # - ptr: Word-aligned pointer to first input variable
+    # - nread: Total count of input and constant elements (computed as id0 + 1 - neval)
+    # - neval: Total number of arithmetic operations
+    #
+    # Note: Since id0 = nread + neval - 1 in the first row, we have nread = id0 - neval + 1
+    ####################################################################################
+
+    # Compute nread from id0 and n_eval
+    # Since id0 = nread + neval - 1 in first row, then: nread = id0 - neval + 1
+    let nread = id0 + 1 - n_eval;
+
+    # Remove ACE INIT response when a section starts
+    bus_6_chiplets_bus.remove(ACEINIT, ctx, ptr, clk, nread, n_eval) when sstart;
 }
 
 # Enforces that on the first row of ACE chiplet we should have sstart' = 1
-ev ace_chiplet_constraints_first_row([ace[16]]) {
+ev ace_chiplet_constraints_first_row([s3, ace[16]]) {
     let sstart = ace[0];    # Section start flag
 
     enf sstart' = 1;
@@ -145,10 +172,7 @@ ev section_block_flags_constraints([s3, sstart, sstart_next, sblock, id0, n_eval
     # Sections must end with EVAL blocks (not READ)
     enf f_read = 0 when f_end;
 
-    # In a READ block, n_eval stays constant.
-    # When transitioning to an EVAL block, the next id0 must equal n_eval - 1.
-    # This ensures proper sequencing: READ loads nodes with IDs, EVAL starts processing
-    # from the highest loaded node ID (n_eval - 1).
+    # READ→EVAL transition occurs when n_eval matches id0+1
     enf select(f_read_next, n_eval', id0' + 1) = n_eval when f_read;
 }
 
@@ -167,9 +191,6 @@ ev enforce_binary_columns([sstart, sblock]) {
 # - Context (ctx) and clock (clk) remain constant within a section
 # - Memory pointer (ptr) increments with fixed increments: +4 in READ, +1 in EVAL
 # - Node identifiers (id0) decrement with fixed decrements: -2 in READ, -1 in EVAL
-#
-# Note: These constraints are active when the next row is NOT the start of a new section,
-# i.e., all but the last rows of the section (intra-section transitions only).
 ev section_constraints([sstart, sblock, ctx, ptr, clk, id0]) {
     let flag_within_section = binary_not(sstart');
     let flag_read = !sblock;
@@ -181,10 +202,10 @@ ev section_constraints([sstart, sblock, ctx, ptr, clk, id0]) {
     # Clock consistency within a section
     enf clk' = clk when flag_within_section;
 
-    # Memory pointer increases by 4 in READ blocks and by 1 in EVAL blocks
+    # Memory pointer must decrease by 4 in READ blocks and by 1 in EVAL blocks
     enf ptr' = ptr + 4 * flag_read + flag_eval when flag_within_section;
 
-    # Node identifiers decrease by 2 in READ blocks and by 1 in EVAL blocks
+    # Node identifiers decreases by 2 in READ blocks and by 1 in EVAL blocks
     enf id0 = id0' + 2 * flag_read + flag_eval when flag_within_section;
 }
 
@@ -310,4 +331,4 @@ fn block_flags(s_block: felt) -> felt[2] {
     let f_eval = s_block;
 
     return [f_read, f_eval];
-}
+}

constraints/bitwise.air

@@ -8,7 +8,7 @@
 #
 # Each bitwise operation spans exactly 8 rows, with limbs processed in little-endian order.
 #
-# STATUS: Partially implemented (missing bus constraints)
+# STATUS: Fully implemented (core constraints + bus responses complete)
 #
 # REFERENCES:
 # - Bitwise Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/bitwise.html
@@ -41,9 +41,38 @@ periodic_columns {
 #
 # Max constraint degree: 4
 ev bitwise_chiplet_constraints([op_flag, a, b, a_limb[4], b_limb[4], zp, z]) {
+    ####################################################################################
+    # TRANSITION CONSTRAINTS
+    ####################################################################################
+
     enf bitwise_op_flag([op_flag]);
     enf input_decomposition([a, b, a_limb, b_limb]);
     enf output_aggregation([op_flag, a, b, a_limb, b_limb, zp, z]);
+
+    ####################################################################################
+    # BUS OPERATIONS - CHIPLETS COMMUNICATION
+    ####################################################################################
+    # The bitwise chiplet provides responses to bitwise operation requests via the
+    # chiplets bus. Each operation spans 8 rows, and the response is removed on the
+    # LAST row of the cycle (when k_transition = 0).
+    #
+    # OPERATIONS:
+    # - BITWISEAND (label = 2): AND operation (op_flag = 0)
+    # - BITWISEXOR (label = 6): XOR operation (op_flag = 1)
+    #
+    # Response format: (operation_label, a, b, z)
+    # where a, b are 32-bit operands and z is the result.
+    ####################################################################################
+
+    # Compute operation flags
+    let is_and = binary_not(op_flag);
+    let is_xor = op_flag;
+
+    # Remove bus responses on the last row of the 8-row cycle
+    let is_last_row = binary_not(k_transition);
+
+    bus_6_chiplets_bus.remove(BITWISEAND, a, b, z) when (is_and * is_last_row);
+    bus_6_chiplets_bus.remove(BITWISEXOR, a, b, z) when (is_xor * is_last_row);
 }
 
 ##########################################################################################

constraints/chiplets.air

@@ -44,7 +44,7 @@ use utils::*;
 # CHIPLETS CONSTRAINTS
 ##########################################################################################
 
-ev chiplets_constraints([chiplets[20]]) {
+ev chiplets_constraints([chiplets[20], system_clk]) {
     # Chiplets' flag constraints
     let s0 = chiplets[0];
     let s1 = chiplets[1];
@@ -68,7 +68,7 @@ ev chiplets_constraints([chiplets[20]]) {
 
     # Apply chiplet-specific constraints based on hierarchical selector state.
     enf match {
-        case hash_active: hash_chiplet([chiplets[1..17]]),
+        case hash_active: hash_chiplet([chiplets[0..16], system_clk]),
         case bitwise_active: bitwise_chiplet_constraints([chiplets[2..15]]),
         case memory_active: memory_chiplet_constraints_all_rows([chiplets[3..18]]),
         case ace_active: ace_chiplet_constraints_all_rows([chiplets[3..20]]),
@@ -96,7 +96,7 @@ ev chiplets_constraints([chiplets[20]]) {
 
     ### Apply ACE chiplet initialization constraints at the transition point
     let next_row_first_ace = binary_and(memory_active, s2');   # Transitioning into ACE chiplet
-    enf ace_chiplet_constraints_first_row([chiplets[4..20]]) when next_row_first_ace;
+    enf ace_chiplet_constraints_first_row([chiplets[3..20]]) when next_row_first_ace;
 
     ## KERNEL ROM
 

constraints/decoder.air

@@ -40,9 +40,11 @@ use utils::*;
 ##########################################################################################
 
 # Main decoder constraint evaluator
-# Note: Decoder needs access to stack top (s0) for general constraints
-ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp, gc, ox, c0, c1, c2, e0, e1, s0]) {
-    # DECODING
+# Note: Decoder needs access to stack top (s0-s2) for operation constraints and general constraints, and system clk/ctx for bus operations
+ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp, gc, ox, c0, c1, c2, e0, e1, s0, s1, s2, system_clk, system_ctx]) {
+    ####################################################################################
+    # TRANSITION CONSTRAINTS
+    ####################################################################################
 
     # GENERAL DECODER CONSTRAINTS
     enf general_constraints([b0, b1, b2, b3, b4, b5, b6, e0, e1, h0, h1, h2, h3, h4, h5, h6, h7, addr, sp, s0]);
@@ -53,19 +55,63 @@ ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp
     # OPERATION BATCH FLAGS CONSTRAINTS
     enf op_batch_flags_constraints([b0, b1, b2, b3, b4, b5, b6, e0, e1, h0, h1, h2, h3, h4, h5, h6, h7, c0, c1, c2]);
 
-    # OP FLAGS BITS
-
-    # U32 OPERATIONS BIT CONSTRAINTS
-    # Force b0 = 0 for all u32 operations (100_xxx0 pattern)
+    # OP FLAGS BITS CONSTRAINTS
     enf u32_bit_constraints([b0, b1, b2, b3, b4, b5, b6]);
-
-    # HIGH-DEGREE OPERATIONS BIT CONSTRAINTS
-    # Define degree reduction: e0 = b6 * (1-b5) * b4 for 101-prefix group
     enf high_degree_bit_constraints([b0, b1, b2, b3, b4, b5, b6, e0]);
-
-    # VERY HIGH-DEGREE OPERATIONS BIT CONSTRAINTS
-    # Define degree reduction and force last 2 bits to be 0 for 11-prefix groups
     enf very_high_degree_bit_constraints([b0, b1, b2, b3, b4, b5, b6, e1]);
+
+    ####################################################################################
+    # BUS OPERATIONS - CHIPLETS COMMUNICATION
+    ####################################################################################
+
+    # Compute operation flags once for all bus operations
+    let fdyn = flag_dyn([b0, b1, b2, b3, b4, b5, b6], e0);
+    let fdyncall = flag_dyncall([b0, b1, b2, b3, b4, b5, b6], e0);
+    let fsyscall = flag_syscall([b0, b1, b2, b3, b4, b5, b6], e1);
+    let fevalcircuit = flag_evalcircuit([b0, b1, b2, b3, b4, b5, b6], e0);
+    let fspan = flag_span([b0, b1, b2, b3, b4, b5, b6], e0);
+    let frespan = flag_respan([b0, b1, b2, b3, b4, b5, b6], e1);
+    let fend = flag_end([b0, b1, b2, b3, b4, b5, b6], e1);
+    let fjoin = flag_join([b0, b1, b2, b3, b4, b5, b6], e0);
+    let fsplit = flag_split([b0, b1, b2, b3, b4, b5, b6], e0);
+    let floop = flag_loop([b0, b1, b2, b3, b4, b5, b6], e0);
+    let fcall = flag_call([b0, b1, b2, b3, b4, b5, b6], e1);
+
+    # Opcode value for domain separation: d = Σ(bi·2^i)
+    let opcode = b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6;
+
+    # Memory operations: DYN/DYNCALL read target hash from memory
+    # The callee hash is read into h0'-h3' for bookkeeping, but the hash computation
+    # itself operates on [ZERO; 8] to compute the block hash
+    bus_6_chiplets_bus.insert(MEMREADWORD, system_ctx, s0, system_clk, h0', h1', h2', h3') when (fdyn + fdyncall);
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', 0, 0, 0, 0, 0, 0, 0, 0) when (fdyn + fdyncall);
+
+    # Kernel ROM: SYSCALL validates kernel procedure and computes block hash
+    # SYSCALL hashes: hash_control_block(kernel_proc_hash, EMPTY_WORD, domain, digest)
+    # The kernel procedure hash is in h0-h3, second child is zeros (no second child)
+    bus_6_chiplets_bus.insert(KERNELPROCCALL, h0, h1, h2, h3) when fsyscall;
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when fsyscall;
+
+    # ACE chiplet: EVALCIRCUIT initializes arithmetic circuit evaluation
+    # Stack layout for EVALCIRCUIT: [ptr, nread, neval, ...]
+    # Message format: (ACE_INIT, ctx, ptr, clk, nread, neval)
+    let ace_ptr = s0;     # Memory pointer to first input variable (word-aligned)
+    let ace_nread = s1;   # Number of input and constant elements
+    let ace_neval = s2;   # Number of arithmetic operations
+    bus_6_chiplets_bus.insert(ACEINIT, system_ctx, ace_ptr, system_clk, ace_nread, ace_neval) when fevalcircuit;
+
+    # Basic block hashing: SPAN/RESPAN/END operations
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7) when fspan;
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7) when frespan;
+    bus_6_chiplets_bus.insert(HASHERRETURNHASH, addr + 7, h0', h1', h2', h3') when fend;
+
+    # Control flow with opcode domain separation: JOIN/SPLIT/LOOP/CALL
+    # JOIN/SPLIT hash two children: hash_control_block(child1, child2, domain, digest)
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7, opcode) when fjoin;
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7, opcode) when fsplit;
+    # LOOP/CALL hash one child + zeros: hash_control_block(child, EMPTY_WORD, domain, digest)
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when floop;
+    bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when fcall;
 }
 
 ##########################################################################################