[quangvdao]

Summary

Reduces constraint (39), LookupOutput(t) = Σ_k Σ_T TableFlag_T(t) · InstructionRa(k,t) · T(k), to one entry lemma per lookup table, and proves 49 of the 55. The main theorem honestWitness_lookupOutputEqInstructionReadRaf has no sorry of its own. Its sorryAx comes only from the 6 shift/rotate lemmas (VirtualSRL, VirtualSRA, VirtualSRLW, VirtualSRAW, VirtualROTR, VirtualROTRW), which are false in the current model; kernel-checked counterexamples are included. The cause is a missing program-validity fact on the Lean side, not a Rust bug (details below).

Stacked on #14 (qvd/registers-34-36 @ 0d9fa22). Draft until the six lemmas are scoped: they need the program-validity fact, not more proof. constraints.md still lists (39) as TODO.

Rebased onto #18. This branch (via #14) is now rebased onto #18 (qvd/trace-assumptions @ a3e7aad0fec915b7a887e4a73aef7a70245f7ea1), which replaces the vacuous JoltTrace.allAssumptions field with TraceAssumptions. lake build JoltConstraints (3566 jobs) plus every Tests/ module (3505 jobs) pass, including LookupShiftMask.lean. The main theorem's sorryAx still comes only from the six shift/rotate lemmas.

One consequence: on the base, the main theorem was vacuously true despite the six false lemmas. After #18, I expect it to be false for arbitrary bytecode, because a trace can now reach a shift row with an improper mask. I have not built that full trace; Tests/TraceNonempty.lean in #18 shows how to construct one.

• Base: qvd/registers-34-36 @ 0d9fa22
• Head: qvd/lookup-39 @ b5483ab
• 2 commits, 8 files, +1676/−31

Commit	Content
213f222	The reduction, 47 table lemmas, the counterexamples
b5483ab	Pext and PextSigned, in the new LookupPextProofHelpers.lean

How the proof goes

Each step is an equality, so the constraint at a row fails exactly when that row's table lemma fails.

1. Address sum. instructionRead_honest collapses Σ_k InstructionRa(k,t) · T(k) to T at the honest lookup index.
2. Table sum. Finset.sum_ite_eq collapses the flag sum to the one flagged table.
3. No table. Rows with no lookup table (FENCE, LD, SD, VirtualHostIO) have output 0 by rowLookupOutput_eq_zero_of_lookupTable_none. Padding rows are handled separately in the main theorem.
4. Per table. lookupEntryCorrect_of_lookupTable matches on the table kind and calls the 55 lemmas lookupEntryCorrect_<Table> in LookupEntryProofHelpers.lean.

Per-table status

Status	Tables
Proved (49)	Pext, PextSigned; RangeCheck, RangeCheckAligned, And, Andn, Or, Xor; Equal, NotEqual, SignedLessThan, UnsignedLessThan, SignedGreaterThanEqual, UnsignedGreaterThanEqual, UnsignedLessThanEqual; SignMask, UpperWord, LowerHalfWord, SignExtendWord, VirtualNegateIf; Pow2, Pow2W, ShiftRightBitmask, ShiftRightBitmaskW; ShiftDataB/H/W, WindowMaskB/H/W, AlignAddr, VirtualRev8W; VirtualXORROTL1, VirtualXORROT32/24/16/63, VirtualXORROTW16/12/8/7/22/19/6; HalfwordAlignment, WordAlignment, MulUNoOverflow, ValidDiv0, ValidUnsignedRemainder
False for arbitrary bytecode (6)	VirtualSRL, VirtualSRA, VirtualSRLW, VirtualSRAW, VirtualROTR, VirtualROTRW

The assert tables (HalfwordAlignment through ValidUnsignedRemainder) get their condition from the row's successful execution (JoltTraceRow.executes).

Pext and PextSigned

LookupPextProofHelpers.lean proves pext_eq_jolt_virtual_pext_value and pextSigned_eq_jolt_virtual_pext_signed_value for all 64-bit operands. They relate the table functions in lookup_table.lean to the honest values from JoltBytecode/JoltISA/Values.lean.

