Fix: Constrain table multiplicities

executor/programs/asm/poc_divu_commit.s

@@ -0,0 +1,22 @@
+	.text
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Compute 7 / 2 with a real DIVU, spill the quotient to the stack and
+	# commit it. The committed public output is the DVRM chip's quotient,
+	# so a proof reporting anything but 3 certifies a false division.
+	addi	a3, zero, 7
+	addi	a4, zero, 2
+	divu	t1, a3, a4		# t1 = 7 / 2
+	addi	sp, sp, -16
+	sd	t1, 0(sp)		# spill to stack
+	li	a0, 1			# fd = 1
+	mv	a1, sp			# buf = sp
+	li	a2, 8			# count = 8
+	li	a7, 64			# syscall = Commit
+	ecall
+
+	addi	sp, sp, 16
+	li	a0, 0
+	li	a7, 93			# syscall = Halt
+	ecall

executor/programs/asm/poc_lb_commit.s

@@ -0,0 +1,23 @@
+	.text
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	# Store the byte 0x05 (sign bit clear), read it back with a real
+	# sign-extending LB, spill the result and commit it. The committed public
+	# output is the LOAD chip's res, so a proof reporting anything but 5
+	# certifies a false sign extension.
+	addi	sp, sp, -16
+	addi	t0, zero, 5
+	sb	t0, 8(sp)
+	lb	t1, 8(sp)		# t1 = sext(0x05) = 5
+	sd	t1, 0(sp)		# spill to stack
+	li	a0, 1			# fd = 1
+	mv	a1, sp			# buf = sp
+	li	a2, 8			# count = 8
+	li	a7, 64			# syscall = Commit
+	ecall
+
+	addi	sp, sp, 16
+	li	a0, 0
+	li	a7, 93			# syscall = Halt
+	ecall

executor/programs/asm/poc_mul_commit.s

@@ -0,0 +1,22 @@
+	.text
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	# Compute 3 * 5 with a real MUL, spill the product to the stack and
+	# commit it. The committed public output is the MUL chip's lo result,
+	# so a proof reporting anything but 15 certifies a false product.
+	addi	a3, zero, 3
+	addi	a4, zero, 5
+	mul	t1, a3, a4		# t1 = 3 * 5
+	addi	sp, sp, -16
+	sd	t1, 0(sp)		# spill to stack
+	li	a0, 1			# fd = 1
+	mv	a1, sp			# buf = sp
+	li	a2, 8			# count = 8
+	li	a7, 64			# syscall = Commit
+	ecall
+
+	addi	sp, sp, 16
+	li	a0, 0
+	li	a7, 93			# syscall = Halt
+	ecall

executor/programs/asm/poc_sll_commit.s

@@ -0,0 +1,22 @@
+	.text
+	.attribute	5, "rv64i2p1"
+	.globl	main
+main:
+	# Compute 1 << 1 with a real SLL, spill the result to the stack and
+	# commit it. The committed public output is the SHIFT chip's result,
+	# so a proof reporting anything but 2 certifies a false shift.
+	addi	a3, zero, 1
+	addi	a4, zero, 1
+	sll	t1, a3, a4		# t1 = 1 << 1
+	addi	sp, sp, -16
+	sd	t1, 0(sp)		# spill to stack
+	li	a0, 1			# fd = 1
+	mv	a1, sp			# buf = sp
+	li	a2, 8			# count = 8
+	li	a7, 64			# syscall = Commit
+	ecall
+
+	addi	sp, sp, 16
+	li	a0, 0
+	li	a7, 93			# syscall = Halt
+	ecall

executor/programs/asm/poc_slt_commit.s

@@ -0,0 +1,23 @@
+	.text
+	.attribute	5, "rv64i2p1"
+	.globl	main
+main:
+	# Compare 5 < 3 with a real SLT, spill the result to the stack and commit
+	# it. The committed public output is the LT chip's result, so a proof
+	# reporting anything but 0 certifies a false comparison. The spill comes
+	# right after the SLT so it is the first instruction to read the result.
+	addi	sp, sp, -16
+	addi	a3, zero, 5
+	addi	a4, zero, 3
+	slt	t1, a3, a4		# t1 = (5 < 3) = 0
+	sd	t1, 0(sp)		# spill to stack
+	li	a0, 1			# fd = 1
+	mv	a1, sp			# buf = sp
+	li	a2, 8			# count = 8
+	li	a7, 64			# syscall = Commit
+	ecall
+
+	addi	sp, sp, 16
+	li	a0, 0
+	li	a7, 93			# syscall = Halt
+	ecall

