Theory JinjaDCI.StartProg

(*  Title: JinjaDCI/BV/StartProg.thy
    Author:     Susannah Mansky
    2019-20, UIUC
*)
section "Properties and types of the starting program"

theory StartProg
imports ClassAdd
begin

lemmas wt_defs = correct_state_def conf_f_def wt_instr_def eff_def norm_eff_def app_def xcpt_app_def

declare wt_defs [simp] ― ‹ removed from @{text simp} at the end of file ›
declare start_class_def [simp]

subsection "Types"

abbreviation start_φm :: "tym" where
"start_φm  [Some([],[]),Some([Void],[])]"

fun Φ_start :: "tyP  tyP" where
"Φ_start Φ C M = (if C=Start  (M=start_m  M=clinit) then start_φm else Φ C M)"

lemma Φ_start: "C. C  Start  Φ_start Φ C = Φ C"
 "Φ_start Φ Start start_m = start_φm" "Φ_start Φ Start clinit = start_φm"
 by auto

lemma check_types_φm: "check_types (start_prog P C M) 1 0 (map OK start_φm)"
 by (auto simp: check_types_def JVM_states_unfold)

(***************************************************************************************)

subsection "Some simple properties"

lemma preallocated_start_state: "start_state P = σ  preallocated (fst(snd σ))"
using preallocated_start[of P] by(auto simp: start_state_def split_beta)

lemma start_prog_Start_super: "start_prog P C M  Start 1 Object"
 by(auto intro!: subcls1I simp: class_def fun_upd_apply)

lemma start_prog_Start_fields:
 "start_prog P C M  Start has_fields FDTs  map_of FDTs (F, Start) = None"
 by(drule Fields.cases, auto simp: class_def fun_upd_apply Object_fields)

lemma start_prog_Start_soconf:
 "(start_prog P C M),h,Start s Map.empty "
 by(simp add: soconf_def has_field_def start_prog_Start_fields)

lemma start_prog_start_shconf:
 "start_prog P C M,start_heap P s start_sheap "
(*<*) using start_prog_Start_soconf by (simp add: shconf_def fun_upd_apply) (*>*)

(************************************)

subsection "Well-typed and well-formed"

lemma start_wt_method:
assumes "P  C sees M, Static :  []Void = m in D" and "M  clinit" and "¬ is_class P Start"
shows "wt_method (start_prog P C M) Start Static [] Void 1 0 [Invokestatic C M 0, Return] [] start_φm"
 (is "wt_method ?P ?C ?b ?Ts ?Tr ?mxs ?mxl0 ?is ?xt ?τs")
proof -
  let ?cdec = "(Object, [], [start_method C M, start_clinit])"
  obtain mxs mxl ins xt where m: "m = (mxs,mxl,ins,xt)" by(cases m)
  have ca_sees: "class_add P (Start, ?cdec)  C sees M, Static :  []Void = m in D"
    by(rule class_add_sees_method[OF assms(1,3)])
  have "pc. pc < size ?is  ?P,?Tr,?mxs,size ?is,?xt  ?is!pc,pc :: ?τs"
  proof -
    fix pc assume pc: "pc < size ?is"
    then show "?P,?Tr,?mxs,size ?is,?xt  ?is!pc,pc :: ?τs"
    proof(cases "pc = 0")
      case True with assms m ca_sees show ?thesis
       by(fastforce simp: wt_method_def wt_start_def relevant_entries_def
                          is_relevant_entry_def xcpt_eff_def)
    next
      case False with pc show ?thesis
       by(simp add: wt_method_def wt_start_def relevant_entries_def
                    is_relevant_entry_def xcpt_eff_def)
    qed
  qed
  with assms check_types_φm show ?thesis by(simp add: wt_method_def wt_start_def)
qed

lemma start_clinit_wt_method:
assumes "P  C sees M, Static :  []Void = m in D" and "M  clinit" and "¬ is_class P Start"
shows "wt_method (start_prog P C M) Start Static [] Void 1 0 [Push Unit,Return] [] start_φm"
 (is "wt_method ?P ?C ?b ?Ts ?Tr ?mxs ?mxl0 ?is ?xt ?τs")
