# Theory StartProg

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

theory StartProg
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 ≺⇧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 √"

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⇩0 ?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"
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
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⇩0 ?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"
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
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⇩0,is,xt)). wt_method P C b Ts T⇩r mxs mxl⇩0 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,T⇩r,(mxs,mxl⇩0,is,xt)). wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M))"
let ?wf_md' = "(λP C (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)). wt_method P C b Ts T⇩r mxs mxl⇩0 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⇩0 S fs ms m. (C⇩0, S, fs, ms) ∈ set P ⟹ m ∈ set ms ⟹ ?wf_md' (start_prog P C M) C⇩0 m"
proof -
fix C⇩0 S fs ms m assume asms: "(C⇩0, S, fs, ms) ∈ set P" "m ∈ set ms"
with nstart have ns: "C⇩0 ≠ Start" by(auto simp: is_class_def class_def dest: weak_map_of_SomeI)
from wf asms have "?wf_md P C⇩0 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⇩0 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```