File size: 5,146 Bytes
9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 0e9783b 9ad95e5 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 | 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
|