# Theory JVM

Up to index of Isabelle/HOL/MicroJava

theory JVM
imports Kildall Typing_Framework_JVM
begin

    (*  Title:      HOL/MicroJava/BV/JVM.thy
        ID:         $Id: JVM.thy,v 1.26 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow, Gerwin Klein
        Copyright   2000 TUM
    *)

    header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}

    theory JVM imports Kildall Typing_Framework_JVM begin

    constdefs
      kiljvm :: "jvm_prog => nat => nat => ty => exception_table =>
                 instr list => state list => state list"
      "kiljvm G maxs maxr rT et bs ==
      kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"

      wt_kil :: "jvm_prog => cname => ty list => ty => nat => nat =>
                 exception_table => instr list => bool"
      "wt_kil G C pTs rT mxs mxl et ins ==
       check_bounded ins et ∧ 0 < size ins ∧
       (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
            start  = OK first#(replicate (size ins - 1) (OK None));
            result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
        in ∀n < size ins. result!n ≠ Err)"

      wt_jvm_prog_kildall :: "jvm_prog => bool"
      "wt_jvm_prog_kildall G ==
      wf_prog (λG C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"

    theorem is_bcv_kiljvm:
      "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==>
          is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
                 (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
      apply (unfold kiljvm_def sl_triple_conv)
      apply (rule is_bcv_kildall)
           apply (simp (no_asm) add: sl_triple_conv [symmetric])
           apply (force intro!: semilat_JVM_slI dest: wf_acyclic
             simp add: symmetric sl_triple_conv)
          apply (simp (no_asm) add: JVM_le_unfold)
          apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
                       dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
         apply (simp add: JVM_le_unfold)
        apply (erule exec_pres_type)
       apply assumption
      apply (drule wf_prog_ws_prog, erule exec_mono, assumption)
      done

    lemma subset_replicate: "set (replicate n x) ⊆ {x}"
      by (induct n) auto

    lemma in_set_replicate:
      "x ∈ set (replicate n y) ==> x = y"
    proof -
      assume "x ∈ set (replicate n y)"
      also have "set (replicate n y) ⊆ {y}" by (rule subset_replicate)
      finally have "x ∈ {y}" .
      thus ?thesis by simp
    qed

    theorem wt_kil_correct:
      assumes wf:  "wf_prog wf_mb G"
      assumes C:   "is_class G C"
      assumes pTs: "set pTs ⊆ types G"

      assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"

      shows "∃phi. wt_method G C pTs rT maxs mxl bs et phi"
    proof -
      let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                    #(replicate (size bs - 1) (OK None))"

      from wtk obtain maxr r where
        bounded: "check_bounded bs et" and
        result:  "r = kiljvm G maxs maxr rT et bs ?start" and
        success: "∀n < size bs. r!n ≠ Err" and
        instrs:  "0 < size bs" and
        maxr:    "maxr = Suc (length pTs + mxl)"
        by (unfold wt_kil_def) simp

      from bounded have "bounded (exec G maxs rT et bs) (size bs)"
        by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
      with wf have bcv:
        "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
        (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
        by (rule is_bcv_kiljvm)

      from C pTs instrs maxr
      have "?start ∈ list (length bs) (states G maxs maxr)"
        apply (unfold JVM_states_unfold)
        apply (rule listI)
        apply (auto intro: list_appendI dest!: in_set_replicate)
        apply force
        done

      with bcv success result have
        "∃ts∈list (length bs) (states G maxs maxr).
             ?start <=[JVMType.le G maxs maxr] ts ∧
             wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
        by (unfold is_bcv_def) auto
      then obtain phi' where
        phi': "phi' ∈ list (length bs) (states G maxs maxr)" and
        s: "?start <=[JVMType.le G maxs maxr] phi'" and
        w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
        by blast
      hence wt_err_step:
        "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
        by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)

      from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
        by (drule_tac p=0 in le_listD) (simp add: lesub_def)+

      from phi' have l: "size phi' = size bs" by simp
      with instrs w have "phi' ! 0 ≠ Err" by (unfold wt_step_def) simp
      with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
        by (clarsimp simp add: not_Err_eq)

      from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
      also from w have "phi' = map OK (map ok_val phi')"
        apply (clarsimp simp add: wt_step_def not_Err_eq)
        apply (rule map_id [symmetric])
        apply (erule allE, erule impE, assumption)
        apply clarsimp
        done
      finally
      have check_types:
        "check_types G maxs maxr (map OK (map ok_val phi'))" .

      from l bounded
      have "bounded (λpc. eff (bs!pc) G pc et) (length phi')"
        by (simp add: exec_def check_bounded_is_bounded)
      hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
        by (auto intro: bounded_lift simp add: exec_def l)
      with wt_err_step
      have "wt_app_eff (sup_state_opt G) (λpc. app (bs!pc) G maxs rT pc et)
                       (λpc. eff (bs!pc) G pc et) (map ok_val phi')"
        by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
      with instrs l le bounded bounded' check_types maxr
      have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
        apply (unfold wt_method_def wt_app_eff_def)
        apply simp
        apply (rule conjI)
         apply (unfold wt_start_def)
         apply (rule JVM_le_convert [THEN iffD1])
         apply (simp (no_asm) add: phi0)
        apply clarify
        apply (erule allE, erule impE, assumption)
        apply (elim conjE)
        apply (clarsimp simp add: lesub_def wt_instr_def)
        apply (simp add: exec_def)
        apply (drule bounded_err_stepD, assumption+)
        apply blast
        done

      thus ?thesis by blast
    qed

    theorem wt_kil_complete:
      assumes wf:  "wf_prog wf_mb G"
      assumes C:   "is_class G C"
      assumes pTs: "set pTs ⊆ types G"

      assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"

      shows "wt_kil G C pTs rT maxs mxl et bs"
    proof -
      let ?mxr = "1+size pTs+mxl"

      from wtm obtain
        instrs:   "0 < length bs" and
        len:      "length phi = length bs" and
        bounded:  "check_bounded bs et" and
        ck_types: "check_types G maxs ?mxr (map OK phi)" and
        wt_start: "wt_start G C pTs mxl phi" and
        wt_ins:   "∀pc. pc < length bs -->
                        wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
        by (unfold wt_method_def) simp

      from ck_types len
      have istype_phi:
        "map OK phi ∈ list (length bs) (states G maxs (1+size pTs+mxl))"
        by (auto simp add: check_types_def intro!: listI)

      let ?eff  = "λpc. eff (bs!pc) G pc et"
      let ?app   = "λpc. app (bs!pc) G maxs rT pc et"

      from bounded
      have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
        by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)

      from wt_ins
      have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
        apply (unfold wt_app_eff_def wt_instr_def lesub_def)
        apply (simp (no_asm) only: len)
        apply blast
        done
      with bounded_exec
      have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
        by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)
      hence wt_err:
        "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
        by (unfold exec_def) (simp add: len)

      from wf bounded_exec
      have is_bcv:
        "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs)
                (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"
        by (rule is_bcv_kiljvm)

      let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                    #(replicate (size bs - 1) (OK None))"

      from C pTs instrs
      have start: "?start ∈ list (length bs) (states G maxs ?mxr)"
        apply (unfold JVM_states_unfold)
        apply (rule listI)
        apply (auto intro!: list_appendI dest!: in_set_replicate)
        apply force
        done

      let ?phi = "map OK phi"
      have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"
      proof -
        from len instrs
        have "length ?start = length (map OK phi)" by simp
        moreover
        { fix n
          from wt_start
          have "G \<turnstile> ok_val (?start!0) <=' phi!0"
            by (simp add: wt_start_def)
          moreover
          from instrs len
          have "0 < length phi" by simp
          ultimately
          have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"
            by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
          moreover
          { fix n'
            have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"
              by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
                split: err.splits)
            hence "[| n = Suc n'; n < length ?start |]
              ==> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"
              by simp
          }
          ultimately
          have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"
            by (unfold lesub_def) (cases n, blast+)
        }
        ultimately show ?thesis by (rule le_listI)
      qed

      from wt_err
      have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"
        by (simp add: wt_err_step_def JVM_le_Err_conv)
      with start istype_phi less_phi is_bcv
      have "∀p. p < length bs --> kiljvm G maxs ?mxr rT et bs ?start ! p ≠ Err"
        by (unfold is_bcv_def) auto
      with bounded instrs
      show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
    qed

    theorem jvm_kildall_sound_complete:
      "wt_jvm_prog_kildall G = (∃Phi. wt_jvm_prog G Phi)"
    proof
      let ?Phi = "λC sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
                  SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"

      assume "wt_jvm_prog_kildall G"
      hence "wt_jvm_prog G ?Phi"
        apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
        apply (erule jvm_prog_lift)
        apply (auto dest!: wt_kil_correct intro: someI)
        done
      thus "∃Phi. wt_jvm_prog G Phi" by fast
    next
      assume "∃Phi. wt_jvm_prog G Phi"
      thus "wt_jvm_prog_kildall G"
        apply (clarify)
        apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
        apply (erule jvm_prog_lift)
        apply (auto intro: wt_kil_complete)
        done
    qed

    end

theorem is_bcv_kiljvm:

      [| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (length bs) |]
      ==> is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) (length bs)
           (states G maxs maxr) (kiljvm G maxs maxr rT et bs)

lemma subset_replicate:

      set (replicate n x) ⊆ {x}

lemma in_set_replicate:

      x ∈ set (replicate n y) ==> x = y

theorem wt_kil_correct:

      [| wf_prog wf_mb G; is_class G C; set pTs ⊆ types G;
         wt_kil G C pTs rT maxs mxl et bs |]
      ==> ∃phi. wt_method G C pTs rT maxs mxl bs et phi

theorem wt_kil_complete:

      [| wf_prog wf_mb G; is_class G C; set pTs ⊆ types G;
         wt_method G C pTs rT maxs mxl bs et phi |]
      ==> wt_kil G C pTs rT maxs mxl et bs

theorem jvm_kildall_sound_complete:

      wt_jvm_prog_kildall G = (∃Phi. wt_jvm_prog G Phi)