perf(keccak): inline HWSL shifts as linear identities (−6.8% pure-keccak prover time, z3-verified)

prover/src/tables/keccak_rnd.rs

@@ -1,7 +1,11 @@
 //! KECCAK_RND: Round chip for Keccak-f[1600] permutation.
 //!
-//! One row per round (24 rows per keccak call). All bitwise operations are
-//! delegated to BITWISE lookup tables (BYTE_ALU, HWSL, ARE_BYTES).
+//! One row per round (24 rows per keccak call). Bitwise XOR/AND are delegated
+//! to BITWISE lookup tables (BYTE_ALU, ARE_BYTES); the halfword shifts (θ
+//! rotate-by-1 and ρ) are enforced directly by μ-gated linear identities over
+//! the committed shift cells instead of HWSL lookups (see
+//! `KeccakRndConstraints`). ARE_BYTES range checks on the shift outputs and the
+//! IS_BIT constraint on the θ carry are load-bearing for the identities.
 //!
 //! ## Column layout (1,480 columns)
 //!
@@ -429,12 +433,17 @@ pub fn generate_keccak_rnd_trace(
 }
 
 // =========================================================================
-// Bus interactions (1,371 total)
+// Bus interactions (1,031 total)
 // =========================================================================
+//
+// The θ/ρ halfword shifts no longer emit HWSL lookups (120 sends/row removed):
+// they are enforced by the inline μ-gated linear identities in
+// `KeccakRndConstraints`. The matching HWSL multiplicities are likewise dropped
+// on the BITWISE side (`collect_bitwise_from_keccak`).
 
 #[allow(clippy::needless_range_loop)]
 pub fn bus_interactions() -> Vec<BusInteraction> {
-    let mut interactions = Vec::with_capacity(1371);
+    let mut interactions = Vec::with_capacity(1031);
 
     // --- IO group (3) ---
 
@@ -587,48 +596,8 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         }
     }
 
-    // --- Theta: HWSL for rotated C (20) ---
-    // HWSL(C[x] halfword[hw], 1) → (Cxz_left, Cxz_right)
-    // Cxz_right is a single carry bit zero-extended to a halfword (spec d75944ee).
-    for x in 0..5 {
-        for hw in 0..4 {
-            interactions.push(BusInteraction::sender(
-                BusId::Hwsl,
-                Multiplicity::Column(cols::MU),
-                vec![
-                    // Input halfword: Cxz[x][3][hw*2] + 256 * Cxz[x][3][hw*2+1]
-                    BusValue::linear(vec![
-                        LinearTerm::Column {
-                            coefficient: 1,
-                            column: cols::cxz(x, 3, hw * 2),
-                        },
-                        LinearTerm::Column {
-                            coefficient: 256,
-                            column: cols::cxz(x, 3, hw * 2 + 1),
-                        },
-                    ]),
-                    // Shift amount = 1
-                    BusValue::constant(1),
-                    // Output: shifted
-                    BusValue::linear(vec![
-                        LinearTerm::Column {
-                            coefficient: 1,
-                            column: cols::cxz_left(x, hw * 2),
-                        },
-                        LinearTerm::Column {
-                            coefficient: 256,
-                            column: cols::cxz_left(x, hw * 2 + 1),
-                        },
-                    ]),
-                    // Output: carry (single bit cast to Half — high byte = 0).
-                    BusValue::Packed {
-                        start_column: cols::cxz_right_bit(x, hw),
-                        packing: Packing::Direct,
-                    },
-                ],
-            ));
-        }
-    }
+    // --- Theta: rotate-C-by-1 shift is enforced by an inline μ-gated linear
+    //     identity (see `KeccakRndConstraints`), not an HWSL lookup. ---
 
     // --- Theta: ARE_BYTES range checks on Cxz_left (20 pairs) ---
     // Spec emits 40 `IS_BYTE<Cxz_left[x][z]>` templates; we merge adjacent
