Theory LBVJVM

(*  Title:      JinjaDCI/BV/LBVJVM.thy

    Author:     Tobias Nipkow, Gerwin Klein, Susannah Mansky
    Copyright   2000 TUM, 2020 UIUC

    Based on the Jinja theory BV/LBVJVM.thy by Tobias Nipkow and Gerwin Klein
*)

section ‹ LBV for the JVM \label{sec:JVM} ›

theory LBVJVM
imports Jinja.Abstract_BV TF_JVM
begin

type_synonym prog_cert = "cname  mname  tyi' err list"

definition check_cert :: "jvm_prog  nat  nat  nat  tyi' err list  bool"
where
  "check_cert P mxs mxl n cert  check_types P mxs mxl cert  size cert = n+1 
                                 (i<n. cert!i  Err)  cert!n = OK None"

definition lbvjvm :: "jvm_prog  nat  nat  ty  ex_table  
             tyi' err list  instr list  tyi' err  tyi' err"
where
  "lbvjvm P mxs maxr Tr et cert bs 
  wtl_inst_list bs cert (JVM_SemiType.sup P mxs maxr) (JVM_SemiType.le P mxs maxr) Err (OK None) (exec P mxs Tr et bs) 0"

definition wt_lbv :: "jvm_prog  cname  staticb  ty list  ty  nat  nat  
             ex_table  tyi' err list  instr list  bool"
where
  "wt_lbv P C b Ts Tr mxs mxl0 et cert ins  (b = Static  b = NonStatic) 
   check_cert P mxs ((case b of Static  0 | NonStatic  1)+size Ts+mxl0) (size ins) cert 
   0 < size ins  
   (let start  = Some ([],(case b of Static  [] | NonStatic  [OK (Class C)])
                            @((map OK Ts))@(replicate mxl0 Err));
        result = lbvjvm P mxs ((case b of Static  0 | NonStatic  1)+size Ts+mxl0) Tr et cert ins (OK start)
    in result  Err)"

definition wt_jvm_prog_lbv :: "jvm_prog  prog_cert  bool"
where
  "wt_jvm_prog_lbv P cert 
  wf_prog (λP C (mn,b,Ts,Tr,(mxs,mxl0,ins,et)). wt_lbv P C b Ts Tr mxs mxl0 et (cert C mn) ins) P"

definition mk_cert :: "jvm_prog  nat  ty  ex_table  instr list 
               tym  tyi' err list"
where
  "mk_cert P mxs Tr et bs phi  make_cert (exec P mxs Tr et bs) (map OK phi) (OK None)"

definition prg_cert :: "jvm_prog  tyP  prog_cert"
where
  "prg_cert P phi C mn  let (C,b,Ts,Tr,(mxs,mxl0,ins,et)) = method P C mn
                         in  mk_cert P mxs Tr et ins (phi C mn)"
   
lemma check_certD [intro?]:
  "check_cert P mxs mxl n cert  cert_ok cert n Err (OK None) (states P mxs mxl)"
  by (unfold cert_ok_def check_cert_def check_types_def) auto


lemma (in start_context) wt_lbv_wt_step:
  assumes lbv: "wt_lbv P C b Ts Tr mxs mxl0 xt cert is"
  shows "τs  nlists (size is) A. wt_step r Err step τs  OK first ⊑⇩r τs!0"
(*<*)
proof -
  from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
  hence "semilat (A, r, f)" by (simp add: sl_def2)
  moreover have "top r Err" by (simp add: JVM_le_Err_conv)
  moreover have "Err  A" by (simp add: JVM_states_unfold)
  moreover have "bottom r (OK None)" 
    by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
  moreover have "OK None  A" by (simp add: JVM_states_unfold)
  moreover note bounded_step
  moreover from lbv have "cert_ok cert (size is) Err (OK None) A"
    by (unfold wt_lbv_def) (auto dest: check_certD)
  moreover note exec_pres_type
  moreover
  from lbv 
  have "wtl_inst_list is cert f r Err (OK None) step 0 (OK first)  Err"
    by (cases b; simp add: wt_lbv_def lbvjvm_def step_def_exec [symmetric])
  moreover note first_in_A
  moreover from lbv have "0 < size is" by (simp add: wt_lbv_def)
  ultimately show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
