Theory BVNoTypeError

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

    Author:     Gerwin Klein
    Copyright   GPL
*)

header {* \isaheader{Welltyped Programs produce no Type Errors} *}

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

lemma has_methodI:
  "P \<turnstile> C sees M:Ts->T = m in D ==> P \<turnstile> 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 \<turnstile> v :≤ T ==> is_refT T ==> is_Ref v"
(*<*)
  apply (cases T)
  apply (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD)
  done
(*>*)

lemma is_IntgI [intro, simp]: "P,h \<turnstile> v :≤ Integer ==> is_Intg v"
(*<*)
  apply (unfold conf_def)
  apply auto
  done
(*>*)

lemma is_BoolI [intro, simp]: "P,h \<turnstile> v :≤ Boolean ==> is_Bool v"
(*<*)
  apply (unfold conf_def)
  apply auto
  done
(*>*)

declare defs1 [simp del]

lemma wt_jvm_prog_states:
  "[| wf_jvm_prog⇩Φ P; P \<turnstile> C sees M: Ts->T = (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)
  done
(*>*)

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,Φ \<turnstile> σ \<surd>"
  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) fast

    from conforms obtain  ST LT Ts T mxs mxl ins xt where
      hconf:  "P \<turnstile> h \<surd>" and
      meth:   "P \<turnstile> C sees M:Ts->T = (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 \<turnstile> stk [:≤] ST" and
      reg: "P,h \<turnstile> reg [:≤⇩\<top>] 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 \<turnstile> ins!pc,pc :: Φ C M"
      by (rule wt_jvm_prog_impl_wt_instr)
    hence app⇣0: "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 app⇣0 Φ have app:
      "xcpt_app (ins!pc) P pc mxs xt (ST,LT) ∧ app⇣i (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 \<turnstile> C sees F:vT in C" and
        stk:   "stk = v # stk'" and
        conf:  "P,h \<turnstile> 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 \<turnstile> D \<preceq>⇧* 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)
        done                            
    next
      case (Putfield F C)
      with app stk reg Φ obtain v ref vT stk' where
        field: "P \<turnstile> C sees F:vT in C" and
        stk:   "stk = v # ref # stk'" and
        confv: "P,h \<turnstile> v :≤ vT" and
        confr: "P,h \<turnstile> 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 \<turnstile> D \<preceq>⇧* C"
          by (auto dest: non_npD)
      }
      ultimately show ?thesis using Putfield field stk confv by fastforce
    next      
      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 \<turnstile> D sees M': Ts->T = m in D'" and
          Ts: "P \<turnstile> rev (take n ST) [≤] Ts"
          by auto
        
        from D stk n have "P,h \<turnstile> 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 \<turnstile> C' \<preceq>⇧* D"
          by (fastforce dest!: conf_ClassD) 

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

        from stk have "P,h \<turnstile> take n stk [:≤] take n ST" ..
        hence "P,h \<turnstile> rev (take n stk) [:≤] rev (take n ST)" ..
        also note Ts also note Ts'
        finally have "P,h \<turnstile> 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      
    next
      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" ..
qed
(*>*)


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,Φ \<turnstile> σ \<surd> ==> P \<turnstile> σ -jvm-> σ'
  ==> P \<turnstile> (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
  done
(*>*)


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,Φ \<turnstile> σ \<surd>" 
  shows "P \<turnstile> (Normal σ) -jvmd-> (Normal σ') = P \<turnstile> σ -jvm-> σ'"
  apply rule
  apply (erule defensive_imp_aggressive)
  apply (erule welltyped_aggressive_imp_defensive [OF wf conforms])
  done

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


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 \<turnstile> (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)
  done

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

corollary (in start) bv_no_type_error:
  shows "P \<turnstile> σ -jvmd-> σ' ==> σ' ≠ TypeError"
proof -
  from wf obtain Φ where "wf_jvm_prog⇩Φ P" by (auto simp: wf_jvm_prog_def)
  moreover
  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 \<turnstile> σ -jvmd-> σ'"
  ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors) 
qed

 
end