Theory BVExec

(*  Title:      JinjaDCI/BV/BVExec.thy

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

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

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

theory BVExec
imports Jinja.Abstract_BV TF_JVM Jinja.Typing_Framework_2
begin

definition kiljvm :: "jvm_prog  nat  nat  ty  
             instr list  ex_table  tyi' err list  tyi' err list"
where
  "kiljvm P mxs mxl Tr is xt 
  kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl) 
          (exec P mxs Tr xt is)"

definition wt_kildall :: "jvm_prog  cname  staticb  ty list  ty  nat  nat  
                 instr list  ex_table  bool"
where
  "wt_kildall P C' b Ts Tr mxs mxl0 is xt  (b = Static  b = NonStatic) 
   0 < size is   
   (let first  = Some ([],(case b of Static  [] | NonStatic  [OK (Class C')])
                            @(map OK Ts)@(replicate mxl0 Err));
        start  = (OK first)#(replicate (size is - 1) (OK None));
        result = kiljvm P mxs
                   ((case b of Static  0 | NonStatic  1)+size Ts+mxl0)
                     Tr is xt start
    in n < size is. result!n  Err)"

definition wf_jvm_progk :: "jvm_prog  bool"
where
  "wf_jvm_progk P 
  wf_prog (λP C' (M,b,Ts,Tr,(mxs,mxl0,is,xt)). wt_kildall P C' b Ts Tr mxs mxl0 is xt) P"


context start_context
begin

lemma Cons_less_Conss3 [simp]:
  "x#xs [⊏⇘r⇙] y#ys = (x ⊏⇘ry  xs [⊑⇘r⇙] ys  x = y  xs [⊏⇘r⇙] ys)"
  apply (unfold lesssub_def )
  apply auto
  apply (insert sup_state_opt_err)
  apply (unfold lesssub_def lesub_def sup_state_opt_def sup_state_def sup_ty_opt_def)
  apply (simp only: JVM_le_unfold )
  apply fastforce
  done

lemma acc_le_listI3 [intro!]:
  " acc r  acc (Listn.le r)"
apply (unfold acc_def)
apply (subgoal_tac
 "wf(UN n. {(ys,xs). size xs = n  size ys = n  xs <_(Listn.le r) ys})")
   apply (erule wf_subset)
 apply (blast intro: lesssub_lengthD)
apply (rule wf_UN)
 prefer 2
 apply (rename_tac m n)
 apply (case_tac "m=n")
  apply simp
 apply (fast intro!: equals0I dest: not_sym)
apply (rename_tac n)
apply (induct_tac n)
 apply (simp add: lesssub_def cong: conj_cong)
apply (rename_tac k)
apply (simp add: wf_eq_minimal del: r_def f_def step_def A_def)
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong del: r_def f_def step_def A_def)
apply clarify
apply (rename_tac M m)
apply (case_tac "x xs. size xs = k  x#xs  M")
 prefer 2
 apply (erule thin_rl)
 apply (erule thin_rl)
 apply blast
apply (erule_tac x = "{a. xs. size xs = k  a#xs:M}" in allE)
apply (erule impE)
 apply blast
apply (thin_tac "x xs. P x xs" for P)
apply clarify
apply (rename_tac maxA xs)
apply (erule_tac x = "{ys. size ys = size xs  maxA#ys  M}" in allE)
apply (erule impE)
 apply blast
apply clarify
apply (thin_tac "m  M")
apply (thin_tac "maxA#xs  M")
apply (rule bexI)
 prefer 2
 apply assumption
apply clarify
apply (simp del: r_def f_def step_def A_def)
apply blast
  done


lemma wf_jvm: " wf {(ss', ss). ss [⊏⇘r⇙] ss'}"
  apply (insert acc_le_listI3 acc_JVM [OF wf])
  by (simp add: acc_def r_def) 

lemma iter_properties_bv[rule_format]:
shows " pw0. p < n; ss0  nlists n A; p<n. p  w0  stable r step ss0 p  
         iter f step ss0 w0 = (ss',w') 
         ss'  nlists n A  stables r step ss'  ss0 [⊑⇩r] ss' 
         (tsnlists n A. ss0 [⊑⇩r] ts  stables r step ts  ss' [⊑⇩r] ts)"
(*<*) (is "PROP ?P")

proof -
  show "PROP ?P"
    apply (insert semi bounded_step exec_pres_type step_mono[OF wf])  
    apply (unfold iter_def stables_def)

    apply (rule_tac P = "λ(ss,w).
                ss  nlists n A  (p<n. p  w  stable r step ss p)  ss0 [⊑⇩r] ss 
   (tsnlists n A. ss0 [⊑⇩r] ts  stables r step ts  ss [⊑⇩r] ts) 
   (pw. p < n)" and
   r = "{(ss',ss) . ss [⊏⇩r] ss'} <*lex*> finite_psubset"
         in while_rule)

  ― ‹Invariant holds initially:›  
        apply (simp add:stables_def  semilat_Def   del: n_def A_def r_def f_def step_def)
        apply (blast intro:le_list_refl')     
   
  ― ‹Invariant is preserved:›
       apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def n_def)
       apply(rename_tac ss w)
       apply(subgoal_tac "(SOME p. p  w)  w")
        prefer 2 apply (fast intro: someI)
       apply(subgoal_tac "(q,t)  set (step (SOME p. p  w) (ss ! (SOME p. p  w))). q < length ss  t  A")
        prefer 2
        apply clarify
        apply (rule conjI)
         apply(clarsimp, blast dest!: boundedD)
        apply (subgoal_tac "(SOME p. p  w) < n")
         apply (subgoal_tac "(ss ! (SOME p. p  w))  A")
          apply (fastforce simp only:n_def dest:pres_typeD )   
         apply simp
        apply simp
       apply (subst decomp_propa)
        apply blast
       apply (simp del:A_def r_def f_def step_def n_def)
       apply (rule conjI)
        apply (rule Semilat.merges_preserves_type[OF Semilat.intro, OF semi])
         apply blast
        apply clarify
        apply (rule conjI)
         apply(clarsimp, blast dest!: boundedD)
        apply (erule pres_typeD)
          prefer 3
          apply assumption
         apply (erule nlistsE_nth_in)
         apply blast
        apply (simp only:n_def)
       apply (rule conjI)
        apply clarify
        apply (subgoal_tac "ss  nlists (length is) A" "pw. p <  (length is) " "p<(length is). p  w  stable r step ss p "
 "p < length is")
            apply (blast   intro!: Semilat.stable_pres_lemma[OF Semilat.intro, OF semi])
           apply (simp only:n_def)
          apply (simp only:n_def)
         apply (simp only:n_def)
        apply (simp only:n_def)
       apply (rule conjI)
        apply (subgoal_tac "ss  nlists (length is) A" 
               "(q,t)set (step (SOME p. p  w) (ss ! (SOME p. p  w))). q < length is  t  A"
               "ss [⊑⇘r⇙] merges f (step (SOME p. p  w) (ss ! (SOME p. p  w))) ss" "ss0 nlists (size is) A"
               "merges f (step (SOME p. p  w) (ss ! (SOME p. p  w))) ss  nlists (size is) A" 
               "ss nlists (size is) A" "order r A" "ss0 [⊑⇘r⇙] ss ")
                apply (blast dest: le_list_trans)
               apply simp
              apply (simp only:semilat_Def)
             apply (simp only:n_def)
            apply (fastforce simp only: n_def dest:Semilat.merges_preserves_type[OF Semilat.intro, OF semi] )
           apply (simp only:n_def)
          apply (blast intro:Semilat.merges_incr[OF Semilat.intro, OF semi])
         apply (subgoal_tac "length ss = n")
          apply (simp only:n_def)
         apply (subgoal_tac "ss nlists n A")
          defer
          apply simp
         apply (simp only:n_def)
        prefer 5
        apply (simp only:nlistsE_length n_def)
       apply(rule conjI)
        apply (clarsimp simp del: A_def r_def f_def step_def)
        apply (blast intro!: Semilat.merges_bounded_lemma[OF Semilat.intro, OF semi])       
       apply (subgoal_tac "bounded step n")
        apply (blast dest!: boundedD)
       apply (simp only:n_def)

  ― ‹Postcondition holds upon termination:›
      apply(clarsimp simp add: stables_def split_paired_all)
  
  ― ‹Well-foundedness of the termination relation:›    
      apply (rule wf_lex_prod)
     apply (simp only:wf_jvm) 
    apply (rule wf_finite_psubset) 

  ― ‹Loop decreases along termination relation:›
     apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def)
     apply(rename_tac ss w)
     apply(subgoal_tac "(SOME p. p  w)  w")
      prefer 2 apply (fast intro: someI)
     apply(subgoal_tac "(q,t)  set (step (SOME p. p  w) (ss ! (SOME p. p  w))). q < length ss  t  A")
      prefer 2
      apply clarify
      apply (rule conjI)
       apply(clarsimp, blast dest!: boundedD)
      apply (erule pres_typeD)
        prefer 3
        apply assumption
       apply (erule nlistsE_nth_in)
       apply blast
      apply blast
     apply (subst decomp_propa)
      apply blast
     apply clarify
  apply (simp del: nlistsE_length  A_def r_def f_def step_def
      add: lex_prod_def finite_psubset_def 
           bounded_nat_set_is_finite)
     apply (rule termination_lemma)
        apply (insert Semilat.intro)
        apply assumption+
      defer
      apply assumption
     defer
     apply clarsimp   
    done
qed

(*>*)


lemma kildall_properties_bv: 
shows " ss0  nlists n A  
  kildall r f step ss0  nlists n A 
  stables r step (kildall r f step ss0) 
  ss0 [⊑⇩r] kildall r f step ss0 
  (tsnlists n A. ss0 [⊑⇩r] ts  stables r step ts 
                 kildall r f step ss0 [⊑⇩r] ts)"
(*<*) (is "PROP ?P")
proof -
  show "PROP ?P"
  apply (unfold kildall_def)
    apply(case_tac "iter f step ss0 (unstables r step ss0)")
    apply (simp del:r_def f_def n_def step_def A_def)
    apply (rule iter_properties_bv)      
     apply (simp_all add: unstables_def stable_def)
    done
qed

end

theorem (in start_context) is_bcv_kiljvm:
  "is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
(*<*)
  apply (insert wf)
  apply (unfold kiljvm_def)
  apply (fold r_def f_def step_def_exec n_def)
  apply(unfold is_bcv_def wt_step_def)
  apply(insert semi  kildall_properties_bv)
  apply(simp only:stables_def)
  apply clarify
  apply(subgoal_tac "kildall r f step τs0  nlists n A")
   prefer 2
   apply (fastforce intro: kildall_properties_bv)
  apply (rule iffI)
   apply (rule_tac x = "kildall r f step τs0" in bexI) 
    apply (rule conjI)
     apply (fastforce intro: kildall_properties_bv)
  apply (force intro: kildall_properties_bv)
   apply simp
  apply clarify
  apply(subgoal_tac "kildall r f step τs0!pa <=_r τs!pa")
   defer
   apply (blast intro!: le_listD less_lengthI)
  apply (subgoal_tac "τs!pa  Err")
   defer
   apply simp
  apply (rule ccontr)
  apply (simp only:top_def r_def JVM_le_unfold)
  apply fastforce
  done
(*
proof -
  let ?n = "length is"
  have "Semilat A r f" using semilat_JVM[OF wf]
    by (simp add: Semilat.intro sl_def2)
  moreover have "acc r" using wf by simp blast
  moreover have "top r Err" by (simp add: JVM_le_unfold)
  moreover have "pres_type step ?n A" by (rule exec_pres_type)
  moreover have "bounded step ?n" by (rule bounded_step)
  moreover have "mono r step ?n A" using step_mono[OF wf] by simp
  ultimately have "is_bcv r Err step ?n A (kildall r f step)"
    by(rule is_bcv_kildall)
  moreover have kileq: "kiljvm P mxs mxl Tr is xt = kildall r f step"
    using f_def kiljvm_def r_def step_def_exec by blast
  ultimately show ?thesis by simp
qed
*)
(*>*)

(* FIXME: move? *)
lemma subset_replicate [intro?]: "set (replicate n x)  {x}"
  by (induct n) auto

lemma in_set_replicate:
  assumes "x  set (replicate n y)"
  shows "x = y"
(*<*)
proof -
  note assms
  also have "set (replicate n y)  {y}" ..
  finally show ?thesis by simp
qed
(*>*)

lemma (in start_context) start_in_A [intro?]:
  "0 < size is  start  nlists (size is) A"
  using Ts C
(*<*)
proof(cases b)
qed (force simp: JVM_states_unfold intro!: nlistsI nlists_appendI
           dest!: in_set_replicate)+
(*>*)


theorem (in start_context) wt_kil_correct:
  assumes wtk: "wt_kildall P C b Ts Tr mxs mxl0 is xt"
  shows "τs. wt_method P C b Ts Tr mxs mxl0 is xt τs"
(*<*)
proof -
  from wtk obtain res where    
    result:   "res = kiljvm P mxs mxl Tr is xt start" and
    success:  "n < size is. res!n  Err" and
    instrs:   "0 < size is" and
    stab:     "b = Static  b = NonStatic" 
    by (unfold wt_kildall_def) simp
      
  have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
    by (rule is_bcv_kiljvm)
    
  from instrs have "start  nlists (size is) A" ..
  with bcv success result have 
    "tsnlists (size is) A. start [⊑⇩r] ts  wt_step r Err step ts"
    by (unfold is_bcv_def) blast
  then obtain τs' where
    in_A: "τs'  nlists (size is) A" and
    s:    "start [⊑⇩r] τs'" and
    w:    "wt_step r Err step τs'"
    by blast
  hence wt_err_step: "wt_err_step (sup_state_opt P) step τs'"
    by (simp add: wt_err_step_def JVM_le_Err_conv)

  from in_A have l: "size τs' = size is" by simp  
  moreover {
    from in_A  have "check_types P mxs mxl τs'" by (simp add: check_types_def)
    also from w have "x  set τs'. x  Err" 
      by (auto simp add: wt_step_def all_set_conv_all_nth)
    hence [symmetric]: "map OK (map ok_val τs') = τs'" 
      by (auto intro!: map_idI simp add: wt_step_def)
    finally  have "check_types P mxs mxl (map OK (map ok_val τs'))" .
  } 
  moreover {  
    from s have "start!0 ⊑⇩r τs'!0" by (rule le_listD) simp
    moreover
    from instrs w l 
    have "τs'!0  Err" by (unfold wt_step_def) simp
    then obtain τs0 where "τs'!0 = OK τs0" by auto
    ultimately
    have "wt_start P C b Ts mxl0 (map ok_val τs')" using l instrs
      by (unfold wt_start_def) 
         (cases b; simp add: lesub_def JVM_le_Err_conv Err.le_def)
  }
  moreover 
  from in_A have "set τs'  A" by simp  
  with wt_err_step bounded_step
  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: l)
  ultimately
  have "wt_method P C b Ts Tr mxs mxl0 is xt (map ok_val τs')"
    using instrs stab by (simp add: wt_method_def2 check_types_def del: map_map)
  thus ?thesis by blast
qed
(*>*)


theorem (in start_context) wt_kil_complete:
  assumes wtm: "wt_method P C b Ts Tr mxs mxl0 is xt τs"
  shows "wt_kildall P C b Ts Tr mxs mxl0 is xt"
(*<*)
proof -
  from wtm obtain
    instrs:   "0 < size is" and
    length:   "length τs = length is" and 
    ck_type:  "check_types P mxs mxl (map OK τ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"  and
    stab: "b = Static  b = NonStatic" 
    by (simp add: wt_method_def2 check_types_def )

  from ck_type
  have in_A: "set (map OK τs)  A" 
    by (simp add: check_types_def)  
  with app_eff in_A bounded_step
  have "wt_err_step (sup_state_opt P) (err_step (size τs) app eff) (map OK τs)"
    by - (erule wt_app_eff_imp_wt_err,
          auto simp add: exec_def length states_def)
  hence wt_err: "wt_err_step (sup_state_opt P) step (map OK τs)" 
    by (simp add: length)
  have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
    by (rule is_bcv_kiljvm)
  moreover from instrs have "start  nlists (size is) A" ..
  moreover
  let ?τs = "map OK τs"  
  have less_τs: "start [⊑⇩r] ?τs"
  proof (rule le_listI)
    from length instrs
    show "length start = length (map OK τs)" by simp
  next
    fix n
    from wt_start have "P  ok_val (start!0) ≤' τs!0" 
      by (cases b; simp add: wt_start_def)
    moreover from instrs length have "0 < length τs" by simp
    ultimately have "start!0 ⊑⇩r ?τs!0" 
      by (simp add: JVM_le_Err_conv lesub_def)
    moreover {
      fix n'
      have "OK None ⊑⇩r ?τs!n"
        by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
                 split: err.splits)
      hence "n = Suc n'; n < size start  start!n ⊑⇩r ?τs!n" by simp
    }
    ultimately
    show "n < size start  start!n ⊑⇩r ?τs!n" by (cases n, blast+)   
  qed
  moreover
  from ck_type length
  have "?τs  nlists (size is) A"
    by (auto intro!: nlistsI simp add: check_types_def)
  moreover
  from wt_err have "wt_step r Err step ?τs" 
    by (simp add: wt_err_step_def JVM_le_Err_conv)
  ultimately
  have "p. p < size is  kiljvm P  mxs mxl Tr is xt start ! p  Err" 
    by (unfold is_bcv_def) blast
  with instrs 
  show "wt_kildall P C b Ts Tr mxs mxl0 is xt" 
    using start_context_intro_auxi[OF staticb] using stab by (unfold wt_kildall_def) simp
