Theory Conform
section ‹ Conformance Relations for Type Soundness Proofs ›
theory Conform
imports Exceptions
begin
definition conf :: "'m prog ⇒ heap ⇒ val ⇒ ty ⇒ bool" ("_,_ ⊢ _ :≤ _" [51,51,51,51] 50)
where
"P,h ⊢ v :≤ T ≡
∃T'. typeof⇘h⇙ v = Some T' ∧ P ⊢ T' ≤ T"
definition oconf :: "'m prog ⇒ heap ⇒ obj ⇒ bool" ("_,_ ⊢ _ √" [51,51,51] 50)
where
"P,h ⊢ obj √ ≡
let (C,fs) = obj in ∀F D T. P ⊢ C has F,NonStatic:T in D ⟶
(∃v. fs(F,D) = Some v ∧ P,h ⊢ v :≤ T)"
definition soconf :: "'m prog ⇒ heap ⇒ cname ⇒ sfields ⇒ bool" ("_,_,_ ⊢⇩s _ √" [51,51,51,51] 50)
where
"P,h,C ⊢⇩s sfs √ ≡
∀F T. P ⊢ C has F,Static:T in C ⟶
(∃v. sfs F = Some v ∧ P,h ⊢ v :≤ T)"
definition hconf :: "'m prog ⇒ heap ⇒ bool" ("_ ⊢ _ √" [51,51] 50)
where
"P ⊢ h √ ≡
(∀a obj. h a = Some obj ⟶ P,h ⊢ obj √) ∧ preallocated h"
definition shconf :: "'m prog ⇒ heap ⇒ sheap ⇒ bool" ("_,_ ⊢⇩s _ √" [51,51,51] 50)
where
"P,h ⊢⇩s sh √ ≡
(∀C sfs i. sh C = Some(sfs,i) ⟶ P,h,C ⊢⇩s sfs √)"
definition lconf :: "'m prog ⇒ heap ⇒ (vname ⇀ val) ⇒ (vname ⇀ ty) ⇒ bool" ("_,_ ⊢ _ '(:≤') _" [51,51,51,51] 50)
where
"P,h ⊢ l (:≤) E ≡
∀V v. l V = Some v ⟶ (∃T. E V = Some T ∧ P,h ⊢ v :≤ T)"
abbreviation
confs :: "'m prog ⇒ heap ⇒ val list ⇒ ty list ⇒ bool"
("_,_ ⊢ _ [:≤] _" [51,51,51,51] 50) where
"P,h ⊢ vs [:≤] Ts ≡ list_all2 (conf P h) vs Ts"
subsection‹ Value conformance @{text":≤"} ›
lemma conf_Null [simp]: "P,h ⊢ Null :≤ T = P ⊢ NT ≤ T"
by (simp (no_asm) add: conf_def)
lemma typeof_conf[simp]: "typeof⇘h⇙ v = Some T ⟹ P,h ⊢ v :≤ T"
by (induct v) (auto simp: conf_def)
lemma typeof_lit_conf[simp]: "typeof v = Some T ⟹ P,h ⊢ v :≤ T"
by (rule typeof_conf[OF typeof_lit_typeof])
lemma defval_conf[simp]: "P,h ⊢ default_val T :≤ T"
by (cases T) (auto simp: conf_def)
lemma conf_upd_obj: "h a = Some(C,fs) ⟹ (P,h(a↦(C,fs')) ⊢ x :≤ T) = (P,h ⊢ x :≤ T)"
by (rule val.induct) (auto simp:conf_def fun_upd_apply)
lemma conf_widen: "P,h ⊢ v :≤ T ⟹ P ⊢ T ≤ T' ⟹ P,h ⊢ v :≤ T'"
by (induct v) (auto intro: widen_trans simp: conf_def)
lemma conf_hext: "h ⊴ h' ⟹ P,h ⊢ v :≤ T ⟹ P,h' ⊢ v :≤ T"
by (induct v) (auto dest: hext_objD simp: conf_def)
lemma conf_ClassD: "P,h ⊢ v :≤ Class C ⟹
v = Null ∨ (∃a obj T. v = Addr a ∧ h a = Some obj ∧ obj_ty obj = T ∧ P ⊢ T ≤ Class C)"
by(induct v) (auto simp: conf_def)
lemma conf_NT [iff]: "P,h ⊢ v :≤ NT = (v = Null)"
by (auto simp add: conf_def)
lemma non_npD: "⟦ v ≠ Null; P,h ⊢ v :≤ Class C ⟧
⟹ ∃a C' fs. v = Addr a ∧ h a = Some(C',fs) ∧ P ⊢ C' ≼⇧* C"
by (auto dest: conf_ClassD)
subsection‹ Value list conformance @{text"[:≤]"} ›
lemma confs_widens [trans]: "⟦P,h ⊢ vs [:≤] Ts; P ⊢ Ts [≤] Ts'⟧ ⟹ P,h ⊢ vs [:≤] Ts'"
by(auto intro: list_all2_trans conf_widen)
lemma confs_rev: "P,h ⊢ rev s [:≤] t = (P,h ⊢ s [:≤] rev t)"
by (simp add: list_all2_rev1)
lemma confs_conv_map:
"⋀Ts'. P,h ⊢ vs [:≤] Ts' = (∃Ts. map typeof⇘h⇙ vs = map Some Ts ∧ P ⊢ Ts [≤] Ts')"
proof(induct vs)
case (Cons a vs)
then show ?case by(case_tac Ts') (auto simp add:conf_def)
qed simp
lemma confs_hext: "P,h ⊢ vs [:≤] Ts ⟹ h ⊴ h' ⟹ P,h' ⊢ vs [:≤] Ts"
by (erule list_all2_mono, erule conf_hext, assumption)
lemma confs_Cons2: "P,h ⊢ xs [:≤] y#ys = (∃z zs. xs = z#zs ∧ P,h ⊢ z :≤ y ∧ P,h ⊢ zs [:≤] ys)"
by (rule list_all2_Cons2)
subsection "Object conformance"
lemma oconf_hext: "P,h ⊢ obj √ ⟹ h ⊴ h' ⟹ P,h' ⊢ obj √"
by (fastforce elim:conf_hext simp: oconf_def)
lemma oconf_blank:
"P ⊢ C has_fields FDTs ⟹ P,h ⊢ blank P C √"
by(fastforce dest: has_fields_fun
simp: has_field_def oconf_def blank_def init_fields_def
map_of_filtered_SomeD)
lemma oconf_fupd [intro?]:
"⟦ P ⊢ C has F,NonStatic:T in D; P,h ⊢ v :≤ T; P,h ⊢ (C,fs) √ ⟧
⟹ P,h ⊢ (C, fs((F,D)↦v)) √"
by (auto dest: has_fields_fun simp add: oconf_def has_field_def fun_upd_apply)
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
subsection "Static object conformance"
lemma soconf_hext: "P,h,C ⊢⇩s obj √ ⟹ h ⊴ h' ⟹ P,h',C ⊢⇩s obj √"
by (fastforce elim:conf_hext simp:soconf_def)
lemma soconf_sblank:
"P ⊢ C has_fields FDTs ⟹ P,h,C ⊢⇩s sblank P C √"
proof -
let ?sfs = "sblank P C"
assume FDTs: "P ⊢ C has_fields FDTs"
then have "⋀F T. P ⊢ C has F,Static:T in C
⟹ ∃v. ?sfs F = Some v ∧ P,h ⊢ v :≤ T"
proof -
fix F T assume has: "P ⊢ C has F,Static:T in C"
with has_fields_fun[OF FDTs] have map: "map_of FDTs (F, C) = ⌊(Static, T)⌋"
by(clarsimp simp: has_field_def)
then have "map_of (map (λ((F, D), b, T). (F, default_val T))
(filter (λ((F, D), b, T). (case ((F, D), b, T) of (x, xa)
⇒ (case x of (F, D) ⇒ λ(b, T). b = Static) xa) ∧ D = C) FDTs)) F
= ⌊default_val T⌋"
by(rule map_of_remove_filtered_SomeD[where P = "default_val"
and Q = "λ((F, D), b, T). b = Static"]) simp
with FDTs show "∃v. ?sfs F = Some v ∧ P,h ⊢ v :≤ T"
by(clarsimp simp: sblank_def init_sfields_def)
qed
then show ?thesis by(simp add: soconf_def)
qed
lemma soconf_fupd [intro?]:
"⟦ P ⊢ C has F,Static:T in C; P,h ⊢ v :≤ T; P,h,C ⊢⇩s sfs √ ⟧
⟹ P,h,C ⊢⇩s sfs(F↦v) √"
by (auto dest: has_fields_fun simp add: fun_upd_apply soconf_def has_field_def)
lemmas soconf_new = soconf_hext [OF _ hext_new]
lemmas soconf_upd_obj = soconf_hext [OF _ hext_upd_obj]
subsection "Heap conformance"
lemma hconfD: "⟦ P ⊢ h √; h a = Some obj ⟧ ⟹ P,h ⊢ obj √"
by (unfold hconf_def) fast
lemma hconf_new: "⟦ P ⊢ h √; h a = None; P,h ⊢ obj √ ⟧ ⟹ P ⊢ h(a↦obj) √"
by (unfold hconf_def) (auto intro: oconf_new preallocated_new)
lemma hconf_upd_obj: "⟦ P ⊢ h√; h a = Some(C,fs); P,h ⊢ (C,fs')√ ⟧ ⟹ P ⊢ h(a↦(C,fs'))√"
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)
subsection "Class statics conformance"
lemma shconfD: "⟦ P,h ⊢⇩s sh √; sh C = Some(sfs,i) ⟧ ⟹ P,h,C ⊢⇩s sfs √"
by (unfold shconf_def) fast
lemma shconf_upd_obj: "⟦ P,h ⊢⇩s sh √; P,h,C ⊢⇩s sfs' √ ⟧
⟹ P,h ⊢⇩s sh(C↦(sfs',i'))√"
by (unfold shconf_def) (auto intro: soconf_upd_obj preallocated_upd_obj)
lemma shconf_hnew: "⟦ P,h ⊢⇩s sh √; h a = None ⟧ ⟹ P,h(a↦obj) ⊢⇩s sh √"
by (unfold shconf_def) (auto intro: soconf_new preallocated_new)
lemma shconf_hupd_obj: "⟦ P,h ⊢⇩s sh √; h a = Some(C,fs) ⟧ ⟹ P,h(a↦(C,fs')) ⊢⇩s sh √"
by (unfold shconf_def) (auto intro: soconf_upd_obj preallocated_upd_obj)
subsection "Local variable conformance"
lemma lconf_hext: "⟦ P,h ⊢ l (:≤) E; h ⊴ h' ⟧ ⟹ P,h' ⊢ l (:≤) E"
by (unfold lconf_def) (fast elim: conf_hext)
lemma lconf_upd:
"⟦ P,h ⊢ l (:≤) E; P,h ⊢ v :≤ T; E V = Some T ⟧ ⟹ P,h ⊢ l(V↦v) (:≤) E"
by (unfold lconf_def) auto
lemma lconf_empty[iff]: "P,h ⊢ Map.empty (:≤) E"
by(simp add:lconf_def)
lemma lconf_upd2: "⟦P,h ⊢ l (:≤) E; P,h ⊢ v :≤ T⟧ ⟹ P,h ⊢ l(V↦v) (:≤) E(V↦T)"
by(simp add:lconf_def)
end