diff --git a/JoltConstraints/Constraints/InstructionLookupRa.lean b/JoltConstraints/Constraints/InstructionLookupRa.lean
new file mode 100644
index 0000000..0996581
--- /dev/null
+++ b/JoltConstraints/Constraints/InstructionLookupRa.lean
@@ -0,0 +1,29 @@
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.Field.Defs
+import JoltConstraints.witness
+import JoltConstraints.lookup_table
+import JoltConstraints.honest_witness
+
+set_option autoImplicit false
+
+namespace JoltConstraints
+
+open scoped BigOperators
+
+/-- The `chunk`th virtual chunk of a 128-bit lookup address, most significant first. -/
+def instructionLookupChunk (params : WitnessParams) (address : Fin (2 ^ 128))
+    (chunk : Fin params.virtualInstructionChunks) : Fin (2 ^ params.virtualChunkBits) :=
+  ⟨(address.val /
+      2 ^ ((params.virtualInstructionChunks - 1 - chunk.val) * params.virtualChunkBits)) %
+      2 ^ params.virtualChunkBits,
+    Nat.mod_lt _ (pow_pos (by decide : 0 < (2 : Nat)) _)⟩
+
+/-- `LookupRa(x,t)` in `constraints.md`: multiply the virtual instruction-address
+entries selected by the chunks of `x`. -/
+noncomputable def instructionLookupRa {F : Type} [Field F] {params : WitnessParams}
+    (witness : WitnessType F params) (address : Fin (2 ^ 128))
+    (t : Fin params.traceLength) : F :=
+  ∏ chunk : Fin params.virtualInstructionChunks,
+    witness.InstructionRa chunk (instructionLookupChunk params address chunk) t
+
+end JoltConstraints
diff --git a/JoltConstraints/Constraints/InstructionReadSelection.lean b/JoltConstraints/Constraints/InstructionReadSelection.lean
index a67b071..ae24c11 100644
--- a/JoltConstraints/Constraints/InstructionReadSelection.lean
+++ b/JoltConstraints/Constraints/InstructionReadSelection.lean
@@ -1,4 +1,4 @@
-import JoltConstraints.Constraints.LookupOutputEqInstructionReadRaf
+import JoltConstraints.Constraints.InstructionLookupRa
 
 set_option autoImplicit false
 
