SETH ⇒ OVC sparsification bundle 8: 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_07

set_option autoImplicit true

/-! Input/output consequences of the full compiled trace simulation. -/
namespace WordRAM.Conjectures.SimulationInterface

open SimulationMemory SimulationExecution
variable {narrow wide : Width}

theorem lift_zero : WidthSimulation.lift wide (0 : Word narrow) = 0 := by
  simp [WidthSimulation.lift]

theorem lift_one (h : narrow.bits ≤ wide.bits) : WidthSimulation.lift wide (1 : Word narrow) = 1 := by
  have one : 1 < 2 ^ narrow.bits := Nat.one_lt_two_pow (by have := narrow.positive; omega)
  exact BitVec.setWidth_ofNat_of_le_of_lt h one

/-- Input serialization at the wider width is the zero extension of its
original narrow serialization, provided the original values fit. -/
theorem initial_memory (input : List Nat) (h : narrow.bits ≤ wide.bits)
    (fits : ∀ value ∈ input, value < 2 ^ narrow.bits) (address : Nat) :
    (initialState wide input).mem address =
      WidthSimulation.lift wide ((initialState narrow input).mem address) := by
  by_cases zero : address = 0
  · subst address; simpa only [initialState, ↓reduceIte] using (lift_zero (narrow := narrow) (wide := wide)).symm
  · simp only [initialState, if_neg zero]
    by_cases inside : address - 1 < input.length
    · simp only [List.getElem?_eq_getElem inside, Option.getD_some, WidthSimulation.lift]
      exact (BitVec.setWidth_ofNat_of_le_of_lt h (fits _ (List.getElem_mem _))).symm
    · simp only [List.getElem?_eq_none (by omega : input.length ≤ address - 1), Option.getD_none]
      exact lift_zero.symm

end WordRAM.Conjectures.SimulationInterface

/-! Return a simulated solver's answer in the actual machine's output cell. -/
namespace WordRAM.Conjectures.SimulationOutput

open SimulationExecution
variable {wide : Width}

def suffix : List SourceInstruction := [.copy (.direct 0) (.memory (.indirect 24)), .halt]

def code (solver : Algorithm) : List SourceInstruction :=
  (SimulationCompiler.code solver.code).map
    (SourceInstruction.returnTo (SimulationCompiler.code solver.code).length) ++ suffix

end WordRAM.Conjectures.SimulationOutput

/-! Finite, input-independent bounds on all literal memory addresses in a solver. -/
namespace WordRAM.Conjectures.SimulationBounds

open SimulationMemory SimulationExecution

def operandBound : SourceOperand → Nat
  | .immediate _ => 0
  | .memory address => staticCell address

def instructionBound : SourceInstruction → Nat
  | .copy dst src | .bitNot dst src => max (staticCell dst) (operandBound src)
  | .binary _ dst x y => max (staticCell dst) (max (operandBound x) (operandBound y))
  | .wordWidth dst => staticCell dst
  | .branch _ x y _ => max (operandBound x) (operandBound y)
  | .jump _ | .halt => 0

def programBound : List SourceInstruction → Nat
  | [] => 0
  | instruction :: rest => max (instructionBound instruction) (programBound rest)

theorem operand_fits (operand : SourceOperand) (base : Nat) (wide : Width)
    (bound : base + operandBound operand < 2 ^ wide.bits) :
    SimulationOperand.FixedFits base operand wide := by
  cases operand with
  | immediate _ => trivial
  | memory _ => exact bound

