Theory BVSpec

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

    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen

*)

section ‹The Bytecode Verifier \label{sec:BVSpec}›

theory BVSpec
imports Effect
begin

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


definition
  ― ‹The method type only contains declared classes:›
  check_types :: "'m prog  nat  nat  tyi' err list  bool"
where 
  "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:›
definition
  wt_instr :: "['m prog,ty,nat,pc,ex_table,instr,pc,tym]  bool"
  ("_,_,_,_,_  _,_ :: _" [60,0,0,0,0,0,0,61] 60)
where
  "P,T,mxs,mpc,xt  i,pc :: τs 
  app i P mxs T pc mpc xt (τs!pc)  
  ((pc',τ')  set (eff i P pc xt (τs!pc)). P  τ' ≤' τs!pc')"

  ― ‹The type at @{text "pc=0"} conforms to the method calling convention:›
definition wt_start :: "['m prog,cname,ty list,nat,tym]  bool"
where
  "wt_start P C Ts mxl0 τs 
  P  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.›
definition wt_method :: "['m prog,cname,ty list,ty,nat,nat,instr list,
                 ex_table,tym]  bool"
where
  "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  is!pc,pc :: τs)"

  ― ‹A program is welltyped if it is wellformed and all methods are welltyped›
definition  wf_jvm_prog_phi :: "tyP  jvm_prog  bool" ("wf'_jvm'_prog⇘_")
where
  "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))"

definition wf_jvm_prog :: "jvm_prog  bool"
where
  "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:
assumes wf: "wf_jvm_prog⇘ΦP" and
      sees: "P  C sees M:Ts  T = (mxs,mxl0,ins,xt) in C" and
        pc: "pc < size ins"
shows "P,T,mxs,size ins,xt  ins!pc,pc :: Φ C M"
(*<*)
proof -
  have wfm: "wf_prog
     (λP C (M, Ts, Tr, mxs, mxl0, is, xt).
         wt_method P C Ts Tr mxs mxl0 is xt (Φ C M)) P" using wf
    by (unfold wf_jvm_prog_phi_def)
  show ?thesis using sees_wf_mdecl[OF wfm sees] pc
    by (simp add: wf_mdecl_def wt_method_def)
qed
(*>*)

lemma wt_jvm_prog_impl_wt_start:
assumes wf: "wf_jvm_prog⇘ΦP" and
      sees: "P  C sees M:Ts  T = (mxs,mxl0,ins,xt) in C"
shows "0 < size ins  wt_start P C Ts mxl0 (Φ C M)"
(*<*)
proof -
  have wfm: "wf_prog
     (λP C (M, Ts, Tr, mxs, mxl0, is, xt).
         wt_method P C Ts Tr mxs mxl0 is xt (Φ C M)) P" using wf
    by (unfold wf_jvm_prog_phi_def)
  show ?thesis using sees_wf_mdecl[OF wfm sees]
    by (simp add: wf_mdecl_def wt_method_def)
qed


end