• Contiguous fast path. The mask is 2^tz · n with n &&& (n+1) = 0, so jolt_pext_nat_two_pow_mul and jolt_pext_nat_of_low_ones reduce jolt_pext_nat 64 to (x >>> tz) &&& n. The case n = 2^64 − 1 (where n + 1 wraps) is covered.
• General loop. The forIn becomes a List.foldl of one step on (bits, k, out). The invariant after n passes is jolt_pext_nat 64 x y = out + 2^k · jolt_pext_nat 64 x bits, with out < 2^k, k ≤ n, and the low n bits of bits clear. So bits = 0 after 64 passes. jolt_pext_nat_peel handles one step: clearing the lowest set bit p of 2^p(2q+1) gives 2^(p+1)q.
• Sign extension. cpop equals jolt_popcount_nat 64. The extracted value is below 2^popcount (jolt_pext_nat_lt), and its bit popcount − 1 is x's bit at log2 y (jolt_pext_nat_testBit_top), which is the bit windowSignBit reads. So adding 2^64 − 2^popcount equals or-ing in ~~~(2^popcount − 1).

The six false lemmas

The shift and rotate tables read the right operand as a right-shift bitmask, with ones from bit s upward. They are correct only for such masks. The honest output shifts by ctz of whatever mask the row carries.

• Counterexample. Source 4 with mask 2 gives index interleaveLookupOperands 4 2 = 36. The table entry is 0 for the four shift tables and 4 for the two rotate tables. The honest output is 2 for all six.
• Zero mask. Register-form VirtualSRLW with mask 0 gives index 34, entry 0 and output 5. The earlier zero-mask fix covered jolt_virtual_srliw_value only.
• Row-level refutation. SRLICounterexample.not_lookupEntryCorrect is a one-row program VirtualSRLI v32, v33, 2. The row is accepted because OperandsRepresentable only asks 2 < 2^64, and LookupEntryCorrect fails whenever v33 = 4. I did not build a full JoltTrace refuting the main theorem, since that needs init_state, prepareSource and the linking obligations.

Why this is a Lean-side gap, not a Rust bug. Rust's to_lookup_output also uses trailing_zeros, e.g. crates/jolt-lookup-tables/src/instructions/virt/srlw.rs at a16z/jolt 754fc88. But Rust's expander only emits proper masks: they come from ShiftRightBitmask outputs, rotr64 and rotri32. Lean's JoltProgram.expandedBytecode is an arbitrary array (the FIXME on JoltProgram.rowValid, program.lean:173). These lemmas become provable once JoltProgram records how rows are produced, i.e. the source → row construction item.

One observation for the Rust side, not filed: the public helper inline.rs::rotri(rs1, imm, rd) would emit VirtualROTRI with any immediate. In-repo it is only called with proper masks.

Other changes

• instructionLookupChunk and instructionLookupRa move to the new InstructionLookupRa.lean, so the selection lemmas no longer import the constraint file.
• model_review.md: the (39) row names the helper file's FIXME.
• JoltConstraints/Tests/LookupShiftMask.lean holds the counterexamples. Like the other Tests/ files it is not in the default build; check it with lake env lean JoltConstraints/Tests/LookupShiftMask.lean. The randomized Pext comparison from the first commit is removed now that the theorems cover it.

Trust footprint

#print axioms honestWitness_lookupOutputEqInstructionReadRaf:

• Sail model axioms, as in the other constraint theorems: load_reservation, match_reservation, plat_term_write, sys_enable_experimental_extensions, plus propext, Classical.choice, Quot.sound.
• sorryAx: only through the 6 shift/rotate lemmas above.
• 215 bv_decide native axioms (*._native.bv_decide.ax_*): results of the compiled LRAT checker that the kernel does not re-check. The repo already relies on the same mechanism, e.g. StoreFamily/Splice.lean, but this PR adds many more. Reviewers may prefer these replaced by kernel proofs over time.
• Pext proofs: pext_eq_jolt_virtual_pext_value and pextSigned_eq_jolt_virtual_pext_signed_value use only propext, Classical.choice and Quot.sound. lookupEntryCorrect_Pext and lookupEntryCorrect_PextSigned have no sorryAx. Their 256 native axioms all come from the shared uninterleave_fst_getLsbD and uninterleave_snd_getLsbD.

Validation

At b5483ab:

• lake build JoltConstraints: 3566 jobs OK. The new sorry warnings are the 6 shift/rotate lemmas in LookupEntryProofHelpers.lean. LookupPextProofHelpers.lean compiles with no warnings.
• lake env lean JoltConstraints/Tests/LookupShiftMask.lean checks with no errors.
• #print axioms on the main theorem gives the list above: sorryAx plus the 215 native axioms.
• No maxHeartbeats changes. LookupEntryProofHelpers.lean takes about 45–70 s wall.

AI usage

Written with Claude Code. An agent drafted the reduction and the table lemmas; the build, axiom listing and counterexample checks were rerun separately before opening. The Pext proofs were written in this session and checked the same way.

🤖 Generated with Claude Code