[don't-merge] fix soundness and constraints for formal verification#101
Open
eason1981 wants to merge 12 commits into
Open
[don't-merge] fix soundness and constraints for formal verification#101eason1981 wants to merge 12 commits into
eason1981 wants to merge 12 commits into
Conversation
- LT: assert a[0] equals lt_signed.result.bit (previously unconstrained) - SR: constrain a[0]/a[1] for SRLW/SRAW (replaces TODO at line 188); use higher_limb[1] for the MSB-carrying limb to avoid including sign-extended upper limbs from limb_result - SLL: bool-check shift_u16 and tie to c_bits[4..6] for SLL/SLLW - Add unit tests covering signed comparison and word cross-boundary shift - Add proposals/nethermind-alu-constraint-fixes.md
eason1981
changed the title
added 2 commits
May 20, 2026 19:32
RISC-V requires JALR to set next_pc = (rs1 + imm) & !1. Previously the
constraint only verified next_pc = rs1 + imm (no masking), and the ALU
trace event used the unmasked sum as `a` while the CPU column used the
masked emulator value — making the proof inconsistent for odd-sum targets.
Adds jalr_lsb witness column and two new constraints:
- jalr_lsb ∈ {0, 1}
- next_pc[0] * inv(2) passes u16 range check (proves next_pc is even)
- ALU ADD lookup now verifies rs1 + imm = next_pc + jalr_lsb
Trace populates jalr_lsb = (rs1 + imm) & 1 and emits the range check
event for next_pc[0] / 2.
LtWordU16Gadget::eval only verifies consistency of the `bit` witness with the comparison limbs — it does not assert that bit = 1 (i.e. that abs(remainder) < max(abs(c), 1) actually holds). A malicious prover could set bit = 0 and supply an invalid remainder >= divisor while satisfying all existing constraints. Add the missing assertion after the gadget eval, gated on remainder_check_multiplicity (= is_real * (1 - is_c_0)), matching SP1's implementation.
|
These all appear correct to me. |
added 9 commits
May 22, 2026 09:48
For DIVW/REMW/DIVUW/REMUW, quot_msb.msb is used to sign-extend the quotient's upper limbs (limbs 2-3) via: quotient[i] = quot_msb.msb * 0xFFFF (i = 2, 3) However, U16MSBGadget::eval was never called for quot_msb, leaving it as a free witness. A prover could set quot_msb.msb arbitrarily and forge the sign extension of the quotient. Add quot_msb to msb_pairs_word so that U16MSBGadget ties quot_msb.msb to the actual MSB of quotient[WORD_SIZE/2-1] (bit 31 of the 32-bit quotient), matching how b_msb, c_msb, and rem_msb are handled.
… constraints For DIVW/REMW/DIVUW/REMUW, constrain c[2] and c[3] to be the proper sign/zero extension of c[1]. Without this, a prover can set c[2] != 0 while c[0]=c[1]=0, making is_c_0 false while the actual 32-bit divisor is zero, bypassing the division-by-zero special case.
… constraints Without constraining b[2]/b[3] for DIVW/REMW/DIVUW/REMUW, a malicious prover can pick a large quotient q such that c×q overflows into b[2]/b[3], satisfying c×q+r=b with an incorrect quotient. The upper MulGadget is disabled for word ops so it provides no protection. This fix adds b alongside the existing c constraint.
Bug 1: the lower/higher limb decomposition of each b[i] was range-checked but never tied back to b[i] itself. A malicious prover could pick any range-valid (lower_limb[i], higher_limb[i]) pair independent of the actual b[i], producing an arbitrary shift result. Fix: add the carry equation b[i] * v_0123 = higher_limb[i] * 2^16 + lower_limb[i] * v_0123 (same pattern as the SLL chip, constraints 21-24). Bug 2: scalar column c (used for shift amount computation via c_bits/v_0123) and Word column c_for_lookup (used in the CPU multiset lookup) were disconnected -- no constraint required them to agree. A malicious prover could shift by c while passing off c_for_lookup to the CPU, writing a wrong result to the destination register. Fix: assert_eq(c, c_for_lookup[0]).
…_memory_access addr_aligned was an unconstrained witness column (4×u16 limbs) passed to eval_memory_access for the State-bus/Memory-bus Regional lookup. No constraint bound it to addr_word or offset_bit, so a malicious prover could supply an arbitrary aligned address, making the two buses reference different 8-byte regions while satisfying all existing constraints. Fix: delete addr_aligned column and compute the aligned address inline as [addr_word[0] - offset_sum, addr_word[1], addr_word[2]], where offset_sum is already constrained by the BitRange check in C2. This eliminates the free witness and closes the soundness gap without adding any new constraints.
When op_a_0 = 1 (rd = x0), both mem_value_is_neg_not_x0 and mem_value_is_pos_not_x0 collapse to zero, making all sign/zero-extension fill constraints vacuous. op_a_val[0..3] was unconstrained, allowing a prover to set values exceeding the u16 bound required by the Memory bus. Fix: add op_a_0 * op_a_val[i] = 0 for i in 0..4. When op_a_0 = 1 this pins each limb to zero; when op_a_0 = 0 the constraint is vacuous and the existing fill constraints remain in charge.
For LB/LBU, selected_limb is split into two bytes via selected_limb_low_byte and (selected_limb - selected_limb_low_byte)*inv_256. Only selected_limb_low_byte was range-checked; the high byte was unconstrained. A malicious prover could supply a fake selected_limb_low_byte that makes the high byte an arbitrary field element (~2.13e9), breaking the u8 bound on selected_byte and the LBU zero-extension equation. Fix: replace slice_range_check_u8 with looking_rangecheck(U8Range, ..., selected_limb_low_byte, high_byte, ...) to force both bytes into [0, 255], mirroring the pattern already used by SB. Update traces accordingly.
… Word op_b_access and op_c_access were typed as MemoryReadCols which carries five unused fields (prev_chunk, prev_clk, compare_clk, diff_16bit_limb, diff_8bit_limb) beyond the actual value. None of these fields were constrained or accessed anywhere — only op_b_val()/op_c_val() were used, which returned the inner value Word. Replace both fields with plain Word<T> and update the populate method and helpers accordingly, removing 18 unused witness columns.
This reverts commit 7860af1.
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.
Summary
a[0]was not constrained to equallt_signed.result.bit, leaving the output unconstrained in the signed comparison patha[0]/a[1]forSRLW/SRAWwere previously unconstrained (TODO comment); now correctly derived fromlimb_resultandhigher_limb[1](the MSB-carrying limb), avoiding sign-extended upper limbslower_limb[i]/higher_limb[i]were range-checked but never tied back tob[i]; a prover could pick any range-valid limb pair independent of the actual input, producing an arbitrary shift resultc(used for shift amount viac_bits/v_0123) andc_for_lookup(used in the CPU multiset lookup) were disconnected; a prover could shift bycwhile passing off a differentc_for_lookupto the CPU, writing a wrong result to the destination registershift_u16was not bool-checked and not tied toc_bits[4..6]forSLL/SLLW, allowing a malicious prover to set an arbitrary shift indexLtWordU16Gadget::evalonly verifies consistency of thebitwitness — it does not assertbit = 1; a malicious prover could supplyremainder >= divisorwhile satisfying all existing constraintsquot_msbwas never passed toU16MSBGadget::eval, leaving it as a free witness; a prover could forge the sign extension of the quotient's upper limbs in word operationsc(c[2],c[3]) were unconstrained in word operations; a prover could setc[2] != 0whilec[0]=c[1]=0, makingis_c_0false and bypassing the division-by-zero special caseb(b[2],b[3]) were unconstrained in word operations; a prover could pick a large quotient such thatc×qoverflows intob[2]/b[3], satisfyingc×q+r=bwith an incorrect quotientaddr_alignedwas a free witness not derived fromaddr; replaced with an inline computation ineval_memory_access, removing the free columnselected_limb_low_bytewas range-checked; the high byte was unconstrained, allowing a prover to break the u8 bound onselected_byte; both bytes are now range-checked togetherop_b_access/op_c_accesswere typed asMemoryReadColscarrying five unused witness columns; replaced with plainWord<T>, removing 18 dead witness columns