Theory VeriComp.Compiler

section ‹Compiler Between Static Representations›

theory Compiler
  imports Language Simulation
begin

definition option_comp :: "('a ⇒ 'b option) ⇒ ('c ⇒ 'a option) ⇒ 'c ⇒ 'b option" (infix ‹⇚› 50) where
  "(f ⇚ g) x ≡ Option.bind (g x) f"

context
  fixes f :: "('a ⇒ 'a option)"
begin

fun option_comp_pow :: "nat ⇒ 'a ⇒ 'a option" where
  "option_comp_pow 0 = (λ_. None)" |
  "option_comp_pow (Suc 0) = f" |
  "option_comp_pow (Suc n) = (option_comp_pow n ⇚ f)"

end

locale compiler =
  L1: language step1 final1 load1 +
  L2: language step2 final2 load2 +
  backward_simulation step1 final1 step2 final2 match order
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and final1 and load1 :: "'prog1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and final2 and load2 :: "'prog2 ⇒ 'state2 ⇒ bool" and
    match and
    order :: "'index ⇒ 'index ⇒ bool" +
  fixes
    compile :: "'prog1 ⇒ 'prog2 option"
  assumes
    compile_load:
      "compile p1 = Some p2 ⟹ load2 p2 s2 ⟹ ∃s1 i. load1 p1 s1 ∧ match i s1 s2"
begin

text ‹
The @{locale compiler} locale relates two languages, L1 and L2, by a backward simulation and provides a @{term compile} partial function from a concrete program in L1 to a concrete program in L2.
The only assumption is that a successful compilation results in a program which, when loaded, is equivalent to the loaded initial program.
›


subsection ‹Preservation of behaviour›

corollary behaviour_preservation:
  assumes
    compiles: "compile p1 = Some p2" and
    behaves: "L2.prog_behaves p2 b2" and
    not_wrong: "¬ is_wrong b2"
  shows "∃b1 i.  L1.prog_behaves p1 b1 ∧ rel_behaviour (match i) b1 b2"
proof -
  obtain s2 where "load2 p2 s2" and "L2.state_behaves s2 b2"
    using behaves L2.prog_behaves_def by auto
  obtain i s1 where "load1 p1 s1" "match i s1 s2"
    using compile_load[OF compiles ‹load2 p2 s2›]
    by auto
  then show ?thesis
    using simulation_behaviour[OF ‹L2.state_behaves s2 b2› not_wrong ‹match i s1 s2›]
    by (auto simp: L1.prog_behaves_def)
qed

end

subsection ‹Composition of compilers›

lemma compiler_composition:
  assumes
    "compiler step1 final1 load1 step2 final2 load2 match1 order1 compile1" and
    "compiler step2 final2 load2 step3 final3 load3 match2 order2 compile2"
  shows "compiler step1 final1 load1 step3 final3 load3
    (rel_comp match1 match2) (lex_prodp order1⇧+⇧+ order2) (compile2 ⇚ compile1)"
proof (rule compiler.intro) 
  show "language step1 final1"
    using assms(1)[THEN compiler.axioms(1)] .
next
  show "language step3 final3"
    using assms(2)[THEN compiler.axioms(2)] .
next
  show "backward_simulation step1 final1 step3 final3
     (rel_comp match1 match2) (lex_prodp order1⇧+⇧+ order2)"
    using backward_simulation_composition[OF assms[THEN compiler.axioms(3)]] .
next
  show "compiler_axioms load1 load3 (rel_comp match1 match2) (compile2 ⇚ compile1)"
  proof unfold_locales
    fix p1 p3 s3
    assume
      compile: "(compile2 ⇚ compile1) p1 = Some p3" and
      load: "load3 p3 s3"
    obtain p2 where c1: "compile1 p1 = Some p2" and c2: "compile2 p2 = Some p3"
      using compile by (auto simp: bind_eq_Some_conv option_comp_def)
    obtain s2 i' where l2: "load2 p2 s2" and "match2 i' s2 s3"
      using assms(2)[THEN compiler.compile_load, OF c2 load]
      by auto
    moreover obtain s1 i where "load1 p1 s1" and "match1 i s1 s2"
      using assms(1)[THEN compiler.compile_load, OF c1 l2]
      by auto
    ultimately show "∃s1 i. load1 p1 s1 ∧ rel_comp match1 match2 i s1 s3"
      unfolding rel_comp_def by auto
  qed
qed

lemma compiler_composition_pow:
  assumes
    "compiler step final load step final load match order compile"
  shows "compiler step final load step final load
    (rel_comp_pow match) (lexp order⇧+⇧+) (option_comp_pow compile n)"
proof (induction n rule: option_comp_pow.induct)
  case 1
  show ?case
    using assms
    by (auto intro: compiler.axioms compiler.intro compiler_axioms.intro backward_simulation_pow)
next
  case 2
  show ?case
  proof (rule compiler.intro)
    show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc 0))"
    proof unfold_locales
      fix p1 p2 s2
      assume
        "option_comp_pow compile (Suc 0) p1 = Some p2" and
        "load p2 s2"
      thus "∃s1 i. load p1 s1 ∧ rel_comp_pow match i s1 s2"
        using compiler.compile_load[OF assms(1)]
        by (metis option_comp_pow.simps(2) rel_comp_pow.simps(2))
    qed
  qed (auto intro: assms compiler.axioms backward_simulation_pow)
next
  case (3 n')
  show ?case
  proof (rule compiler.intro)
    show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc (Suc n')))"
    proof unfold_locales
      fix p1 p3 s3
      assume
        "option_comp_pow compile  (Suc (Suc n')) p1 = Some p3" and
        "load p3 s3"
      then obtain p2 where
        comp: "compile p1 = Some p2" and
        comp_IH: "option_comp_pow compile (Suc n') p2 = Some p3"
        by (auto simp: option_comp_def bind_eq_Some_conv)
      obtain s2 i' where "load p2 s2" and "rel_comp_pow match i' s2 s3"
        using compiler.compile_load[OF "3.IH" comp_IH ‹load p3 s3›]
        by auto
      moreover obtain s1 i where "load p1 s1" and "match i s1 s2"
        using compiler.compile_load[OF assms comp ‹load p2 s2›]
        by auto
      moreover have "rel_comp_pow match (i # i') s1 s3"
        using ‹rel_comp_pow match i' s2 s3› ‹match i s1 s2› rel_comp_pow.elims(2) by fastforce
      ultimately show "∃s1 i. load p1 s1 ∧ rel_comp_pow match i s1 s3"
        by blast
    qed
  qed (auto intro: assms compiler.axioms backward_simulation_pow)
qed

end