# Theory BVNoTypeError

Up to index of Isabelle/HOL/MicroJava

theory BVNoTypeError
imports JVMDefensive BVSpecTypeSafe
begin

    (*  Title:      HOL/MicroJava/BV/BVNoTypeErrors.thy
        ID:         $Id: BVNoTypeError.thy,v 1.8 2005/06/17 14:13:08 haftmann Exp $
        Author:     Gerwin Klein
    *)

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

    theory BVNoTypeError imports 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 \<turnstile> oT \<preceq> 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 \<turnstile> oT \<preceq> Class C ∧ G \<turnstile> vT \<preceq> 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 (case_tac prim_ty)
      apply auto
      apply (case_tac prim_ty)
      apply auto
      apply (case_tac list)
      apply auto
      apply (case_tac a)
      apply auto
      apply (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 \<turnstile> T \<preceq> 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, 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 \<turnstile> aT \<preceq> fT) ∧
      method (G,C) (mn,fpTs) = Some (mD', rT', b') ∧ G \<turnstile> X \<preceq> Class C)"
      (is "?app ST LT = ?P ST LT")
    proof
      assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
    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 add: min_def)
        ultimately show ?thesis ..
      qed
      obtain apTs where
        "ST = (rev apTs) @ ys" and "length apTs = length fpTs"
      proof -
        have "ST = rev (rev xs) @ ys" by simp
        with xs show ?thesis by - (rule that, assumption, simp)
      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_def min_def)
        apply ((rule exI)+, (rule 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_def)

    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 \<turnstile> v ::\<preceq> RefT T ==> isRef v"
      apply (drule conf_RefTD)
      apply (auto simp add: isRef_def)
      done

    lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer ==> isIntg v"
      apply (unfold conf_def)
      apply auto
      apply (erule widen.elims)
      apply auto
      apply (cases v)
      apply auto
      done

    lemma list_all2_approx:
      "!!s. list_all2 (approx_val G hp) s (map OK S) =
           list_all2 (conf G hp) s S"
      apply (induct 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 \<turnstile> x \<preceq> 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 \<turnstile>JVM s \<surd>"
      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) fast

        from conforms obtain  ST LT rT maxs maxl ins et where
          hconf:  "G \<turnstile>h hp \<surd>" 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 \<turnstile> v ::\<preceq> 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 \<turnstile> D \<preceq>C C"
              by (auto dest!: non_np_objD)
          }
          ultimately show ?thesis using Getfield field class stk hconf wf
            apply clarsimp
            apply (fastsimp intro: wf_prog_ws_prog
              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 \<turnstile> v ::\<preceq> vT" and
            confr: "G,hp \<turnstile> ref ::\<preceq> 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 \<turnstile> D \<preceq>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∈set (zip apTs ps). x ∈ widen G" and
            C:   "G \<turnstile> X \<preceq> 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 \<turnstile> x ::\<preceq> 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 \<turnstile> x \<preceq> y) apTs ps"
            by (simp add: list_all2_def)

          from stk' l ps have "length ps < length stk" by simp
          moreover
          from wf x C
          have x: "G,hp \<turnstile> x ::\<preceq> 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 \<turnstile> D \<preceq>C C"
              by - (drule non_npD, assumption, clarsimp, blast)
            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
            with wf 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 \<turnstile>JVM s \<surd> ==> G \<turnstile> s -jvm-> t
      ==> G \<turnstile> (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 \<turnstile>JVM s \<surd>
      ==> G \<turnstile> (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_jvm_prog Γ Φ"
      assumes "is_class Γ C" "method (Γ,C) (m,[]) = Some (C, b)" "m ≠ init"
      defines start: "s ≡ start_state Γ C m"

      assumes "Γ \<turnstile> (Normal s) -jvmd-> t"
      shows "t ≠ TypeError"
    proof -
      have "Γ,Φ \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
      thus ?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_jvm_prog Γ Φ" and "Γ,Φ \<turnstile>JVM s \<surd>"
      shows "Γ \<turnstile> (Normal s) -jvmd-> (Normal t) = Γ \<turnstile> s -jvm-> t"
      by rule (erule defensive_imp_aggressive,rule welltyped_aggressive_imp_defensive)

    corollary welltyped_initial_commutes:
      fixes G ("Γ") and Phi ("Φ")
      assumes "wt_jvm_prog Γ Φ"
      assumes "is_class Γ C" "method (Γ,C) (m,[]) = Some (C, b)" "m ≠ init"
      defines start: "s ≡ start_state Γ C m"
      shows "Γ \<turnstile> (Normal s) -jvmd-> (Normal t) = Γ \<turnstile> s -jvm-> t"
    proof -
      have "Γ,Φ \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
      thus ?thesis by  - (rule welltyped_commutes)
    qed

    end

lemma typeof_NoneD:

      typeof empty v = Some x ==> ¬ isAddr v

lemma isRef_def2:

      isRef v = (v = Null ∨ (∃loc. v = Addr loc))

lemma app'Store:

      app' (Store idx, G, pc, maxs, rT, ST, LT) =
      (∃T ST'. ST = T # ST' ∧ idx < length LT)

lemma app'GetField:

      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)

lemma app'PutField:

      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')

lemma app'Checkcast:

      app' (Checkcast C, G, pc, maxs, rT, ST, LT) =
      (∃rT ST'. ST = RefT rT # ST' ∧ is_class G C)

lemma app'Pop:

      app' (Pop, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST')

lemma app'Dup:

      app' (Dup, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST' ∧ length ST < maxs)

