Theory Typing_Framework_JVM

Up to index of Isabelle/HOL/objinit

(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: Typing_Framework_JVM.html,v 1.1 2002/11/28 14:12:09 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 rT ini et) (\<lambda>pc. eff (bs!pc) G pc et)"


constdefs
  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ((init_ty list × init_ty err list) × bool) option set"
  "opt_states G maxs maxr \<equiv> opt ((\<Union>{list n (init_tys G) |n. n \<le> maxs} × list maxr (err (init_tys G))) × {True,False})"



locale 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"
  defines [simp]: "r   \<equiv> JVMType.le G mxs mxr"

  defines [simp]: "app \<equiv> \<lambda>pc. Effect.app (bs!pc) G C pc mxs 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: "set pTs \<subseteq> types G"

  fixes this and first :: "state_bool option" 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> Some (([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)), C=Object)"
  defines [simp]:
  "start \<equiv> OK first#(replicate (size bs - 1) (OK None))"


section {*  Executability of @{term check_bounded} *}
consts
  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
primrec
  "list_all'_rec P n []     = True"
  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"

constdefs
  list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  "list_all' P xs \<equiv> list_all'_rec P 0 xs"

lemma list_all'_rec:
  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
  apply (induct xs)
  apply auto
  apply (case_tac p)
  apply auto
  done

lemma list_all' [iff]:
  "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
  by (unfold list_all'_def) (simp add: list_all'_rec)

lemma list_all_ball:
  "list_all P xs = (\<forall>x \<in> set xs. P x)"
  by (induct xs) auto

lemma [code]:
  "check_bounded ins et = 
  (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> 
   list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
  by (simp add: list_all_ball check_bounded_def)
  

section {* Connecting JVM and Framework *}

lemma check_bounded_is_bounded:
  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
  apply (unfold bounded_def eff_def)
  apply clarify
  apply simp
  apply (unfold check_bounded_def)
  apply clarify
  apply (erule disjE)
   apply blast
  apply (erule allE, erule impE, assumption)
  apply (unfold xcpt_eff_def)
  apply clarsimp    
  apply (drule xcpt_names_in_et)
  apply clarify
  apply (drule bspec, assumption)
  apply simp
  done
   

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

lemmas [simp] = init_tys_def JType.esl_def

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)

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)"
  apply (unfold exec_def JVM_states_unfold)
  apply (rule pres_type_lift)
  apply clarify
  apply (case_tac s)
   apply simp
   apply (drule effNone)
   apply simp  
  apply (simp add: eff_def eff_bool_def xcpt_eff_def norm_eff_def)
  apply (case_tac "bs!p")

  -- load
  apply (clarsimp simp add: not_Err_eq)
  apply (drule listE_nth_in, assumption)
  apply fastsimp

  -- store
  apply (fastsimp simp add: not_None_eq)

  -- litpush 
  apply clarsimp
  apply (rule_tac x="Suc n" in exI)
  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)

  -- new
  apply clarsimp
  apply (erule disjE)
   apply (fastsimp intro: replace_in_setI)
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- getfield
  apply clarsimp
  apply (erule disjE)
   apply (fastsimp dest: field_fields fields_is_type)
  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 fastsimp
  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 fastsimp
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- invoke
  apply (erule disjE)
   apply (clarsimp simp add: Un_subset_iff)  
   apply (drule method_wf_mdecl, assumption+)
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   apply fastsimp
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastsimp

  -- "@{text invoke_special}"
  apply (erule disjE)
   apply (clarsimp simp add: Un_subset_iff)  
   apply (drule method_wf_mdecl, assumption+)
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   apply (fastsimp intro: replace_in_setI subcls_is_class)
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastsimp  

  -- return
  apply fastsimp

  -- pop
  apply fastsimp

  -- dup
  apply clarsimp
  apply (rule_tac x="n'+2" in exI)  
  apply fastsimp

  -- "@{text dup_x1}"
  apply clarsimp
  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
  apply fastsimp

  -- "@{text dup_x2}"
  apply clarsimp
  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
  apply fastsimp

  -- swap
  apply fastsimp

  -- iadd
  apply fastsimp

  -- goto
  apply fastsimp

  -- icmpeq
  apply fastsimp

  -- throw
  apply clarsimp
  apply (erule disjE)
   apply fastsimp
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastsimp 
  done

lemmas [iff] = not_None_eq


lemma sup_state_opt_unfold:
  "sup_state_opt G \<equiv> Opt.le (Product.le (Product.le (Listn.le (init_le G)) (Listn.le (Err.le (init_le G)))) (op =))"
  by (simp add: sup_state_opt_def sup_state_bool_def sup_state_def sup_loc_def sup_ty_opt_def)

lemma app_mono:
  "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G C pc maxs rT ini et) (length bs) (opt_states G maxs maxr)"
  by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
  
lemma lesubstep_type_simple:
  "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
  apply (unfold lesubstep_type_def)
  apply clarify
  apply (simp add: set_conv_nth)
  apply clarify
  apply (drule le_listD, assumption)
  apply (clarsimp simp add: lesub_def Product.le_def)
  apply (rule exI)
  apply (rule conjI)
   apply (rule exI)
   apply (rule conjI)
    apply (rule sym)
    apply assumption
   apply assumption
  apply assumption
  done

  