@@ -717,53 +686,8 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         }
     }
 
-    // --- Rho: HWSL (100) ---
-    // HWSL(theta[x][y] halfword[hw], rnc[x][y]) → (rot_left, rot_right)
-    // rnc is inlined as a constant: KECCAK_RHO[x][y] % 16.
-    for x in 0..5 {
-        for y in 0..5 {
-            let rnc_val = (KECCAK_RHO[x][y] % 16) as u64;
-            for hw in 0..4 {
-                interactions.push(BusInteraction::sender(
-                    BusId::Hwsl,
-                    Multiplicity::Column(cols::MU),
-                    vec![
-                        BusValue::linear(vec![
-                            LinearTerm::Column {
-                                coefficient: 1,
-                                column: cols::theta(x, y, hw * 2),
-                            },
-                            LinearTerm::Column {
-                                coefficient: 256,
-                                column: cols::theta(x, y, hw * 2 + 1),
-                            },
-                        ]),
-                        BusValue::constant(rnc_val),
-                        BusValue::linear(vec![
-                            LinearTerm::Column {
-                                coefficient: 1,
-                                column: cols::rot_left(x, y, hw * 2),
-                            },
-                            LinearTerm::Column {
-                                coefficient: 256,
-                                column: cols::rot_left(x, y, hw * 2 + 1),
-                            },
-                        ]),
-                        BusValue::linear(vec![
-                            LinearTerm::Column {
-                                coefficient: 1,
-                                column: cols::rot_right(x, y, hw * 2),
-                            },
-                            LinearTerm::Column {
-                                coefficient: 256,
-                                column: cols::rot_right(x, y, hw * 2 + 1),
-                            },
-                        ]),
-                    ],
-                ));
-            }
-        }
-    }
+    // --- Rho: the per-lane shift is enforced by inline μ-gated linear
+    //     identities (see `KeccakRndConstraints`), not HWSL lookups. ---
 
     // --- Rho: ARE_BYTES range checks on rot_left + rot_right (200 pairs) ---
     // Spec emits 400 IS_BYTE templates (200 per side); we merge each
@@ -900,26 +824,98 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
 // Single-source constraint set (ConstraintBuilder front-end)
 // =========================================================================
 