qed
(*>*)


lemma (in start_context) wt_lbv_wt_method:
  assumes lbv: "wt_lbv P C b Ts Tr mxs mxl0 xt cert is"  
  shows "τs. wt_method P C b Ts Tr mxs mxl0 is xt τs"
(*<*)
proof -
  from lbv have l: "is  []" and  
             stab: "b = Static  b = NonStatic" by (auto simp add: wt_lbv_def)
  moreover
  from wf lbv C Ts obtain τs where 
    list:  "τs  nlists (size is) A" and
    step:  "wt_step r Err step τs" and    
    start: "OK first ⊑⇩r τs!0" 
    by (blast dest: wt_lbv_wt_step)
  from list have [simp]: "size τs = size is" by simp
  have "size (map ok_val τs) = size is" by simp  
  moreover from l have 0: "0 < size τs" by simp
  with step obtain τs0 where "τs!0 = OK τs0"
    by (unfold wt_step_def) blast
  with start 0 have "wt_start P C b Ts mxl0 (map ok_val τs)"
    by (cases b; simp add: wt_start_def JVM_le_Err_conv lesub_def Err.le_def)    
  moreover {
    from list have "check_types P mxs mxl τs" by (simp add: check_types_def)
    also from step  have "x  set τs. x  Err" 
      by (auto simp add: all_set_conv_all_nth wt_step_def)    
    hence [symmetric]: "map OK (map ok_val τs) = τs"
      by (auto intro!: map_idI)
    finally have "check_types P mxs mxl (map OK (map ok_val τs))" .
  }
  moreover {  
    note bounded_step
    moreover from list have "set τs  A" by simp
    moreover from step have "wt_err_step (sup_state_opt P) step τs"
      by (simp add: wt_err_step_def JVM_le_Err_conv)
    ultimately have "wt_app_eff (sup_state_opt P) app eff (map ok_val τs)"
      by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def states_def)
  }    
  ultimately have "wt_method P C b Ts Tr mxs mxl0 is xt (map ok_val τs)"
    by (simp add: wt_method_def2 check_types_def del: map_map)
  thus ?thesis ..
qed
(*>*)

  
lemma (in start_context) wt_method_wt_lbv:
  assumes wt: "wt_method P C b Ts Tr mxs mxl0 is xt τs" 
  defines [simp]: "cert  mk_cert P mxs Tr xt is τs"
  
  shows "wt_lbv P C b Ts Tr mxs mxl0 xt cert is" 
(*<*)
proof -
  let ?τs  = "map OK τs"
  let ?cert = "make_cert step ?τs (OK None)"

  from wt obtain 
    0:        "0 < size is" and
    size:     "size is = size ?τs" and
    ck_types: "check_types P mxs mxl ?τs" and
    wt_start: "wt_start P C b Ts mxl0 τs" and
    app_eff:  "wt_app_eff (sup_state_opt P) app eff τs"
    by (force simp add: wt_method_def2 check_types_def) 
  
  from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
  hence "semilat (A, r, f)" by (simp add: sl_def2)
  moreover have "top r Err" by (simp add: JVM_le_Err_conv)
  moreover have "Err  A" by (simp add: JVM_states_unfold)
  moreover have "bottom r (OK None)" 
    by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
  moreover have "OK None  A" by (simp add: JVM_states_unfold)
  moreover from wf have "mono r step (size is) A" by (rule step_mono)
  hence "mono r step (size ?τs) A" by (simp add: size)
  moreover from exec_pres_type 
  have "pres_type step (size ?τs) A" by (simp add: size) 
  moreover
  from ck_types have τs_in_A: "set ?τs  A" by (simp add: check_types_def)
  hence "pc. pc < size ?τs  ?τs!pc  A  ?τs!pc  Err" by auto
  moreover from bounded_step 
  have "bounded step (size ?τs)" by (simp add: size)
  moreover have "OK None  Err" by simp
  moreover from bounded_step size τs_in_A app_eff
  have "wt_err_step (sup_state_opt P) step ?τs"
    by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def)    
  hence "wt_step r Err step ?τs"
    by (simp add: wt_err_step_def JVM_le_Err_conv)
  moreover
  from 0 size have "0 < size τs" by auto
  hence "?τs!0 = OK (τs!0)" by simp
  with wt_start have "OK first ⊑⇩r ?τs!0"
    by (cases b; clarsimp simp add: wt_start_def lesub_def Err.le_def JVM_le_Err_conv)
  moreover note first_in_A
  moreover have "OK first  Err" by simp
  moreover note size 
  ultimately
  have "wtl_inst_list is ?cert f r Err (OK None) step 0 (OK first)  Err"
    by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
  moreover from 0 size have "τs  []" by auto
  moreover from ck_types have "check_types P mxs mxl ?cert"
    by (fastforce simp: make_cert_def check_types_def JVM_states_unfold
                  dest!: nth_mem)
  moreover note 0 size
  ultimately show ?thesis using staticb
    by (simp add: wt_lbv_def lbvjvm_def mk_cert_def step_def_exec [symmetric]
                  check_cert_def make_cert_def nth_append)