proof -
  let ?cdec = "(Object, [], [start_method C M, start_clinit])"
  obtain mxs mxl ins xt where m: "m = (mxs,mxl,ins,xt)" by(cases m)
  have ca_sees: "class_add P (Start, ?cdec)  C sees M, Static :  []Void = m in D"
    by(rule class_add_sees_method[OF assms(1,3)])
  have "pc. pc < size ?is  ?P,?Tr,?mxs,size ?is,?xt  ?is!pc,pc :: ?τs"
  proof -
    fix pc assume pc: "pc < size ?is"
    then show "?P,?Tr,?mxs,size ?is,?xt  ?is!pc,pc :: ?τs"
    proof(cases "pc = 0")
      case True with assms m ca_sees show ?thesis
       by(fastforce simp: wt_method_def wt_start_def relevant_entries_def
                          is_relevant_entry_def xcpt_eff_def)
    next
      case False with pc show ?thesis
       by(simp add: wt_method_def wt_start_def relevant_entries_def
                    is_relevant_entry_def xcpt_eff_def)
    qed
  qed
  with assms check_types_φm show ?thesis by(simp add: wt_method_def wt_start_def)
qed

lemma start_class_wf:
assumes "P  C sees M, Static :  []Void = m in D"
 and "M  clinit" and "¬ is_class P Start"
 and "Φ Start start_m = start_φm" and "Φ Start clinit = start_φm"
 and "is_class P Object"
 and "b' Ts' T' m' D'. P  Object sees start_m, b' :  Ts'T' = m' in D'
          b' = Static  Ts' = []  T' = Void"
 and "b' Ts' T' m' D'. P  Object sees clinit, b' :  Ts'T' = m' in D'
          b' = Static  Ts' = []  T' = Void"
shows "wf_cdecl (λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). wt_method P C b Ts Tr mxs mxl0 is xt (Φ C M))
       (start_prog P C M) (start_class C M)"
proof -
  from assms start_wt_method start_clinit_wt_method class_add_sees_method_rev_Obj[where P=P and C=Start]
   show ?thesis
    by(auto simp: start_method_def wf_cdecl_def wf_fdecl_def wf_mdecl_def
                  is_class_def class_def fun_upd_apply wf_clinit_def) fast+
qed

lemma start_prog_wf_jvm_prog_phi:
assumes wtp: "wf_jvm_prog⇘ΦP"
 and nstart: "¬ is_class P Start"
 and meth: "P  C sees M, Static :  []Void = m in D" and nclinit: "M  clinit"
 and Φ: "C. C  Start  Φ' C = Φ C"
 and Φ': "Φ' Start start_m = start_φm" "Φ' Start clinit = start_φm"
 and Obj_start_m: "b' Ts' T' m' D'. P  Object sees start_m, b' :  Ts'T' = m' in D'
          b' = Static  Ts' = []  T' = Void"
shows "wf_jvm_prog⇘Φ'(start_prog P C M)"
proof -
  let ?wf_md = "(λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). wt_method P C b Ts Tr mxs mxl0 is xt (Φ C M))"
  let ?wf_md' = "(λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). wt_method P C b Ts Tr mxs mxl0 is xt (Φ' C M))"
  from wtp have wf: "wf_prog ?wf_md P" by(simp add: wf_jvm_prog_phi_def)
  from wf_subcls_nCls'[OF wf nstart]
  have nsp: "cd D'. cd  set P  ¬P  fst cd * Start" by simp
  have wf_md':
    "C0 S fs ms m. (C0, S, fs, ms)  set P  m  set ms  ?wf_md' (start_prog P C M) C0 m"
  proof -
    fix C0 S fs ms m assume asms: "(C0, S, fs, ms)  set P" "m  set ms"
    with nstart have ns: "C0  Start" by(auto simp: is_class_def class_def dest: weak_map_of_SomeI)
    from wf asms have "?wf_md P C0 m" by(auto simp: wf_prog_def wf_cdecl_def wf_mdecl_def)

    with Φ[OF ns] class_add_wt_method[OF _ wf nstart]
     show "?wf_md' (start_prog P C M) C0 m" by fastforce
  qed
  from wtp have a1: "is_class P Object" by (simp add: wf_jvm_prog_phi_def)
  with wf_sees_clinit[where P=P and C=Object] wtp
   have a2: "b' Ts' T' m' D'. P  Object sees clinit, b' :  Ts'T' = m' in D'
          b' = Static  Ts' = []  T' = Void"
    by(fastforce simp: wf_jvm_prog_phi_def is_class_def dest: sees_method_fun)
  from wf have dist: "distinct_fst P" by (simp add: wf_prog_def)
  with class_add_distinct_fst[OF _ nstart] have "distinct_fst (start_prog P C M)" by simp
  moreover from wf have "wf_syscls (start_prog P C M)" by(simp add: wf_prog_def wf_syscls_def)
  moreover
  from class_add_wf_cdecl'[where wf_md'="?wf_md'", OF _ _ nsp dist] wf_md' nstart wf
  have "c. c  set P  wf_cdecl ?wf_md' (start_prog P C M) c" by(fastforce simp: wf_prog_def)
  moreover from start_class_wf[OF meth] nclinit nstart Φ' a1 Obj_start_m a2
  have "wf_cdecl ?wf_md' (start_prog P C M) (start_class C M)" by simp
  ultimately show ?thesis by(simp add: wf_jvm_prog_phi_def wf_prog_def)
