# Theory Conform

```(*  Title:      JinjaThreads/Common/Conform.thy
Author:     David von Oheimb, Tobias Nipkow, Andreas Lochbihler

Based on the Jinja theory Common/Conform.thy by David von Oheimb and Tobias Nipkow
*)

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)

end

locale heap_conf_base =
heap_base +
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
fixes hconf :: "'heap ⇒ bool"
and P :: "'m prog"

sublocale heap_conf_base < prog P .

locale heap_conf =
heap
spurious_wakeups
P
+
heap_conf_base
spurious_wakeups
hconf P
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
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
spurious_wakeups
hconf P
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
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'"

heap_conf
spurious_wakeups
hconf P
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
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_progress +
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
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"

lemma conf_NT [iff]: "P,h ⊢ v :≤ NT = (v = Null)"

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(rule_tac x="T' # Ts" in exI)
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"

lemma lconf_upd2: "⟦P,h ⊢ l (:≤) E; P,h ⊢ v :≤ T⟧ ⟹ P,h ⊢ l(V↦v) (:≤) E(V↦T)"

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

context heap_base begin

end

context heap begin

lemma tconf_hext_mono: "⟦ P,h ⊢ t √t; h ⊴ h' ⟧ ⟹ P,h' ⊢ t √t"

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"
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 simp
apply(rule tconfI)
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
```