-/// The KECCAK round table's 20 transition constraints as a single
-/// [`ConstraintSet`]: for `x ∈ 0..5`, `hw ∈ 0..4` (idx `x·4 + hw`), the μ-gated
-/// `IS_BIT` on `Cxz_right[x][hw]` — `μ · Cxz_right·(1 − Cxz_right)`.
+/// The 16-bit value `main[lo_col] + 256·main[hi_col]` (byte pair → halfword).
+#[inline]
+fn halfword<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>(
+    b: &B,
+    lo_col: usize,
+    hi_col: usize,
+) -> B::Expr {
+    b.main(0, lo_col) + b.main(0, hi_col) * b.const_base(256)
+}
+
+/// The KECCAK round table's 140 transition constraints as a single
+/// [`ConstraintSet`]:
+///
+/// * **20 IS_BIT** on the θ carry bits: for `x ∈ 0..5`, `hw ∈ 0..4`, the μ-gated
+///   `μ · Cxz_right·(1 − Cxz_right)` (degree 3). Load-bearing: it pins the θ
+///   carry to a single bit so the θ shift identity below is unique.
+/// * **20 θ shift identities** (rnc = 1): for `x ∈ 0..5`, `hw ∈ 0..4`,
+///   `μ · (in·2 − right·2¹⁶ − left)` where `in` is the `Cxz[x][3]` halfword,
+///   `left` the `Cxz_left` byte pair and `right` the single `Cxz_right` carry
+///   bit (degree 2).
+/// * **100 ρ shift identities**: for `x,y ∈ 0..5`, `hw ∈ 0..4` with
+///   `rnc = KECCAK_RHO[x][y] % 16`, `μ · (in·2^rnc − right·2¹⁶ − left)` where
+///   `in` is the `theta[x][y]` halfword, `left`/`right` the `rot_left`/
+///   `rot_right` byte pairs (degree 2; the general form covers rnc = 0, which
+///   pins right = 0, left = in).
+///
+/// These identities replace the former θ/ρ HWSL bus lookups. Uniqueness of the
+/// (left, right) decomposition rests on the ARE_BYTES range checks bounding both
+/// halves to `[0, 2¹⁶)` and on `2¹⁶` being invertible mod the Goldilocks prime
+/// (z3-verified equivalent to the HWSL contract).
 pub struct KeccakRndConstraints;
 
 impl ConstraintSet<GoldilocksField, GoldilocksExtension> for KeccakRndConstraints {
-    // The IS_BIT constraints are gated by μ (cond·x·(1−x)), so degree 3.
+    // The IS_BIT constraints are gated by μ (cond·x·(1−x)), so degree 3; the
+    // shift identities are μ × linear, degree 2.
     fn max_degree(&self) -> usize {
         3
     }
 
+    #[allow(clippy::needless_range_loop)]
     fn eval<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>(&self, b: &mut B) {
         use crate::constraints::templates::emit_is_bit;
 
+        let two_16 = 1u64 << 16;
         let mut idx = 0;
+
+        // (1) IS_BIT on the θ carry bits (Cxz_right).
         for x in 0..5 {
             for hw in 0..4 {
                 emit_is_bit(b, idx, cols::cxz_right_bit(x, hw), Some(cols::MU));
                 idx += 1;
             }
         }
+
+        // (2) θ rotate-C-by-1 shift identity (rnc = 1):
+        //     μ · (in·2 − right·2¹⁶ − left) = 0.
+        for x in 0..5 {
+            for hw in 0..4 {
+                let inp = halfword(b, cols::cxz(x, 3, hw * 2), cols::cxz(x, 3, hw * 2 + 1));
+                let left = halfword(b, cols::cxz_left(x, hw * 2), cols::cxz_left(x, hw * 2 + 1));
+                let right = b.main(0, cols::cxz_right_bit(x, hw));
+                let identity = inp * b.const_base(2) - right * b.const_base(two_16) - left;
+                let mu = b.main(0, cols::MU);
+                b.emit_base(idx, mu * identity);
+                idx += 1;
+            }
+        }
+
+        // (3) ρ shift identity (rnc = KECCAK_RHO[x][y] % 16):
+        //     μ · (in·2^rnc − right·2¹⁶ − left) = 0.
+        for x in 0..5 {
+            for y in 0..5 {
+                let rnc = KECCAK_RHO[x][y] % 16;
+                let pow = 1u64 << rnc;
+                for hw in 0..4 {
+                    let inp = halfword(b, cols::theta(x, y, hw * 2), cols::theta(x, y, hw * 2 + 1));
+                    let left = halfword(
+                        b,
+                        cols::rot_left(x, y, hw * 2),
+                        cols::rot_left(x, y, hw * 2 + 1),
+                    );
+                    let right = halfword(
+                        b,
+                        cols::rot_right(x, y, hw * 2),
+                        cols::rot_right(x, y, hw * 2 + 1),
+                    );
+                    let identity = inp * b.const_base(pow) - right * b.const_base(two_16) - left;
+                    let mu = b.main(0, cols::MU);
+                    b.emit_base(idx, mu * identity);
+                    idx += 1;
+                }
+            }
+        }
     }
 }

prover/src/tables/trace_builder.rs

@@ -2343,8 +2343,9 @@ pub(crate) fn collect_bitwise_from_ecdas(ops: &[ecdas::EcdasOperation]) -> Vec<B
 
 /// Collect BITWISE lookups generated by the keccak chips.
 ///
