SETH ⇒ OVC sparsification bundle 1: word-RAM execution primitives

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

set_option autoImplicit true

namespace WordRAM

/-- The only cell an instruction can write; control instructions write no cell. -/
def Instruction.destination : Instruction w m k → Option Address
  | .copy dst _ | .binary _ dst _ _ | .bitNot dst _ | .native dst _ => some dst
  | .jump _ | .branch _ _ _ _ | .halt => none

end WordRAM

namespace WordRAM

/-! Specification correspondence: these hold at EVERY positive word width. -/

theorem execute_cost (cs : NativeConstants k) (i : Instruction w m k) (s : State w) :
    (execute cs i s).ticks = s.ticks + 1 := by cases i <;> rfl

theorem step_cost (cs : NativeConstants k) (p : Program w m k)
    (s t : State w) (h : step cs p s = some t) : t.ticks = s.ticks + 1 := by
  unfold step at h
  split at h
  · simp at h
  · cases hf : p[s.pc]? with
    | none => simp [hf] at h
    | some i =>
      simp only [hf, Option.map_some, Option.some.injEq] at h
      subst t
      exact execute_cost cs i s

theorem runs_cost (h : Runs cs p n s t) : t.ticks = s.ticks + n := by
  induction h with
  | refl => simp
  | cons hs _ ih =>
      have hc := step_cost _ _ _ _ hs
      omega

/-- Every fuel-based run corresponds to an actual trace, including early stop. -/
theorem run_has_trace (cs : NativeConstants k) (p : Program w m k)
    (fuel : Nat) (s : State w) :
    ∃ n, n ≤ fuel ∧ Runs cs p n s (run cs p fuel s) := by
  induction fuel generalizing s with
  | zero => exact ⟨0, Nat.le_refl 0, .refl s⟩
  | succ fuel ih =>
      cases hs : step cs p s with
      | none => exact ⟨0, Nat.zero_le _, by simpa [run, hs] using Runs.refl (constants := cs) (p := p) s⟩
      | some t =>
          obtain ⟨n, hn, ht⟩ := ih t
          exact ⟨n + 1, by omega, by simpa [run, hs] using Runs.cons hs ht⟩

end WordRAM

namespace WordRAM.Conjectures

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

private theorem member_le_fold_max (xs : List Nat) (seed x : Nat) (h : x ∈ xs) :
    x ≤ xs.foldl max seed := by
  induction xs generalizing seed with
  | nil => simp at h
  | cons y ys ih =>
      simp only [List.mem_cons] at h
      rcases h with h | h
      · subst x
        exact Nat.le_trans (Nat.le_max_right seed y) (fold_max_ge ys (max seed y))
      · exact ih (max seed y) h

/-- Serialization cannot silently truncate an input value at the chosen width. -/
theorem encoded_value_fits (a : Algorithm) (input : List Nat) (extra x : Nat)
    (h : x ∈ input) : x < 2 ^ (a.width input extra).bits := by
  have hm := member_le_fold_max input input.length x h
  have hx : x < inputMagnitude input := by unfold inputMagnitude; omega
  have hl : inputMagnitude input < 2 ^ ((inputMagnitude input).log2 + 1) := Nat.lt_log2_self
  have hw : (inputMagnitude input).log2 + 1 ≤ (a.width input extra).bits := by
    have := Nat.le_mul_of_pos_left (extra + (inputMagnitude input).log2 + 1) a.wordFactor_pos
    simp only [Algorithm.width]
    omega
  exact Nat.lt_of_lt_of_le (Nat.lt_trans hx hl) (Nat.pow_le_pow_right (by decide) hw)

namespace Checks

-- Definitional check: this is the implication proposition, not a proof of it.

end Checks
end WordRAM.Conjectures

/-!
The split-and-list SAT-to-OV reduction, with an unconditional correctness proof.
The computational transfer propositions are defined at the end. Their proofs
are supplied by `OVToSparseSAT.lean` and `SparsificationTransfer.lean`; the latter
also proves the full implication with the original conjecture definitions.
-/
namespace WordRAM.Conjectures
namespace Reduction

/-- Pack an arbitrary finite assignment into the standard enumeration. -/
def pack (a : Fin h → Bool) : BitVec h :=
  (BitVec.ofBoolListLE (List.ofFn a)).cast (by simp)

theorem pack_bit (a : Fin h → Bool) (i : Nat) (hi : i < h) :
    (pack a).getLsbD i = a ⟨i, hi⟩ := by
  simp only [pack, BitVec.getLsbD_cast, BitVec.getLsbD_ofBoolListLE]
  simp [List.getD, hi]

end Reduction

/-! ## Computational transfer propositions

The following propositions separate the computational obligations.
`OVToSparseSAT.lean` supplies the first and `SparsificationTransfer.lean` the
second. The conditional theorem below assembles the two transfers without
changing SETH or OVConjecture.
-/

/-- Algorithmic sparsification in our concrete wordRAM. Proved by
`sparsification_transfer` in `SparsificationTransfer.lean`. -/
def SparsificationTransfer : Prop :=
  ∀ r, 2 ≤ r → ∀ k, 3 ≤ k →
    (∀ density, 1 ≤ density → HasFastSparseSAT k density r) →
      HasFastSAT k (2 * r)

