Theory BVNoTypeError

(*  Title:      HOL/MicroJava/BV/BVNoTypeErrors.thy

    Author:     Gerwin Klein
    Copyright   GPL

section ‹Welltyped Programs produce no Type Errors›

theory BVNoTypeError
imports "../JVM/JVMDefensive" BVSpecTypeSafe

lemma has_methodI:
  "P  C sees M:TsT = m in D  P  C has M"
  by (unfold has_method_def) blast

text ‹
  Some simple lemmas about the type testing functions of the
  defensive JVM:
lemma typeof_NoneD [simp,dest]: "typeof v = Some x  ¬is_Addr v"
  by (cases v) auto

lemma is_Ref_def2:
  "is_Ref v = (v = Null  (a. v = Addr a))"
  by (cases v) (auto simp add: is_Ref_def)

lemma [iff]: "is_Ref Null" by (simp add: is_Ref_def2)

lemma is_RefI [intro, simp]: "P,h  v :≤ T  is_refT T  is_Ref v"
  apply (cases T)
  apply (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD)

lemma is_IntgI [intro, simp]: "P,h  v :≤ Integer  is_Intg v"
  apply (unfold conf_def)
  apply auto

lemma is_BoolI [intro, simp]: "P,h  v :≤ Boolean  is_Bool v"
  apply (unfold conf_def)
  apply auto

declare defs1 [simp del]

lemma wt_jvm_prog_states:
  " wf_jvm_prog⇘ΦP; P  C sees M: TsT = (mxs, mxl, ins, et) in C; 
     Φ C M ! pc = τ; pc < size ins 
   OK τ  states P mxs (1+size Ts+mxl)"
  apply (unfold wf_jvm_prog_phi_def)
  apply (drule (1) sees_wf_mdecl)
  apply (simp add: wf_mdecl_def wt_method_def check_types_def)
  apply (blast intro: nth_in)

text ‹
  The main theorem: welltyped programs do not produce type errors if they
  are started in a conformant state.
theorem no_type_error:
  fixes σ :: jvm_state
  assumes welltyped: "wf_jvm_prog⇘ΦP" and conforms: "P,Φ  σ "
  shows "exec_d P σ  TypeError"
proof -
  from welltyped obtain mb where wf: "wf_prog mb P" by (fast dest: wt_jvm_progD)
  obtain xcp h frs where s [simp]: "σ = (xcp, h, frs)" by (cases σ)

  from conforms have "xcp  None  frs = []  check P σ" 
    by (unfold correct_state_def check_def) auto
  moreover {
    assume "¬(xcp  None  frs = [])"
    then obtain stk reg C M pc frs' where
      xcp [simp]: "xcp = None" and
      frs [simp]: "frs = (stk,reg,C,M,pc)#frs'" 
      by (clarsimp simp add: neq_Nil_conv)

    from conforms obtain  ST LT Ts T mxs mxl ins xt where
      hconf:  "P  h " and
      meth:   "P  C sees M:TsT = (mxs, mxl, ins, xt) in C" and
      Φ:      "Φ C M ! pc = Some (ST,LT)" and
      frame:  "conf_f P h (ST,LT) ins (stk,reg,C,M,pc)" and
      frames: "conf_fs P h Φ M (size Ts) T frs'"
      by (fastforce simp add: correct_state_def dest: sees_method_fun)
    from frame obtain
      stk: "P,h  stk [:≤] ST" and
      reg: "P,h  reg [:≤] LT" and
      pc:  "pc < size ins" 
      by (simp add: conf_f_def)

    from welltyped meth Φ pc
    have "OK (Some (ST, LT))  states P mxs (1+size Ts+mxl)"
      by (rule wt_jvm_prog_states)
    hence "size ST  mxs" by (auto simp add: JVM_states_unfold)
    with stk have mxs: "size stk  mxs" 
      by (auto dest: list_all2_lengthD)

    from welltyped meth pc
    have "P,T,mxs,size ins,xt  ins!pc,pc :: Φ C M"
      by (rule wt_jvm_prog_impl_wt_instr)
    hence app0: "app (ins!pc) P mxs T pc (size ins) xt (Φ C M!pc) "
      by (simp add: wt_instr_def)
    with Φ have eff: 
      "(pc',s')set (eff (ins ! pc) P pc xt (Φ C M ! pc)). pc' < size ins"
      by (unfold app_def) simp

    from app0 Φ have app:
      "xcpt_app (ins!pc) P pc mxs xt (ST,LT)  appi (ins!pc, P, pc, mxs, T, (ST,LT))"
      by (clarsimp simp add: app_def)

    with eff stk reg 
    have "check_instr (ins!pc) P h stk reg C M pc frs'"
    proof (cases "ins!pc")
      case (Getfield F C) 
      with app stk reg Φ obtain v vT stk' where
        field: "P  C sees F:vT in C" and
        stk:   "stk = v # stk'" and
        conf:  "P,h  v :≤ Class C"
        by auto
      from conf have is_Ref: "is_Ref v" by auto
      moreover {
        assume "v  Null" 
        with conf field is_Ref wf
        have "D vs. h (the_Addr v) = Some (D,vs)  P  D * C" 
          by (auto dest!: non_npD)
      ultimately show ?thesis using Getfield field stk hconf
        apply clarsimp
        apply (rule conjI, fastforce)
        apply clarsimp
        apply (drule has_visible_field)
        apply (drule (1) has_field_mono)
        apply (drule (1) hconfD)
        apply (unfold oconf_def has_field_def)
        apply clarsimp
        apply (fastforce dest: has_fields_fun)
      case (Putfield F C)
      with app stk reg Φ obtain v ref vT stk' where
        field: "P  C sees F:vT in C" and
        stk:   "stk = v # ref # stk'" and
        confv: "P,h  v :≤ vT" and
        confr: "P,h  ref :≤ Class C"
        by fastforce
      from confr have is_Ref: "is_Ref ref" by simp
      moreover {
        assume "ref  Null" 
        with confr field is_Ref wf
        have "D vs. h (the_Addr ref) = Some (D,vs)  P  D * C"
          by (auto dest: non_npD)
      ultimately show ?thesis using Putfield field stk confv by fastforce
      case (Invoke M' n)
      with app have n: "n < size ST" by simp

      from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD)
      { assume "stk!n = Null" with n Invoke have ?thesis by simp }
      moreover { 
        assume "ST!n = NT"
        with n stk have "stk!n = Null" by (auto simp: list_all2_conv_all_nth)
        with n Invoke have ?thesis by simp
      moreover {
        assume Null: "stk!n  Null" and NT: "ST!n  NT"

        from NT app Invoke
        obtain D D' Ts T m where
          D:  "ST!n = Class D" and
          M': "P  D sees M': TsT = m in D'" and
          Ts: "P  rev (take n ST) [≤] Ts"
          by auto
        from D stk n have "P,h  stk!n :≤ Class D" 
          by (auto simp: list_all2_conv_all_nth)
        with Null obtain a C' fs where 
          [simp]: "stk!n = Addr a" "h a = Some (C',fs)" and
          "P  C' * D"
          by (fastforce dest!: conf_ClassD) 

        with M' wf obtain m' Ts' T' D'' where 
          C': "P  C' sees M': Ts'T' = m' in D''" and
          Ts': "P  Ts [≤] Ts'"
          by (auto dest!: sees_method_mono)

        from stk have "P,h  take n stk [:≤] take n ST" ..
        hence "P,h  rev (take n stk) [:≤] rev (take n ST)" ..
        also note Ts also note Ts'
        finally have "P,h  rev (take n stk) [:≤] Ts'" .

        with Invoke Null n C'
        have ?thesis by (auto simp add: is_Ref_def2 has_methodI)
      ultimately show ?thesis by blast      
      case Return with stk app Φ meth frames 
      show ?thesis by (auto simp add: has_methodI)
    qed (auto simp add: list_all2_lengthD)
    hence "check P σ" using meth pc mxs by (simp add: check_def has_methodI)
  } ultimately
  have "check P σ" by blast
  thus "exec_d P σ  TypeError" ..

text ‹
  The theorem above tells us that, in welltyped programs, the
  defensive machine reaches the same result as the aggressive
  one (after arbitrarily many steps).
theorem welltyped_aggressive_imp_defensive:
  "wf_jvm_prog⇘ΦP  P,Φ  σ   P  σ -jvm→ σ'
   P  (Normal σ) -jvmd→ (Normal σ')"
  apply (simp only: exec_all_def) 
  apply (erule rtrancl_induct)
   apply (simp add: exec_all_d_def1)
  apply simp
  apply (simp only: exec_all_def [symmetric])
  apply (frule BV_correct, assumption+) 
  apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
  apply (simp add: exec_all_d_def1)
  apply (rule rtrancl_trans, assumption)
  apply (drule exec_1_d_NormalI)
  apply auto

text ‹
  As corollary we get that the aggressive and the defensive machine
  are equivalent for welltyped programs (if started in a conformant
  state or in the canonical start state)
corollary welltyped_commutes:
  fixes σ :: jvm_state
  assumes wf: "wf_jvm_prog⇘ΦP" and conforms: "P,Φ  σ " 
  shows "P  (Normal σ) -jvmd→ (Normal σ') = P  σ -jvm→ σ'"
  apply rule
  apply (erule defensive_imp_aggressive)
  apply (erule welltyped_aggressive_imp_defensive [OF wf conforms])

corollary welltyped_initial_commutes:
  assumes wf: "wf_jvm_prog P"  
  assumes meth: "P  C sees M:[]T = b in C" 
  defines start: "σ  start_state P C M"
  shows "P  (Normal σ) -jvmd→ (Normal σ') = P  σ -jvm→ σ'"
proof -
  from wf obtain Φ where wf': "wf_jvm_prog⇘ΦP" by (auto simp: wf_jvm_prog_def)
  from this meth have "P,Φ  σ " unfolding start by (rule BV_correct_initial)
  with wf' show ?thesis by (rule welltyped_commutes)

lemma not_TypeError_eq [iff]:
  "x  TypeError = (t. x = Normal t)"
  by (cases x) auto

locale cnf =
  fixes P and Φ and σ
  assumes wf: "wf_jvm_prog⇘ΦP"  
  assumes cnf: "correct_state P Φ σ" 

theorem (in cnf) no_type_errors:
  "P  (Normal σ) -jvmd→ σ'  σ'  TypeError"
  apply (unfold exec_all_d_def1)   
  apply (erule rtrancl_induct)
   apply simp
  apply (fold exec_all_d_def1)
  apply (insert cnf wf)
  apply clarsimp
  apply (drule defensive_imp_aggressive)
  apply (frule (2) BV_correct)
  apply (drule (1) no_type_error) back
  apply (auto simp add: exec_1_d_eq)

locale start =
  fixes P and C and M and σ and T and b
  assumes wf: "wf_jvm_prog P"  
  assumes sees: "P  C sees M:[]T = b in C" 
  defines "σ  Normal (start_state P C M)"

corollary (in start) bv_no_type_error:
  shows "P  σ -jvmd→ σ'  σ'  TypeError"
proof -
  from wf obtain Φ where "wf_jvm_prog⇘ΦP" by (auto simp: wf_jvm_prog_def)
  with sees have "correct_state P Φ (start_state P C M)" 
    by - (rule BV_correct_initial)
  ultimately have "cnf P Φ (start_state P C M)" by (rule cnf.intro)
  moreover assume "P  σ -jvmd→ σ'"
  ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors)