Theory TF_JVM

(*  Title:      JinjaDCI/BV/TF_JVM.thy

    Author:     Tobias Nipkow, Gerwin Klein, Susannah Mansky
    Copyright   2000 TUM, 2019-20 UIUC

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

section ‹ The Typing Framework for the JVM \label{sec:JVM} ›

theory TF_JVM
imports Jinja.Typing_Framework_err EffectMono BVSpec
begin

definition exec :: "jvm_prog ⇒ nat ⇒ ty ⇒ ex_table ⇒ instr list ⇒ ty⇩i' err step_type"
where 
  "exec G maxs rT et bs ≡
  err_step (size bs) (λpc. app (bs!pc) G maxs rT pc (size bs) et) 
                     (λpc. eff (bs!pc) G pc et)"

locale JVM_sl =
  fixes P :: jvm_prog and mxs and mxl⇩0 and n
  fixes b and Ts :: "ty list" and "is" and xt and T⇩r

  fixes mxl and A and r and f and app and eff and step
  defines [simp]: "mxl ≡ (case b of Static ⇒ 0 | NonStatic ⇒ 1)+size Ts+mxl⇩0"
  defines [simp]: "A   ≡ states P mxs mxl"
  defines [simp]: "r   ≡ JVM_SemiType.le P mxs mxl"
  defines [simp]: "f   ≡ JVM_SemiType.sup P mxs mxl"

  defines [simp]: "app ≡ λpc. Effect.app (is!pc) P mxs T⇩r pc (size is) xt"
  defines [simp]: "eff ≡ λpc. Effect.eff (is!pc) P pc xt"
  defines [simp]: "step ≡ err_step (size is) app eff"

  defines [simp]: "n ≡ size is"
  assumes staticb: "b = Static ∨ b = NonStatic" 

locale start_context = JVM_sl +
  fixes p and C

  assumes wf: "wf_prog p P"
  assumes C:  "is_class P C"
  assumes Ts: "set Ts ⊆ types P"

 
  fixes first :: ty⇩i' and start
  defines [simp]: 
  "first ≡ Some ([],(case b of Static ⇒ [] | NonStatic ⇒ [OK (Class C)]) @ map OK Ts @ replicate mxl⇩0 Err)"
  defines [simp]:
  "start ≡ (OK first) #  replicate (size is - 1) (OK None)"
thm start_context.intro

lemma start_context_intro_auxi: 
  fixes  P b Ts p C
  assumes "b = Static ∨ b = NonStatic " 
      and "wf_prog p P"
      and "is_class P C"
      and "set Ts ⊆ types P"
    shows " start_context P b Ts p C"
  using start_context.intro[OF JVM_sl.intro] start_context_axioms_def assms  by auto

subsection ‹ Connecting JVM and Framework ›

lemma (in start_context) semi: "semilat (A, r, f)"
  apply (insert semilat_JVM[OF wf])
  apply (unfold A_def r_def f_def JVM_SemiType.le_def JVM_SemiType.sup_def states_def)
  apply auto
  done


lemma (in JVM_sl) step_def_exec: "step ≡ exec P mxs T⇩r xt is" 
  by (simp add: exec_def)  

lemma special_ex_swap_lemma [iff]: 
  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
  by blast

lemma ex_in_list [iff]:
  "(∃n. ST ∈ nlists n A ∧ n ≤ mxs) = (set ST ⊆ A ∧ size ST ≤ mxs)"
  by (unfold nlists_def) auto

lemma singleton_nlists: 
  "(∃n. [Class C] ∈ nlists n (types P) ∧ n ≤ mxs) = (is_class P C ∧ 0 < mxs)"
  by auto

lemma set_drop_subset:
  "set xs ⊆ A ⟹ set (drop n xs) ⊆ A"
  by (auto dest: in_set_dropD)

lemma Suc_minus_minus_le:
  "n < mxs ⟹ Suc (n - (n - b)) ≤ mxs"
  by arith

lemma in_nlistsE:
  "⟦ xs ∈ nlists n A; ⟦size xs = n; set xs ⊆ A⟧ ⟹ P ⟧ ⟹ P"
  by (unfold nlists_def) blast

declare is_relevant_entry_def [simp]
declare set_drop_subset [simp]

theorem (in start_context) exec_pres_type:
  "pres_type step (size is) A"
(*<*)
proof -
  let ?n = "size is" and ?app = app and ?step = eff
  let ?mxl = "(case b of Static ⇒ 0 | NonStatic ⇒ 1) + length Ts + mxl⇩0"
  let ?A = "opt((Union {nlists n (types P) |n. n <= mxs}) ×
                                 nlists ?mxl (err(types P)))"
  have "pres_type (err_step ?n ?app ?step) ?n (err ?A)"
  proof(rule pres_type_lift)
    have "⋀s pc pc' s'. s∈?A ⟹ pc < ?n ⟹ ?app pc s
             ⟹ (pc', s')∈set (?step pc s) ⟹ s' ∈ ?A"
    proof -
      fix s pc pc' s'
      assume asms: "s∈?A" "pc < ?n" "?app pc s" "(pc', s')∈set (?step pc s)"
      show "s' ∈ ?A"
      proof(cases s)
        case None
        then show ?thesis using asms by (fastforce dest: effNone)
      next
        case (Some ab)
        then show ?thesis using asms proof(cases "is!pc")
          case Load
          then show ?thesis using asms
            by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                                xcpt_eff_def norm_eff_def
                          dest: nlistsE_nth_in)
        next
          case Push
          then show ?thesis using asms Some
            by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                xcpt_eff_def norm_eff_def typeof_lit_is_type)
        next
          case Getfield
          then show ?thesis using asms wf
            by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                xcpt_eff_def norm_eff_def
                          dest: sees_field_is_type)
        next
          case Getstatic
          then show ?thesis using asms wf
            by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                xcpt_eff_def norm_eff_def
                          dest: sees_field_is_type)
        next
          case (Invoke M n)
          obtain a b where [simp]: "s = ⌊(a,b)⌋" using Some asms(1) by blast
          show ?thesis
          proof(cases "a!n = NT")
            case True
            then show ?thesis using Invoke asms wf
              by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                                  xcpt_eff_def norm_eff_def)
          next
            case False
            have "(pc', s') ∈ set (norm_eff (Invoke M n) P pc (a, b)) ∨
              (pc', s') ∈ set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
              using Invoke asms(4) by (simp add: Effect.eff_def)
            then show ?thesis proof(rule disjE)
              assume "(pc', s') ∈ set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
              then show ?thesis using Invoke asms(1-3)
                by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
            next
              assume norm: "(pc', s') ∈ set (norm_eff (Invoke M n) P pc (a, b))"
              also have "Suc (length a - Suc n) ≤ mxs" using Invoke asms(1,3)
                by (simp add: Effect.app_def xcpt_app_def) arith
              ultimately show ?thesis using False Invoke asms(1-3) wf
                by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
                         dest!: sees_wf_mdecl)
            qed
          qed
        next
          case (Invokestatic C M n)
          obtain a b where [simp]: "s = ⌊(a,b)⌋" using Some asms(1) by blast
          have "(pc', s') ∈ set (norm_eff (Invokestatic C M n) P pc (a, b)) ∨
            (pc', s') ∈ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
            using Invokestatic asms(4) by (simp add: Effect.eff_def)
          then show ?thesis proof(rule disjE)
            assume "(pc', s') ∈ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
            then show ?thesis using Invokestatic asms(1-3)
              by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
          next
            assume norm: "(pc', s') ∈ set (norm_eff (Invokestatic C M n) P pc (a, b))"
            also have "Suc (length a - Suc n) ≤ mxs" using Invokestatic asms(1,3)
              by (simp add: Effect.app_def xcpt_app_def) arith
            ultimately show ?thesis using Invokestatic asms(1-3) wf
              by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
                       dest!: sees_wf_mdecl)
          qed
        qed (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                             xcpt_eff_def norm_eff_def)+
      qed
    qed
    then show "∀s∈?A. ∀p. p < ?n ⟶ ?app p s ⟶ (∀(q, s')∈set (?step p s). s' ∈ ?A)"
      by clarsimp
  qed
  then show ?thesis by (simp add: JVM_states_unfold)