end WordRAM.Conjectures

/-! Small program-composition facts for proofs about actual wordRAM instructions. -/
namespace WordRAM

/-- Sequential executions compose with addition of their EXACT step counts. -/
theorem Runs.append (first : Runs cs p n s t) (second : Runs cs p m t u) :
    Runs cs p (n + m) s u := by
  induction first with
  | refl => simpa using second
  | cons hs _ ih => simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using Runs.cons hs (ih second)

/-- A fetched instruction gives a one-step execution, provided the state is live. -/
theorem runs_instruction (cs : NativeConstants k) (p : Program w m k)
    (s : State w) (i : Instruction w m k)
    (live : s.halted = false) (fetch : p[s.pc]? = some i) :
    Runs cs p 1 s (execute cs i s) := by
  exact Runs.cons (by simp [step, live, fetch]) (Runs.refl _)

def State.relocate (offset : Nat) (s : State w) : State w :=
  { s with pc := offset + s.pc }

/-- Relocation preserves memory, status and cost, and shifts only the PC. -/
theorem execute_relocate (cs : NativeConstants k) (i : Instruction w m k)
    (offset : Nat) (s : State w) :
    execute cs (i.relocate offset) (s.relocate offset) =
      (execute cs i s).relocate offset := by
  cases i <;> simp [Instruction.relocate, State.relocate, execute, Nat.add_assoc]
  split <;> rfl

/-- A code embedding is a precise fetch condition. It covers appending a
relocated subroutine to a prefix without assuming a new machine instruction. -/
def EmbedsAt (small big : Program w m k) (offset : Nat) : Prop :=
  ∀ pc i, small[pc]? = some i → big[offset + pc]? = some (i.relocate offset)

/-- Appending a relocated block between arbitrary prefix/suffix code satisfies
the embedding condition; all original valid instruction fetches are preserved. -/
theorem embeds_append (setupPrefix p suffix : Program w m k) :
    EmbedsAt p (setupPrefix ++ (p.map (Instruction.relocate setupPrefix.length) ++ suffix)) setupPrefix.length := by
  intro pc i hf
  have hp : pc < p.length := (List.getElem?_eq_some_iff.mp hf).1
  rw [List.getElem?_append_right (by omega)]
  simp only [Nat.add_sub_cancel_left]
  rw [List.getElem?_append_left (by simpa using hp)]
  simp [hf]

theorem step_relocate (cs : NativeConstants k) (p q : Program w m k)
    (offset : Nat) (embed : EmbedsAt p q offset) (s t : State w)
    (hs : step cs p s = some t) :
    step cs q (s.relocate offset) = some (t.relocate offset) := by
  unfold step at hs
  split at hs
  · simp at hs
  · rename_i live
    cases hf : p[s.pc]? with
    | none => simp [hf] at hs
    | some i =>
        have he := embed s.pc i hf
        simp only [hf, Option.map_some, Option.some.injEq] at hs
        subst t
        simpa [step, State.relocate, live, he] using congrArg some (execute_relocate cs i offset s)

/-- All terminating and nonterminating finite trace prefixes relocate with no
change in step count; this does not yet handle different word widths. -/
theorem Runs.relocate (h : Runs cs p n s t) (embed : EmbedsAt p q offset) :
    Runs cs q n (s.relocate offset) (t.relocate offset) := by
  induction h with
  | refl => exact .refl _
  | cons hs _ ih => exact .cons (step_relocate _ _ _ _ embed _ _ hs) ih

@[simp] theorem Instruction.relocate_zero (i : Instruction w m k) :
    i.relocate 0 = i := by cases i <;> simp [Instruction.relocate]

@[simp] theorem State.relocate_zero (s : State w) : s.relocate 0 = s := by
  simp [State.relocate]

/-- A program's existing finite trace remains valid when more code is appended.
This also applies to trace prefixes that end just before the appended code. -/
theorem Runs.append_code {p : Program w m k} {cs : NativeConstants k} {s t : State w}
    (h : Runs cs p n s t) (suffix : Program w m k) :
    Runs cs (p ++ suffix) n s t := by
  have embed : EmbedsAt p (p ++ suffix) 0 := by
    intro pc i fetch
    have bound : pc < p.length := (List.getElem?_eq_some_iff.mp fetch).1
    simpa [List.getElem?_append_left bound] using fetch
  simpa using h.relocate embed

/-- Turn a standalone program into a block that jumps to a continuation. -/
def Instruction.returnTo (target : Nat) : Instruction w m k → Instruction w m k
  | .halt => .jump target
  | i => i

def State.returnTo (target : Nat) (s : State w) : State w :=
  if s.halted then { s with pc := target, halted := false } else s

theorem execute_returnTo (cs : NativeConstants k) (i : Instruction w m k)
    (target : Nat) (s : State w) (live : s.halted = false) :
    execute cs (i.returnTo target) s = (execute cs i s).returnTo target := by
  cases i <;> simp [Instruction.returnTo, State.returnTo, execute, live]

