# Theory BVSpec

(*  Title:      JinjaDCI/BV/BVSpec.thy

Author:     Cornelia Pusch, Gerwin Klein, Susannah Mansky
Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

Based on the Jinja theory BV/BVSpec.thy by Tobias Nipkow
*)

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 ⇒ 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"
("_,_,_,_,_ ⊢ _,_ :: _" [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,staticb,ty list,nat,ty⇩m] ⇒ bool"
where
"wt_start P C b Ts mxl⇩0 τs ≡
case b of NonStatic ⇒ P ⊢ Some ([],OK (Class C)#map OK Ts@replicate mxl⇩0 Err) ≤' τs!0
| Static ⇒  P ⊢ Some ([],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,staticb,ty list,ty,nat,nat,instr list,
ex_table,ty⇩m] ⇒ bool"
where
"wt_method P C b Ts T⇩r mxs mxl⇩0 is xt τs ≡ (b = Static ∨ b = NonStatic) ∧
0 < size is ∧ size τs = size is ∧
check_types P mxs ((case b of Static ⇒ 0 | NonStatic ⇒ 1)+size Ts+mxl⇩0) (map OK τs) ∧
wt_start P C b Ts mxl⇩0 τ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 ⇒ jvm_prog ⇒ bool" ("wf'_jvm'_prog⇘_⇙")
where
"wf_jvm_prog⇘Φ⇙ ≡
wf_prog (λP C (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)).
wt_method P C b 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"

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,b:Ts → T = (mxs,mxl⇩0,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, b, Ts, T⇩r, mxs, mxl⇩0, is, xt).
wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M)) P" using wf
by (unfold wf_jvm_prog_phi_def)
show ?thesis using sees_wf_mdecl[OF wfm sees] pc
qed
(*>*)

lemma wt_jvm_prog_impl_wt_start:
assumes wf: "wf_jvm_prog⇘Φ⇙ P" and
sees: "P ⊢ C sees M,b:Ts → T = (mxs,mxl⇩0,ins,xt) in C"
shows "0 < size ins ∧ wt_start P C b Ts mxl⇩0 (Φ C M)"
(*<*)
proof -
have wfm: "wf_prog
(λP C (M, b, Ts, T⇩r, mxs, mxl⇩0, is, xt).
wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M)) P" using wf
by (unfold wf_jvm_prog_phi_def)
show ?thesis using sees_wf_mdecl[OF wfm sees]
qed
(*>*)

lemma wf_jvm_prog_nclinit:
assumes wtp: "wf_jvm_prog⇘Φ⇙ P"
and meth:  "P ⊢ C sees M, b :  Ts→T = (mxs, mxl⇩0, ins, xt) in D"
and wt:    "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
and pc:    "pc < length ins" and Φ: "Φ C M ! pc = Some(ST,LT)"
and ins:   "ins ! pc = Invokestatic C⇩0 M⇩0 n"
shows "M⇩0 ≠ clinit"
using assms by(simp add: wf_jvm_prog_phi_def wt_instr_def app_def)

end