Theory Typing_Framework_JVM

Up to index of Isabelle/HOL/jsr

theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:
(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: Typing_Framework_JVM.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}

theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:


constdefs
  exec :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> 
           state step_type" 
  "exec G C maxs rT ini et bs == 
  err_step (size bs) (\<lambda>pc. app (bs!pc) G C pc maxs (size bs) rT ini et) (\<lambda>pc. eff (bs!pc) G pc et)"


locale (open) JVM_sl =
  fixes wf_mb and G and C and mxs and mxl 
  fixes pTs :: "ty list" and mn and bs and et and rT

  fixes mxr and A and r and app and eff and step
  defines [simp]: "mxr \<equiv> 1+length pTs+mxl"
  defines [simp]: "A   \<equiv> states G mxs mxr (length bs)"
  defines [simp]: "r   \<equiv> JVMType.le"

  defines [simp]: "app \<equiv> \<lambda>pc. Effect.app (bs!pc) G C pc mxs (size bs) rT (mn=init) et"
  defines [simp]: "eff \<equiv> \<lambda>pc. Effect.eff (bs!pc) G pc et"
  defines [simp]: "step \<equiv> exec G C mxs rT (mn=init) et bs"


locale (open) start_context = JVM_sl +
  assumes wf:  "wf_prog wf_mb G"
  assumes C:   "is_class G C"
  assumes pTs: "Init ` set pTs \<subseteq> init_tys G (size bs)"

  fixes this and first :: state_bool and start
  defines [simp]:
  "this \<equiv> OK (if mn=init \<and> C \<noteq> Object then PartInit C else Init (Class C))"
  defines [simp]: 
  "first \<equiv> (([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)), C=Object)"
  defines [simp]:
  "start \<equiv> OK {first}#(replicate (size bs - 1) (OK {}))"



section {* Connecting JVM and Framework *}

lemma special_ex_swap_lemma [iff]: 
  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
  by blast

lemmas [iff del] = not_None_eq


lemma replace_in_setI:
  "\<And>n. ls \<in> list n A \<Longrightarrow> b \<in> A \<Longrightarrow> replace a b ls \<in> list n A"
  by (induct ls) (auto simp add: replace_def)



lemma in_list_Ex [iff]:
  "(\<exists>n. xs \<in> list n A \<and> P xs n) = (set xs \<subseteq> A \<and> P xs (length xs))"
  apply (unfold list_def)
  apply auto
  done
  
lemma boundedRAI1:
  "¬is_RA T \<Longrightarrow> boundedRA (n,T)"
  apply (cases T)
  apply auto 
  apply (case_tac prim_ty)
  apply auto
  done