theorem step_live (cs : NativeConstants k) (p : Program w m k) (s t : State w)
    (h : step cs p s = some t) : s.halted = false := by
  cases hh : s.halted with
  | false => rfl
  | true => simp [step, hh] at h

theorem step_returnTo (cs : NativeConstants k) (p : Program w m k)
    (target : Nat) (s t : State w) (h : step cs p s = some t) :
    step cs (p.map (Instruction.returnTo target)) (s.returnTo target) =
      some (t.returnTo target) := by
  have live := step_live cs p s t h
  cases hf : p[s.pc]? with
  | none => simp [step, live, hf] at h
  | some i =>
      have he : execute cs i s = t := by simpa [step, live, hf] using h
      subst t
      simpa [step, State.returnTo, live, hf] using
        congrArg some (execute_returnTo cs i target s live)

/-- Replacing halts by jumps preserves a whole finite execution and its exact
cost, releasing the final halt flag so another block can execute afterwards. -/
theorem Runs.returnTo (h : Runs cs p n s t) (target : Nat) :
    Runs cs (p.map (Instruction.returnTo target)) n (s.returnTo target) (t.returnTo target) := by
  induction h with
  | refl => exact .refl _
  | cons hs _ ih => exact .cons (step_returnTo _ _ _ _ _ hs) ih

/-- A subroutine may be entered after an arbitrary amount of earlier work. -/
def State.addTicks (elapsed : Nat) (s : State w) : State w :=
  { s with ticks := elapsed + s.ticks }

namespace Conjectures

/-- These source-level transformations keep programs uniform across widths. -/
def SourceInstruction.relocate (offset : Nat) : SourceInstruction → SourceInstruction
  | .jump target => .jump (offset + target)
  | .branch cmp x y target => .branch cmp x y (offset + target)
  | i => i

def SourceInstruction.returnTo (target : Nat) : SourceInstruction → SourceInstruction
  | .halt => .jump target
  | i => i

theorem compile_relocate (i : SourceInstruction) (w : Width) (offset : Nat) :
    (i.relocate offset).compile w = (i.compile w).relocate offset := by
  cases i <;> rfl

theorem compile_returnTo (i : SourceInstruction) (w : Width) (target : Nat) :
    (i.returnTo target).compile w = (i.compile w).returnTo target := by
  cases i <;> rfl

end Conjectures

end WordRAM

/-! Mathematical correctness of the two clause masks consumed by ClauseMachine.
Mask construction is explicit and computable; MaskBuilder and MaskPipeline
prove its wordRAM implementation. -/
namespace WordRAM.Conjectures.ClauseMasks

/-- One bit per variable of the selected polarity on the selected side. -/
def mask (w : Width) (side : Fin n → Bool) (clause : List (Literal n))
    (polarity : Bool) : Word w :=
  Reduction.pack fun i : Fin w.bits =>
    clause.any fun l => side l.index && (l.positive == polarity) && (l.index.val == i.val)

theorem mask_bit (side : Fin n → Bool) (clause : List (Literal n))
    (polarity : Bool) (i : Nat) (hi : i < w.bits) :
    (mask w side clause polarity).getLsbD i = true ↔
      ∃ l ∈ clause, side l.index = true ∧ l.positive = polarity ∧ l.index.val = i := by
  simp only [mask, Reduction.pack_bit _ _ hi]
  simp [List.any_eq_true, Bool.and_eq_true, and_assoc]

end WordRAM.Conjectures.ClauseMasks

/-! Verified logical branching used in sparsification.
This is not yet the algorithmic sparsification lemma: selecting sufficiently
large flowers and bounding the total search tree remain unproved. -/
namespace WordRAM.Conjectures.Sparsification

abbrev Clause (n : Nat) := List (Literal n)
abbrev CNF (n : Nat) := List (Clause n)

def ClauseHolds (a : Fin n → Bool) (c : Clause n) : Prop :=
  ∃ l ∈ c, l.eval a = true

def Holds (a : Fin n → Bool) (f : CNF n) : Prop :=
  ∀ c ∈ f, ClauseHolds a c

theorem holds_append (a : Fin n → Bool) (f g : CNF n) :
    Holds a (f ++ g) ↔ Holds a f ∧ Holds a g := by
  simp only [Holds, List.mem_append]
  constructor
  · intro h
    exact ⟨fun c hc => h c (Or.inl hc), fun c hc => h c (Or.inr hc)⟩
  · rintro ⟨hf, hg⟩ c (hc | hc)
    · exact hf c hc
    · exact hg c hc

/-- Literal occurrences, with multiplicities. This gives a termination measure,
NOT the much sharper branching bound needed for the sparsification lemma. -/
def weight : CNF n → Nat
  | [] => 0
  | clause :: rest => clause.length + weight rest

theorem weight_append (f g : CNF n) : weight (f ++ g) = weight f + weight g := by
  induction f with
  | nil => simp [weight]
  | cons c f ih => simp [weight, ih, Nat.add_assoc]

end WordRAM.Conjectures.Sparsification