Theory Conform

(*  Title:      HOL/Bali/Conform.thy
    Author:     David von Oheimb
*)

subsection ‹Conformance notions for the type soundness proof for Java›

theory Conform imports State begin

text ‹
design issues:
\begin{itemize}
\item lconf allows for (arbitrary) inaccessible values
\item ''conforms'' does not directly imply that the dynamic types of all 
      objects on the heap are indeed existing classes. Yet this can be 
      inferred for all referenced objs.
\end{itemize}
›

type_synonym env' = "prog × (lname, ty) table" (* same as env of WellType.thy *)


subsubsection "extension of global store"


definition gext :: "st ⇒ st ⇒ bool" ("_≤|_"       [71,71]   70) where
   "s≤|s' ≡ ∀r. ∀obj∈globs s r: ∃obj'∈globs s' r: tag obj'= tag obj"

text ‹For the the proof of type soundness we will need the 
property that during execution, objects are not lost and moreover retain the 
values of their tags. So the object store grows conservatively. Note that if 
we considered garbage collection, we would have to restrict this property to 
accessible objects.
›

lemma gext_objD: 
"⟦s≤|s'; globs s r = Some obj⟧ 
⟹ ∃obj'. globs s' r = Some obj' ∧ tag obj' = tag obj"
apply (simp only: gext_def)
by force

lemma rev_gext_objD: 
"⟦globs s r = Some obj; s≤|s'⟧ 
 ⟹ ∃obj'. globs s' r = Some obj' ∧ tag obj' = tag obj"
by (auto elim: gext_objD)

lemma init_class_obj_inited: 
   "init_class_obj G C s1≤|s2 ⟹ inited C (globs s2)"
apply (unfold inited_def init_obj_def)
apply (auto dest!: gext_objD)
done

lemma gext_refl [intro!, simp]: "s≤|s"
apply (unfold gext_def)
apply (fast del: fst_splitE)
done

lemma gext_gupd [simp, elim!]: "⋀s. globs s r = None ⟹ s≤|gupd(r↦x)s"
by (auto simp: gext_def)

lemma gext_new [simp, elim!]: "⋀s. globs s r = None ⟹ s≤|init_obj G oi r s"
apply (simp only: init_obj_def)
apply (erule_tac gext_gupd)
done

lemma gext_trans [elim]: "⋀X. ⟦s≤|s'; s'≤|s''⟧ ⟹ s≤|s''" 
by (force simp: gext_def)

lemma gext_upd_gobj [intro!]: "s≤|upd_gobj r n v s"
apply (simp only: gext_def)
apply auto
apply (case_tac "ra = r")
apply auto
apply (case_tac "globs s r = None")
apply auto
done

lemma gext_cong1 [simp]: "set_locals l s1≤|s2 = s1≤|s2"
by (auto simp: gext_def)

lemma gext_cong2 [simp]: "s1≤|set_locals l s2 = s1≤|s2"
by (auto simp: gext_def)


lemma gext_lupd1 [simp]: "lupd(vn↦v)s1≤|s2 = s1≤|s2"
by (auto simp: gext_def)

lemma gext_lupd2 [simp]: "s1≤|lupd(vn↦v)s2 = s1≤|s2"
by (auto simp: gext_def)


lemma inited_gext: "⟦inited C (globs s); s≤|s'⟧ ⟹ inited C (globs s')"
apply (unfold inited_def)
apply (auto dest: gext_objD)
done


subsubsection "value conformance"

definition conf :: "prog ⇒ st ⇒ val ⇒ ty ⇒ bool" ("_,_⊢_∷≼_"   [71,71,71,71] 70)
  where "G,s⊢v∷≼T = (∃T'∈typeof (λa. map_option obj_ty (heap s a)) v:G⊢T'≼T)"

lemma conf_cong [simp]: "G,set_locals l s⊢v∷≼T = G,s⊢v∷≼T"
by (auto simp: conf_def)

lemma conf_lupd [simp]: "G,lupd(vn↦va)s⊢v∷≼T = G,s⊢v∷≼T"
by (auto simp: conf_def)