lemma eff_pres_type:
  "\<lbrakk>wf_prog wf_mb S; s \<subseteq> address_types S maxs maxr (length bs); 
    p < length bs; app (bs!p) S C p maxs (length bs) rT ini et s;
   (a, b) \<in> set (eff (bs ! p) S p et s)\<rbrakk>
  \<Longrightarrow> \<forall>x \<in> b. x \<in> address_types S maxs maxr (length bs)"
  apply clarify
  apply (unfold eff_def xcpt_eff_def norm_eff_def eff_bool_def)
  apply (case_tac "bs!p")

  -- load
  apply (clarsimp simp add: not_Err_eq address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (rotate_tac -1)
  apply clarsimp
  apply (drule listE_nth_in, assumption)
  apply fastsimp
 
  -- store
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply fastsimp

  -- litpush
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)  
  apply clarsimp 
  apply (rotate_tac -3) -- "for n = length ab"
  apply (fastsimp simp add: init_tys_def)

  -- new
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply (fastsimp simp add: replace_in_setI init_tys_def)
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply (fastsimp simp add: init_tys_def)

  -- getfield
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply clarsimp 
   apply (rule_tac x="Suc n'" in exI)
   apply (drule field_fields)
   apply simp
   apply (frule fields_is_type, assumption, assumption)
   apply (frule fields_no_RA, assumption, assumption)
   apply (simp (no_asm) add: init_tys_def)
   apply simp
   apply (rule boundedRAI1, assumption)
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (simp add: match_some_entry split: split_if_asm)
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- putfield
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply (clarsimp simp add: init_tys_def)
   apply fastsimp
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (simp add: match_some_entry split: split_if_asm)
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- checkcast
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply (clarsimp simp add: init_tys_def)
   apply fastsimp
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- invoke
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply (clarsimp simp add: init_tys_def) 
   apply (drule method_wf_mdecl, assumption+)
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   apply (rule in_list_Ex [THEN iffD2])
   apply (simp add: boundedRAI1)
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def) 
  apply (rule_tac x=1 in exI)
  apply fastsimp 

  -- "@{text invoke_special}"
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp add: address_types_def)
   apply (drule bspec, assumption)
   apply (drule subsetD, assumption)
   apply (clarsimp simp add: init_tys_def) 
   apply (drule method_wf_mdecl, assumption+)
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)   
   apply (rule conjI)   
    apply (rule_tac x="Suc (length ST)" in exI)
    apply (fastsimp intro: replace_in_setI subcls_is_class boundedRAI1)
   apply (fastsimp intro: replace_in_setI subcls_is_class boundedRAI1)
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def) 
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- return
  apply fastsimp

  -- pop
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply fastsimp

  -- dup
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (rule_tac x="n'+2" in exI)  
  apply simp

  -- "@{text dup_x1}"
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
  apply simp

  -- "@{text dup_x2}"
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
  apply simp

  -- swap
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply fastsimp

  -- iadd
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply fastsimp

  -- goto
  apply fastsimp

  -- icmpeq
  apply (clarsimp simp add: address_types_def)
  apply fastsimp

  -- throw
  apply (clarsimp simp add: address_types_def init_tys_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply clarsimp 
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- jsr
  apply (clarsimp simp add: address_types_def)
  apply (drule bspec, assumption)
  apply (drule subsetD, assumption)
  apply (clarsimp simp add: init_tys_def)
  apply fastsimp

  -- ret
  apply fastsimp
  done


lemmas [iff] = not_None_eq

lemma app_mono:
  "app_mono (op \<subseteq>) (\<lambda>pc. app (bs!pc) G C pc maxs (size bs) rT ini et) (length bs) (Pow (address_types G mxs mxr mpc))"
  apply (unfold app_mono_def lesub_def)
  apply clarify
  apply (drule in_address_types_finite)+  
  apply (blast intro: EffectMono.app_mono)
  done


theorem exec_pres_type:
  "wf_prog wf_mb S \<Longrightarrow> 
  pres_type (exec S C maxs rT ini et bs) (size bs) (states S maxs maxr (length bs))"
  apply (unfold exec_def states_def)
  apply (rule pres_type_lift)
  apply clarify 
  apply (blast dest: eff_pres_type)
  done

  
declare split_paired_All [simp del]

declare eff_defs [simp del]

lemma eff_mono:
  "\<lbrakk>wf_prog wf_mb G; t \<subseteq> address_types G maxs maxr (length bs); p < length bs; s \<subseteq> t; app (bs!p) G C p maxs (size bs) rT ini et t\<rbrakk>
  \<Longrightarrow> eff (bs ! p) G p et s <=|op \<subseteq>| eff (bs ! p) G p et t"
  apply (unfold lesubstep_type_def lesub_def)
  apply clarify
  apply (frule in_address_types_finite) 
  apply (frule EffectMono.app_mono, assumption, assumption)
  apply (frule subset_trans, assumption)
  apply (drule eff_pres_type, assumption, assumption, assumption, assumption)
  apply (frule finite_subset, assumption)
  apply (unfold eff_def)
  apply clarsimp
  apply (erule disjE)
  defer
   apply (unfold xcpt_eff_def)
   apply clarsimp
   apply blast
  apply clarsimp
  apply (rule exI)
  apply (rule conjI)
   apply (rule disjI1)
   apply (rule imageI) 
   apply (rule subsetD [OF succs_mono], assumption+)
  apply (unfold norm_eff_def)
  apply clarsimp
  apply (rule conjI)
   apply clarsimp
   apply (simp add: set_SOME_lists finite_imageI)
   apply (rule imageI)
   apply clarsimp
   apply (rule subsetD, assumption+)
  apply clarsimp
  apply (rule imageI)
  apply (rule subsetD, assumption+)
  done


lemma bounded_exec:
  "bounded (exec G C maxs rT ini et bs) (size bs) (states G maxs maxr (size bs))"
  apply (unfold bounded_def exec_def err_step_def app_def)
  apply (auto simp add: error_def map_snd_def split: err.splits split_if_asm)
  done
  
theorem exec_mono:
  "wf_prog wf_mb G \<Longrightarrow> 
  mono JVMType.le (exec G C maxs rT ini et bs) (size bs) (states G maxs maxr (size bs))" 
  apply (insert bounded_exec [of G C maxs rT ini et bs maxr])
  apply (unfold exec_def JVMType.le_def JVMType.states_def)   
  apply (rule mono_lift)
     apply (unfold order_def lesub_def)
     apply blast
    apply (rule app_mono)
   apply assumption
  apply clarify
  apply (rule eff_mono)
  apply assumption+
  done


lemma map_id [rule_format]:
  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
  by (induct xs, auto)


lemma is_type_pTs:
  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
  \<Longrightarrow> Init`set pTs \<subseteq> init_tys G mpc"
proof 
  assume "wf_prog wf_mb G" 
         "(C,S,fs,mdecls) \<in> set G"
         "((mn,pTs),rT,code) \<in> set mdecls"
  hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
    by (unfold wf_prog_def wf_cdecl_def) auto  
  hence "\<forall>t \<in> set pTs. is_type G t \<and> ¬is_RA t"
    by (unfold wf_mdecl_def wf_mhead_def) auto
  moreover
  fix t assume "t \<in> Init`set pTs"
  then obtain t' where t': "t = Init t'" and "t' \<in> set pTs" by auto
  ultimately 
  have "is_type G t' \<and> ¬is_RA t'" by blast
  with t' show "t \<in> init_tys G mpc" by (auto simp add: init_tys_def boundedRAI1) 
qed


lemma (in JVM_sl) wt_method_def2:
  "wt_method G C mn pTs rT mxs mxl bs et phi =
  (bs \<noteq> [] \<and> 
   length phi = length bs \<and>
   check_types G mxs mxr (size bs) (map OK phi) \<and>   
   wt_start G C mn pTs mxl phi \<and> 
   wt_app_eff (op \<subseteq>) app eff phi)"
  apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def)
  apply rule
  apply fastsimp
  apply clarsimp
  apply (rule conjI)
  defer
  apply fastsimp
  apply (insert bounded_exec [of G C mxs rT "mn=init" et bs "Suc (length pTs + mxl)"])
  apply (unfold exec_def bounded_def err_step_def)
  apply (erule allE, erule impE, assumption)+
  apply clarsimp
  apply (drule_tac x = "OK (phi!pc)" in bspec)
  apply (fastsimp simp add: check_types_def)
  apply (fastsimp simp add: map_snd_def)
  done