qed

lemma start_prog_wf_jvm_prog:
assumes wf: "wf_jvm_prog P"
 and nstart: "¬ is_class P Start"
 and meth: "P  C sees M, Static :  []Void = m in D" and nclinit: "M  clinit"
 and Obj_start_m: "b' Ts' T' m' D'. P  Object sees start_m, b' :  Ts'T' = m' in D'
          b' = Static  Ts' = []  T' = Void"
shows "wf_jvm_prog (start_prog P C M)"
proof -
  from wf obtain Φ where wtp: "wf_jvm_prog⇘ΦP" by(clarsimp simp: wf_jvm_prog_def)

  let ?Φ' = "λC f. if C = Start  (f = start_m  f = clinit) then start_φm else Φ C f"

  from start_prog_wf_jvm_prog_phi[OF wtp nstart meth nclinit _ _ _ Obj_start_m] have
    "wf_jvm_prog⇘?Φ'(start_prog P C M)" by simp
  then show ?thesis by(auto simp: wf_jvm_prog_def)
qed

(*****************************************************************************)

subsection "Methods and instructions"

lemma start_prog_Start_sees_methods:
 "P  Object sees_methods Mm
  start_prog P C M 
  Start sees_methods Mm ++ (map_option (λm. (m,Start))  map_of [start_method C M, start_clinit])"
 by (auto simp: class_def fun_upd_apply
          dest!: class_add_sees_methods_Obj[where P=P and C=Start] intro: sees_methods_rec)

lemma start_prog_Start_sees_start_method:
 "P  Object sees_methods Mm
   start_prog P C M 
         Start sees start_m, Static : []Void = (1, 0, [Invokestatic C M 0,Return], []) in Start"
 by(auto simp: start_method_def Method_def fun_upd_apply
         dest!: start_prog_Start_sees_methods)

lemma wf_start_prog_Start_sees_start_method:
assumes wf: "wf_prog wf_md P"
shows "start_prog P C M 
         Start sees start_m, Static : []Void = (1, 0, [Invokestatic C M 0,Return], []) in Start"
proof -
  from wf have "is_class P Object" by simp
  with sees_methods_Object  obtain Mm where "P  Object sees_methods Mm"
   by(fastforce simp: is_class_def dest: sees_methods_Object)
  then show ?thesis by(rule start_prog_Start_sees_start_method)
qed

lemma start_prog_start_m_instrs:
assumes wf: "wf_prog wf_md P"
shows "(instrs_of (start_prog P C M) Start start_m) = [Invokestatic C M 0, Return]"
proof -
  from wf_start_prog_Start_sees_start_method[OF wf]
  have "start_prog P C M  Start sees start_m, Static :
           []Void = (1,0,[Invokestatic C M 0,Return],[]) in Start" by simp
  then show ?thesis by simp
qed

(******************************************************************)

declare wt_defs [simp del]

end