qed
(*>*)

declare is_relevant_entry_def [simp del]
declare set_drop_subset [simp del]

lemma lesubstep_type_simple:
  "xs [⊑⇘Product.le (=) r⇙] ys ⟹ set xs {⊑⇘r⇙} set ys"
(*<*)
proof -
  assume assm: "xs [⊑⇘Product.le (=) r⇙] ys"
  have "⋀a b i y. (a, b) = xs ! i ⟹ i < length xs
     ⟹ ∃τ'. (∃i. (a, τ') = ys ! i ∧ i < length xs) ∧ b ⊑⇘r⇙ τ'"
  proof -
    fix a b i assume ith: "(a, b) = xs ! i" and len: "i < length xs"
    obtain τ where "ys ! i = (a, τ) ∧ r b τ"
      using le_listD[OF assm len] ith
      by (clarsimp simp: lesub_def Product.le_def)
    then have "(a, τ) = ys ! i ∧ b ⊑⇘r⇙ τ"
      by (clarsimp simp: lesub_def)
    with len show "∃τ'. (∃i. (a, τ') = ys ! i ∧ i < length xs) ∧ b ⊑⇘r⇙ τ'"
      by fastforce
  qed
  then show "set xs {⊑⇘r⇙} set ys" using assm
    by (clarsimp simp: lesubstep_type_def set_conv_nth)
