(*  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 :: "ty_m" where
"start_φ_m ≡ [Some([],[]),Some([Void],[])]"

fun Φ_start :: "ty_P → ty_P" 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 ≺¹ 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 ?T_r ?mxs ?mxl₀ ?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,?T_r,?mxs,size ?is,?xt ⊨ ?is!pc,pc :: ?τs"
  proof -
    fix pc assume pc: "pc < size ?is"
    then show "?P,?T_r,?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 ?T_r ?mxs ?mxl₀ ?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,?T_r,?mxs,size ?is,?xt ⊨ ?is!pc,pc :: ?τs"
  proof -
    fix pc assume pc: "pc < size ?is"
    then show "?P,?T_r,?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,T_r,(mxs,mxl₀,is,xt)). wt_method P C b Ts T_r mxs mxl₀ 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_<Phi> 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_<Phi>' (start_prog P C M)"
proof -
  let ?wf_md = "(λP C (M,b,Ts,T_r,(mxs,mxl₀,is,xt)). wt_method P C b Ts T_r mxs mxl₀ is xt (Φ C M))"
  let ?wf_md' = "(λP C (M,b,Ts,T_r,(mxs,mxl₀,is,xt)). wt_method P C b Ts T_r mxs mxl₀ 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':
    "∧C₀ S fs ms m. (C₀, S, fs, ms) ∈ set P ==> m ∈ set ms ==> ?wf_md' (start_prog P C M) C₀ m"
  proof -
    fix C₀ S fs ms m assume asms: "(C₀, S, fs, ms) ∈ set P" "m ∈ set ms"
    with nstart have ns: "C₀ ≠ Start" by(auto simp: is_class_def class_def dest: weak_map_of_SomeI)
    from wf asms have "?wf_md P C₀ 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) C₀ 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_<Phi> 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