lemma app'Dup_x1:

      app' (Dup_x1, G, pc, maxs, rT, ST, LT) =
      (∃T1 T2 ST'. ST = T1 # T2 # ST' ∧ length ST < maxs)

lemma app'Dup_x2:

      app' (Dup_x2, G, pc, maxs, rT, ST, LT) =
      (∃T1 T2 T3 ST'. ST = T1 # T2 # T3 # ST' ∧ length ST < maxs)

lemma app'Swap:

      app' (Swap, G, pc, maxs, rT, ST, LT) = (∃T1 T2 ST'. ST = T1 # T2 # ST')

lemma app'IAdd:

      app' (IAdd, G, pc, maxs, rT, ST, LT) =
      (∃ST'. ST = PrimT Integer # PrimT Integer # ST')

lemma app'Ifcmpeq:

      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')))

lemma app'Return:

      app' (Return, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST' ∧ G |- T <= rT)

lemma app'Throw:

      app' (Throw, G, pc, maxs, rT, ST, LT) = (∃ST' r. ST = RefT r # ST')

lemma app'Invoke:

      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)

lemma approx_loc_len:

      approx_loc G hp loc LT ==> length loc = length LT

lemma approx_stk_len:

      approx_stk G hp stk ST ==> length stk = length ST

lemma isRefI:

      G,hp |- v ::<= RefT T ==> isRef v

lemma isIntgI:

      G,hp |- v ::<= PrimT Integer ==> isIntg v

lemma list_all2_approx:

      list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S

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

theorem no_type_error:

      [| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |] ==> exec_d G (Normal s) ≠ TypeError

theorem welltyped_aggressive_imp_defensive:

      [| wt_jvm_prog G Phi; G,Phi |-JVM s [ok]; G |- s -jvm-> t |]
      ==> G |- Normal s -jvmd-> Normal t

lemma neq_TypeError_eq:

      (s ≠ TypeError) = (∃s'. s = Normal s')

theorem no_type_errors:

      [| wt_jvm_prog G Phi; G,Phi |-JVM s [ok]; G |- Normal s -jvmd-> t |]
      ==> t ≠ TypeError

corollary no_type_errors_initial:

      [| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
         m ≠ init; G |- Normal (start_state G C m) -jvmd-> t |]
      ==> t ≠ TypeError

corollary welltyped_commutes:

      [| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |]
      ==> G |- Normal s -jvmd-> Normal t = G |- s -jvm-> t

corollary welltyped_initial_commutes:

      [| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
         m ≠ init |]
      ==> G |- Normal (start_state G C m) -jvmd-> Normal t =
          G |- start_state G C m -jvm-> t