(* Title: HOL/MicroJava/BV/LBVJVM.thy Author: Tobias Nipkow, Gerwin Klein Copyright 2000 TUM *) section {* LBV for the JVM \label{sec:JVM} *} theory LBVJVM imports Typing_Framework_JVM begin type_synonym prog_cert = "cname => sig => JVMType.state list" definition check_cert :: "jvm_prog => nat => nat => nat => JVMType.state list => bool" where "check_cert G mxs mxr n cert ≡ check_types G mxs mxr cert ∧ length cert = n+1 ∧ (∀i<n. cert!i ≠ Err) ∧ cert!n = OK None" definition lbvjvm :: "jvm_prog => nat => nat => ty => exception_table => JVMType.state list => instr list => JVMType.state => JVMType.state" where "lbvjvm G maxs maxr rT et cert bs ≡ wtl_inst_list bs cert (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0" definition wt_lbv :: "jvm_prog => cname => ty list => ty => nat => nat => exception_table => JVMType.state list => instr list => bool" where "wt_lbv G C pTs rT mxs mxl et cert ins ≡ check_bounded ins et ∧ check_cert G mxs (1+size pTs+mxl) (length ins) cert ∧ 0 < size ins ∧ (let start = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start) in result ≠ Err)" definition wt_jvm_prog_lbv :: "jvm_prog => prog_cert => bool" where "wt_jvm_prog_lbv G cert ≡ wf_prog (λG C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G" definition mk_cert :: "jvm_prog => nat => ty => exception_table => instr list => method_type => JVMType.state list" where "mk_cert G maxs rT et bs phi ≡ make_cert (exec G maxs rT et bs) (map OK phi) (OK None)" definition prg_cert :: "jvm_prog => prog_type => prog_cert" where "prg_cert G phi C sig ≡ let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in mk_cert G maxs rT et ins (phi C sig)" lemma wt_method_def2: fixes pTs and mxl and G and mxs and rT and et and bs and phi defines [simp]: "mxr ≡ 1 + length pTs + mxl" defines [simp]: "r ≡ sup_state_opt G" defines [simp]: "app0 ≡ λpc. app (bs!pc) G mxs rT pc et" defines [simp]: "step0 ≡ λpc. eff (bs!pc) G pc et" shows "wt_method G C pTs rT mxs mxl bs et phi = (bs ≠ [] ∧ length phi = length bs ∧ check_bounded bs et ∧ check_types G mxs mxr (map OK phi) ∧ wt_start G C pTs mxl phi ∧ wt_app_eff r app0 step0 phi)" by (auto simp add: wt_method_def wt_app_eff_def wt_instr_def lesub_def dest: check_bounded_is_bounded boundedD) lemma check_certD: "check_cert G mxs mxr n cert ==> cert_ok cert n Err (OK None) (states G mxs mxr)" apply (unfold cert_ok_def check_cert_def check_types_def) apply (auto simp add: list_all_iff) done lemma wt_lbv_wt_step: assumes wf: "wf_prog wf_mb G" assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins" assumes C: "is_class G C" assumes pTs: "set pTs ⊆ types G" defines [simp]: "mxr ≡ 1+length pTs+mxl" shows "∃ts ∈ list (size ins) (states G mxs mxr). wt_step (JVMType.le G mxs mxr) Err (exec G mxs rT et ins) ts ∧ OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) <=_(JVMType.le G mxs mxr) ts!0" proof - let ?step = "exec G mxs rT et ins" let ?r = "JVMType.le G mxs mxr" let ?f = "JVMType.sup G mxs mxr" let ?A = "states G mxs mxr" have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI, rule wf_prog_ws_prog, rule wf) hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) moreover have "top ?r Err" by (simp add: JVM_le_unfold) moreover have "Err ∈ ?A" by (simp add: JVM_states_unfold) moreover have "bottom ?r (OK None)" by (simp add: JVM_le_unfold bottom_def) moreover have "OK None ∈ ?A" by (simp add: JVM_states_unfold) moreover from lbv have "bounded ?step (length ins)" by (clarsimp simp add: wt_lbv_def exec_def) (intro bounded_lift check_bounded_is_bounded) moreover from lbv have "cert_ok cert (length ins) Err (OK None) ?A" by (unfold wt_lbv_def) (auto dest: check_certD) moreover from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type) moreover let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" from lbv have "wtl_inst_list ins cert ?f ?r Err (OK None) ?step 0 ?start ≠ Err" by (simp add: wt_lbv_def lbvjvm_def) moreover from C pTs have "?start ∈ ?A" by (unfold JVM_states_unfold) (auto intro: list_appendI, force) moreover from lbv have "0 < length ins" by (simp add: wt_lbv_def) ultimately show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro]) qed lemma wt_lbv_wt_method: assumes wf: "wf_prog wf_mb G" assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins" assumes C: "is_class G C" assumes pTs: "set pTs ⊆ types G" shows "∃phi. wt_method G C pTs rT mxs mxl ins et phi" proof - let ?mxr = "1 + length pTs + mxl" let ?step = "exec G mxs rT et ins" let ?r = "JVMType.le G mxs ?mxr" let ?f = "JVMType.sup G mxs ?mxr" let ?A = "states G mxs ?mxr" let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" from lbv have l: "ins ≠ []" by (simp add: wt_lbv_def) moreover from wf lbv C pTs obtain phi where list: "phi ∈ list (length ins) ?A" and step: "wt_step ?r Err ?step phi" and start: "?start <=_?r phi!0" by (blast dest: wt_lbv_wt_step) from list have [simp]: "length phi = length ins" by simp have "length (map ok_val phi) = length ins" by simp moreover from l have 0: "0 < length phi" by simp with step obtain phi0 where "phi!0 = OK phi0" by (unfold wt_step_def) blast with start 0 have "wt_start G C pTs mxl (map ok_val phi)" by (simp add: wt_start_def JVM_le_Err_conv lesub_def) moreover from lbv have chk_bounded: "check_bounded ins et" by (simp add: wt_lbv_def) moreover { from list have "check_types G mxs ?mxr phi" by (simp add: check_types_def) also from step have [symmetric]: "map OK (map ok_val phi) = phi" by (auto intro!: nth_equalityI simp add: wt_step_def) finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" . } moreover { let ?app = "λpc. app (ins!pc) G mxs rT pc et" let ?eff = "λpc. eff (ins!pc) G pc et" from chk_bounded have "bounded (err_step (length ins) ?app ?eff) (length ins)" by (blast dest: check_bounded_is_bounded boundedD intro: bounded_err_stepI) moreover from step have "wt_err_step (sup_state_opt G) ?step phi" by (simp add: wt_err_step_def JVM_le_Err_conv) ultimately have "wt_app_eff (sup_state_opt G) ?app ?eff (map ok_val phi)" by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def) } ultimately have "wt_method G C pTs rT mxs mxl ins et (map ok_val phi)" by - (rule wt_method_def2 [THEN iffD2], simp) thus ?thesis .. qed lemma wt_method_wt_lbv: assumes wf: "wf_prog wf_mb G" assumes wt: "wt_method G C pTs rT mxs mxl ins et phi" assumes C: "is_class G C" assumes pTs: "set pTs ⊆ types G" defines [simp]: "cert ≡ mk_cert G mxs rT et ins phi" shows "wt_lbv G C pTs rT mxs mxl et cert ins" proof - let ?mxr = "1 + length pTs + mxl" let ?step = "exec G mxs rT et ins" let ?app = "λpc. app (ins!pc) G mxs rT pc et" let ?eff = "λpc. eff (ins!pc) G pc et" let ?r = "JVMType.le G mxs ?mxr" let ?f = "JVMType.sup G mxs ?mxr" let ?A = "states G mxs ?mxr" let ?phi = "map OK phi" let ?cert = "make_cert ?step ?phi (OK None)" from wt have 0: "0 < length ins" and length: "length ins = length ?phi" and ck_bounded: "check_bounded ins et" and ck_types: "check_types G mxs ?mxr ?phi" and wt_start: "wt_start G C pTs mxl phi" and app_eff: "wt_app_eff (sup_state_opt G) ?app ?eff phi" by (simp_all add: wt_method_def2) have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf]) hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) moreover have "top ?r Err" by (simp add: JVM_le_unfold) moreover have "Err ∈ ?A" by (simp add: JVM_states_unfold) moreover have "bottom ?r (OK None)" by (simp add: JVM_le_unfold bottom_def) moreover have "OK None ∈ ?A" by (simp add: JVM_states_unfold) moreover from ck_bounded have bounded: "bounded ?step (length ins)" by (clarsimp simp add: exec_def) (intro bounded_lift check_bounded_is_bounded) with wf have "mono ?r ?step (length ins) ?A" by (rule wf_prog_ws_prog [THEN exec_mono]) hence "mono ?r ?step (length ?phi) ?A" by (simp add: length) moreover from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type) hence "pres_type ?step (length ?phi) ?A" by (simp add: length) moreover from ck_types have "set ?phi ⊆ ?A" by (simp add: check_types_def) hence "∀pc. pc < length ?phi --> ?phi!pc ∈ ?A ∧ ?phi!pc ≠ Err" by auto moreover from bounded have "bounded (exec G mxs rT et ins) (length ?phi)" by (simp add: length) moreover have "OK None ≠ Err" by simp moreover from bounded length app_eff have "wt_err_step (sup_state_opt G) ?step ?phi" by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def) hence "wt_step ?r Err ?step ?phi" by (simp add: wt_err_step_def JVM_le_Err_conv) moreover let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" from 0 length have "0 < length phi" by auto hence "?phi!0 = OK (phi!0)" by simp with wt_start have "?start <=_?r ?phi!0" by (clarsimp simp add: wt_start_def lesub_def JVM_le_Err_conv) moreover from C pTs have "?start ∈ ?A" by (unfold JVM_states_unfold) (auto intro: list_appendI, force) moreover have "?start ≠ Err" by simp moreover note length ultimately have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start ≠ Err" by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro]) moreover from 0 length have "phi ≠ []" by auto moreover from ck_types have "check_types G mxs ?mxr ?cert" by (auto simp add: make_cert_def check_types_def JVM_states_unfold) moreover note ck_bounded 0 length ultimately show ?thesis by (simp add: wt_lbv_def lbvjvm_def mk_cert_def check_cert_def make_cert_def nth_append) qed theorem jvm_lbv_correct: "wt_jvm_prog_lbv G Cert ==> ∃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_lbv G Cert" hence "wt_jvm_prog G ?Phi" apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) apply (erule jvm_prog_lift) apply (auto dest: wt_lbv_wt_method intro: someI) done thus ?thesis by blast qed theorem jvm_lbv_complete: "wt_jvm_prog G Phi ==> wt_jvm_prog_lbv G (prg_cert G Phi)" apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) apply (erule jvm_prog_lift) apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv) done end