lemma conf_PrimT [simp]: "∀dt. typeof dt v = Some (PrimT t) ⟹ G,s⊢v∷≼PrimT t"
apply (simp add: conf_def)
done

lemma conf_Boolean: "G,s⊢v∷≼PrimT Boolean ⟹ ∃ b. v=Bool b"
by (cases v)
   (auto simp: conf_def obj_ty_def 
         dest: widen_Boolean2 
        split: obj_tag.splits)


lemma conf_litval [rule_format (no_asm)]: 
  "typeof (λa. None) v = Some T ⟶ G,s⊢v∷≼T"
apply (unfold conf_def)
apply (rule val.induct)
apply auto
done

lemma conf_Null [simp]: "G,s⊢Null∷≼T = G⊢NT≼T"
by (simp add: conf_def)

lemma conf_Addr: 
  "G,s⊢Addr a∷≼T = (∃obj. heap s a = Some obj ∧ G⊢obj_ty obj≼T)"
by (auto simp: conf_def)

lemma conf_AddrI:"⟦heap s a = Some obj; G⊢obj_ty obj≼T⟧ ⟹ G,s⊢Addr a∷≼T"
apply (rule conf_Addr [THEN iffD2])
by fast

lemma defval_conf [rule_format (no_asm), elim]: 
  "is_type G T ⟶ G,s⊢default_val T∷≼T"
apply (unfold conf_def)
apply (induct "T")
apply (auto intro: prim_ty.induct)
done

lemma conf_widen [rule_format (no_asm), elim]: 
  "G⊢T≼T' ⟹ G,s⊢x∷≼T ⟶ ws_prog G ⟶ G,s⊢x∷≼T'"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto elim: ws_widen_trans)
done

lemma conf_gext [rule_format (no_asm), elim]: 
  "G,s⊢v∷≼T ⟶ s≤|s' ⟶ G,s'⊢v∷≼T"
apply (unfold gext_def conf_def)
apply (rule val.induct)
apply force+
done


lemma conf_list_widen [rule_format (no_asm)]: 
"ws_prog G ⟹  
  ∀Ts Ts'. list_all2 (conf G s) vs Ts 
           ⟶   G⊢Ts[≼] Ts' ⟶ list_all2 (conf G s) vs Ts'"
apply (unfold widens_def)
apply (rule list_all2_trans)
apply auto
done

lemma conf_RefTD [rule_format (no_asm)]: 
 "G,s⊢a'∷≼RefT T 
  ⟶ a' = Null ∨ (∃a obj T'. a' = Addr a ∧ heap s a = Some obj ∧  
                    obj_ty obj = T' ∧ G⊢T'≼RefT T)"
apply (unfold conf_def)
apply (induct_tac "a'")
apply (auto dest: widen_PrimT)
done


subsubsection "value list conformance"

definition
  lconf :: "prog ⇒ st ⇒ ('a, val) table ⇒ ('a, ty) table ⇒ bool" ("_,_⊢_[∷≼]_" [71,71,71,71] 70)
  where "G,s⊢vs[∷≼]Ts = (∀n. ∀T∈Ts n: ∃v∈vs n: G,s⊢v∷≼T)"

lemma lconfD: "⟦G,s⊢vs[∷≼]Ts; Ts n = Some T⟧ ⟹ G,s⊢(the (vs n))∷≼T"
by (force simp: lconf_def)


lemma lconf_cong [simp]: "⋀s. G,set_locals x s⊢l[∷≼]L = G,s⊢l[∷≼]L"
by (auto simp: lconf_def)

lemma lconf_lupd [simp]: "G,lupd(vn↦v)s⊢l[∷≼]L = G,s⊢l[∷≼]L"
by (auto simp: lconf_def)

(* unused *)
lemma lconf_new: "⟦L vn = None; G,s⊢l[∷≼]L⟧ ⟹ G,s⊢l(vn↦v)[∷≼]L"
by (auto simp: lconf_def)

lemma lconf_upd: "⟦G,s⊢l[∷≼]L; G,s⊢v∷≼T; L vn = Some T⟧ ⟹  
  G,s⊢l(vn↦v)[∷≼]L"
by (auto simp: lconf_def)