theorem instruction_fits (instruction : SourceInstruction) (base : Nat) (wide : Width)
    (bound : base + instructionBound instruction < 2 ^ wide.bits) : Fits base wide instruction := by
  cases instruction with
  | copy dst src =>
    change SimulationOperand.FixedFits base src wide ∧ True ∧ base + staticCell dst < 2 ^ wide.bits
    have bs : base + operandBound src < 2 ^ wide.bits := by simp only [instructionBound] at bound; omega
    exact ⟨operand_fits src base wide bs, trivial, by simp only [instructionBound] at bound; omega⟩
  | bitNot dst src =>
    change SimulationOperand.FixedFits base src wide ∧ True ∧ base + staticCell dst < 2 ^ wide.bits
    have bs : base + operandBound src < 2 ^ wide.bits := by simp only [instructionBound] at bound; omega
    exact ⟨operand_fits src base wide bs, trivial, by simp only [instructionBound] at bound; omega⟩
  | binary op dst x y =>
    change SimulationOperand.FixedFits base x wide ∧ SimulationOperand.FixedFits base y wide ∧
      base + staticCell dst < 2 ^ wide.bits
    simp only [instructionBound] at bound
    exact ⟨operand_fits x base wide (by omega), operand_fits y base wide (by omega), by omega⟩
  | wordWidth dst => exact ⟨trivial, trivial, bound⟩
  | branch cmp x y target =>
    change SimulationOperand.FixedFits base x wide ∧ SimulationOperand.FixedFits base y wide
    simp only [instructionBound] at bound
    exact ⟨operand_fits x base wide (by omega), operand_fits y base wide (by omega)⟩
  | jump _ => trivial
  | halt => trivial

theorem member_bound (program : List SourceInstruction) (instruction : SourceInstruction)
    (member : instruction ∈ program) : instructionBound instruction ≤ programBound program := by
  induction program with
  | nil => simp at member
  | cons head rest ih =>
    simp only [List.mem_cons] at member
    rcases member with eq | member
    · subst instruction; exact Nat.le_max_left _ _
    · exact Nat.le_trans (ih member) (Nat.le_max_right _ _)

/-- One bound on the finite source program establishes every static-address
precondition of the arbitrary-trace simulation, uniformly across inputs. -/
theorem program_fits (program : List SourceInstruction) (base : Nat) (wide : Width)
    (bound : base + programBound program < 2 ^ wide.bits) :
    ∀ instruction ∈ program, Fits base wide instruction := by
  intro instruction member
  apply instruction_fits
  have := member_bound program instruction member
  omega

end WordRAM.Conjectures.SimulationBounds

/-! Exact input magnitude used to compute an OV solver's word width. -/
namespace WordRAM.Conjectures.OVMagnitude

theorem fold_ge (xs : List Nat) (seed : Nat) : seed ≤ xs.foldl max seed := by
  induction xs generalizing seed with
  | nil => exact Nat.le_refl _
  | cons x xs ih => exact Nat.le_trans (Nat.le_max_left seed x) (ih (max seed x))

end WordRAM.Conjectures.OVMagnitude

/-! A fixed RAM loop computing floor(log₂ n) by unsigned right shifts. -/
namespace WordRAM.Conjectures.LogarithmMachine

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

/-- Cell 25 is the shrinking input; cell 26 is an accumulated logarithm.
Only these cells change. The caller initializes the accumulator. -/
def algorithm : Algorithm :=
  ⟨[.branch .lt (reg 25) (.immediate 2) 4,
    .binary .shr (.direct 25) (reg 25) (.immediate 1),
    .binary .add (.direct 26) (reg 26) (.immediate 1),
    .jump 0, .halt], 1, by decide⟩

theorem iteration (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (width : 2 ≤ w.bits) (large : 2 ≤ (s.mem 25).toNat) :
    let t := run widthConstant (algorithm.program w) 4 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 4 ∧
    t.mem 25 = s.mem 25 >>> 1 ∧ t.mem 26 = s.mem 26 + 1#w.bits ∧
    (∀ cell, cell ≠ 25 → cell ≠ 26 → t.mem cell = s.mem cell) := by
  have two : 2 < 2 ^ w.bits := Nat.lt_of_lt_of_le (by decide : 2 < 2 ^ 2)
    (Nat.pow_le_pow_right (by decide) width)
  have one : 1 < 2 ^ w.bits := by omega
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
    Comparison.test, pc, live, Nat.mod_eq_of_lt two, Nat.mod_eq_of_lt one,
    show ¬ (s.mem 25).toNat < 2 by omega, Nat.add_assoc, -BitVec.toNat_add]
  intro cell h25 h26; simp [h25, h26]

theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (width : 2 ≤ w.bits) (small : (s.mem 25).toNat < 2) :
    let t := run widthConstant (algorithm.program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem = s.mem := by
  have two : 2 < 2 ^ w.bits := Nat.lt_of_lt_of_le (by decide : 2 < 2 ^ 2)
    (Nat.pow_le_pow_right (by decide) width)
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Comparison.test,
    pc, live, Nat.mod_eq_of_lt two, small, Nat.add_assoc]

private theorem trace_of_ticks (s : State w) (fuel : Nat)
    (ticks : (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 ⟨n, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) fuel s
  have hc := runs_cost trace
  have eq : n = fuel := by omega
  subst n; exact trace

/-- Exact cost, arbitrary accumulated offset, and preservation of all other
memory. The width hypotheses prevent truncation of the comparison constant and
of the accumulated result. Zero and one are both valid inputs. -/
theorem computes (number offset : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (width : 2 ≤ w.bits)
    (fits : number < 2 ^ w.bits) (counterFits : offset + number.log2 < 2 ^ w.bits)
    (input : s.mem 25 = BitVec.ofNat w.bits number)
    (counter : s.mem 26 = BitVec.ofNat w.bits offset) :
    ∃ final, Runs widthConstant (algorithm.program w) (4 * number.log2 + 2) s final ∧
      final.halted = true ∧ final.mem 26 = BitVec.ofNat w.bits (offset + number.log2) ∧
      (∀ cell, cell ≠ 25 → cell ≠ 26 → final.mem cell = s.mem cell) := by
  induction number using Nat.strongRecOn generalizing offset s with
  | ind number ih =>
    have value : (s.mem 25).toNat = number := by rw [input]; exact Nat.mod_eq_of_lt fits
    by_cases large : 2 ≤ number
    · have log : number.log2 = (number / 2).log2 + 1 := by rw [Nat.log2_def]; simp [large]
      obtain ⟨nextPC, nextLive, ticks, shifted, incremented, frame⟩ := iteration s pc live width (by omega)
      let next := run widthConstant (algorithm.program w) 4 s
      have inputNext : next.mem 25 = BitVec.ofNat w.bits (number / 2) := by
        rw [shifted, input]
        apply BitVec.eq_of_toNat_eq
        simp [BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt fits,
          Nat.mod_eq_of_lt (show number / 2 < 2 ^ w.bits by omega)]
      have counterNext : next.mem 26 = BitVec.ofNat w.bits (offset + 1) := by
        rw [incremented, counter, ← BitVec.ofNat_add]
      obtain ⟨final, trace, halted, output, preserved⟩ := ih (number / 2)
        (Nat.log2_terminates number large) (offset + 1) next nextPC nextLive
        (by omega) (by omega) inputNext counterNext
      refine ⟨final, ?_, halted, ?_, ?_⟩
      · have full := (trace_of_ticks s 4 ticks).append trace
        have cost : 4 + (4 * (number / 2).log2 + 2) = 4 * number.log2 + 2 := by omega
        simpa only [cost] using full
      · simpa only [log, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using output
      · intro cell h25 h26; exact (preserved cell h25 h26).trans (frame cell h25 h26)
    · have log : number.log2 = 0 := by rw [Nat.log2_def]; simp [large]
      obtain ⟨halted, ticks, memory⟩ := exits s pc live width (by omega)
      refine ⟨_, ?_, halted, ?_, ?_⟩
      · simpa only [log, Nat.mul_zero, Nat.zero_add] using trace_of_ticks s 2 ticks
      · simpa only [memory, log, Nat.add_zero] using counter
      · intro cell _ _; rw [memory]

end WordRAM.Conjectures.LogarithmMachine

/-! Executable input-magnitude and width/mask setup blocks. -/
namespace WordRAM.Conjectures.SolverSetupParts

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

def widthAlgorithm (factor : Nat) : Algorithm :=
  ⟨[.binary .add (.direct 31) (reg 26) (.immediate 1),
    .binary (.mul rfl) (.direct 31) (reg 31) (.immediate factor),
    .wordWidth (.direct 27),
    .binary .sub (.direct 27) (reg 27) (reg 31),
    .bitNot (.direct 30) (.immediate 0),
    .binary .shr (.direct 30) (reg 30) (reg 27), .halt], 1, by decide⟩

theorem width_run (narrow wide : Width) (s : State wide) (factor logarithm : Nat)
    (pc : s.pc = 0) (live : s.halted = false)
    (width : narrow.bits ≤ wide.bits) (formula : narrow.bits = factor * (logarithm + 1))
    (input : s.mem 26 = BitVec.ofNat wide.bits logarithm) :
    let final := run widthConstant ((widthAlgorithm factor).program wide) 7 s
    final.halted = true ∧ final.ticks = s.ticks + 7 ∧
    final.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow) ∧
    final.mem 30 = WidthSimulation.mask narrow wide ∧
    (∀ cell, cell ≠ 27 → cell ≠ 30 → cell ≠ 31 → final.mem cell = s.mem cell) := by
  have wideFits : wide.bits < 2 ^ wide.bits := Nat.lt_pow_self (by decide)
  have narrowFits : narrow.bits < 2 ^ wide.bits := by omega
  have sub : BitVec.ofNat wide.bits wide.bits - BitVec.ofNat wide.bits narrow.bits =
      BitVec.ofNat wide.bits (wide.bits - narrow.bits) := by
    exact BitVec.ofNat_sub_ofNat_of_le _ _ narrowFits width
  have shift : (BitVec.ofNat wide.bits (wide.bits - narrow.bits)).toNat = wide.bits - narrow.bits :=
    Nat.mod_eq_of_lt (by omega)
  have native : BitVec.ofNat wide.bits narrow.bits =
      WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow) := by
    exact (BitVec.setWidth_ofNat_of_le_of_lt width (Nat.lt_pow_self (by decide))).symm
  have multiply : (logarithm + 1) * factor = narrow.bits := by rw [Nat.mul_comm, ← formula]
  have maskEq : BitVec.allOnes wide.bits >>> (wide.bits - narrow.bits) = WidthSimulation.mask narrow wide :=
    by simpa using WidthSimulation.mask_from_shift width
  simp [widthAlgorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, widthConstant,
    pc, live, input, ← BitVec.ofNat_add, ← BitVec.ofNat_mul, multiply, sub, shift, maskEq, Nat.add_assoc, -BitVec.toNat_ofNat, -BitVec.toNat_sub]
  refine ⟨native, ?_⟩
  intro cell h27 h30 h31; simp [h27, h30, h31]

end WordRAM.Conjectures.SolverSetupParts

/-! Total-time arithmetic for the implemented SAT-to-OV reduction. -/
namespace WordRAM.Conjectures.ReductionRuntime

theorem add_power_bound (a b exponent : Nat) :
    (a + b) ^ exponent ≤ 2 ^ exponent * (a ^ exponent + b ^ exponent) := by
  by_cases order : a ≤ b
  · have h := Nat.pow_le_pow_left (show a + b ≤ 2 * b by omega) exponent
    rw [Nat.mul_pow] at h
    exact Nat.le_trans h (Nat.mul_le_mul_left _ (by omega))
  · have h := Nat.pow_le_pow_left (show a + b ≤ 2 * a by omega) exponent
    rw [Nat.mul_pow] at h
    exact Nat.le_trans h (Nat.mul_le_mul_left _ (by omega))

end WordRAM.Conjectures.ReductionRuntime