crosslang/TsmLean/Compile/Correctness.lean

import TsmLean.Compile.Compile
import TsmLean.Core.Semantics

namespace TsmLean.Compile

open TsmLean.Core

/-! # Compiler-correctness theorem.

  `Source.Eval e v  ⟹  TSM.MultiStep (start of compile e) (end of compile e, with v on stack)`

The CompCert-flavored bridge: source-level evaluation and target-level
execution agree on the value produced. This is the substrate-projection
theorem at miniature scale — for v0.1 instantiated only on integer
literals; extending to compound expressions is mechanical and the
infrastructure (multi-step utilities, code-lookup helper, single-step
reduction lemmas) is already in place. -/

/-! ## Multi-step utilities. -/

theorem MultiStep.trans
    {s₁ s₂ s₃ : State}
    (h₁ : MultiStep s₁ s₂) (h₂ : MultiStep s₂ s₃) :
    MultiStep s₁ s₃ := by
  induction h₁ with
  | refl => exact h₂
  | cons hs _ ih => exact .cons hs (ih h₂)

theorem MultiStep.single
    {s s' : State} (h : step s = some s') :
    MultiStep s s' := .cons h (.refl _)

/-! ## Single-step reduction lemmas. -/

theorem step_push
    {code : Code} {pc : Nat} {stack : List Value} {n : Int}
    (h_pc : pc < code.size) (h_get : code[pc]'h_pc = .push n) :
    step { code := code, pc := pc, stack := stack }
    = some { code := code, pc := pc + 1, stack := .vInt n :: stack } := by
  unfold step; rw [dif_pos h_pc, h_get]

theorem step_add
    {code : Code} {pc : Nat} {a b : Int} {rest : List Value}
    (h_pc : pc < code.size) (h_get : code[pc]'h_pc = .add) :
    step { code := code, pc := pc, stack := .vInt b :: .vInt a :: rest }
    = some { code := code, pc := pc + 1, stack := .vInt (a + b) :: rest } := by
  unfold step; rw [dif_pos h_pc, h_get]

/-! ## Compile-output lookup helpers. -/

/-- The instruction at the end of `compile (.add e1 e2)` (right after both
    sub-compiled segments) is `.add`. -/
theorem compile_add_get_op
    (e1 e2 : Source.Expr)
    (h : (compile e1).size + (compile e2).size < (compile (Source.Expr.add e1 e2)).size) :
    (compile (Source.Expr.add e1 e2))[(compile e1).size + (compile e2).size]'h = .add := by
  show ((compile e1 ++ compile e2) ++ #[Instr.add])[(compile e1).size + (compile e2).size]'h = .add
  have hle : (compile e1 ++ compile e2).size ≤ (compile e1).size + (compile e2).size :=
    Nat.le_of_eq Array.size_append
  rw [Array.getElem_append_right hle]
  simp [Array.size_append, Nat.sub_self]

/-! ## Code-lookup helper.

Looking up an index `pre.size + i` in `pre ++ compile e ++ suf` reduces
to the corresponding index in `compile e` — used in the inductive case
when extending v0.1 to compound expressions. -/

theorem getElem_compile
    (pre : Code) (e : Source.Expr) (suf : Code) (i : Nat)
    (h_lt : i < (compile e).size)
    (h_pc : pre.size + i < (pre ++ compile e ++ suf).size) :
    (pre ++ compile e ++ suf)[pre.size + i]'h_pc = (compile e)[i]'h_lt := by
  have h_pre_ce : pre.size + i < (pre ++ compile e).size := by
    rw [Array.size_append]; omega
  rw [Array.getElem_append_left h_pre_ce]
  rw [Array.getElem_append_right (Nat.le_add_right _ _)]
  congr 1; omega

/-! ## Main theorem. -/

theorem compile_correct
    {e : Source.Expr} {v : Source.Value}
    (h_eval : Source.Eval e v) :
    ∀ (pre suf : Code) (rest : List Value),
      MultiStep
        { code := pre ++ compile e ++ suf, pc := pre.size, stack := rest }
        { code := pre ++ compile e ++ suf,
          pc := pre.size + (compile e).size, stack := v :: rest } := by
  induction h_eval with
  | intLit n =>
    intros pre suf rest
    apply MultiStep.single
    have h_pc : pre.size < (pre ++ compile (Source.Expr.intLit n) ++ suf).size := by
      simp only [compile, Array.size_append, Array.size_singleton]; omega
    have h_get : (pre ++ compile (Source.Expr.intLit n) ++ suf)[pre.size]'h_pc = .push n := by
      have h_pre_ce : pre.size < (pre ++ compile (Source.Expr.intLit n)).size := by
        simp only [compile, Array.size_append, Array.size_singleton]; omega
      rw [Array.getElem_append_left h_pre_ce]
      rw [Array.getElem_append_right (Nat.le_refl _)]
      simp [compile, Nat.sub_self]
    have step_thm := step_push h_pc h_get (stack := rest)
    have h_size : (compile (Source.Expr.intLit n)).size = 1 := by simp [compile]
    rw [h_size]
    exact step_thm
  | @add e1 e2 a b _ _ ih1 ih2 =>
    intros pre suf rest
    -- Step A: compile e1
    have stepA := ih1 pre (compile e2 ++ #[.add] ++ suf) rest
    -- Step B: compile e2 (with prefix extended)
    have stepB := ih2 (pre ++ compile e1) (#[.add] ++ suf) (.vInt a :: rest)
    -- Code rearrangements
    have h_code_A : pre ++ compile e1 ++ (compile e2 ++ #[Instr.add] ++ suf)
                  = pre ++ compile (Source.Expr.add e1 e2) ++ suf := by
      simp only [compile, Array.append_assoc]
    have h_code_B : pre ++ compile e1 ++ compile e2 ++ (#[Instr.add] ++ suf)
                  = pre ++ compile (Source.Expr.add e1 e2) ++ suf := by
      simp only [compile, Array.append_assoc]
    rw [h_code_A] at stepA
    rw [show (pre ++ compile e1).size = pre.size + (compile e1).size from
        by simp [Array.size_append]] at stepB
    rw [h_code_B] at stepB
    apply MultiStep.trans stepA
    apply MultiStep.trans stepB
    apply MultiStep.single
    -- Final .add step
    have h_total_size : (compile (Source.Expr.add e1 e2)).size
                      = (compile e1).size + (compile e2).size + 1 := by
      show (compile e1 ++ compile e2 ++ #[Instr.add]).size
         = (compile e1).size + (compile e2).size + 1
      simp [Array.size_append]; omega
    have h_op_pc : pre.size + (compile e1).size + (compile e2).size
                 < (pre ++ compile (Source.Expr.add e1 e2) ++ suf).size := by
      simp only [Array.size_append, h_total_size]; omega
    have h_in_comp : (compile e1).size + (compile e2).size
                     < (compile (Source.Expr.add e1 e2)).size := by
      simp [compile, Array.size_append]
    have h_full_pc : pre.size + ((compile e1).size + (compile e2).size)
                     < (pre ++ compile (Source.Expr.add e1 e2) ++ suf).size := by
      simp only [Array.size_append, h_total_size]; omega
    have h_op_get : (pre ++ compile (Source.Expr.add e1 e2) ++ suf)[pre.size + ((compile e1).size + (compile e2).size)]'h_full_pc = .add := by
      rw [getElem_compile pre (Source.Expr.add e1 e2) suf
            ((compile e1).size + (compile e2).size) h_in_comp h_full_pc]
      exact compile_add_get_op e1 e2 h_in_comp
    have h_step := step_add (a := a) (b := b) (rest := rest) h_full_pc h_op_get
    have h_pre_pc : pre.size + (compile e1).size + (compile e2).size
                  = pre.size + ((compile e1).size + (compile e2).size) := by omega
    have h_post_pc : pre.size + ((compile e1).size + (compile e2).size) + 1
                   = pre.size + (compile (Source.Expr.add e1 e2)).size := by
      rw [h_total_size]; omega
    rw [h_pre_pc, ← h_post_pc]
    exact h_step

/-! ## Demo run.

A self-contained `compile_correct` corollary for the standalone case
where the compile output IS the entire program (no surrounding code). -/

theorem compile_correct_standalone
    {e : Source.Expr} {v : Source.Value}
    (h_eval : Source.Eval e v) :
    MultiStep
      { code := compile e, pc := 0, stack := [] }
      { code := compile e, pc := (compile e).size, stack := [v] } := by
  have h := compile_correct h_eval #[] #[] []
  simp [Array.size_empty, Array.append_empty, Array.empty_append] at h
  exact h

end TsmLean.Compile