header {* \isaheader{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 => 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,instr,pc,ty⇣m] => bool"
("_,_,_,_,_ \<turnstile> _,_ :: _" [60,0,0,0,0,0,0,61] 60)
where
"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: *}
definition wt_start :: "['m prog,cname,ty list,nat,ty⇣m] => bool"
where
"wt_start P C Ts mxl⇣0 τs ≡
P \<turnstile> Some ([],OK (Class C)#map OK Ts@replicate mxl⇣0 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,ty⇣m] => bool"
where
"wt_method P C Ts T⇣r mxs mxl⇣0 is xt τs ≡
0 < size is ∧ size τs = size is ∧
check_types P mxs (1+size Ts+mxl⇣0) (map OK τs) ∧
wt_start P C Ts mxl⇣0 τs ∧
(∀pc < size is. P,T⇣r,mxs,size is,xt \<turnstile> is!pc,pc :: τs)"
-- "A program is welltyped if it is wellformed and all methods are welltyped"
definition wf_jvm_prog_phi :: "ty⇣P => jvm_prog => bool" ("wf'_jvm'_prog⇘_⇙")
where
"wf_jvm_prog⇘Φ⇙ ≡
wf_prog (λP C (M,Ts,T⇣r,(mxs,mxl⇣0,is,xt)).
wt_method P C Ts T⇣r mxs mxl⇣0 is xt (Φ C M))"
definition wf_jvm_prog :: "jvm_prog => bool"
where
"wf_jvm_prog P ≡ ∃Φ. wf_jvm_prog⇘Φ⇙ P"
notation (input)
wf_jvm_prog_phi ("wf'_jvm'_prog⇩_ _" [0,999] 1000)
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,mxl⇣0,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,mxl⇣0,ins,xt) in C |] ==>
0 < size ins ∧ wt_start P C Ts mxl⇣0 (Φ 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