lemma eff_mono:
  "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G C p maxs rT ini et t\<rbrakk>
  \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
  apply (unfold eff_def)
  apply (rule lesubstep_type_simple)
  apply (rule le_list_appendI)
   apply (simp add: norm_eff_def)
   apply (rule le_listI)
    apply simp
   apply simp
   apply (simp add: lesub_def)
   apply (case_tac s)
    apply simp
   apply (simp del: split_paired_All split_paired_Ex)
   apply (elim exE conjE)
   apply simp
   apply (drule eff_bool_mono, assumption+)
  apply (simp add: xcpt_eff_def)
  apply (rule le_listI)
    apply simp
  apply simp
  apply (simp add: lesub_def)
  apply (case_tac s)
   apply simp
  apply simp
  apply (case_tac t)
   apply simp
  apply (clarsimp simp add: sup_state_conv)
  done

lemma order_sup_state_opt:
  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
  by (unfold sup_state_opt_unfold) (blast intro: order_init eq_order)


theorem exec_mono:
  "wf_prog wf_mb G \<Longrightarrow> bounded (exec G C maxs rT ini et bs) (size bs) \<Longrightarrow>
  mono (JVMType.le G maxs maxr) (exec G C maxs rT ini et bs) (size bs) 
       (states G maxs maxr)" 
  apply (unfold exec_def JVM_le_unfold JVM_states_unfold)   
  apply (rule mono_lift)
     apply (fold sup_state_opt_unfold opt_states_def)
     apply (erule order_sup_state_opt)
    apply (rule app_mono)
   apply assumption
  apply clarify
  apply (rule eff_mono)
  apply assumption+
  done


theorem semilat_JVM_slI:
  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
  apply (rule semilat_opt)
  apply (rule err_semilat_Product_esl)
  apply (rule err_semilat_Product_esl)
  apply (rule err_semilat_upto_esl)
  apply (rule err_semilat_init, assumption)
  apply (rule err_semilat_eslI)
  apply (rule Listn_sl)
  apply (rule err_semilat_init, assumption)
  apply (rule bool_err_semilat)
  done

lemma sl_triple_conv:
  "JVMType.sl G maxs maxr == 
  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)


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> set pTs \<subseteq> types G"
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" 
    by (unfold wf_mdecl_def wf_mhead_def) auto
  moreover
  fix t assume "t \<in> set pTs"
  ultimately
  have "is_type G t" by blast
  thus "t \<in> types G" ..
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_bounded bs et \<and> 
   check_types G mxs mxr (map OK phi) \<and>   
   wt_start G C mn pTs mxl phi \<and> 
   wt_app_eff (sup_state_opt G) app eff phi)"
  by (auto simp add: wt_method_def wt_app_eff_def wt_instr_def lesub_def
           dest: check_bounded_is_bounded boundedD)


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>
   set pTs \<subseteq> types G \<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

Executability of @{term check_bounded}

lemma list_all'_rec:

  list_all'_rec P n xs = (ALL p. p < length xs --> P (xs ! p) (p + n))

lemma list_all':

  list_all' P xs = (ALL n. n < length xs --> P (xs ! n) n)

lemma list_all_ball:

  list_all P xs = Ball (set xs) P

lemma

  check_bounded ins et =
  (list_all' (%i pc. list_all (%pc'. pc' < length ins) (succs i pc)) ins &
   list_all (%e. fst (snd (snd e)) < length ins) et)

Connecting JVM and Framework

lemma check_bounded_is_bounded:

  check_bounded ins et ==> bounded (%pc. eff (ins ! pc) G pc et) (length ins)

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)

lemmas

  init_tys G ==
  {x. EX y:fst (JType.esl G). x = Init y} Un {x. EX c n. x = UnInit c n} Un
  {x. EX c. x = PartInit c}

  JType.esl G == (types G, subtype G, JType.sup G)

lemma replace_in_setI:

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

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)

lemmas

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

lemma sup_state_opt_unfold:

  sup_state_opt G ==
  Opt.le
   (Product.le (Product.le (Listn.le (init_le G)) (Listn.le (Err.le (init_le G))))
     op =)

lemma app_mono:

  app_mono (sup_state_opt G) (%pc. app (bs ! pc) G C pc maxs rT ini et)
   (length bs) (opt_states G maxs maxr)

lemma lesubstep_type_simple:

  a <=[Product.le op = r] b ==> a <=|r| b

lemma eff_mono:

  [| p < length bs; s <=_(sup_state_opt G) t;
     app (bs ! p) G C p maxs rT ini et t |]
  ==> eff (bs ! p) G p et s <=|sup_state_opt G| eff (bs ! p) G p et t

lemma order_sup_state_opt:

  wf_prog wf_mb G ==> order (sup_state_opt G)

theorem exec_mono:

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

theorem semilat_JVM_slI:

  wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)

lemma sl_triple_conv:

  JVMType.sl G maxs maxr ==
  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)

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 |]
  ==> set pTs <= types G

lemma wt_method_def2:

  wt_method G C mn pTs rT mxs mxl bs et phi =
  (bs ~= [] &
   length phi = length bs &
   check_bounded bs et &
   check_types G mxs (1 + length pTs + mxl) (map OK phi) &
   wt_start G C mn pTs mxl phi &
   wt_app_eff (sup_state_opt G) (%pc. app (bs ! pc) G C pc mxs 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; set pTs <= types G;
           bd = ((mn, pTs), rT, maxs, maxl, b, et); P G Ca bd |]
        ==> Q G Ca bd |]
  ==> wf_prog Q G