qed
(*>*)


theorem jvm_kildall_correct:
  "wf_jvm_progk P = wf_jvm_prog P"
(*<*)
proof -
  let  = "λC M. let (C,b,Ts,Tr,(mxs,mxl0,is,xt)) = method P C M in 
              SOME τs. wt_method P C b Ts Tr mxs mxl0 is xt τs"
  let ?A = "λP C' (M, b, Ts, Tr, mxs, mxl0, is, xt). wt_kildall P C' b Ts Tr mxs mxl0 is xt"
  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))"

  show ?thesis proof(rule iffI)
    ― ‹soundness›
    assume wt: "wf_jvm_progk P"
    then have wt': "wf_prog ?A P" by(simp add: wf_jvm_progk_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_kildall_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_kil_correct[OF start_context_intro_auxi[OF stab]]
                 intro: someI)
    }
    ultimately have "wf_prog (?BΦ ) P" by(rule wf_prog_lift)
    then have "wf_jvm_prog⇘P" by (simp add: wf_jvm_prog_phi_def)
    thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
  next  
    ― ‹completeness›
    
    assume wt: "wf_jvm_prog P" 
    then obtain Φ where "wf_prog (?BΦ Φ) 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: "(?BΦ Φ) 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 "?A P Ca bd" using sees_method_is_class[OF sees] using JVM_sl.staticb
        by (auto intro!: start_context.wt_kil_complete start_context_intro_auxi[OF stab])
    }
    ultimately have "wf_prog ?A P" by(rule wf_prog_lift)
    thus "wf_jvm_progk P" by (simp add: wf_jvm_progk_def)
  qed
qed
(*>*)

end