qed
(*>*)

declare is_relevant_entry_def [simp del]


lemma conjI2: "⟦ A; A ⟹ B ⟧ ⟹ A ∧ B" by blast
  
lemma (in JVM_sl) eff_mono:
assumes wf: "wf_prog p P" and "pc < length is" and
  lesub: "s ⊑⇘sup_state_opt P⇙ t" and app: "app pc t"
shows "set (eff pc s) {⊑⇘sup_state_opt P⇙} set (eff pc t)"
(*<*)
proof(cases t)
  case None then show ?thesis using lesub
   by (simp add: Effect.eff_def lesub_def)
next
  case tSome: (Some a)
  show ?thesis proof(cases s)
    case None then show ?thesis using lesub
     by (simp add: Effect.eff_def lesub_def)
  next
    case (Some b)
    let ?norm = "λx. norm_eff (is ! pc) P pc x"
    let ?xcpt = "λx. xcpt_eff (is ! pc) P pc x xt"
    let ?r = "Product.le (=) (sup_state_opt P)"
    let ?τ' = "⌊eff⇩i (is ! pc, P, a)⌋"
    {
      fix x assume xb: "x ∈ set (succs (is ! pc) b pc)"
      then have appi: "app⇩i (is ! pc, P, pc, mxs, T⇩r, a)" and
                bia: "P ⊢ b ≤⇩i a" and appa: "app pc ⌊a⌋"
        using lesub app tSome Some by (auto simp add: lesub_def Effect.app_def)
      have xa: "x ∈ set (succs (is ! pc) a pc)"
        using xb succs_mono[OF wf appi bia] by auto
      then have "(x, ?τ') ∈ (λpc'. (pc', ?τ')) ` set (succs (is ! pc) a pc)"
        by (rule imageI)
      moreover have "P ⊢ ⌊eff⇩i (is ! pc, P, b)⌋ ≤' ?τ'"
        using xb xa eff⇩i_mono[OF wf bia] appa by fastforce
      ultimately have "∃τ'. (x, τ') ∈ (λpc'. (pc', ⌊eff⇩i (is ! pc, P, a)⌋)) ` set (succs (is ! pc) a pc) ∧
              P ⊢ ⌊eff⇩i (is ! pc, P, b)⌋ ≤' τ'" by blast
    }
    then have norm: "set (?norm b) {⊑⇘sup_state_opt P⇙} set (?norm a)"
      using tSome Some by (clarsimp simp: norm_eff_def lesubstep_type_def lesub_def)
    obtain a1 b1 a2 b2 where a: "a = (a1, b1)" and b: "b = (a2, b2)"
      using tSome Some by fastforce
    then have a12: "size a2 = size a1" using lesub tSome Some
      by (clarsimp simp: lesub_def list_all2_lengthD)
    have "length (?xcpt b) = length (?xcpt a)"
      by (simp add: xcpt_eff_def split_beta)
    moreover have "⋀n. n < length (?xcpt b) ⟹ (?xcpt b) ! n ⊑⇘?r⇙ (?xcpt a) ! n"
      using lesub tSome Some a b a12
      by (simp add: xcpt_eff_def split_beta fun_of_def) (simp add: lesub_def)
    ultimately have "?xcpt b [⊑⇘?r⇙] ?xcpt a"
      by(rule le_listI)
    then have "set (?xcpt b) {⊑⇘sup_state_opt P⇙} set (?xcpt a)"
      by (rule lesubstep_type_simple)
    moreover note norm
    ultimately have
     "set (?norm b) ∪ set (?xcpt b) {⊑⇘sup_state_opt P⇙} set (?norm a) ∪ set (?xcpt a)"
      by(intro lesubstep_union)
    then show ?thesis using tSome Some by(simp add: Effect.eff_def)
  qed
