Theory JMM_Compiler_Type2

(*  Title:      JinjaThreads/MM/JMM_Compiler_Type2.thy
    Author:     Andreas Lochbihler
*)

section ‹Compiler correctness for JMM heap implementation 2›

theory JMM_Compiler_Type2
imports
  JMM_Compiler
  JMM_J_Typesafe
  JMM_JVM_Typesafe
  JMM_Interp
begin

theorem J2JVM_jmm_correct:
  assumes wf: "wf_J_prog P"
  and wf_start: "jmm_wf_start_state P C M vs"
  shows "legal_execution P (jmm_J_ℰ P C M vs Running) (E, ws) ⟷ 
         legal_execution (J2JVM P) (jmm_JVMd_ℰ (J2JVM P) C M vs Running) (E, ws)"
using JVMd_legal_typesafe[OF wt_J2JVM[OF wf], of C M vs Running, symmetric] wf_start
by(simp only: J_legal_typesafe[OF assms] J_JVM_conf_read.red_ℰ_eq_mexecd_ℰ[OF jmm'_J_JVM_conf_read assms] J2JVM_def o_apply compP1_def compP2_def legal_execution_compP heap_base.wf_start_state_compP jmm_typeof_addr_compP heap_base.heap_read_typed_compP)

theorem J2JVM_jmm_correct_weak:
  assumes wf: "wf_J_prog P"
  and wf_start: "jmm_wf_start_state P C M vs"
  shows "weakly_legal_execution P (jmm_J_ℰ P C M vs Running) (E, ws) ⟷ 
         weakly_legal_execution (J2JVM P) (jmm_JVMd_ℰ (J2JVM P) C M vs Running) (E, ws)"
using JVMd_weakly_legal_typesafe[OF wt_J2JVM[OF wf], of C M vs Running, symmetric] wf_start
by(simp only: J_weakly_legal_typesafe[OF assms] J_JVM_conf_read.red_ℰ_eq_mexecd_ℰ[OF jmm'_J_JVM_conf_read assms] J2JVM_def o_apply compP1_def compP2_def weakly_legal_execution_compP heap_base.wf_start_state_compP jmm_typeof_addr_compP heap_base.heap_read_typed_compP)

theorem J2JVM_jmm_correctly_synchronized:
  assumes wf: "wf_J_prog P"
  and wf_start: "jmm_wf_start_state P C M vs"
  and ka: "⋃(ka_Val ` set vs) ⊆ set jmm.start_addrs"
  shows "correctly_synchronized (J2JVM P) (jmm_JVMd_ℰ (J2JVM P) C M vs Running) ⟷ 
         correctly_synchronized P (jmm_J_ℰ P C M vs Running)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  show ?rhs unfolding correctly_synchronized_def
  proof(intro strip)
    fix E ws a a'
    assume E: "E ∈ jmm_J_ℰ P C M vs Running"
      and wf_exec: "P ⊢ (E, ws) √"
      and sc: "sequentially_consistent P (E, ws)"
      and actions: "a ∈ actions E" "a' ∈ actions E"
      and conflict: "P,E ⊢ a † a'"

    from E wf_exec sc
    have "legal_execution P (jmm_J_ℰ P C M vs Running) (E, ws)"
      by(rule sc_legal.SC_is_legal[OF J_allocated_progress.J_sc_legal[OF jmm_J_allocated_progress wf jmm_heap_read_typeable wf_start ka]])
    hence "legal_execution (J2JVM P) (jmm_JVMd_ℰ (J2JVM P) C M vs Running) (E, ws)"
      by(simp only: J2JVM_jmm_correct[OF wf wf_start])
    hence "E ∈ jmm_JVMd_ℰ (J2JVM P) C M vs Running" "J2JVM P ⊢ (E, ws) √"
      by(simp_all add: gen_legal_execution.simps)
    moreover from sc have "sequentially_consistent (J2JVM P) (E, ws)"
      by(simp add: J2JVM_def compP2_def)
    moreover from conflict have "J2JVM P,E ⊢ a † a'"
      by(simp add: J2JVM_def compP2_def)
    ultimately have "J2JVM P,E ⊢ a ≤hb a' ∨ J2JVM P,E ⊢ a' ≤hb a"
      using ‹?lhs› actions by(auto simp add: correctly_synchronized_def)
    thus "P,E ⊢ a ≤hb a' ∨ P,E ⊢ a' ≤hb a"
      by(simp add: J2JVM_def compP2_def)
  qed
next
  assume ?rhs
  show ?lhs unfolding correctly_synchronized_def
  proof(intro strip)
    fix E ws a a'
    assume E: "E ∈ jmm_JVMd_ℰ (J2JVM P) C M vs Running"
      and wf_exec: "J2JVM P ⊢ (E, ws) √"
      and sc: "sequentially_consistent (J2JVM P) (E, ws)"
      and actions: "a ∈ actions E" "a' ∈ actions E"
      and conflict: "J2JVM P,E ⊢ a † a'"

    from wf have "wf_jvm_prog (J2JVM P)" by(rule wt_J2JVM)
    then obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ (J2JVM P)"
      by(auto simp add: wf_jvm_prog_def)
    from wf_start have wf_start': "jmm_wf_start_state (J2JVM P) C M vs"
      by(simp add: J2JVM_def compP2_def heap_base.wf_start_state_compP)
    from E wf_exec sc
    have "legal_execution (J2JVM P) (jmm_JVMd_ℰ (J2JVM P) C M vs Running) (E, ws)"
      by(rule sc_legal.SC_is_legal[OF JVM_allocated_progress.JVM_sc_legal[OF jmm_JVM_allocated_progress wf' jmm_heap_read_typeable wf_start' ka]])
    hence "legal_execution P (jmm_J_ℰ P C M vs Running) (E, ws)"
      by(simp only: J2JVM_jmm_correct[OF wf wf_start])
    hence "E ∈ jmm_J_ℰ P C M vs Running" "P ⊢ (E, ws) √"
      by(simp_all add: gen_legal_execution.simps)
    moreover from sc have "sequentially_consistent P (E, ws)"
      by(simp add: J2JVM_def compP2_def)
    moreover from conflict have "P,E ⊢ a † a'"
      by(simp add: J2JVM_def compP2_def)
    ultimately have "P,E ⊢ a ≤hb a' ∨ P,E ⊢ a' ≤hb a"
      using ‹?rhs› actions by(auto simp add: correctly_synchronized_def)
    thus "J2JVM P,E ⊢ a ≤hb a' ∨ J2JVM P,E ⊢ a' ≤hb a" 
      by(simp add: J2JVM_def compP2_def)
  qed
qed

end