perf(zkvm): W-aware right-shift lookup tables — SRLW/SRAW 5->2 rows, SRLIW/SRAIW 3->1 - #1753
Draft
0xAndoroid wants to merge 3 commits into
Draft
perf(zkvm): W-aware right-shift lookup tables — SRLW/SRAW 5->2 rows, SRLIW/SRAIW 3->1#17530xAndoroid wants to merge 3 commits into
0xAndoroid wants to merge 3 commits into
Conversation
Contributor
|
Warning This PR has more than 500 changed lines and does not include a spec. Large features and architectural changes benefit from a spec-driven workflow. If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message. |
Contributor
Benchmark comparison (crates) |
The instruction read-raf kernel parity fixture assigned arbitrary random lookup indices to whatever tables sit at fixed enum positions. With the W-aware right-shift tables appended, the last variant (VirtualSRAW) has a constrained operand domain: its prefix-suffix decomposition only matches materialize_entry when the right operand is bitmask-shaped, so the first-principles input claim diverged from the kernels' round sums (RoundCheckFailed at round 0). Expose per-table in-domain index generation behind a new jolt-lookup-tables test-utils feature (random_lookup_index takes &self and dispatches through LookupTableKind; the bitmask generators move to an index_gen module shared between cfg(test) and the feature). The fixture now draws each table row's index from that table's domain and keeps the edge indices (0, all-ones, all-ones upper half) on table-less rows, since the RAF operand paths they target are table-independent. This also lets the fixture exercise constrained tables at all — previously any fixture position landing on SRA/SRL/ROTR would have failed the same way. Regenerate the registered-inline expansion parity hashes: SHA-256 inlines expand SRLIW/SRAIW sites, so the shrunk sequences change row counts (2436 -> 2244 per block) and row-stream hashes.
0xAndoroid
force-pushed
the
vseq-wshift-tables
branch
from
August 10, 2026 15:49
5dfd2f5 to
f24dc41
Compare
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
Adds three W-aware lookup tables so the word right-shifts stop lifting through the 64-bit shift machinery:
These are hot in real RV64 guests (u32 arithmetic codegen).
New tables + shape budget
ShiftRightBitmaskW: combine =2^32·One − Pow2W·pow2w— 2 suffixes, reuses the shipped Pow2W machinery including its final-phase absorption.VirtualSRAW: exact arity mirror of the shippedVirtualSRA— 3 prefixes / 4 suffixes, fill termx31·(2^64 − 2^(32−s')).VirtualSRLW: 2 prefixes / 4 suffixes; the result's bit-31 sign-extension stays live at s' = 0 via a dedicated y₀ term (validated first, before anything else, by the phase-boundary-sweepingprefix_suffixharness at both geometries).All three are bilinear and within the
MAX_SUFFIXES = 4budget.Why new tables instead of reusing the 64-bit SRL/SRA tables with a 32-bit mask: that shortcut is unsound — the existing tables' prefix/suffix closed forms (
leading_ones/trailing_zeros) assume ones-prefix mask shapes and give wrong values on 32-bit-confined masks (counterexample-checked during design). The W tables exist because the mask algebra genuinely differs.Read-raf cost, priced: +3 used tables ≈ 120–230K field mults/proof (~0.01% at 2^22; present-table-gated, zero cost in guests without W-shifts), verifier +~900 mults, proof +96 B. This is a small fixed set serving four architectural instructions in every RV64 guest — not a per-constant family.
Testing
mle_full_hypercube::<8>with 32-bit-mask index override (ROTRW precedent); exhaustive host-sidematerialize_entryvsw >> sover all s' ∈ [0,32) × edge operands (sign bit, garbage upper word) — both stacks; ABI append tests-D warnings; fmtRebased on current main (post-#1748).