diff --git a/JoltConstraints/Constraints/LookupEntryProofHelpers.lean b/JoltConstraints/Constraints/LookupEntryProofHelpers.lean
new file mode 100644
index 0000000..73720d6
--- /dev/null
+++ b/JoltConstraints/Constraints/LookupEntryProofHelpers.lean
@@ -0,0 +1,1050 @@
+import JoltConstraints.Constraints.LookupOperandData
+import JoltConstraints.Constraints.LookupWriteProofHelpers
+import JoltConstraints.Constraints.LookupPextProofHelpers
+
+/-!
+# Per-table obligations for constraint (39)
+
+Constraint (39) says that on an execution row the lookup output equals the
+selected table entry at the honest lookup address. After the address sum and the
+table sum are collapsed (see `LookupOutputEqInstructionReadRaf.lean`), what is
+left is one obligation per `LookupTableKind`:
+
+  lookupTableEntry k (rowLookupAddress row) = rowLookupOutput row
+
+whenever the row's instruction uses table `k`. This file states that obligation
+as `LookupEntryCorrect` and proves it table by table as
+`lookupEntryCorrect_<Table>`. `lookupEntryCorrect_of_lookupTable` dispatches on
+the table.
+-/
+
+set_option autoImplicit false
+
+namespace JoltConstraints
+
+open HonestWitness
+open Sail PreSail LeanRV64D.Functions
+
+/-- The expanded instruction executed by a trace row. -/
+abbrev rowInstruction {program : JoltProgram} (row : JoltTraceRow program) : JoltISA.Instr :=
+  (getElem program.expandedBytecode row.rowIndex.val row.rowIndex.isLt).expandedInstruction
+
+/-- The honest 128-bit lookup index of an execution row. -/
+noncomputable def rowLookupIndex {program : JoltProgram} (row : JoltTraceRow program) :
+    BitVec 128 :=
+  let bc := getElem program.expandedBytecode row.rowIndex.val row.rowIndex.isLt
+  instructionLookupIndex bc.expandedInstruction bc.address row.preState row.postState
+
+/-- The honest lookup index as a table address. -/
+noncomputable def rowLookupAddress {program : JoltProgram} (row : JoltTraceRow program) :
+    Fin (2 ^ 128) :=
+  (rowLookupIndex row).toFin
+
+/-- The per-table obligation of constraint (39): table `table` at the honest
+address is the honest lookup output. -/
+def LookupEntryCorrect (F : Type) [Field F] {program : JoltProgram}
+    (table : LookupTableKind) (row : JoltTraceRow program) : Prop :=
+  lookupTableEntry (F := F) table (rowLookupAddress row) = ((rowLookupOutput row).toNat : F)
+
+/-! ## Uninterleaving -/
+
+theorem uninterleave_fst_getLsbD (v : BitVec 128) (i : Nat) (hi : i < 64) :
+    (uninterleave v.toFin).1.getLsbD i = v.getLsbD (2 * i + 1) := by
+  interval_cases i <;> (simp only [uninterleave, BitVec.ofFin_toFin]; bv_decide)
+
+theorem uninterleave_snd_getLsbD (v : BitVec 128) (i : Nat) (hi : i < 64) :
+    (uninterleave v.toFin).2.getLsbD i = v.getLsbD (2 * i) := by
+  interval_cases i <;> (simp only [uninterleave, BitVec.ofFin_toFin]; bv_decide)
+
+theorem uninterleave_interleave (l r : BitVec 64) :
+    uninterleave (interleaveLookupOperands l r).toFin = (l, r) := by
+  ext i hi
+  · rw [← BitVec.getLsbD_eq_getElem, ← BitVec.getLsbD_eq_getElem,
+      uninterleave_fst_getLsbD _ i hi, BitVec.getLsbD,
+      interleaveLookupOperands_testBit l r (by omega)]
+    have h1 : (2 * i + 1) % 2 = 1 := by omega
+    have h2 : (2 * i + 1) / 2 = i := by omega
+    simp only [h1, h2, ↓reduceIte]
+  · rw [← BitVec.getLsbD_eq_getElem, ← BitVec.getLsbD_eq_getElem,
+      uninterleave_snd_getLsbD _ i hi, BitVec.getLsbD,
+      interleaveLookupOperands_testBit l r (by omega)]
+    have h1 : 2 * i % 2 = 0 := by omega
+    have h2 : 2 * i / 2 = i := by omega
+    simp only [h1, h2, Nat.zero_ne_one, ↓reduceIte]
+
+/-! ## Wide arithmetic as bit-vector arithmetic -/
+
+theorem ofNat128_addWide (x y : BitVec 64) :
+    BitVec.ofNat 128 (JoltISA.addWide x y) = x.setWidth 128 + y.setWidth 128 := by
+  apply BitVec.eq_of_toNat_eq
+  have hx := x.isLt; have hy := y.isLt
+  simp only [JoltISA.addWide, BitVec.toNat_ofNat, BitVec.toNat_add, BitVec.toNat_setWidth]
+  omega
+
+theorem ofNat64_addWide (x y : BitVec 64) :
+    BitVec.ofNat 64 (JoltISA.addWide x y) = x + y := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [JoltISA.addWide, BitVec.toNat_ofNat, BitVec.toNat_add]
+
+theorem ofNat128_mulWide (x y : BitVec 64) :
+    BitVec.ofNat 128 (JoltISA.mulWide x y) = x.setWidth 128 * y.setWidth 128 := by
+  apply BitVec.eq_of_toNat_eq
+  have hx := x.isLt; have hy := y.isLt
+  have hxy : x.toNat * y.toNat < 2 ^ 128 := by
+    calc x.toNat * y.toNat < 2 ^ 64 * 2 ^ 64 := Nat.mul_lt_mul'' hx hy
+      _ = 2 ^ 128 := by norm_num
+  simp only [JoltISA.mulWide, BitVec.toNat_ofNat, BitVec.toNat_mul, BitVec.toNat_setWidth]
+  rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega), Nat.mod_eq_of_lt (a := y.toNat) (by omega),
+    Nat.mod_eq_of_lt hxy]
+
+/-! ## Table entries at honest addresses -/
+
+section entries
+variable {F : Type} [Field F]
+
+theorem rangeCheck_entry (v : BitVec 128) :
+    rangeCheckTableEntry (F := F) v.toFin = ((v.setWidth 64).toNat : F) := by
+  unfold rangeCheckTableEntry
+  have h : (v &&& ((1#128 <<< 64) - 1)).setWidth 64 = v.setWidth 64 := by bv_decide
+  simp only [BitVec.ofFin_toFin, h]
+
+theorem interleave_testBit_odd (l r : BitVec 64) (i : Nat) (hi : i < 64) :
+    (interleaveLookupOperands l r).toNat.testBit (2 * i + 1) = l.getLsbD i := by
+  rw [interleaveLookupOperands_testBit l r (by omega)]
+  have h1 : (2 * i + 1) % 2 = 1 := by omega
+  have h2 : (2 * i + 1) / 2 = i := by omega
+  simp only [h1, h2, ↓reduceIte]
+
+theorem interleave_testBit_even (l r : BitVec 64) (i : Nat) (hi : i < 64) :
+    (interleaveLookupOperands l r).toNat.testBit (2 * i) = r.getLsbD i := by
+  rw [interleaveLookupOperands_testBit l r (by omega)]
+  have h1 : 2 * i % 2 = 0 := by omega
+  have h2 : 2 * i / 2 = i := by omega
+  simp only [h1, h2, Nat.zero_ne_one, ↓reduceIte]
+
+theorem and_entry (l r : BitVec 64) :
+    andTableEntry (F := F) (interleaveLookupOperands l r).toFin = ((l &&& r).toNat : F) := by
+  rw [bitVec_toNat_cast_eq_sum]
+  unfold andTableEntry
+  refine Finset.sum_congr rfl fun i _ => ?_
+  simp only [BitVec.val_toFin, interleave_testBit_odd l r i i.isLt,
+    interleave_testBit_even l r i i.isLt, BitVec.getLsbD_and]
+
+theorem or_entry (l r : BitVec 64) :
+    orTableEntry (F := F) (interleaveLookupOperands l r).toFin = ((l ||| r).toNat : F) := by
+  rw [bitVec_toNat_cast_eq_sum]
+  unfold orTableEntry
+  refine Finset.sum_congr rfl fun i _ => ?_
+  simp only [BitVec.val_toFin, interleave_testBit_odd l r i i.isLt,
+    interleave_testBit_even l r i i.isLt, BitVec.getLsbD_or]
+
+theorem xor_entry (l r : BitVec 64) :
+    xorTableEntry (F := F) (interleaveLookupOperands l r).toFin = ((l ^^^ r).toNat : F) := by
+  rw [bitVec_toNat_cast_eq_sum]
+  unfold xorTableEntry
+  refine Finset.sum_congr rfl fun i _ => ?_
+  simp only [BitVec.val_toFin, interleave_testBit_odd l r i i.isLt,
+    interleave_testBit_even l r i i.isLt, BitVec.getLsbD_xor, bne]
+
+theorem andn_entry (l r : BitVec 64) :
+    andnTableEntry (F := F) (interleaveLookupOperands l r).toFin = ((l &&& ~~~r).toNat : F) := by
+  simp only [andnTableEntry, uninterleave_interleave]
+
+theorem equal_entry (l r : BitVec 64) :
+    equalTableEntry (F := F) (interleaveLookupOperands l r).toFin = if l = r then 1 else 0 := by
+  simp only [equalTableEntry, uninterleave_interleave]
+
+theorem notEqual_entry (l r : BitVec 64) :
+    notEqualTableEntry (F := F) (interleaveLookupOperands l r).toFin = if l ≠ r then 1 else 0 := by
+  simp only [notEqualTableEntry, uninterleave_interleave]
+
+theorem unsignedLessThan_entry (l r : BitVec 64) :
+    unsignedLessThanTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l < r then 1 else 0 := by
+  simp only [unsignedLessThanTableEntry, uninterleave_interleave]
+
+theorem unsignedLessThanEqual_entry (l r : BitVec 64) :
+    unsignedLessThanEqualTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l ≤ r then 1 else 0 := by
+  simp only [unsignedLessThanEqualTableEntry, uninterleave_interleave]
+
+theorem unsignedGreaterThanEqual_entry (l r : BitVec 64) :
+    unsignedGreaterThanEqualTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l ≥ r then 1 else 0 := by
+  simp only [unsignedGreaterThanEqualTableEntry, uninterleave_interleave]
+
+theorem signedLessThan_entry (l r : BitVec 64) :
+    signedLessThanTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l.toInt < r.toInt then 1 else 0 := by
+  simp only [signedLessThanTableEntry, uninterleave_interleave]
+
+theorem signedGreaterThanEqual_entry (l r : BitVec 64) :
+    signedGreaterThanEqualTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l.toInt ≥ r.toInt then 1 else 0 := by
+  simp only [signedGreaterThanEqualTableEntry, uninterleave_interleave]
+
+theorem validDiv0_entry (l r : BitVec 64) :
+    validDiv0TableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if l = 0 ∧ r ≠ -1 then 0 else 1 := by
+  have hmax : ((1#128 <<< 64) - 1).setWidth 64 = (-1 : BitVec 64) := by decide
+  simp only [validDiv0TableEntry, uninterleave_interleave, hmax]
+  split_ifs <;> simp_all
+
+theorem validUnsignedRemainder_entry (l r : BitVec 64) :
+    validUnsignedRemainderTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      if r = 0 ∨ l < r then 1 else 0 := by
+  simp only [validUnsignedRemainderTableEntry, uninterleave_interleave]
+
+theorem signMask_entry (l r : BitVec 64) :
+    signMaskTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((if l.msb then (-1 : BitVec 64) else 0).toNat : F) := by
+  unfold signMaskTableEntry
+  have hbit : (interleaveLookupOperands l r &&& 1#128 <<< 127 ≠ 0) = (l.msb = true) := by
+    have h127 := interleave_testBit_odd l r 63 (by omega)
+    have hiff : ∀ v : BitVec 128, (v &&& 1#128 <<< 127 ≠ 0) ↔ v.getLsbD 127 = true := by
+      intro v; bv_decide
+    rw [hiff, BitVec.getLsbD, h127, BitVec.msb_eq_getLsbD_last]
+  have hones : ((1#128 <<< 64) - 1).setWidth 64 = (-1 : BitVec 64) := by decide
+  simp only [BitVec.ofFin_toFin, hbit, hones]
+  split <;> simp
+
+theorem cast_ite_one_zero (c : Prop) [Decidable c] :
+    (((if c then (1 : BitVec 64) else 0).toNat : F)) = if c then 1 else 0 := by
+  split <;> simp
+
+end entries
+
+theorem jolt_slt_value_eq (x y : BitVec 64) :
+    jolt_slt_value x y = if x.toInt < y.toInt then 1 else 0 := by
+  unfold jolt_slt_value zopz0zI_s bool_to_bit bool_bit_forwards zero_extend Sail.BitVec.zeroExtend
+  by_cases hc : x.toInt < y.toInt <;> simp [hc]
+
+theorem toNatInt_lt (x y : BitVec 64) : (BitVec.toNatInt x < BitVec.toNatInt y) ↔ x < y := by
+  simp [BitVec.toNatInt, BitVec.lt_def]
+
+theorem toNatInt_ge (x y : BitVec 64) : (BitVec.toNatInt x ≥ BitVec.toNatInt y) ↔ x ≥ y := by
+  simp [BitVec.toNatInt, BitVec.le_def]
+
+theorem jolt_sltu_value_eq (x y : BitVec 64) :
+    jolt_sltu_value x y = if x < y then 1 else 0 := by
+  unfold jolt_sltu_value zopz0zI_u bool_to_bit bool_bit_forwards zero_extend Sail.BitVec.zeroExtend
+  by_cases hc : x < y <;> simp [hc, toNatInt_lt]
+
+
+theorem row_executes_exists {program : JoltProgram} (row : JoltTraceRow program) :
+    ∃ advice : (rowInstruction row).RuntimeAdvice,
+      JoltISA.execInstr ((rowInstruction row).withRuntimeAdvice advice) row.preState =
+        .ok (.Retire_Success ()) row.postState :=
+  ⟨row.runtimeAdvice, row.executes⟩
+
+theorem upper_zero_of_lt (n : Nat) (h : n < 2 ^ 64) : BitVec.ofNat 128 n >>> 64 = 0 := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [BitVec.toNat_ushiftRight, BitVec.toNat_ofNat, Nat.shiftRight_eq_div_pow]
+  rw [Nat.mod_eq_of_lt (by omega), Nat.div_eq_of_lt h]
+  rfl
+
+/-! ## Per-table obligations -/
+
+section tables
+variable {F : Type} [Field F] {program : JoltProgram}
+
+set_option hygiene false in
+/-- Split on the row instruction, keep the instructions that use the table, and
+unfold the index, output and table definitions. -/
+macro "lookup_cases" : tactic => `(tactic| (
+  unfold LookupEntryCorrect rowLookupAddress rowLookupIndex
+  cases hi : rowInstruction row <;>
+    simp only [hi, JoltMetadata.lookupTable, reduceCtorEq, Option.some.injEq] at h <;>
+    simp only [lookupTableEntry, rowLookupOutput, instructionLookupIndex, hi]))
+
+theorem lookupEntryCorrect_RangeCheck (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .RangeCheck) :
+    LookupEntryCorrect F .RangeCheck row := by
+  lookup_cases
+  all_goals simp only [rangeCheck_entry]
+  all_goals simp [ BitVec.setWidth_ofNat_of_le, BitVec.setWidth_setWidth_of_le,
+    jolt_virtual_muli_value]
+
+theorem lookupEntryCorrect_And (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .And) :
+    LookupEntryCorrect F .And row := by
+  lookup_cases
+  all_goals simp only [and_entry, Riscv.andi]
+
+theorem lookupEntryCorrect_Or (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Or) :
+    LookupEntryCorrect F .Or row := by
+  lookup_cases
+  all_goals simp only [or_entry, Riscv.ori]
+
+theorem lookupEntryCorrect_Xor (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Xor) :
+    LookupEntryCorrect F .Xor row := by
+  lookup_cases
+  all_goals simp only [xor_entry, jolt_xor_value]
+
+theorem lookupEntryCorrect_Andn (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Andn) :
+    LookupEntryCorrect F .Andn row := by
+  lookup_cases
+  all_goals simp only [andn_entry, jolt_andn_value]
+
+theorem lookupEntryCorrect_SignedLessThan (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .SignedLessThan) :
+    LookupEntryCorrect F .SignedLessThan row := by
+  lookup_cases
+  all_goals simp only [signedLessThan_entry, jolt_slt_value_eq, cast_ite_one_zero,
+    JoltISA.branchDecisionPure, zopz0zI_s, decide_eq_true_eq]
+
+theorem lookupEntryCorrect_UnsignedLessThan (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .UnsignedLessThan) :
+    LookupEntryCorrect F .UnsignedLessThan row := by
+  lookup_cases
+  all_goals simp only [unsignedLessThan_entry, jolt_sltu_value_eq, cast_ite_one_zero,
+    JoltISA.branchDecisionPure, zopz0zI_u, decide_eq_true_eq, toNatInt_lt]
+
+theorem lookupEntryCorrect_SignedGreaterThanEqual (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .SignedGreaterThanEqual) :
+    LookupEntryCorrect F .SignedGreaterThanEqual row := by
+  lookup_cases
+  all_goals simp only [signedGreaterThanEqual_entry, cast_ite_one_zero,
+    JoltISA.branchDecisionPure, zopz0zKzJ_s, decide_eq_true_eq]
+
+theorem lookupEntryCorrect_UnsignedGreaterThanEqual (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .UnsignedGreaterThanEqual) :
+    LookupEntryCorrect F .UnsignedGreaterThanEqual row := by
+  lookup_cases
+  all_goals simp only [unsignedGreaterThanEqual_entry, cast_ite_one_zero,
+    JoltISA.branchDecisionPure, zopz0zKzJ_u, decide_eq_true_eq, toNatInt_ge]
+
+theorem lookupEntryCorrect_Equal (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Equal) :
+    LookupEntryCorrect F .Equal row := by
+  lookup_cases
+  all_goals simp only [equal_entry, cast_ite_one_zero, JoltISA.branchDecisionPure,
+    beq_iff_eq, jolt_assert_eq]
+
+theorem lookupEntryCorrect_NotEqual (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .NotEqual) :
+    LookupEntryCorrect F .NotEqual row := by
+  lookup_cases
+  all_goals simp only [notEqual_entry, cast_ite_one_zero, JoltISA.branchDecisionPure,
+    bne_iff_ne, ne_eq]
+
+end tables
+
+section entries2
+variable {F : Type} [Field F]
+
+theorem signExtendWord_entry (v : BitVec 128) :
+    signExtendWordTableEntry (F := F) v.toFin =
+      (((v.setWidth 32).signExtend 64).toNat : F) := by
+  unfold signExtendWordTableEntry
+  simp only [BitVec.ofFin_toFin]
+  split
+  · rename_i hs
+    congr 2
+    bv_decide
+  · rename_i hs
+    congr 2
+    bv_decide
+
+theorem upperWord_entry (n : Nat) (hn : n < 2 ^ 128) :
+    upperWordTableEntry (F := F) (BitVec.ofNat 128 n).toFin =
+      ((BitVec.ofNat 64 (n / 2 ^ 64)).toNat : F) := by
+  unfold upperWordTableEntry
+  simp only [BitVec.ofFin_toFin]
+  congr 2
+  apply BitVec.eq_of_toNat_eq
+  simp only [BitVec.toNat_setWidth, BitVec.toNat_ushiftRight, BitVec.toNat_ofNat,
+    Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt hn]
+
+theorem lowerHalfWord_entry (v : BitVec 128) :
+    lowerHalfWordTableEntry (F := F) v.toFin = (((v.setWidth 32).setWidth 64).toNat : F) := by
+  unfold lowerHalfWordTableEntry
+  simp only [BitVec.ofFin_toFin]
+  congr 2
+  bv_decide
+
+theorem rangeCheckAligned_entry (v : BitVec 128) :
+    rangeCheckAlignedTableEntry (F := F) v.toFin =
+      ((v.setWidth 64 &&& ~~~1#64).toNat : F) := by
+  unfold rangeCheckAlignedTableEntry
+  have h : (v &&& ((1#128 <<< 64) - 1)).setWidth 64 = v.setWidth 64 := by bv_decide
+  simp only [BitVec.ofFin_toFin, h]
+
+theorem alignAddr_entry (v : BitVec 128) :
+    alignAddrTableEntry (F := F) v.toFin =
+      ((v.setWidth 64 &&& ~~~7#64).toNat : F) := by
+  unfold alignAddrTableEntry
+  have h : (v &&& ((1#128 <<< 64) - 1)).setWidth 64 = v.setWidth 64 := by bv_decide
+  simp only [BitVec.ofFin_toFin, h]
+
+theorem umod_toNat (v : BitVec 128) (m : Nat) (hm : m < 2 ^ 128) :
+    (v % BitVec.ofNat 128 m).toNat = v.toNat % m := by
+  simp only [BitVec.toNat_umod, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hm]
+
+theorem one_shiftLeft_eq (k : Nat) : 1#64 <<< k = BitVec.ofNat 64 (2 ^ k) := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [BitVec.toNat_shiftLeft, BitVec.toNat_ofNat, Nat.shiftLeft_eq]
+  norm_num
+
+theorem pow2_entry (v : BitVec 128) :
+    pow2TableEntry (F := F) v.toFin = ((BitVec.ofNat 64 (2 ^ (v.toNat % 64))).toNat : F) := by
+  unfold pow2TableEntry
+  simp only [BitVec.ofFin_toFin, one_shiftLeft_eq]
+  rw [show (64 : BitVec 128) = BitVec.ofNat 128 64 from rfl, umod_toNat _ _ (by norm_num)]
+
+theorem pow2W_entry (v : BitVec 128) :
+    pow2WTableEntry (F := F) v.toFin = ((BitVec.ofNat 64 (2 ^ (v.toNat % 32))).toNat : F) := by
+  unfold pow2WTableEntry
+  simp only [BitVec.ofFin_toFin, one_shiftLeft_eq]
+  rw [show (32 : BitVec 128) = BitVec.ofNat 128 32 from rfl, umod_toNat _ _ (by norm_num)]
+
+theorem shiftRightBitmask_value (s : Nat) (hs : s < 64) :
+    ((1#128 <<< (64 - s)) - 1).setWidth 64 <<< s =
+      BitVec.ofNat 64 (((1 <<< (64 - s)) - 1) <<< s) := by
+  interval_cases s <;> decide
+
+theorem shiftRightBitmask_entry (v : BitVec 128) :
+    shiftRightBitmaskTableEntry (F := F) v.toFin =
+      ((BitVec.ofNat 64 (((1 <<< (64 - v.toNat % 64)) - 1) <<< (v.toNat % 64))).toNat : F) := by
+  unfold shiftRightBitmaskTableEntry
+  simp only [BitVec.ofFin_toFin]
+  rw [show (64 : BitVec 128) = BitVec.ofNat 128 64 from rfl, umod_toNat _ _ (by norm_num),
+    shiftRightBitmask_value _ (Nat.mod_lt _ (by norm_num))]
+
+theorem shiftRightBitmaskW_value (s : Nat) (hs : s < 32) :
+    ((1#128 <<< 32) - (1#128 <<< s)).setWidth 64 = BitVec.ofNat 64 (2 ^ 32 - 2 ^ s) := by
+  interval_cases s <;> decide
+
+theorem shiftRightBitmaskW_entry (v : BitVec 128) :
+    shiftRightBitmaskWTableEntry (F := F) v.toFin =
+      ((BitVec.ofNat 64 (2 ^ 32 - 2 ^ (v.toNat % 32))).toNat : F) := by
+  unfold shiftRightBitmaskWTableEntry
+  simp only [BitVec.ofFin_toFin]
+  rw [show (32 : BitVec 128) = BitVec.ofNat 128 32 from rfl, umod_toNat _ _ (by norm_num),
+    shiftRightBitmaskW_value _ (Nat.mod_lt _ (by norm_num))]
+
+theorem negateIf_entry (l r : BitVec 64) :
+    virtualNegateIfTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((if l.msb then -r else r).toNat : F) := by
+  have hmask : ((1#128 <<< 64) - 1).setWidth 64 = (-1 : BitVec 64) := by decide
+  have h1 : r &&& -1 = r := by bv_decide
+  have h2 : -r &&& -1 = -r := by bv_decide
+  simp only [virtualNegateIfTableEntry, uninterleave_interleave, hmask, h1, h2]
+  have hsign : (l &&& 1#64 <<< 63 = 0) ↔ l.msb = false := by bv_decide
+  by_cases hm : l.msb
+  · have : ¬ (l &&& 1#64 <<< 63 = 0) := by rw [hsign, hm]; simp
+    simp only [this, hm, ↓reduceIte]
+  · have : l &&& 1#64 <<< 63 = 0 := by rw [hsign]; simpa using hm
+    simp only [this, hm, ↓reduceIte, Bool.false_eq_true]
+
+theorem shiftDataB_entry (l r : BitVec 64) :
+    shiftDataBTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((jolt_virtual_shift_data_b_value l r).toNat : F) := by
+  have hm : ((1#128 <<< 8) - 1).setWidth 64 = (0xFF : BitVec 64) := by decide
+  simp only [shiftDataBTableEntry, uninterleave_interleave, hm, jolt_virtual_shift_data_b_value]
+
+theorem shiftDataH_entry (l r : BitVec 64) :
+    shiftDataHTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((jolt_virtual_shift_data_h_value l r).toNat : F) := by
+  have hm : ((1#128 <<< 16) - 1).setWidth 64 = (0xFFFF : BitVec 64) := by decide
+  simp only [shiftDataHTableEntry, uninterleave_interleave, hm, jolt_virtual_shift_data_h_value]
+
+theorem shiftDataW_entry (l r : BitVec 64) :
+    shiftDataWTableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((jolt_virtual_shift_data_w_value l r).toNat : F) := by
+  have hm : ((1#128 <<< 32) - 1).setWidth 64 = (0xFFFF_FFFF : BitVec 64) := by decide
+  simp only [shiftDataWTableEntry, uninterleave_interleave, hm, jolt_virtual_shift_data_w_value]
+
+theorem shiftLeft_ofNat_eq (c k : Nat) :
+    BitVec.ofNat 64 c <<< k = BitVec.ofNat 64 (c <<< k) := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [BitVec.toNat_shiftLeft, BitVec.toNat_ofNat, Nat.shiftLeft_eq]
+  rw [Nat.mod_mul_mod]
+
+theorem toNat_eq_of_setWidth (a : BitVec 128) (b : BitVec 64) (h : a = b.setWidth 128) :
+    a.toNat = b.toNat := by
+  rw [h, BitVec.toNat_setWidth, Nat.mod_eq_of_lt (by have := b.isLt; omega)]
+
+theorem ofNat64_eq_setWidth (n : Nat) :
+    BitVec.ofNat 64 n = (BitVec.ofNat 128 n).setWidth 64 := by
+  rw [BitVec.setWidth_ofNat_of_le (by norm_num)]
+
+theorem windowMaskB_entry (n : Nat) :
+    windowMaskBTableEntry (F := F) (BitVec.ofNat 128 n).toFin =
+      ((BitVec.ofNat 64 (0xFF <<< (8 * (BitVec.ofNat 64 n &&& 7).toNat))).toNat : F) := by
+  have hm : ((1#128 <<< 8) - 1).setWidth 64 = BitVec.ofNat 64 0xFF := by decide
+  have ho : (BitVec.ofNat 128 n &&& 7).toNat = (BitVec.ofNat 64 n &&& 7).toNat :=
+    toNat_eq_of_setWidth _ _ (by rw [ofNat64_eq_setWidth]; bv_decide)
+  simp only [windowMaskBTableEntry, BitVec.ofFin_toFin, hm, shiftLeft_ofNat_eq, ho]
+
+theorem windowMaskH_entry (n : Nat) :
+    windowMaskHTableEntry (F := F) (BitVec.ofNat 128 n).toFin =
+      ((BitVec.ofNat 64 (0xFFFF <<< (8 * (BitVec.ofNat 64 n &&& 6).toNat))).toNat : F) := by
+  have hm : ((1#128 <<< 16) - 1).setWidth 64 = BitVec.ofNat 64 0xFFFF := by decide
+  have ho : (BitVec.ofNat 128 n &&& 6).toNat = (BitVec.ofNat 64 n &&& 6).toNat :=
+    toNat_eq_of_setWidth _ _ (by rw [ofNat64_eq_setWidth]; bv_decide)
+  simp only [windowMaskHTableEntry, BitVec.ofFin_toFin, hm, shiftLeft_ofNat_eq, ho]
+
+theorem windowMaskW_entry (n : Nat) :
+    windowMaskWTableEntry (F := F) (BitVec.ofNat 128 n).toFin =
+      ((BitVec.ofNat 64 (0xFFFF_FFFF <<< (32 * ((BitVec.ofNat 64 n >>> 2) &&& 1).toNat))).toNat : F) := by
+  have hm : ((1#128 <<< 32) - 1).setWidth 64 = BitVec.ofNat 64 0xFFFF_FFFF := by decide
+  have ho : ((BitVec.ofNat 128 n >>> 2) &&& 1).toNat = ((BitVec.ofNat 64 n >>> 2) &&& 1).toNat :=
+    toNat_eq_of_setWidth _ _ (by rw [ofNat64_eq_setWidth]; bv_decide)
+  simp only [windowMaskWTableEntry, BitVec.ofFin_toFin, hm, shiftLeft_ofNat_eq, ho]
+
+theorem rotater_eq {n : Nat} (z : BitVec n) (s : Nat) (hs : s ≤ n) :
+    rotater z s = (z >>> s) ||| (z <<< (n - s)) := by
+  unfold rotater
+  have : (Sail.BitVec.length z -i (s : Int)) = ((n - s : Nat) : Int) := by
+    simp only [Sail.BitVec.length]; omega
+  rw [this]
+  rfl
+
+theorem rotatel_one (z : BitVec 64) : rotatel z 1 = (z <<< 1) ||| (z >>> 63) := rfl
+
+theorem xorRotL1_getLsbD (x y : BitVec 64) (i : Nat) (hi : i < 64) :
+    (x ^^^ ((y <<< 1) ||| (y >>> 63))).getLsbD i = (x.getLsbD i != y.getLsbD ((i + 63) % 64)) := by
+  interval_cases i <;> bv_decide
+
+theorem xorRotL1_entry (l r : BitVec 64) :
+    virtualXorRotL1TableEntry (F := F) (interleaveLookupOperands l r).toFin =
+      ((jolt_virtual_xorrotl1_value l r).toNat : F) := by
+  rw [jolt_virtual_xorrotl1_value, rotatel_one, bitVec_toNat_cast_eq_sum]
+  unfold virtualXorRotL1TableEntry
+  refine Finset.sum_congr rfl fun i _ => ?_
+  simp only [BitVec.val_toFin, interleave_testBit_odd l r i i.isLt,
+    interleave_testBit_even l r _ (Nat.mod_lt _ (by omega)), xorRotL1_getLsbD l r i i.isLt]
+
+theorem xorRot_entry (r : Nat) (hr : r = 32 ∨ r = 24 ∨ r = 16 ∨ r = 63) (l y : BitVec 64) :
+    virtualXorRotTableEntry (F := F) r (interleaveLookupOperands l y).toFin =
+      ((jolt_virtual_xorrot_value r l y).toNat : F) := by
+  have hr64 : r < 64 := by omega
+  simp only [virtualXorRotTableEntry, uninterleave_interleave, jolt_virtual_xorrot_value,
+    rotater_eq _ r hr64.le, Nat.mod_eq_of_lt hr64]
+  congr 2
+  rcases hr with rfl | rfl | rfl | rfl <;> bv_decide
+
+theorem xorRotW_entry (r : Nat)
+    (hr : r = 16 ∨ r = 12 ∨ r = 8 ∨ r = 7 ∨ r = 22 ∨ r = 19 ∨ r = 6) (l y : BitVec 64) :
+    virtualXorRotWTableEntry (F := F) r (interleaveLookupOperands l y).toFin =
+      ((jolt_virtual_xorrotw_value r l y).toNat : F) := by
+  have hr32 : r < 32 := by omega
+  simp only [virtualXorRotWTableEntry, uninterleave_interleave, jolt_virtual_xorrotw_value,
+    rotater_eq _ r hr32.le, Nat.mod_eq_of_lt hr32, zero_extend, Sail.BitVec.zeroExtend,
+    Sail.BitVec.extractLsb]
+  congr 2
+  rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> bv_decide
+
+theorem halfword_aligned (n : Nat) (h : BitVec.ofNat 64 n &&& 1 = 0) :
+    BitVec.ofNat 128 n % 2 = 0 := by
+  rw [ofNat64_eq_setWidth] at h
+  generalize BitVec.ofNat 128 n = v at h ⊢
+  bv_decide
+
+theorem word_aligned (n : Nat) (h : BitVec.ofNat 64 n &&& 3 = 0) :
+    BitVec.ofNat 128 n % 4 = 0 := by
+  rw [ofNat64_eq_setWidth] at h
+  generalize BitVec.ofNat 128 n = v at h ⊢
+  bv_decide
+
+end entries2
+
+theorem mulWide_lt (x y : BitVec 64) : JoltISA.mulWide x y < 2 ^ 128 := by
+  have hx := x.isLt; have hy := y.isLt
+  calc x.toNat * y.toNat < 2 ^ 64 * 2 ^ 64 := Nat.mul_lt_mul'' hx hy
+    _ = 2 ^ 128 := by norm_num
+
+section tables2
+variable {F : Type} [Field F] {program : JoltProgram}
+
+theorem lookupEntryCorrect_SignExtendWord (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .SignExtendWord) :
+    LookupEntryCorrect F .SignExtendWord row := by
+  lookup_cases
+  all_goals simp only [signExtendWord_entry]
+  all_goals simp only [jolt_addiw_value64, jolt_addw_value,
+    jolt_subw_value, jolt_mulw_value, jolt_virtual_muliw_value, jolt_virtual_sign_extend_word_value,
+    BitVec.setWidth_ofNat_of_le (by norm_num : 32 ≤ 128), BitVec.setWidth_ofNat_of_le (by norm_num : 32 ≤ 64),
+    BitVec.setWidth_setWidth_of_le _ (by norm_num : 32 ≤ 128)]
+
+theorem lookupEntryCorrect_UpperWord (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .UpperWord) :
+    LookupEntryCorrect F .UpperWord row := by
+  lookup_cases
+  rw [upperWord_entry _ (mulWide_lt _ _)]
+  rfl
+
+theorem lookupEntryCorrect_LowerHalfWord (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .LowerHalfWord) :
+    LookupEntryCorrect F .LowerHalfWord row := by
+  lookup_cases
+  simp only [lowerHalfWord_entry, jolt_virtual_zero_extend_word_value, zero_extend,
+    Sail.BitVec.zeroExtend, Sail.BitVec.extractLsb]
+  congr 2
+
+theorem lookupEntryCorrect_RangeCheckAligned (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .RangeCheckAligned) :
+    LookupEntryCorrect F .RangeCheckAligned row := by
+  lookup_cases
+  simp only [rangeCheckAligned_entry, jolt_jalr_target64, BitVec.setWidth_ofNat_of_le (by norm_num : 64 ≤ 128),
+    Sail.BitVec.update, Sail.BitVec.updateSubrange']
+  congr 2
+  bv_decide
+
+theorem lookupEntryCorrect_AlignAddr (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .AlignAddr) :
+    LookupEntryCorrect F .AlignAddr row := by
+  lookup_cases
+  simp only [alignAddr_entry, jolt_virtual_align_addr_value64,
+    BitVec.setWidth_ofNat_of_le (by norm_num : 64 ≤ 128)]
+  rfl
+
+theorem lookupEntryCorrect_SignMask (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .SignMask) :
+    LookupEntryCorrect F .SignMask row := by
+  lookup_cases
+  simp only [signMask_entry, jolt_movsign_value]
+
+theorem lookupEntryCorrect_VirtualNegateIf (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualNegateIf) :
+    LookupEntryCorrect F .VirtualNegateIf row := by
+  lookup_cases
+  simp only [negateIf_entry, jolt_virtual_negate_if_value]
+
+theorem lookupEntryCorrect_Pow2 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Pow2) :
+    LookupEntryCorrect F .Pow2 row := by
+  lookup_cases
+  all_goals simp only [pow2_entry, jolt_virtual_pow2_value, jolt_virtual_pow2i_value]
+  all_goals congr 4
+  all_goals simp [BitVec.toNat_setWidth, Nat.mod_mod_of_dvd]
+
+theorem lookupEntryCorrect_Pow2W (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Pow2W) :
+    LookupEntryCorrect F .Pow2W row := by
+  lookup_cases
+  all_goals simp only [pow2W_entry, jolt_virtual_pow2w_value, jolt_virtual_pow2iw_value]
+  all_goals congr 4
+  all_goals simp [BitVec.toNat_setWidth, Nat.mod_mod_of_dvd]
+
+theorem lookupEntryCorrect_ShiftRightBitmask (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ShiftRightBitmask) :
+    LookupEntryCorrect F .ShiftRightBitmask row := by
+  lookup_cases
+  all_goals simp only [shiftRightBitmask_entry, jolt_virtual_shift_right_bitmask_value,
+    jolt_virtual_shift_right_bitmaski_value]
+  all_goals congr 4 <;> simp [BitVec.toNat_setWidth, Nat.mod_mod_of_dvd]
+
+theorem lookupEntryCorrect_ShiftRightBitmaskW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ShiftRightBitmaskW) :
+    LookupEntryCorrect F .ShiftRightBitmaskW row := by
+  lookup_cases
+  simp only [shiftRightBitmaskW_entry, jolt_virtual_shift_right_bitmaskw_value]
+  congr 5
+
+theorem lookupEntryCorrect_ShiftDataB (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ShiftDataB) :
+    LookupEntryCorrect F .ShiftDataB row := by
+  lookup_cases
+  simp only [shiftDataB_entry]
+
+theorem lookupEntryCorrect_ShiftDataH (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ShiftDataH) :
+    LookupEntryCorrect F .ShiftDataH row := by
+  lookup_cases
+  simp only [shiftDataH_entry]
+
+theorem lookupEntryCorrect_ShiftDataW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ShiftDataW) :
+    LookupEntryCorrect F .ShiftDataW row := by
+  lookup_cases
+  simp only [shiftDataW_entry]
+
+theorem lookupEntryCorrect_WindowMaskB (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .WindowMaskB) :
+    LookupEntryCorrect F .WindowMaskB row := by
+  lookup_cases
+  simp only [windowMaskB_entry, jolt_virtual_window_mask_b_value64]
+
+theorem lookupEntryCorrect_WindowMaskH (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .WindowMaskH) :
+    LookupEntryCorrect F .WindowMaskH row := by
+  lookup_cases
+  simp only [windowMaskH_entry, jolt_virtual_window_mask_h_value64]
+
+theorem lookupEntryCorrect_WindowMaskW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .WindowMaskW) :
+    LookupEntryCorrect F .WindowMaskW row := by
+  lookup_cases
+  simp only [windowMaskW_entry, jolt_virtual_window_mask_w_value64]
+
+theorem lookupEntryCorrect_VirtualXORROTL1 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTL1) :
+    LookupEntryCorrect F .VirtualXORROTL1 row := by
+  lookup_cases
+  simp only [xorRotL1_entry]
+
+theorem lookupEntryCorrect_VirtualXORROT32 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROT32) :
+    LookupEntryCorrect F .VirtualXORROT32 row := by
+  lookup_cases
+  exact xorRot_entry 32 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROT24 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROT24) :
+    LookupEntryCorrect F .VirtualXORROT24 row := by
+  lookup_cases
+  exact xorRot_entry 24 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROT16 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROT16) :
+    LookupEntryCorrect F .VirtualXORROT16 row := by
+  lookup_cases
+  exact xorRot_entry 16 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROT63 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROT63) :
+    LookupEntryCorrect F .VirtualXORROT63 row := by
+  lookup_cases
+  exact xorRot_entry 63 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW16 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW16) :
+    LookupEntryCorrect F .VirtualXORROTW16 row := by
+  lookup_cases
+  exact xorRotW_entry 16 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW12 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW12) :
+    LookupEntryCorrect F .VirtualXORROTW12 row := by
+  lookup_cases
+  exact xorRotW_entry 12 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW8 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW8) :
+    LookupEntryCorrect F .VirtualXORROTW8 row := by
+  lookup_cases
+  exact xorRotW_entry 8 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW7 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW7) :
+    LookupEntryCorrect F .VirtualXORROTW7 row := by
+  lookup_cases
+  exact xorRotW_entry 7 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW22 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW22) :
+    LookupEntryCorrect F .VirtualXORROTW22 row := by
+  lookup_cases
+  exact xorRotW_entry 22 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW19 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW19) :
+    LookupEntryCorrect F .VirtualXORROTW19 row := by
+  lookup_cases
+  exact xorRotW_entry 19 (by decide) _ _
+
+theorem lookupEntryCorrect_VirtualXORROTW6 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualXORROTW6) :
+    LookupEntryCorrect F .VirtualXORROTW6 row := by
+  lookup_cases
+  exact xorRotW_entry 6 (by decide) _ _
+
+theorem rev8_32 (x : BitVec 32) : rev8 x = swapBytes32 x := by
+  unfold rev8
+  simp only [Id.run]
+  change IntRange.forIn' _ _ _ >>= _ = _
+  unfold IntRange.forIn'
+  simp only [Sail.BitVec.length, BitVec.length, Nat.cast_ofNat]
+  iterate 5
+    rw [IntRange.forIn'.loop]
+    simp (config := { decide := true }) only [Membership.mem, dite_true, dite_false, pure_bind,
+      bind_pure, Int.reduceAdd, Int.reduceSub, Int.reduceToNat]
+  change BitVec.updateSubrange _ _ _ _ = _
+  simp only [BitVec.updateSubrange, Sail.BitVec.updateSubrange', Sail.BitVec.extractLsb,
+    zeros, swapBytes32, Nat.reduceSub, Nat.reduceAdd]
+  bv_decide
+
+theorem rev8w_eq (v : BitVec 64) :
+    rev8w v = swapBytes32 (v.extractLsb 63 32) +++ swapBytes32 (v.extractLsb 31 0) := by
+  simp only [rev8w, swapBytes32]
+  bv_decide
+
+theorem lookupEntryCorrect_VirtualRev8W (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualRev8W) :
+    LookupEntryCorrect F .VirtualRev8W row := by
+  lookup_cases
+  simp only [virtualRev8WTableEntry, BitVec.ofFin_toFin, jolt_virtual_rev8w_value, rev8_32,
+    Sail.BitVec.extractLsb, BitVec.setWidth_setWidth_of_le _ (by norm_num : 64 ≤ 128)]
+  rw [BitVec.setWidth_eq, rev8w_eq]
+
+
+-- FIXME: the six shift/rotate lemmas below are false while
+-- `JoltProgram.expandedBytecode` is an arbitrary array: a `VirtualSRLI` row with
+-- mask immediate `2` (or a `VirtualSRL` row whose mask register holds `2`) is
+-- accepted, and its entry differs from its output. Rust's expander only emits
+-- right-shift bitmasks here. Once `JoltProgram` records that construction,
+-- prove these for bitmask-shaped masks.
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualSRL`/`VirtualSRLI` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `0`, output `4 >>> ctz 2 = 2`.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualSRL (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualSRL) :
+    LookupEntryCorrect F .VirtualSRL row := by
+  sorry
+
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualSRA`/`VirtualSRAI` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `0`, output `4.sshiftRight 1 = 2`.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualSRA (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualSRA) :
+    LookupEntryCorrect F .VirtualSRA row := by
+  sorry
+
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualSRLW`/`VirtualSRLIW` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `0`, output `2`. Also mask `0` for `VirtualSRLW`: entry `0`, output the sign-extended low word.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualSRLW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualSRLW) :
+    LookupEntryCorrect F .VirtualSRLW row := by
+  sorry
+
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualSRAW`/`VirtualSRAIW` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `0`, output `2`.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualSRAW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualSRAW) :
+    LookupEntryCorrect F .VirtualSRAW row := by
+  sorry
+
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualROTRI` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `4`, output `rotater 4 1 = 2`.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualROTR (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualROTR) :
+    LookupEntryCorrect F .VirtualROTR row := by
+  sorry
+
+/-- FALSE for arbitrary programs; left as `sorry`.
+The table reads the right operand as a right-shift bitmask (ones from bit
+`s` upward) and is correct only for such masks, while the honest output of
+`VirtualROTRIW` shifts by `ctz` of whatever mask the row carries.
+`JoltProgram.expandedBytecode` is an arbitrary array (see the FIXME on
+`JoltProgram.rowValid`), so nothing constrains the mask shape.
+Counterexample: source `4`, mask `2`: entry `4`, output `2`.
+See `JoltConstraints/Tests/LookupShiftMask.lean`. -/
+theorem lookupEntryCorrect_VirtualROTRW (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .VirtualROTRW) :
+    LookupEntryCorrect F .VirtualROTRW row := by
+  sorry
+
+theorem lookupEntryCorrect_Pext (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .Pext) :
+    LookupEntryCorrect F .Pext row := by
+  lookup_cases
+  all_goals simp only [pextTableEntry, uninterleave_interleave, pext_eq_jolt_virtual_pext_value]
+
+theorem lookupEntryCorrect_PextSigned (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .PextSigned) :
+    LookupEntryCorrect F .PextSigned row := by
+  lookup_cases
+  all_goals simp only [pextSignedTableEntry, uninterleave_interleave,
+    pextSigned_eq_jolt_virtual_pext_signed_value]
+
+theorem lookupEntryCorrect_UnsignedLessThanEqual (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .UnsignedLessThanEqual) :
+    LookupEntryCorrect F .UnsignedLessThanEqual row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  have h2 := lookup_read_bind _ _ _ _ _ h1
+  split_ifs at h2 with hc
+  · rw [unsignedLessThanEqual_entry, if_pos (BitVec.le_def.mpr hc)]
+    simp
+  · exact absurd h2 (by simp [throw, throwThe, MonadExceptOf.throw, EStateM.throw])
+
+theorem lookupEntryCorrect_HalfwordAlignment (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .HalfwordAlignment) :
+    LookupEntryCorrect F .HalfwordAlignment row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  split_ifs at h1 with hc
+  · simp only [halfwordAlignmentTableEntry, BitVec.ofFin_toFin]
+    rw [if_pos (halfword_aligned _ hc)]
+    simp
+  · exact absurd h1 (by simp [pure, EStateM.pure])
+
+theorem lookupEntryCorrect_WordAlignment (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .WordAlignment) :
+    LookupEntryCorrect F .WordAlignment row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  split_ifs at h1 with hc
+  · simp only [wordAlignmentTableEntry, BitVec.ofFin_toFin]
+    rw [if_pos (word_aligned _ hc)]
+    simp
+  · exact absurd h1 (by simp [pure, EStateM.pure])
+
+theorem lookupEntryCorrect_MulUNoOverflow (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .MulUNoOverflow) :
+    LookupEntryCorrect F .MulUNoOverflow row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  have h2 := lookup_read_bind _ _ _ _ _ h1
+  split_ifs at h2 with hc
+  · simp only [mulUNoOverflowTableEntry, BitVec.ofFin_toFin]
+    rw [if_pos (upper_zero_of_lt _ hc)]
+    simp
+  · exact absurd h2 (by simp [throw, throwThe, MonadExceptOf.throw, EStateM.throw])
+
+theorem lookupEntryCorrect_ValidDiv0 (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ValidDiv0) :
+    LookupEntryCorrect F .ValidDiv0 row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  have h2 := lookup_read_bind _ _ _ _ _ h1
+  split_ifs at h2 with hc
+  · exact absurd h2 (by simp [throw, throwThe, MonadExceptOf.throw, EStateM.throw])
+  · rw [validDiv0_entry, if_neg (by simpa using hc)]
+    simp
+
+theorem lookupEntryCorrect_ValidUnsignedRemainder (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some .ValidUnsignedRemainder) :
+    LookupEntryCorrect F .ValidUnsignedRemainder row := by
+  have hexec := row_executes_exists row
+  lookup_cases
+  rw [hi] at hexec
+  obtain ⟨_, hexec⟩ := hexec
+  simp only [JoltISA.Instr.withRuntimeAdvice, JoltISA.execInstr] at hexec
+  have h1 := lookup_read_bind _ _ _ _ _ hexec
+  have h2 := lookup_read_bind _ _ _ _ _ h1
+  split_ifs at h2 with hc
+  · rw [validUnsignedRemainder_entry, if_pos (by simpa [BitVec.lt_def] using hc)]
+    simp
+  · exact absurd h2 (by simp [throw, throwThe, MonadExceptOf.throw, EStateM.throw])
+
+/-- Rows whose instruction has no lookup table (`FENCE`, `LD`, `SD`,
+`VirtualHostIO`) have lookup output zero. -/
+theorem rowLookupOutput_eq_zero_of_lookupTable_none (row : JoltTraceRow program)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = none) :
+    rowLookupOutput row = 0 := by
+  unfold rowLookupOutput
+  cases hi : rowInstruction row <;>
+    simp only [hi, JoltMetadata.lookupTable, reduceCtorEq] at h <;>
+    simp only [hi]
+
+/-- Dispatcher: the honest entry of the row's lookup table equals the honest
+lookup output. Depends on every `lookupEntryCorrect_*` lemma, including the
+ones left as `sorry` (`VirtualSRL`, `VirtualSRA`, `VirtualSRLW`, `VirtualSRAW`,
+`VirtualROTR`, `VirtualROTRW`). -/
+theorem lookupEntryCorrect_of_lookupTable (row : JoltTraceRow program) (k : LookupTableKind)
+    (h : JoltMetadata.lookupTable (rowInstruction row) = some k) :
+    LookupEntryCorrect F k row :=
+  match k with
+  | .RangeCheck => lookupEntryCorrect_RangeCheck row h
+  | .RangeCheckAligned => lookupEntryCorrect_RangeCheckAligned row h
+  | .And => lookupEntryCorrect_And row h
+  | .Andn => lookupEntryCorrect_Andn row h
+  | .Or => lookupEntryCorrect_Or row h
+  | .Xor => lookupEntryCorrect_Xor row h
+  | .Equal => lookupEntryCorrect_Equal row h
+  | .SignedGreaterThanEqual => lookupEntryCorrect_SignedGreaterThanEqual row h
+  | .UnsignedGreaterThanEqual => lookupEntryCorrect_UnsignedGreaterThanEqual row h
+  | .NotEqual => lookupEntryCorrect_NotEqual row h
+  | .SignedLessThan => lookupEntryCorrect_SignedLessThan row h
+  | .UnsignedLessThan => lookupEntryCorrect_UnsignedLessThan row h
+  | .SignMask => lookupEntryCorrect_SignMask row h
+  | .UpperWord => lookupEntryCorrect_UpperWord row h
+  | .UnsignedLessThanEqual => lookupEntryCorrect_UnsignedLessThanEqual row h
+  | .ValidUnsignedRemainder => lookupEntryCorrect_ValidUnsignedRemainder row h
+  | .ValidDiv0 => lookupEntryCorrect_ValidDiv0 row h
+  | .HalfwordAlignment => lookupEntryCorrect_HalfwordAlignment row h
+  | .WordAlignment => lookupEntryCorrect_WordAlignment row h
+  | .LowerHalfWord => lookupEntryCorrect_LowerHalfWord row h
+  | .SignExtendWord => lookupEntryCorrect_SignExtendWord row h
+  | .Pow2 => lookupEntryCorrect_Pow2 row h
+  | .Pow2W => lookupEntryCorrect_Pow2W row h
+  | .ShiftRightBitmask => lookupEntryCorrect_ShiftRightBitmask row h
+  | .VirtualRev8W => lookupEntryCorrect_VirtualRev8W row h
+  | .VirtualSRL => lookupEntryCorrect_VirtualSRL row h
+  | .VirtualSRA => lookupEntryCorrect_VirtualSRA row h
+  | .VirtualROTR => lookupEntryCorrect_VirtualROTR row h
+  | .VirtualROTRW => lookupEntryCorrect_VirtualROTRW row h
+  | .VirtualNegateIf => lookupEntryCorrect_VirtualNegateIf row h
+  | .MulUNoOverflow => lookupEntryCorrect_MulUNoOverflow row h
+  | .VirtualXORROT32 => lookupEntryCorrect_VirtualXORROT32 row h
+  | .VirtualXORROT24 => lookupEntryCorrect_VirtualXORROT24 row h
+  | .VirtualXORROT16 => lookupEntryCorrect_VirtualXORROT16 row h
+  | .VirtualXORROT63 => lookupEntryCorrect_VirtualXORROT63 row h
+  | .VirtualXORROTW16 => lookupEntryCorrect_VirtualXORROTW16 row h
+  | .VirtualXORROTW12 => lookupEntryCorrect_VirtualXORROTW12 row h
+  | .VirtualXORROTW8 => lookupEntryCorrect_VirtualXORROTW8 row h
+  | .VirtualXORROTW7 => lookupEntryCorrect_VirtualXORROTW7 row h
+  | .WindowMaskW => lookupEntryCorrect_WindowMaskW row h
+  | .PextSigned => lookupEntryCorrect_PextSigned row h
+  | .VirtualXORROTW22 => lookupEntryCorrect_VirtualXORROTW22 row h
+  | .VirtualXORROTW19 => lookupEntryCorrect_VirtualXORROTW19 row h
+  | .VirtualXORROTW6 => lookupEntryCorrect_VirtualXORROTW6 row h
+  | .ShiftRightBitmaskW => lookupEntryCorrect_ShiftRightBitmaskW row h
+  | .VirtualSRLW => lookupEntryCorrect_VirtualSRLW row h
+  | .VirtualSRAW => lookupEntryCorrect_VirtualSRAW row h
+  | .Pext => lookupEntryCorrect_Pext row h
+  | .WindowMaskB => lookupEntryCorrect_WindowMaskB row h
+  | .WindowMaskH => lookupEntryCorrect_WindowMaskH row h
+  | .AlignAddr => lookupEntryCorrect_AlignAddr row h
+  | .ShiftDataB => lookupEntryCorrect_ShiftDataB row h
+  | .ShiftDataH => lookupEntryCorrect_ShiftDataH row h
+  | .ShiftDataW => lookupEntryCorrect_ShiftDataW row h
+  | .VirtualXORROTL1 => lookupEntryCorrect_VirtualXORROTL1 row h
+
+end tables2
+
+end JoltConstraints
diff --git a/JoltConstraints/Constraints/LookupOperandData.lean b/JoltConstraints/Constraints/LookupOperandData.lean
index b9e7f42..7f000a8 100644
--- a/JoltConstraints/Constraints/LookupOperandData.lean
+++ b/JoltConstraints/Constraints/LookupOperandData.lean
@@ -1,4 +1,4 @@
-import JoltConstraints.Constraints.LookupOutputEqInstructionReadRaf
+import JoltConstraints.Constraints.InstructionLookupRa
 
 set_option autoImplicit false
 
diff --git a/JoltConstraints/Constraints/LookupOutputEqInstructionReadRaf.lean b/JoltConstraints/Constraints/LookupOutputEqInstructionReadRaf.lean
index 6c57fff..3fa7cb7 100644
--- a/JoltConstraints/Constraints/LookupOutputEqInstructionReadRaf.lean
+++ b/JoltConstraints/Constraints/LookupOutputEqInstructionReadRaf.lean
@@ -1,8 +1,6 @@
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.Field.Defs
-import JoltConstraints.witness
-import JoltConstraints.lookup_table
-import JoltConstraints.honest_witness
+import JoltConstraints.Constraints.InstructionLookupRa
+import JoltConstraints.Constraints.InstructionReadSelection
+import JoltConstraints.Constraints.LookupEntryProofHelpers
 
 set_option autoImplicit false
 
@@ -10,22 +8,6 @@ namespace JoltConstraints
 
 open scoped BigOperators
 
-/-- The `chunk`th virtual chunk of a 128-bit lookup address, most significant first. -/
-def instructionLookupChunk (params : WitnessParams) (address : Fin (2 ^ 128))
-    (chunk : Fin params.virtualInstructionChunks) : Fin (2 ^ params.virtualChunkBits) :=
-  ⟨(address.val /
-      2 ^ ((params.virtualInstructionChunks - 1 - chunk.val) * params.virtualChunkBits)) %
-      2 ^ params.virtualChunkBits,
-    Nat.mod_lt _ (pow_pos (by decide : 0 < (2 : Nat)) _)⟩
-
-/-- `LookupRa(x,t)` in `constraints.md`: multiply the virtual instruction-address
-entries selected by the chunks of `x`. -/
-noncomputable def instructionLookupRa {F : Type} [Field F] {params : WitnessParams}
-    (witness : WitnessType F params) (address : Fin (2 ^ 128))
-    (t : Fin params.traceLength) : F :=
-  ∏ chunk : Fin params.virtualInstructionChunks,
-    witness.InstructionRa chunk (instructionLookupChunk params address chunk) t
-
 /-
 For every padded trace index t ∈ T:
 
@@ -47,8 +29,9 @@ def lookupOutputEqInstructionReadRaf {F : Type} [Field F] {params : WitnessParam
       ∑ address : Fin (2 ^ 128), instructionLookupRa witness address t *
         ∑ table : LookupTableKind, witness.LookupTableFlag table t * lookupTableEntry table address
 
-/-- Completeness of the lookup-output constraint. The execution-row case is
-pending the correspondence of the fixed table definitions with ISA outputs. -/
+/-- Completeness of the lookup-output constraint. The execution-row case
+reduces to `lookupEntryCorrect_of_lookupTable` (one lemma per lookup table in
+`LookupEntryProofHelpers.lean`); some of those remain `sorry`, see there. -/
 theorem honestWitness_lookupOutputEqInstructionReadRaf
     {F : Type} [Field F] (params : WitnessParams)
     {program : JoltProgram} (trace : JoltTrace program)
@@ -59,11 +42,35 @@ theorem honestWitness_lookupOutputEqInstructionReadRaf
       (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain) := by
   intro t
   by_cases inBounds : t.val < trace.rows.size
-  · -- FIXME (translation): all lookup-table entries are now defined, and
-    -- honest address selection is proved in `InstructionReadSelection.lean`.
-    -- Relate each selected entry to `HonestWitness.rowLookupOutput` before
-    -- closing this target.
-    sorry
+  · -- Execution row: collapse the address sum to the honest index, the table
+    -- sum to the flagged table, and apply the per-table entry lemmas.
+    set row := getElem trace.rows t.val inBounds with hrow
+    rw [instructionRead_honest params trace ramFits traceFits bytecodeDomain
+      (fun a => ∑ table : LookupTableKind,
+        (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain).LookupTableFlag
+          table t * lookupTableEntry table a) t]
+    have hidx : (⟨(HonestWitness.lookupIndex trace t.val).toNat,
+        (HonestWitness.lookupIndex trace t.val).isLt⟩ : Fin (2 ^ 128)) = rowLookupAddress row := by
+      simp only [HonestWitness.lookupIndex, dif_pos inBounds, rowLookupAddress, rowLookupIndex, hrow]
+      rfl
+    rw [hidx]
+    have hflag : ∀ table : LookupTableKind,
+        (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain).LookupTableFlag
+          table t = if JoltMetadata.lookupTable (rowInstruction row) = some table then 1 else 0 := by
+      intro table
+      simp only [JoltProgram.honestWitness, HonestWitness.LookupTableFlag, dif_pos inBounds,
+        JoltMetadata.lookupTableFlag, beq_iff_eq, rowInstruction, hrow]
+    have hout : (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain).LookupOutput t
+        = ((HonestWitness.rowLookupOutput row).toNat : F) := by
+      simp only [JoltProgram.honestWitness, HonestWitness.LookupOutput, dif_pos inBounds]
+      rfl
+    simp only [hflag, hout, ite_mul, one_mul, zero_mul]
+    cases hk : JoltMetadata.lookupTable (rowInstruction row) with
+    | none =>
+      simp [rowLookupOutput_eq_zero_of_lookupTable_none row hk]
+    | some k =>
+      simp only [Option.some.injEq, Finset.sum_ite_eq, Finset.mem_univ, if_true]
+      exact (lookupEntryCorrect_of_lookupTable row k hk).symm
   · -- Padding has zero output and every table flag is zero.
     simp [JoltProgram.honestWitness, HonestWitness.LookupOutput,
       HonestWitness.LookupTableFlag, inBounds]
diff --git a/JoltConstraints/Constraints/LookupPextProofHelpers.lean b/JoltConstraints/Constraints/LookupPextProofHelpers.lean
new file mode 100644
index 0000000..8f9b414
--- /dev/null
+++ b/JoltConstraints/Constraints/LookupPextProofHelpers.lean
@@ -0,0 +1,460 @@
+import Mathlib.Tactic.Ring
+import JoltConstraints.lookup_table
+import JoltBytecode.JoltISA.Values
+
+/-!
+# The PEXT tables against the honest `VirtualPext` values
+
+`pext_eq_jolt_virtual_pext_value` shows that the table's `pext` (a contiguous
+fast path plus a 64-pass clear-lowest-set-bit loop) equals
+`jolt_virtual_pext_value`, the fuel recursion `jolt_pext_nat 64` used by the
+honest witness. `pextSigned_eq_jolt_virtual_pext_signed_value` adds the sign
+extension: `windowSignBit` reads the source bit at the mask's highest set bit,
+which `jolt_pext_nat_testBit_top` shows is bit `popcount - 1` of the extracted
+value, and adding `2^64 - 2^popcount` to a value below `2^popcount` is the same
+as or-ing in the high ones.
+
+The loop is handled by rewriting its `forIn` as a `List.foldl` of `pextStep`
+and carrying `PextInv`: after `n` passes the extracted prefix `out` and the
+remaining mask `bits` satisfy
+`jolt_pext_nat 64 x y = out + 2^k * jolt_pext_nat 64 x bits`, and the low `n`
+bits of `bits` are clear, so `bits = 0` after 64 passes.
+-/
+
+set_option autoImplicit false
+
+namespace JoltConstraints
+
+/-- Peel the lowest set bit `p` of the mask `2^p * (2q+1)`. -/
+theorem jolt_pext_nat_peel (p : Nat) : ∀ (fuel x q : Nat), p < fuel →
+    jolt_pext_nat fuel x (2 ^ p * (2 * q + 1)) =
+      x / 2 ^ p % 2 + 2 * jolt_pext_nat fuel x (2 ^ (p + 1) * q) := by
+  induction p with
+  | zero =>
+    intro fuel x q hp
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rw [jolt_pext_nat, jolt_pext_nat]
+    simp only [zero_add, pow_zero, pow_one, one_mul, Nat.div_one]
+    rw [if_pos (by omega), if_neg (by omega)]
+    rw [(show (2 * q + 1) / 2 = q by omega), (show 2 * q / 2 = q by omega)]
+  | succ p ih =>
+    intro fuel x q hp
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rw [jolt_pext_nat, jolt_pext_nat]
+    have e1 : 2 ^ (p + 1) * (2 * q + 1) = 2 * (2 ^ p * (2 * q + 1)) := by ring
+    have e2 : 2 ^ (p + 1 + 1) * q = 2 * (2 ^ (p + 1) * q) := by ring
+    rw [e1, e2, if_neg (by omega), if_neg (by omega),
+      Nat.mul_div_cancel_left _ (by decide), Nat.mul_div_cancel_left _ (by decide),
+      ih f (x / 2) q (by omega), Nat.div_div_eq_div_mul, pow_succ, mul_comm (2 ^ p) 2]
+
+theorem jolt_pext_nat_zero (fuel x : Nat) : jolt_pext_nat fuel x 0 = 0 := by
+  induction fuel generalizing x with
+  | zero => rfl
+  | succ fuel ih => rw [jolt_pext_nat, if_neg (by decide), Nat.zero_div, ih]
+
+/-- A low-ones mask (`n &&& (n+1) = 0`) extracts by masking. -/
+theorem jolt_pext_nat_of_low_ones : ∀ (fuel x n : Nat), n < 2 ^ fuel → n &&& (n + 1) = 0 →
+    jolt_pext_nat fuel x n = x &&& n := by
+  intro fuel
+  induction fuel with
+  | zero => intro x n hn _; simp at hn; subst hn; simp [jolt_pext_nat]
+  | succ f ih =>
+    intro x n hn hlow
+    rw [jolt_pext_nat]
+    split_ifs with hodd
+    · have hm : (n / 2) &&& (n / 2 + 1) = 0 := by
+        have := congrArg (· / 2) hlow
+        simp only [Nat.and_div_two, Nat.zero_div] at this
+        rwa [show (n + 1) / 2 = n / 2 + 1 by omega] at this
+      rw [ih (x / 2) (n / 2) (by rw [pow_succ] at hn; omega) hm]
+      apply Nat.eq_of_testBit_eq
+      intro i
+      cases i with
+      | zero => simp [Nat.testBit_zero, hodd]
+      | succ i =>
+        have hd : (x % 2 + 2 * (x / 2 &&& n / 2)) / 2 = x / 2 &&& n / 2 := by omega
+        simp only [Nat.testBit_succ, hd, Nat.and_div_two]
+    · have hn0 : n = 0 := by
+        by_contra hne
+        have h2 : (n &&& (n + 1)) % 2 = 0 := by simp [hlow]
+        have hb : n &&& (n + 1) = n := by
+          apply Nat.eq_of_testBit_eq; intro i
+          cases i with
+          | zero => simp [Nat.testBit_zero]; omega
+          | succ i =>
+            have hd : (n + 1) / 2 = n / 2 := by omega
+            simp only [Nat.testBit_succ, Nat.and_div_two, hd, Nat.and_self]
+        omega
+      subst hn0
+      simp [jolt_pext_nat_zero]
+
+
+/-- One pass of the table's general `pext` loop on the state (bits, k, out). -/
+private def pextStep (x : BitVec 64) (r : MProd (BitVec 64) (MProd Nat (BitVec 64))) :
+    MProd (BitVec 64) (MProd Nat (BitVec 64)) :=
+  if r.fst = 0 then r
+  else ⟨r.fst &&& r.fst - 1, r.snd.fst + 1,
+    r.snd.snd ||| ((x >>> r.fst.ctz.toNat) &&& 1) <<< r.snd.fst⟩
+
+private theorem forIn_eq_foldl_of {S : Type} (g : S → S) (f : Nat → S → Id (ForInStep S))
+    (hf : ∀ a r, f a r = pure (.yield (g r))) (l : List Nat) (s : S) :
+    forIn l s f = pure (l.foldl (fun r _ => g r) s) := by
+  have : f = fun _ r => pure (.yield (g r)) := funext fun a => funext fun r => hf a r
+  subst this
+  simp
+
+private theorem pext_general (x y : BitVec 64) (hy : y ≠ 0)
+    (hc : ¬ (y >>> y.ctz.toNat) &&& ((y >>> y.ctz.toNat) + 1) = 0) :
+    pext x y = ((List.range 64).foldl (fun r _ => pextStep x r) ⟨y, 0, 0⟩).snd.snd := by
+  unfold pext
+  simp only [Id.run, hy, if_false, hc, pure_bind]
+  rw [forIn_eq_foldl_of (pextStep x)]
+  · simp only [pure_bind]
+    generalize List.foldl _ _ _ = r
+    rfl
+  · rintro _ ⟨b, k, o⟩
+    by_cases h0 : b = 0
+    · subst h0; simp [pextStep]
+    · simp only [pextStep]; rw [if_neg h0, if_pos h0]
+
+private theorem two_pow_mul_odd_and_pred (p q : Nat) :
+    (2 ^ p * (2 * q + 1)) &&& (2 ^ p * (2 * q + 1) - 1) = 2 ^ (p + 1) * q := by
+  have hp : 0 < 2 ^ p := Nat.two_pow_pos p
+  have ha : 2 ^ p * (2 * q + 1) = 2 ^ (p + 1) * q + 2 ^ p := by rw [pow_succ]; ring
+  have hb : 2 ^ p * (2 * q + 1) - 1 = 2 ^ (p + 1) * q + (2 ^ p - 1) := by rw [ha]; omega
+  have h1 : 2 ^ p < 2 ^ (p + 1) := Nat.pow_lt_pow_right (by decide) (by omega)
+  rw [hb, ha]
+  apply Nat.eq_of_testBit_eq
+  intro j
+  rw [Nat.testBit_and, Nat.testBit_two_pow_mul_add _ h1, Nat.testBit_two_pow_mul_add _ (by omega),
+    Nat.testBit_two_pow_mul]
+  by_cases hj : j < p + 1
+  · simp only [hj, if_true, Nat.testBit_two_pow, Nat.testBit_two_pow_sub_one]
+    have h3 : ¬ (p + 1 ≤ j) := by omega
+    by_cases hjp : p = j
+    · subst hjp; simp
+    · simp [hjp, ge_iff_le, h3]
+  · simp only [hj, if_false, Bool.and_self]
+    simp; omega
+
+private theorem eq_two_pow_mul_odd (m p : Nat) (hlow : m % 2 ^ p = 0) (hbit : m.testBit p = true) :
+    m = 2 ^ p * (2 * (m / 2 ^ p / 2) + 1) := by
+  have h1 : (m / 2 ^ p) % 2 = 1 := by
+    have := Nat.testBit_div_two_pow (n := p) m 0
+    rw [zero_add, hbit, Nat.testBit_zero] at this
+    simpa using this
+  have h2 : 2 * (m / 2 ^ p / 2) + 1 = m / 2 ^ p := by omega
+  rw [h2, Nat.mul_div_cancel' (Nat.dvd_of_mod_eq_zero hlow)]
+
+
+/-- Loop invariant after `n` passes from `⟨y, 0, 0⟩`. -/
+private def PextInv (x y : BitVec 64) (n : Nat)
+    (r : MProd (BitVec 64) (MProd Nat (BitVec 64))) : Prop :=
+  jolt_pext_nat 64 x.toNat y.toNat =
+      r.snd.snd.toNat + 2 ^ r.snd.fst * jolt_pext_nat 64 x.toNat r.fst.toNat ∧
+    r.snd.snd.toNat < 2 ^ r.snd.fst ∧ r.snd.fst ≤ n ∧ 2 ^ n ∣ r.fst.toNat
+
+private theorem toNat_sub_one_of_ne_zero {b : BitVec 64} (hb : b ≠ 0) :
+    (b - 1).toNat = b.toNat - 1 := by
+  have : b.toNat ≠ 0 := fun h => hb (BitVec.eq_of_toNat_eq (by simpa using h))
+  rw [BitVec.toNat_sub]; simp; omega
+
+private theorem pextInv_step (x y : BitVec 64) (n : Nat)
+    (r : MProd (BitVec 64) (MProd Nat (BitVec 64)))
+    (h : PextInv x y n r) : PextInv x y (n + 1) (pextStep x r) := by
+  obtain ⟨b, k, o⟩ := r
+  obtain ⟨hJ, ho, hk, hd⟩ := h
+  simp only at hJ ho hk hd
+  by_cases hb : b = 0
+  · subst hb
+    simp only [pextStep, if_true]
+    exact ⟨hJ, ho, show k ≤ n + 1 by omega, by simp⟩
+  · simp only [pextStep, if_neg hb]
+    generalize hp : b.ctz.toNat = p
+    have hlow : b.toNat % 2 ^ p = 0 := by
+      apply Nat.eq_of_testBit_eq; intro i
+      rw [Nat.testBit_mod_two_pow, Nat.zero_testBit]
+      by_cases hi : i < p
+      · rw [BitVec.testBit_toNat, BitVec.getLsbD_false_of_lt_ctz (by omega)]; simp
+      · simp [hi]
+    have hbit : b.toNat.testBit p = true := by
+      rw [BitVec.testBit_toNat, ← hp]; exact BitVec.getLsbD_true_ctz_of_ne_zero hb
+    have hp64 : p < 64 := by
+      by_contra hc
+      have := Nat.testBit_lt_two_pow
+        (lt_of_lt_of_le b.isLt (Nat.pow_le_pow_right (by decide) (by omega : 64 ≤ p)))
+      rw [hbit] at this; exact absurd this (by decide)
+    have hnp : n ≤ p := by
+      by_contra hc
+      obtain ⟨c, hc'⟩ := hd
+      have : b.toNat.testBit p = false := by
+        rw [hc', Nat.testBit_two_pow_mul]; simp; omega
+      rw [hbit] at this; exact absurd this (by decide)
+    obtain ⟨q, hq⟩ : ∃ q, b.toNat = 2 ^ p * (2 * q + 1) := ⟨_, eq_two_pow_mul_odd _ _ hlow hbit⟩
+    have hbits : (b &&& (b - 1)).toNat = 2 ^ (p + 1) * q := by
+      rw [BitVec.toNat_and, toNat_sub_one_of_ne_zero hb, hq, two_pow_mul_odd_and_pred]
+    have hc : ((x >>> p) &&& 1).toNat = x.toNat / 2 ^ p % 2 := by
+      simp [BitVec.toNat_and, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow]
+    have hc1 : x.toNat / 2 ^ p % 2 ≤ 1 := by omega
+    have hk64 : 2 ^ k ≤ 2 ^ 63 := Nat.pow_le_pow_right (by decide) (by omega)
+    have hsh : (((x >>> p) &&& 1) <<< k).toNat = 2 ^ k * (x.toNat / 2 ^ p % 2) := by
+      rw [BitVec.toNat_shiftLeft, hc, Nat.shiftLeft_eq, Nat.mul_comm]
+      apply Nat.mod_eq_of_lt
+      have := Nat.mul_le_mul hk64 hc1
+      omega
+    have hor : (o ||| ((x >>> p) &&& 1) <<< k).toNat = o.toNat + 2 ^ k * (x.toNat / 2 ^ p % 2) := by
+      rw [BitVec.toNat_or, hsh, Nat.or_comm, ← Nat.two_pow_add_eq_or_of_lt ho]; ring
+    refine ⟨?_, ?_, by simp only; omega, ?_⟩
+    · simp only [hbits, hor]
+      rw [hJ, hq, jolt_pext_nat_peel p 64 _ q hp64, pow_succ]; ring
+    · simp only [hor]
+      have := Nat.mul_le_mul_left (2 ^ k) hc1
+      rw [pow_succ]; omega
+    · simp only [hbits]
+      exact Dvd.dvd.mul_right (Nat.pow_dvd_pow 2 (by omega)) q
+
+private theorem pextInv_foldl (x y : BitVec 64) :
+    ∀ (l : List Nat) (n : Nat) (r : MProd (BitVec 64) (MProd Nat (BitVec 64))),
+    PextInv x y n r → PextInv x y (n + l.length) (l.foldl (fun r _ => pextStep x r) r)
+  | [], n, r, h => by simpa using h
+  | _ :: l, n, r, h => by
+    simp only [List.foldl_cons, List.length_cons]
+    have := pextInv_foldl x y l (n + 1) _ (pextInv_step x y n r h)
+    rwa [show n + 1 + l.length = n + (l.length + 1) by omega] at this
+
+private theorem pext_eq_of_general (x y : BitVec 64) (hy : y ≠ 0)
+    (hc : ¬ (y >>> y.ctz.toNat) &&& ((y >>> y.ctz.toNat) + 1) = 0) :
+    pext x y = jolt_virtual_pext_value x y := by
+  rw [pext_general x y hy hc]
+  have h := pextInv_foldl x y (List.range 64) 0 ⟨y, 0, 0⟩ ⟨by simp, by simp, le_refl _, by simp⟩
+  generalize (List.range 64).foldl _ _ = r at h ⊢
+  obtain ⟨b, k, o⟩ := r
+  obtain ⟨hJ, -, -, hd⟩ := h
+  simp only [List.length_range, zero_add] at hd hJ
+  have hb0 : b.toNat = 0 := Nat.eq_zero_of_dvd_of_lt hd b.isLt
+  rw [hb0, jolt_pext_nat_zero, mul_zero, add_zero] at hJ
+  apply BitVec.eq_of_toNat_eq
+  simp only [jolt_virtual_pext_value, BitVec.toNat_ofNat, hJ]
+  exact (Nat.mod_eq_of_lt o.isLt).symm
+
+
+theorem jolt_pext_nat_two_pow_mul (f X : Nat) : ∀ (t m : Nat),
+    jolt_pext_nat (f + t) X (2 ^ t * m) = jolt_pext_nat f (X / 2 ^ t) m := by
+  intro t
+  induction t generalizing X with
+  | zero => intro m; simp
+  | succ t ih =>
+    intro m
+    rw [show f + (t + 1) = (f + t) + 1 by omega, jolt_pext_nat,
+      show 2 ^ (t + 1) * m = 2 * (2 ^ t * m) by rw [pow_succ]; ring,
+      if_neg (by omega), Nat.mul_div_cancel_left _ (by decide), ih,
+      Nat.div_div_eq_div_mul, pow_succ, mul_comm (2 ^ t) 2]
+
+private theorem toNat_mod_two_pow_ctz (b : BitVec 64) : b.toNat % 2 ^ b.ctz.toNat = 0 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  rw [Nat.testBit_mod_two_pow, Nat.zero_testBit]
+  by_cases hi : i < b.ctz.toNat
+  · rw [BitVec.testBit_toNat, BitVec.getLsbD_false_of_lt_ctz hi]; simp
+  · simp [hi]
+
+private theorem ctz_toNat_lt (b : BitVec 64) (hb : b ≠ 0) : b.ctz.toNat < 64 := by
+  by_contra hc
+  have := Nat.testBit_lt_two_pow
+    (lt_of_lt_of_le b.isLt (Nat.pow_le_pow_right (by decide) (by omega : 64 ≤ b.ctz.toNat)))
+  rw [BitVec.testBit_toNat, BitVec.getLsbD_true_ctz_of_ne_zero hb] at this
+  exact absurd this (by decide)
+
+private theorem pext_eq_of_contiguous (x y : BitVec 64) (hy : y ≠ 0)
+    (hc : (y >>> y.ctz.toNat) &&& ((y >>> y.ctz.toNat) + 1) = 0) :
+    pext x y = jolt_virtual_pext_value x y := by
+  have hpx : pext x y = (x >>> y.ctz.toNat) &&& (y >>> y.ctz.toNat) := by
+    unfold pext
+    simp only [Id.run, hy, if_false, hc, if_true, pure_bind]
+    rfl
+  rw [hpx]
+  generalize ht : y.ctz.toNat = t at hc
+  have ht64 : t < 64 := ht ▸ ctz_toNat_lt y hy
+  have hlow : y.toNat % 2 ^ t = 0 := ht ▸ toNat_mod_two_pow_ctz y
+  have hy' : y.toNat = 2 ^ t * (y.toNat / 2 ^ t) :=
+    (Nat.mul_div_cancel' (Nat.dvd_of_mod_eq_zero hlow)).symm
+  have hN : y.toNat / 2 ^ t < 2 ^ (64 - t) := by
+    rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos t), ← pow_add, show 64 - t + t = 64 by omega]
+    exact y.isLt
+  have hNlow : (y.toNat / 2 ^ t) &&& (y.toNat / 2 ^ t + 1) = 0 := by
+    have h := congrArg BitVec.toNat hc
+    simp only [BitVec.toNat_and, BitVec.toNat_add, BitVec.toNat_ushiftRight,
+      Nat.shiftRight_eq_div_pow] at h
+    rw [show (1 : BitVec 64).toNat = 1 from rfl, show (0 : BitVec 64).toNat = 0 from rfl] at h
+    by_cases hw : y.toNat / 2 ^ t + 1 < 2 ^ 64
+    · rwa [Nat.mod_eq_of_lt hw] at h
+    · have he : y.toNat / 2 ^ t = 2 ^ 64 - 1 := by
+        have : y.toNat / 2 ^ t ≤ y.toNat := Nat.div_le_self _ _
+        have := y.isLt; omega
+      rw [he, show 2 ^ 64 - 1 + 1 = 2 ^ 64 by rfl]
+      apply Nat.eq_of_testBit_eq; intro i
+      simp only [Nat.testBit_and, Nat.testBit_two_pow_sub_one, Nat.testBit_two_pow,
+        Nat.zero_testBit]
+      by_cases hi : i < 64 <;> simp [hi]; omega
+  apply BitVec.eq_of_toNat_eq
+  simp only [BitVec.toNat_and, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow,
+    jolt_virtual_pext_value, BitVec.toNat_ofNat]
+  have hs : jolt_pext_nat 64 x.toNat (2 ^ t * (y.toNat / 2 ^ t)) =
+      jolt_pext_nat (64 - t) (x.toNat / 2 ^ t) (y.toNat / 2 ^ t) := by
+    have := jolt_pext_nat_two_pow_mul (64 - t) x.toNat t (y.toNat / 2 ^ t)
+    rwa [show 64 - t + t = 64 by omega] at this
+  rw [hy', hs, Nat.mul_div_cancel_left _ (Nat.two_pow_pos t),
+    jolt_pext_nat_of_low_ones _ _ _ hN hNlow]
+  have : y.toNat / 2 ^ t < 2 ^ 64 := lt_of_le_of_lt (Nat.div_le_self _ _) y.isLt
+  exact (Nat.mod_eq_of_lt (lt_of_le_of_lt Nat.and_le_right this)).symm
+
+/-- The PEXT table's `pext` is the honest `VirtualPext` value. -/
+theorem pext_eq_jolt_virtual_pext_value (x y : BitVec 64) :
+    pext x y = jolt_virtual_pext_value x y := by
+  by_cases hy : y = 0
+  · subst hy
+    unfold pext
+    simp [Id.run, jolt_virtual_pext_value, jolt_pext_nat_zero]
+    rfl
+  by_cases hc : (y >>> y.ctz.toNat) &&& ((y >>> y.ctz.toNat) + 1) = 0
+  · exact pext_eq_of_contiguous x y hy hc
+  · exact pext_eq_of_general x y hy hc
+
+
+/-! ## PextSigned -/
+
+theorem jolt_popcount_nat_eq_sum : ∀ (f m : Nat),
+    jolt_popcount_nat f m = ∑ i ∈ Finset.range f, (m.testBit i).toNat := by
+  intro f
+  induction f with
+  | zero => intro m; rfl
+  | succ f ih =>
+    intro m
+    rw [jolt_popcount_nat, ih, Finset.sum_range_succ']
+    simp only [Nat.testBit_succ, Nat.testBit_zero]
+    rw [add_comm]; congr 1
+    by_cases h : m % 2 = 1 <;> simp [h]; omega
+
+private theorem cpopNatRec_eq_sum (b : BitVec 64) : ∀ n : Nat,
+    b.cpopNatRec n 0 = ∑ i ∈ Finset.range n, (b.getLsbD i).toNat := by
+  intro n
+  induction n with
+  | zero => rfl
+  | succ n ih => rw [BitVec.cpopNatRec_succ, BitVec.cpopNatRec_eq, ih, Finset.sum_range_succ]; simp
+
+private theorem cpop_toNat_eq (y : BitVec 64) : y.cpop.toNat = jolt_popcount_nat 64 y.toNat := by
+  rw [BitVec.toNat_cpop, cpopNatRec_eq_sum, jolt_popcount_nat_eq_sum]
+  rfl
+
+theorem jolt_popcount_nat_le : ∀ (f m : Nat), jolt_popcount_nat f m ≤ f := by
+  intro f; induction f with
+  | zero => intro m; rfl
+  | succ f ih => intro m; rw [jolt_popcount_nat]; have := ih (m / 2); omega
+
+theorem jolt_popcount_nat_zero : ∀ (f : Nat), jolt_popcount_nat f 0 = 0 := by
+  intro f; induction f with
+  | zero => rfl
+  | succ f ih => rw [jolt_popcount_nat, Nat.zero_div, ih]
+
+theorem jolt_popcount_nat_pos : ∀ (f m : Nat), m ≠ 0 → m < 2 ^ f → 0 < jolt_popcount_nat f m := by
+  intro f; induction f with
+  | zero => intro m hm hlt; simp at hlt; omega
+  | succ f ih =>
+    intro m hm hlt
+    rw [jolt_popcount_nat]
+    by_cases h : m % 2 = 1
+    · omega
+    · have := ih (m / 2) (by omega) (by rw [pow_succ] at hlt; omega); omega
+
+theorem jolt_pext_nat_lt : ∀ (f X m : Nat), jolt_pext_nat f X m < 2 ^ jolt_popcount_nat f m := by
+  intro f; induction f with
+  | zero => intro X m; simp [jolt_pext_nat, jolt_popcount_nat]
+  | succ f ih =>
+    intro X m
+    have := ih (X / 2) (m / 2)
+    rw [jolt_pext_nat, jolt_popcount_nat]
+    split_ifs with h
+    · rw [h, Nat.add_comm 1, pow_succ]; omega
+    · rw [show m % 2 = 0 by omega, zero_add]; exact this
+
+theorem jolt_pext_nat_testBit_top : ∀ (f X m : Nat), m ≠ 0 → m < 2 ^ f →
+    (jolt_pext_nat f X m).testBit (jolt_popcount_nat f m - 1) = X.testBit m.log2 := by
+  intro f; induction f with
+  | zero => intro X m hm hlt; simp at hlt; omega
+  | succ f ih =>
+    intro X m hm hlt
+    have hlt' : m / 2 < 2 ^ f := by rw [pow_succ] at hlt; omega
+    rw [jolt_pext_nat, jolt_popcount_nat]
+    split_ifs with h
+    · by_cases h0 : m / 2 = 0
+      · have hm1 : m = 1 := by omega
+        subst hm1
+        simp only [h0, jolt_pext_nat_zero, jolt_popcount_nat_zero, (Nat.log2_eq_iff (by decide)).mpr
+          (by decide : 2 ^ 0 ≤ 1 ∧ 1 < 2 ^ (0 + 1))]
+        simp [Nat.testBit_zero]
+      · have hpos := jolt_popcount_nat_pos f (m / 2) h0 hlt'
+        have hlog : m.log2 = (m / 2).log2 + 1 := by
+          rw [Nat.log2_def, if_pos (by omega)]
+        rw [h, hlog, show 1 + jolt_popcount_nat f (m / 2) - 1 =
+            (jolt_popcount_nat f (m / 2) - 1) + 1 by omega, Nat.testBit_succ, Nat.testBit_succ,
+          show (X % 2 + 2 * jolt_pext_nat f (X / 2) (m / 2)) / 2 = jolt_pext_nat f (X / 2) (m / 2)
+            by omega]
+        exact ih _ _ h0 hlt'
+    · have h0 : m / 2 ≠ 0 := by omega
+      have hlog : m.log2 = (m / 2).log2 + 1 := by
+        rw [Nat.log2_def, if_pos (by omega)]
+      rw [show m % 2 = 0 by omega, zero_add, hlog, Nat.testBit_succ]
+      exact ih _ _ h0 hlt'
+
+private theorem shift_and_one_toNat (x : BitVec 64) (p : Nat) :
+    ((x >>> p) &&& 1).toNat = x.toNat / 2 ^ p % 2 := by
+  simp [BitVec.toNat_and, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow]
+
+/-- The PEXT_SIGNED table's `pextSigned` is the honest `VirtualPextSigned` value. -/
+theorem pextSigned_eq_jolt_virtual_pext_signed_value (x y : BitVec 64) :
+    pextSigned x y = jolt_virtual_pext_signed_value x y := by
+  unfold pextSigned jolt_virtual_pext_signed_value
+  rw [cpop_toNat_eq, pext_eq_jolt_virtual_pext_value]
+  generalize hP : jolt_popcount_nat 64 y.toNat = P
+  by_cases hP0 : P = 0
+  · simp [hP0]
+  simp only [hP0, if_false]
+  have hy : y ≠ 0 := by
+    rintro rfl
+    rw [show (0 : BitVec 64).toNat = 0 from rfl, jolt_popcount_nat_zero] at hP; exact hP0 hP.symm
+  have hY : y.toNat ≠ 0 := fun h => hy (BitVec.eq_of_toNat_eq (by simpa using h))
+  have hP64 : P ≤ 64 := hP ▸ jolt_popcount_nat_le 64 y.toNat
+  have hJ : jolt_pext_nat 64 x.toNat y.toNat < 2 ^ P := hP ▸ jolt_pext_nat_lt 64 x.toNat y.toNat
+  have hPle : 2 ^ P ≤ 2 ^ 64 := Nat.pow_le_pow_right (by decide) hP64
+  have hE : (jolt_virtual_pext_value x y).toNat = jolt_pext_nat 64 x.toNat y.toNat := by
+    simp only [jolt_virtual_pext_value, BitVec.toNat_ofNat]; exact Nat.mod_eq_of_lt (by omega)
+  have htop : (jolt_virtual_pext_value x y).getLsbD (P - 1) = x.toNat.testBit y.toNat.log2 := by
+    rw [← BitVec.testBit_toNat, hE, ← hP]; exact jolt_pext_nat_testBit_top 64 _ _ hY y.isLt
+  have hsign : (windowSignBit x y = 1) ↔ x.toNat.testBit y.toNat.log2 = true := by
+    unfold windowSignBit
+    rw [if_neg hy, ← BitVec.toNat_inj, shift_and_one_toNat, Nat.testBit_eq_decide_div_mod_eq]
+    simp
+  rw [htop]
+  by_cases hb : x.toNat.testBit y.toNat.log2 = true
+  · rw [if_pos (hsign.mpr hb), if_pos hb]
+    apply BitVec.eq_of_toNat_eq
+    have hsub : (((1#128 <<< 64) - (1#128 <<< P)).setWidth 64).toNat = 2 ^ 64 - 2 ^ P := by
+      rw [BitVec.toNat_setWidth, BitVec.toNat_sub, BitVec.toNat_shiftLeft, BitVec.toNat_shiftLeft,
+        show (1#128).toNat = 1 from rfl, Nat.shiftLeft_eq, Nat.shiftLeft_eq, Nat.one_mul,
+        Nat.one_mul]
+      have hP2 : 2 ≤ 2 ^ P := by
+        calc 2 = 2 ^ 1 := rfl
+          _ ≤ 2 ^ P := Nat.pow_le_pow_right (by decide) (by omega)
+      generalize 2 ^ P = Q at *
+      omega
+    have hlow : (BitVec.ofNat 64 (2 ^ P - 1)).toNat = 2 ^ P - 1 := by
+      rw [BitVec.toNat_ofNat]; exact Nat.mod_eq_of_lt (by omega)
+    have hsplit : 2 ^ 64 - 2 ^ P = 2 ^ P * (2 ^ (64 - P) - 1) := by
+      rw [Nat.mul_sub_one, ← pow_add, show P + (64 - P) = 64 by omega]
+    rw [BitVec.toNat_add, BitVec.toNat_or, BitVec.toNat_not, hlow, hE, hsub,
+      show 2 ^ 64 - 1 - (2 ^ P - 1) = 2 ^ 64 - 2 ^ P by omega, hsplit, Nat.or_comm,
+      ← Nat.two_pow_add_eq_or_of_lt hJ, ← hsplit, Nat.mod_eq_of_lt (by omega)]
+    omega
+  · have hns : ¬ windowSignBit x y = 1 := fun h => hb (hsign.mp h)
+    rw [if_neg hns, if_neg hb]; simp
+
+end JoltConstraints
diff --git a/JoltConstraints/Tests/LookupShiftMask.lean b/JoltConstraints/Tests/LookupShiftMask.lean
new file mode 100644
index 0000000..7960077
--- /dev/null
+++ b/JoltConstraints/Tests/LookupShiftMask.lean
@@ -0,0 +1,99 @@
+import JoltConstraints.Constraints.LookupEntryProofHelpers
+
+set_option autoImplicit false
+
+/-!
+Counterexamples and checks for the per-table lemmas in
+`JoltConstraints/Constraints/LookupEntryProofHelpers.lean` left as `sorry`.
+Not part of the default build; check with `lake env lean JoltConstraints/Tests/LookupShiftMask.lean`.
+
+Shift/rotate tables (`VirtualSRL`, `VirtualSRA`, `VirtualSRLW`, `VirtualSRAW`,
+`VirtualROTR`, `VirtualROTRW`) read the right operand as a right-shift bitmask,
+while the honest outputs shift by `ctz` of whatever mask the row carries.
+Source `4`, mask `2`: index `interleave 4 2 = 36`; entries 0/0/0/0/4/4 versus
+output `2` for all six. `VirtualSRLW` with mask `0` (register form): index 34,
+entry 0, output `5`.
+-/
+
+open JoltConstraints
+
+#eval (HonestWitness.interleaveLookupOperands 4 2).toNat
+#eval (HonestWitness.interleaveLookupOperands 5 0).toNat
+#eval (jolt_virtual_srl_value 4 2, jolt_virtual_srli_value 4 2, jolt_virtual_sra_value 4 2,
+  jolt_virtual_srlw_value 4 2, jolt_virtual_sraw_value 4 2, jolt_virtual_rotri_value 4 2,
+  jolt_virtual_rotriw_value 4 2, jolt_virtual_srlw_value 5 0, jolt_virtual_srliw_value 5 0)
+
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualSRL ⟨36, by decide⟩ : ℚ) = 0 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualSRA ⟨36, by decide⟩ : ℚ) = 0 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualSRLW ⟨36, by decide⟩ : ℚ) = 0 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualSRAW ⟨36, by decide⟩ : ℚ) = 0 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualROTR ⟨36, by decide⟩ : ℚ) = 4 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualROTRW ⟨36, by decide⟩ : ℚ) = 4 := by decide +kernel
+set_option maxRecDepth 8192 in
+example : (lookupTableEntry .VirtualSRLW ⟨34, by decide⟩ : ℚ) = 0 := by decide +kernel
+
+/-! Row-level refutation of `lookupEntryCorrect_VirtualSRL`: a one-row program
+`VirtualSRLI v32, v33, 2` (mask immediate `2`, not a right-shift bitmask) run
+from any state with `v33 = 4`. `OperandsRepresentable` only asks `2 < 2^64`. -/
+namespace SRLICounterexample
+
+def instruction : JoltISA.Instr := .VirtualSRLI (.vreg 32) (.vreg 33) 2
+
+def bytecodeRow : JoltProgramRow :=
+  { inputInstruction := instruction
+    registerOperandsCanonical := by decide
+    isBytecodeTemplate := True.intro
+    operandsRepresentable := by
+      simp [finalProgramRowInstruction, instruction, JoltISA.Instr.OperandsRepresentable]
+    address := 0x80000000
+    virtualSequenceRemaining := some 0
+    isFirstInSequence := true
+    isCompressed := false }
+
+def program (state : SailJoltState) : JoltProgram :=
+  { expandedBytecode := #[bytecodeRow]
+    initialState := state }
+
+noncomputable def visit (state : SailJoltState) : JoltTraceRow (program state) :=
+  { rowIndex := ⟨0, by simp [program]⟩
+    runtimeAdvice := ()
+    preState := state
+    postState := { state with
+      vregs := fun r => if r = 32 then (jolt_virtual_srli_value (state.vregs 33) 2) else state.vregs r }
+    executes := rfl
+    storeMemoryPresent := True.intro }
+
+example (state : SailJoltState) :
+    JoltMetadata.lookupTable (rowInstruction (visit state)) = some .VirtualSRL := rfl
+
+example (state : SailJoltState) (h : state.vregs 33 = 4) :
+    HonestWitness.rowLookupOutput (visit state) = 2 := by
+  change jolt_virtual_srli_value (state.vregs 33) 2 = 2
+  rw [h]; decide +kernel
+
+example (state : SailJoltState) (h : state.vregs 33 = 4) :
+    rowLookupAddress (visit state) = ⟨36, by decide⟩ := by
+  change (HonestWitness.interleaveLookupOperands (state.vregs 33) (BitVec.ofNat 64 2)).toFin = _
+  rw [h]; decide +kernel
+
+set_option maxRecDepth 8192 in
+theorem not_lookupEntryCorrect (state : SailJoltState) (h : state.vregs 33 = 4) :
+    ¬ LookupEntryCorrect ℚ .VirtualSRL (visit state) := by
+  unfold LookupEntryCorrect
+  have ha : rowLookupAddress (visit state) = ⟨36, by decide⟩ := by
+    change (HonestWitness.interleaveLookupOperands (state.vregs 33) (BitVec.ofNat 64 2)).toFin = _
+    rw [h]; decide +kernel
+  have ho : HonestWitness.rowLookupOutput (visit state) = 2 := by
+    change jolt_virtual_srli_value (state.vregs 33) 2 = 2
+    rw [h]; decide +kernel
+  have he : (lookupTableEntry .VirtualSRL ⟨36, by decide⟩ : ℚ) = 0 := by decide +kernel
+  rw [ha, ho, he]
+  simp
+
+end SRLICounterexample
diff --git a/JoltConstraints/model_review.md b/JoltConstraints/model_review.md
index f536fb2..b4aaebb 100644
--- a/JoltConstraints/model_review.md
+++ b/JoltConstraints/model_review.md
@@ -218,7 +218,7 @@ are **deferred work or documented modeling choices**, not established proofs.
 | [program.lean](program.lean), two `FIXME`s | `rowValid` (including writable jump destinations, canonical x0 writes, and jumps at the end of expansions) and `noEarlyNextPCChange` use `sorry` and are false for arbitrary arrays. Connect rows to Rust source expansion and native rewrites, then prove the claims for those outputs. |
 | [program.lean](program.lean), `WARNING` | Rust currently permits source-PC wraparound; `SequenceLayout.addressAdvanceNoWrap` is a temporary assumption pending the fix tracked by [Jolt issue #1949](https://github.com/a16z/jolt/issues/1949). |
 | [trace.lean](trace.lean), `FIXME` | Derive `hostIOPreservesPC` from live `execInstr` using the new Sail byte-read frame; it is still an explicit trace-row obligation. |
-| [LookupOutputEqInstructionReadRaf.lean](Constraints/LookupOutputEqInstructionReadRaf.lean), `FIXME` | Connect each now-defined fixed table entry to `HonestWitness.rowLookupOutput` for execution rows. |
+| [LookupEntryProofHelpers.lean](Constraints/LookupEntryProofHelpers.lean), `FIXME` | Constraint (39) is proved modulo six per-table `sorry`s. `lookupEntryCorrect_{VirtualSRL,VirtualSRA,VirtualSRLW,VirtualSRAW,VirtualROTR,VirtualROTRW}` are false for arbitrary bytecode (non-bitmask mask operand; see `JoltConstraints/Tests/LookupShiftMask.lean`) and need the expander's bitmask invariant. |
 | [RamValEqInitialPlusPrefixRamInc.lean](Constraints/RamValEqInitialPlusPrefixRamInc.lean), `FIXME` | Relate captured RAM reads to initialized memory and prefix RAM history. |
 | [RamValFinalEqInitialPlusRamInc.lean](Constraints/RamValFinalEqInitialPlusRamInc.lean), `FIXME` | Establish Rust memory-history and terminal-state correspondence. |
 | [RamOutputEqPublicIo.lean](Constraints/RamOutputEqPublicIo.lean), `FIXME` | Relate Rust's final public output to the Lean witness. |