prover/src/tables/branch.rs

@@ -150,20 +150,50 @@ impl BranchOperation {
     }
 }
 
-/// Generates the BRANCH trace table from a list of operations.
+/// Largest per-row multiplicity: `μ` is range-checked to a byte
+/// (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many lookups. The
+/// bound keeps μ non-negative: without it a `μ = −1` twin of an honest row
+/// cancels it on the BRANCH bus while *receiving* its range lookups, absorbing
+/// another row's out-of-range limb (same bug as LT).
 ///
-/// Duplicate operations (same pc, offset, register, jalr) are merged into a single row
-/// with their multiplicities summed. The table is then padded to the next power of 2.
-pub fn generate_branch_trace(
-    operations: &[BranchOperation],
-) -> TraceTable<GoldilocksField, GoldilocksExtension> {
-    // Deduplicate operations: (pc, offset, register, jalr) -> multiplicity
+/// The bound rides the ARE_BYTES bus, which the limb range checks
+/// (IS_HALFWORD) never use. That is what closes it: an IS_HALFWORD-bus
+/// bound could be cancelled by a non-canonical limb `(p−1, b+1)` (same
+/// packed value, passes every constraint) sending `IS_HALFWORD[p−1]`;
+/// on ARE_BYTES no limb can reach the `p−1` tuple, so a `μ = −1` row's
+/// bound send has no receiver and the whole proof is rejected.
+pub const MU_MAX: u64 = (1 << 8) - 1;
+
+/// Deduplicates BRANCH operations into trace rows: `(pc, offset, register,
+/// jalr) -> μ`, splitting an op over several rows when its count exceeds
+/// [`MU_MAX`]. Shared by trace generation and the BITWISE collector so the
+/// per-row lookups they count cannot drift apart.
+pub fn dedup_branch_rows(operations: &[BranchOperation]) -> Vec<(BranchOperation, u64)> {
     let mut op_map: HashMap<BranchOperation, u64> = HashMap::new();
     for op in operations {
         *op_map.entry(op.clone()).or_insert(0) += 1;
     }
 
-    let unique_ops: Vec<_> = op_map.into_iter().collect();
+    let mut rows = Vec::with_capacity(op_map.len());
+    for (op, mut left) in op_map {
+        while left > 0 {
+            let mu = left.min(MU_MAX);
+            left -= mu;
+            rows.push((op.clone(), mu));
+        }
+    }
+    rows
+}
+
+/// Generates the BRANCH trace table from a list of operations.
+///
+/// Duplicate operations (same pc, offset, register, jalr) are merged into a
+/// single row with their multiplicities summed (see [`dedup_branch_rows`]). The
+/// table is then padded to the next power of 2.
+pub fn generate_branch_trace(
+    operations: &[BranchOperation],
+) -> TraceTable<GoldilocksField, GoldilocksExtension> {
+    let unique_ops = dedup_branch_rows(operations);
     let num_rows = unique_ops.len().next_power_of_two().max(4);
     let mut trace = TraceTable::new_main(
         crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS),
@@ -222,7 +252,8 @@ pub fn generate_branch_trace(
 /// - **Sends** ARE_BYTES lookup for next_pc_low[1] range check (Y=0)
 /// - **Sends** BYTE_ALU[AND] lookup for LSB masking
 ///   (next_pc_low[0] = unmasked_low_byte & 254)
-/// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks
+/// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks and for
+///   (next_pc_high limbs); ARE_BYTES for the μ multiplicity bound
 /// - **Receives** BRANCH lookups from CPU table
 pub fn bus_interactions() -> Vec<BusInteraction> {
     vec![
@@ -283,6 +314,24 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
                 packing: Packing::Direct,
             }],
         ),
+        // ARE_BYTES[μ, 0] | μ. Every lookup here fires with μ, so μ itself must be
+        // bounded and non-negative. Otherwise a μ = −1 twin of an honest row
+        // cancels it on the BRANCH bus while *receiving* its range lookups and
+        // absorbs an out-of-range IS_HALFWORD sent by any row (same as LT). Sent
+        // with itself as multiplicity: `k` rows holding an out-of-range `v` put
+        // weight `k·v ≠ 0` on a byte tuple ARE_BYTES has no row for, while padding
+        // (μ = 0) contributes nothing. See `MU_MAX`.
+        BusInteraction::sender(
+            BusId::AreBytes,
+            Multiplicity::Column(cols::MU),
+            vec![
+                BusValue::Packed {
+                    start_column: cols::MU,
+                    packing: Packing::Direct,
+                },
+                BusValue::constant(0),
+            ],
+        ),
         // BRANCH[next_pc; pc, offset, register, JALR] (receiver)
         // Signature: [next_pc (DWordWL), pc (DWordWL), offset (DWordWL), register (DWordWL), JALR (Bit)]
         BusInteraction::receiver(

prover/src/tables/bytewise.rs

@@ -92,19 +92,40 @@ impl BytewiseOperation {
 
 /// Generates the BYTEWISE trace from a list of operations.
 ///
-/// Duplicate operations are merged with summed multiplicities, then padded to
-/// the next power of two (minimum 4).
-pub fn generate_bytewise_trace(
-    operations: &[BytewiseOperation],
-) -> TraceTable<GoldilocksField, GoldilocksExtension> {
+/// Largest per-row multiplicity: `μ` is range-checked to a byte on the ARE_BYTES
+/// bus (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many lookups.
+/// The bound keeps μ non-negative: without it a `μ = −1` row inverts its byte
+/// range checks and can hold an out-of-range byte (carrier). See [`dedup_bytewise_rows`].
+pub const MU_MAX: u64 = (1 << 8) - 1;
+
+/// Deduplicates BYTEWISE operations into trace rows: `op -> μ`, splitting an op
+/// over several rows when its count exceeds [`MU_MAX`]. Shared by trace
+/// generation and the BITWISE collector so the per-row lookups cannot drift.
+pub fn dedup_bytewise_rows(operations: &[BytewiseOperation]) -> Vec<(BytewiseOperation, u64)> {
     use std::collections::HashMap;
 
     let mut op_map: HashMap<BytewiseOperation, u64> = HashMap::new();
     for op in operations {
         *op_map.entry(op.clone()).or_insert(0) += 1;
     }
 
-    let unique_ops: Vec<_> = op_map.into_iter().collect();
+    let mut rows = Vec::with_capacity(op_map.len());
+    for (op, mut left) in op_map {
+        while left > 0 {
+            let mu = left.min(MU_MAX);
+            left -= mu;
+            rows.push((op.clone(), mu));
+        }
+    }
+    rows
+}
+
+/// Duplicate operations are merged with summed multiplicities (split at
+/// [`MU_MAX`]), then padded to the next power of two (minimum 4).
+pub fn generate_bytewise_trace(
+    operations: &[BytewiseOperation],
+) -> TraceTable<GoldilocksField, GoldilocksExtension> {
+    let unique_ops = dedup_bytewise_rows(operations);
     let num_rows = unique_ops.len().next_power_of_two().max(4);
     let mut trace = TraceTable::new_main(
         crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS),
@@ -132,6 +153,7 @@ pub fn generate_bytewise_trace(
 
 /// All bus interactions for the BYTEWISE table:
 /// - **Sends** `BYTE_ALU[op, a[i], b[i]] -> res[i]` for each of the 8 bytes.
+/// - **Sends** `ARE_BYTES[μ, 0]` to bound the multiplicity.
 /// - **Receives** `ALU[a, b, op] -> res` (operands packed DWordBL -> 2 words).
 pub fn bus_interactions() -> Vec<BusInteraction> {
     let mut interactions = Vec::with_capacity(9);
@@ -161,6 +183,22 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ));
     }
 
+    // ARE_BYTES[μ, 0] | μ. Bounds μ to a byte and keeps it non-negative: the eight
+    // BYTE_ALU sends above are weighted by μ, so a free μ = −1 would invert them
+    // and let the row hold an out-of-range byte. The bound rides ARE_BYTES with
+    // value = weight = μ, so a μ = −1 row lands at `(p−1, 0)` with no receiver.
+    interactions.push(BusInteraction::sender(
+        BusId::AreBytes,
+        Multiplicity::Column(cols::MU),
+        vec![
+            BusValue::Packed {
+                start_column: cols::MU,
+                packing: Packing::Direct,
+            },
+            BusValue::constant(0),
+        ],
+    ));
+
     // ALU[a, b, op] -> res (receiver). a/b/res are DWordBL (8 bytes) packed
     // into 2 words each, matching the CPU's DWordWL operands.
     interactions.push(BusInteraction::receiver(