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

Author: Tobias Nipkow, Gerwin Klein

Copyright 2000 TUM

*)

header {* \isaheader{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