Quelle  BVSpec.thy

(*  Title:      JinjaThreads/BV/BVSpec.thy
    Author:     Cornelia Pusch, Gerwin Klein, Andreas Lochbihler

    Based on the theory Jinja/BV/BVSpec
*)

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}.
 ›

― ‹The method type only contains declared classes:›
definition check_types :: "'m prog ==> nat ==> nat ==> ty_i' 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,'addr instr,pc,ty_m] ==> 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,ty_m] ==> bool"
where
  "wt_start P C Ts mxl₀ τs ≡
  P ⊨ Some ([],OK (Class C)#map OK Ts@replicate mxl₀ 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,'addr instr list, ex_table,ty_m] ==> bool"
where
  "wt_method P C Ts T_r mxs mxl₀ is xt τs ≡
  0 < size is ∧ size τs = size is ∧
  check_types P mxs (1+size Ts+mxl₀) (map OK τs) ∧
  wt_start P C Ts mxl₀ τs ∧
  (∀pc < size is. P,T_r,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 :: "ty_P ==> 'addr jvm_prog ==> bool" (‹wf'_jvm'_prog›)
where
  "wf_jvm_prog_<Phi> ≡
    wf_prog (λP C (M,Ts,T_r,(mxs,mxl₀,is,xt)).
      wt_method P C Ts T_r mxs mxl₀ is xt (Φ C M))"

definition wf_jvm_prog :: "'addr jvm_prog ==> bool"
where
  "wf_jvm_prog P ≡ ∃Φ. wf_jvm_prog_<Phi> P"

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

lemma wt_jvm_prog_impl_wt_instr:
  "[ wf_jvm_prog_<Phi> P;
      P ⊨ C sees M:Ts → T = ⌊(mxs,mxl₀,ins,xt)⌋ in C; pc < size ins ]
  ==> P,T,mxs,size ins,xt ⊨ 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_<Phi> P;
     P ⊨ C sees M:Ts → T = ⌊(mxs,mxl₀,ins,xt)⌋ in C ] ==>
  0 < size ins ∧ wt_start P C Ts mxl₀ (Φ 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