SETH ⇒ OVC sparsification bundle 5: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_04

set_option autoImplicit true

/-! Link input protection, length scanning and tail copying into one program. -/
namespace WordRAM.Conjectures.InputRelocation

private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def scanSetup : List SourceInstruction :=
  [.copy (.direct 6) (reg 1),
   .binary .sub (.direct 5) (reg 0) (.immediate 15),
   .copy (.direct 1) (.immediate 3)]

def copySetup : List SourceInstruction :=
  [.binary .sub (.direct 7) (reg 1) (.immediate 1),
   .copy (.direct 3) (.immediate 0),
   .branch .le (reg 7) (.immediate 15) 54,
   .binary .sub (.direct 3) (reg 7) (.immediate 15),
   .copy (.direct 1) (.immediate 16),
   .binary .add (.direct 2) (reg 5) (.immediate 15)]

/-- One fixed source program. On termination register 5 is the relocated input
base, register 6 the variable count, and register 7 the serialized input length. -/
def algorithm : Algorithm :=
  ⟨InputBootstrap.algorithm.code.map (SourceInstruction.returnTo 34) ++ scanSetup ++
    ((InputScan.algorithm.code.map (SourceInstruction.returnTo 13)).map
      (SourceInstruction.relocate 37)) ++ copySetup ++
    MemoryCopy.algorithm.code.map (SourceInstruction.relocate 56), 6, by decide⟩

private theorem program_eq (w : Width) : algorithm.program w =
    (InputBootstrap.algorithm.program w).map (Instruction.returnTo 34) ++
    (scanSetup.map (SourceInstruction.compile w) ++
    (((InputScan.algorithm.program w).map (Instruction.returnTo 13)).map (Instruction.relocate 37) ++
    (copySetup.map (SourceInstruction.compile w) ++
    (MemoryCopy.algorithm.program w).map (Instruction.relocate 56)))) := by rfl

theorem prepares_scan (s : State w) (backup : Nat) (pc : s.pc = 34) (live : s.halted = false)
    (fits : backup + 15 < 2 ^ w.bits)
    (pointer : s.mem 0 = BitVec.ofNat w.bits (backup + 15)) :
    let t := run widthConstant (algorithm.program w) 3 s
    t.pc = 37 ∧ t.halted = false ∧ t.ticks = s.ticks + 3 ∧
    t.mem 1 = BitVec.ofNat w.bits 3 ∧ t.mem 2 = s.mem 2 ∧
    t.mem 5 = BitVec.ofNat w.bits backup ∧ t.mem 6 = s.mem 1 ∧
    (∀ a, a ≠ 1 → a ≠ 5 → a ≠ 6 → t.mem a = s.mem a) := by
  have sub : BitVec.ofNat w.bits (backup + 15) - 15#w.bits = BitVec.ofNat w.bits backup := by
    rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
    simp
  simp [algorithm, Algorithm.program, InputBootstrap.algorithm, InputBootstrap.header,
    SavePrefix.code, scanSetup, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
    pc, live, pointer, sub, Nat.add_assoc, List.getElem?_cons_zero, List.getElem?_cons_succ]
  intro a h1 h5 h6
  simp [h1, h5, h6]

def setupCost (length : Nat) := if length ≤ 15 then 5 else 6

