Theory JinjaDCI.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⇘hv = 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⇘hv = 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⇘hvs = 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(Fv) "
(*<*)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(aobj) "
(*<*)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(aobj) 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(Vv) (:≤) 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(Vv) (:≤) E(VT)"
(*<*)by(simp add:lconf_def)(*>*)


end