| import WordIR.Straight |
|
|
| /-! |
| # WordIR.Program |
|
|
| Whole-program lifting for straight-line code: `code ++ [HALT]` run from `pc = 0` halts with |
| the state `execSeq` computes, or traps with the trap `execSeq` reports. |
| -/ |
|
|
| namespace WordDialect |
| namespace IR |
|
|
| theorem exec_straight_halt {n : Nat} {code : List (Instr n)} {s s1 : State n} |
| (hs : ∀ i ∈ code, i.isStraight = true) (hpc : s.pc = 0) |
| (h : execSeq code s = .next s1) : |
| Exec (code ++ [.halt]) s (.halted s1) := by |
| have hat : At (code ++ [.halt]) s.pc code := by |
| have := at_embed ([] : Prog n) code [.halt] |
| simpa [hpc] using this |
| obtain ⟨hst, hpc1⟩ := execSeq_steps hs hat h |
| refine Exec.of_steps hst (.halt ?_) |
| have hfetch : (code ++ [.halt])[s1.pc]? = some .halt := by |
| rw [hpc1, hpc]; simp |
| rw [step_of_fetch hfetch]; rfl |
|
|
| theorem exec_straight_trap {n : Nat} {code : List (Instr n)} {s : State n} {t : Trap} |
| (hs : ∀ i ∈ code, i.isStraight = true) (hpc : s.pc = 0) |
| (h : execSeq code s = .trapped t) : |
| Exec (code ++ [.halt]) s (.trapped t) := by |
| have hat : At (code ++ [.halt]) s.pc code := by |
| have := at_embed ([] : Prog n) code [.halt] |
| simpa [hpc] using this |
| obtain ⟨s1, hst, ht⟩ := execSeq_trap hs hat h |
| exact Exec.of_steps hst (.trap ht) |
|
|
| end IR |
| end WordDialect |
|
|
