Theory JVM_SemiType

(*  Title:      JinjaThreads/BV/JVM_SemiType.thy
    Author:     Gerwin Klein, Andreas Lochbihler

    Based on the theory Jinja/BV/JVM_SemiType
*)

chapter ‹Bytecode verifier›

section ‹The JVM Type System as Semilattice›

theory JVM_SemiType
imports
  "../Common/SemiType"
begin

type_synonym tyl = "ty err list"
type_synonym tys = "ty list"
type_synonym tyi = "tys × tyl"
type_synonym tyi' = "tyi option"
type_synonym tym = "tyi' list"
type_synonym tyP = "mname  cname  tym"

definition stk_esl :: "'c prog  nat  tys esl"
where
  "stk_esl P mxs  upto_esl mxs (SemiType.esl P)"

definition loc_sl :: "'c prog  nat  tyl sl"
where
  "loc_sl P mxl  Listn.sl mxl (Err.sl (SemiType.esl P))"

definition sl :: "'c prog  nat  nat  tyi' err sl"
where
  "sl P mxs mxl 
  Err.sl(Opt.esl(Product.esl (stk_esl P mxs) (Err.esl(loc_sl P mxl))))"

definition "states" :: "'c prog  nat  nat  tyi' err set"
where
  "states P mxs mxl  fst(sl P mxs mxl)"

definition le :: "'c prog  nat  nat  tyi' err ord"
where
  "le P mxs mxl  fst(snd(sl P mxs mxl))"

definition sup :: "'c prog  nat  nat  tyi' err binop"
where
  "sup P mxs mxl  snd(snd(sl P mxs mxl))"

definition sup_ty_opt :: "['c prog,ty err,ty err]  bool" 
  ("_  _  _" [71,71,71] 70)
where
  "sup_ty_opt P  Err.le (widen P)"

definition sup_state :: "['c prog,tyi,tyi]  bool"   
  ("_  _ i _" [71,71,71] 70)
where
  "sup_state P  Product.le (Listn.le (widen P)) (Listn.le (sup_ty_opt P))"

definition sup_state_opt :: "['c prog,tyi',tyi']  bool" 
  ("_  _ ≤'' _" [71,71,71] 70)
where
  "sup_state_opt P  Opt.le (sup_state P)"

abbreviation sup_loc :: "['c prog,tyl,tyl]  bool" ("_  _ [≤] _"  [71,71,71] 70)
where "P  LT [≤] LT'  list_all2 (sup_ty_opt P) LT LT'"

notation (ASCII)
  sup_ty_opt ("_ |- _ <=T _" [71,71,71] 70) and
  sup_state ("_ |- _ <=i _"  [71,71,71] 70) and
  sup_state_opt ("_ |- _ <=' _"  [71,71,71] 70) and
  sup_loc ("_ |- _ [<=T] _"  [71,71,71] 70)

subsection "Unfolding"

lemma JVM_states_unfold: 
  "states P mxs mxl  err(opt((Union {list n (types P) |n. n <= mxs}) ×
                                 list mxl (err(types P))))"
  apply (unfold states_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
  apply simp
  done

lemma JVM_le_unfold:
 "le P m n  
  Err.le(Opt.le(Product.le(Listn.le(widen P))(Listn.le(Err.le(widen P)))))" 
  apply (unfold le_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def  
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def) 
  apply simp
  done

lemma sl_def2:
  "JVM_SemiType.sl P mxs mxl  
  (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
 by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp 


lemma JVM_le_conv:
  "le P m n (OK t1) (OK t2) = P  t1 ≤' t2"
 by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def  
                sup_state_def sup_ty_opt_def) 

lemma JVM_le_Err_conv:
  "le P m n = Err.le (sup_state_opt P)"
 by (unfold sup_state_opt_def sup_state_def  
             sup_ty_opt_def JVM_le_unfold) simp 

lemma err_le_unfold [iff]: 
  "Err.le r (OK a) (OK b) = r a b"
 by (simp add: Err.le_def lesub_def) 
  

subsection ‹Semilattice›

lemma order_sup_state_opt [intro, simp]: 
  "wf_prog wf_mb P  order (sup_state_opt P)"   
 by (unfold sup_state_opt_def sup_state_def sup_ty_opt_def) blast 

lemma semilat_JVM [intro?]:
  "wf_prog wf_mb P  semilat (JVM_SemiType.sl P mxs mxl)"
  apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)  
  apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl 
                      Listn_sl err_semilat_JType_esl)
  done

