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

@@ -21,7 +21,7 @@
 //! - `carry[0]`, `carry[1]`: Carries from 64-bit addition
 //!
 //! ## Bus Interactions
-//! - Sender: ARE_BYTES (×1 for `[next_pc_low[1], 0]`, spec template `IS_BYTE<next_pc_low[1]>`)
+//! - Sender: ARE_BYTES (×1 for `[μ, next_pc_low[1]]`, spec `IS_BYTE<μ>` and `IS_BYTE<next_pc_low[1]>` batched)
 //! - Sender: BYTE_ALU[AND] (×1 for masking LSB)
 //! - Sender: IS_HALFWORD (×3 for next_pc_high[0..3])
 //! - Receiver: BRANCH (provides branch targets to CPU)
@@ -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 by `IS_BYTE[μ]`,
+/// batched with `IS_BYTE[next_pc_low_1]` into one `ARE_BYTES[μ, next_pc_low_1]`
+/// with multiplicity 1 (the spec's default `cond`), 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
+/// `next_pc_low_1` is only constrained packed (`low0 + 2^8·low1 + 2^16·high0`),
+/// so its byte check must not be weighted by μ either: with weight μ a row with
+/// μ < 0 and `low1 = p−1` cancels its own (or another table's) bound on
+/// `(p−1, 0)` (`branch_carrier_poc::lt_forgery_with_branch_cycle_is_rejected`).
+/// See `lt::MU_MAX`.
+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),
@@ -219,23 +249,33 @@ pub fn generate_branch_trace(
 /// Creates all bus interactions for the BRANCH table.
 ///
 /// The BRANCH table:
-/// - **Sends** ARE_BYTES lookup for next_pc_low[1] range check (Y=0)
+/// - **Sends** ARE_BYTES[μ, next_pc_low[1]]: the μ bound and the next_pc_low[1]
+///   range check, batched (both have multiplicity 1)
 /// - **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 the next_pc_high[0..2] range checks
 /// - **Receives** BRANCH lookups from CPU table
 pub fn bus_interactions() -> Vec<BusInteraction> {
     vec![
-        // ARE_BYTES[next_pc_low[1], 0] - range check bits 8-15
+        // IS_BYTE[μ], IS_BYTE[next_pc_low[1]] = ARE_BYTES[μ, next_pc_low[1]] | 1.
+        // 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). Both checks
+        // have the spec's default `cond` (1), so they batch into one
+        // interaction; padding rows send ARE_BYTES[0, 0]. See `MU_MAX`.
         BusInteraction::sender(
             BusId::AreBytes,
-            Multiplicity::Column(cols::MU),
+            Multiplicity::One,
             vec![
+                BusValue::Packed {
+                    start_column: cols::MU,
+                    packing: Packing::Direct,
+                },
                 BusValue::Packed {
                     start_column: cols::NEXT_PC_LOW_1,
                     packing: Packing::Direct,
                 },
-                BusValue::constant(0),
             ],
         ),
         // BYTE_ALU[next_pc_low[0]; AND, unmasked_low_byte, 254]

prover/src/tables/bytewise.rs

@@ -90,21 +90,44 @@ 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 by `IS_BYTE[μ]`
+/// (`ARE_BYTES[μ, 0]` with multiplicity 1, the spec's default `cond`), 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`] and `lt::MU_MAX` for why the bound is
+/// sent with multiplicity 1 rather than μ.
+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
+}
+
+/// Generates the BYTEWISE trace from a list of operations.
+///
+/// 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 +155,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 +185,23 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ));
     }
 
+    // IS_BYTE[μ] = ARE_BYTES[μ, 0] | 1. 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.
+    // Multiplicity 1 (the spec's default `cond`), so padding rows send
+    // ARE_BYTES[0, 0] too. See `MU_MAX`.
+    interactions.push(BusInteraction::sender(
+        BusId::AreBytes,
+        Multiplicity::One,
+        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(