import BCPL.Compile

/-!
# BCPL.ExprCorrect

Straight-line correctness of expression and assignment lowering against `evalE` /
`assignSem`: whenever the reference semantics succeeds, `execSeq` of the lowered code
reaches the corresponding state; whenever it traps, `execSeq` traps with the same trap.
-/

namespace WordDialect
namespace BCPL

open IR

theorem binCode_straight {n : Nat} (o : BinOp) :
    ∀ i ∈ (binCode o : List (Instr n)), i.isStraight = true := by
  cases o <;> simp [binCode, cmpFlagCode, Instr.isStraight]

theorem unCode_straight {n : Nat} (o : UnOp) :
    ∀ i ∈ (unCode o : List (Instr n)), i.isStraight = true := by
  cases o <;> simp [unCode, Instr.isStraight]

theorem compileE_straight {n : Nat} (addr : Var → Word n) (e : Expr) :
    ∀ i ∈ (compileE addr e), i.isStraight = true := by
  induction e with
  | num z => simp [compileE, Instr.isStraight]
  | var x => simp [compileE, Instr.isStraight]
  | addrOf x => simp [compileE, Instr.isStraight]
  | rv e ih =>
    intro i hi
    simp only [compileE, List.mem_append, List.mem_singleton] at hi
    rcases hi with hi | rfl
    · exact ih i hi
    · rfl
  | un o e ih =>
    intro i hi
    simp only [compileE, List.mem_append] at hi
    rcases hi with hi | hi
    · exact ih i hi
    · exact unCode_straight o i hi
  | bin o a b iha ihb =>
    intro i hi
    simp only [compileE, List.mem_append] at hi
    rcases hi with (hi | hi) | hi
    · exact iha i hi
    · exact ihb i hi
    · exact binCode_straight o i hi

