From 6b538c6b39e9496074d0efe5056fa9ba33a7a0e2 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 3 Aug 2026 12:33:40 -0300 Subject: [PATCH] =?UTF-8?q?perf(keccak):=20inline=20=CE=B8/=CF=81=20halfwo?= =?UTF-8?q?rd=20shifts=20as=20=CE=BC-gated=20identities,=20drop=20120=20HW?= =?UTF-8?q?SL=20sends/row?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace KECCAK_RND's 120 HWSL bus sends per row (θ rotate-by-1: 20, ρ shifts: 100) with degree-2 linear identities over the same committed cells: μ · (in · 2^rnc − right · 2^16 − left) = 0. The existing IS_BYTE and IS_BIT checks make the split unique — given left, right ∈ [0, 2^16), the pair is the Euclidean quotient/remainder of in · 2^rnc ÷ 2^16, and all values stay < 2^32 ≪ p. Sends/row 1151 → 1031 ⇒ −60 aux extension columns (−180 committed base cells/row, ~4.3k/permutation), zero new columns. Constraints 20 → 140, all degree ≤ 3; max_degree() unchanged. Measured −6.8% median prover time on a pure-keccak guest (see the PR for the full A/B). Matches the chip spec as updated by the research team on spec/main (d397668a, #873). --- prover/src/tables/keccak_rnd.rs | 194 ++++++++++++------------ prover/src/tables/trace_builder.rs | 27 ++-- prover/src/tests/trace_builder_tests.rs | 17 ++- 3 files changed, 114 insertions(+), 124 deletions(-) diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 1b121a8b9..51b7759f3 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/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) //! @@ -25,8 +29,8 @@ //! //! Note: spec [[variables.constant]] `rnc` and `rbc` are inlined as compile-time //! constants derived from `KECCAK_RHO[x][y]`, not materialized as columns. -//! `Cxz_right` is typed `[Bit, 4]` per spec d75944ee — HWSL with shift=1 -//! produces a single-bit carry, range-checked via IS_BIT polynomial constraints. +//! `Cxz_right` is typed `[Bit, 4]` per spec d75944ee — a halfword rotate-by-1 +//! carries out a single bit, range-checked via IS_BIT polynomial constraints. use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; @@ -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 { - 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 { } } - // --- 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` templates; we merge adjacent @@ -717,53 +686,8 @@ pub fn bus_interactions() -> Vec { } } - // --- 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,27 +824,99 @@ pub fn bus_interactions() -> Vec { // 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: &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). #[derive(Clone, Copy)] pub struct KeccakRndConstraints; impl ConstraintSet 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>(&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; + } + } + } } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 43654bb54..5ec9fa566 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2336,8 +2336,9 @@ pub(crate) fn collect_bitwise_from_ecdas(ops: &[ecdas::EcdasOperation]) -> Vec Vec { @@ -2414,21 +2415,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( @@ -2493,7 +2489,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; @@ -2506,12 +2503,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. diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 8540b2926..428fd4700 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/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" ); } }