Theory Conform
section ‹Conformance Relations for Type Soundness Proofs›
theory Conform
imports
StartConfig
begin
context heap_base begin
definition conf :: "'m prog ⇒ 'heap ⇒ 'addr val ⇒ ty ⇒ bool" ("_,_ ⊢ _ :≤ _" [51,51,51,51] 50)
where "P,h ⊢ v :≤ T ≡ ∃T'. typeof⇘h⇙ v = Some T' ∧ P ⊢ T' ≤ T"
definition lconf :: "'m prog ⇒ 'heap ⇒ (vname ⇀ 'addr 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 ⇒ 'addr val list ⇒ ty list ⇒ bool" ("_,_ ⊢ _ [:≤] _" [51,51,51,51] 50)
where "P,h ⊢ vs [:≤] Ts == list_all2 (conf P h) vs Ts"
definition tconf :: "'m prog ⇒ 'heap ⇒ 'thread_id ⇒ bool" ("_,_ ⊢ _ √t" [51,51,51] 50)
where "P,h ⊢ t √t ≡ ∃C. typeof_addr h (thread_id2addr t) = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread"
end
locale heap_conf_base =
heap_base +
constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
fixes hconf :: "'heap ⇒ bool"
and P :: "'m prog"
sublocale heap_conf_base < prog P .
locale heap_conf =
heap
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
P
+
heap_conf_base
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
hconf P
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and P :: "'m prog"
+
assumes hconf_empty [iff]: "hconf empty_heap"
and typeof_addr_is_type: "⟦ typeof_addr h a = ⌊hT⌋; hconf h ⟧ ⟹ is_type P (ty_of_htype hT)"
and hconf_allocate_mono: "⋀a. ⟦ (h', a) ∈ allocate h hT; hconf h; is_htype P hT ⟧ ⟹ hconf h'"
and hconf_heap_write_mono:
"⋀T. ⟦ heap_write h a al v h'; hconf h; P,h ⊢ a@al : T; P,h ⊢ v :≤ T ⟧ ⟹ hconf h'"
locale heap_progress =
heap_conf
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
hconf P
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and P :: "'m prog"
+
assumes heap_read_total: "⟦ hconf h; P,h ⊢ a@al : T ⟧ ⟹ ∃v. heap_read h a al v ∧ P,h ⊢ v :≤ T"
and heap_write_total: "⟦ hconf h; P,h ⊢ a@al : T; P,h ⊢ v :≤ T ⟧ ⟹ ∃h'. heap_write h a al v h'"
locale heap_conf_read =
heap_conf
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
hconf P
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and P :: "'m prog"
+
assumes heap_read_conf: "⟦ heap_read h a al v; P,h ⊢ a@al : T; hconf h ⟧ ⟹ P,h ⊢ v :≤ T"
locale heap_typesafe =
heap_conf_read +
heap_progress +
constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and P :: "'m prog"
context heap_conf begin
lemmas hconf_heap_ops_mono =
hconf_allocate_mono
hconf_heap_write_mono
end
subsection‹Value conformance ‹:≤››
context heap_base begin
lemma conf_Null [simp]: "P,h ⊢ Null :≤ T = P ⊢ NT ≤ T"
unfolding conf_def by(simp (no_asm))
lemma typeof_conf[simp]: "typeof⇘h⇙ v = Some T ⟹ P,h ⊢ v :≤ T"
unfolding conf_def by (cases v) auto
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"
unfolding conf_def by (cases T) auto
lemma conf_widen: "P,h ⊢ v :≤ T ⟹ P ⊢ T ≤ T' ⟹ P,h ⊢ v :≤ T'"
unfolding conf_def by (cases v) (auto intro: widen_trans)
lemma conf_sys_xcpt:
"⟦preallocated h; C ∈ sys_xcpts⟧ ⟹ P,h ⊢ Addr (addr_of_sys_xcpt C) :≤ Class C"
by(simp add: conf_def typeof_addr_sys_xcp)
lemma conf_NT [iff]: "P,h ⊢ v :≤ NT = (v = Null)"
by (auto simp add: conf_def)
lemma is_IntgI: "P,h ⊢ v :≤ Integer ⟹ is_Intg v"
by (unfold conf_def) auto
lemma is_BoolI: "P,h ⊢ v :≤ Boolean ⟹ is_Bool v"
by (unfold conf_def) auto
lemma is_RefI: "P,h ⊢ v :≤ T ⟹ is_refT T ⟹ is_Ref v"
by(cases v)(auto elim: is_refT.cases simp add: conf_def is_Ref_def)
lemma non_npD:
"⟦ v ≠ Null; P,h ⊢ v :≤ Class C; C ≠ Object ⟧
⟹ ∃a C'. v = Addr a ∧ typeof_addr h a = ⌊Class_type C'⌋ ∧ P ⊢ C' ≼⇧* C"
by(cases v)(auto simp add: conf_def widen_Class)
lemma non_npD2:
"⟦v ≠ Null; P,h ⊢ v :≤ Class C ⟧
⟹ ∃a hT. v = Addr a ∧ typeof_addr h a = ⌊hT⌋ ∧ P ⊢ class_type_of hT ≼⇧* C"
by(cases v)(auto simp add: conf_def widen_Class)
end
context heap begin
lemma conf_hext: "⟦ h ⊴ h'; P,h ⊢ v :≤ T ⟧ ⟹ P,h' ⊢ v :≤ T"
unfolding conf_def by(cases v)(auto dest: typeof_addr_hext_mono)
lemma conf_heap_ops_mono:
assumes "P,h ⊢ v :≤ T"
shows conf_allocate_mono: "(h', a) ∈ allocate h hT ⟹ P,h' ⊢ v :≤ T"
and conf_heap_write_mono: "heap_write h a al v' h' ⟹ P,h' ⊢ v :≤ T"
using assms
by(auto intro: conf_hext dest: hext_heap_ops)
end
subsection‹Value list conformance ‹[:≤]››
context heap_base begin
lemma confs_widens [trans]: "⟦P,h ⊢ vs [:≤] Ts; P ⊢ Ts [≤] Ts'⟧ ⟹ P,h ⊢ vs [:≤] Ts'"
by (rule list_all2_trans)(rule conf_widen)
lemma confs_rev: "P,h ⊢ rev s [:≤] t = (P,h ⊢ s [:≤] rev t)"
by(rule list_all2_rev1)
lemma confs_conv_map:
"P,h ⊢ vs [:≤] Ts' = (∃Ts. map typeof⇘h⇙ vs = map Some Ts ∧ P ⊢ Ts [≤] Ts')"
apply(induct vs arbitrary: Ts')
apply simp
apply(case_tac Ts')
apply(auto simp add:conf_def)
apply(rule_tac x="T' # Ts" in exI)
apply(simp add: fun_of_def)
done
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)
end
context heap begin
lemma confs_hext: "P,h ⊢ vs [:≤] Ts ⟹ h ⊴ h' ⟹ P,h' ⊢ vs [:≤] Ts"
by (erule list_all2_mono, erule conf_hext, assumption)
end
subsection ‹Local variable conformance›
context heap_base begin
lemma lconf_upd:
"⟦ P,h ⊢ l (:≤) E; P,h ⊢ v :≤ T; E V = Some T ⟧ ⟹ P,h ⊢ l(V↦v) (:≤) E"
unfolding lconf_def by 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
context heap begin
lemma lconf_hext: "⟦ P,h ⊢ l (:≤) E; h ⊴ h' ⟧ ⟹ P,h' ⊢ l (:≤) E"
unfolding lconf_def by(fast elim: conf_hext)
end
subsection ‹Thread object conformance›
context heap_base begin
lemma tconfI: "⟦ typeof_addr h (thread_id2addr t) = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧ ⟹ P,h ⊢ t √t"
by(simp add: tconf_def)
lemma tconfD: "P,h ⊢ t √t ⟹ ∃C. typeof_addr h (thread_id2addr t) = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread"
by(auto simp add: tconf_def)
end
context heap begin
lemma tconf_hext_mono: "⟦ P,h ⊢ t √t; h ⊴ h' ⟧ ⟹ P,h' ⊢ t √t"
by(auto simp add: tconf_def dest: typeof_addr_hext_mono)
lemma tconf_heap_ops_mono:
assumes "P,h ⊢ t √t"
shows tconf_allocate_mono: "(h', a) ∈ allocate h hT ⟹ P,h' ⊢ t √t"
and tconf_heap_write_mono: "heap_write h a al v h' ⟹ P,h' ⊢ t √t"
using tconf_hext_mono[OF assms, of h']
by(blast intro: hext_heap_ops)+
lemma tconf_start_heap_start_tid:
"⟦ start_heap_ok; wf_syscls P ⟧ ⟹ P,start_heap ⊢ start_tid √t"
unfolding start_tid_def start_heap_def start_heap_ok_def start_heap_data_def initialization_list_def addr_of_sys_xcpt_def start_addrs_def sys_xcpts_list_def
apply(clarsimp split: prod.split_asm simp add: create_initial_object_simps split: if_split_asm)
apply(erule not_empty_pairE)+
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule allocate_SomeD[where hT="Class_type Thread"])
apply simp
apply(rule tconfI)
apply(erule typeof_addr_hext_mono[OF hext_allocate])+
apply simp
apply blast
done
lemma start_heap_write_typeable:
assumes "WriteMem ad al v ∈ set start_heap_obs"
shows "∃T. P,start_heap ⊢ ad@al : T ∧ P,start_heap ⊢ v :≤ T"
using assms
unfolding start_heap_obs_def start_heap_def
by clarsimp
end
subsection ‹Well-formed start state›
context heap_base begin
inductive wf_start_state :: "'m prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ bool"
for P :: "'m prog" and C :: cname and M :: mname and vs :: "'addr val list"
where
wf_start_state:
"⟦ P ⊢ C sees M:Ts→T = ⌊meth⌋ in D; start_heap_ok; P,start_heap ⊢ vs [:≤] Ts ⟧
⟹ wf_start_state P C M vs"
end
end