theorem assignCode_straight {n : Nat} (addr : Var → Word n) (l : LVal) (e : Expr) :
    ∀ i ∈ (assignCode addr l e), i.isStraight = true := by
  cases l with
  | var x =>
    intro i hi
    simp only [assignCode, List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hi
    rcases hi with hi | rfl | rfl
    · exact compileE_straight addr e i hi
    · rfl
    · rfl
  | rv a =>
    intro i hi
    simp only [assignCode, List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hi
    rcases hi with (hi | hi) | rfl
    · exact compileE_straight addr e i hi
    · exact compileE_straight addr a i hi
    · rfl


theorem binCode_ok {n : Nat} (o : BinOp) (s : State n) (a b v : Word n) (d : List (Word n))
    (hs : s.dstack = b :: a :: d) (h : o.sem a b = .ok v) :
    execSeq (binCode o) s =
      .next { s with pc := s.pc + (binCode o : List (Instr n)).length, dstack := v :: d } := by
  cases o <;> simp only [BinOp.sem] at h <;> (try split at h) <;>
    first
      | (exfalso; cases h; done)
      | (cases h
         first
           | (simp [binCode, execSeq, exec, State.fall, hs, *]; done)
           | (simp [binCode, cmpFlagCode, execSeq, exec, State.fall, hs, flag, *]))

theorem binCode_err {n : Nat} (o : BinOp) (s : State n) (a b : Word n) (d : List (Word n))
    (t : Trap) (hs : s.dstack = b :: a :: d) (h : o.sem a b = .error t) :
    execSeq (binCode o) s = .trapped t := by
  cases o <;> simp only [BinOp.sem] at h <;> (try split at h) <;>
    first
      | (exfalso; cases h; done)
      | (cases h; simp [binCode, execSeq, exec, State.fall, hs, *])

theorem unCode_ok {n : Nat} (o : UnOp) (s : State n) (a : Word n) (d : List (Word n))
    (hs : s.dstack = a :: d) :
    execSeq (unCode o) s =
      .next { s with pc := s.pc + (unCode o : List (Instr n)).length, dstack := o.sem a :: d } := by
  cases o <;> simp [unCode, UnOp.sem, execSeq, exec, State.fall, hs]

theorem compileE_ok {n : Nat} (addr : Var → Word n) (e : Expr) :
    ∀ (s : State n) (v : Word n), evalE addr e s.mem = .ok v →
      execSeq (compileE addr e) s =
        .next { s with pc := s.pc + (compileE addr e).length, dstack := v :: s.dstack } := by
  induction e with
  | num z =>
    intro s v h
    simp only [evalE] at h; cases h
    simp [compileE, execSeq, exec, State.fall]
  | var x =>
    intro s v h
    simp only [evalE, readW] at h
    split at h
    · rename_i hr; cases h
      simp [compileE, execSeq, exec, State.fall, hr]
    · cases h
  | addrOf x =>
    intro s v h
    simp only [evalE] at h; cases h
    simp [compileE, execSeq, exec, State.fall]
  | rv e ih =>
    intro s v h
    simp only [evalE] at h
    split at h
    · cases h
    · rename_i a ha
      simp only [readW] at h
      split at h
      · rename_i hr; cases h
        rw [compileE, execSeq_append, ih s a ha]
        simp [Outcome.andThen, execSeq, exec, State.fall, hr, Nat.add_assoc]
      · cases h
  | un o e ih =>
    intro s v h
    simp only [evalE] at h
    split at h
    · cases h
    · rename_i a ha; cases h
      rw [compileE, execSeq_append, ih s a ha]
      simp only [Outcome.andThen]
      rw [unCode_ok o _ a s.dstack rfl]
      simp [List.length_append]; omega
  | bin o a b iha ihb =>
    intro s v h
    simp only [evalE] at h
    split at h
    · cases h
    · rename_i va ha
      split at h
      · cases h
      · rename_i vb hb
        rw [compileE, execSeq_append, execSeq_append, iha s va ha]
        simp only [Outcome.andThen]
        rw [ihb { s with pc := s.pc + (compileE addr a).length, dstack := va :: s.dstack } vb hb]
        simp only [Outcome.andThen]
        rw [binCode_ok o _ va vb v s.dstack rfl h]
        simp [List.length_append]; omega

theorem compileE_err {n : Nat} (addr : Var → Word n) (e : Expr) :
    ∀ (s : State n) (t : Trap), evalE addr e s.mem = .error t →
      execSeq (compileE addr e) s = .trapped t := by
  induction e with
  | num z => intro s t h; simp [evalE] at h
  | var x =>
    intro s t h
    simp only [evalE, readW] at h
    split at h
    · cases h
    · rename_i hr; cases h
      simp [compileE, execSeq, exec, State.fall, hr]
  | addrOf x => intro s t h; simp [evalE] at h
  | rv e ih =>
    intro s t h
    simp only [evalE] at h
    split at h
    · rename_i t' ht; cases h
      rw [compileE, execSeq_append, ih s _ ht]; rfl
    · rename_i a ha
      simp only [readW] at h
      split at h
      · cases h
      · rename_i hr; cases h
        rw [compileE, execSeq_append, compileE_ok addr e s a ha]
        simp [Outcome.andThen, execSeq, exec, State.fall, hr, Nat.add_assoc]
  | un o e ih =>
    intro s t h
    simp only [evalE] at h
    split at h
    · rename_i t' ht; cases h
      rw [compileE, execSeq_append, ih s _ ht]; rfl
    · cases h
  | bin o a b iha ihb =>
    intro s t h
    simp only [evalE] at h
    split at h
    · rename_i t' ht; cases h
      rw [compileE, execSeq_append, execSeq_append, iha s _ ht]; rfl
    · rename_i va ha
      split at h
      · rename_i t' ht; cases h
        rw [compileE, execSeq_append, execSeq_append, compileE_ok addr a s va ha]
        simp only [Outcome.andThen]
        rw [ihb { s with pc := s.pc + (compileE addr a).length, dstack := va :: s.dstack } _ ht]
      · rename_i vb hb
        rw [compileE, execSeq_append, execSeq_append, compileE_ok addr a s va ha]
        simp only [Outcome.andThen]
        rw [compileE_ok addr b { s with pc := s.pc + (compileE addr a).length, dstack := va :: s.dstack } vb hb]
        simp only [Outcome.andThen]
        exact binCode_err o _ va vb s.dstack t rfl h

end BCPL
end WordDialect