From 30ebfb04063d28e817b9c4205054513051b5ba45 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 23 Jul 2026 16:56:14 -0300 Subject: [PATCH 1/3] =?UTF-8?q?perf(keccak):=20inline=20=CE=B8/=CF=81=20ha?= =?UTF-8?q?lfword=20shifts=20as=20=CE=BC-gated=20identities,=20drop=20120?= =?UTF-8?q?=20HWSL=20sends/row?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the keccak_rnd θ rotate-by-1 (20/row) and ρ (100/row) HWSL bus lookups with inline μ-gated linear identities over the same committed shift cells: μ · (in · 2^rnc − right · 2^16 − left) = 0 (degree 2) Uniqueness of the (left, right) decomposition rests on the existing ARE_BYTES range checks bounding both halves to [0, 2^16) and on 2^16 being invertible mod the Goldilocks prime; the θ IS_BIT carry constraint is now load-bearing. Equivalence to the HWSL contract was z3-verified (all 24 rounds UNSAT under the rewrite; bound-necessity confirmed). Removing the 120 sends/row cuts the LogUp aux width by 3·⌈120/2⌉ = 180 base cells/row (~5.6% of the keccak_rnd table's committed cells) with no new columns. The matching HWSL multiplicities are dropped on the BITWISE side (collect_bitwise_from_keccak). max_degree stays 3; constraint count 20 → 140. Witness values are unchanged (same cells, same values). --- prover/src/tables/keccak_rnd.rs | 190 ++++++++++++------------ prover/src/tables/trace_builder.rs | 27 ++-- prover/src/tests/trace_builder_tests.rs | 17 ++- 3 files changed, 112 insertions(+), 122 deletions(-) diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index afc5dee3a..8f2b184c9 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) //! @@ -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,26 +824,98 @@ 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). 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 5c6b3085e..0ba99e619 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2343,8 +2343,9 @@ pub(crate) fn collect_bitwise_from_ecdas(ops: &[ecdas::EcdasOperation]) -> Vec Vec { @@ -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. 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" ); } } From f6fa7f146d04d062e4816f6fc7c8a62194e77af5 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 23 Jul 2026 17:19:42 -0300 Subject: [PATCH 2/3] spec(keccak): HWSL-inline variant spec + z3 verification and bench evidence Add spec/src/keccak_round_hwsl_inline.toml as an alternative KECCAK_RND specification with the 120 HWSL interactions replaced by mu-gated linear identities (in * 2^rnc = right * 2^16 + left), and thoughts/keccak-hwsl-inline/ with the z3 gate that proves the rewrite equivalent (UNSAT x24 rounds), the bound-necessity proofs (dropping any range check yields a forgery witness), the negative/positive controls, and the pure-keccak bench methodology (-6.8% prover time, 5000-permutation single-epoch continuation proof). --- spec/src/keccak_round_hwsl_inline.toml | 363 ++++++++++++++++++ thoughts/keccak-hwsl-inline/README.md | 101 +++++ .../keccak-hwsl-inline/gen_keccak_bench.sh | 51 +++ thoughts/keccak-hwsl-inline/hwsl_inline.log | 48 +++ .../keccak-hwsl-inline/hwsl_inline_test.py | 266 +++++++++++++ thoughts/keccak-hwsl-inline/keccak_ref.py | 136 +++++++ thoughts/keccak-hwsl-inline/model_dataflow.py | 158 ++++++++ thoughts/keccak-hwsl-inline/par.log | 41 ++ thoughts/keccak-hwsl-inline/tamper_test.py | 53 +++ thoughts/keccak-hwsl-inline/test_dataflow.py | 52 +++ thoughts/keccak-hwsl-inline/test_ref.py | 41 ++ thoughts/keccak-hwsl-inline/z3_parallel.py | 67 ++++ thoughts/keccak-hwsl-inline/z3_verify.py | 291 ++++++++++++++ 13 files changed, 1668 insertions(+) create mode 100644 spec/src/keccak_round_hwsl_inline.toml create mode 100644 thoughts/keccak-hwsl-inline/README.md create mode 100755 thoughts/keccak-hwsl-inline/gen_keccak_bench.sh create mode 100644 thoughts/keccak-hwsl-inline/hwsl_inline.log create mode 100644 thoughts/keccak-hwsl-inline/hwsl_inline_test.py create mode 100644 thoughts/keccak-hwsl-inline/keccak_ref.py create mode 100644 thoughts/keccak-hwsl-inline/model_dataflow.py create mode 100644 thoughts/keccak-hwsl-inline/par.log create mode 100644 thoughts/keccak-hwsl-inline/tamper_test.py create mode 100644 thoughts/keccak-hwsl-inline/test_dataflow.py create mode 100644 thoughts/keccak-hwsl-inline/test_ref.py create mode 100644 thoughts/keccak-hwsl-inline/z3_parallel.py create mode 100644 thoughts/keccak-hwsl-inline/z3_verify.py diff --git a/spec/src/keccak_round_hwsl_inline.toml b/spec/src/keccak_round_hwsl_inline.toml new file mode 100644 index 000000000..c2a296be4 --- /dev/null +++ b/spec/src/keccak_round_hwsl_inline.toml @@ -0,0 +1,363 @@ +# Alternative specification of the KECCAK_RND chip with the HWSL lookups +# inlined as arithmetic constraints (see keccak_round.toml for the original). +# +# Difference vs the original: the 120 HWSL bus interactions (θ rotate-by-1 and +# ρ shifts) are replaced by μ-gated linear identities over the same variables: +# +# in · 2^rnc = right · 2^16 + left +# +# A shift by a compile-time constant is linear over the field, so the lookup +# buys nothing the identity does not — PROVIDED left and right are range +# checked. Given `left, right ∈ [0, 2^16)` the pair is the unique Euclidean +# quotient/remainder of `in · 2^rnc ÷ 2^16` (all values < 2^32 ≪ 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 +# therefore LOAD-BEARING in this variant: without them the decomposition is +# ambiguous and the permutation output is forgeable. +# +# Equivalence with the original chip and the necessity of the range checks +# were machine-checked with an SMT solver (z3): the constraint system below +# admits no witness whose output differs from the FIPS-202 reference round +# (UNSAT, all 24 round indices), while dropping any range bound or IS_BIT +# yields a concrete forgery (SAT). Measured on a pure-keccak continuation +# proof this variant is ~7% faster end to end (−120 sends/row → −60 LogUp +# auxiliary extension columns; +120 degree-2 constraints; no new columns; +# max constraint degree unchanged at 3). + +name = "KECCAK_RND_HWSL_INLINE" + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp at which the permutation is performed" + + +[[variables.input]] +name = "round" +type = "BaseField" +desc = "index of the permutation round" + +[[variables.input]] +name = "start" +type = [[["Byte", 8], 5], 5] +desc = "state at the start of executing the permutation" + +[[variables.auxiliary]] +name = "Cxz" +type = [[["Byte", 8], 4], 5] +desc = "$xor_(i=0)^(y+2) #`start[x,i,z]`$" + +[[variables.auxiliary]] +name = "Cxz_left" +type = [["Byte", 8], 5] +desc = "the left-rotated component of `rotated_Cxz`" + +[[variables.auxiliary]] +name = "Cxz_right" +type = [["Bit", 4], 5] +desc = "the right-rotated component of `rotated_Cxz` (which is a single bit)" + +[[variables.auxiliary]] +name = "Dxz" +type = [["Byte", 8], 5] +desc = "$#`Cxz[`\\(#`x` - 1) mod 5#`,y,z]` xor #`rotated_Cxz[`\\(#`x` + 1) mod 5#`,y,z]`$" + +[[variables.auxiliary]] +name = "theta" +type = [[["Byte", 8], 5], 5] +desc = "$theta(#`start`)$, the state after applying $theta$." + +[[variables.auxiliary]] +name = "rot_left" +type = [[["Byte", 8], 5], 5] +desc = "the left-rotated component of $#`theta[x,y]` <<< #`rnc`$" + +[[variables.auxiliary]] +name = "rot_right" +type = [[["Byte", 8], 5], 5] +desc = "the right-rotated component of $#`theta[x,y]` <<< #`rnc`$" + +[[variables.auxiliary]] +name = "chi_ANDs" +type = [[["Byte", 8], 5], 5] +desc = "$(#`pi[`\\(x+1) mod 5#`,y,z]` xor 255) times.o #`pi[`\\(x + 2) mod 5#`,y,z]`$" + +[[variables.auxiliary]] +name = "chi" +type = [[["Byte", 8], 5], 5] +desc = "$(chi compose pi compose rho compose theta)(#`start`)$; the state after applying $chi$" + +[[variables.auxiliary]] +name = "rc" +type = ["Byte", 8] +desc = "round constants" + +[[variables.auxiliary]] +name = "iota" +type = ["Byte", 8] +desc = "state update following from step $iota$." + +[[variables.virtual]] +name = "rotated_Cxz" +type = [["Byte", 8], 5] +desc = "$#`Cxz[x,`3#`,z]` <<< 1$" +def = {polys=[ + {iters=[["x", 0, 4], ["z", 0]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 3]]}, + {iters=[["x", 0, 4], ["z", 1]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]}, + {iters=[["x", 0, 4], ["z", 2]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 0]]}, + {iters=[["x", 0, 4], ["z", 3]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]}, + {iters=[["x", 0, 4], ["z", 4]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 1]]}, + {iters=[["x", 0, 4], ["z", 5]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]}, + {iters=[["x", 0, 4], ["z", 6]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 2]]}, + {iters=[["x", 0, 4], ["z", 7]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]}, +]} + +[[variables.virtual]] +name = "out" +type = [[["Byte", 8], 5], 5] +desc = "state at the end of executing the permutation" +def = {polys=[ + {iters=[["x", 0], ["y", 0], ["z", 0, 7]], poly=["idx", "iota","z"]}, + {iters=[["x", 1, 4], ["y", 0], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 0], ["y", 1, 4], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 1, 4], ["y", 1, 4], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]} +]} + +[[variables.virtual]] +name = "rho" +type = [[["Byte", 8], 5], 5] +desc = "$(rho compose theta)(#`start`)$; the state after applying $rho$" +def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[ + "+", + ["*", + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0]], + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 2], 8]], + ] + ], + ["*", + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0], + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 2], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 4], 8]], + ] + ], + ["*", + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0]], + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 4], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 6], 8]], + ] + ], + ["*", + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0], + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 6], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"], + ] + ], +]} + +[[variables.virtual]] +name = "pi" +type = [[["Byte", 8], 5], 5] +desc = "$(pi compose rho compose theta)(#`start`)$; the state after applying $pi$" +def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=["idx", ["idx", ["idx", "rho", ["mod", ["+", "x", ["*", 3, "y"]], 5]], "x"], "z"]} + +[[variables.constant]] +name = "rnc" +type = [["Byte", 5], 5] +desc = "lower nibble of `ρ` constants" + +[[variables.constant]] +name = "rpc" +type = [["Half", 5], 5] +desc = "$2^#`rnc`$; the shift factor of the `ρ` rotation as a field constant" + +[[variables.constant]] +name = "rbc" +type = [[["Bit", 2], 5], 5] +desc = "top two bits of `ρ` constants" + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + +# Assumptions + + +# Constraints + +[[constraint_groups]] +name = "io" + +[[constraints.io]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", "round", "start"] +multiplicity = ["-", "μ"] + +[[constraints.io]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", ["+", "round", 1], "out"] +multiplicity = "μ" + +[[constraints.io]] +kind = "interaction" +tag = "KECCAK_RC" +input = ["round"] +output = "rc" +multiplicity = ["-", "μ"] + +[[constraint_groups]] +name = "theta" + +[[constraints.theta]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["idx", ["idx", ["idx", "start", "x"], 1], "z"]] +output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] +iters = [["x", 0, 4], ["z", 0, 7]] +multiplicity = "μ" +ref = "keccak:c:theta_cxz_start" + +[[constraints.theta]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"]] +output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] +iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] +multiplicity = "μ" +ref = "keccak:c:theta_cxz" + +# Inlined θ rotate-by-1 (replaces the HWSL interaction of the original spec). +# A shift by 1 is linear: 2 · C = carry · 2^16 + left, with the halfword `left` +# and the bit `carry` uniquely determined by the IS_BYTE/IS_BIT checks below +# (Euclidean division; all values < 2^17 ≪ p). +[[constraints.theta]] +kind = "arith" +constraint = "$#`μ` => 2 dot #`Cxz[x,3]`_#`z` = #`Cxz_right[x,z]` dot 2^16 + #`Cxz_left[x]`_#`z`$" +poly = ["*", "μ", ["-", + ["*", 2, ["idx", ["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordHL"], "z"]], + ["+", + ["*", ["idx", ["idx", "Cxz_right", "x"], "z"], 65536], + ["idx", ["cast", ["idx", "Cxz_left", "x"], "DWordHL"], "z"], + ], +]] +iters = [["x", 0, 4], ["z", 0, 3]] + +# Note: these IS_BYTE checks are LOAD-BEARING in this variant. Together with +# the linear identity above they pin (Cxz_left, Cxz_right) to the unique +# Euclidean decomposition of 2 · Cxz[x,3]. Without them the decomposition is +# ambiguous and the round output is forgeable (z3: dropping either yields a +# concrete forgery witness). +[[constraints.theta]] +kind = "template" +tag = "IS_BYTE" +input = [["idx", ["idx", "Cxz_left", "x"], "z"]] +iters = [["x", 0, 4], ["z", 0, 7]] +cond = "μ" + +[[constraints.theta]] +kind = "template" +tag = "IS_BIT" +input = [["idx", ["idx", "Cxz_right", "x"], "z"]] +iters = [["x", 0, 4], ["z", 0, 3]] + +[[constraints.theta]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", ["mod", ["-", "x", 1], 5]], 3], "z"], ["idx", ["idx", "rotated_Cxz", ["mod", ["+", "x", 1], 5]], "z"]] +output = ["idx", ["idx", "Dxz", "x"], "z"] +iters = [["x", 0, 4], ["z", 0, 7]] +multiplicity = "μ" +ref = "keccak:c:Dxz" + +[[constraints.theta]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] +output = ["idx", ["idx", ["idx", "theta", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraint_groups]] +name = "rho" + +# Inlined ρ rotation (replaces the HWSL interaction of the original spec). +# A shift by the compile-time constant rnc is linear: +# theta · 2^rnc = rot_right · 2^16 + rot_left, with the decomposition uniquely +# determined by the IS_BYTE checks below (Euclidean division; all values +# < 2^32 ≪ p). For rnc = 0 the identity degenerates to rot_left = theta, +# rot_right = 0 as required. +[[constraints.rho]] +kind = "arith" +constraint = "$#`μ` => #`theta[x,y]`_#`z` dot #`rpc[x,y]` = #`rot_right[x,y]`_#`z` dot 2^16 + #`rot_left[x,y]`_#`z`$" +poly = ["*", "μ", ["-", + ["*", ["idx", ["idx", "rpc", "x"], "y"], ["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"]], + ["+", + ["*", ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"], 65536], + ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], + ], +]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] +ref = "keccak:c:rho_rotation" + +# Note: these IS_BYTE checks are LOAD-BEARING in this variant. Together with +# the linear identity above they pin (rot_left, rot_right) to the unique +# Euclidean decomposition of theta · 2^rnc. Without them the decomposition is +# ambiguous and the round output is forgeable (z3: dropping either yields a +# concrete forgery witness). +[[constraints.rho]] +kind = "template" +tag = "IS_BYTE" +input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +cond = "μ" +ref = "keccak:c:range_rot_left" + +[[constraints.rho]] +kind = "template" +tag = "IS_BYTE" +input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +cond = "μ" +ref = "keccak:c:range_rot_right" + +[[constraint_groups]] +name = "chi" + +[[constraints.chi]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["-", 255, ["idx", ["idx", ["idx", "pi", ["mod", ["+", "x", 1], 5]], "y"], "z"]], ["idx",["idx",["idx", "pi", ["mod", ["+", "x", 2], 5]], "y"], "z"]] +output = ["idx", ["idx", ["idx", "chi_ANDs", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.chi]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "pi", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] +output = ["idx", ["idx", ["idx", "chi", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraint_groups]] +name = "iota" + +[[constraints.iota]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc","z"]] +output = ["idx", "iota", "z"] +iter = ["z", 0, 7] +multiplicity = "μ" diff --git a/thoughts/keccak-hwsl-inline/README.md b/thoughts/keccak-hwsl-inline/README.md new file mode 100644 index 000000000..a9b2ba3af --- /dev/null +++ b/thoughts/keccak-hwsl-inline/README.md @@ -0,0 +1,101 @@ +# KECCAK_RND: inline HWSL shifts as linear identities — formal verification + bench + +This directory contains the SMT (z3) verification and bench evidence behind the +change in this branch: replacing the 120 HWSL bus sends per KECCAK_RND row +(θ rotate-by-1: 20, ρ shifts: 100) with μ-gated degree-2 linear identities + +``` +in · 2^rnc = right · 2^16 + left +``` + +over the same committed cells, keeping all existing IS_BYTE (AreBytes) and +IS_BIT checks. Spec: `spec/src/keccak_round_hwsl_inline.toml` (alternative to +`spec/src/keccak_round.toml`). + +## Why it is sound + +A shift by a compile-time constant is linear over the field. Given +`left ∈ [0, 2^16)` and `right ∈ [0, 2^16)` (θ: `right ∈ {0,1}`), the pair +`(right, left)` is the unique Euclidean quotient/remainder of +`in · 2^rnc ÷ 2^16`; all involved values are `< 2^32 ≪ p`, so field semantics +coincide with the integers. The range checks are load-bearing: without them +`2^16` is invertible mod p and the decomposition is ambiguous. + +## What was machine-checked (z3, QF_BV + Int-mod-p) + +Model: every trace column a free variable; each bus interaction under its +chip's contract and each eval constraint becomes an equation; assert +`output ≠ FIPS-202 reference round` and ask for a counterexample. + +Baseline gate (`z3_verify.py`, `par.log`): +- Original circuit: **UNSAT for all 24 round indices** (round wiring correct + given the chip contracts). +- Positive control: constraints uniquely pin the output to the reference + (the UNSATs are not vacuous). +- Negative controls: 9 injected bugs (dropped θ rotate, swapped ρ offsets, + mangled χ ×2, dropped ι RC, wrong RC, ρ off-by-one, dropped χ equation, + dropped HWSL carry pinning) — **all SAT** (each detected). +- Reference independently anchored: FIPS-202-generated RC/RHO equal the + repo constants; concrete mirror reproduces keccak-f over randomized runs + (`test_ref.py`, `test_dataflow.py`). + +Rewrite gate (`hwsl_inline_test.py`, `hwsl_inline.log`): +- HWSL contracts replaced by the linear identities + only the range checks + that exist in the circuit: **UNSAT for all 24 rounds** (equivalent). +- Bound necessity, in a genuine Int-mod-p model (bitvectors cannot test this: + 2^16 is a zero divisor mod 2^64 but invertible mod p): + dropping a range bound → **SAT** (ambiguous decomposition); + dropping IS_BIT → **SAT** (the θ carry becomes forgeable). +- Coverage audit: every left/right halfword's 16-bit bound comes from an + existing circuit check (AreBytes on `Cxz_left`/`rot_left`/`rot_right`, + IS_BIT on `Cxz_right`) — zero new sends needed. + +Scope: one round's transition given the precomputed-chip contracts +(BITWISE is a fully enumerated 2^20-row preprocessed table). Multiplicity +gating across padding rows degrades identically for the identity and the +old lookup (both ×μ). The model is hand-transcribed from +`keccak_rnd.rs::bus_interactions`; mitigations above (controls + concrete +mirror), long-term fix is generating the model from the constraint IR. + +## Cost accounting + +- Sends: 1151 → 1031 per row (HWSL 120 → 0). +- LogUp aux: 2 interactions per committed pair column + 1 accumulator, + extension degree 3 → −60 extension columns = **−180 committed base + cells/row** (~4.3k per permutation). Zero new columns. +- Constraints: 20 → 140, all measured degree ≤ 3 (identities are μ×linear = + degree 2); `max_degree()` unchanged at 3. + +## Bench (pure-keccak, single-epoch continuation proof) + +Guest: 5000 keccak-f[1600] syscalls (`gen_keccak_bench.sh`). Box: 32 cores / +124 GB. Alternated A/B ×4 after warm-up, prover wall time: + +| | runs (s) | median | +|---|---|---| +| main | 13.988 13.948 13.976 14.398 | 13.982 | +| branch | 13.083 12.971 13.334 12.855 | 13.027 | + +**−6.8% median (−7.2% mean)**; distributions disjoint (slowest branch run +beats fastest main run; cv ≈ 1.3%). keccak_rnd is 86.6% of committed cells in +this bench; committed-cell delta measured 5.61% (prediction: 5.6%); implied +wall-time table delta ≈ 7.9% — above the cell prediction because the removed +cells are all cubic-extension aux (LDE + Merkle + FRI each). For real +workloads: expected gain ≈ 7.9% × keccak_rnd's share of committed cells. + +All proofs verify; a branch proof correctly fails main's verifier (aux layout +shrank — the change is intentionally not wire-identical). + +## Files + +- `z3_verify.py` — baseline gate: free-var model of the original circuit, + contracts, 24-round check, positive + negative controls +- `z3_parallel.py`, `par.log` — parallel driver + full baseline run +- `tamper_test.py` — changed-constraint and removed-constraint controls +- `hwsl_inline_test.py`, `hwsl_inline.log` — the rewrite gate (equivalence + + bound necessity in Int-mod-p) +- `keccak_ref.py`, `test_ref.py` — independent FIPS-202 reference + + external anchoring (hashlib SHA3, regenerated RC/RHO) +- `model_dataflow.py`, `test_dataflow.py` — concrete byte-level mirror of the + modeled equations vs the reference +- `gen_keccak_bench.sh` — bench guest generator diff --git a/thoughts/keccak-hwsl-inline/gen_keccak_bench.sh b/thoughts/keccak-hwsl-inline/gen_keccak_bench.sh new file mode 100755 index 000000000..824f7c73c --- /dev/null +++ b/thoughts/keccak-hwsl-inline/gen_keccak_bench.sh @@ -0,0 +1,51 @@ +#!/bin/bash +# Generate + compile a keccak-heavy guest that applies keccak-f[1600] N times +# in place on a 200-byte state, then commits it. N is arg 1; output ELF is arg 2. +set -euo pipefail +N="${1:?usage: gen_keccak_bench.sh N out.elf}" +OUT="${2:?usage: gen_keccak_bench.sh N out.elf}" +SRC="$(mktemp /tmp/keccak_bench.XXXXXX.s)" +trap 'rm -f "$SRC"' EXIT + +cat > "$SRC" < linear identity) === + ('main', 5) -> unsat + ('main', 3) -> unsat + ('main', 0) -> unsat + ('main', 8) -> unsat + ('main', 4) -> unsat + ('main', 9) -> unsat + ('main', 7) -> unsat + ('main', 2) -> unsat + ('main', 1) -> unsat + ('main', 6) -> unsat + ('main', 11) -> unsat + ('main', 10) -> unsat + ('main', 15) -> unsat + ('main', 16) -> unsat + ('main', 12) -> unsat + ('ctrl', 'theta_no_rot') -> sat + ('ctrl', 'rho_swap') -> sat + ('ctrl', 'chi_no_not') -> sat + ('main', 14) -> unsat + ('ctrl', 'chi_swap') -> sat + ('ctrl', 'iota_no_rc') -> sat + ('main', 13) -> unsat + ('main', 19) -> unsat + ('main', 18) -> unsat + ('main', 17) -> unsat + ('main', 20) -> unsat + ('main', 21) -> unsat + ('main', 22) -> unsat + ('main', 23) -> unsat + + MAIN all-24 UNSAT: True + round-logic controls all SAT: True + +=== PART 2: FIELD (mod p) bound-necessity controls === + rho rnc=12 bounds present -> unsat (want unsat: unique/pinned) + rho rnc=12 DROP right bound -> sat (want sat: ambiguous) + theta rnc=1 IS_BIT present -> unsat (want unsat: carry pinned) + theta rnc=1 DROP IS_BIT -> sat (want sat: ambiguous) + +================ SUMMARY ================ + equivalent under rewrite (all bounds present): YES + round-logic negative controls SAT: True + DROP right-range -> SAT (ambiguous): True + DROP IS_BIT -> SAT (now load-bearing): True + bounds-present -> pinned (rho unsat=True, theta unsat=True) + + OVERALL: REWRITE VALID + BOUNDS NECESSARY (as predicted) diff --git a/thoughts/keccak-hwsl-inline/hwsl_inline_test.py b/thoughts/keccak-hwsl-inline/hwsl_inline_test.py new file mode 100644 index 000000000..77f2423d1 --- /dev/null +++ b/thoughts/keccak-hwsl-inline/hwsl_inline_test.py @@ -0,0 +1,266 @@ +""" +REVERSE REWRITE experiment: replace the keccak_rnd Hwsl bus lookups with a +mu-gated LINEAR IDENTITY over the same committed cells, pinned to a unique +solution by the range bounds that ALREADY exist in the circuit. + +The identity (field elements): for input halfword `in`, shift `rnc`, + in * 2^rnc == right * 2^16 + left +where left = shifted-halfword (Hwsl SLL) and right = carry-halfword (Hwsl SLLC). +Given 0<=left<2^16 and 0<=right<2^16 (from AreBytes byte cells) the pair +(right,left) = (quotient,remainder) of Euclidean division of in*2^rnc by 2^16 — +UNIQUE. Soundness relies on 2^16 being INVERTIBLE in the Goldilocks prime field. + +Two models, deliberately: + (Part 1) BV full-round variant, all bounds present (byte cells = 8-bit BVs = + AreBytes; carry bit = IS_BIT). Here all honest values < 2^31 << p, so a wide + BV with NO wraparound equals field integer arithmetic -> faithful. Used for + the equivalence main-check (all 24 rounds) + the existing round-logic + negative controls. The Hwsl `<<`/`>>` semantics are REMOVED; left/right are + free byte cells related to `in` ONLY by the linear equation. + (Part 2) FIELD (Int mod p) isolated decomposition. A BV model CANNOT show the + drop-range / drop-IS_BIT ambiguity, because 2^16 is a ZERO DIVISOR mod 2^n + (the carry can only absorb multiples of 2^16), so BV would wrongly keep the + decomposition pinned. The prime field is required: 2^16 invertible => a wrong + `left` admits a (large) field `right`. So bound-necessity is proven mod p. +""" +import sys +from concurrent.futures import ProcessPoolExecutor, as_completed +from z3 import ( + BitVec, BitVecVal, Concat, Extract, ZeroExt, Or, And, Not, Solver, sat, unsat, + Int, IntVal, +) +from keccak_ref import RHO, RC, keccak_round +from z3_verify import zref_round, pi_src, cxz_right_bit_for_byte + +P = 2**64 - 2**32 + 1 # Goldilocks prime + +# =========================================================================== +# PART 1 — BV full-round variant (Hwsl lookups -> linear identity) +# =========================================================================== +W = 40 # wide BV width: honest values < 2^33, no wraparound + + +def build_variant(round_idx, tag, bug=None): + C = [] + def V(name, w=8): + return BitVec(f"{tag}_{name}", w) + + start = {(x, y, b): V(f"start_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + cxz = {(x, s, b): V(f"cxz_{x}_{s}_{b}") for x in range(5) for s in range(4) for b in range(8)} + cxzL = {(x, b): V(f"cxzL_{x}_{b}") for x in range(5) for b in range(8)} + cxzR = {(x, hw): V(f"cxzR_{x}_{hw}") for x in range(5) for hw in range(4)} + dxz = {(x, b): V(f"dxz_{x}_{b}") for x in range(5) for b in range(8)} + theta = {(x, y, b): V(f"theta_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotL = {(x, y, b): V(f"rotL_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotR = {(x, y, b): V(f"rotR_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chA = {(x, y, b): V(f"chiand_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chi = {(x, y, b): V(f"chi_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rc = {b: V(f"rc_{b}") for b in range(8)} + iota = {b: V(f"iota_{b}") for b in range(8)} + + def hw16(lo, hi): + return Concat(hi, lo) + + def wb(b8): # widen an 8-bit byte cell to W bits + return ZeroExt(W - 8, b8) + + def operand(sum16): + C.append(sum16 <= BitVecVal(255, 16)) + return Extract(7, 0, sum16) + + # cxz XOR chain (unchanged) + for x in range(5): + for b in range(8): + C.append(cxz[(x, 0, b)] == start[(x, 0, b)] ^ start[(x, 1, b)]) + for s in range(1, 4): + yy = s + 1 + for b in range(8): + C.append(cxz[(x, s, b)] == cxz[(x, s - 1, b)] ^ start[(x, yy, b)]) + + # === THETA rotate-C-by-1: LINEAR IDENTITY replaces Hwsl (rnc=1) === + # in*2 == carry*2^16 + left ; carry in {0,1} via IS_BIT (now LOAD-BEARING); + # left = cxzL halfword bounded to [0,2^16) by the 8-bit byte cells (AreBytes). + for x in range(5): + for hw in range(4): + inpW = wb(cxz[(x, 3, 2 * hw)]) + BitVecVal(256, W) * wb(cxz[(x, 3, 2 * hw + 1)]) + leftW = wb(cxzL[(x, 2 * hw)]) + BitVecVal(256, W) * wb(cxzL[(x, 2 * hw + 1)]) + rightW = wb(cxzR[(x, hw)]) + C.append(inpW * BitVecVal(2, W) == rightW * BitVecVal(2 ** 16, W) + leftW) + if bug != "drop_isbit": + C.append(Or(cxzR[(x, hw)] == 0, cxzR[(x, hw)] == 1)) # IS_BIT (load-bearing) + + def rotated_c(xp, b): + hw = cxz_right_bit_for_byte(b) + expr = ZeroExt(8, cxzL[(xp, b)]) + if hw is not None: + expr = expr + ZeroExt(8, cxzR[(xp, hw)]) + return operand(expr) + + for x in range(5): + for b in range(8): + cm1 = cxz[((x + 4) % 5, 3, b)] + if bug == "theta_no_rot": + rc1 = cxz[((x + 1) % 5, 3, b)] + else: + rc1 = rotated_c((x + 1) % 5, b) + C.append(dxz[(x, b)] == cm1 ^ rc1) + + for x in range(5): + for y in range(5): + for b in range(8): + C.append(theta[(x, y, b)] == start[(x, y, b)] ^ dxz[(x, b)]) + + # === RHO: LINEAR IDENTITY replaces Hwsl === + # in*2^rnc == right*2^16 + left ; left,right = rotL/rotR halfwords bounded to + # [0,2^16) by 8-bit byte cells (AreBytes rs:771-789). + rho_tbl = [[RHO[x][y] for y in range(5)] for x in range(5)] + if bug == "rho_swap": + rho_tbl[1][0], rho_tbl[2][0] = rho_tbl[2][0], rho_tbl[1][0] + for x in range(5): + for y in range(5): + rnc = rho_tbl[x][y] % 16 + for hw in range(4): + inpW = wb(theta[(x, y, 2 * hw)]) + BitVecVal(256, W) * wb(theta[(x, y, 2 * hw + 1)]) + leftW = wb(rotL[(x, y, 2 * hw)]) + BitVecVal(256, W) * wb(rotL[(x, y, 2 * hw + 1)]) + rightW = wb(rotR[(x, y, 2 * hw)]) + BitVecVal(256, W) * wb(rotR[(x, y, 2 * hw + 1)]) + C.append(inpW * BitVecVal(2 ** rnc, W) == rightW * BitVecVal(2 ** 16, W) + leftW) + + def pi(X, Y, z): + sx, sy, l, r = pi_src(X, Y, z) + return operand(ZeroExt(8, rotL[(sx, sy, l)]) + ZeroExt(8, rotR[(sx, sy, r)])) + + for x in range(5): + for y in range(5): + for b in range(8): + p0 = pi(x, y, b) + p1 = pi((x + 1) % 5, y, b) + p2 = pi((x + 2) % 5, y, b) + if bug == "chi_no_not": + C.append(chA[(x, y, b)] == (p1 & p2)) + elif bug == "chi_swap": + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p2) & p1)) + else: + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p1) & p2)) + C.append(chi[(x, y, b)] == p0 ^ chA[(x, y, b)]) + + rc_bytes = [(RC[round_idx] >> (8 * b)) & 0xFF for b in range(8)] + for b in range(8): + C.append(rc[b] == BitVecVal(rc_bytes[b], 8)) + if bug == "iota_no_rc": + C.append(iota[b] == chi[(0, 0, b)]) + else: + C.append(iota[b] == chi[(0, 0, b)] ^ rc[b]) + + def out_byte(x, y, b): + return iota[b] if (x == 0 and y == 0) else chi[(x, y, b)] + + return C, out_byte, start + + +def variant_main_check(round_idx, bug=None): + tag = f"v{round_idx}" + (f"_{bug}" if bug else "") + C, out_byte, start = build_variant(round_idx, tag, bug) + lanes = [[Concat(*[start[(x, y, b)] for b in reversed(range(8))]) for y in range(5)] + for x in range(5)] + ref = zref_round(lanes, RC[round_idx]) + s = Solver() + s.add(And(*C)) + s.add(Or(*[out_byte(x, y, b) != Extract(8 * b + 7, 8 * b, ref[x][y]) + for x in range(5) for y in range(5) for b in range(8)])) + return str(s.check()) + + +# =========================================================================== +# PART 2 — FIELD (mod p) isolated decomposition: bound-necessity controls +# =========================================================================== +def _byte(s, name): + v = Int(name) + s.add(v >= 0, v < 256) + return v + + +def field_rho(rnc, in_val, drop_right_bound): + """Uniqueness of (left,right) for in*2^rnc == right*2^16 + left, mod p. + Returns 'unsat' if a WRONG decomposition (!= Hwsl output) is impossible.""" + s = Solver() + llo, lhi = _byte(s, "llo"), _byte(s, "lhi") # left bytes (AreBytes always present) + left = llo + 256 * lhi + if drop_right_bound: + right = Int("right") # UNBOUNDED field element [0,p) + s.add(right >= 0, right < P) + else: + rlo, rhi = _byte(s, "rlo"), _byte(s, "rhi") # right bytes (AreBytes) + right = rlo + 256 * rhi + # field identity + s.add((in_val * (2 ** rnc) - right * (2 ** 16) - left) % P == 0) + # honest Hwsl output + prod = in_val * (2 ** rnc) + left_ref = prod % (2 ** 16) + # a decomposition that DIFFERS from the honest shifted-left is admissible? + s.add(left != left_ref) + return str(s.check()) # unsat => left pinned to Hwsl value; sat => ambiguous + + +def field_theta(in_val, drop_isbit): + """rnc=1: in*2 == carry*2^16 + left, mod p. carry bounded by IS_BIT only.""" + s = Solver() + llo, lhi = _byte(s, "llo"), _byte(s, "lhi") + left = llo + 256 * lhi + if drop_isbit: + carry = Int("carry") # UNBOUNDED field element + s.add(carry >= 0, carry < P) + else: + carry = Int("carry") + s.add(Or(carry == 0, carry == 1)) # IS_BIT (load-bearing here) + s.add((in_val * 2 - carry * (2 ** 16) - left) % P == 0) + left_ref = (in_val * 2) % (2 ** 16) + s.add(left != left_ref) + return str(s.check()) + + +# =========================================================================== +def main(): + print("=== PART 1: BV full-round variant (Hwsl -> linear identity) ===", flush=True) + controls = ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"] + results = {} + with ProcessPoolExecutor(max_workers=10) as ex: + futs = {} + for r in range(24): + futs[ex.submit(variant_main_check, r, None)] = ("main", r) + for bug in controls: + futs[ex.submit(variant_main_check, 1, bug)] = ("ctrl", bug) + for f in as_completed(futs): + results[futs[f]] = f.result() + print(f" {futs[f]} -> {f.result()}", flush=True) + + main_unsat = all(results[("main", r)] == "unsat" for r in range(24)) + ctrl_ok = all(results[("ctrl", b)] == "sat" for b in controls) + print(f"\n MAIN all-24 UNSAT: {main_unsat}", flush=True) + print(f" round-logic controls all SAT: {ctrl_ok}", flush=True) + + print("\n=== PART 2: FIELD (mod p) bound-necessity controls ===", flush=True) + IN = 0x9C3A # representative input halfword + # rho with a shift whose right halfword is a genuine 2-byte value (rnc=12) + a = field_rho(12, IN, drop_right_bound=False) + b = field_rho(12, IN, drop_right_bound=True) + print(f" rho rnc=12 bounds present -> {a} (want unsat: unique/pinned)", flush=True) + print(f" rho rnc=12 DROP right bound -> {b} (want sat: ambiguous)", flush=True) + c = field_theta(IN, drop_isbit=False) + d = field_theta(IN, drop_isbit=True) + print(f" theta rnc=1 IS_BIT present -> {c} (want unsat: carry pinned)", flush=True) + print(f" theta rnc=1 DROP IS_BIT -> {d} (want sat: ambiguous)", flush=True) + + print("\n================ SUMMARY ================", flush=True) + verdict = (main_unsat and ctrl_ok and a == "unsat" and b == "sat" + and c == "unsat" and d == "sat") + print(f" equivalent under rewrite (all bounds present): {'YES' if main_unsat else 'NO'}") + print(f" round-logic negative controls SAT: {ctrl_ok}") + print(f" DROP right-range -> SAT (ambiguous): {b == 'sat'}") + print(f" DROP IS_BIT -> SAT (now load-bearing): {d == 'sat'}") + print(f" bounds-present -> pinned (rho unsat={a=='unsat'}, theta unsat={c=='unsat'})") + print(f"\n OVERALL: {'REWRITE VALID + BOUNDS NECESSARY (as predicted)' if verdict else 'CHECK FAILURES ABOVE'}") + sys.exit(0 if verdict else 1) + + +if __name__ == "__main__": + main() diff --git a/thoughts/keccak-hwsl-inline/keccak_ref.py b/thoughts/keccak-hwsl-inline/keccak_ref.py new file mode 100644 index 000000000..0c5ab61a3 --- /dev/null +++ b/thoughts/keccak-hwsl-inline/keccak_ref.py @@ -0,0 +1,136 @@ +""" +Independent Keccak-f[1600] reference, built from the FIPS-202 spec ALGORITHMS +(not by copying the circuit or the repo's constant tables). + + - RHO offsets generated from the FIPS-202 (x,y) walk with triangular offsets. + - RC round constants generated from the FIPS-202 LFSR (rc(t)). + - theta / rho / pi / chi / iota implemented per FIPS-202. + +Validation anchors (see run at bottom / test_ref.py): + - The permutation is wired into a SHA3-256 sponge and checked against + Python's hashlib (an independent NIST implementation). + - RHO/RC are separately cross-checked against the repo's KECCAK_RHO/KECCAK_RC. + +Lane indexing matches the circuit: state[x + 5*y], x = column, y = row. +""" + +MASK64 = (1 << 64) - 1 + + +def rotl64(v, r): + r &= 63 + if r == 0: + return v & MASK64 + return ((v << r) | (v >> (64 - r))) & MASK64 + + +# --- RHO offsets from the FIPS-202 recurrence (Algorithm 2, rho) --------------- +# Start at (x,y) = (1,0); for t = 0..23 the offset is (t+1)(t+2)/2 mod 64, +# then (x,y) <- (y, (2x+3y) mod 5). (0,0) keeps offset 0. +def gen_rho(): + rho = [[0] * 5 for _ in range(5)] # rho[x][y] + x, y = 1, 0 + for t in range(24): + rho[x][y] = ((t + 1) * (t + 2) // 2) % 64 + x, y = y, (2 * x + 3 * y) % 5 + return rho + + +RHO = gen_rho() + + +# --- RC round constants from the FIPS-202 LFSR (Algorithm 5, rc) --------------- +def _rc_bit(t): + t %= 255 + if t == 0: + return 1 + R = 0b10000000 # register holding r0..r7, r0 = MSB per our shifting below + # Use the standard byte-register formulation. + R = 0x01 + for _ in range(t): + R <<= 1 + if R & 0x100: + R ^= 0x71 # x^8 + x^6 + x^5 + x^4 + 1 -> low byte feedback 0x71 + R &= 0xFF + return R & 1 + + +def gen_rc(): + rc = [] + for ir in range(24): + w = 0 + for j in range(7): # j = 0..6 -> bit positions 2^j - 1 + if _rc_bit(j + 7 * ir): + w |= 1 << ((1 << j) - 1) + rc.append(w & MASK64) + return rc + + +RC = gen_rc() + + +# --- The permutation, per FIPS-202 ------------------------------------------- +def keccak_round(state, rc): + """One round of Keccak-f[1600]. `state` is list[25] of u64, state[x+5y].""" + a = list(state) + + # theta + C = [a[x] ^ a[x + 5] ^ a[x + 10] ^ a[x + 15] ^ a[x + 20] for x in range(5)] + D = [C[(x + 4) % 5] ^ rotl64(C[(x + 1) % 5], 1) for x in range(5)] + for x in range(5): + for y in range(5): + a[x + 5 * y] ^= D[x] + + # rho + pi: B[X][Y] = rotl(A[(X+3Y)%5][X], RHO[(X+3Y)%5][X]) + B = [0] * 25 + for X in range(5): + for Y in range(5): + sx = (X + 3 * Y) % 5 + sy = X + B[X + 5 * Y] = rotl64(a[sx + 5 * sy], RHO[sx][sy]) + + # chi + out = [0] * 25 + for x in range(5): + for y in range(5): + out[x + 5 * y] = B[x + 5 * y] ^ ((~B[(x + 1) % 5 + 5 * y] & MASK64) & B[(x + 2) % 5 + 5 * y]) + + # iota + out[0] ^= rc + return out + + +def keccak_f1600(state): + s = list(state) + for r in range(24): + s = keccak_round(s, RC[r]) + return s + + +# --- SHA3-256 sponge on top of the permutation (for external validation) ------ +def sha3_256(msg: bytes) -> bytes: + rate = 136 # bytes (1088 bits) + # pad10*1 with SHA-3 domain separation 0x06 + m = bytearray(msg) + m.append(0x06) + while len(m) % rate != 0: + m.append(0x00) + m[-1] ^= 0x80 + + state = [0] * 25 + for off in range(0, len(m), rate): + block = m[off:off + rate] + for i in range(rate // 8): + lane = int.from_bytes(block[i * 8:i * 8 + 8], "little") + state[i] ^= lane + state = keccak_f1600(state) + + out = bytearray() + while len(out) < 32: + for i in range(rate // 8): + out += state[i].to_bytes(8, "little") + if len(out) >= 32: + break + if len(out) < 32: + state = keccak_f1600(state) + return bytes(out[:32]) diff --git a/thoughts/keccak-hwsl-inline/model_dataflow.py b/thoughts/keccak-hwsl-inline/model_dataflow.py new file mode 100644 index 000000000..9579a787b --- /dev/null +++ b/thoughts/keccak-hwsl-inline/model_dataflow.py @@ -0,0 +1,158 @@ +""" +Concrete byte-level mirror of the keccak_rnd circuit's contract dataflow. + +Every equation here corresponds 1:1 to a bus interaction / eval constraint in +prover/src/tables/keccak_rnd.rs, evaluated FORWARD with concrete ints. Its sole +job is to validate that the byte-level wiring I will hand-encode into z3 +actually reproduces the FIPS-202 reference round (guards against a wholesale +wrong model that a symbolic UNSAT could not reveal). + +The `bug` flag lets us confirm each negative control genuinely perturbs output. +Line-number citations (prover/src/tables/keccak_rnd.rs) in comments. +""" +from keccak_ref import RHO, RC + + +def lane_to_bytes(v): + return [(v >> (8 * b)) & 0xFF for b in range(8)] + + +def bytes_to_lane(bs): + return sum(int(bs[b]) << (8 * b) for b in range(8)) + + +def cxz_right_bit_for_byte(b): + # keccak_rnd.rs:126-132 -> even b: Some((b/2 + 3)%4); odd: None + return (b // 2 + 3) % 4 if b % 2 == 0 else None + + +def pi_src_bytes(X, Y, z): + # keccak_rnd.rs:161-174 pi_src_cols: (sx,sy)=((X+3Y)%5, X), rbc=RHO[sx][sy]//16 + sx = (X + 3 * Y) % 5 + sy = X + rbc = RHO[sx][sy] // 16 + if rbc == 0: + l, r = z, (z + 6) % 8 + elif rbc == 1: + l, r = (z + 6) % 8, (z + 4) % 8 + elif rbc == 2: + l, r = (z + 4) % 8, (z + 2) % 8 + else: + l, r = (z + 2) % 8, z + return sx, sy, l, r + + +def round_dataflow(start_lanes, r, bug=None): + """Forward-evaluate one round via the circuit's contract equations. + + start_lanes: list[25] u64. Returns list[25] u64 (out state).""" + S = [[lane_to_bytes(start_lanes[x + 5 * y]) for y in range(5)] for x in range(5)] + # index as S[x][y][b] + + # === theta: Cxz XOR chain === keccak_rnd.rs:539-588 + cxz = [[[0] * 8 for _ in range(4)] for _ in range(5)] + for x in range(5): + for b in range(8): + cxz[x][0][b] = S[x][0][b] ^ S[x][1][b] # :541-559 + for stage in range(1, 4): + y = stage + 1 + for b in range(8): + cxz[x][stage][b] = cxz[x][stage - 1][b] ^ S[x][y][b] # :567-585 + + # === theta: HWSL rotate-C-by-1 === keccak_rnd.rs:593-631 + cxz_left = [[0] * 8 for _ in range(5)] + cxz_right = [[0] * 4 for _ in range(5)] + for x in range(5): + for hw in range(4): + Chw = cxz[x][3][2 * hw] | (cxz[x][3][2 * hw + 1] << 8) # :600-609 input hw + left16 = (Chw << 1) & 0xFFFF # :613-622 shifted + cxz_left[x][2 * hw] = left16 & 0xFF + cxz_left[x][2 * hw + 1] = (left16 >> 8) & 0xFF + cxz_right[x][hw] = (Chw >> 15) & 1 # :624 carry bit + + def rotated_c(xp, b): + # keccak_rnd.rs:322-329 / 663-672 reconstruction + contrib = 0 + hw = cxz_right_bit_for_byte(b) + if hw is not None: + contrib = cxz_right[xp][hw] + val = cxz_left[xp][b] + contrib + assert val <= 255, "rotated_C operand exceeds a byte" + return val + + # === theta: Dxz XOR === keccak_rnd.rs:661-690 + Dxz = [[0] * 8 for _ in range(5)] + for x in range(5): + for b in range(8): + cm1 = cxz[(x + 4) % 5][3][b] # C[(x-1)%5] + rc1 = rotated_c((x + 1) % 5, b) # rot(C[(x+1)%5],1) + if bug == "theta_no_rot": + rc1 = cxz[(x + 1) % 5][3][b] # drop the rotate + Dxz[x][b] = cm1 ^ rc1 + + # === theta final XOR === keccak_rnd.rs:694-717 + theta = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + for b in range(8): + theta[x][y][b] = S[x][y][b] ^ Dxz[x][b] + + # === rho: HWSL === keccak_rnd.rs:723-766 + rho_tbl = [[RHO[x][y] for y in range(5)] for x in range(5)] + if bug == "rho_swap": + rho_tbl[1][0], rho_tbl[2][0] = rho_tbl[2][0], rho_tbl[1][0] + rot_left = [[[0] * 8 for _ in range(5)] for _ in range(5)] + rot_right = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + rnc = rho_tbl[x][y] % 16 + for hw in range(4): + Thw = theta[x][y][2 * hw] | (theta[x][y][2 * hw + 1] << 8) + left16 = (Thw << rnc) & 0xFFFF + right16 = (Thw >> (16 - rnc)) & 0xFFFF if rnc > 0 else 0 + rot_left[x][y][2 * hw] = left16 & 0xFF + rot_left[x][y][2 * hw + 1] = (left16 >> 8) & 0xFF + rot_right[x][y][2 * hw] = right16 & 0xFF + rot_right[x][y][2 * hw + 1] = (right16 >> 8) & 0xFF + + def pi(X, Y, z): + # keccak_rnd.rs:793-795 virtual pi = rot_left[l] + rot_right[r] + sx, sy, l, rr = pi_src_bytes(X, Y, z) + val = rot_left[sx][sy][l] + rot_right[sx][sy][rr] + assert val <= 255, "pi operand exceeds a byte" + return val + + # === chi: AND then XOR === keccak_rnd.rs:796-870 + chi = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + for b in range(8): + p0 = pi(x, y, b) + p1 = pi((x + 1) % 5, y, b) + p2 = pi((x + 2) % 5, y, b) + if bug == "chi_no_not": + ands = p1 & p2 # drop the NOT + elif bug == "chi_swap": + ands = (0xFF - p2) & p1 # swap the two operands + else: + ands = (0xFF - p1) & p2 # (255 - pi[x+1]) AND pi[x+2] + chi[x][y][b] = p0 ^ ands + + # === iota === keccak_rnd.rs:872-894 + rc_bytes = lane_to_bytes(RC[r]) + iota = [0] * 8 + for b in range(8): + if bug == "iota_no_rc": + iota[b] = chi[0][0][b] # drop rc XOR + else: + iota[b] = chi[0][0][b] ^ rc_bytes[b] + + # === output handoff === keccak_rnd.rs:496-509 + out = [0] * 25 + for x in range(5): + for y in range(5): + if x == 0 and y == 0: + out[0] = bytes_to_lane(iota) + else: + out[x + 5 * y] = bytes_to_lane(chi[x][y]) + return out diff --git a/thoughts/keccak-hwsl-inline/par.log b/thoughts/keccak-hwsl-inline/par.log new file mode 100644 index 000000000..e509ade4b --- /dev/null +++ b/thoughts/keccak-hwsl-inline/par.log @@ -0,0 +1,41 @@ +DONE pos True -> output uniquely pinned to reference +DONE bug chi_swap -> sat +DONE bug chi_no_not -> sat +DONE bug theta_no_rot -> sat +DONE bug rho_swap -> sat +DONE bug iota_no_rc -> sat +DONE round 3 -> unsat +DONE round 2 -> unsat +DONE round 5 -> unsat +DONE round 6 -> unsat +DONE round 0 -> unsat +DONE round 1 -> unsat +DONE round 9 -> unsat +DONE round 8 -> unsat +DONE round 4 -> unsat +DONE round 7 -> unsat +DONE round 10 -> unsat +DONE round 13 -> unsat +DONE round 12 -> unsat +DONE round 15 -> unsat +DONE round 11 -> unsat +DONE round 14 -> unsat +DONE round 18 -> unsat +DONE round 16 -> unsat +DONE round 19 -> unsat +DONE round 17 -> unsat +DONE round 20 -> unsat +DONE round 21 -> unsat +DONE round 23 -> unsat +DONE round 22 -> unsat + +================ SUMMARY ================ +positive control (non-vacuity): PASS (output uniquely pinned to reference) +negative control theta_no_rot : sat OK +negative control rho_swap : sat OK +negative control chi_no_not : sat OK +negative control chi_swap : sat OK +negative control iota_no_rc : sat OK +main check: ALL 24 UNSAT + +VERDICT: VERIFIED (given contracts) diff --git a/thoughts/keccak-hwsl-inline/tamper_test.py b/thoughts/keccak-hwsl-inline/tamper_test.py new file mode 100644 index 000000000..c731a3cb3 --- /dev/null +++ b/thoughts/keccak-hwsl-inline/tamper_test.py @@ -0,0 +1,53 @@ +"""Tamper demo: CHANGED constraints and REMOVED constraints must both flip +the gate from UNSAT (verified) to SAT (forgeable). Clean model run first as +the control.""" +from z3 import Solver, And, Or, Concat, Extract, sat, unsat, is_true +import z3_verify as zv +from keccak_ref import RC + +ROUND = 1 + +print("=== control: clean model, round 1 ===") +r = zv.check_round(ROUND) +print(f" clean -> {r} (want unsat) {'OK' if r == unsat else '!!! BROKEN'}") +assert r == unsat + +CASES = [ + ("iota_wrong_rc", "CHANGED"), + ("rho_off_by_one", "CHANGED"), + ("drop_chi_xor_byte", "REMOVED"), + ("drop_hwsl_carry", "REMOVED"), +] + +print("\n=== tampered models: gate must catch every one (SAT) ===") +for bug, kind in CASES: + r = zv.check_round(ROUND, bug=bug) + ok = "OK — gate catches it" if r == sat else "!!! GATE MISSED THE BUG" + print(f" {kind} {bug:18s} -> {r} {ok}") + assert r == sat, f"gate failed to catch {bug}" + +# ---- exhibit the forged witnesses for the two REMOVED cases ----------------- +def exhibit(bug): + C, out_byte, start = zv.build_circuit(ROUND, f"cex_{bug}", bug=bug) + lanes = [[Concat(*[start[(x, y, b)] for b in reversed(range(8))]) + for y in range(5)] for x in range(5)] + ref = zv.zref_round(lanes, RC[ROUND]) + rb = lambda x, y, b: Extract(8 * b + 7, 8 * b, ref[x][y]) + s = Solver() + s.add(And(*C)) + s.add(Or(*[out_byte(x, y, b) != rb(x, y, b) + for x in range(5) for y in range(5) for b in range(8)])) + assert s.check() == sat + m = s.model() + bad = [(x, y, b) for x in range(5) for y in range(5) for b in range(8) + if is_true(m.evaluate(out_byte(x, y, b) != rb(x, y, b)))] + lanes_hit = sorted(set((x, y) for x, y, _ in bad)) + print(f" {bug}: forged witness makes {len(bad)} output bytes wrong; " + f"lanes hit: {lanes_hit[:8]}{'...' if len(lanes_hit) > 8 else ''}") + +print("\n=== forged-witness exhibits (REMOVED cases) ===") +exhibit("drop_chi_xor_byte") +exhibit("drop_hwsl_carry") + +print("\nVERDICT: clean=UNSAT, all 4 tampers=SAT -> gate is sensitive to both " + "changed AND removed constraints.") diff --git a/thoughts/keccak-hwsl-inline/test_dataflow.py b/thoughts/keccak-hwsl-inline/test_dataflow.py new file mode 100644 index 000000000..a0361f2cb --- /dev/null +++ b/thoughts/keccak-hwsl-inline/test_dataflow.py @@ -0,0 +1,52 @@ +"""Validate the concrete contract-dataflow against the independent reference.""" +import random +from keccak_ref import RC, keccak_round, keccak_f1600 +from model_dataflow import round_dataflow + +rng = random.Random(0xC0FFEE) +M = (1 << 64) - 1 + +print("=== per-round: contract dataflow vs FIPS-202 reference (random states) ===") +ok = True +for trial in range(200): + st = [rng.randrange(0, 1 << 64) for _ in range(25)] + r = rng.randrange(0, 24) + got = round_dataflow(st, r) + exp = keccak_round(st, RC[r]) + if got != exp: + ok = False + print(f" MISMATCH trial={trial} round={r}") + break +print(" 200 random single rounds match:", ok) +assert ok + +print("\n=== 24-round chain (full permutation) via dataflow vs reference ===") +ok2 = True +for trial in range(20): + st = [rng.randrange(0, 1 << 64) for _ in range(25)] + s = list(st) + for r in range(24): + s = round_dataflow(s, r) + if s != keccak_f1600(st): + ok2 = False + print(f" MISMATCH trial={trial}") + break +print(" 20 full 24-round permutations match:", ok2) +assert ok2 + +# Also: all-zero and specific structured inputs +for st in ([0] * 25, [1] * 25, list(range(25)), [M] * 25): + s = list(st) + for r in range(24): + s = round_dataflow(s, r) + assert s == keccak_f1600(st), st[:3] +print(" structured inputs (zeros/ones/range/all-FF) match: True") + +print("\n=== sanity: each injected bug DOES change output (concrete) ===") +st = [rng.randrange(0, 1 << 64) for _ in range(25)] +for bug in ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"]: + changed = any(round_dataflow(st, r, bug=bug) != keccak_round(st, RC[r]) for r in range(24)) + print(f" bug={bug:14s} perturbs output: {changed}") + assert changed, bug + +print("\nALL DATAFLOW VALIDATIONS PASSED") diff --git a/thoughts/keccak-hwsl-inline/test_ref.py b/thoughts/keccak-hwsl-inline/test_ref.py new file mode 100644 index 000000000..0f80d6eac --- /dev/null +++ b/thoughts/keccak-hwsl-inline/test_ref.py @@ -0,0 +1,41 @@ +"""Validate the independent reference: constants + full permutation.""" +import hashlib +from keccak_ref import RC, RHO, sha3_256 + +# Repo constants (from executor/src/vm/instruction/execution.rs:646-680), pasted +# here ONLY to cross-check my spec-generated values. Correctness is anchored to +# FIPS-202 (my generators) + hashlib, not to these. +REPO_RC = [ + 0x0000000000000001, 0x0000000000008082, 0x800000000000808A, 0x8000000080008000, + 0x000000000000808B, 0x0000000080000001, 0x8000000080008081, 0x8000000000008009, + 0x000000000000008A, 0x0000000000000088, 0x0000000080008009, 0x000000008000000A, + 0x000000008000808B, 0x800000000000008B, 0x8000000000008089, 0x8000000000008003, + 0x8000000000008002, 0x8000000000000080, 0x000000000000800A, 0x800000008000000A, + 0x8000000080008081, 0x8000000000008080, 0x0000000080000001, 0x8000000080008008, +] +# KECCAK_RHO[x][y] in the repo +REPO_RHO = [ + [0, 36, 3, 41, 18], + [1, 44, 10, 45, 2], + [62, 6, 43, 15, 61], + [28, 55, 25, 21, 56], + [27, 20, 39, 8, 14], +] + +print("=== constant cross-checks (spec-generated vs repo) ===") +print("RC match:", RC == REPO_RC) +print("RHO match:", RHO == REPO_RHO) +assert RC == REPO_RC, (RC, REPO_RC) +assert RHO == REPO_RHO, (RHO, REPO_RHO) + +print("\n=== SHA3-256 vs hashlib (external NIST impl) ===") +tests = [b"", b"abc", b"The quick brown fox jumps over the lazy dog", bytes(range(200))] +allok = True +for t in tests: + mine = sha3_256(t).hex() + ref = hashlib.sha3_256(t).hexdigest() + ok = mine == ref + allok &= ok + print(f" len={len(t):3d} match={ok} {mine}") +assert allok +print("\nALL REFERENCE VALIDATIONS PASSED") diff --git a/thoughts/keccak-hwsl-inline/z3_parallel.py b/thoughts/keccak-hwsl-inline/z3_parallel.py new file mode 100644 index 000000000..2797a7d84 --- /dev/null +++ b/thoughts/keccak-hwsl-inline/z3_parallel.py @@ -0,0 +1,67 @@ +"""Parallel driver: run all 24 round UNSAT checks + 5 negative controls + +positive control concurrently, print each result as it lands.""" +import sys +from concurrent.futures import ProcessPoolExecutor, as_completed +from z3 import sat, unsat +from z3_verify import check_round, positive_control + +BUGS = ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"] + + +def w_round(r): + return ("round", r, str(check_round(r))) + + +def w_bug(bug): + return ("bug", bug, str(check_round(1, bug=bug))) + + +def w_pos(): + ok, msg = positive_control(5, seed=1) + return ("pos", ok, msg) + + +def main(): + tasks = [] + with ProcessPoolExecutor(max_workers=10) as ex: + futs = [] + futs.append(ex.submit(w_pos)) + for bug in BUGS: + futs.append(ex.submit(w_bug, bug)) + for r in range(24): + futs.append(ex.submit(w_round, r)) + + results = {} + for f in as_completed(futs): + kind, key, val = f.result() + results[(kind, key)] = val + print(f"DONE {kind} {key} -> {val}", flush=True) + + print("\n================ SUMMARY ================", flush=True) + pos = results[("pos", True)] if ("pos", True) in results else results.get(("pos", False)) + # positive control stored under actual ok value; find it + pos_ok = ("pos", True) in results + pos_msg = results.get(("pos", True)) or results.get(("pos", False)) + print(f"positive control (non-vacuity): {'PASS' if pos_ok else 'FAIL'} ({pos_msg})") + + neg_ok = True + for bug in BUGS: + v = results[("bug", bug)] + ok = (v == "sat") + neg_ok &= ok + print(f"negative control {bug:14s}: {v:6s} {'OK' if ok else 'FAIL(!vacuous)'}") + + all_unsat = True + for r in range(24): + v = results[("round", r)] + all_unsat &= (v == "unsat") + bad = [r for r in range(24) if results[("round", r)] != "unsat"] + print(f"main check: {'ALL 24 UNSAT' if all_unsat else 'NOT ALL UNSAT: ' + str([(r, results[('round', r)]) for r in bad])}") + + verdict = pos_ok and neg_ok and all_unsat + print("\nVERDICT:", "VERIFIED (given contracts)" if verdict else "NOT VERIFIED — investigate") + sys.exit(0 if verdict else 1) + + +if __name__ == "__main__": + main() diff --git a/thoughts/keccak-hwsl-inline/z3_verify.py b/thoughts/keccak-hwsl-inline/z3_verify.py new file mode 100644 index 000000000..dc2a12148 --- /dev/null +++ b/thoughts/keccak-hwsl-inline/z3_verify.py @@ -0,0 +1,291 @@ +""" +Formal (z3 / QF_BV) assume-guarantee check that one `keccak_rnd` round, as +wired in prover/src/tables/keccak_rnd.rs, computes a correct Keccak-f[1600] +round GIVEN the helper-chip contracts (ByteAlu XOR/AND, Hwsl, KeccakRc; the +AreBytes/IS_BIT range checks are captured by byte-width + explicit bit/byte +domain constraints). + +Method: every trace column is a FREE bitvector. Each bus interaction and eval +constraint becomes an equation relating those free vars (under the referenced +chip's contract). The output lanes are whatever the constraints force. We assert +`output != reference_round(input)` and ask z3 for a counterexample: + UNSAT -> for all constraint-satisfying assignments, output == reference. + SAT -> the constraints permit a wrong output (under-constrained / mis-wired). + +The reference round (`zref_round`) is written directly from FIPS-202 with 64-bit +BV ops (RotateLeft / xor / and / not) — structurally independent of the circuit's +byte-level HWSL wiring. + +Contracts assumed (assume-guarantee): + ByteAlu(op,a,b,c): a,b,c are bytes and c = a `op` b (op in {XOR,AND}). Operands + given as linear combos are required to be bytes (the lookup only has byte + rows) -> modeled as `sum <= 255` on the field value, low 8 bits used. + Hwsl(in16, s, left16, right16): left16 = (in16 << s) mod 2^16, + right16 = in16 >> (16 - s) (right16 = 0 when s = 0). + KeccakRc(round, rc[8]): rc = little-endian bytes of KECCAK_RC[round]. +""" +import sys +from z3 import ( + BitVec, BitVecVal, Concat, Extract, LShR, RotateLeft, ZeroExt, Or, And, + Solver, sat, unsat, +) +from keccak_ref import RHO, RC + +# -------------------------------------------------------------------------- +# byte<->column helpers mirroring keccak_rnd.rs::cols +# -------------------------------------------------------------------------- +def cxz_right_bit_for_byte(b): # rs:126-132 + return (b // 2 + 3) % 4 if b % 2 == 0 else None + +def pi_src(X, Y, z): # rs:161-174 + sx = (X + 3 * Y) % 5 + sy = X + rbc = RHO[sx][sy] // 16 + l, r = [(z, (z + 6) % 8), + ((z + 6) % 8, (z + 4) % 8), + ((z + 4) % 8, (z + 2) % 8), + ((z + 2) % 8, z)][rbc] + return sx, sy, l, r + + +# -------------------------------------------------------------------------- +# Independent z3-native reference round (FIPS-202, 64-bit lanes) +# -------------------------------------------------------------------------- +def zref_round(lanes, rc_val, bug=None): + # lanes[x][y] : 64-bit BV. Reference is ALWAYS correct (bug only perturbs + # the circuit model, never this). + C = [lanes[x][0] ^ lanes[x][1] ^ lanes[x][2] ^ lanes[x][3] ^ lanes[x][4] + for x in range(5)] + D = [C[(x + 4) % 5] ^ RotateLeft(C[(x + 1) % 5], 1) for x in range(5)] + a = [[lanes[x][y] ^ D[x] for y in range(5)] for x in range(5)] + B = [[None] * 5 for _ in range(5)] + for X in range(5): + for Y in range(5): + sx = (X + 3 * Y) % 5 + sy = X + B[X][Y] = RotateLeft(a[sx][sy], RHO[sx][sy]) + out = [[None] * 5 for _ in range(5)] + for x in range(5): + for y in range(5): + out[x][y] = B[x][y] ^ ((~B[(x + 1) % 5][y]) & B[(x + 2) % 5][y]) + out[0][0] = out[0][0] ^ BitVecVal(rc_val, 64) + return out + + +# -------------------------------------------------------------------------- +# Build the circuit-model constraint system as free vars + equations. +# Returns (constraints, out_byte(x,y,b), start_byte(x,y,b)). +# -------------------------------------------------------------------------- +def build_circuit(round_idx, tag, bug=None): + C = [] # list of z3 Bool constraints + def V(name, w=8): # fresh free var + return BitVec(f"{tag}_{name}", w) + + # free columns ----------------------------------------------------------- + start = {(x, y, b): V(f"start_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + cxz = {(x, s, b): V(f"cxz_{x}_{s}_{b}") for x in range(5) for s in range(4) for b in range(8)} + cxzL = {(x, b): V(f"cxzL_{x}_{b}") for x in range(5) for b in range(8)} + cxzR = {(x, hw): V(f"cxzR_{x}_{hw}") for x in range(5) for hw in range(4)} + dxz = {(x, b): V(f"dxz_{x}_{b}") for x in range(5) for b in range(8)} + theta = {(x, y, b): V(f"theta_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotL = {(x, y, b): V(f"rotL_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotR = {(x, y, b): V(f"rotR_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chA = {(x, y, b): V(f"chiand_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chi = {(x, y, b): V(f"chi_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rc = {b: V(f"rc_{b}") for b in range(8)} + iota = {b: V(f"iota_{b}") for b in range(8)} + + def hw16(lo, hi): # 16-bit from (low byte, high byte) + return Concat(hi, lo) + + def byte_op_operand(field_expr16): + # ByteAlu operand contract: field value must be a byte. + C.append(field_expr16 <= BitVecVal(255, 16)) + return Extract(7, 0, field_expr16) + + # === theta: Cxz XOR chain === rs:539-588 + for x in range(5): + for b in range(8): + C.append(cxz[(x, 0, b)] == start[(x, 0, b)] ^ start[(x, 1, b)]) + for s in range(1, 4): + yy = s + 1 + for b in range(8): + C.append(cxz[(x, s, b)] == cxz[(x, s - 1, b)] ^ start[(x, yy, b)]) + + # === theta: HWSL rotate-C-by-1 === rs:593-631 (+ eval IS_BIT rs:914-924) + for x in range(5): + for hw in range(4): + inp = hw16(cxz[(x, 3, 2 * hw)], cxz[(x, 3, 2 * hw + 1)]) + left16 = inp << 1 + C.append(hw16(cxzL[(x, 2 * hw)], cxzL[(x, 2 * hw + 1)]) == left16) + if bug != "drop_hwsl_carry": + C.append(cxzR[(x, hw)] == ZeroExt(7, Extract(15, 15, inp))) # carry bit + # REMOVAL DEMO drop_hwsl_carry: no Hwsl lookup pins the carry — + # only the IS_BIT eval constraint below survives (carry forgeable). + C.append(Or(cxzR[(x, hw)] == 0, cxzR[(x, hw)] == 1)) # IS_BIT (redundant) + + def rotated_c(xp, b): # rs:322-329 / 663-672 + hw = cxz_right_bit_for_byte(b) + expr = ZeroExt(8, cxzL[(xp, b)]) + if hw is not None: + expr = expr + ZeroExt(8, cxzR[(xp, hw)]) + return byte_op_operand(expr) + + # === theta: Dxz XOR === rs:661-690 + for x in range(5): + for b in range(8): + cm1 = cxz[((x + 4) % 5, 3, b)] + if bug == "theta_no_rot": + rc1 = cxz[((x + 1) % 5, 3, b)] # drop rotate + else: + rc1 = rotated_c((x + 1) % 5, b) + C.append(dxz[(x, b)] == cm1 ^ rc1) + + # === theta final XOR === rs:694-717 + for x in range(5): + for y in range(5): + for b in range(8): + C.append(theta[(x, y, b)] == start[(x, y, b)] ^ dxz[(x, b)]) + + # === rho: HWSL === rs:723-766 + rho_tbl = [[RHO[x][y] for y in range(5)] for x in range(5)] + if bug == "rho_swap": + rho_tbl[1][0], rho_tbl[2][0] = rho_tbl[2][0], rho_tbl[1][0] + if bug == "rho_off_by_one": + rho_tbl[3][2] += 1 # one lane's shift amount off by 1 + for x in range(5): + for y in range(5): + rnc = rho_tbl[x][y] % 16 + for hw in range(4): + inp = hw16(theta[(x, y, 2 * hw)], theta[(x, y, 2 * hw + 1)]) + left16 = inp << rnc + C.append(hw16(rotL[(x, y, 2 * hw)], rotL[(x, y, 2 * hw + 1)]) == left16) + if rnc == 0: + C.append(rotR[(x, y, 2 * hw)] == 0) + C.append(rotR[(x, y, 2 * hw + 1)] == 0) + else: + right16 = LShR(inp, 16 - rnc) + C.append(hw16(rotR[(x, y, 2 * hw)], rotR[(x, y, 2 * hw + 1)]) == right16) + + def pi(X, Y, z): # rs:793-795 virtual pi + sx, sy, l, r = pi_src(X, Y, z) + return byte_op_operand(ZeroExt(8, rotL[(sx, sy, l)]) + ZeroExt(8, rotR[(sx, sy, r)])) + + # === chi: AND then XOR === rs:796-870 + for x in range(5): + for y in range(5): + for b in range(8): + if bug == "drop_chi_xor_byte" and (x, y, b) == (2, 3, 5): + continue # REMOVAL DEMO: this output byte's defining equations gone + p0 = pi(x, y, b) + p1 = pi((x + 1) % 5, y, b) + p2 = pi((x + 2) % 5, y, b) + if bug == "chi_no_not": + C.append(chA[(x, y, b)] == (p1 & p2)) + elif bug == "chi_swap": + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p2) & p1)) + else: + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p1) & p2)) + C.append(chi[(x, y, b)] == p0 ^ chA[(x, y, b)]) + + # === iota === rs:872-894 (rc pinned by KeccakRc contract rs:518-535) + rc_round = (round_idx + 1) % 24 if bug == "iota_wrong_rc" else round_idx + rc_bytes = [(RC[rc_round] >> (8 * b)) & 0xFF for b in range(8)] + for b in range(8): + C.append(rc[b] == BitVecVal(rc_bytes[b], 8)) + if bug == "iota_no_rc": + C.append(iota[b] == chi[(0, 0, b)]) + else: + C.append(iota[b] == chi[(0, 0, b)] ^ rc[b]) + + def out_byte(x, y, b): # rs:496-509 handoff + return iota[b] if (x == 0 and y == 0) else chi[(x, y, b)] + + return C, out_byte, start + + +# -------------------------------------------------------------------------- +def check_round(round_idx, bug=None): + tag = f"r{round_idx}" + (f"_{bug}" if bug else "") + C, out_byte, start = build_circuit(round_idx, tag, bug=bug) + + # symbolic input lanes from the SAME free start bytes + lanes = [[Concat(*[start[(x, y, b)] for b in reversed(range(8))]) for y in range(5)] + for x in range(5)] + ref = zref_round(lanes, RC[round_idx]) + ref_byte = lambda x, y, b: Extract(8 * b + 7, 8 * b, ref[x][y]) + + s = Solver() + s.add(And(*C)) + # counterexample: circuit output differs from reference somewhere + s.add(Or(*[out_byte(x, y, b) != ref_byte(x, y, b) + for x in range(5) for y in range(5) for b in range(8)])) + return s.check() + + +def positive_control(round_idx, seed): + # Non-vacuity: fix start to concrete bytes, solve the constraint system + # (no diff assertion), confirm SAT and that the pinned output == reference. + import random + rng = random.Random(seed) + tag = f"pos{round_idx}" + C, out_byte, start = build_circuit(round_idx, tag) + s = Solver() + s.add(And(*C)) + concrete = {} + for x in range(5): + for y in range(5): + for b in range(8): + v = rng.randrange(0, 256) + concrete[(x, y, b)] = v + s.add(start[(x, y, b)] == v) + if s.check() != sat: + return False, "constraint system UNSAT for a concrete input (VACUOUS!)" + m = s.model() + # reference from concrete input + from keccak_ref import keccak_round + in_lanes = [sum(concrete[(x, y, b)] << (8 * b) for b in range(8)) + for y in range(5) for x in range(5)] + # in_lanes indexed x+5y: + in_lanes = [0] * 25 + for x in range(5): + for y in range(5): + in_lanes[x + 5 * y] = sum(concrete[(x, y, b)] << (8 * b) for b in range(8)) + exp = keccak_round(in_lanes, RC[round_idx]) + for x in range(5): + for y in range(5): + got = sum(int(str(m.evaluate(out_byte(x, y, b)))) << (8 * b) for b in range(8)) + if got != exp[x + 5 * y]: + return False, f"pinned output != reference at lane ({x},{y})" + return True, "output uniquely pinned to reference" + + +if __name__ == "__main__": + bugs = ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"] + + print("=== POSITIVE CONTROL (non-vacuity): constraints SAT & pin output ===") + ok, msg = positive_control(5, seed=1) + print(f" round 5: {ok} ({msg})") + assert ok + + print("\n=== NEGATIVE CONTROLS (round 1): each buggy model must be SAT ===") + for bug in bugs: + r = check_round(1, bug=bug) + print(f" bug={bug:14s} -> {r} (want sat)") + assert r == sat, f"VACUOUS ENCODING: buggy model {bug} returned {r}" + + print("\n=== MAIN CHECK: clean model, all 24 rounds must be UNSAT ===") + allunsat = True + for r in range(24): + res = check_round(r) + allunsat &= (res == unsat) + print(f" round {r:2d} -> {res}") + if res != unsat: + print(" !!! COUNTEREXAMPLE FOUND — investigate") + print() + if allunsat: + print("VERDICT: all 24 rounds UNSAT + all negative controls SAT + positive control OK") + print("=> keccak_rnd round is provably correct GIVEN the chip contracts.") + else: + print("VERDICT: at least one round SAT — see above.") + sys.exit(1) From afe78a0604da9c6013642f86451224090801d8c9 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 23 Jul 2026 17:38:03 -0300 Subject: [PATCH 3/3] spec(keccak): render the HWSL-inline variant chip in the keccak chapter Wire keccak_round_hwsl_inline.toml into keccak.typ as an explicit alternative section (variables + changed theta/rho constraint groups; chi/iota/io are identical to KECCAK_RND), with the Euclidean-uniqueness soundness argument in prose. Rename the variant's constraint refs to keccak:c:inline_* to avoid duplicate labels with the original chip. The spec machinery independently derives KECCAK_RND_HWSL_INLINE = 1251 interactions vs KECCAK_RND = 1371, confirming the -120 HWSL sends. --- spec/keccak.typ | 26 ++++++++++++++++++++++++++ spec/src/keccak_round_hwsl_inline.toml | 12 ++++++------ 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 11d900c73..cf7ba1142 100644 --- a/spec/keccak.typ +++ b/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) diff --git a/spec/src/keccak_round_hwsl_inline.toml b/spec/src/keccak_round_hwsl_inline.toml index c2a296be4..bb16bd899 100644 --- a/spec/src/keccak_round_hwsl_inline.toml +++ b/spec/src/keccak_round_hwsl_inline.toml @@ -227,7 +227,7 @@ input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["id output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" -ref = "keccak:c:theta_cxz_start" +ref = "keccak:c:inline_theta_cxz_start" [[constraints.theta]] kind = "interaction" @@ -236,7 +236,7 @@ input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] multiplicity = "μ" -ref = "keccak:c:theta_cxz" +ref = "keccak:c:inline_theta_cxz" # Inlined θ rotate-by-1 (replaces the HWSL interaction of the original spec). # A shift by 1 is linear: 2 · C = carry · 2^16 + left, with the halfword `left` @@ -279,7 +279,7 @@ input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", ["mod", ["-", "x", 1], output = ["idx", ["idx", "Dxz", "x"], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" -ref = "keccak:c:Dxz" +ref = "keccak:c:inline_Dxz" [[constraints.theta]] kind = "interaction" @@ -309,7 +309,7 @@ poly = ["*", "μ", ["-", ], ]] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] -ref = "keccak:c:rho_rotation" +ref = "keccak:c:inline_rho_rotation" # Note: these IS_BYTE checks are LOAD-BEARING in this variant. Together with # the linear identity above they pin (rot_left, rot_right) to the unique @@ -322,7 +322,7 @@ tag = "IS_BYTE" input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] cond = "μ" -ref = "keccak:c:range_rot_left" +ref = "keccak:c:inline_range_rot_left" [[constraints.rho]] kind = "template" @@ -330,7 +330,7 @@ tag = "IS_BYTE" input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] cond = "μ" -ref = "keccak:c:range_rot_right" +ref = "keccak:c:inline_range_rot_right" [[constraint_groups]] name = "chi"