lemma lconf_ext: "⟦G,s⊢l[∷≼]L; G,s⊢v∷≼T⟧ ⟹ G,s⊢l(vn↦v)[∷≼]L(vn↦T)"
by (auto simp: lconf_def)

lemma lconf_map_sum [simp]: 
 "G,s⊢l1 (+) l2[∷≼]L1 (+) L2 = (G,s⊢l1[∷≼]L1 ∧ G,s⊢l2[∷≼]L2)"
apply (unfold lconf_def)
apply safe
apply (case_tac [3] "n")
apply (force split: sum.split)+
done

lemma lconf_ext_list [rule_format (no_asm)]: "
 ⋀X. ⟦G,s⊢l[∷≼]L⟧ ⟹ 
      ∀vs Ts. distinct vns ⟶ length Ts = length vns 
      ⟶ list_all2 (conf G s) vs Ts ⟶ G,s⊢l(vns[↦]vs)[∷≼]L(vns[↦]Ts)"
apply (unfold lconf_def)
apply (induct_tac "vns")
apply  clarsimp
apply clarify
apply (frule list_all2_lengthD)
apply (clarsimp)
done


lemma lconf_deallocL: "⟦G,s⊢l[∷≼]L(vn↦T); L vn = None⟧ ⟹ G,s⊢l[∷≼]L"
apply (simp only: lconf_def)
apply safe
apply (drule spec)
apply (drule ospec)
apply auto
done 


lemma lconf_gext [elim]: "⟦G,s⊢l[∷≼]L; s≤|s'⟧ ⟹ G,s'⊢l[∷≼]L"
apply (simp only: lconf_def)
apply fast
done

lemma lconf_empty [simp, intro!]: "G,s⊢vs[∷≼]Map.empty"
apply (unfold lconf_def)
apply force
done

lemma lconf_init_vals [intro!]: 
        " ∀n. ∀T∈fs n:is_type G T ⟹ G,s⊢init_vals fs[∷≼]fs"
apply (unfold lconf_def)
apply force
done

subsubsection "weak value list conformance"

text ‹Only if the value is defined it has to conform to its type. 
        This is the contribution of the definite assignment analysis to 
        the notion of conformance. The definite assignment analysis ensures
        that the program only attempts to access local variables that 
        actually have a defined value in the state. 
        So conformance must only ensure that the
        defined values are of the right type, and not also that the value
        is defined. 
›

  
definition
  wlconf :: "prog ⇒ st ⇒ ('a, val) table ⇒ ('a, ty) table ⇒ bool" ("_,_⊢_[∼∷≼]_" [71,71,71,71] 70)
  where "G,s⊢vs[∼∷≼]Ts = (∀n. ∀T∈Ts n: ∀ v∈vs n: G,s⊢v∷≼T)"

lemma wlconfD: "⟦G,s⊢vs[∼∷≼]Ts; Ts n = Some T; vs n = Some v⟧ ⟹ G,s⊢v∷≼T"
by (auto simp: wlconf_def)


lemma wlconf_cong [simp]: "⋀s. G,set_locals x s⊢l[∼∷≼]L = G,s⊢l[∼∷≼]L"
by (auto simp: wlconf_def)

lemma wlconf_lupd [simp]: "G,lupd(vn↦v)s⊢l[∼∷≼]L = G,s⊢l[∼∷≼]L"
by (auto simp: wlconf_def)


lemma wlconf_upd: "⟦G,s⊢l[∼∷≼]L; G,s⊢v∷≼T; L vn = Some T⟧ ⟹  
  G,s⊢l(vn↦v)[∼∷≼]L"
by (auto simp: wlconf_def)

lemma wlconf_ext: "⟦G,s⊢l[∼∷≼]L; G,s⊢v∷≼T⟧ ⟹ G,s⊢l(vn↦v)[∼∷≼]L(vn↦T)"
by (auto simp: wlconf_def)

lemma wlconf_map_sum [simp]: 
 "G,s⊢l1 (+) l2[∼∷≼]L1 (+) L2 = (G,s⊢l1[∼∷≼]L1 ∧ G,s⊢l2[∼∷≼]L2)"
apply (unfold wlconf_def)
apply safe
apply (case_tac [3] "n")
apply (force split: sum.split)+
done

