Theory BVSpec

(*  Title:      HOL/MicroJava/BV/BVSpec.thy
    ID:         $Id: BVSpec.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen

*)

header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}

theory BVSpec = Effect:

text {*
  This theory contains a specification of the BV. The specification
  describes correct typings of method bodies; it corresponds 
  to type \emph{checking}.
*}


constdefs
  -- "The method type only contains declared classes:"
  check_types :: "'m prog => nat => nat => tyi' err list => bool"
  "check_types P mxs mxl τs ≡ set τs ⊆ states P mxs mxl"

  -- "An instruction is welltyped if it is applicable and its effect"
  -- "is compatible with the type at all successor instructions:"
  wt_instr :: "['m prog,ty,nat,pc,ex_table,instr,pc,tym] => bool"
  ("_,_,_,_,_ \<turnstile> _,_ :: _" [60,0,0,0,0,0,0,61] 60)
  "P,T,mxs,mpc,xt \<turnstile> i,pc :: τs ≡
  app i P mxs T pc mpc xt (τs!pc) ∧ 
  (∀(pc',τ') ∈ set (eff i P pc xt (τs!pc)). P \<turnstile> τ' ≤' τs!pc')"

  -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
  wt_start :: "['m prog,cname,ty list,nat,tym] => bool"
  "wt_start P C Ts mxl0 τs ≡
  P \<turnstile> Some ([],OK (Class C)#map OK Ts@replicate mxl0 Err) ≤' τs!0"

  -- "A method is welltyped if the body is not empty,"
  -- "if the method type covers all instructions and mentions"
  -- "declared classes only, if the method calling convention is respected, and"
  -- "if all instructions are welltyped."
  wt_method :: "['m prog,cname,ty list,ty,nat,nat,instr list,
                 ex_table,tym] => bool"
  "wt_method P C Ts Tr mxs mxl0 is xt τs ≡
  0 < size is ∧ size τs = size is ∧
  check_types P mxs (1+size Ts+mxl0) (map OK τs) ∧
  wt_start P C Ts mxl0 τs ∧
  (∀pc < size is. P,Tr,mxs,size is,xt \<turnstile> is!pc,pc :: τs)"

  -- "A program is welltyped if it is wellformed and all methods are welltyped"
  wf_jvm_prog_phi :: "tyP => jvm_prog => bool" ("wf'_jvm'_prog_")
  "wf_jvm_progΦ ≡
    wf_prog (λP C' (M,Ts,Tr,(mxs,mxl0,is,xt)). 
      wt_method P C' Ts Tr mxs mxl0 is xt (Φ C' M))"

  wf_jvm_prog :: "jvm_prog => bool"
  "wf_jvm_prog P ≡ ∃Φ. wf_jvm_progΦ P"

syntax
  wf_jvm_prog_phi :: "tyP => jvm_prog => bool" ("wf'_jvm'_prog_ _" [0,999] 1000)
translations
  "wf_jvm_progΦ P" <= "wf_jvm_progΦ P"


lemma wt_jvm_progD:
  "wf_jvm_progΦ P ==> ∃wt. wf_prog wt P"
(*<*) by (unfold wf_jvm_prog_phi_def, blast) (*>*)

lemma wt_jvm_prog_impl_wt_instr:
  "[| wf_jvm_progΦ P; 
      P \<turnstile> C sees M:Ts -> T = (mxs,mxl0,ins,xt) in C; pc < size ins |] 
  ==> P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
(*<*)
  apply (unfold wf_jvm_prog_phi_def)
  apply (drule (1) sees_wf_mdecl)
  apply (simp add: wf_mdecl_def wt_method_def)
  done
(*>*)

lemma wt_jvm_prog_impl_wt_start:
  "[| wf_jvm_progΦ P; 
     P \<turnstile> C sees M:Ts -> T = (mxs,mxl0,ins,xt) in C |] ==> 
  0 < size ins ∧ wt_start P C Ts mxl0 (Φ C M)"
(*<*)
  apply (unfold wf_jvm_prog_phi_def)
  apply (drule (1) sees_wf_mdecl)
  apply (simp add: wf_mdecl_def wt_method_def)
  done
(*>*)

end