Impressum BVExec.thy

(*  Title:      HOL/MicroJava/BV/JVM.thy

    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

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

theory BVExec
imports "../DFA/Abstract_BV" TF_JVM "../DFA/Typing_Framework_2"
begin

definition kiljvm :: "jvm_prog ==> nat ==> nat ==> ty ==>
             instr list ==> ex_table ==> ty_i' err list ==> ty_i' err list"
where
  "kiljvm P mxs mxl T_r is xt ≡
  kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
          (exec P mxs T_r xt is)"

definition wt_kildall :: "jvm_prog ==> cname ==> ty list ==> ty ==> nat ==> nat ==>
                 instr list ==> ex_table ==> bool"
where
  "wt_kildall P C' Ts T_r mxs mxl₀ is xt ≡
   0 < size is ∧
   (let first = Some ([],[OK (Class C')]@(map OK Ts)@(replicate mxl₀ Err));
        start = OK first#(replicate (size is - 1) (OK None));
        result = kiljvm P mxs (1+size Ts+mxl₀) T_r is xt start
    in ∀n < size is. result!n ≠ Err)"

definition wf_jvm_prog_k :: "jvm_prog ==> bool"
where
  "wf_jvm_prog_k P ≡
  wf_prog (λP C' (M,Ts,T_r,(mxs,mxl₀,is,xt)). wt_kildall P C' Ts T_r mxs mxl₀ is xt) P"

context start_context
begin

lemma Cons_less_Conss3 [simp]:
  "x#xs [⊏] y#ys = (x ⊏ y ∧ xs [⊑] ys ∨ x = y ∧ xs [⊏] ys)"
  unfolding lesssub_def r_def
  by (metis JVM_le_Err_conv lesub_def sup_state_opt_err Cons_le_Cons list.inject)

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 fastforce
  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 metis
  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
  using Cons_less_Conss3 by blast


lemma wf_jvm: " wf {(ss', ss). ss [⊏] ss'}"
  using Semilat.acc_def acc_le_listI3 local.wf r_def by blast

lemma iter_properties_bv[rule_format]:
  shows "[ ∀p∈w0. 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' ∧
         (∀ts∈nlists n A. ss0 [⊑_r] ts ∧ stables r step ts ⟶ ss' [⊑_r] ts)"
    (*<*)

  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 ∧
   (∀ts∈nlists n A. ss0 [⊑_r] ts ∧ stables r step ts ⟶ ss [⊑_r] ts) ∧
   (∀p∈w. 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 "∀(q,t) ∈ set (step (some_elem w) (ss ! (some_elem w))). q < length ss ∧ t ∈ A")
      prefer 2
      apply clarify
      apply (metis boundedD n_def nlistsE_length nlistsE_nth_in pres_typeD some_elem_nonempty)
     apply (subst decomp_propa)
      apply (metis bounded_def n_def nlistsE_length some_elem_def
      some_elem_nonempty)
     apply (simp del:A_def r_def f_def step_def n_def)
     apply (rule conjI)
      apply (metis Semilat.intro[of A r f] nlistsE_length[of _ n A]
      Semilat.merges_preserves_type[of A r f _ n
        "step (some_elem _) (_ ! some_elem _)"])
     apply (simp only:n_def)
     apply (rule conjI)
      apply clarify
      apply (smt (verit, best) Semilat.intro Semilat.stable_pres_lemma some_elem_nonempty)
     apply (rule conjI)
      apply (subgoal_tac "ss ∈ nlists (length is) A" 
      "∀(q,t)∈set (step (some_elem w) (ss ! (some_elem w))). q < length is ∧ t ∈ A"
      "ss [⊑] merges f (step (some_elem w) (ss ! (some_elem w))) ss" "ss0∈ nlists (size is) A"
      "merges f (step (some_elem w) (ss ! (some_elem w))) ss ∈ nlists (size is) A" 
      "ss ∈nlists (size is) A" "order r A" "ss0 [⊑] 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 (metis nlistsE_length)
       apply (simp only:n_def)
     apply(rule conjI)
      apply (clarsimp simp del: A_def r_def f_def step_def)
      apply (blast intro!: some_elem_nonempty Semilat.merges_bounded_lemma[OF Semilat.intro, OF semi])
  apply (smt (verit, best) Un_def case_prod_conv mem_Collect_eq nlists_def set_diff_eq)

― ‹Postcondition holds upon termination:›
    apply(clarsimp simp add: stables_def split_paired_all)

― ‹Well-foundedness of the termination relation:›
  using wf_finite_psubset wf_jvm apply blast  

― ‹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_elem w) ∈ w")
   prefer 2 apply (fast intro: some_elem_nonempty)
  apply(subgoal_tac "∀(q,t) ∈ set (step (some_elem w) (ss ! (some_elem w))). q < length ss ∧ t ∈ A")
   prefer 2
   apply clarify
   apply (metis boundedD nlistsE_length nlistsE_nth_in pres_typeD)
  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)
  by (intro termination_lemma [OF Semilat.intro], auto)

(*>*)


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 ∧
  (∀ts∈nlists n A. ss0 [⊑_r] ts ∧ stables r step ts ⟶
                 kildall r f step ss0 [⊑_r] ts)"
(*<*) 
  unfolding kildall_def
  by (smt (verit, ccfv_SIG) in_nlistsE iter_properties_bv mem_Collect_eq prod.collapse
      unstables_def)

end

lemma (in start_context) is_bcv_kiljvm: 
shows "is_bcv r Err step (size is) A (kiljvm P mxs mxl T_r is xt)" 
  using wf semi kildall_properties_bv
  unfolding kiljvm_def
  apply (fold r_def f_def step_def_exec n_def)
  apply(unfold is_bcv_def wt_step_def)
  unfolding stables_def
  by (metis Err_le_conv JVM_le_Err_conv le_listD nlistsE_length r_def)

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

lemma in_set_replicate:
  assumes "x ∈ set (replicate n y)"
  shows "x = y"
(*<*)
  using assms by force
(*>*)

lemma (in start_context) start_in_A [intro?]:
  "0 < size is ==> start ∈ nlists (size is) A"
  using Ts C
(*<*)
  apply (simp add: JVM_states_unfold) 
  apply (force intro!: nlistsI nlists_appendI dest!: in_set_replicate)
  done   
(*>*)


theorem (in start_context) wt_kil_correct:
  assumes wtk: "wt_kildall P C Ts T_r mxs mxl₀ is xt"
  shows "∃τs. wt_method P C Ts T_r mxs mxl₀ is xt τs"
(*<*)
proof -
  from wtk obtain res where    
    result:   "res = kiljvm P mxs mxl T_r is xt start" and
    success:  "∀n < size is. res!n ≠ Err" and
    instrs:   "0 < size is" 
    by (unfold wt_kildall_def) simp
      
  have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T_r is xt)"
    by (rule is_bcv_kiljvm)
    
  from instrs have "start ∈ nlists (size is) A" ..
  with bcv success result have 
    "∃ts∈nlists (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 Ts mxl₀ (map ok_val τs')" using l instrs
      by (unfold wt_start_def) 
         (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 Ts T_r mxs mxl₀ is xt (map ok_val τs')"
    using instrs 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 Ts T_r mxs mxl₀ is xt τs"
  shows "wt_kildall P C Ts T_r mxs mxl₀ 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 Ts mxl₀ τs" and
    app_eff:  "wt_app_eff (sup_state_opt P) app eff τs"
    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 T_r 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 (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 T_r is xt start ! p ≠ Err" 
    by (unfold is_bcv_def) blast
  with instrs 
  show "wt_kildall P C Ts T_r mxs mxl₀ is xt" by (unfold wt_kildall_def) simp
qed
(*>*)


theorem jvm_kildall_correct:
  "wf_jvm_prog_k P = wf_jvm_prog P"
(*<*)
proof 
  let ?Φ = "λC M. let (C,Ts,T_r,(mxs,mxl₀,is,xt)) = method P C M in
              SOME τs. wt_method P C Ts T_r mxs mxl₀ is xt τs"

  ― ‹soundness›
  assume wt: "wf_jvm_prog_k P"
  hence "wf_jvm_prog_Φ P"
    apply (unfold wf_jvm_prog_phi_def wf_jvm_prog_{k_def})    
    apply (erule wf_prog_lift)
    apply (auto dest!: start_context.wt_kil_correct [OF start_context.intro] 
                intro: someI)
    apply (erule sees_method_is_class)
    done
  thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
next
  ― ‹completeness›
  assume wt: "wf_jvm_prog P"
  thus "wf_jvm_prog_k P"
    apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_prog_{k_def})
    apply (clarify)
    apply (erule wf_prog_lift)
    apply (auto intro!: start_context.wt_kil_complete start_context.intro)
    apply (erule sees_method_is_class)
    done
qed
(*>*)

end