lemma wlconf_ext_list [rule_format (no_asm)]: "
 ⋀X. ⟦G,s⊢l[∼∷≼]L⟧ ⟹ 
      ∀vs Ts. distinct vns ⟶ length Ts = length vns 
      ⟶ list_all2 (conf G s) vs Ts ⟶ G,s⊢l(vns[↦]vs)[∼∷≼]L(vns[↦]Ts)"
apply (unfold wlconf_def)
apply (induct_tac "vns")
apply  clarsimp
apply clarify
apply (frule list_all2_lengthD)
apply clarsimp
done


lemma wlconf_deallocL: "⟦G,s⊢l[∼∷≼]L(vn↦T); L vn = None⟧ ⟹ G,s⊢l[∼∷≼]L"
apply (simp only: wlconf_def)
apply safe
apply (drule spec)
apply (drule ospec)
defer
apply (drule ospec )
apply auto
done 


lemma wlconf_gext [elim]: "⟦G,s⊢l[∼∷≼]L; s≤|s'⟧ ⟹ G,s'⊢l[∼∷≼]L"
apply (simp only: wlconf_def)
apply fast
done

lemma wlconf_empty [simp, intro!]: "G,s⊢vs[∼∷≼]Map.empty"
apply (unfold wlconf_def)
apply force
done

lemma wlconf_empty_vals: "G,s⊢Map.empty[∼∷≼]ts"
  by (simp add: wlconf_def)

lemma wlconf_init_vals [intro!]: 
        " ∀n. ∀T∈fs n:is_type G T ⟹ G,s⊢init_vals fs[∼∷≼]fs"
apply (unfold wlconf_def)
apply force
done

lemma lconf_wlconf:
 "G,s⊢l[∷≼]L ⟹ G,s⊢l[∼∷≼]L"
by (force simp add: lconf_def wlconf_def)

subsubsection "object conformance"

definition
  oconf :: "prog ⇒ st ⇒ obj ⇒ oref ⇒ bool" ("_,_⊢_∷≼√_"  [71,71,71,71] 70) where
  "(G,s⊢obj∷≼√r) = (G,s⊢values obj[∷≼]var_tys G (tag obj) r ∧ 
                           (case r of 
                              Heap a ⇒ is_type G (obj_ty obj) 
                            | Stat C ⇒ True))"


lemma oconf_is_type: "G,s⊢obj∷≼√Heap a ⟹ is_type G (obj_ty obj)"
by (auto simp: oconf_def Let_def)

lemma oconf_lconf: "G,s⊢obj∷≼√r ⟹ G,s⊢values obj[∷≼]var_tys G (tag obj) r"
by (simp add: oconf_def) 

lemma oconf_cong [simp]: "G,set_locals l s⊢obj∷≼√r = G,s⊢obj∷≼√r"
by (auto simp: oconf_def Let_def)

lemma oconf_init_obj_lemma: 
"⟦⋀C c. class G C = Some c ⟹ unique (DeclConcepts.fields G C);  
  ⋀C c f fld. ⟦class G C = Some c; 
                table_of (DeclConcepts.fields G C) f = Some fld ⟧ 
            ⟹ is_type G (type fld);  
  (case r of 
     Heap a ⇒ is_type G (obj_ty obj) 
  | Stat C ⇒ is_class G C)
⟧ ⟹  G,s⊢obj ⦇values:=init_vals (var_tys G (tag obj) r)⦈∷≼√r"
apply (auto simp add: oconf_def)
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
defer
apply (subst obj_ty_cong)
apply (auto dest!: fields_table_SomeD split: sum.split_asm obj_tag.split_asm)
done

subsubsection "state conformance"

definition
  conforms :: "state ⇒ env' ⇒ bool"  ("_∷≼_" [71,71] 70)  where
   "xs∷≼E =
      (let (G, L) = E; s = snd xs; l = locals s in
        (∀r. ∀obj∈globs s r: G,s⊢obj ∷≼√r) ∧ G,s⊢l [∼∷≼]L ∧
        (∀a. fst xs=Some(Xcpt (Loc a)) ⟶ G,s⊢Addr a∷≼ Class (SXcpt Throwable)) ∧
             (fst xs=Some(Jump Ret) ⟶ l Result ≠ None))"