lemma acc_JVM [intro]:
  "wf_prog wf_mb P  acc (JVM_SemiType.states P mxs mxl) (JVM_SemiType.le P mxs mxl)"
by(unfold JVM_le_unfold JVM_states_unfold) blast

subsection ‹Widening with ⊤›

lemma widen_refl[iff]: "widen P t t"  by (simp add: fun_of_def) 

lemma sup_ty_opt_refl [iff]: "P  T  T"
  apply (unfold sup_ty_opt_def)
  apply (fold lesub_def)
  apply (rule le_err_refl)
  apply (simp add: lesub_def)
  done

lemma Err_any_conv [iff]: "P  Err  T = (T = Err)"
 by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def]) 

lemma any_Err [iff]: "P  T  Err"
 by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def]) 

lemma OK_OK_conv [iff]:
  "P  OK T  OK T' = P  T  T'"
 by (simp add: sup_ty_opt_def fun_of_def) 

lemma any_OK_conv [iff]:
  "P  X  OK T' = (T. X = OK T  P  T  T')"
  apply (unfold sup_ty_opt_def) 
  apply (rule le_OK_conv [simplified lesub_def])
  done  

lemma OK_any_conv:
 "P  OK T  X = (X = Err  (T'. X = OK T'  P  T  T'))"
  apply (unfold sup_ty_opt_def) 
  apply (rule OK_le_conv [simplified lesub_def])
  done

lemma sup_ty_opt_trans [intro?, trans]:
  "P  a  b; P  b  c  P  a  c"
 by (auto intro: widen_trans  
           simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
           split: err.splits) 

subsection "Stack and Registers"

lemma stk_convert:
  "P  ST [≤] ST' = Listn.le (widen P) ST ST'"
 by (simp add: Listn.le_def lesub_def) 

lemma sup_loc_refl [iff]: "P  LT [≤] LT"
 by (rule list_all2_refl) simp 

lemmas sup_loc_Cons1 [iff] = list_all2_Cons1 [of "sup_ty_opt P"] for P

lemma sup_loc_def:
  "P  LT [≤] LT'  Listn.le (sup_ty_opt P) LT LT'"
 by (simp add: Listn.le_def lesub_def) 

lemma sup_loc_widens_conv [iff]:
  "P  map OK Ts [≤] map OK Ts' = P  Ts [≤] Ts'"
  by (simp add: list_all2_map1 list_all2_map2)

lemma sup_loc_trans [intro?, trans]:
  "P  a [≤] b; P  b [≤] c  P  a [≤] c"
 by (rule list_all2_trans, rule sup_ty_opt_trans) 

subsection "State Type"

lemma sup_state_conv [iff]:
  "P  (ST,LT) i (ST',LT') = (P  ST [≤] ST'  P  LT [≤] LT')"
 by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def) 
  
lemma sup_state_conv2:
  "P  s1 i s2 = (P  fst s1 [≤] fst s2  P  snd s1 [≤] snd s2)"
 by (cases s1, cases s2) simp 

lemma sup_state_refl [iff]: "P  s i s"
by (auto simp add: sup_state_conv2 intro: list_all2_refl)

lemma sup_state_trans [intro?, trans]:
  "P  a i b; P  b i c  P  a i c"
 by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2) 

lemma sup_state_opt_None_any [iff]:
  "P  None ≤' s"
 by (simp add: sup_state_opt_def Opt.le_def) 

lemma sup_state_opt_any_None [iff]:
  "P  s ≤' None = (s = None)"
 by (simp add: sup_state_opt_def Opt.le_def) 

lemma sup_state_opt_Some_Some [iff]:
  "P  Some a ≤' Some b = P  a i b"  
 by (simp add: sup_state_opt_def Opt.le_def lesub_def) 

lemma sup_state_opt_any_Some:
  "P  (Some s) ≤' X = (s'. X = Some s'  P  s i s')"
 by (simp add: sup_state_opt_def Opt.le_def lesub_def) 

lemma sup_state_opt_refl [iff]: "P  s ≤' s"
 by (simp add: sup_state_opt_def Opt.le_def lesub_def) 

lemma sup_state_opt_trans [intro?, trans]:
  "P  a ≤' b; P  b ≤' c  P  a ≤' c"
  apply (unfold sup_state_opt_def Opt.le_def lesub_def)
  apply (simp del: split_paired_All)
  apply (rule sup_state_trans, assumption+)
  done

end