Sync from GitHub at 25c8330: hardware-in-the-loop rig, SAM D21 board, guard elimination on RV32/Cortex-M3
0e9783b verified | import RV32.SimMem | |
| /-! | |
| # RV32.SimMemOps | |
| The address bounds guard `movImm rt, memSize; bltu t0, rt, ok; exitTrap badAddress`, and the | |
| simulation theorems for `push`, `pop`, `load`, `store`. RV32 has no indexed addressing, so `load` | |
| and `store` compute the cell's address with `slli t0, t0, 2; add t0, s3` (`idx_steps`). | |
| -/ | |
| namespace WordDialect | |
| namespace RV32 | |
| open Reg | |
| 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 ult_memSize {a : W} {n : Nat} (hn : n < 2 ^ 32) : | |
| a.ult (BitVec.ofNat 32 n) = decide (a.toNat < n) := by | |
| simp [BitVec.ult_eq_decide, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hn] | |
| /-- The bounds guard, passing case. -/ | |
| theorem addr_pass (hs : Rel0 c p s x) {rt : Reg} (hrt : rt = t1 ∨ rt = t2) {n : Nat} | |
| (hn : n < 2 ^ 32) {t : Nat} (ht : t = x.pc + 3) {a : W} (hrax : x.regs t0 = a) (ha : a.toNat < n) | |
| (hat : RAt code x.pc [.movImm rt (BitVec.ofNat 32 n), .bcc .ult t0 rt t, | |
| .exitTrap .badAddress]) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p s x' ∧ x'.pc = x.pc + 3 ∧ x'.regs t0 = a ∧ | |
| (∀ r, r ≠ rt → x'.regs r = x.regs r) ∧ x'.mem = x.mem := by | |
| subst ht | |
| obtain ⟨f0, f1, f2, _⟩ := hat | |
| have hrt' : rt = t0 ∨ rt = t1 ∨ rt = t2 ∨ rt = t3 := by rcases hrt with h | h <;> simp [h] | |
| have hne : t0 ≠ rt := by rcases hrt with h | h <;> simp [h] | |
| obtain ⟨x1, hs1, hr1, hpc1, hv1, ho1, hm1⟩ := movimm_step (code := code) hs (rd := rt) hrt' | |
| (v := BitVec.ofNat 32 n) f0 | |
| have hax1 : x1.regs t0 = a := by rw [ho1 t0 hne, hrax] | |
| have hhold : Cond.eval .ult (x1.regs t0) (x1.regs rt) = true := by | |
| simp only [Cond.eval, hax1, hv1]; rw [ult_memSize hn]; simpa using ha | |
| have hg := guard_pass (code := code) (pc := x.pc + 1) (m := x1) (t := .badAddress) | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ hpc1 hhold | |
| refine ⟨{ x1 with pc := x.pc + 1 + 2 }, hs1.trans hg, hr1.congr rfl rfl rfl rfl rfl rfl rfl, | |
| by simp, by simp [hax1], ?_, by simp [hm1]⟩ | |
| intro r hr; simp [ho1 r hr] | |
| /-- The bounds guard, failing case. -/ | |
| theorem addr_trap (hs : Rel0 c p s x) {rt : Reg} (hrt : rt = t1 ∨ rt = t2) {n : Nat} | |
| (hn : n < 2 ^ 32) {t : Nat} (ht : t = x.pc + 3) {a : W} (hrax : x.regs t0 = a) (ha : ¬ a.toNat < n) | |
| (hat : RAt code x.pc [.movImm rt (BitVec.ofNat 32 n), .bcc .ult t0 rt t, | |
| .exitTrap .badAddress]) : | |
| RExec code x (.trapped .badAddress) := by | |
| subst ht | |
| obtain ⟨f0, f1, f2, _⟩ := hat | |
| have hrt' : rt = t0 ∨ rt = t1 ∨ rt = t2 ∨ rt = t3 := by rcases hrt with h | h <;> simp [h] | |
| have hne : t0 ≠ rt := by rcases hrt with h | h <;> simp [h] | |
| obtain ⟨x1, hs1, hr1, hpc1, hv1, ho1, hm1⟩ := movimm_step (code := code) hs (rd := rt) hrt' | |
| (v := BitVec.ofNat 32 n) f0 | |
| have hax1 : x1.regs t0 = a := by rw [ho1 t0 hne, hrax] | |
| have hhold : Cond.eval .ult (x1.regs t0) (x1.regs rt) = false := by | |
| simp only [Cond.eval, hax1, hv1]; rw [ult_memSize hn]; simpa using ha | |
| exact RExec.of_steps hs1 | |
| (guard_trap (code := code) (pc := x.pc + 1) (m := x1) (t := .badAddress) | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ hpc1 hhold) | |
| theorem sim_push_ok (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) {r : Nat} | |
| (hr : r < c.nregs) (hLd : L.dLim = ofN (c.dBase + 4)) | |
| (hat : RAt code base (lowerInstr L base off g (.push r))) | |
| (hfit : c.dBase + 4 * (s.dstack.length + 1) ≤ c.dEnd) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := s.regs r :: s.dstack } x' ∧ | |
| x'.pc = base + isize g (.push r : 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 | |
| have hst : step code x0 = .next (x0.mov t0 (s.regs r)) := by | |
| rw [rstep_of_fetch (by rw [hpc0]; exact f0), ld_reg hr0 hr t0 rfl] | |
| have hr1 : Rel0 c p s (x0.mov t0 (s.regs r)) := mov_rel0 hr0 t0 (scratch_ne t0 (by simp)) _ | |
| have hpc1 : (x0.mov t0 (s.regs r)).pc = base + ovfSize g + 1 := by simp [M.mov, M.setReg, M.adv, hpc0] | |
| obtain ⟨x2, hs2, hr2, hpc2, _⟩ := push_pair hg hr1 t0 (by decide) hfit | |
| ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), trivial⟩ | |
| have hv : (x0.mov t0 (s.regs r)).regs t0 = s.regs r := by simp [M.mov, M.setReg, M.adv] | |
| rw [hv] at hr2 | |
| exact ⟨x2, (hs0.trans (RSteps.single hst)).trans hs2, hr2, by simp [isize]; omega⟩ | |
| theorem sim_push_ovf (hn : g.noOvf = false) (hg : Geom c) (hs : Rel0 c p s x) (hpc : x.pc = base) {r : Nat} | |
| (hLd : L.dLim = ofN (c.dBase + 4)) (hat : RAt code base (lowerInstr L base off g (.push r))) | |
| (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_pop_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hs : Rel0 c p s x) (hpc : x.pc = base) | |
| {r : Nat} (hr : r < c.nregs) (hat : RAt code base (lowerInstr L base off g (.pop r))) | |
| {a : W} {d : List W} (hd : s.dstack = a :: d) : | |
| ∃ x', RSteps code x x' ∧ | |
| Rel0 c p { s with dstack := d, regs := State.setReg s.regs r a } x' ∧ | |
| x'.pc = base + isize g (.pop r : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 1) base ++ [.load t0 Reg.s1 0, .addImm Reg.s1 4, | |
| .store Reg.s2 (4 * (r : Int)) t0]) := 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 := t0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, ho3⟩ := adj_step (code := code) hg hr2 (n := 1) (by simp [hd]) | |
| (δ := 4) (by simp) (fetch_cast f1 (by omega)) | |
| have hax3 : x3.regs t0 = a := by rw [ho3 t0 (by decide), hv2] | |
| obtain ⟨mem', e4, hr4⟩ := st_reg hg hr3 hr t0 (disp := 4 * (r : Int)) rfl | |
| have hst4 : step code x3 = .next { x3.adv with mem := mem' } := by | |
| rw [rstep_of_fetch (fetch_cast f2 (by omega)), e4] | |
| have hr4' : Rel0 c p { s with dstack := s.dstack.drop 1, regs := State.setReg s.regs r (x3.regs t0) } | |
| { x3.adv with mem := mem' } := hr4 | |
| have e : s.dstack.drop 1 = d := by simp [hd] | |
| rw [e, hax3] at hr4' | |
| exact ⟨_, ((hs1.trans hs2).trans hs3).trans (RSteps.single hst4), hr4', | |
| by simp [M.adv, isize]; omega⟩ | |
| theorem sim_load_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hMs : L.memSize = c.M) | |
| (hs : Rel0 c p s x) (hpc : x.pc = base) (hat : RAt code base (lowerInstr L base off g .load)) | |
| {a v : W} {d : List W} (hd : s.dstack = a :: d) (hv : s.mem.read? a = some v) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := v :: d } x' ∧ | |
| x'.pc = base + isize g (.load : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 1) base ++ [.load t0 Reg.s1 0, .movImm t1 (BitVec.ofNat 32 L.memSize), | |
| .bcc .ult t0 t1 (base + ufSize (need g 1) + 4), .exitTrap .badAddress, .shlImm t0 2, .add t0 Reg.s3, | |
| .load t0 t0 0, .store Reg.s1 0 t0]) := 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, f3, f4, f5, f6, f7, _⟩ := hatr | |
| have hk : 1 ≤ s.dstack.length := by simp [hd] | |
| have hMlt : c.M < 2 ^ 32 := by have := hg.mb_lt; omega | |
| have hlt : a.toNat < c.M := by | |
| obtain ⟨hvv, _⟩ := Memory.read?_some hv | |
| have := hs.irvalid a | |
| rw [hvv] at this | |
| simpa using this.symm | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, ho2, hm2⟩ := ld_step (code := code) hr1 (j := 0) (v := a) | |
| (by simp [hd]) (rd := t0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hax3, ho3, hm3⟩ := addr_pass (code := code) hr2 (rt := t1) (by simp) | |
| (n := c.M) hMlt (t := base + ufSize (need g 1) + 4) (by omega) hv2 hlt (by | |
| rw [← hMs] | |
| refine ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), fetch_cast f3 (by omega), trivial⟩) | |
| obtain ⟨x4, hs4, hr4, hpc4, hax4, _, _⟩ := idx_steps hr3 hax3 | |
| ⟨fetch_cast f4 (by omega), fetch_cast f5 (by omega), trivial⟩ | |
| have hst5 : step code x4 = .next (x4.mov t0 v) := by | |
| rw [rstep_of_fetch (fetch_cast f6 (by omega)), ld_mem hr4 hv hax4] | |
| have hr5 : Rel0 c p s (x4.mov t0 v) := mov_rel0 hr4 t0 (scratch_ne t0 (by simp)) v | |
| obtain ⟨x6, hs6, hr6, hpc6, _⟩ := st_step (code := code) hg hr5 (j := 0) (by simp [hd]) | |
| (rs := t0) (disp := 0) (by simp) (fetch_cast f7 (by simp [M.mov, M.setReg, M.adv]; omega)) | |
| have e : s.dstack.set 0 ((x4.mov t0 v).regs t0) = v :: d := by | |
| simp [hd, M.mov, M.setReg, M.adv] | |
| rw [e] at hr6 | |
| exact ⟨x6, ((((hs1.trans hs2).trans hs3).trans hs4).trans (RSteps.single hst5)).trans hs6, hr6, | |
| by simp [M.mov, M.setReg, M.adv, isize] at *; omega⟩ | |
| theorem sim_load_trap (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hMs : L.memSize = c.M) | |
| (hs : Rel0 c p s x) (hpc : x.pc = base) (hat : RAt code base (lowerInstr L base off g .load)) | |
| {a : W} {d : List W} (hd : s.dstack = a :: d) (hv : s.mem.read? a = none) : | |
| RExec code x (.trapped .badAddress) := by | |
| have hat' : RAt code base (uf L (need g 1) base ++ [.load t0 Reg.s1 0, .movImm t1 (BitVec.ofNat 32 L.memSize), | |
| .bcc .ult t0 t1 (base + ufSize (need g 1) + 4), .exitTrap .badAddress, .shlImm t0 2, .add t0 Reg.s3, | |
| .load t0 t0 0, .store Reg.s1 0 t0]) := 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, f3, _⟩ := hatr | |
| have hk : 1 ≤ s.dstack.length := by simp [hd] | |
| have hMlt : c.M < 2 ^ 32 := by have := hg.mb_lt; omega | |
| have hge : ¬ a.toNat < c.M := by | |
| have hvv := (Memory.read?_none_iff s.mem a).mp hv | |
| have := hs.irvalid a | |
| rw [hvv] at this | |
| simpa using this | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, ho2, hm2⟩ := ld_step (code := code) hr1 (j := 0) (v := a) | |
| (by simp [hd]) (rd := t0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| exact RExec.of_steps (hs1.trans hs2) (addr_trap (code := code) hr2 (rt := t1) (by simp) | |
| (n := c.M) hMlt (t := base + ufSize (need g 1) + 4) (by omega) hv2 hge (by | |
| rw [← hMs] | |
| refine ⟨fetch_cast f1 (by omega), fetch_cast f2 (by omega), fetch_cast f3 (by omega), trivial⟩)) | |
| theorem sim_store_ok (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hMs : L.memSize = c.M) | |
| (hs : Rel0 c p s x) (hpc : x.pc = base) (hat : RAt code base (lowerInstr L base off g .store)) | |
| {a v : W} {d : List W} (hd : s.dstack = a :: v :: d) {m : Memory 32} | |
| (hw : s.mem.write? a v = some m) : | |
| ∃ x', RSteps code x x' ∧ Rel0 c p { s with dstack := d, mem := m } x' ∧ | |
| x'.pc = base + isize g (.store : WordDialect.Instr 32) := by | |
| have hat' : RAt code base (uf L (need g 2) base ++ [.load t0 Reg.s1 0, .load t1 Reg.s1 4, | |
| .movImm t2 (BitVec.ofNat 32 L.memSize), .bcc .ult t0 t2 (base + ufSize (need g 2) + 5), | |
| .exitTrap .badAddress, .shlImm t0 2, .add t0 Reg.s3, .store t0 0 t1, .addImm Reg.s1 8]) := 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, f4, f5, f6, f7, f8, _⟩ := hatr | |
| have hk : 2 ≤ s.dstack.length := by simp [hd] | |
| have hMlt : c.M < 2 ^ 32 := by have := hg.mb_lt; omega | |
| have hv : s.mem.valid a = true := by | |
| by_cases hh : s.mem.valid a = true | |
| · exact hh | |
| · have := (Memory.write?_none_iff s.mem a v).mpr (by simpa using hh); rw [hw] at this; simp at this | |
| have hlt : a.toNat < c.M := by | |
| have := hs.irvalid a | |
| rw [hv] at this | |
| simpa using this.symm | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, ho2, hm2⟩ := ld_step (code := code) hr1 (j := 0) (v := a) | |
| (by simp [hd]) (rd := t0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hv3, ho3, hm3⟩ := ld_step (code := code) hr2 (j := 1) (v := v) | |
| (by simp [hd]) (rd := t1) (by simp) (disp := 4) (by simp) (fetch_cast f1 (by omega)) | |
| have hax3 : x3.regs t0 = a := by rw [ho3 t0 (by decide), hv2] | |
| obtain ⟨x4, hs4, hr4, hpc4, hax4, ho4, hm4⟩ := addr_pass (code := code) hr3 (rt := t2) (by simp) | |
| (n := c.M) hMlt (t := base + ufSize (need g 2) + 5) (by omega) hax3 hlt (by | |
| rw [← hMs] | |
| refine ⟨fetch_cast f2 (by omega), fetch_cast f3 (by omega), fetch_cast f4 (by omega), trivial⟩) | |
| have hcx4 : x4.regs t1 = v := by rw [ho4 t1 (by decide), hv3] | |
| obtain ⟨x5, hs5, hr5, hpc5, hax5, ho5, _⟩ := idx_steps hr4 hax4 | |
| ⟨fetch_cast f5 (by omega), fetch_cast f6 (by omega), trivial⟩ | |
| have hcx5 : x5.regs t1 = v := by rw [ho5 t1 (by decide), hcx4] | |
| obtain ⟨mem', e6, hr6⟩ := st_mem hg hr5 hw hax5 hcx5 | |
| have hst6 : step code x5 = .next { x5.adv with mem := mem' } := by | |
| rw [rstep_of_fetch (fetch_cast f7 (by omega)), e6] | |
| have hlen : 2 ≤ ({ s with mem := m } : State 32).dstack.length := by simp [hd] | |
| obtain ⟨x7, hs7, hr7, hpc7, _⟩ := adj_step (code := code) hg hr6 (n := 2) hlen (δ := 8) (by simp) | |
| (fetch_cast f8 (by simp [M.adv]; omega)) | |
| have hr7' : Rel0 c p { s with dstack := d, mem := m } x7 := by | |
| have : ({ { s with mem := m } with dstack := ({ s with mem := m } : State 32).dstack.drop 2 } : State 32) | |
| = { s with dstack := d, mem := m } := by simp [hd] | |
| rw [← this]; exact hr7 | |
| exact ⟨x7, (((((hs1.trans hs2).trans hs3).trans hs4).trans hs5).trans (RSteps.single hst6)).trans hs7, | |
| hr7', by simp [M.adv, isize] at *; omega⟩ | |
| theorem sim_store_trap (hg : Geom c) (hL : L.dEnd = ofN c.dEnd) (hMs : L.memSize = c.M) | |
| (hs : Rel0 c p s x) (hpc : x.pc = base) (hat : RAt code base (lowerInstr L base off g .store)) | |
| {a v : W} {d : List W} (hd : s.dstack = a :: v :: d) (hw : s.mem.write? a v = none) : | |
| RExec code x (.trapped .badAddress) := by | |
| have hat' : RAt code base (uf L (need g 2) base ++ [.load t0 Reg.s1 0, .load t1 Reg.s1 4, | |
| .movImm t2 (BitVec.ofNat 32 L.memSize), .bcc .ult t0 t2 (base + ufSize (need g 2) + 5), | |
| .exitTrap .badAddress, .shlImm t0 2, .add t0 Reg.s3, .store t0 0 t1, .addImm Reg.s1 8]) := 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, f4, _⟩ := hatr | |
| have hk : 2 ≤ s.dstack.length := by simp [hd] | |
| have hMlt : c.M < 2 ^ 32 := by have := hg.mb_lt; omega | |
| have hge : ¬ a.toNat < c.M := by | |
| have hvv := (Memory.write?_none_iff s.mem a v).mp hw | |
| have := hs.irvalid a | |
| rw [hvv] at this | |
| simpa using this | |
| obtain ⟨x1, hs1, hr1, hpc1, hm1, _⟩ := uf_pass hg hs hL (by decide) hk hpc hatuf | |
| obtain ⟨x2, hs2, hr2, hpc2, hv2, ho2, hm2⟩ := ld_step (code := code) hr1 (j := 0) (v := a) | |
| (by simp [hd]) (rd := t0) (by simp) (disp := 0) (by simp) (fetch_cast f0 (by omega)) | |
| obtain ⟨x3, hs3, hr3, hpc3, hv3, ho3, hm3⟩ := ld_step (code := code) hr2 (j := 1) (v := v) | |
| (by simp [hd]) (rd := t1) (by simp) (disp := 4) (by simp) (fetch_cast f1 (by omega)) | |
| have hax3 : x3.regs t0 = a := by rw [ho3 t0 (by decide), hv2] | |
| exact RExec.of_steps ((hs1.trans hs2).trans hs3) (addr_trap (code := code) hr3 (rt := t2) | |
| (by simp) (n := c.M) hMlt (t := base + ufSize (need g 2) + 5) (by omega) hax3 hge (by | |
| rw [← hMs] | |
| refine ⟨fetch_cast f2 (by omega), fetch_cast f3 (by omega), fetch_cast f4 (by omega), trivial⟩)) | |
| end Ops | |
| end RV32 | |
| end WordDialect | |