theorem prepares_copy (s : State w) (length backup : Nat)
    (pc : s.pc = 50) (live : s.halted = false) (wide : 6 ≤ w.bits)
    (lengthFits : length + 1 < 2 ^ w.bits)
    (endPointer : s.mem 1 = BitVec.ofNat w.bits (length + 1))
    (basePointer : s.mem 5 = BitVec.ofNat w.bits backup) :
    let t := run widthConstant (algorithm.program w) (setupCost length) s
    t.pc = 56 ∧ t.halted = false ∧ t.ticks = s.ticks + setupCost length ∧
    t.mem 1 = BitVec.ofNat w.bits 16 ∧ t.mem 2 = BitVec.ofNat w.bits (backup + 15) ∧
    t.mem 3 = BitVec.ofNat w.bits (length - 15) ∧ t.mem 7 = BitVec.ofNat w.bits length ∧
    (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 3 → a ≠ 7 → t.mem a = s.mem a) := by
  have smallFit : 15 < 2 ^ w.bits := by
    have h := Nat.pow_le_pow_right (n := 2) (by decide) wide
    omega
  have lenSub : BitVec.ofNat w.bits (length + 1) - 1#w.bits = BitVec.ofNat w.bits length := by
    rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
    simp
  by_cases short : length ≤ 15
  · simp [algorithm, Algorithm.program, InputBootstrap.algorithm, InputBootstrap.header,
      SavePrefix.code, scanSetup, copySetup, InputScan.algorithm, SourceInstruction.compile,
      SourceOperand.compile, SourceInstruction.relocate, SourceInstruction.returnTo,
      reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
      Comparison.test, pc, live, endPointer, basePointer, lenSub, setupCost, short,
      Nat.mod_eq_of_lt (show length < 2 ^ w.bits by omega), Nat.mod_eq_of_lt smallFit,
      Nat.sub_eq_zero_of_le short, Nat.add_assoc]
    constructor
    · rw [← BitVec.ofNat_add]
    · intro a h1 h2 h3 h7; simp [h1, h2, h3, h7]
  · have countSub : BitVec.ofNat w.bits length - 15#w.bits = BitVec.ofNat w.bits (length - 15) := by
      rw [BitVec.ofNat_sub_ofNat_of_le _ _ smallFit (by omega)]
    simp [algorithm, Algorithm.program, InputBootstrap.algorithm, InputBootstrap.header,
      SavePrefix.code, scanSetup, copySetup, InputScan.algorithm, SourceInstruction.compile,
      SourceOperand.compile, SourceInstruction.relocate, SourceInstruction.returnTo,
      reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
      Comparison.test, pc, live, endPointer, basePointer, lenSub, countSub, setupCost, short,
      Nat.mod_eq_of_lt (show length < 2 ^ w.bits by omega), Nat.mod_eq_of_lt smallFit, Nat.add_assoc]
    constructor
    · rw [← BitVec.ofNat_add]
    · intro a h1 h2 h3 h7; simp [h1, h2, h3, h7]

