src/HOL/MicroJava/BV/LBVSpec.thy

exceptions

+
−(*  Title:      HOL/MicroJava/BV/LBVSpec.thy
+
−    ID:         $Id$
+
−    Author:     Gerwin Klein
+
−    Copyright   1999 Technische Universitaet Muenchen
+
−*)
+
−
+
−header {* The Lightweight Bytecode Verifier *}
+
−
+
−theory LBVSpec = Effect + Kildall:
+
−
+
−text {* 
+
−  The Lightweight Bytecode Verifier with exceptions has not 
+
−  made it completely into the Isabelle 2001 release. Currently 
+
−  there is only the specification itself available. The proofs of
+
−  soundness and completeness are broken (they still need to be
+
−  ported to the exception version). Both theories are included
+
−  for documentation (but they don't work for this specification), 
+
−  please see the Isabelle 99-2 release for a working copy.
+
−*}
+
−
+
−types
+
−  certificate       = "state_type option list" 
+
−  class_certificate = "sig => certificate"
+
−  prog_certificate  = "cname => class_certificate"
+
−
+
−consts
+
−  merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+
−primrec
+
−  "merge G pc mxs mxr max_pc cert []     x = x"
+
−  "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in 
+
−                                       if pc' < max_pc \<and> pc' = pc+1 then 
+
−                                         merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x) 
+
−                                       else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then 
+
−                                         merge G pc mxs mxr max_pc cert ss x
+
−                                       else Err)"
+
−
+
−constdefs 
+
−  wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
+
−               => state_type option err" 
+
−  "wtl_inst i G rT s cert maxs maxr max_pc et pc == 
+
−     if app i G maxs rT pc et s then 
+
−       merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
+
−     else Err"
+
−
+
−  wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
+
−               => state_type option err"  
+
−  "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
+
−     case cert!pc of
+
−        None    => wtl_inst i G rT s cert maxs maxr max_pc et pc
+
−      | Some s' => if G \<turnstile> s <=' (Some s') then 
+
−                    wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc 
+
−                  else Err"
+
−
+
−consts 
+
−  wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
+
−                     state_type option] => state_type option err"
+
−primrec
+
−  "wtl_inst_list []     G rT cert maxs maxr max_pc et pc s = OK s"
+
−  "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s = 
+
−    (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
+
−     strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
+
−              
+
−
+
−constdefs
+
− wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"  
+
− "wtl_method G C pTs rT mxs mxl et ins cert ==  
+
−	let max_pc = length ins  
+
−  in 
+
−  0 < max_pc \<and>   
+
−  wtl_inst_list ins G rT cert mxs mxl max_pc et 0 
+
−                (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
+
−
+
− wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
+
− "wtl_jvm_prog G cert ==  
+
−  wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
+
−
+
−
+
−lemmas [iff] = not_Err_eq
+
−
+
−lemma if_eq_cases:
+
−  "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
+
−  by simp
+
−
+
−lemma merge_def:
+
−  "!!x. merge G pc mxs mxr max_pc cert ss x = 
+
−  (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
+
−    map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
+
−  else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
+
−proof (induct ss)
+
−  show "!!x. ?P [] x" by simp
+
−next
+
−  have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
+
−  fix x ss and s::"nat \<times> (state_type option)"
+
−  assume IH: "\<And>x. ?P ss x"
+
−  obtain pc' s' where s: "s = (pc',s')" by (cases s)  
+
−  hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
+
−  also
+
−  have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then 
+
−               ?merge ss (OK s' +_(sup G mxs mxr) x)
+
−             else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then 
+
−               ?merge ss x
+
−             else Err)" 
+
−    (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
+
−    by simp 
+
−  also 
+
−  let "if ?all ss then _ else _" = "?if ss x"    
+
−  have "\<dots> = ?if ((pc',s')#ss) x"
+
−  proof (cases "?pc'")    
+
−    case True
+
−    hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
+
−    with True
+
−    have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+
−    hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
+
−    with True show ?thesis by (fast intro: if_eq_cases)
+
−  next
+
−    case False
+
−    have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x" 
+
−    proof (cases ?G)
+
−      assume G: ?G with False
+
−      have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+
−      hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
+
−      with G show ?thesis by (fast intro: if_eq_cases)
+
−    next
+
−      assume G: "\<not>?G"
+
−      with False have "Err = ?if ((pc',s')#ss) x" by auto
+
−      with G show ?thesis by (fast intro: if_eq_cases)
+
−    qed
+
−    with False show ?thesis by (fast intro: if_eq_cases)
+
−  qed
+
−  also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
+
−  finally show "?P (s#ss) x" .
+
−qed
+
−  
+
−
+
−lemma wtl_inst_OK:
+
−"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
+
− app i G mxs rT pc et s \<and> 
+
−  (\<forall>(pc',r) \<in> set (eff i G pc et s). 
+
−  pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and> 
+
−  map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1] 
+
−  ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
+
−  by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
+
−
+
−lemma wtl_Cons:
+
−  "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err = 
+
−  (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and> 
+
−        wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
+
−  by (auto simp del: split_paired_Ex)
+
−
+
−lemma wtl_append:
+
−"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
+
−   (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and> 
+
−          wtl_inst_list b G rT cert mxs mxr mpc et (pc+length a) s'' = OK s')" 
+
−  (is "\<forall> s pc. ?C s pc a" is "?P a")
+
−proof (induct ?P a)
+
−  show "?P []" by simp
+
−next
+
−  fix x xs  assume IH: "?P xs"
+
−  show "?P (x#xs)"
+
−  proof (intro allI)
+
−    fix s pc 
+
−    show "?C s pc (x#xs)"
+
−    proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
+
−      case Err thus ?thesis by simp
+
−    next
+
−      fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"      
+
−      with IH have "?C s0 (Suc pc) xs" by blast
+
−      thus ?thesis by (simp!)
+
−    qed
+
−  qed
+
−qed
+
−
+
−lemma wtl_take:
+
−  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
+
−   \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
+
−proof -
+
−  assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
+
−  hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
+
−    by simp
+
−  thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
+
−qed
+
−
+
−lemma take_Suc:
+
−  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+
−proof (induct l)
+
−  show "?P []" by simp
+
−next
+
−  fix x xs assume IH: "?P xs"  
+
−  show "?P (x#xs)"
+
−  proof (intro strip)
+
−    fix n assume "n < length (x#xs)"
+
−    with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" 
+
−      by (cases n, auto)
+
−  qed
+
−qed
+
−
+
−lemma wtl_Suc:
+
− "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
+
−     wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
+
−     Suc pc < length is |] ==>
+
−  wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''" 
+
−proof -
+
−  assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
+
−         "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+
−         "Suc pc < length is"
+
−  hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+
−  thus ?thesis by (simp! add: wtl_append min_def)
+
−qed
+
−
+
−lemma wtl_all:
+
−  "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
+
−      pc < length is |] ==> 
+
−   \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and> 
+
−            wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+
−proof -
+
−  assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
+
−
+
−  assume pc: "pc < length is"
+
−  hence  "0 < length (drop pc is)" by simp
+
−  then  obtain i r where Cons: "drop pc is = i#r" 
+
−    by (auto simp add: neq_Nil_conv simp del: length_drop)
+
−  hence "i#r = drop pc is" ..
+
−  with all have take: 
+
−    "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
+
−    by simp
+
− 
+
−  from pc have "is!pc = drop pc is ! 0" by simp
+
−  with Cons have "is!pc = i" by simp
+
−  with take pc show ?thesis by (auto simp add: wtl_append min_def)
+
−qed
+
−
+
−
+
−end