src/HOL/MicroJava/BV/LBVComplete.thy

completeness of the lightweight bytecode verifier

(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
    ID:         $Id$
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen

Proof of completeness for the lightweight bytecode verifier
*)

LBVComplete= LBVSpec +

constdefs
  is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
  "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
                   (a!n = None \\<or> a!n = Some (b!n)))"
  
  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
                            (\\<forall> pc. pc < length ins \\<longrightarrow>
                                   contains_dead ins cert phi pc \\<and> 
                                   contains_targets ins cert phi pc)"

  contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
  "contains_dead ins cert phi pc \\<equiv>
    (((\\<exists> branch. ins!pc = BR (Goto branch)) \\<or> ins!pc = MR Return) \\<or>
     (\\<exists>mi. ins!pc = MI mi)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
      cert ! (Suc pc) = Some (phi ! Suc pc)"

  contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
  "contains_targets ins cert phi pc \\<equiv> 
    \\<forall> branch. (ins!pc = BR (Goto branch) \\<or> ins!pc = BR (Ifcmpeq branch)) \\<longrightarrow>
        (let pc' = nat (int pc+branch) in pc' < length phi \\<longrightarrow> cert!pc' = Some (phi!pc'))" 

  is_target :: "[instr list, p_count] \\<Rightarrow> bool" 
  "is_target ins pc \\<equiv> 
     \\<exists> pc' branch. pc' < length ins \\<and> 
                   (ins ! pc' = (BR (Ifcmpeq branch)) \\<or> ins ! pc' = (BR (Goto branch))) \\<and> 
                   pc = (nat(int pc'+branch))"
  
  maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
  "maybe_dead ins pc \\<equiv>
     \\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = BR (Goto branch)) \\<or>
                          ins!pc' = MR Return \\<or>
                          (\\<exists>mi. ins!pc' = MI mi))"


  mdot :: "[instr list, p_count] \\<Rightarrow> bool"
  "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"


consts
  option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list" 
primrec 
  "option_filter_n []    P n = []"  
  "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) 
                                         else None   # option_filter_n t P (n+1))"  
  
constdefs 
  option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" 
  "option_filter l P \\<equiv> option_filter_n l P 0" 
  
  make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
  "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
  
  make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
  "make_Cert G Phi \\<equiv>  \\<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
        make_cert b (Phi C sig)"
  
constdefs
  wfprg :: "jvm_prog \\<Rightarrow> bool"
  "wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G"

end