lemma jvm_prog_lift:  
  assumes wf: 
  "wf_prog (\<lambda>G C bd. P G C bd) G"

  assumes rule:
  "\<And>wf_mb C mn pTs C rT maxs maxl b et bd.
   wf_prog wf_mb G \<Longrightarrow>
   method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) \<Longrightarrow>
   is_class G C \<Longrightarrow>
   Init`set pTs \<subseteq> init_tys G (length b) \<Longrightarrow>
   bd = ((mn,pTs),rT,maxs,maxl,b,et) \<Longrightarrow>
   P G C bd \<Longrightarrow>
   Q G C bd"
 
  shows 
  "wf_prog (\<lambda>G C bd. Q G C bd) G"
proof -
  from wf show ?thesis
    apply (unfold wf_prog_def wf_cdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply (unfold wf_mdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (frule methd [OF wf], assumption+)
    apply (frule is_type_pTs [OF wf], assumption+)
    apply clarify
    apply (drule rule [OF wf], assumption+)
    apply (rule refl)
    apply assumption+
    done
qed


end

Connecting JVM and Framework

lemma special_ex_swap_lemma:

  (EX X. (EX n. X = A n & P n) & Q X) = (EX n. Q (A n) & P n)

lemmas

  (x ~= None) = (EX y. x = Some y)

lemma replace_in_setI:

  [| ls : list n A; b : A |] ==> replace a b ls : list n A

lemma in_list_Ex:

  (EX n. xs : list n A & P xs n) = (set xs <= A & P xs (length xs))

lemma boundedRAI1:

  ¬ is_RA T ==> boundedRA (n, T)

lemma eff_pres_type:

  [| wf_prog wf_mb S; s <= address_types S maxs maxr (length bs); p < length bs;
     app (bs ! p) S C p maxs (length bs) rT ini et s;
     (a, b) : set (eff (bs ! p) S p et s) |]
  ==> ALL x:b. x : address_types S maxs maxr (length bs)

lemmas

  (x ~= None) = (EX y. x = Some y)

lemma app_mono:

  app_mono op <= (%pc. app (bs ! pc) G C pc maxs (length bs) rT ini et)
   (length bs) (Pow (address_types G mxs mxr mpc))

theorem exec_pres_type:

  wf_prog wf_mb S
  ==> pres_type (Typing_Framework_JVM.exec S C maxs rT ini et bs) (length bs)
       (states S maxs maxr (length bs))

lemma eff_mono:

  [| wf_prog wf_mb G; t <= address_types G maxs maxr (length bs); p < length bs;
     s <= t; app (bs ! p) G C p maxs (length bs) rT ini et t |]
  ==> eff (bs ! p) G p et s <=|op <=| eff (bs ! p) G p et t

lemma bounded_exec:

  bounded (Typing_Framework_JVM.exec G C maxs rT ini et bs) (length bs)
   (states G maxs maxr (length bs))

theorem exec_mono:

  wf_prog wf_mb G
  ==> SemilatAlg.mono JVMType.le (Typing_Framework_JVM.exec G C maxs rT ini et bs)
       (length bs) (states G maxs maxr (length bs))

lemma map_id:

  (!!n. n < length xs ==> f (g (xs ! n)) = xs ! n) ==> map f (map g xs) = xs

lemma is_type_pTs:

  [| wf_prog wf_mb G; (C, S, fs, mdecls) : set G;
     ((mn, pTs), rT, code) : set mdecls |]
  ==> Init ` set pTs <= init_tys G mpc

lemma wt_method_def2:

  wt_method G C mn pTs rT mxs mxl bs et phi =
  (bs ~= [] &
   length phi = length bs &
   check_types G mxs (1 + length pTs + mxl) (length bs) (map OK phi) &
   wt_start G C mn pTs mxl phi &
   wt_app_eff op <= (%pc. app (bs ! pc) G C pc mxs (length bs) rT (mn = init) et)
    (%pc. eff (bs ! pc) G pc et) phi)

lemma

  [| wf_prog P G;
     !!wf_mb C mn pTs Ca rT maxs maxl b et bd.
        [| wf_prog wf_mb G;
           method (G, Ca) (mn, pTs) = Some (Ca, rT, maxs, maxl, b, et);
           is_class G Ca; Init ` set pTs <= init_tys G (length b);
           bd = ((mn, pTs), rT, maxs, maxl, b, et); P G Ca bd |]
        ==> Q G Ca bd |]
  ==> wf_prog Q G