header {* \isaheader{The JVM Type System as Semilattice} *}
theory JVM_SemiType imports SemiType begin
type_synonym ty⇣l = "ty err list"
type_synonym ty⇣s = "ty list"
type_synonym ty⇣i = "ty⇣s × ty⇣l"
type_synonym ty⇣i' = "ty⇣i option"
type_synonym ty⇣m = "ty⇣i' list"
type_synonym ty⇣P = "mname => cname => ty⇣m"
definition stk_esl :: "'c prog => nat => ty⇣s esl"
where
"stk_esl P mxs ≡ upto_esl mxs (SemiType.esl P)"
definition loc_sl :: "'c prog => nat => ty⇣l sl"
where
"loc_sl P mxl ≡ Listn.sl mxl (Err.sl (SemiType.esl P))"
definition sl :: "'c prog => nat => nat => ty⇣i' err sl"
where
"sl P mxs mxl ≡
Err.sl(Opt.esl(Product.esl (stk_esl P mxs) (Err.esl(loc_sl P mxl))))"
definition states :: "'c prog => nat => nat => ty⇣i' err set"
where "states P mxs mxl ≡ fst(sl P mxs mxl)"
definition le :: "'c prog => nat => nat => ty⇣i' err ord"
where
"le P mxs mxl ≡ fst(snd(sl P mxs mxl))"
definition sup :: "'c prog => nat => nat => ty⇣i' err binop"
where
"sup P mxs mxl ≡ snd(snd(sl P mxs mxl))"
definition sup_ty_opt :: "['c prog,ty err,ty err] => bool"
("_ |- _ <=T _" [71,71,71] 70)
where
"sup_ty_opt P ≡ Err.le (subtype P)"
definition sup_state :: "['c prog,ty⇣i,ty⇣i] => bool"
("_ |- _ <=i _" [71,71,71] 70)
where
"sup_state P ≡ Product.le (Listn.le (subtype P)) (Listn.le (sup_ty_opt P))"
definition sup_state_opt :: "['c prog,ty⇣i',ty⇣i'] => bool"
("_ |- _ <=' _" [71,71,71] 70)
where
"sup_state_opt P ≡ Opt.le (sup_state P)"
abbreviation
sup_loc :: "['c prog,ty⇣l,ty⇣l] => bool" ("_ |- _ [<=T] _" [71,71,71] 70)
where "P |- LT [<=T] LT' ≡ list_all2 (sup_ty_opt P) LT LT'"
notation (xsymbols)
sup_ty_opt ("_ \<turnstile> _ ≤⇩\<top> _" [71,71,71] 70) and
sup_state ("_ \<turnstile> _ ≤⇩i _" [71,71,71] 70) and
sup_state_opt ("_ \<turnstile> _ ≤' _" [71,71,71] 70) and
sup_loc ("_ \<turnstile> _ [≤⇩\<top>] _" [71,71,71] 70)
section "Unfolding"
lemma JVM_states_unfold:
"states P mxs mxl ≡ err(opt((Union {list n (types P) |n. n <= mxs}) <*>
list mxl (err(types P))))"
apply (unfold states_def sl_def Opt.esl_def Err.sl_def
stk_esl_def loc_sl_def Product.esl_def
Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
apply simp
done
lemma JVM_le_unfold:
"le P m n ≡
Err.le(Opt.le(Product.le(Listn.le(subtype P))(Listn.le(Err.le(subtype P)))))"
apply (unfold le_def sl_def Opt.esl_def Err.sl_def
stk_esl_def loc_sl_def Product.esl_def
Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
apply simp
done
lemma sl_def2:
"JVM_SemiType.sl P mxs mxl ≡
(states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp
lemma JVM_le_conv:
"le P m n (OK t1) (OK t2) = P \<turnstile> t1 ≤' t2"
by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def
sup_state_def sup_ty_opt_def)
lemma JVM_le_Err_conv:
"le P m n = Err.le (sup_state_opt P)"
by (unfold sup_state_opt_def sup_state_def
sup_ty_opt_def JVM_le_unfold) simp
lemma err_le_unfold [iff]:
"Err.le r (OK a) (OK b) = r a b"
by (simp add: Err.le_def lesub_def)
section {* Semilattice *}
lemma order_sup_state_opt [intro, simp]:
"wf_prog wf_mb P ==> order (sup_state_opt P)"
by (unfold sup_state_opt_def sup_state_def sup_ty_opt_def) blast
lemma semilat_JVM [intro?]:
"wf_prog wf_mb P ==> semilat (JVM_SemiType.sl P mxs mxl)"
apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)
apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl
Listn_sl err_semilat_JType_esl)
done
lemma acc_JVM [intro]:
"wf_prog wf_mb P ==> acc (JVM_SemiType.le P mxs mxl)"
by (unfold JVM_le_unfold) blast
section {* Widening with @{text "\<top>"} *}
lemma subtype_refl[iff]: "subtype P t t" by (simp add: fun_of_def)
lemma sup_ty_opt_refl [iff]: "P \<turnstile> T ≤⇩\<top> T"
apply (unfold sup_ty_opt_def)
apply (fold lesub_def)
apply (rule le_err_refl)
apply (simp add: lesub_def)
done
lemma Err_any_conv [iff]: "P \<turnstile> Err ≤⇩\<top> T = (T = Err)"
by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def])
lemma any_Err [iff]: "P \<turnstile> T ≤⇩\<top> Err"
by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def])
lemma OK_OK_conv [iff]:
"P \<turnstile> OK T ≤⇩\<top> OK T' = P \<turnstile> T ≤ T'"
by (simp add: sup_ty_opt_def fun_of_def)
lemma any_OK_conv [iff]:
"P \<turnstile> X ≤⇩\<top> OK T' = (∃T. X = OK T ∧ P \<turnstile> T ≤ T')"
apply (unfold sup_ty_opt_def)
apply (rule le_OK_conv [simplified lesub_def])
done
lemma OK_any_conv:
"P \<turnstile> OK T ≤⇩\<top> X = (X = Err ∨ (∃T'. X = OK T' ∧ P \<turnstile> T ≤ T'))"
apply (unfold sup_ty_opt_def)
apply (rule OK_le_conv [simplified lesub_def])
done
lemma sup_ty_opt_trans [intro?, trans]:
"[|P \<turnstile> a ≤⇩\<top> b; P \<turnstile> b ≤⇩\<top> c|] ==> P \<turnstile> a ≤⇩\<top> c"
by (auto intro: widen_trans
simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
split: err.splits)
section "Stack and Registers"
lemma stk_convert:
"P \<turnstile> ST [≤] ST' = Listn.le (subtype P) ST ST'"
by (simp add: Listn.le_def lesub_def)
lemma sup_loc_refl [iff]: "P \<turnstile> LT [≤⇩\<top>] LT"
by (rule list_all2_refl) simp
lemmas sup_loc_Cons1 [iff] = list_all2_Cons1 [of "sup_ty_opt P"] for P
lemma sup_loc_def:
"P \<turnstile> LT [≤⇩\<top>] LT' ≡ Listn.le (sup_ty_opt P) LT LT'"
by (simp add: Listn.le_def lesub_def)
lemma sup_loc_widens_conv [iff]:
"P \<turnstile> map OK Ts [≤⇩\<top>] map OK Ts' = P \<turnstile> Ts [≤] Ts'"
by (simp add: list_all2_map1 list_all2_map2)
lemma sup_loc_trans [intro?, trans]:
"[|P \<turnstile> a [≤⇩\<top>] b; P \<turnstile> b [≤⇩\<top>] c|] ==> P \<turnstile> a [≤⇩\<top>] c"
by (rule list_all2_trans, rule sup_ty_opt_trans)
section "State Type"
lemma sup_state_conv [iff]:
"P \<turnstile> (ST,LT) ≤⇩i (ST',LT') = (P \<turnstile> ST [≤] ST' ∧ P \<turnstile> LT [≤⇩\<top>] LT')"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def)
lemma sup_state_conv2:
"P \<turnstile> s1 ≤⇩i s2 = (P \<turnstile> fst s1 [≤] fst s2 ∧ P \<turnstile> snd s1 [≤⇩\<top>] snd s2)"
by (cases s1, cases s2) simp
lemma sup_state_refl [iff]: "P \<turnstile> s ≤⇩i s"
by (auto simp add: sup_state_conv2)
lemma sup_state_trans [intro?, trans]:
"[|P \<turnstile> a ≤⇩i b; P \<turnstile> b ≤⇩i c|] ==> P \<turnstile> a ≤⇩i c"
by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2)
lemma sup_state_opt_None_any [iff]:
"P \<turnstile> None ≤' s"
by (simp add: sup_state_opt_def Opt.le_def)
lemma sup_state_opt_any_None [iff]:
"P \<turnstile> s ≤' None = (s = None)"
by (simp add: sup_state_opt_def Opt.le_def)
lemma sup_state_opt_Some_Some [iff]:
"P \<turnstile> Some a ≤' Some b = P \<turnstile> a ≤⇩i b"
by (simp add: sup_state_opt_def Opt.le_def lesub_def)
lemma sup_state_opt_any_Some:
"P \<turnstile> (Some s) ≤' X = (∃s'. X = Some s' ∧ P \<turnstile> s ≤⇩i s')"
by (simp add: sup_state_opt_def Opt.le_def lesub_def)
lemma sup_state_opt_refl [iff]: "P \<turnstile> s ≤' s"
by (simp add: sup_state_opt_def Opt.le_def lesub_def)
lemma sup_state_opt_trans [intro?, trans]:
"[|P \<turnstile> a ≤' b; P \<turnstile> b ≤' c|] ==> P \<turnstile> a ≤' c"
apply (unfold sup_state_opt_def Opt.le_def lesub_def)
apply (simp del: split_paired_All)
apply (rule sup_state_trans, assumption+)
done
end