backend/cortexm0/CM0/SimBin.lean

import CM0.Guard

/-!
# CM0.SimBin

Generic simulation of the binary-operation lowering shape

    uf 2 ; load r1,[r4] ; load r0,[r4+4] ; <mid> ; store [r4+4],rr ; add r4,4

`mid` only has to compute `f a b` into `rr` from `r0 = a`, `r1 = b`, touching nothing but
scratch state. Instantiated below for add/sub/mul/and/or/xor, shifts, rotates and compares.
-/

namespace WordDialect
namespace CM0

open Reg

def MidSpec (mid : List (Instr Nat)) (rr : Reg) (f : W → W → W) : Prop :=
  ∀ (m : M) (a b : W), m.regs r0 = a → m.regs r1 = b →
    ∃ m', rseq mid m = .next m' ∧ m'.regs rr = f a b ∧ m'.mem = m.mem ∧
      m'.regs r4 = m.regs r4 ∧ m'.regs r5 = m.regs r5 ∧ m'.regs r8 = m.regs r8 ∧
      m'.regs r9 = m.regs r9 ∧ m'.regs sp = m.regs sp ∧ m'.regs r6 = m.regs r6 ∧
      m'.pc = m.pc + mid.length

theorem scratch_ne (r : Reg) (h : r = r0 ∨ r = r1 ∨ r = r2 ∨ r = r3) :
    r ≠ r4 ∧ r ≠ r5 ∧ r ≠ r8 ∧ r ≠ r9 ∧ r ≠ sp ∧ r ≠ r6 := by
  rcases h with rfl | rfl | rfl | rfl <;> decide

theorem sim_bin_ok {c : Cfg} {p : Prog 32} {s : State 32} {x : M} {code : List (Instr Nat)}
    {L : Layout} {base : Nat} {g : Facts} (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x)
    (hpc : x.pc = base) (mid : List (Instr Nat)) (rr : Reg)
    (hrr : rr = r0 ∨ rr = r1 ∨ rr = r2 ∨ rr = r3) (f : W → W → W)
    (hmid : MidSpec mid rr f) (hstr : ∀ i ∈ mid, i.straightR = true)
    (hat : RAt code base (uf L (need g 2) base ++
      ([.load r1 r4 0, .load r0 r4 4] ++ mid ++ [.store r4 4 rr, .addImm r4 4])))
    {b a : W} {d : List W} (hd : s.dstack = b :: a :: d) :
    ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := f a b :: d } x' ∧
      x'.pc = base + ufSize (need g 2) + (4 + mid.length) := by
  have hk : 2 ≤ s.dstack.length := by simp [hd]
  obtain ⟨hatuf, hatrest⟩ := rat_append.mp hat
  have hufl := uf_length L (need g 2) base
  rw [hufl] at hatrest
  obtain ⟨hatA, hatB⟩ := rat_append.mp hatrest
  obtain ⟨hatLd, hatMid⟩ := rat_append.mp hatA
  obtain ⟨f0, f1, _⟩ := hatLd
  obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf
  have hrcx := scratch_ne r1 (by simp)
  have hrax := scratch_ne r0 (by simp)
  -- load r1, [r4 + 0]
  have e0 := ld_stack hr1 (j := 0) (v := b) (by simp [hd]) r1 (disp := 0) (by simp)
  obtain ⟨x2, hx2⟩ : ∃ x2, x2 = x1.mov r1 b := ⟨_, rfl⟩
  have hst0 : RSteps code x1 x2 := RSteps.single (by
    rw [rstep_of_fetch (m := x1) (by rw [hpc1]; exact f0), e0, hx2])
  have hr2 : Rel0 c p s x2 := by rw [hx2]; exact mov_rel0 hr1 r1 hrcx b
  have hpc2 : x2.pc = base + ufSize (need g 2) + 1 := by simp [hx2, M.mov, M.setReg, M.adv, hpc1]
  -- load r0, [r4 + 4]
  have e1 := ld_stack hr2 (j := 1) (v := a) (by simp [hd]) r0 (disp := 4) (by simp)
  obtain ⟨x3, hx3⟩ : ∃ x3, x3 = x2.mov r0 a := ⟨_, rfl⟩
  have hst1 : RSteps code x2 x3 := RSteps.single (by
    rw [rstep_of_fetch (m := x2) (by rw [hpc2]; exact f1), e1, hx3])
  have hr3 : Rel0 c p s x3 := by rw [hx3]; exact mov_rel0 hr2 r0 hrax a
  have hpc3 : x3.pc = base + ufSize (need g 2) + 2 := by simp [hx3, M.mov, M.setReg, M.adv, hpc2]
  have hax : x3.regs r0 = a := by simp [hx3, M.mov, M.setReg, M.adv]
  have hcx : x3.regs r1 = b := by simp [hx3, hx2, M.mov, M.setReg, M.adv]
  -- mid
  obtain ⟨x4, hx4, hrr4, hm4, h15, h14, h13, h12, hsp, hbp, hpc4⟩ := hmid x3 a b hax hcx
  obtain ⟨hstM, _⟩ := rseq_steps hstr (by rw [hpc3]; exact hatMid) hx4
  have hr4 : Rel0 c p s x4 := hr3.congr hm4 h15 h14 h13 h12 hsp hbp
  -- store [r4 + 4], rr
  have hlen : 1 < s.dstack.length := by simp [hd]
  obtain ⟨mem', e2, hr5⟩ := st_stack hg hr4 (j := 1) hlen rr (disp := 4) (by simp)
  obtain ⟨st, adj, _⟩ := hatB
  have hpc4' : x4.pc = base + ufSize (need g 2) + (2 + mid.length) := by rw [hpc4, hpc3]; omega
  obtain ⟨x5, hx5⟩ : ∃ x5, x5 = ({ x4.adv with mem := mem' } : M) := ⟨_, rfl⟩
  have hst2 : RSteps code x4 x5 := RSteps.single (by
    rw [rstep_of_fetch (m := x4) (fetch_cast st (by rw [hpc4']; simp; omega)), e2, hx5])
  rw [← hx5] at hr5
  have hpc5 : x5.pc = base + ufSize (need g 2) + (2 + mid.length + 1) := by
    simp [hx5, M.adv]; omega
  -- adjust r4
  have hlen5 : 1 ≤ ({ s with dstack := s.dstack.set 1 (x4.regs rr) } : State 32).dstack.length := by
    simp [hd]
  obtain ⟨e3, hr6⟩ := adj_drop hg hr5 (n := 1) hlen5 (δ := 4) (by simp)
  obtain ⟨x6, hx6⟩ : ∃ x6, x6 = x5.arith Reg.r4
      (ofN (c.dEnd - 4 * (({ s with dstack := s.dstack.set 1 (x4.regs rr) } : State 32).dstack.length - 1))) :=
    ⟨_, rfl⟩
  rw [← hx6] at e3 hr6
  have hst3 : RSteps code x5 x6 := RSteps.single (by
    rw [rstep_of_fetch (m := x5) (fetch_cast adj (by rw [hpc5]; simp; omega)), e3])
  have hrrv : x4.regs rr = f a b := hrr4
  refine ⟨x6, ((((hst0 |> fun h => (hs1.trans h)).trans hst1).trans hstM).trans hst2).trans hst3, ?_, ?_⟩
  · have e : (({ s with dstack := s.dstack.set 1 (x4.regs rr) } : State 32).dstack).drop 1 = f a b :: d := by
      simp [hd, hrrv]
    simpa [e] using hr6
  · simp [hx6, M.arith, hpc5]
    omega

end CM0
end WordDialect