(* Title: HOL/MicroJava/BV/BVLcorrect.thy
ID: $Id$
Author: Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
Correctness of the lightweight bytecode verifier
*)
theory LBVCorrect = LBVSpec:;
constdefs
fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow>
wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow>
wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow>
((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and>
(\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert";
lemma fitsD:
"fits phi is G rT s0 s2 cert \\<Longrightarrow>
(a@(i#b) = is) \\<Longrightarrow>
wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\<Longrightarrow>
wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\<Longrightarrow>
((cert!(0+length a) = None \\<longrightarrow> phi!(0+length a) = s1) \\<and>
(\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))";
by (unfold fits_def fits_partial_def) blast;
lemma exists_list: "\\<exists>l. n < length l" (is "?Q n");
proof (induct "n");
fix n; assume "?Q n";
thus "?Q (Suc n)";
proof elim;
fix l; assume "n < length (l::'a list)";
hence "Suc n < length (a#l)"; by simp;
thus ?thesis; ..;
qed;
qed auto;
lemma exists_phi:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
\\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi";
proof -;
assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
have "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc
\\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)"
(is "?P is");
proof (induct "?P" "is");
case Nil;
show "?P []"; by (simp add: fits_partial_def exists_list);
case Cons;
show "?P (a#list)";
proof (intro allI impI);
fix s0 pc;
assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc";
thus "\\<exists>phi. pc + length (a # list) < length phi \\<and>
fits_partial phi pc (a # list) G rT s0 s2 cert";
obtain s1 where
opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and
wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)";
by auto;
with Cons;
show ?thesis;
obtain phi where fits: "fits_partial phi (Suc pc) list G rT s1 s2 cert"
and length: "(Suc pc) + length list < length phi"; by blast;
let "?A phi pc x s1'" =
"(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
(\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)";
show ?thesis;
proof (cases "cert!pc");
case None;
have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert";
proof (unfold fits_partial_def, intro allI impI);
fix x i y s1';
assume * :
"x @ i # y = a # list"
"wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
"wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
show "?A (phi[pc:= s0]) pc x s1'";
proof (cases "x");
assume "x = []";
with * length None;
show ?thesis; by simp;
next;
fix b l; assume Cons: "x = b#l";
with fits *;
have "?A (phi[pc:= s0]) (Suc pc) l s1'";
proof (unfold fits_partial_def, elim allE impE);
from * Cons;
show "l @ i # y = list"; by simp;
from Cons opt *;
show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)";
by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
qed simp+;
with Cons length;
show ?thesis; by auto;
qed;
qed;
with length;
show ?thesis; by intro auto;
next;
fix c; assume Some: "cert!pc = Some c";
have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert";
proof (unfold fits_partial_def, intro allI impI);
fix x i y s1';
assume * :
"x @ i # y = a # list"
"wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
"wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
show "?A (phi[pc:= c]) pc x s1'";
proof (cases "x");
assume "x = []";
with length Some;
show ?thesis; by simp;
next;
fix b l; assume Cons: "x = b#l";
with fits *;
have "?A (phi[pc:= c]) (Suc pc) l s1'";
proof (unfold fits_partial_def, elim allE impE);
from * Cons;
show "l @ i # y = list"; by simp;
from Cons opt *;
show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)";
by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
qed simp+;
with Cons length;
show ?thesis; by auto;
qed;
qed;
with length;
show ?thesis; by intro auto;
qed;
qed;
qed;
qed;
qed;
with all;
show ?thesis;
proof elim;
show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0"; by simp;
qed (auto simp add: fits_def);
qed;
lemma fits_lemma1:
"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
\\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
proof intro;
fix pc t;
assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0";
assume fits: "fits phi is G rT s0 s3 cert";
assume pc: "pc < length is";
assume cert: "cert ! pc = Some t";
from pc;
have "is \\<noteq> []"; by auto;
hence cons: "\\<exists>i y. is = i#y"; by (simp add: neq_Nil_conv);
from wtl pc;
have "\\<exists>a b s1. a@b = is \\<and> length a = pc \\<and>
wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<and>
wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
(is "\\<exists>a b s1. ?A a b \\<and> ?L a \\<and> ?W1 a s1 \\<and> ?W2 a b s1");
by (rule wtl_partial [rulify]);
with cons;
show "phi ! pc = t";
proof (elim exE conjE);
fix a b s1 i y;
assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y";
with pc;
have "b \\<noteq> []"; by auto;
hence "\\<exists>b' bs. b = b'#bs"; by (simp add: neq_Nil_conv);
thus ?thesis;
proof (elim exE);
fix b' bs; assume Cons: "b=b'#bs";
with * fits cert;
show ?thesis;
proof (unfold fits_def fits_partial_def, elim allE impE);
from * Cons; show "a@b'#bs=is"; by simp;
qed simp+;
qed;
qed;
qed;
lemma fits_lemma2:
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None;
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk>
\\<Longrightarrow> phi!(length a) = s1";
proof (unfold fits_def fits_partial_def, elim allE impE);
qed (auto simp del: split_paired_Ex);
lemma wtl_suc_pc:
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a));
fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow>
b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
proof;
assume f: "fits phi (a@i#b) G rT s0 s3 cert";
assume "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
"wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append);
assume "b \\<noteq> []";
thus "G \\<turnstile> s2 <=s phi ! Suc (length a)";
obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
with f;
show ?thesis;
proof (rule fitsD [elimify]);
from Cons w;
show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
by simp;
from a;
show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;
assume cert:
"(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
(\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
show ?thesis;
proof (cases "cert ! Suc (length a)");
assume "cert ! Suc (length a) = None";
with cert;
have "s2 = phi ! Suc (length a)"; by simp;
thus ?thesis; by simp;
next;
fix t; assume "cert ! Suc (length a) = Some t";
with cert;
have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
with cert Cons w;
show ?thesis; by (auto simp add: wtl_inst_option_def);
qed;
qed;
qed;
qed;
lemma wtl_lemma:
"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1);
wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1));
fits phi (i1@i#i2) G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i");
proof -;
assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1);
assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)";
assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))";
assume f: "fits phi (i1@i#i2) G rT s0 s3 cert";
from w1 wo w2;
have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0";
by (rule wtl_cons_appendl);
with f;
have c1: "\\<forall>t. cert ! (length i1) = Some t \\<longrightarrow> phi ! (length i1) = t";
by intro (rule fits_lemma1 [rulify], auto);
from w1 wo w2 f;
have c2: "cert ! (length i1) = None \\<Longrightarrow> phi ! (length i1) = s1";
by - (rule fits_lemma2);
from wtl f;
have c3: "\\<forall>pc t. pc < length(i1@i#i2) \\<longrightarrow> cert ! pc = Some t \\<longrightarrow> phi ! pc = t";
by (rule fits_lemma1);
from w1 wo w2 f;
have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)";
by (rule wtl_suc_pc [rulify]);
show ?thesis;
proof (cases "i");
case LS;
with wo suc;
show ?thesis;
by - (cases "load_and_store",
(cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
next;
case CO;
with wo suc;
show ?thesis;
by - (cases "create_object" ,
cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
next;
case MO;
with wo suc;
show ?thesis;
by - (cases "manipulate_object" ,
(cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
next;
case CH;
with wo suc;
show ?thesis;
by - (cases "check_object" , cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
next;
case MI;
with wo suc;
show ?thesis;
by - (cases "meth_inv", cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
intro exI conjI, rule refl, simp, force,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def,
intro exI conjI, rule refl, simp, force);
next;
case MR;
with wo suc;
show ?thesis;
by - (cases "meth_ret" , cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
next;
case OS;
with wo suc;
show ?thesis;
by - (cases "op_stack" ,
(cases "cert ! (length i1)",
clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
next;
case BR;
with wo suc;
show ?thesis;
by - (cases "branch",
(cases "cert ! (length i1)",
clarsimp_tac simp add: c2 c3 wt_instr_def wtl_inst_option_def split_beta,
clarsimp_tac simp add: c1 c3 wt_instr_def wtl_inst_option_def)+);
qed;
qed;
lemma wtl_fits_wt:
"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk>
\\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
proof intro;
assume fits: "fits phi is G rT s0 s3 cert";
fix pc;
assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
and pc: "pc < length is";
thus "wt_instr (is ! pc) G rT phi (length is) pc";
obtain i1 i2' s1 where l: "i1 @ i2' = is" "length i1 = pc" and
w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and
w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)";
by (rule wtl_partial [rulify, elimify]) (elim, rule that);
from l pc;
have "i2' \\<noteq> []"; by auto;
thus ?thesis;
obtain i i2 where c: "i2' = i#i2"; by (simp add: neq_Nil_conv) (elim, rule that);
with w2 l;
show ?thesis;
obtain s2 where w3:
"wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
"wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"; by auto;
from w1 l c;
have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0"; by simp;
from l c fits;
have "fits phi (i1@i#i2) G rT s0 s3 cert"; by simp;
with w4 w3;
have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)"; by (rule wtl_lemma);
with l c;
show ?thesis; by (auto simp add: nth_append);
qed;
qed;
qed;
qed;
lemma wtl_inst_list_correct:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
\\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
proof -;
assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
thus ?thesis;
obtain phi where "fits phi is G rT s0 s2 cert";
by (rule exists_phi [elimify]) blast;
with wtl;
show ?thesis;
by (rule wtl_fits_wt [elimify]) blast;
qed;
qed;
lemma fits_first:
"\\<lbrakk>is \\<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0;
fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
proof -;
assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
assume fits: "fits phi is G rT s0 s2 cert";
assume "is \\<noteq> []";
thus ?thesis;
obtain y ys where cons: "is = y#ys"; by (simp add: neq_Nil_conv) (elim, rule that);
from fits;
show ?thesis;
proof (rule fitsD [elimify]);
from cons; show "[]@y#ys = is"; by simp;
from cons wtl;
show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])";
by simp;
assume cert:
"(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
(\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)";
show ?thesis;
proof (cases "cert!0");
assume "cert!0 = None";
with cert;
show ?thesis; by simp;
next;
fix t; assume "cert!0 = Some t";
with cert;
have "phi!0 = t"; by (simp del: split_paired_All);
with cert cons wtl;
show ?thesis; by (auto simp add: wtl_inst_option_def);
qed;
qed simp;
qed;
qed;
lemma wtl_method_correct:
"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi";
proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE);
let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)";
fix s2;
assume neqNil: "ins \\<noteq> []";
assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0";
thus ?thesis;
obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi";
by (rule exists_phi [elimify]) blast;
with wtl;
have allpc:
"\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc";
by elim (rule wtl_fits_wt [elimify]);
from neqNil wtl fits;
have "wt_start G C pTs mxl phi";
by (elim conjE, unfold wt_start_def) (rule fits_first);
with neqNil allpc fits;
show ?thesis; by (auto simp add: wt_method_def);
qed;
qed;
lemma unique_set:
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
by (induct "l") auto;
lemma unique_epsilon:
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
by (auto simp add: unique_set);
theorem wtl_correct:
"wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
proof (clarsimp_tac simp add: wt_jvm_prog_def wf_prog_def, intro conjI);
assume wtl_prog: "wtl_jvm_prog G cert";
thus "ObjectC \\<in> set G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
from wtl_prog;
show uniqueG: "unique G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
show "\\<exists>Phi. Ball (set G) (wf_cdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
(is "\\<exists>Phi. ?Q Phi");
proof (intro exI);
let "?Phi" =
"\\<lambda> C sig. let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in\
\\<epsilon> phi. wt_method G C (snd sig) rT maxl b phi";
from wtl_prog;
show "?Q ?Phi";
proof (unfold wf_cdecl_def, intro);
fix x a b aa ba ab bb m;
assume 1: "x \\<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \\<in> set bb";
with wtl_prog;
show "wf_mdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m";
proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE);
apply_end (drule bspec, assumption, simp, elim conjE);
assume "\\<forall>(sig,rT,mb)\\<in>set bb. wf_mhead G sig rT \\<and>
(\\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
"unique bb";
with 1 uniqueG;
show "(\\<lambda>(sig,rT,mb).
wf_mhead G sig rT \\<and>
(\\<lambda>(maxl,b).
wt_method G a (snd sig) rT maxl b
((\\<lambda>(C,x,y,mdecls).
(\\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
(\\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \\<in> set mdecls \\<and> sg = sig))
(\\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\<in> set G \\<and> Cl = a))) mb) m";
by - (drule bspec, assumption,
clarsimp_tac elim: wtl_method_correct [elimify],
clarsimp_tac intro: selectI simp add: unique_epsilon);
qed;
qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
qed;
qed;
end;