private theorem trace_of_ticks (s : State w) (fuel : Nat)
    (cost : (run widthConstant (algorithm.program w) fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant (algorithm.program w) fuel s
      (run widthConstant (algorithm.program w) fuel s) := by
  obtain ⟨t, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) fuel s
  have hc := runs_cost trace
  have : t = fuel := by omega
  subst t
  exact trace

private theorem stored_of_get (xs : List (Word w)) (address : Nat)
    (h : ∀ i (hi : i < xs.length), mem (address + i) = xs[i]) :
    VectorBuilder.Stored mem address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    refine ⟨?_, ?_⟩
    · have hh := h 0 (by simp)
      change mem (address + 0) = x at hh
      exact hh
    apply ih (address + 1)
    intro i hi
    have hh := h (i + 1) (by simpa using hi)
    change mem (address + (i + 1)) = xs[i] at hh
    simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hh

private theorem scan_embedded (w : Width) :
    EmbedsAt ((InputScan.algorithm.program w).map (Instruction.returnTo 13)) (algorithm.program w) 37 := by
  let pre := (InputBootstrap.algorithm.program w).map (Instruction.returnTo 34) ++
    scanSetup.map (SourceInstruction.compile w)
  have he := embeds_append pre ((InputScan.algorithm.program w).map (Instruction.returnTo 13))
    (copySetup.map (SourceInstruction.compile w) ++ (MemoryCopy.algorithm.program w).map (Instruction.relocate 56))
  have len : pre.length = 37 := by rfl
  rw [len] at he
  rw [program_eq]
  simpa only [pre, List.append_assoc] using he

private theorem copy_embedded (w : Width) :
    EmbedsAt (MemoryCopy.algorithm.program w) (algorithm.program w) 56 := by
  let pre := ((InputBootstrap.algorithm.program w).map (Instruction.returnTo 34) ++
    scanSetup.map (SourceInstruction.compile w)) ++
    (((InputScan.algorithm.program w).map (Instruction.returnTo 13)).map (Instruction.relocate 37) ++
      copySetup.map (SourceInstruction.compile w))
  have he := embeds_append pre (MemoryCopy.algorithm.program w) []
  have len : pre.length = 56 := by rfl
  rw [len] at he
  rw [program_eq]
  simpa only [pre, List.append_assoc, List.append_nil] using he

/-- Starting with the actual serialized input, one fixed program relocates it
into a contiguous high-memory buffer. Every setup instruction and subroutine
call is included in the trace and cost bound. -/
theorem relocates (w : Width) (f : SATInstance) (wide : 6 ≤ w.bits)
    (inputBelow : f.encode.length < InputBootstrap.base w) :
    ∃ cost, cost ≤ 10 * f.clauses.length + 7 * (f.encode.length - 15) + 47 ∧ ∃ final : State w,
      Runs widthConstant (algorithm.program w) cost (initialState w f.encode) final ∧
      final.halted = true ∧ final.mem 5 = BitVec.ofNat w.bits (InputBootstrap.base w) ∧
      final.mem 6 = BitVec.ofNat w.bits f.variables ∧ final.mem 7 = BitVec.ofNat w.bits f.encode.length ∧
      (∀ i, i < f.encode.length → final.mem (InputBootstrap.base w + i) =
        BitVec.ofNat w.bits (f.encode[i]?.getD 0)) ∧
      (∀ a, 16 ≤ a →
        (a < InputBootstrap.base w ∨ InputBootstrap.base w + max 15 f.encode.length ≤ a) →
        final.mem a = (initialState w f.encode).mem a) := by
  let original := initialState w f.encode
  let backup := InputBootstrap.base w
  have bounds := InputBootstrap.base_bounds wide
  have capacity : 2 ^ w.bits = 2 * backup := by
    have he : w.bits = (w.bits - 1) + 1 := by omega
    calc
      2 ^ w.bits = 2 ^ ((w.bits - 1) + 1) := congrArg (fun k => 2 ^ k) he
      _ = 2 * backup := by simp [backup, InputBootstrap.base, Nat.pow_succ, Nat.mul_comm]
  have lengthFit : f.encode.length + 1 < 2 ^ w.bits := by omega
  obtain ⟨boot, bootTrace, bootHalt, bootPointer, bootSaved, bootFrame⟩ :=
    InputBootstrap.protects original rfl rfl wide
  let released := boot.returnTo 34
  have first : Runs widthConstant (algorithm.program w) 34 original released := by
    rw [program_eq]
    simpa only [released, State.returnTo, initialState, original, Bool.false_eq_true, ↓reduceIte] using
      (bootTrace.returnTo 34).append_code
        (scanSetup.map (SourceInstruction.compile w) ++
        (((InputScan.algorithm.program w).map (Instruction.returnTo 13)).map (Instruction.relocate 37) ++
        (copySetup.map (SourceInstruction.compile w) ++ (MemoryCopy.algorithm.program w).map (Instruction.relocate 56))))
  have releaseMem : released.mem = boot.mem := by simp [released, State.returnTo, bootHalt]
  obtain ⟨spc, slive, sticks, sp, sc, sb, sn, sf⟩ := prepares_scan released backup
    (by simp [released, State.returnTo, bootHalt]) (by simp [released, State.returnTo, bootHalt])
    bounds.2 (by simpa only [releaseMem] using bootPointer)
  let readyScan := run widthConstant (algorithm.program w) 3 released
  let scanEntry : State w := { readyScan with pc := 0 }
  have prepSaved : ∀ i, i < 15 → scanEntry.mem (backup + i) = original.mem (i + 1) := by
    intro i hi
    have h := sf (backup + i) (by omega) (by omega) (by omega)
    rw [releaseMem] at h
    exact h.trans (bootSaved i hi)
  have prepTail : ∀ a, 15 < a → a ≤ f.encode.length → scanEntry.mem a = original.mem a := by
    intro a lo hi
    have h := sf a (by omega) (by omega) (by omega)
    rw [releaseMem] at h
    exact h.trans (bootFrame a (by omega) (Or.inl (by omega)))
  have prepCount : scanEntry.mem 2 = BitVec.ofNat w.bits f.clauses.length := by
    rw [sc, releaseMem, bootFrame 2 (by decide) (Or.inl (by omega))]
    simp [original, initialState, SATInstance.encode]
  have prepVariables : scanEntry.mem 6 = BitVec.ofNat w.bits f.variables := by
    rw [sn, releaseMem, bootFrame 1 (by decide) (Or.inl (by omega))]
    simp [original, initialState, SATInstance.encode]
  obtain ⟨scanCost, scanBound, scanned, scanTrace, scanHalt, scanEnd, _, scanFrame⟩ :=
    InputScan.scans f.clauses scanEntry 3 backup rfl slive (by decide) (by omega) bounds.2
      (by have hl := InputScan.encoding_length f; omega) sp prepCount sb
      (InputScan.encoded_protected w f scanEntry.mem backup prepSaved prepTail)
  let afterScan := (scanned.returnTo 13).relocate 37
  have scanLinked : Runs widthConstant (algorithm.program w) scanCost readyScan afterScan := by
    have he : (scanEntry.returnTo 13).relocate 37 = readyScan := by
      have hs : scanEntry.halted = false := slive
      simp only [State.returnTo, hs, Bool.false_eq_true, ↓reduceIte]
      change { readyScan with pc := 37 } = readyScan
      have hp : readyScan.pc = 37 := spc
      rw [← hp]
    simpa only [he] using (scanTrace.returnTo 13).relocate (scan_embedded w)
  have scanMem : afterScan.mem = scanned.mem := by
    simp [afterScan, State.returnTo, State.relocate, scanHalt]
  have afterBase : afterScan.mem 5 = BitVec.ofNat w.bits backup := by
    rw [scanMem, scanFrame 5 (by decide)]
    exact sb
  have endPointer : afterScan.mem 1 = BitVec.ofNat w.bits (f.encode.length + 1) := by
    rw [scanMem, scanEnd]
    congr 1
    have hl := InputScan.encoding_length f
    omega
  obtain ⟨cpc, clive, cticks, cp, cd, cc, clen, cf⟩ := prepares_copy afterScan f.encode.length backup
    (by simp [afterScan, State.returnTo, State.relocate, scanHalt])
    (by simp [afterScan, State.returnTo, State.relocate, scanHalt]) wide lengthFit endPointer afterBase
  let readyCopy := run widthConstant (algorithm.program w) (setupCost f.encode.length) afterScan
  let copyEntry : State w := { readyCopy with pc := 0 }
  have savedPrefix : ∀ i, i < 15 → copyEntry.mem (backup + i) = original.mem (i + 1) := by
    intro i hi
    have h := cf (backup + i) (by omega) (by omega) (by omega) (by omega)
    rw [scanMem, scanFrame _ (by omega)] at h
    exact h.trans (prepSaved i hi)
  have savedTail : ∀ a, 16 ≤ a → a ≤ f.encode.length → copyEntry.mem a = original.mem a := by
    intro a lo hi
    have h := cf a (by omega) (by omega) (by omega) (by omega)
    rw [scanMem, scanFrame a (by omega)] at h
    exact h.trans (prepTail a (by omega) hi)
  let tailWords : List (Word w) := List.ofFn fun i : Fin (f.encode.length - 15) => original.mem (16 + i.val)
  have tailLength : tailWords.length = f.encode.length - 15 := by simp [tailWords]
  have copyInput : VectorBuilder.Stored copyEntry.mem 16 tailWords := by
    apply stored_of_get
    intro i hi
    have bound : i < f.encode.length - 15 := by simpa only [tailLength] using hi
    simpa [tailWords] using savedTail (16 + i) (by omega) (by omega)
  obtain ⟨copied, copyTrace, copyHalt, outputWords, copyFrame⟩ :=
    MemoryCopy.copies tailWords copyEntry 16 (backup + 15) rfl clive (by decide)
      (by rw [tailLength]; omega) (by rw [tailLength]; omega) cp cd
      (by simpa only [tailLength] using cc) copyInput
  have copyLinked : Runs widthConstant (algorithm.program w) (7 * tailWords.length + 2)
      readyCopy (copied.relocate 56) := by
    have he : copyEntry.relocate 56 = readyCopy := by
      change { readyCopy with pc := 56 } = readyCopy
      have hp : readyCopy.pc = 56 := cpc
      rw [← hp]
    simpa only [he] using copyTrace.relocate (copy_embedded w)
  have copyLow : ∀ a, 5 ≤ a → a ≤ 7 → copied.mem a = copyEntry.mem a := by
    intro a lo hi
    exact copyFrame a lo (Or.inl (by omega))
  have finalBase : copied.mem 5 = BitVec.ofNat w.bits backup := by
    rw [copyLow 5 (by decide) (by decide), cf 5 (by decide) (by decide) (by decide) (by decide)]
    exact afterBase
  have finalVariables : copied.mem 6 = BitVec.ofNat w.bits f.variables := by
    rw [copyLow 6 (by decide) (by decide), cf 6 (by decide) (by decide) (by decide) (by decide),
      scanMem, scanFrame 6 (by decide)]
    exact prepVariables
  have finalLength : copied.mem 7 = BitVec.ofNat w.bits f.encode.length := by
    rw [copyLow 7 (by decide) (by decide)]
    exact clen
  refine ⟨34 + 3 + scanCost + setupCost f.encode.length + (7 * tailWords.length + 2), ?_,
    copied.relocate 56,
    (((first.append (trace_of_ticks released 3 sticks)).append scanLinked).append
      (trace_of_ticks afterScan (setupCost f.encode.length) cticks)).append copyLinked,
    copyHalt, finalBase, finalVariables, finalLength, ?_, ?_⟩
  · have bound : setupCost f.encode.length ≤ 6 := by unfold setupCost; split <;> omega
    rw [tailLength]
    omega
  · intro i hi
    change copied.mem (backup + i) = _
    have read : copied.mem (backup + i) = original.mem (i + 1) := by
      by_cases small : i < 15
      · exact (copyFrame (backup + i) (by omega) (Or.inl (by omega))).trans (savedPrefix i small)
      · have h := VectorBuilder.Stored.get tailWords (backup + 15) outputWords (i - 15)
          (by rw [tailLength]; omega)
        simp only [tailWords, List.getElem_ofFn] at h
        have addr : backup + 15 + (i - 15) = backup + i := by omega
        have src : 16 + (i - 15) = i + 1 := by omega
        simpa only [addr, src] using h
    simpa [original, initialState] using read
  · intro a ha outside
    change copied.mem a = original.mem a
    have h := copyFrame a (by omega) (by rw [tailLength]; omega)
    rw [cf a (by omega) (by omega) (by omega) (by omega), scanMem, scanFrame a (by omega),
      sf a (by omega) (by omega) (by omega), releaseMem] at h
    exact h.trans (bootFrame a (by omega) (by omega))

/-- Turn the relocation's pointwise memory result into the standard consecutive
buffer representation consumed by later verified programs. -/
theorem stored_input (w : Width) (input : List Nat) (mem : Memory w) (backup : Nat)
    (h : ∀ i, i < input.length → mem (backup + i) = BitVec.ofNat w.bits (input[i]?.getD 0)) :
    VectorBuilder.Stored mem backup (input.map (BitVec.ofNat w.bits)) := by
  apply stored_of_get
  intro i hi
  have bound : i < input.length := by simpa using hi
  have hh := h i bound
  simpa only [List.getElem_map, List.getElem?_eq_getElem bound, Option.getD_some] using hh

/-- The relocated formula immediately satisfies the clause-table builder's
input invariant, with its two header words skipped. -/
theorem encoded_clauses (w : Width) (f : SATInstance) (mem : Memory w) (backup : Nat)
    (h : ∀ i, i < f.encode.length → mem (backup + i) = BitVec.ofNat w.bits (f.encode[i]?.getD 0)) :
    MaskTable.Encoded mem (backup + 2) f.clauses := by
  have stored := stored_input w f.encode mem backup h
  rw [← MaskTable.words_encode w f] at stored
  have tail : VectorBuilder.Stored mem (backup + 2) (MaskTable.words w f.clauses) := by
    simpa [Nat.add_assoc] using stored.2.2
  apply MaskTable.encoded_of_words
  intro i hi
  have entry := VectorBuilder.Stored.get _ _ tail i hi
  simpa only [List.getElem?_eq_getElem hi, Option.getD_some] using entry

end WordRAM.Conjectures.InputRelocation

/-! Word-level obligations for simulating a narrower RAM. These are semantic
identities, not yet a compiled instruction simulation or runtime transfer. -/
namespace WordRAM.Conjectures.WidthSimulation

variable {narrow wide : Width}

/-- Narrow words are represented by their unsigned value in the wider word. -/
def lift (wide : Width) (x : Word narrow) : Word wide := x.setWidth wide.bits

/-- Keeping only the original word's low bits implements its modular arithmetic. -/
def mask (narrow wide : Width) : Word wide := (BitVec.allOnes narrow.bits).setWidth wide.bits

theorem lift_value (h : narrow.bits ≤ wide.bits) (x : Word narrow) :
    (lift wide x).toNat = x.toNat := BitVec.toNat_setWidth_of_le h

theorem project_lift (h : narrow.bits ≤ wide.bits) (x : Word narrow) :
    (lift wide x).setWidth narrow.bits = x := by
  simp [lift, BitVec.setWidth_setWidth_of_le _ h]

theorem mask_project (h : narrow.bits ≤ wide.bits) (x : Word wide) :
    x &&& mask narrow wide = lift wide (x.setWidth narrow.bits : Word narrow) := by
  apply BitVec.eq_of_getLsbD_eq
  intro i
  simp only [mask, lift, BitVec.getLsbD_and, BitVec.getLsbD_setWidth, BitVec.getLsbD_allOnes]
  by_cases hi : i < narrow.bits
  · have hw : i < wide.bits := Nat.lt_of_lt_of_le hi h
    simp [hi, hw]
  · simp [hi]

theorem project_sub (h : narrow.bits ≤ wide.bits) (x y : Word wide) :
    (x - y).setWidth narrow.bits = x.setWidth narrow.bits - y.setWidth narrow.bits := by
  simp only [BitVec.sub_eq_add_neg, BitVec.neg_eq_not_add, BitVec.setWidth_add _ _ h,
    BitVec.setWidth_not h, BitVec.setWidth_ofNat_of_le h]

/-- The mask can be constructed using a wide NOT and right-shift instruction;
it does not require a new native constant. -/
theorem mask_from_shift (h : narrow.bits ≤ wide.bits) :
    (~~~(0 : Word wide)) >>> (wide.bits - narrow.bits) = mask narrow wide := by
  apply BitVec.eq_of_getLsbD_eq
  intro i
  simp only [mask, BitVec.getLsbD_ushiftRight, BitVec.getLsbD_not,
    BitVec.getLsbD_setWidth, BitVec.getLsbD_allOnes]
  by_cases hi : i < narrow.bits
  · have hw : i < wide.bits := Nat.lt_of_lt_of_le hi h
    have hs : i + (wide.bits - narrow.bits) < wide.bits := by omega
    simp [hi, hw, hs, Nat.add_comm]
  · have hs : ¬ i + (wide.bits - narrow.bits) < wide.bits := by omega
    simp [hi, hs, Nat.add_comm]

/-- Compile an arbitrary fixed natural literal at the wide width, then mask
it to obtain precisely its original narrow compilation. -/
theorem immediate (h : narrow.bits ≤ wide.bits) (literal : Nat) :
    BitVec.ofNat wide.bits literal &&& mask narrow wide =
      lift wide (BitVec.ofNat narrow.bits literal : Word narrow) := by
  rw [mask_project h, BitVec.setWidth_ofNat_of_le h]

/-- Every binary instruction, including multiplication and both shifts, is
correct when wide execution is followed by a low-bit mask. -/
theorem binary (h : narrow.bits ≤ wide.bits) (op : BinOp m) (x y : Word narrow) :
    BinOp.eval op (lift wide x) (lift wide y) &&& mask narrow wide =
      lift wide (BinOp.eval op x y) := by
  rw [mask_project h]
  apply congrArg (fun z : Word narrow => lift wide z)
  cases op with
  | add => simp only [BinOp.eval, BitVec.setWidth_add _ _ h, project_lift h]
  | sub => simp only [BinOp.eval, project_sub h, project_lift h]
  | mul _ => simp only [BinOp.eval, BitVec.setWidth_mul _ _ h, project_lift h]
  | band => simp only [BinOp.eval, BitVec.setWidth_and, project_lift h]
  | bor => simp only [BinOp.eval, BitVec.setWidth_or, project_lift h]
  | shl => simp only [BinOp.eval, lift_value h, BitVec.setWidth_shiftLeft_of_le h, project_lift h]
  | shr =>
    simp only [BinOp.eval, lift]
    rw [← BitVec.setWidth_ushiftRight h, BitVec.setWidth_setWidth_of_le _ h, BitVec.setWidth_eq]
    rw [BitVec.toNat_setWidth_of_le h]

theorem bitNot (h : narrow.bits ≤ wide.bits) (x : Word narrow) :
    (~~~lift wide x) &&& mask narrow wide = lift wide (~~~x) := by
  rw [mask_project h]
  simp only [BitVec.setWidth_not h, project_lift h]

/-- Unsigned comparisons need no adjustment on zero-extended operands. -/
theorem comparison (h : narrow.bits ≤ wide.bits) (cmp : Comparison) (x y : Word narrow) :
    cmp.test (lift wide x) (lift wide y) = cmp.test x y := by
  cases cmp with
  | lt => simp only [Comparison.test, lift_value h]
  | le => simp only [Comparison.test, lift_value h]
  | eq =>
    apply Bool.eq_iff_iff.mpr
    simp only [Comparison.test, beq_iff_eq]
    constructor
    · intro eq
      have := congrArg (fun z : Word wide => z.setWidth narrow.bits) eq
      simpa only [project_lift h] using this
    · exact congrArg (lift wide)

end WordRAM.Conjectures.WidthSimulation