Feat/is whh by jotabulacios · Pull Request #1022 · yetanotherco/lambda_vm

jotabulacios · 2026-10-15T13:39:14Z

Merge after #1016.

Implements the spec changes from #1003 and #1015, plus the IS_WH multiplicity bound from #1017.

New IS_WH table: one row per distinct (Word, Half) pair, range-checks its three halves with multiplicity μ and bounds μ with IS_B20[μ]. Pairs sent more than 2^20 − 1 times are split over several rows.
is_whh() helper for the template: sends IS_WH[word_hi, half_mid] and IS_HALF[half_lo]. The caller's cond must be a bit.
KECCAK state_ptr moves from DWordHL to DWordWHH: 486 columns and 84 interactions instead of 511 and 134.
TableCounts gets an is_wh field (at most one table), so RECURSION_INPUT_VERSION goes to 5 (main's v4 is the layout without commit) and the statement/epoch tags to V5.
The constant-multiplicity guard for optional tables also accepts IS_B20 sends, same reasoning as ARE_BYTES.

…forgery harness

jotabulacios · 2026-10-15T14:16:42Z

/ai-review

github-actions · 2026-10-15T14:18:16Z

Codex Code Review

No actionable issues found in the PR diff. Reviewed statically for safety, correctness, significant performance issues, and dead code; no builds or tests run.

claude · 2026-10-15T14:18:35Z

Static review of the IS_WH table, the IS_WHH template and the KECCAK state_ptr move to DWordWHH. I found no correctness or security problems.

What I checked:

IS_WH bus: the receiver's word, value[1] + 2^16·value[2], has both halves IS_HALF-checked. So the KECCAK word_hi column is range-checked to 32 bits through the bus, and the ADD constraint ties the limbs to addr + 8·lane.
μ bound: the IS_B20[μ] send has multiplicity 1 and the same packing as the other IS_B20 senders. All-zero padding rows send IS_B20[0], which the collector counts. The MU_MAX split is correct and keeps rows sorted, so the trace is deterministic.
KECCAK: cond = MU is constrained to a bit (idx 51). Padding rows (μ = 0) gate every send.
Wiring and versions: TableCounts.is_wh is included in the statement absorb, the total, the at-most-one guard and the AIR/trace pairing. RECURSION_INPUT_VERSION and both domain tags are bumped. Bus ID 32 is new and does not collide.

One non-blocking comment, inline: is_wh_keys builds one key per lane for every call, and dedup_is_wh_rows runs twice over that list (once in the collector, once in trace generation). Deduplicating once and sharing the rows would cut memory and time on keccak-heavy runs, and is simpler.

Nit: lib.rs now reads "none of the nineteen optional chips carries…" — fine as-is.

Not covered: the PR branch wasn't checked out in the sandbox, so I reviewed from gh pr diff alone and could not read the surrounding code. I did not build or run the tests.

github-actions · 2026-10-15T14:29:51Z

AI Review

PR #1022 · 28 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

nicole-graus · 2026-10-16T19:02:10Z

/bench

github-actions · 2026-10-16T19:14:21Z

Benchmark — real block (`ethrex_mainnet_25368371.bin`) (median of 3)

_{continuations · epoch 2^22 · 8 epochs}

Metric	main	PR	Δ
Peak heap	46399 MB	47079 MB	+680 MB (+1.5%) ⚪
Prove time	101.718s	102.980s	+1.262s (+1.2%) ⚪

✅ No significant change.

_{Prove-time spread 1.6% (102.980s / 104.448s / 102.766s)}

_{Commit: 0a78672 · Baseline: built from main · Runner: self-hosted bench}

(lo = two halves, hi = the word). Needed for the KECCAK state_ptr.

and use them for the KECCAK state_ptr. IS_WH range checks the top 48 bits of an address, with one row per distinct (word, half) pair. Its multiplicity is bounded with IS_B20, as in down from 511 and 134. TableCounts gets an is_wh field, so RECURSION_INPUT_VERSION goes to 4 and the statement tags to V5.

… both the trace and the BITWISE collector, instead of deduplicating the full key list twice. Also fix two comments: the at-most-one check is not only for accelerators, and bus ID 29 was the EC_SCALAR ServeK bus, not an ECSM one.

… Word in an IS_WH row, and a KECCAK state_ptr resplit that keeps the ADD and the memory address but puts half_mid out of range. Each one fails if its IS_HALF send is removed. Also add IS_WH to the IR, OOD and GPU differential test lists, rename its MU_MAX to IS_WH_MU_MAX and pin it to the IS_B20 range, and fix the at_most_one comment: for IS_WH the count is what bounds the μ sum.

…a 64 KiB boundary (new test_keccak_64k program), a continuation run where only the keccak epoch ships IS_WH, and a recursion blob whose inner proof has IS_WH. The two IS_WH range forgeries now check that the bus balance is what rejects them, and the Word one gets its own control. Also add IS_WH to the GPU test list and fix a few stale bits: the TableCounts doc, KECCAK's interaction capacity, the debug bus legend (stopped at ID 21) and the no-accelerators test.

…ecutor tests, as its comment says, and have the two IS_WH forgery tests run the real verifier again next to the bus check.

jotabulacios · 2026-10-23T12:27:42Z

/ai-review

github-actions · 2026-10-23T12:28:48Z

Codex Code Review

No actionable issues found in the PR diff. Reviewed statically; no builds or tests were run.

claude · 2026-10-23T12:29:57Z

Reviewed statically. I found no blocking issues.

Checked and OK:

Bus payloads match. is_whh sends [word_hi, half_mid], and IS_WH receives [v1 + 2^16·v2, v0]. All three halves are range-checked with multiplicity μ, so word_hi < 2^32 holds. That is the assumption the from_dword_whh ADD carry needs for hi.
μ bound. IS_B20[μ] is sent with multiplicity 1, IS_WH_MU_MAX is the top BITWISE row (there is a test for this), and at_most_one caps the table count. Together these keep the per-key sum far below p. A row with μ = 0 receives nothing, so its unchecked halves can't be used.
Relaxed constant-multiplicity guard. The IS_B20 send uses Multiplicity::One, so padding rows do contribute. collect_bitwise_from_is_wh counts them with the same padded_rows as generate_is_wh_trace, and the table is never shipped present-but-empty. Both builders read the same is_wh_rows vector.
New table is wired in everywhere. AIR order matches trace order (air_trace_pairs and the refs list both put is_wh after hints). TableCounts, the statement absorb, the version/tag bumps and the exhaustive Traces destructures all include it.

One low-priority readability nit: state_addr.checked_add(lane * 8).expect("keccak state address range must be validated…") now appears three times: generate_keccak_trace, collect_bitwise_from_keccak and the new keccak::is_wh_keys. A small fn state_ptr(op, lane) -> u64 in keccak.rs would keep the trace, the BITWISE counts and the IS_WH keys from drifting apart.

Resolve the two conflicts with #984 (COPY replaces COMMIT): - trace_builder.rs BITWISE collectors: keep COPY's collector from main and this branch's KECCAK_RND padding count (keccak_rnd::padding_are_bytes). - skip_empty_tables_tests.rs: COMMIT left the optional-table list (17 tables); keep this branch's ARE_BYTES exemption imports.

- dvrm.rs / trace_builder.rs: DVRM's MSB16 and NEG ZERO lookups are counted once per row, so an op split at MU_MAX sends them once per row. - trace_builder.rs: KECCAK_RND no longer sends HWSL. - continuations_design.md: LT and MUL bound their own mu with a constant-1 ARE_BYTES send.

Brings in main's #984 (COPY replaces COMMIT) through #1016's branch. Conflicts resolved by keeping both sides: - TableCounts / statement / VmAirs / Traces: drop commit, keep is_wh and copy. - BusId: IS_WH = 32 next to COPY's CopyNext = 33. 32 was one of the two IDs main's comment listed as unused; 29 and 34 stay unused. - RECURSION_INPUT_VERSION 5 with a v5 note: main's v4 already means the layout without commit, so is_wh needs its own number. - Tests: counts 20 / 18 / 6, the accelerator test renamed to a_run_without_accelerators_omits_all_five_and_is_wh, COMMIT's omission tests dropped as on main, and main's committed-output test kept with this branch's "dropping ..." message style.

- lib.rs: eighteen optional chips, not nineteen (COMMIT left, IS_WH joined). - copy.rs: the prover now has an IS_WH table; COPY keeps four IS_HALF lookups where the spec uses IS_WHH, and moving them is a follow-up. - skip_empty_tables_tests.rs: the cap covers the five accelerators and IS_WH; COPY is among the always-present tables. - gpu_constraint_interp_real.rs: 27 tables. - continuations_design.md: validate() also caps IS_WH at one table, which is what bounds its multiplicity sum.

#1016 landed on main as 8e413a3, whose tree is identical to the branch head 647c6b8 already merged here, so this merge only joins the histories; the tree is unchanged.

Conflict: lib.rs, VmAirs::new builds both the IS_WH AIRs and the pinned REGISTER AIR. Changes the merge needs without a textual conflict: - cpu_start counts the IS_WH sub-proofs, which air_refs places after the accelerators and before the CPU tables; without it the verifier would read CPU heights one sub-proof early in every proof that ships IS_WH. The air_refs debug check and cpu_proof_start_matches_air_refs_layout (64 masks, is_wh included) follow. - is_wh_tests: VmAirs::new takes the CPU heights and the REGISTER commitment; the prover commits to its own trace.

nicole-graus added 16 commits October 2, 2026 16:35

Bound MUL/DVRM multiplicities and bit-constrain SHIFT zbs and μ

8e4b829

Bit-constrain LOAD μ

7c7e62a

Bound LT multiplicity

8580f42

Bound BRANCH multiplicity

5fec4bf

Fix clippy lints in tests

4dd1ee5

Bound table multiplicities with IS_BYTE instead of IS_HALFWORD

6eea7c2

Force is_negative to 0 on unsigned shift rows

3a5a3f4

Document why the multiplicity bound rides the ARE_BYTES bus

de098d6

Bit-constrain KECCAK and KECCAK_RND multiplicities

af6f14d

Fix stale test docs and rebalance forgery residue on ARE_BYTES

01f8f5e

Bound BYTEWISE multiplicity with IS_BYTE and keep EQ multiplicity a bit

2c1335d

Guard the BYTEWISE multiplicity collector against a zero row cap

a4b8083

Treat a prover refusal as inconclusive instead of a rejection in the …

cb19d79

…forgery harness

Range check multiplicities with ARE_BYTES sends as in spec

8e62f38

Align SHIFT and KECCAK_RND byte and bit checks with the spec

cc8a181

Add missing multiplicity tests, guard zero row caps and fix stale docs

a85946e

jotabulacios added this pull request to stack #1023 October 15, 2026 13:39

Reference the SIGN template in SHIFT is_negative comments

363b32c

jotabulacios force-pushed the feat/is-whh branch from d2834a8 to b82adaf Compare October 15, 2026 14:09

claude Bot reviewed Oct 15, 2026

View reviewed changes

Comment thread prover/src/tables/trace_builder.rs Outdated

nicole-graus added 3 commits October 15, 2026 11:36

Require padding-safe values in the #977 byte check exemption

d329077

Update the max rows width table and wrap a long SHIFT doc line

b8824bd

Share MU_MAX and the row dedup helper across the dedup tables

0ea6872

jotabulacios force-pushed the feat/is-whh branch from 3b11a2c to 6598fc9 Compare October 15, 2026 18:22

Describe the pre-fix BRANCH send in past tense

976c5e1

jotabulacios added 5 commits October 20, 2026 17:33

Add AddOperand::from_dword_whh so ADD can take a DWordWHH operand

f96f820

(lo = two halves, hi = the word). Needed for the KECCAK state_ptr.

jotabulacios force-pushed the feat/is-whh branch from 7839475 to 7dfe593 Compare October 20, 2026 20:33

Check the test_keccak_64k output against the zero-state KAT in the ex…

3f0ffb5

…ecutor tests, as its comment says, and have the two IS_WH forgery tests run the real verifier again next to the bus check.

MauroToscano added 4 commits October 23, 2026 14:52

Base automatically changed from fix/multiplicity-soundness to main October 23, 2026 19:01

MauroToscano approved these changes Oct 23, 2026

View reviewed changes

Merge main into feat/is-whh after #1016's squash

8222838

#1016 landed on main as 8e413a3, whose tree is identical to the branch head 647c6b8 already merged here, so this merge only joins the histories; the tree is unchanged.

MauroToscano added this pull request to the merge queue Oct 23, 2026

Merged via the queue into main with commit e70bde4 Oct 23, 2026
15 checks passed

MauroToscano deleted the feat/is-whh branch October 23, 2026 19:58

Navigation Menu

Repository navigation

Feat/is whh - #1022

Feat/is whh#1022
MauroToscano merged 32 commits into
mainfrom
feat/is-whh

jotabulacios commented Oct 15, 2026 •

edited by MauroToscano

Loading

Uh oh!

jotabulacios commented Oct 15, 2026

Uh oh!

github-actions Bot commented Oct 15, 2026

Uh oh!

Uh oh!

claude Bot commented Oct 15, 2026

Uh oh!

github-actions Bot commented Oct 15, 2026 •

edited

Loading

Uh oh!

nicole-graus commented Oct 16, 2026

Uh oh!

github-actions Bot commented Oct 16, 2026

Uh oh!

jotabulacios commented Oct 23, 2026

Uh oh!

github-actions Bot commented Oct 23, 2026

Uh oh!

claude Bot commented Oct 23, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

jotabulacios commented Oct 15, 2026 • edited by MauroToscano Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jotabulacios commented Oct 15, 2026

Uh oh!

github-actions Bot commented Oct 15, 2026

Codex Code Review

Uh oh!

Uh oh!

claude Bot commented Oct 15, 2026

Uh oh!

github-actions Bot commented Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

AI Review

Findings

Reviewer Lanes

Uh oh!

nicole-graus commented Oct 16, 2026

Uh oh!

github-actions Bot commented Oct 16, 2026

Benchmark — real block (ethrex_mainnet_25368371.bin) (median of 3)

Uh oh!

jotabulacios commented Oct 23, 2026

Uh oh!

github-actions Bot commented Oct 23, 2026

Codex Code Review

Uh oh!

claude Bot commented Oct 23, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jotabulacios commented Oct 15, 2026 •

edited by MauroToscano

Loading

github-actions Bot commented Oct 15, 2026 •

edited

Loading

Benchmark — real block (`ethrex_mainnet_25368371.bin`) (median of 3)