fix: RV64 completeness defects in DivRem/Weierstrass & revert RISCOF CI / chip tests (#108, #109) - #107
Merged
Merged
Conversation
Closes #108 and #109. Two one-sided completeness defects in the DivRem AIR: each can only make the prover reject an honest execution, never accept an invalid one. Together they are nine lines in one file and add no columns, so the embedded vk map is unaffected by this commit. Defect 1 (#108, DIVUW) -- the trace populates `quot_msb` and emits the matching `U16Range` byte event, but the AIR never evaluated the MSB gadget on the second limb of the quotient. Every word division therefore recorded one unpaired byte event. No constraint is violated, so it surfaces only at the very end as `verifier.rs:391 Regional cumulative sum is not zero`, with no chip name attached. Defect 2 (#109, REMUW) -- the `|remainder| == abs_remainder` check compared the sign-extended `remainder` instead of the zero-extended `remainder_comp`, so an unsigned word operation whose remainder has bit 31 set failed at `verifier.rs:384`. Defect 2 masks defect 1: `:384` is raised inside the per-chip loop while `:391` is only reached after it, so until defect 2 is fixed the defect-1 failure is invisible. Measured on the two issues' own reproducers, with nothing else applied: defect 1 only -> #108 reproducer passes; #109 fails :384 chip: DivRem defects 1 + 2 -> both reproducers pass Golden counts for the chip move 337/120 -> 339/121; the delta is entirely the newly evaluated MSB gadget. Defect 2 changes no counts.
A third completeness defect, independent of #108 and #109 and not needed to close them, but latent on any RV64 word division whose operand has bit 31 set. RV64 word operations read only the low 32 bits of their operands, so the upper 32 bits of the source register are whatever happened to be there. That is not a corner case: the RV64 ABI keeps 32-bit values sign-extended, so LLVM materialises `0xFFFF_FFFFu32` as `li -1` and the upper half is all ones. The DivRem chip stored only the *computational* operands -- the low 32 bits zero- or sign-extended according to the opcode -- and put those on the ALU bus. The CPU chip sends the raw register values. For an unsigned word operation with bit 31 set the two disagree in the upper limbs, the send and the receive never pair up, and the proof dies at `verifier.rs:391 Regional cumulative sum is not zero` -- again with no chip name, because nothing is actually violated. Fix: keep both forms. `b_raw`/`c_raw` hold what the CPU read and are what the bus now carries; `b`/`c` stay the computational form the arithmetic uses, and new constraints tie the two together (equal on the low limbs; on the high limbs either the raw value or the sign fill, selected by `is_word_operation`). The padding row is a non-word op, so it must satisfy `*_raw == *` on every limb. This adds 8 columns, which changes every DivRem vk digest -- the embedded vk map has to be rebuilt (done in a later commit on this branch). Golden counts for the chip move 339 -> 347 constraints (four limb pairs, two operands); lookups are unchanged.
A fourth completeness defect, in the Weierstrass decompress chips this time, with the same signature as the other unpaired-lookup bugs: the proof dies at `verifier.rs:391 Regional cumulative sum is not zero` with no chip named. The trace populates `y_access.prev_value_u8` and, in doing so, emits a u8 range check for every byte. The AIR only ran the u16->u8 conversion on `x_access`, so those `y_access` byte events had no matching evaluation and the byte table was over-received. Evaluating the conversion on `y_access` too pairs them up. The returned limbs are deliberately unused -- `y_access`'s value is already constrained against `sqrt_y`/`neg_y` further down -- so the call exists to balance the lookups and to pin the byte decomposition. It is a write access, hence the `write` helper, which reads `inner.prev_value` exactly as the trace did. Pure AIR change: no new columns, no trace change, so the vk digest moves only because the lookup set does. Golden lookups for the secp256k1 decompress chip move 658 -> 674: four `y_access` words, four u8 range checks each. Constraints are unchanged, because the conversion gadget only emits lookups.
…tion Two changes that make the vk map rebuild required by the previous commits cheaper to produce and cheaper to debug. (a) `program_heights` drops the 19 entry, cutting the enumerated shape count by 25% (403,014 -> 302,355) and so cutting the `build_vk_map` run by the same proportion. The old list is kept as a comment. This is not a correctness change. `find_shape_from_allowed_heights` scans the allowed heights in ascending order and takes the first one that fits, so a program that used to land on 19 now lands on 20 -- it pads up, it does not fail. Only removing the *largest* height can produce `PreprocessedShapeError`. Measured across the whole corpus, nothing needed 19 in the first place: every example ELF is under 37k instructions and lands on 18, while the reth ELF is 548,975 instructions and already needed 20 (2^19 is 524,288). The band between 2^18 and 2^19 is empty. The Merkle tree height is unaffected: it is `total_num.next_power_of_two().ilog2()` over the *deduplicated* shape count, and 302,355 still rounds up to 2^19. (b) When a vk is rejected, print the preprocessed shape and the map size instead of only the digest. The bare digest cannot distinguish the two causes that actually occur -- a map that is stale with respect to the circuit, versus a shape the config never enumerated -- and the message now names both, plus the `riscv_proofshape_map_*.bin` cache, which is keyed only on chip names and log heights and so will silently hand back pre-change digests if left in place across a rebuild.
The added DivRem columns and the changed DivRem/decompress lookup sets move
every affected vk digest, so the maps shipped in-tree no longer match the
circuit and `VK_VERIFICATION=true` would reject valid proofs outright.
Rebuilt from scratch on clean machines, once per field, with no
`riscv_proofshape_map_*.bin` cache present -- that cache is keyed only on chip
names and log heights, so leaving it in place would have silently reproduced
the old digests while still reporting success.
Total num of all shapes (after deduplication): 302355
for both fields, matching the shape count expected from the height-19 removal,
and still inside 2^19 so the Merkle tree height is unchanged.
Both maps were then exercised with `VK_VERIFICATION=true` end to end: the
eight DivRem corner ELFs and the decompress gate plus two controls on
KoalaBear, and a sample of the same on BabyBear -- the two maps are separate
build runs, so checking only one field would leave the other unverified.
NOTE for downstream consumers: vk indices come from a `BTreeSet` ordering over
the digests, so essentially every index shifts, not just the changed ones. Any
deployed on-chain verifier pinned to the previous `vk_root` needs to be
regenerated.
kaiwei-0
changed the title
This was referenced Jul 29, 2026
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
2 participants
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.
Closes #108. Closes #109.
Summary
This PR addresses RV64 completeness defects in
DivRemandWeierstrass decompresschips, and reverts changes of RISCOF CI and chip tests.What this fixes
Four completeness defects. Each one makes the prover reject an execution that is valid.
DIVW/DIVUW/REMW/REMUW)Regional cumulative sum is not zeroConstraint verification failed, chip: DivRemRegional cumulative sum is not zeroRegional cumulative sum is not zero