subsubsection "conforms"

lemma conforms_globsD: 
"⟦(x, s)∷≼(G, L); globs s r = Some obj⟧ ⟹ G,s⊢obj∷≼√r"
by (auto simp: conforms_def Let_def)

lemma conforms_localD: "(x, s)∷≼(G, L) ⟹ G,s⊢locals s[∼∷≼]L"
by (auto simp: conforms_def Let_def)

lemma conforms_XcptLocD: "⟦(x, s)∷≼(G, L); x = Some (Xcpt (Loc a))⟧ ⟹  
          G,s⊢Addr a∷≼ Class (SXcpt Throwable)"
by (auto simp: conforms_def Let_def)

lemma conforms_RetD: "⟦(x, s)∷≼(G, L); x = Some (Jump Ret)⟧ ⟹  
          (locals s) Result ≠ None"
by (auto simp: conforms_def Let_def)

lemma conforms_RefTD: 
 "⟦G,s⊢a'∷≼RefT t; a' ≠ Null; (x,s) ∷≼(G, L)⟧ ⟹  
   ∃a obj. a' = Addr a ∧ globs s (Inl a) = Some obj ∧  
   G⊢obj_ty obj≼RefT t ∧ is_type G (obj_ty obj)"
apply (drule_tac conf_RefTD)
apply clarsimp
apply (rule conforms_globsD [THEN oconf_is_type])
apply auto
done

lemma conforms_Jump [iff]:
  "j=Ret ⟶ locals s Result ≠ None 
   ⟹ ((Some (Jump j), s)∷≼(G, L)) = (Norm s∷≼(G, L))"
by (auto simp: conforms_def Let_def)

lemma conforms_StdXcpt [iff]: 
  "((Some (Xcpt (Std xn)), s)∷≼(G, L)) = (Norm s∷≼(G, L))"
by (auto simp: conforms_def)

lemma conforms_Err [iff]:
   "((Some (Error e), s)∷≼(G, L)) = (Norm s∷≼(G, L))"
  by (auto simp: conforms_def)  

lemma conforms_raise_if [iff]: 
  "((raise_if c xn x, s)∷≼(G, L)) = ((x, s)∷≼(G, L))"
by (auto simp: abrupt_if_def)

lemma conforms_error_if [iff]: 
  "((error_if c err x, s)∷≼(G, L)) = ((x, s)∷≼(G, L))"
by (auto simp: abrupt_if_def)

lemma conforms_NormI: "(x, s)∷≼(G, L) ⟹ Norm s∷≼(G, L)"
by (auto simp: conforms_def Let_def)

lemma conforms_absorb [rule_format]:
  "(a, b)∷≼(G, L) ⟶ (absorb j a, b)∷≼(G, L)"
apply (rule impI)
apply (case_tac a)
apply (case_tac "absorb j a")
apply auto
apply (rename_tac a')
apply (case_tac "absorb j (Some a')",auto)
apply (erule conforms_NormI)
done

lemma conformsI: "⟦∀r. ∀obj∈globs s r: G,s⊢obj∷≼√r;  
     G,s⊢locals s[∼∷≼]L;  
     ∀a. x = Some (Xcpt (Loc a)) ⟶ G,s⊢Addr a∷≼ Class (SXcpt Throwable);
     x = Some (Jump Ret)⟶ locals s Result ≠ None⟧ ⟹ 
  (x, s)∷≼(G, L)"
by (auto simp: conforms_def Let_def)

lemma conforms_xconf: "⟦(x, s)∷≼(G,L);   
 ∀a. x' = Some (Xcpt (Loc a)) ⟶ G,s⊢Addr a∷≼ Class (SXcpt Throwable);
     x' = Some (Jump Ret) ⟶ locals s Result ≠ None⟧ ⟹ 
 (x',s)∷≼(G,L)"
by (fast intro: conformsI elim: conforms_globsD conforms_localD)

lemma conforms_lupd: 
 "⟦(x, s)∷≼(G, L); L vn = Some T; G,s⊢v∷≼T⟧ ⟹ (x, lupd(vn↦v)s)∷≼(G, L)"
by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
                                           conforms_XcptLocD conforms_RetD 
          simp: oconf_def)


lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]

