# Theory Conform

```(*  Title:      JinjaDCI/Common/Conform.thy

Author:     David von Oheimb, Tobias Nipkow, Susannah Mansky
Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

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 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"

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)"

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)"

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"