perf(keccak): inline HWSL shifts as linear identities (−6.8% pure-keccak prover time, z3-verified)#860
Draft
MauroToscano wants to merge 3 commits into
Draft
perf(keccak): inline HWSL shifts as linear identities (−6.8% pure-keccak prover time, z3-verified)#860MauroToscano wants to merge 3 commits into
MauroToscano wants to merge 3 commits into
Conversation
…120 HWSL sends/row
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).
…idence 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).
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.
MauroToscano
marked this pull request as draft
July 23, 2026 20:49
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Replace the 120 HWSL bus sends per KECCAK_RND row (θ rotate-by-1: 20, ρ shifts: 100) with μ-gated degree-2 linear identities over the same committed cells:
All existing IS_BYTE (AreBytes) and IS_BIT checks are kept — they become load-bearing: given
left, right ∈ [0, 2^16), the pair is the unique Euclidean quotient/remainder ofin · 2^rnc ÷ 2^16(values < 2^32 ≪ p, so field semantics = integer semantics). A shift by a compile-time constant is field-linear, so the lookup bought nothing the identity doesn't — it only paid LogUp aux.max_degree()unchanged)spec/src/keccak_round_hwsl_inline.toml: alternative chip spec for this variant (original left untouched)Formal verification (z3)
thoughts/keccak-hwsl-inline/contains the full SMT gate + logs:output ≠ FIPS-202 reference roundis UNSAT for all 24 round indices. Positive control: constraints uniquely pin the output (UNSAT not vacuous). Negative controls: 9 injected bugs (dropped rotate, swapped ρ offsets, mangled χ, dropped RC, dropped carry pinning, …) — all correctly SAT.Bench
Pure-keccak guest (5000 keccak-f syscalls, single-epoch continuation proof), 32-core box, alternated A/B ×4 after warm-up:
−6.8% median (−7.2% mean), distributions disjoint (cv ≈ 1.3%). keccak_rnd = 86.6% of committed cells in this bench; measured committed-cell delta 5.61% matches the predicted −180 cells/row; implied wall-time table delta ≈ 7.9% (beats the cell prediction — the removed cells are all cubic-extension aux). Expected real-workload gain ≈ 7.9% × keccak_rnd's share of committed cells.
Happy to run
/bench-abbaon the bench server for the real-block number if wanted.Tests
check_tablekeccak_rnd: prover folder ≡ verifier folder ≡ IR interpreter; 140 constraints, every one measured degree ≤ 3test_keccak_constraint_counts,test_keccak_bitwise_ops_count(HWSL 2880 → 0),test_keccak_bus_interaction_countstest_prove_elfs_keccak,_keccak_multi_call(tiny-keccak cross-check),_unaligned_state_addr(tamper still rejected), IR/window-capture agreement testsmake lintclean