Theory BVNoTypeError

(*  Title:      HOL/MicroJava/BV/BVNoTypeError.thy
    Author:     Gerwin Klein
*)

section ‹Welltyped Programs produce no Type Errors›

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

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

lemma isRef_def2:
  "isRef v = (v = Null ∨ (∃loc. v = Addr loc))"
  by (cases v) (auto simp add: isRef_def)

lemma app'Store[simp]:
  "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST' ∧ idx < length LT)"
  by (cases ST) auto

lemma app'GetField[simp]:
  "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) =  
  (∃oT vT ST'. ST = oT#ST' ∧ is_class G C ∧  
  field (G,C) F = Some (C,vT) ∧ G ⊢ oT ≼ Class C)"
  by (cases ST) auto

lemma app'PutField[simp]:
"app' (Putfield F C, G,  pc, maxs, rT, (ST,LT)) = 
 (∃vT vT' oT ST'. ST = vT#oT#ST' ∧ is_class G C ∧ 
  field (G,C) F = Some (C, vT') ∧ 
  G ⊢ oT ≼ Class C ∧ G ⊢ vT ≼ vT')"
  apply rule
  defer
  apply clarsimp
  apply (cases ST)
  apply simp
  apply (cases "tl ST")
  apply auto
  done

lemma app'Checkcast[simp]:
"app' (Checkcast C, G, pc, maxs, rT, (ST,LT)) =
 (∃rT ST'. ST = RefT rT#ST' ∧ is_class G C)"
apply rule
defer
apply clarsimp
apply (cases ST)
apply simp
apply (cases "hd ST")
defer 
apply simp
apply simp
done


lemma app'Pop[simp]: 
  "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST')"
  by (cases ST) auto


lemma app'Dup[simp]:
  "app' (Dup, G, pc, maxs, rT, (ST,LT)) =
  (∃T ST'. ST = T#ST' ∧ length ST < maxs)"
  by (cases ST) auto
 

lemma app'Dup_x1[simp]:
  "app' (Dup_x1, G, pc, maxs, rT, (ST,LT)) = 
  (∃T1 T2 ST'. ST = T1#T2#ST' ∧ length ST < maxs)"
  by (cases ST, simp, cases "tl ST", auto)

  
lemma app'Dup_x2[simp]:
  "app' (Dup_x2, G, pc, maxs, rT, (ST,LT)) = 
  (∃T1 T2 T3 ST'. ST = T1#T2#T3#ST' ∧ length ST < maxs)"
  by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto)


lemma app'Swap[simp]:
  "app' (Swap, G, pc, maxs, rT, (ST,LT)) = (∃T1 T2 ST'. ST = T1#T2#ST')" 
  by (cases ST, simp, cases "tl ST", auto)

  
lemma app'IAdd[simp]:
  "app' (IAdd, G, pc, maxs, rT, (ST,LT)) = 
  (∃ST'. ST = PrimT Integer#PrimT Integer#ST')"
  apply (cases ST)
  apply simp
  apply simp
  apply (case_tac a)
  apply auto
  apply (rename_tac prim_ty, case_tac prim_ty)
  apply auto
  apply (rename_tac prim_ty, case_tac prim_ty)
  apply auto
  apply (case_tac list)
  apply auto
  apply (case_tac a)
  apply auto
  apply (rename_tac prim_ty, case_tac prim_ty)
  apply auto
  done
 

lemma app'Ifcmpeq[simp]:
  "app' (Ifcmpeq b, G, pc, maxs, rT, (ST,LT)) =
  (∃T1 T2 ST'. ST = T1#T2#ST' ∧ 0 ≤ b + int pc ∧ 
  ((∃p. T1 = PrimT p ∧ T1 = T2) ∨ 
  (∃r r'. T1 = RefT r ∧ T2 = RefT r')))" 
  apply auto
  apply (cases ST)
  apply simp
  apply (cases "tl ST")
  apply (case_tac a)
  apply auto
  done
  

lemma app'Return[simp]:
  "app' (Return, G, pc, maxs, rT, (ST,LT)) = 
  (∃T ST'. ST = T#ST'∧ G ⊢ T ≼ rT)" 
  by (cases ST) auto


lemma app'Throw[simp]:
  "app' (Throw, G, pc, maxs, rT, (ST,LT)) = 
  (∃ST' r. ST = RefT r#ST')"
  apply (cases ST)
  apply simp
  apply (cases "hd ST")
  apply auto
  done

  
lemma app'Invoke[simp]:
"app' (Invoke C mn fpTs, G, pc, maxs, rT, ST, LT) = 
 (∃apTs X ST' mD' rT' b'.
  ST = (rev apTs) @ X # ST' ∧ 
  length apTs = length fpTs ∧ is_class G C ∧
  (∀(aT,fT)∈set(zip apTs fpTs). G ⊢ aT ≼ fT) ∧ 
  method (G,C) (mn,fpTs) = Some (mD', rT', b') ∧ G ⊢ X ≼ Class C)"
  (is "?app ST LT = ?P ST LT")
proof
  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_iff)
next  
  assume app: "?app ST LT"
  hence l: "length fpTs < length ST" by simp
  obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
  proof -
    have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
    moreover from l have "length (take (length fpTs) ST) = length fpTs"
      by simp
    ultimately show ?thesis ..
  qed
  obtain apTs where
    "ST = (rev apTs) @ ys" and "length apTs = length fpTs"
  proof -
    from xs(1) have "ST = rev (rev xs) @ ys" by simp
    then show thesis by (rule that) (simp add: xs(2))
  qed
  moreover
  from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
  ultimately
  have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
  with app
  show "?P ST LT"
    apply (clarsimp simp add: list_all2_iff)
    apply (intro exI conjI)
    apply auto
    done
qed

lemma approx_loc_len [simp]:
  "approx_loc G hp loc LT ⟹ length loc = length LT"
  by (simp add: approx_loc_def list_all2_iff)

lemma approx_stk_len [simp]:
  "approx_stk G hp stk ST ⟹ length stk = length ST"
  by (simp add: approx_stk_def)

lemma isRefI [intro, simp]: "G,hp ⊢ v ::≼ RefT T ⟹ isRef v"
  apply (drule conf_RefTD)
  apply (auto simp add: isRef_def)
  done

lemma isIntgI [intro, simp]: "G,hp ⊢ v ::≼ PrimT Integer ⟹ isIntg v"
  apply (unfold conf_def)
  apply auto
  apply (erule widen.cases)
  apply auto
  apply (cases v)
  apply auto
  done

lemma list_all2_approx:
  "list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S"
  apply (induct S arbitrary: s)
  apply (auto simp add: list_all2_Cons2 approx_val_def)
  done

lemma list_all2_conf_widen:
  "wf_prog mb G ⟹
  list_all2 (conf G hp) a b ⟹
  list_all2 (λx y. G ⊢ x ≼ y) b c ⟹
  list_all2 (conf G hp) a c"
  apply (rule list_all2_trans)
  defer
  apply assumption
  apply assumption
  apply (drule conf_widen, assumption+)
  done


text ‹
  The main theorem: welltyped programs do not produce type errors if they
  are started in a conformant state.
›
theorem no_type_error:
  assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi ⊢JVM s √"
  shows "exec_d G (Normal s) ≠ TypeError"
proof -
  from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD)
  
  obtain xcp hp frs where s [simp]: "s = (xcp, hp, frs)" by (cases s)

  from conforms have "xcp ≠ None ∨ frs = [] ⟹ check G s" 
    by (unfold correct_state_def check_def) auto
  moreover {
    assume "¬(xcp ≠ None ∨ frs = [])"
    then obtain stk loc C sig pc frs' where
      xcp [simp]: "xcp = None" and
      frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
      by (clarsimp simp add: neq_Nil_conv)

    from conforms obtain  ST LT rT maxs maxl ins et where
      hconf:  "G ⊢h hp √" and
      "class":  "is_class G C" and
      meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
      phi:    "Phi C sig ! pc = Some (ST,LT)" and
      frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
      frames: "correct_frames G hp Phi rT sig frs'"
      by (auto simp add: correct_state_def)

    from frame obtain
      stk: "approx_stk G hp stk ST" and
      loc: "approx_loc G hp loc LT" and
      pc:  "pc < length ins" and
      len: "length loc = length (snd sig) + maxl + 1"
      by (auto simp add: correct_frame_def)

    note approx_val_def [simp]

    from welltyped meth conforms
    have "wt_instr (ins!pc) G rT (Phi C sig) maxs (length ins) et pc"
      by simp (rule wt_jvm_prog_impl_wt_instr_cor)    
    then obtain
      app': "app (ins!pc) G maxs rT pc et (Phi C sig!pc) " and
      eff: "∀(pc', s')∈set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins"
      by (simp add: wt_instr_def phi) blast

    from eff 
    have pc': "∀pc' ∈ set (succs (ins!pc) pc). pc' < length ins"
      by (simp add: eff_def) blast

    from app' phi
    have app:
      "xcpt_app (ins!pc) G pc et ∧ app' (ins!pc, G, pc, maxs, rT, (ST,LT))"
      by (clarsimp simp add: app_def)

    with eff stk loc pc'
    have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
    proof (cases "ins!pc")
      case (Getfield F C) 
      with app stk loc phi obtain v vT stk' where
        "class": "is_class G C" and
        field: "field (G, C) F = Some (C, vT)" and
        stk:   "stk = v # stk'" and
        conf:  "G,hp ⊢ v ::≼ Class C"
        apply clarsimp
        apply (blast dest: conf_widen [OF wf])
        done
      from conf have isRef: "isRef v" ..
      moreover {
        assume "v ≠ Null" 
        with conf field isRef wf
        have "∃D vs. hp (the_Addr v) = Some (D,vs) ∧ G ⊢ D ≼C C" 
          by (auto dest!: non_np_objD)
      }
      ultimately show ?thesis using Getfield field "class" stk hconf wf
        apply clarsimp
        apply (fastforce dest!: hconfD widen_cfs_fields oconf_objD)
        done
    next
      case (Putfield F C)
      with app stk loc phi obtain v ref vT stk' where
        "class": "is_class G C" and
        field: "field (G, C) F = Some (C, vT)" and
        stk:   "stk = v # ref # stk'" and
        confv: "G,hp ⊢ v ::≼ vT" and
        confr: "G,hp ⊢ ref ::≼ Class C"
        apply clarsimp
        apply (blast dest: conf_widen [OF wf])
        done
      from confr have isRef: "isRef ref" ..
      moreover {
        assume "ref ≠ Null" 
        with confr field isRef wf
        have "∃D vs. hp (the_Addr ref) = Some (D,vs) ∧ G ⊢ D ≼C C"
          by (auto dest: non_np_objD)
      }
      ultimately show ?thesis using Putfield field "class" stk confv
        by clarsimp
    next      
      case (Invoke C mn ps)
      with app
      obtain apTs X ST' where
        ST: "ST = rev apTs @ X # ST'" and
        ps: "length apTs = length ps" and
        w:   "∀(x, y)∈set (zip apTs ps). G ⊢ x ≼ y" and
        C:   "G ⊢ X ≼ Class C" and
        mth: "method (G, C) (mn, ps) ≠ None"
        by (simp del: app'.simps) blast
        
      from ST stk
      obtain aps x stk' where
        stk': "stk = aps @ x # stk'" and
        aps: "approx_stk G hp aps (rev apTs)" and
        x: "G,hp ⊢ x ::≼ X" and        
        l: "length aps = length apTs"
        by (auto dest!: approx_stk_append)
      
      from stk' l ps 
      have [simp]: "stk!length ps = x" by (simp add: nth_append)
      from stk' l ps
      have [simp]: "take (length ps) stk = aps" by simp
      from w ps
      have widen: "list_all2 (λx y. G ⊢ x ≼ y) apTs ps"
        by (simp add: list_all2_iff) 

      from stk' l ps have "length ps < length stk" by simp
      moreover
      from wf x C 
      have x: "G,hp ⊢ x ::≼ Class C" by (rule conf_widen) 
      hence "isRef x" by simp
      moreover
      { assume "x ≠ Null"
        with x
        obtain D fs where
          hp: "hp (the_Addr x) = Some (D,fs)" and
          D:  "G ⊢ D ≼C C"
          by (auto dest: non_npD)
        hence "hp (the_Addr x) ≠ None" (is ?P1) by simp
        moreover
        from wf mth hp D
        have "method (G, cname_of hp x) (mn, ps) ≠ None" (is ?P2)
          by (auto dest: subcls_widen_methd)
        moreover
        from aps have "list_all2 (conf G hp) aps (rev apTs)"
          by (simp add: list_all2_approx approx_stk_def approx_loc_def)        
        hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
          by (simp only: list_all2_rev)
        hence "list_all2 (conf G hp) (rev aps) apTs" by simp
        from wf this widen
        have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
          by (rule list_all2_conf_widen) 
        ultimately
        have "?P1 ∧ ?P2 ∧ ?P3" by blast
      }
      moreover 
      note Invoke
      ultimately
      show ?thesis by simp
    next
      case Return with stk app phi meth frames 
      show ?thesis        
        apply clarsimp
        apply (drule conf_widen [OF wf], assumption)
        apply (clarsimp simp add: neq_Nil_conv isRef_def2)
        done
    qed auto
    hence "check G s" by (simp add: check_def meth pc)
  } ultimately
  have "check G s" by blast
  thus "exec_d G (Normal s) ≠ 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:
  "wt_jvm_prog G Phi ⟹ G,Phi ⊢JVM s √ ⟹ G ⊢ s ─jvm→ t 
  ⟹ G ⊢ (Normal s) ─jvmd→ (Normal t)"
  apply (unfold exec_all_def) 
  apply (erule rtrancl_induct)
   apply (simp add: exec_all_d_def)
  apply simp
  apply (fold exec_all_def)
  apply (frule BV_correct, assumption+)
  apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
  apply (simp add: exec_all_d_def)
  apply (rule rtrancl_trans, assumption)
  apply blast
  done


lemma neq_TypeError_eq [simp]: "s ≠ TypeError = (∃s'. s = Normal s')"
  by (cases s, auto)

theorem no_type_errors:
  "wt_jvm_prog G Phi ⟹ G,Phi ⊢JVM s √
  ⟹ G ⊢ (Normal s) ─jvmd→ t ⟹ t ≠ TypeError"
  apply (unfold exec_all_d_def)   
  apply (erule rtrancl_induct)
   apply simp
  apply (fold exec_all_d_def)
  apply (auto dest: defensive_imp_aggressive BV_correct no_type_error)
  done

corollary no_type_errors_initial:
  fixes G ("Γ") and Phi ("Φ")
  assumes wt: "wt_jvm_prog Γ Φ"  
  assumes is_class: "is_class Γ C"
    and "method": "method (Γ,C) (m,[]) = Some (C, b)"
    and m: "m ≠ init"
  defines start: "s ≡ start_state Γ C m"

  assumes s: "Γ ⊢ (Normal s) ─jvmd→ t" 
  shows "t ≠ TypeError"
proof -
  from wt is_class "method" have "Γ,Φ ⊢JVM s √"
    unfolding start by (rule BV_correct_initial)
  from wt this s show ?thesis by (rule no_type_errors)
qed

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 G ("Γ") and Phi ("Φ")
  assumes wt: "wt_jvm_prog Γ Φ" and *: "Γ,Φ ⊢JVM s √" 
  shows "Γ ⊢ (Normal s) ─jvmd→ (Normal t) = Γ ⊢ s ─jvm→ t"
  apply rule
   apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive)
    apply (rule wt)
   apply (rule *)
  apply assumption
  done

corollary welltyped_initial_commutes:
  fixes G ("Γ") and Phi ("Φ")
  assumes wt: "wt_jvm_prog Γ Φ"  
  assumes is_class: "is_class Γ C"
    and "method": "method (Γ,C) (m,[]) = Some (C, b)"
    and m: "m ≠ init"
  defines start: "s ≡ start_state Γ C m"
  shows "Γ ⊢ (Normal s) ─jvmd→ (Normal t) = Γ ⊢ s ─jvm→ t"
proof -
  from wt is_class "method" have "Γ,Φ ⊢JVM s √"
    unfolding start by (rule BV_correct_initial)
  with wt show ?thesis by (rule welltyped_commutes)
qed
 
end