qed  
(*>*)



theorem jvm_lbv_correct:
  "wt_jvm_prog_lbv P Cert  wf_jvm_prog P"
(*<*)
proof -  
  let  = "λC mn. let (C,b,Ts,Tr,(mxs,mxl0,is,xt)) = method P C mn in 
              SOME τs. wt_method P C b Ts Tr mxs mxl0 is xt τs"
  
  let ?A = "λP C (mn,b,Ts,Tr,(mxs,mxl0,ins,et)). wt_lbv P C b Ts Tr mxs mxl0 et (Cert C mn) ins"
  let ?B = "λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). 
                wt_method P C b Ts Tr mxs mxl0 is xt ( C M)"

  assume wt: "wt_jvm_prog_lbv P Cert"
  then have "wf_prog ?A P" by(simp add: wt_jvm_prog_lbv_def)
  moreover {
    fix wf_md C M b Ts Ca T m bd
    
    assume ass1: "wf_prog wf_md P" and sees: "P  Ca sees M, b :  TsT = m in Ca" and
           ass2: "set Ts  types P" and ass3: "bd = (M, b, Ts, T, m)" and
           ass4: "?A P Ca bd"
    from ass3 ass4 have stab: "b = Static  b = NonStatic" by (simp add:wt_lbv_def)        
    from ass1 sees ass2 ass3 ass4 have "?B P Ca bd" using sees_method_is_class[OF sees] 
      by (auto  dest!: start_context.wt_lbv_wt_method [OF start_context_intro_auxi[OF stab]]
               intro: someI)  
  }
  ultimately have "wf_prog ?B P" by(rule wf_prog_lift)
  hence "wf_jvm_prog⇘P" by (simp add: wf_jvm_prog_phi_def)
  thus ?thesis by (unfold wf_jvm_prog_def) blast
qed
(*>*)

theorem jvm_lbv_complete:
  assumes wt: "wf_jvm_prog⇘ΦP" 
  shows "wt_jvm_prog_lbv P (prg_cert P Φ)"
(*<*)
proof -
  let ?cert = "prg_cert P Φ"
  let ?A = "λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). 
                wt_method P C b Ts Tr mxs mxl0 is xt (Φ C M)"
  let ?B = "λP C (mn,b,Ts,Tr,(mxs,mxl0,ins,et)).
                wt_lbv P C b Ts Tr mxs mxl0 et (?cert C mn) ins"

  from wt have "wf_prog ?A P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
  moreover {
    fix wf_md C M b Ts Ca T m bd
    assume ass1: "wf_prog wf_md P" and sees: "P  Ca sees M, b :  TsT = m in Ca" and
           ass2: "set Ts  types P" and ass3: "bd = (M, b, Ts, T, m)" and
           ass4: "?A P Ca bd"
    from ass3 ass4 have stab: "b = Static  b = NonStatic" by (simp add:wt_method_def)
    from ass1 sees ass2 ass3 ass4 have "?B P Ca bd" using sees_method_is_class[OF sees]  
      by (auto simp add: prg_cert_def 
               intro!: start_context.wt_method_wt_lbv start_context_intro_auxi[OF stab])
  }
  ultimately have "wf_prog ?B P" by(rule wf_prog_lift)
  thus "wt_jvm_prog_lbv P (prg_cert P Φ)" by (simp add: wt_jvm_prog_lbv_def)
qed
(*>*)

end