-/// The keccak round chip sends BYTE_ALU, HWSL, and ARE_BYTES
-/// interactions; the keccak core chip sends IS_HALF interactions.
+/// The keccak round chip sends BYTE_ALU and ARE_BYTES interactions (the θ/ρ
+/// halfword shifts are enforced by inline constraints, not HWSL lookups); the
+/// keccak core chip sends IS_HALF interactions.
 /// All of these must be registered so the BITWISE table's multiplicities are correct.
 #[allow(clippy::needless_range_loop)]
 pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec<BitwiseOperation> {
@@ -2421,21 +2422,16 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec
                 }
             }
 
-            // theta: HWSL for rotated C (20) + ARE_BYTES on Cxz_left (20 pairs).
-            // Cxz_right is range-checked via IS_BIT polynomial constraints
-            // on the keccak_rnd chip, not via lookups (spec d75944ee).
+            // theta: ARE_BYTES on Cxz_left (20 pairs). The rotate-by-1 shift is
+            // enforced by the keccak_rnd inline μ-gated identity, so no HWSL
+            // lookup is emitted here. Cxz_right is range-checked via IS_BIT
+            // polynomial constraints on the keccak_rnd chip (spec d75944ee).
             let mut rotated_c = [[0u8; 8]; 5];
             for x in 0..5 {
                 let c = cxz[x][3];
                 for hw in 0..4 {
                     let halfword = (c[hw * 2] as u16) | ((c[hw * 2 + 1] as u16) << 8);
                     let shifted = halfword << 1; // u16 wraps
-                    ops.push(BitwiseOperation::new(
-                        BitwiseOperationType::Hwsl,
-                        (halfword & 0xFF) as u8,
-                        ((halfword >> 8) & 0xFF) as u8,
-                        1,
-                    ));
                     // ARE_BYTES for cxz_left bytes: paired (low, high) of the halfword,
                     // matching `(cxz_left[x][2i], cxz_left[x][2i+1])` sender pairing.
                     ops.push(BitwiseOperation::byte_op(
@@ -2500,7 +2496,8 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec
                 }
             }
 
-            // rho: HWSL (100) + ARE_BYTES (200 pairs)
+            // rho: ARE_BYTES (200 pairs). The per-lane shift is enforced by the
+            // keccak_rnd inline μ-gated identities, so no HWSL lookup is emitted.
             for x in 0..5 {
                 for y in 0..5 {
                     let rho_offset = KECCAK_RHO[x][y] as usize;
@@ -2513,12 +2510,6 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec
                         } else {
                             (halfword << rnc_val, halfword >> (16 - rnc_val))
                         };
-                        ops.push(BitwiseOperation::new(
-                            BitwiseOperationType::Hwsl,
-                            (halfword & 0xFF) as u8,
-                            ((halfword >> 8) & 0xFF) as u8,
-                            rnc_val,
-                        ));
                         // ARE_BYTES paired as (rot_left[b], rot_right[b]) for
                         // each byte of the halfword, matching the sender pairing
                         // in keccak_rnd::bus_interactions.

prover/src/tests/trace_builder_tests.rs

@@ -627,9 +627,11 @@ mod keccak_tests {
         // Spec emits one IS_BYTE template per byte; ops pair adjacent bytes
         // into ARE_BYTES (20 cxz_left + 200 rho per round, 4 addr per call).
         assert_eq!(are_bytes, 24 * 220 + 4, "AreBytes count");
-        assert_eq!(hwsl, 24 * 120, "Hwsl count");
+        // θ/ρ halfword shifts are enforced by inline μ-gated identities on the
+        // keccak_rnd chip, so no HWSL lookups are emitted (was 24 * 120).
+        assert_eq!(hwsl, 0, "Hwsl count");
         assert_eq!(is_half, 100, "IsHalf count");
-        assert_eq!(ops.len(), 105 + 24 * 1148, "Total bitwise ops");
+        assert_eq!(ops.len(), 105 + 24 * 1028, "Total bitwise ops");
     }
 
     #[test]
@@ -732,9 +734,10 @@ mod keccak_tests {
         );
         assert_eq!(
             keccak_rnd::bus_interactions().len(),
-            1151,
-            "KECCAK_RND: 3 IO + 440 theta + 300 rho + 400 chi + 8 iota \
-             (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee; \
+            1031,
+            "KECCAK_RND: 3 IO + 420 theta + 200 rho + 400 chi + 8 iota \
+             (θ/ρ HWSL sends replaced by inline μ-gated shift identities: −20 θ, −100 ρ; \
+             Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee; \
              ARE_BYTES sends are paired per spec ARE_BYTES interaction signature)"
         );
         assert_eq!(
@@ -765,8 +768,8 @@ mod keccak_tests {
         );
         assert_eq!(
             keccak_rnd::KeccakRndConstraints.meta().len(),
-            20,
-            "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) per spec d75944ee"
+            140,
+            "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) + 20 θ + 100 ρ inline shift identities"
         );
     }
 }

spec/keccak.typ

@@ -114,6 +114,32 @@ Lastly, the round chip contributes the following interactions to the lookup:
 - when executed in large volumnes, `KECCAK_RND` could benefit from having a three-way XOR lookup table. With this in place, the 80 interactions in @keccak:c:theta_cxz_start and @keccak:c:theta_cxz could be dropped.
   Likewise, 80 columns could be removed from the chip (a \~5% savings).
 
+= Round chip: HWSL-inline variant (alternative)
+#let round_inline_chip = load_chip("src/keccak_round_hwsl_inline.toml", config)
+#let keccak_rnd_inline = raw(round_inline_chip.name)
+
+This section specifies #keccak_rnd_inline, an alternative to #keccak_rnd in which the 120 `HWSL` interactions (the $theta$ rotate-by-one and the $rho$ shifts) are replaced by arithmetic constraints over the same variables.
+A shift by a compile-time constant is linear over the field:
+$ #`in` dot 2^#`rnc` = #`right` dot 2^16 + #`left` $
+Given $#`left`, #`right` in [0, 2^16)$, the pair is the unique Euclidean quotient/remainder of $#`in` dot 2^#`rnc` div 2^16$; all values involved are smaller than $2^32 lt.double p$, so field semantics coincide with the integers.
+The `IS_BYTE` checks on `Cxz_left`/`rot_left`/`rot_right` and the `IS_BIT` checks on `Cxz_right` are load-bearing here: without them $2^16$ is invertible modulo $p$ and the decomposition is ambiguous.
+Equivalence with #keccak_rnd and the necessity of the range checks were machine-checked with an SMT solver; the constraint system admits no witness whose output differs from the FIPS-202 reference round, while dropping any range check yields a concrete forgery (see `thoughts/keccak-hwsl-inline/`).
+Compared to #keccak_rnd this removes 120 interactions per row (60 fewer committed auxiliary extension columns) at the cost of 120 degree-2 constraints; columns and maximum constraint degree are unchanged.
+
+== Columns
+#let nr_variables = total_nr_variables(round_inline_chip)
+#let nr_columns = total_nr_instantiated_columns(round_inline_chip, config)
+#let nr_interactions = compute_nr_interactions(round_inline_chip)
+
+The #keccak_rnd_inline chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s).
+The variables are those of #keccak_rnd plus the constant `rpc`, with $#`rpc[x][y]` = 2^#`rnc[x][y]`$:
+#render_chip_variable_table(round_inline_chip, config)
+
+== Constraints
+Only the $theta$ and $rho$ groups differ from #keccak_rnd; the `chi`, `iota` and `io` groups are identical.
+#render_constraint_table(round_inline_chip, config, groups: "theta")
+#render_constraint_table(round_inline_chip, config, groups: "rho")
+
 = Round constant lookup
 #let rc_chip = load_chip("src/keccak_rc.toml", config)
 #let keccak_rc = raw(rc_chip.name)