Sync from GitHub at 25c8330: hardware-in-the-loop rig, SAM D21 board, guard elimination on RV32/Cortex-M3
0e9783b verified | import CM.SimOps | |
| /-! | |
| # CM.SimStack | |
| Single-instruction step lemmas (`load`/`store`/`addImm` on the data stack, `movImm`, `not`) and | |
| the simulation theorems for the instructions that only move words on the data stack: | |
| `word ptr not dup drop swap over rot`. | |
| -/ | |
| namespace WordDialect | |
| namespace CM | |
| open Reg | |
| section Steps | |
| variable {c : Cfg} {p : Prog 32} {s : State 32} {x : M} {code : List (Instr Nat)} | |
| theorem ld_step (hs : Rel0 c p s x) {j : Nat} {v : W} (hj : s.dstack[j]? = some v) {rd : Reg} | |
| (hrd : rd = r0 ∨ rd = r1 ∨ rd = r2 ∨ rd = r3) {disp : Int} (hd : disp = 4 * (j : Int)) | |
| (hf : code[x.pc]? = some (.load rd Reg.r4 disp)) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p s x' ∧ x'.pc = x.pc + 1 ∧ x'.regs rd = v ∧ | |
| (∀ r, r ≠ rd → x'.regs r = x.regs r) ∧ x'.mem = x.mem := by | |
| refine ⟨x.mov rd v, RSteps.single (by rw [rstep_of_fetch hf, ld_stack hs hj rd hd]), | |
| mov_rel0 hs rd (scratch_ne rd hrd) v, ?_, ?_, ?_, ?_⟩ | |
| · simp [M.mov, M.setReg, M.adv] | |
| · simp [M.mov, M.setReg, M.adv] | |
| · intro r hr; simp [M.mov, M.setReg, M.adv, hr] | |
| · simp [M.mov, M.setReg, M.adv] | |
| theorem st_step (hg : Geom c) (hs : Rel0 c p s x) {j : Nat} (hj : j < s.dstack.length) {rs : Reg} | |
| {disp : Int} (hd : disp = 4 * (j : Int)) (hf : code[x.pc]? = some (.store Reg.r4 disp rs)) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := s.dstack.set j (x.regs rs) } x' ∧ | |
| x'.pc = x.pc + 1 ∧ x'.regs = x.regs := by | |
| obtain ⟨mem', e, hr⟩ := st_stack hg hs hj rs hd | |
| exact ⟨_, RSteps.single (by rw [rstep_of_fetch hf, e]), hr, by simp [M.adv], by simp [M.adv]⟩ | |
| theorem adj_step (hg : Geom c) (hs : Rel0 c p s x) {n : Nat} (hn : n ≤ s.dstack.length) {δ : Int} | |
| (hd : δ = 4 * (n : Int)) (hf : code[x.pc]? = some (.addImm Reg.r4 δ)) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := s.dstack.drop n } x' ∧ | |
| x'.pc = x.pc + 1 ∧ (∀ r, r ≠ Reg.r4 → x'.regs r = x.regs r) := by | |
| obtain ⟨e, hr⟩ := adj_drop hg hs hn hd | |
| exact ⟨_, RSteps.single (by rw [rstep_of_fetch hf, e]), hr, by simp [M.arith, M.setReg], | |
| by intro r hr; simp [M.arith, M.setReg, hr]⟩ | |
| theorem movimm_step (hs : Rel0 c p s x) {rd : Reg} (hrd : rd = r0 ∨ rd = r1 ∨ rd = r2 ∨ rd = r3) | |
| {v : W} (hf : code[x.pc]? = some (.movImm rd v)) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p s x' ∧ x'.pc = x.pc + 1 ∧ x'.regs rd = v ∧ | |
| (∀ r, r ≠ rd → x'.regs r = x.regs r) ∧ x'.mem = x.mem := by | |
| refine ⟨x.mov rd v, RSteps.single (by rw [rstep_of_fetch hf]; rfl), | |
| mov_rel0 hs rd (scratch_ne rd hrd) v, ?_, ?_, ?_, ?_⟩ | |
| · simp [M.mov, M.setReg, M.adv] | |
| · simp [M.mov, M.setReg, M.adv] | |
| · intro r hr; simp [M.mov, M.setReg, M.adv, hr] | |
| · simp [M.mov, M.setReg, M.adv] | |
| theorem not_step (hs : Rel0 c p s x) (hf : code[x.pc]? = some (.not r0)) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p s x' ∧ x'.pc = x.pc + 1 ∧ x'.regs r0 = ~~~x.regs r0 := by | |
| refine ⟨x.mov r0 (~~~x.regs r0), RSteps.single (by rw [rstep_of_fetch hf]; rfl), | |
| mov_rel0 hs r0 (scratch_ne r0 (by simp)) _, ?_, ?_⟩ | |
| · simp [M.mov, M.setReg, M.adv] | |
| · simp [M.mov, M.setReg, M.adv] | |
| end Steps | |
| /-- Placement of `ovf L g base ++ [i0, i1, i2]`. -/ | |
| theorem xat_ovf3 {code : List (Instr Nat)} {L : Layout} {g : Facts} {base : Nat} | |
| {i0 i1 i2 : Instr Nat} (hat : RAt code base (ovf L g base ++ [i0, i1, i2])) : | |
| RAt code base (ovf L g base) ∧ code[base + ovfSize g]? = some i0 ∧ | |
| code[base + ovfSize g + 1]? = some i1 ∧ code[base + ovfSize g + 1 + 1]? = some i2 := by | |
| obtain ⟨hato, hatr⟩ := rat_append.mp hat | |
| rw [ovf_length] at hatr | |
| obtain ⟨f0, f1, f2, _⟩ := hatr | |
| exact ⟨hato, f0, f1, f2⟩ | |
| /-- Placement of `uf L n base ++ ovf L g (base + ufSize n) ++ [i0, i1, i2]`. -/ | |
| theorem xat_uf_ovf {code : List (Instr Nat)} {L : Layout} {g : Facts} {base n : Nat} | |
| {i0 i1 i2 : Instr Nat} {rest : List (Instr Nat)} (hrest : rest = [i0, i1, i2]) | |
| (hat : RAt code base (uf L n base ++ ovf L g (base + ufSize n) ++ rest)) : | |
| RAt code base (uf L n base) ∧ RAt code (base + ufSize n) (ovf L g (base + ufSize n)) ∧ | |
| code[base + ufSize n + ovfSize g]? = some i0 ∧ | |
| code[base + ufSize n + ovfSize g + 1]? = some i1 ∧ | |
| code[base + ufSize n + ovfSize g + 1 + 1]? = some i2 := by | |
| subst hrest | |
| obtain ⟨hatuo, hatr⟩ := rat_append.mp hat | |
| obtain ⟨hatuf, hato⟩ := rat_append.mp hatuo | |
| have hufl := uf_length L n base | |
| rw [hufl] at hato | |
| have hl : (uf L n base ++ ovf L g (base + ufSize n)).length = ufSize n + ovfSize g := by | |
| simp [hufl, ovf_length] | |
| rw [hl] at hatr | |
| obtain ⟨f0, f1, f2, _⟩ := hatr | |
| exact ⟨hatuf, hato, by simpa [Nat.add_assoc] using f0, by simpa [Nat.add_assoc] using f1, | |
| by simpa [Nat.add_assoc] using f2⟩ | |
| section Ops | |
| variable {c : Cfg} {p : Prog 32} {s : State 32} {x : M} {code : List (Instr Nat)} | |
| {L : Layout} {base : Nat} {off : Nat → Nat} {g : Facts} | |
| theorem sim_not_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hat : RAt code base (lowerInstr L base off g .not)) {a : W} {d : List W} | |
| (hd : s.dstack = a :: d) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := (~~~a) :: d } x' ∧ | |
| x'.pc = base + isize g (.not : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 1) base ++ [.load r0 Reg.r4 0, .not r0, .store Reg.r4 0 r0]) := hat | |
| obtain ⟨hatuf, hatr⟩ := rat_append.mp hat' | |
| have hufl := uf_length L (need g 1) base | |
| rw [hufl] at hatr | |
| obtain ⟨f0, f1, f2, _⟩ := hatr | |
| have hk : 1 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, _, _⟩ := ld_step (code := code) hr1 (j := 0) (v := a) | |
| (by simp [hd]) (rd := r0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hv3⟩ := not_step (code := code) hr2 (fetch_cast f1 (by omega)) | |
| obtain ⟨x4, hs4, hr4, hpc4, _⟩ := st_step (code := code) hg hr3 (j := 0) (by simp [hd]) | |
| (rs := r0) (disp := 0) (by simp) (fetch_cast f2 (by omega)) | |
| have e : s.dstack.set 0 (x3.regs r0) = (~~~a) :: d := by simp [hd, hv3, hv2] | |
| rw [e] at hr4 | |
| exact ⟨x4, ((hs1.trans hs2).trans hs3).trans hs4, hr4, by simp [isize]; omega⟩ | |
| theorem sim_dup_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g .dup)) {a : W} | |
| {d : List W} (hd : s.dstack = a :: d) (hfit : c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := a :: a :: d } x' ∧ | |
| x'.pc = base + isize g (.dup : WordDialect.Instr 32) := by | |
| obtain ⟨hatuf, hato, f0, f1, f2⟩ := xat_uf_ovf (L := L) (n := need g 1) rfl hat | |
| have hk : 1 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x1', hs1', hr1', hpc1', _, _⟩ := ovfG_pass hg hr1 hLd hfit hpc1 hato | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, _, _⟩ := ld_step (code := code) hr1' (j := 0) (v := a) | |
| (by simp [hd]) (rd := r0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, _⟩ := push_pair hg hr2 r0 (by decide) hfit | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ | |
| rw [hv2, hd] at hr3 | |
| exact ⟨x3, ((hs1.trans hs1').trans hs2).trans hs3, hr3, by simp [isize]; omega⟩ | |
| theorem sim_dup_ovf (hn : g.noOvf = false) (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g .dup)) {a : W} | |
| {d : List W} (hd : s.dstack = a :: d) (h : ¬ c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| RExec code x .overflow := by | |
| obtain ⟨hatuf, hato, _⟩ := xat_uf_ovf (L := L) (n := need g 1) rfl hat | |
| obtain ⟨x1, hs1, hr1, hpc1, _, _⟩ := uf_pass hg hs hL (by decide) (by simp [hd]) hpc hatuf | |
| exact RExec.of_steps hs1 (ovfG_trap hn hg hr1 hLd h hpc1 hato) | |
| theorem sim_drop_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hat : RAt code base (lowerInstr L base off g .drop)) {a : W} {d : List W} | |
| (hd : s.dstack = a :: d) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := d } x' ∧ | |
| x'.pc = base + isize g (.drop : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 1) base ++ [.addImm Reg.r4 4]) := hat | |
| obtain ⟨hatuf, hatr⟩ := rat_append.mp hat' | |
| have hufl := uf_length L (need g 1) base | |
| rw [hufl] at hatr | |
| obtain ⟨f0, _⟩ := hatr | |
| have hk : 1 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, _⟩ := adj_step (code := code) hg hr1 (n := 1) (by simp [hd]) | |
| (δ := 4) (by simp) (fetch_cast f0 (by omega)) | |
| have e : (s.dstack).drop 1 = d := by simp [hd] | |
| rw [e] at hr2 | |
| exact ⟨x2, hs1.trans hs2, hr2, by simp [isize]; omega⟩ | |
| theorem sim_word_ok (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) (w : W) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g (.word w))) | |
| (hfit : c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := w :: s.dstack } x' ∧ | |
| x'.pc = base + isize g (.word w : WordDialect.Instr 32) := by | |
| obtain ⟨hato, f0, f1, f2⟩ := xat_ovf3 (L := L) (by exact hat) | |
| obtain ⟨x0, hs0, hr0, hpc0, _, _⟩ := ovfG_pass hg hs hLd hfit hpc hato | |
| obtain ⟨x1, hs1, hr1, hpc1, hv1, _⟩ := movimm_step (code := code) hr0 (rd := r0) (by simp) | |
| (v := w) (by rw [hpc0]; exact f0) | |
| obtain ⟨x2, hs2, hr2, hpc2, _⟩ := push_pair hg hr1 r0 (by decide) hfit | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ | |
| rw [hv1] at hr2 | |
| exact ⟨x2, (hs0.trans hs1).trans hs2, hr2, by simp [isize]; omega⟩ | |
| theorem sim_word_ovf (hn : g.noOvf = false) (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) (w : W) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g (.word w))) | |
| (h : ¬ c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : RExec code x .overflow := by | |
| obtain ⟨hato, _⟩ := xat_ovf3 (L := L) (by exact hat) | |
| exact ovfG_trap hn hg hs hLd h hpc hato | |
| theorem sim_ptr_ok (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) (q : WordDialect.Ptr 32) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g (.ptr q))) | |
| (hfit : c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := q.toWord :: s.dstack } x' ∧ | |
| x'.pc = base + isize g (.ptr q : WordDialect.Instr 32) := | |
| sim_word_ok (L := L) (off := off) (g := g) hg hs hpc q.toWord hLd hat hfit | |
| theorem sim_ptr_ovf (hn : g.noOvf = false) (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) (q : WordDialect.Ptr 32) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g (.ptr q))) | |
| (h : ¬ c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : RExec code x .overflow := | |
| sim_word_ovf (L := L) (off := off) (g := g) hn hg hs hpc q.toWord hLd hat h | |
| theorem sim_swap_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hat : RAt code base (lowerInstr L base off g .swap)) {b a : W} {d : List W} | |
| (hd : s.dstack = b :: a :: d) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := a :: b :: d } x' ∧ | |
| x'.pc = base + isize g (.swap : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 2) base ++ [.load r0 Reg.r4 0, .load r1 Reg.r4 4, | |
| .store Reg.r4 0 r1, .store Reg.r4 4 r0]) := hat | |
| obtain ⟨hatuf, hatr⟩ := rat_append.mp hat' | |
| have hufl := uf_length L (need g 2) base | |
| rw [hufl] at hatr | |
| obtain ⟨f0, f1, f2, f3, _⟩ := hatr | |
| have hk : 2 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, _, _⟩ := ld_step (code := code) hr1 (j := 0) (v := b) | |
| (by simp [hd]) (rd := r0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hv3, ho3, _⟩ := ld_step (code := code) hr2 (j := 1) (v := a) | |
| (by simp [hd]) (rd := r1) (by simp) (disp := 4) (by simp) (fetch_cast f1 (by omega)) | |
| have hax3 : x3.regs r0 = b := by rw [ho3 r0 (by decide), hv2] | |
| obtain ⟨x4, hs4, hr4, hpc4, hreg4⟩ := st_step (code := code) hg hr3 (j := 0) (by simp [hd]) | |
| (rs := r1) (disp := 0) (by simp) (fetch_cast f2 (by omega)) | |
| have hlen : 1 < ({ s with dstack := s.dstack.set 0 (x3.regs r1) } : State 32).dstack.length := by | |
| simp [hd] | |
| obtain ⟨x5, hs5, hr5, hpc5, _⟩ := st_step (code := code) hg hr4 (j := 1) hlen | |
| (rs := r0) (disp := 4) (by simp) (fetch_cast f3 (by omega)) | |
| have hr5' : Rel0 c p { s with dstack := (s.dstack.set 0 (x3.regs r1)).set 1 (x4.regs r0) } x5 := hr5 | |
| have e : (s.dstack.set 0 (x3.regs r1)).set 1 (x4.regs r0) = a :: b :: d := by | |
| simp [hd, hv3, hreg4, hax3] | |
| rw [e] at hr5' | |
| exact ⟨x5, (((hs1.trans hs2).trans hs3).trans hs4).trans hs5, hr5', by simp [isize]; omega⟩ | |
| theorem sim_over_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g .over)) {b a : W} | |
| {d : List W} (hd : s.dstack = b :: a :: d) (hfit : c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := a :: b :: a :: d } x' ∧ | |
| x'.pc = base + isize g (.over : WordDialect.Instr 32) := by | |
| obtain ⟨hatuf, hato, f0, f1, f2⟩ := xat_uf_ovf (L := L) (n := need g 2) rfl hat | |
| have hk : 2 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x1', hs1', hr1', hpc1', _, _⟩ := ovfG_pass hg hr1 hLd hfit hpc1 hato | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, _, _⟩ := ld_step (code := code) hr1' (j := 1) (v := a) | |
| (by simp [hd]) (rd := r0) (by simp) (disp := 4) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, _⟩ := push_pair hg hr2 r0 (by decide) hfit | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ | |
| rw [hv2, hd] at hr3 | |
| exact ⟨x3, ((hs1.trans hs1').trans hs2).trans hs3, hr3, by simp [isize]; omega⟩ | |
| theorem sim_over_ovf (hn : g.noOvf = false) (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g .over)) {b a : W} | |
| {d : List W} (hd : s.dstack = b :: a :: d) (h : ¬ c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| RExec code x .overflow := by | |
| obtain ⟨hatuf, hato, _⟩ := xat_uf_ovf (L := L) (n := need g 2) rfl hat | |
| obtain ⟨x1, hs1, hr1, hpc1, _, _⟩ := uf_pass hg hs hL (by decide) (by simp [hd]) hpc hatuf | |
| exact RExec.of_steps hs1 (ovfG_trap hn hg hr1 hLd h hpc1 hato) | |
| theorem sim_rot_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| (hat : RAt code base (lowerInstr L base off g .rot)) {cc b a : W} {d : List W} | |
| (hd : s.dstack = cc :: b :: a :: d) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := a :: cc :: b :: d } x' ∧ | |
| x'.pc = base + isize g (.rot : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 3) base ++ [.load r0 Reg.r4 0, .load r1 Reg.r4 4, | |
| .load r2 Reg.r4 8, .store Reg.r4 0 r2, .store Reg.r4 4 r0, .store Reg.r4 8 r1]) := hat | |
| obtain ⟨hatuf, hatr⟩ := rat_append.mp hat' | |
| have hufl := uf_length L (need g 3) base | |
| rw [hufl] at hatr | |
| obtain ⟨f0, f1, f2, f3, f4, f5, _⟩ := hatr | |
| have hk : 3 ≤ s.dstack.length := by simp [hd] | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, _, _⟩ := ld_step (code := code) hr1 (j := 0) (v := cc) | |
| (by simp [hd]) (rd := r0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hv3, ho3, _⟩ := ld_step (code := code) hr2 (j := 1) (v := b) | |
| (by simp [hd]) (rd := r1) (by simp) (disp := 4) (by simp) (fetch_cast f1 (by omega)) | |
| obtain ⟨x4, hs4, hr4, hpc4, hv4, ho4, _⟩ := ld_step (code := code) hr3 (j := 2) (v := a) | |
| (by simp [hd]) (rd := r2) (by simp) (disp := 8) (by simp) (fetch_cast f2 (by omega)) | |
| have hax4 : x4.regs r0 = cc := by rw [ho4 r0 (by decide), ho3 r0 (by decide), hv2] | |
| have hcx4 : x4.regs r1 = b := by rw [ho4 r1 (by decide), hv3] | |
| obtain ⟨x5, hs5, hr5, hpc5, hreg5⟩ := st_step (code := code) hg hr4 (j := 0) (by simp [hd]) | |
| (rs := r2) (disp := 0) (by simp) (fetch_cast f3 (by omega)) | |
| have hl1 : 1 < ({ s with dstack := s.dstack.set 0 (x4.regs r2) } : State 32).dstack.length := by | |
| simp [hd] | |
| obtain ⟨x6, hs6, hr6, hpc6, hreg6⟩ := st_step (code := code) hg hr5 (j := 1) hl1 | |
| (rs := r0) (disp := 4) (by simp) (fetch_cast f4 (by omega)) | |
| have hl2 : 2 < ({ { s with dstack := s.dstack.set 0 (x4.regs r2) } with | |
| dstack := (s.dstack.set 0 (x4.regs r2)).set 1 (x5.regs r0) } : State 32).dstack.length := by | |
| simp [hd] | |
| obtain ⟨x7, hs7, hr7, hpc7, _⟩ := st_step (code := code) hg hr6 (j := 2) hl2 | |
| (rs := r1) (disp := 8) (by simp) (fetch_cast f5 (by omega)) | |
| have hr7' : Rel0 c p { s with dstack := ((s.dstack.set 0 (x4.regs r2)).set 1 (x5.regs r0)).set 2 (x6.regs r1) } x7 := hr7 | |
| have e : ((s.dstack.set 0 (x4.regs r2)).set 1 (x5.regs r0)).set 2 (x6.regs r1) = | |
| a :: cc :: b :: d := by | |
| simp [hd, hv4, hreg5, hreg6, hax4, hcx4] | |
| rw [e] at hr7' | |
| exact ⟨x7, (((((hs1.trans hs2).trans hs3).trans hs4).trans hs5).trans hs6).trans hs7, hr7', | |
| by simp [isize]; omega⟩ | |
| end Ops | |
| end CM | |
| end WordDialect | |