qed
(*>*)

lemma (in JVM_sl) bounded_step: "bounded step (size is)"
(*<*)
  by (auto simp: bounded_def err_step_def Effect.app_def Effect.eff_def
                 error_def map_snd_def
          split: err.splits option.splits)
(*>*)

theorem (in JVM_sl) step_mono:
  "wf_prog wf_mb P ⟹ mono r step (size is) A"
(*<*)
 apply (simp add: JVM_le_Err_conv)  
  apply (insert bounded_step)
  apply (unfold JVM_states_unfold)
  apply (rule mono_lift)    
  apply (subgoal_tac "b = Static ∨ b = NonStatic") 
      apply (fastforce split:if_splits)―‹ order_sup_state_opt' order_sup_state_opt'' ›
     apply (simp only:staticb)
     apply (unfold app_mono_def lesub_def)
    apply clarsimp
    apply (erule (2) app_mono)
   apply simp
  apply clarify
  apply (drule eff_mono)
      apply (auto simp add: lesub_def)
  done
(*
proof -
  assume wf: "wf_prog wf_mb P"
  let ?r = "sup_state_opt P" and ?n = "length is" and ?app = app and ?step = eff
  let ?A = "opt (⋃ {list n (types P) |n. n ≤ mxs} ×
                list ((case b of Static ⇒ 0 | NonStatic ⇒ 1) + length Ts + mxl⇩0)
                 (err (types P)))"
  have "order ?r ?A" using wf by simp
  moreover have "app_mono ?r ?app ?n ?A" using app_mono[OF wf]
    by (clarsimp simp: app_mono_def lesub_def)
  moreover have "bounded (err_step ?n ?app ?step) ?n" using bounded_step
    by simp
  moreover have "∀s p t. s ∈ ?A ∧ p < ?n ∧ s ⊑⇘?r⇙ t ⟶
   ?app p t ⟶ set (?step p s) {⊑⇘?r⇙} set (?step p t)"
     using eff_mono[OF wf] by simp
  ultimately have "mono (Err.le ?r) (err_step ?n ?app ?step) ?n (err ?A)"
    by(rule mono_lift)
  then show "mono r step (size is) A" using bounded_step
    by (simp add: JVM_le_Err_conv JVM_states_unfold)
qed
*)
(*>*)


lemma (in start_context) first_in_A [iff]: "OK first ∈ A"
  using Ts C by (cases b; force intro!: nlists_appendI simp add: JVM_states_unfold)


lemma (in JVM_sl) wt_method_def2:
  "wt_method P C' b Ts T⇩r mxs mxl⇩0 is xt τs =
  (is ≠ [] ∧ 
   (b = Static ∨ b = NonStatic) ∧
   size τs = size is ∧
   OK ` set τs ⊆ states P mxs mxl ∧
   wt_start P C' b Ts mxl⇩0 τs ∧ 
   wt_app_eff (sup_state_opt P) app eff τs)"
(*<*)using staticb
  by (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def
             check_types_def) auto
(*>*)


end