lemma conforms_allocL: 
  "⟦(x, s)∷≼(G, L); G,s⊢v∷≼T⟧ ⟹ (x, lupd(vn↦v)s)∷≼(G, L(vn↦T))"
by (force intro: conformsI dest: conforms_globsD conforms_RetD 
          elim: conforms_XcptLocD  conforms_allocL_aux 
          simp: oconf_def)

lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]

lemma conforms_deallocL: "⋀s.⟦s∷≼(G, L(vn↦T)); L vn = None⟧ ⟹ s∷≼(G,L)"
by (fast intro: conformsI dest: conforms_globsD conforms_RetD
         elim: conforms_XcptLocD conforms_deallocL_aux)

lemma conforms_gext: "⟦(x, s)∷≼(G,L); s≤|s';  
  ∀r. ∀obj∈globs s' r: G,s'⊢obj∷≼√r;  
   locals s'=locals s⟧ ⟹ (x,s')∷≼(G,L)"
apply (rule conformsI)
apply     assumption
apply    (drule conforms_localD) apply force
apply   (intro strip)
apply  (drule (1) conforms_XcptLocD) apply force 
apply (intro strip)
apply (drule (1) conforms_RetD) apply force
done



lemma conforms_xgext: 
  "⟦(x ,s)∷≼(G,L); (x', s')∷≼(G, L); s'≤|s;dom (locals s') ⊆ dom (locals s)⟧ 
   ⟹ (x',s)∷≼(G,L)"
apply (erule_tac conforms_xconf)
apply  (fast dest: conforms_XcptLocD)
apply (intro strip)
apply (drule (1) conforms_RetD) 
apply (auto dest: domI)
done

lemma conforms_gupd: "⋀obj. ⟦(x, s)∷≼(G, L); G,s⊢obj∷≼√r; s≤|gupd(r↦obj)s⟧ 
⟹  (x, gupd(r↦obj)s)∷≼(G, L)"
apply (rule conforms_gext)
apply    auto
apply (force dest: conforms_globsD simp add: oconf_def)+
done

lemma conforms_upd_gobj: "⟦(x,s)∷≼(G, L); globs s r = Some obj; 
  var_tys G (tag obj) r n = Some T; G,s⊢v∷≼T⟧ ⟹ (x,upd_gobj r n v s)∷≼(G,L)"
apply (rule conforms_gext)
apply auto
apply (drule (1) conforms_globsD)
apply (simp add: oconf_def)
apply safe
apply (rule lconf_upd)
apply auto
apply (simp only: obj_ty_cong)
apply (force dest: conforms_globsD intro!: lconf_upd 
       simp add: oconf_def cong del: old.sum.case_cong_weak)
done

lemma conforms_set_locals: 
  "⟦(x,s)∷≼(G, L'); G,s⊢l[∼∷≼]L; x=Some (Jump Ret) ⟶ l Result ≠ None⟧ 
   ⟹ (x,set_locals l s)∷≼(G,L)"
apply (rule conformsI)
apply     (intro strip)
apply     simp
apply     (drule (2) conforms_globsD)
apply    simp
apply   (intro strip)
apply   (drule (1) conforms_XcptLocD)
apply   simp
apply (intro strip)
apply (drule (1) conforms_RetD)
apply simp
done

lemma conforms_locals: 
  "⟦(a,b)∷≼(G, L); L x = Some T;locals b x ≠None⟧
   ⟹ G,b⊢the (locals b x)∷≼T"
apply (force simp: conforms_def Let_def wlconf_def)
done

lemma conforms_return: 
"⋀s'. ⟦(x,s)∷≼(G, L); (x',s')∷≼(G, L'); s≤|s';x'≠Some (Jump Ret)⟧ ⟹  
  (x',set_locals (locals s) s')∷≼(G, L)"
apply (rule conforms_xconf)
prefer 2 apply (force dest: conforms_XcptLocD)
apply (erule conforms_gext)
apply (force dest: conforms_globsD)+
done

end