Session Regression_Test_Selection

Theory RTS_safe

(* Title: RTS/Common/RTS_safe.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Regression Test Selection algorithm model"

theory RTS_safe
imports Main
begin

text ‹ This describes an \emph{existence safe} RTS algorithm: if a test
 is deselected based on an output, there is SOME equivalent output
 under the changed program. ›
locale RTS_safe =
 fixes
  out :: "'prog  'test  'prog_out set" and
  equiv_out :: "'prog_out  'prog_out  bool" and
  deselect :: "'prog  'prog_out  'prog  bool" and
  progs :: "'prog set" and
  tests :: "'test set"
 assumes
  existence_safe: " P  progs; P'  progs; t  tests; o1  out P t; deselect P o1 P' 
    (o2  out P' t. equiv_out o1 o2)" and
  equiv_out_equiv: "equiv UNIV {(x,y). equiv_out x y}" and
  equiv_out_deselect: " equiv_out o1 o2; deselect P o1 P'   deselect P o2 P'"

context RTS_safe begin

lemma equiv_out_refl: "equiv_out a a"
using equiv_class_eq_iff equiv_out_equiv by fastforce

lemma equiv_out_trans: " equiv_out a b; equiv_out b c   equiv_out a c"
using equiv_class_eq_iff equiv_out_equiv by fastforce

text "This shows that it is safe to continue deselecting a test based
 on its output under a previous program, to an arbitrary number of
 program changes, as long as the test is continually deselected. This
 is useful because it means changed programs don't need to generate new
 outputs for deselected tests to ensure safety of future deselections."
lemma existence_safe_trans:
assumes Pst_in: "Ps  []" "set Ps  progs" "t  tests" and
 o0: "o0  out (Ps!0) t" and
 des: "n < (length Ps) - 1. deselect (Ps!n) o0 (Ps!(Suc n))"
shows "on  out (last Ps) t. equiv_out o0 on"
using assms proof(induct "length Ps" arbitrary: Ps)
  case 0 with Pst_in show ?case by simp
next
  case (Suc x) then show ?case
  proof(induct x)
  case z: 0
    from z.prems(2,3) have "Ps ! (length Ps - 2) = last Ps"
      by (simp add: last_conv_nth numeral_2_eq_2)
    with equiv_out_refl z.prems(2,6) show ?case by auto
  next
    case Suc':(Suc x')
    let ?Ps = "take (Suc x') Ps"
    have len': "Suc x' = length (take (Suc x') Ps)" using Suc'.prems(2) by auto
    moreover have nmt': "take (Suc x') Ps  []" using len' by auto
    moreover have sub': "set (take (Suc x') Ps)  progs" using Suc.prems(2)
      by (meson order_trans set_take_subset)
    moreover have "t  tests" using Pst_in(3) by simp
    moreover have "o0  out (take (Suc x') Ps ! 0) t" using Suc.prems(4) by simp
    moreover have "n<length (take (Suc x') Ps) - 1.
     deselect (take (Suc x') Ps ! n) o0 (take (Suc x') Ps ! (Suc n))"
      using Suc.prems(5) len' by simp
    ultimately have "o'out (last ?Ps) t. equiv_out o0 o'" by(rule Suc'.prems(1)[of ?Ps])
    then obtain o' where o': "o'  out (last ?Ps) t" and eo: "equiv_out o0 o'" by clarify
    from Suc.prems(1) Suc'.prems(2) len' nmt'
    have "last (take (Suc x') Ps) = Ps!x'" "last Ps = Ps!(Suc x')"
      by (metis diff_Suc_1 last_conv_nth lessI nth_take)+
    moreover have "x' < length Ps - 1" using Suc'.prems(2) by linarith
    ultimately have des':"deselect (last (take (Suc x') Ps)) o0 (last Ps)"
      using Suc.prems(5) by simp
    from Suc.prems(1,2) sub' nmt' last_in_set
    have Ps_in: "last (take (Suc x') Ps)  progs" "last Ps  progs" by blast+
    have "on  out (last Ps) t. equiv_out o' on"
      by(rule existence_safe[where P="last (take (Suc x') Ps)" and P'="last Ps" and t=t,
                    OF Ps_in Pst_in(3) o' equiv_out_deselect[OF eo des']])
    then obtain on where oN: "on  out (last Ps) t" and eo': "equiv_out o' on" by clarify
    moreover from eo eo' have "equiv_out o0 on" by(rule equiv_out_trans)
    ultimately show ?case by auto
  qed
qed

end ― ‹ @{text RTS_safe}

end

Theory Semantics

(* Title: RTS/Common/Semantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Semantics model"

theory Semantics
imports Main
begin

text "General model for small-step semantics:"
locale Semantics =
 fixes
  small :: "'prog  'state  'state set" and
  endset :: "'state set"
 assumes
  endset_final: "σ  endset  P. small P σ = {}"

context Semantics begin

subsection "Extending @{term small} to multiple steps"

primrec small_nstep :: "'prog  'state  nat  'state set" where
small_nstep_base:
 "small_nstep P σ 0 = {σ}" |
small_nstep_Rec:
 "small_nstep P σ (Suc n) =
  { σ2. σ1. σ1  small_nstep P σ n  σ2  small P σ1 }"

lemma small_nstep_Rec2:
 "small_nstep P σ (Suc n) =
  { σ2. σ1. σ1  small P σ  σ2  small_nstep P σ1 n }"
proof(induct n arbitrary: σ)
  case (Suc n)
  have right: "σ'. σ'  small_nstep P σ (Suc(Suc n))
     σ1. σ1  small P σ  σ'  small_nstep P σ1 (Suc n)"
  proof -
    fix σ'
    assume "σ'  small_nstep P σ (Suc(Suc n))"
    then obtain σ1 where Sucnstep: "σ1  small_nstep P σ (Suc n)" "σ'  small P σ1" by fastforce
    obtain σ12 where nstep: "σ12  small P σ  σ1  small_nstep P σ12 n"
      using Suc Sucnstep(1) by fastforce
    then show "σ1. σ1  small P σ  σ'  small_nstep P σ1 (Suc n)"
     using Sucnstep by fastforce
  qed
  have left: "σ' . σ1. σ1  small P σ  σ'  small_nstep P σ1 (Suc n)
     σ'  small_nstep P σ (Suc(Suc n))"
  proof -
    fix σ' 
    assume "σ1. σ1  small P σ  σ'  small_nstep P σ1 (Suc n)"
    then obtain σ1 where Sucnstep: "σ1  small P σ" "σ'  small_nstep P σ1 (Suc n)"
      by fastforce
    obtain σ12 where nstep: "σ12  small_nstep P σ1 n  σ'  small P σ12"
      using Sucnstep(2) by auto
    then show "σ'  small_nstep P σ (Suc(Suc n))" using Suc Sucnstep by fastforce
  qed
  show ?case using right left by fast
qed(simp)

lemma small_nstep_SucD:
assumes "σ'  small_nstep P σ (Suc n)"
shows "σ1. σ1  small P σ  σ'  small_nstep P σ1 n"
  using small_nstep_Rec2 case_prodD assms by fastforce

lemma small_nstep_Suc_nend: "σ'  small_nstep P σ (Suc n1)  σ  endset"
  using endset_final small_nstep_SucD by fastforce

subsection "Extending @{term small} to a big-step semantics"

definition big :: "'prog  'state  'state set" where
"big P σ  { σ'. n. σ'  small_nstep P σ n  σ'  endset }"

lemma bigI:
 " σ'  small_nstep P σ n; σ'  endset   σ'  big P σ"
by (fastforce simp add: big_def)

lemma bigD:
 " σ'  big P σ   n. σ'  small_nstep P σ n  σ'  endset"
by (simp add: big_def)

lemma big_def2:
 "σ'  big P σ  (n. σ'  small_nstep P σ n  σ'  endset)"
proof(rule iffI)
  assume "σ'  big P σ"
  then show "n. σ'  small_nstep P σ n  σ'  endset" using bigD big_def by auto
next
  assume "n. σ'  small_nstep P σ n  σ'  endset"
  then show "σ'  big P σ" using big_def big_def by auto
qed

lemma big_stepD:
assumes big: "σ'  big P σ" and nend: "σ  endset"
shows "σ1. σ1  small P σ  σ'  big P σ1"
proof -
  obtain n where n: "σ'  small_nstep P σ n" "σ'  endset"
    using big_def2 big by auto
  then show ?thesis using small_nstep_SucD nend big_def2 by(cases n, simp) blast
qed

(***)

lemma small_nstep_det_last_eq:
assumes det: "σ. small P σ = {}  (σ'. small P σ = {σ'})"
shows " σ'  big P σ; σ'  small_nstep P σ n; σ'  small_nstep P σ n'   n = n'"
proof(induct n arbitrary: n' σ σ')
  case 0
  have "σ' = σ" using "0.prems"(2) small_nstep_base by blast
  then have endset: "σ  endset" using "0.prems"(1) bigD by blast
  show ?case
  proof(cases n')
    case Suc then show ?thesis using "0.prems"(3) small_nstep_SucD endset_final[OF endset] by blast
  qed(simp)
next
  case (Suc n1)
  then have endset: "σ'  endset" using Suc.prems(1) bigD by blast
  have nend: "σ  endset" using small_nstep_Suc_nend[OF Suc.prems(2)] by simp
  then have neq: "σ'  σ" using endset by auto
  obtain σ1 where σ1: "σ1  small P σ" "σ'  small_nstep P σ1 n1"
    using small_nstep_SucD[OF Suc.prems(2)] by clarsimp
  then have big: "σ'  big P σ1" using endset by(auto simp: big_def)
  show ?case
  proof(cases n')
    case 0 then show ?thesis using neq Suc.prems(3) using small_nstep_base by blast
  next
    case Suc': (Suc n1')
    then obtain σ1' where σ1': "σ1'  small P σ" "σ'  small_nstep P σ1' n1'"
      using small_nstep_SucD[where σ=σ and σ'=σ' and n=n1'] Suc.prems(3) by blast
    then have "σ1=σ1'" using σ1(1) det by auto
    then show ?thesis using Suc.hyps(1)[OF big σ1(2)] σ1'(2) Suc' by blast
  qed
qed

end ― ‹ Semantics ›


end

Theory CollectionSemantics

(* Title: RTS/Common/CollectionSemantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Collection Semantics"

theory CollectionSemantics
imports Semantics
begin

text "General model for small step semantics instrumented
 with an information collection mechanism:"
locale CollectionSemantics = Semantics +
 constrains
  small :: "'prog  'state  'state set" and
  endset :: "'state set"
 fixes
  collect :: "'prog  'state  'state  'coll" and
  combine :: "'coll  'coll  'coll" and
  collect_id :: "'coll"
 assumes
  combine_assoc: "combine (combine c1 c2) c3 = combine c1 (combine c2 c3)" and
  collect_idl[simp]: "combine collect_id c = c" and
  collect_idr[simp]: "combine c collect_id = c"

context CollectionSemantics begin

subsection "Small-Step Collection Semantics"

definition csmall :: "'prog  'state  ('state × 'coll) set" where
"csmall P σ  { (σ', coll). σ'  small P σ  collect P σ σ' = coll }"

lemma small_det_csmall_det:
assumes "σ. small P σ = {}  (σ'. small P σ = {σ'})"
shows "σ. csmall P σ = {}  (o'. csmall P σ = {o'})"
using assms by(fastforce simp: csmall_def)

subsection "Extending @{term csmall} to multiple steps"

primrec csmall_nstep :: "'prog  'state  nat  ('state × 'coll) set" where
csmall_nstep_base:
 "csmall_nstep P σ 0 = {(σ, collect_id)}" |
csmall_nstep_Rec:
 "csmall_nstep P σ (Suc n) =
  { (σ2, coll). σ1 coll1 coll2. (σ1, coll1)  csmall_nstep P σ n
                       (σ2, coll2)  csmall P σ1  combine coll1 coll2 = coll }"

lemma small_nstep_csmall_nstep_equiv:
 "small_nstep P σ n
       = { σ'. coll. (σ', coll)  csmall_nstep P σ n }"
proof (induct n) qed(simp_all add: csmall_def)

lemma csmall_nstep_exists:
 "σ'  big P σ  n coll. (σ', coll)  csmall_nstep P σ n  σ'  endset"
proof(drule bigD) qed(clarsimp simp: small_nstep_csmall_nstep_equiv)

lemma csmall_det_csmall_nstep_det:
assumes "σ. csmall P σ = {}  (o'. csmall P σ = {o'})"
shows "σ. csmall_nstep P σ n = {}  (o'. csmall_nstep P σ n = {o'})"
using assms
proof(induct n)
  case (Suc n) then show ?case by fastforce
qed(simp)

lemma csmall_nstep_Rec2:
 "csmall_nstep P σ (Suc n) =
  { (σ2, coll). σ1 coll1 coll2. (σ1, coll1)  csmall P σ
                       (σ2, coll2)  csmall_nstep P σ1 n  combine coll1 coll2 = coll }"
proof(induct n arbitrary: σ)
  case (Suc n)
  have right: "σ' coll'. (σ', coll')  csmall_nstep P σ (Suc(Suc n))
     σ1 coll1 coll2. (σ1, coll1)  csmall P σ
                       (σ', coll2)  csmall_nstep P σ1 (Suc n)  combine coll1 coll2 = coll'"
  proof -
    fix σ' coll'
    assume "(σ', coll')  csmall_nstep P σ (Suc(Suc n))"
    then obtain σ1 coll1 coll2 where Sucnstep: "(σ1, coll1)  csmall_nstep P σ (Suc n)"
                        "(σ', coll2)  csmall P σ1" "combine coll1 coll2 = coll'" by fastforce
    obtain σ12 coll12 coll22 where nstep: "(σ12, coll12)  csmall P σ
                         (σ1, coll22)  csmall_nstep P σ12 n  combine coll12 coll22 = coll1"
      using Suc Sucnstep(1) by fastforce
    then show "σ1 coll1 coll2. (σ1, coll1)  csmall P σ
                       (σ', coll2)  csmall_nstep P σ1 (Suc n)  combine coll1 coll2 = coll'"
     using combine_assoc[of coll12 coll22 coll2] Sucnstep by fastforce
  qed
  have left: "σ' coll'. σ1 coll1 coll2. (σ1, coll1)  csmall P σ
                       (σ', coll2)  csmall_nstep P σ1 (Suc n)  combine coll1 coll2 = coll'
     (σ', coll')  csmall_nstep P σ (Suc(Suc n))"
  proof -
    fix σ' coll'
    assume "σ1 coll1 coll2. (σ1, coll1)  csmall P σ
                       (σ', coll2)  csmall_nstep P σ1 (Suc n)  combine coll1 coll2 = coll'"
    then obtain σ1 coll1 coll2 where Sucnstep: "(σ1, coll1)  csmall P σ"
                      "(σ', coll2)  csmall_nstep P σ1 (Suc n)" "combine coll1 coll2 = coll'"
      by fastforce
    obtain σ12 coll12 coll22 where nstep: "(σ12, coll12)  csmall_nstep P σ1 n
                         (σ', coll22)  csmall P σ12  combine coll12 coll22 = coll2"
      using Sucnstep(2) by auto
    then show "(σ', coll')  csmall_nstep P σ (Suc(Suc n))"
      using combine_assoc[of coll1 coll12 coll22] Suc Sucnstep by fastforce
  qed
  show ?case using right left by fast
qed(simp)

lemma csmall_nstep_SucD:
assumes "(σ',coll')  csmall_nstep P σ (Suc n)"
shows "σ1 coll1. (σ1, coll1)  csmall P σ
    (coll. coll' = combine coll1 coll  (σ',coll)  csmall_nstep P σ1 n)"
  using csmall_nstep_Rec2 CollectionSemantics_axioms case_prodD assms by fastforce

lemma csmall_nstep_Suc_nend: "o'  csmall_nstep P σ (Suc n1)  σ  endset"
  using endset_final csmall_nstep_SucD CollectionSemantics.csmall_def CollectionSemantics_axioms
  by fastforce

lemma small_to_csmall_nstep_pres:
assumes Qpres: "P σ σ'. Q P σ  σ'  small P σ  Q P σ'"
shows "Q P σ  (σ', coll)  csmall_nstep P σ n  Q P σ'"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1)  csmall_nstep P σ n
                       (σ', coll2)  csmall P σ1  combine coll1 coll2 = coll" by clarsimp
  then show ?case using Suc Qpres[where P=P and σ=σ1 and σ'=σ'] by(auto simp: csmall_def)
qed(simp)

lemma csmall_to_csmall_nstep_prop:
assumes cond: "P σ σ' coll. (σ', coll)  csmall P σ  R P coll  Q P σ  R' P σ σ' coll"
  and Rcomb: "P coll1 coll2. R P (combine coll1 coll2) = (R P coll1  R P coll2)"
  and Qpres: "P σ σ'. Q P σ  σ'  small P σ  Q P σ'"
  and Rtrans': "P σ σ1 σ' coll1 coll2.
                        R' P σ σ1 coll1  R' P σ1 σ' coll2  R' P σ σ' (combine coll1 coll2)"
  and base: "σ. R' P σ σ collect_id"
shows "(σ', coll)  csmall_nstep P σ n  R P coll  Q P σ  R' P σ σ' coll"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1)  csmall_nstep P σ n
                       (σ', coll2)  csmall P σ1  combine coll1 coll2 = coll" by clarsimp
  then have "Q P σ1" using small_to_csmall_nstep_pres[where Q=Q] Qpres Suc by blast
  then show ?case using nstep assms Suc by auto blast
qed(simp add: base)

lemma csmall_to_csmall_nstep_prop2:
assumes cond: "P P' σ σ' coll. (σ', coll)  csmall P σ
              R P P' coll  Q σ  (σ', coll)  csmall P' σ"
  and Rcomb: "P P' coll1 coll2. R P P' (combine coll1 coll2) = (R P P' coll1  R P P' coll2)"
  and Qpres: "P σ σ'. Q σ  σ'  small P σ  Q σ'"
shows "(σ', coll)  csmall_nstep P σ n  R P P' coll  Q σ  (σ', coll)  csmall_nstep P' σ n"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1)  csmall_nstep P σ n
                       (σ', coll2)  csmall P σ1  combine coll1 coll2 = coll" by clarsimp
  then have "Q σ1" using small_to_csmall_nstep_pres[where Q="λP. Q"] Qpres Suc by blast
  then show ?case using nstep assms Suc by auto blast
qed(simp)

subsection "Extending @{term csmall} to a big-step semantics"

definition cbig :: "'prog  'state  ('state × 'coll) set" where
"cbig P σ 
  { (σ', coll). n. (σ', coll)  csmall_nstep P σ n  σ'  endset }"

lemma cbigD:
 " (σ',coll')  cbig P σ   n. (σ',coll')  csmall_nstep P σ n  σ'  endset"
  by(simp add: cbig_def)

lemma cbigD':
 " o'  cbig P σ   n. o'  csmall_nstep P σ n  fst o'  endset"
  by(cases o', simp add: cbig_def)

lemma cbig_def2:
 "(σ', coll)  cbig P σ  (n. (σ', coll)  csmall_nstep P σ n  σ'  endset)"
proof(rule iffI)
  assume "(σ', coll)  cbig P σ"
  then show "n. (σ', coll)  csmall_nstep P σ n  σ'  endset" using bigD cbig_def by auto
next
  assume "n. (σ', coll)  csmall_nstep P σ n  σ'  endset"
  then show "(σ', coll)  cbig P σ" using big_def cbig_def small_nstep_csmall_nstep_equiv by auto
qed

lemma cbig_big_equiv:
 "(coll. (σ', coll)  cbig P σ)  σ'  big P σ"
proof(rule iffI)
  assume "coll. (σ', coll)  cbig P σ"
  then show "σ'  big P σ" by (auto simp: big_def cbig_def small_nstep_csmall_nstep_equiv)
next
  assume "σ'  big P σ"
  then show "coll. (σ', coll)  cbig P σ" by (fastforce simp: cbig_def dest: csmall_nstep_exists)
qed

lemma cbig_big_implies:
 "(σ', coll)  cbig P σ  σ'  big P σ"
using cbig_big_equiv by blast

lemma csmall_to_cbig_prop:
assumes "P σ σ' coll. (σ', coll)  csmall P σ  R P coll  Q P σ  R' P σ σ' coll"
  and "P coll1 coll2. R P (combine coll1 coll2) = (R P coll1  R P coll2)"
  and "P σ σ'. Q P σ  σ'  small P σ  Q P σ'"
  and "P σ σ1 σ' coll1 coll2.
                        R' P σ σ1 coll1  R' P σ1 σ' coll2  R' P σ σ' (combine coll1 coll2)"
  and "σ. R' P σ σ collect_id"
shows "(σ', coll)  cbig P σ  R P coll  Q P σ  R' P σ σ' coll"
using assms csmall_to_csmall_nstep_prop[where R=R and Q=Q and R'=R' and σ=σ]
  by(auto simp: cbig_def2)

lemma csmall_to_cbig_prop2:
assumes "P P' σ σ' coll. (σ', coll)  csmall P σ  R P P' coll  Q σ  (σ', coll)  csmall P' σ"
  and "P P' coll1 coll2. R P P' (combine coll1 coll2) = (R P P' coll1  R P P' coll2)"
  and Qpres: "P σ σ'. Q σ  σ'  small P σ  Q σ'"
shows "(σ', coll)  cbig P σ  R P P' coll  Q σ  (σ', coll)  cbig P' σ"
using assms csmall_to_csmall_nstep_prop2[where R=R and Q=Q] by(auto simp: cbig_def2) blast

lemma cbig_stepD:
assumes cbig: "(σ',coll')  cbig P σ" and nend: "σ  endset"
shows "σ1 coll1. (σ1, coll1)  csmall P σ
    (coll. coll' = combine coll1 coll  (σ',coll)  cbig P σ1)"
proof -
  obtain n where n: "(σ', coll')  csmall_nstep P σ n" "σ'  endset"
    using cbig_def2 cbig by auto
  then show ?thesis using csmall_nstep_SucD nend cbig_def2 by(cases n, simp) blast
qed

(****)

lemma csmall_nstep_det_last_eq:
assumes det: "σ. small P σ = {}  (σ'. small P σ = {σ'})"
shows " (σ',coll')  cbig P σ; (σ',coll')  csmall_nstep P σ n; (σ',coll'')  csmall_nstep P σ n' 
  n = n'"
proof(induct n arbitrary: n' σ σ' coll' coll'')
  case 0
  have "σ' = σ" using "0.prems"(2) csmall_nstep_base by blast
  then have endset: "σ  endset" using "0.prems"(1) cbigD by blast
  show ?case
  proof(cases n')
    case Suc then show ?thesis using "0.prems"(3) csmall_nstep_Suc_nend endset by blast
  qed(simp)
next
  case (Suc n1)
  then have endset: "σ'  endset" using Suc.prems(1) cbigD by blast
  have nend: "σ  endset" using csmall_nstep_Suc_nend[OF Suc.prems(2)] by simp
  then have neq: "σ'  σ" using endset by auto
  obtain σ1 coll coll1 where σ1: "(σ1,coll1)  csmall P σ" "coll' = combine coll1 coll"
     "(σ',coll)  csmall_nstep P σ1 n1"
    using csmall_nstep_SucD[OF Suc.prems(2)] by clarsimp
  then have cbig: "(σ',coll)  cbig P σ1" using endset by(auto simp: cbig_def)
  show ?case
  proof(cases n')
    case 0 then show ?thesis using neq Suc.prems(3) using csmall_nstep_base by simp
  next
    case Suc': (Suc n1')
    then obtain σ1' coll2 coll1' where σ1': "(σ1',coll1')  csmall P σ" "coll'' = combine coll1' coll2"
      "(σ',coll2)  csmall_nstep P σ1' n1'"
      using csmall_nstep_SucD[where σ=σ and σ'=σ' and coll'=coll'' and n=n1'] Suc.prems(3) by blast
    then have "σ1=σ1'" using σ1 det csmall_def by auto
    then show ?thesis using Suc.hyps(1)[OF cbig σ1(3)] σ1'(3) Suc' by blast
  qed
qed

end ― ‹ CollectionSemantics ›

end

Theory CollectionBasedRTS

(* Title: RTS/Common/CollectionBasedRTS.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Collection-based RTS"

theory CollectionBasedRTS
imports RTS_safe CollectionSemantics
begin

locale CollectionBasedRTS_base = RTS_safe + CollectionSemantics

text "General model for Regression Test Selection based on
 @{term CollectionSemantics}:"
locale CollectionBasedRTS = CollectionBasedRTS_base where
  small = "small :: 'prog  'state  'state set" and
  collect = "collect :: 'prog  'state  'state  'coll" and
  out = "out :: 'prog  'test  ('state × 'coll) set"
 for small collect out
+
 fixes
  make_test_prog :: "'prog  'test  'prog" and
  collect_start :: "'prog  'coll"
 assumes
  out_cbig:
   "i. out P t = {(σ',coll'). coll. (σ',coll)  cbig (make_test_prog P t) i
                                                   coll' = combine coll (collect_start P) }"

context CollectionBasedRTS begin

end ― ‹ CollectionBasedRTS ›

end

Theory JVMSemantics

(* Title: RTS/JVM_RTS/JVMSemantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Instantiating @{term Semantics} with Jinja JVM"

theory JVMSemantics
imports "../Common/Semantics" JinjaDCI.JVMExec
begin

fun JVMsmall :: "jvm_prog  jvm_state  jvm_state set" where
"JVMsmall P σ = { σ'. exec (P, σ) = Some σ' }"

lemma JVMsmall_prealloc_pres:
assumes pre: "preallocated (fst(snd σ))"
  and "σ'  JVMsmall P σ"
shows "preallocated (fst(snd σ'))"
using exec_prealloc_pres[OF pre] assms by(cases σ, cases σ', auto)

lemma JVMsmall_det: "JVMsmall P σ = {}  (σ'. JVMsmall P σ = {σ'})"
by auto

definition JVMendset :: "jvm_state set" where
"JVMendset  { (xp,h,frs,sh). frs = []  (x. xp = Some x) }"

lemma JVMendset_final: "σ  JVMendset  P. JVMsmall P σ = {}"
 by(auto simp: JVMendset_def)

lemma start_state_nend:
 "start_state P  JVMendset"
 by(simp add: start_state_def JVMendset_def)

interpretation JVMSemantics: Semantics JVMsmall JVMendset
 by unfold_locales (auto dest: JVMendset_final)

end

Theory ClassesChanged

(*  Title:      RTS/JinjaSuppl/ClassesChanged.thy
    Author:    Susannah Mansky, UIUC 2020
    Description: Theory around the classes changed from one program to another
*)

section "@{term classes_changed} theory"

theory ClassesChanged
imports JinjaDCI.Decl
begin

text "A class is considered changed if it exists only in one program or the other,
  or exists in both but is different."
definition classes_changed :: "'m prog  'm prog  cname set" where
"classes_changed P1 P2 = {cn. class P1 cn  class P2 cn}"

definition class_changed :: "'m prog  'm prog  cname  bool" where
"class_changed P1 P2 cn = (class P1 cn  class P2 cn)"

lemma classes_changed_class_changed[simp]: "cn  classes_changed P1 P2 = class_changed P1 P2 cn"
 by (simp add: classes_changed_def class_changed_def)

lemma classes_changed_self[simp]: "classes_changed P P = {}"
 by (auto simp: class_changed_def)

lemma classes_changed_sym: "classes_changed P P' = classes_changed P' P"
 by (auto simp: class_changed_def)

lemma classes_changed_class: " cn  classes_changed P P'  class P cn = class P' cn"
 by (clarsimp simp: class_changed_def)

lemma classes_changed_class_set: " S  classes_changed P P' = {} 
   C  S. class P C = class P' C"
 by (fastforce simp: disjoint_iff_not_equal dest: classes_changed_class)

text "We now relate @{term classes_changed} over two programs to those
 over programs with an added class (such as a test class)."

lemma classes_changed_cons_eq:
 "classes_changed (t # P) P' = (classes_changed P P' - {fst t})
                      (if class_changed [t] P' (fst t) then {fst t} else {})"
 by (auto simp: classes_changed_def class_changed_def class_def)

lemma class_changed_cons:
 "fst t  classes_changed (t#P) (t#P')"
 by (simp add: class_changed_def class_def)

lemma classes_changed_cons:
 "classes_changed (t # P) (t # P') = classes_changed P P' - {fst t}"
proof(cases "fst t  classes_changed P P'")
  case True
  then show ?thesis using class_changed_cons[where t=t and P=P and P'=P']
    classes_changed_cons_eq[where t=t] by (auto simp: class_changed_def class_cons)
next
  case False
  then show ?thesis using class_changed_cons[where t=t and P=P and P'=P']
    by (auto simp: class_changed_def) (metis (no_types, lifting) class_cons)+
qed

lemma classes_changed_int_Cons:
assumes "coll  classes_changed P P' = {}"
shows "coll  classes_changed (t # P) (t # P') = {}"
proof(cases "fst t  classes_changed P P'")
  case True
  then have "classes_changed P P' = classes_changed (t # P) (t # P')  {fst t}"
    using classes_changed_cons[where t=t and P=P and P'=P'] by fastforce
  then show ?thesis using assms by simp
next
  case False
  then have "classes_changed P P' = classes_changed (t # P) (t # P')"
    using classes_changed_cons[where t=t and P=P and P'=P'] by fastforce
  then show ?thesis using assms by simp
qed

end

Theory Subcls

(*  Title:      RTS/JinjaSuppl/Subcls.thy
    Author:    Susannah Mansky, UIUC 2020
    Description:  Theory for the subcls relation
*)

section "@{term subcls} theory"

theory Subcls
imports JinjaDCI.TypeRel
begin

lemma subcls_class_ex: " P  C * C'; C  C' 
  D' fs ms. class P C = (D', fs, ms)"
proof(induct rule: converse_rtrancl_induct)
  case (step y z) then show ?case by(auto dest: subcls1D)
qed(simp)

lemma class_subcls1:
 " class P y = class P' y; P  y 1 z   P'  y 1 z"
 by(auto dest!: subcls1D intro!: subcls1I intro: sym)


lemma subcls1_single_valued: "single_valued (subcls1 P)"
by (clarsimp simp: single_valued_def subcls1.simps)

lemma subcls_confluent:
  " P  C * C'; P  C * C''   P  C' * C''  P  C'' * C'"
 by (simp add: single_valued_confluent subcls1_single_valued)

lemma subcls1_confluent: " P  a 1 b; P  a * c; a  c   P  b * c"
using subcls1_single_valued
 by (auto elim!: converse_rtranclE[where x=a] simp: single_valued_def)


lemma subcls_self_superclass: " P  C 1 C; P  C * D   D = C"
using subcls1_single_valued
 by (auto elim!: rtrancl_induct[where b=D] simp: single_valued_def)

lemma subcls_of_Obj_acyclic:
 " P  C * Object; C  D  ¬(P  C * D  P  D * C)"
proof(induct arbitrary: D rule: converse_rtrancl_induct)
  case base then show ?case by simp
next
  case (step y z) show ?case
  proof(cases "y=z")
    case True with step show ?thesis by simp
  next
    case False show ?thesis
    proof(cases "z = D")
      case True with False step.hyps(3)[of y] show ?thesis by clarsimp
    next
      case neq: False
      with step.hyps(3) have "¬(P  z * D  P  D * z)" by simp
      moreover from step.hyps(1)
      have "P  D * y  P  D * z" by(simp add: rtrancl_into_rtrancl)
      moreover from step.hyps(1) step.prems(1)
      have "P  y * D  P  z * D" by(simp add: subcls1_confluent)
      ultimately show ?thesis by clarsimp
    qed
  qed
qed

lemma subcls_of_Obj: " P  C * Object; P  C * D   P  D * Object"
 by(auto dest: subcls_confluent)

end

Theory ClassesAbove

(*  Title:      RTS/JinjaSuppl/ClassesAbove.thy
    Author:    Susannah Mansky, UIUC 2020
*)

section "@{term classes_above} theory"

text "This section contains theory around the classes above
 (superclasses of) a class in the class structure, in particular
 noting that if their contents have not changed, then much of what
 that class sees (methods, fields) stays the same."

theory ClassesAbove
imports ClassesChanged Subcls JinjaDCI.Exceptions
begin

abbreviation classes_above :: "'m prog  cname  cname set" where
"classes_above P c  { cn. P  c * cn }"

abbreviation classes_between :: "'m prog  cname  cname  cname set" where
"classes_between P c d  { cn. (P  c * cn  P  cn * d) }"

abbreviation classes_above_xcpts :: "'m prog  cname set" where
"classes_above_xcpts P  xsys_xcpts. classes_above P x"

(******************************************************************************)

lemma classes_above_def2:
 "P  C 1 D  classes_above P C = {C}  classes_above P D"
using subcls1_confluent by auto

lemma classes_above_class:
 " classes_above P C  classes_changed P P' = {}; P  C * C' 
   class P C' = class P' C'"
 by (drule classes_changed_class_set, simp)

lemma classes_above_subset:
assumes "classes_above P C  classes_changed P P' = {}"
shows "classes_above P C  classes_above P' C"
proof -
  have ind: "x. P  C * x  P'  C * x"
  proof -
    fix x assume sub: "P  C * x"
    then show "P'  C * x"
    proof(induct rule: rtrancl_induct)
      case base then show ?case by simp
    next
      case (step y z)
      have "P'  y 1 z" by(rule class_subcls1[OF classes_above_class[OF assms step(1)] step(2)])
      then show ?case using step(3) by simp
    qed
  qed
  with classes_changed_class_set[OF assms] show ?thesis by clarsimp
qed

lemma classes_above_subcls:
 " classes_above P C  classes_changed P P' = {}; P  C * C' 
    P'  C * C'"
 by (fastforce dest: classes_above_subset)

lemma classes_above_subset2:
assumes "classes_above P C  classes_changed P P' = {}"
shows "classes_above P' C  classes_above P C"
proof -
  have ind: "x. P'  C * x  P  C * x"
  proof -
    fix x assume sub: "P'  C * x"
    then show "P  C * x"
    proof(induct rule: rtrancl_induct)
      case base then show ?case by simp
    next
      case (step y z)
      with class_subcls1 classes_above_class[OF assms] rtrancl_into_rtrancl show ?case by metis
    qed
  qed
  with classes_changed_class_set[OF assms] show ?thesis by clarsimp
qed

lemma classes_above_subcls2:
 " classes_above P C  classes_changed P P' = {}; P'  C * C' 
    P  C * C'"
 by (fastforce dest: classes_above_subset2)

lemma classes_above_set:
 " classes_above P C  classes_changed P P' = {} 
   classes_above P C = classes_above P' C"
 by(fastforce dest: classes_above_subset classes_above_subset2)

lemma classes_above_classes_changed_sym:
assumes "classes_above P C  classes_changed P P' = {}"
shows "classes_above P' C  classes_changed P' P = {}"
proof -
  have "classes_above P C = classes_above P' C" by(rule classes_above_set[OF assms])
  with classes_changed_sym[where P=P] assms show ?thesis by simp
qed

lemma classes_above_sub_classes_between_eq:
 "P  C * D  classes_above P C = (classes_between P C D - {D})  classes_above P D"
using subcls_confluent by auto

lemma classes_above_subcls_subset:
 " P  C * C'   classes_above P C'  classes_above P C"
 by auto

(************************************************************)
subsection "Methods"

lemma classes_above_sees_methods:
assumes int: "classes_above P C  classes_changed P P' = {}" and ms: "P  C sees_methods Mm"
shows "P'  C sees_methods Mm"
proof -
  have cls: "C'classes_above P C. class P C' = class P' C'"
   by(rule classes_changed_class_set[OF int])

  have "C Mm. P  C sees_methods Mm 
               C'classes_above P C. class P C' = class P' C'  P'  C sees_methods Mm"
  proof -
    fix C Mm assume "P  C sees_methods Mm" and "C'classes_above P C. class P C' = class P' C'"
    then show "P'  C sees_methods Mm"
    proof(induct rule: Methods.induct)
      case Obj: (sees_methods_Object D fs ms Mm)
      with cls have "class P' Object = (D, fs, ms)" by simp
      with Obj show ?case by(auto intro!: sees_methods_Object)
    next
      case rec: (sees_methods_rec C D fs ms Mm Mm')
      then have "P  C * D" by (simp add: r_into_rtrancl[OF subcls1I])
      with converse_rtrancl_into_rtrancl have "x. P  D * x  P  C * x" by simp
      with rec.prems(1) have "C'classes_above P D. class P C' = class P' C'" by simp
      with rec show ?case by(auto intro: sees_methods_rec)
    qed
  qed
  with ms cls show ?thesis by simp
qed

lemma classes_above_sees_method:
 " classes_above P C  classes_changed P P' = {};
     P  C sees M,b: TsT = m in C' 
   P'  C sees M,b: TsT = m in C'"
 by (auto dest: classes_above_sees_methods simp: Method_def)

lemma classes_above_sees_method2:
 " classes_above P C  classes_changed P P' = {};
     P'  C sees M,b: TsT = m in C' 
   P  C sees M,b: TsT = m in C'"
 by (auto dest: classes_above_classes_changed_sym intro: classes_above_sees_method)

lemma classes_above_method:
assumes "classes_above P C  classes_changed P P' = {}"
shows "method P C M = method P' C M"
proof(cases "Ts T m D b. P  C sees M,b :  TsT = m in D")
  case True
  with assms show ?thesis by (auto dest: classes_above_sees_method)
next
  case False
  with assms have "¬(Ts T m D b. P'  C sees M,b :  TsT = m in D)"
    by (auto dest: classes_above_sees_method2)
  with False show ?thesis by(simp add: method_def)
qed

(*********************************************)
subsection "Fields"

lemma classes_above_has_fields:
assumes int: "classes_above P C  classes_changed P P' = {}" and fs: "P  C has_fields FDTs"
shows "P'  C has_fields FDTs"
proof -
  have cls: "C'classes_above P C. class P C' = class P' C'"
   by(rule classes_changed_class_set[OF int])

  have "C Mm. P  C has_fields FDTs 
               C'classes_above P C. class P C' = class P' C'  P'  C has_fields FDTs"
  proof -
    fix C Mm assume "P  C has_fields FDTs" and "C'classes_above P C. class P C' = class P' C'"
    then show "P'  C has_fields FDTs"
    proof(induct rule: Fields.induct)
      case Obj: (has_fields_Object D fs ms FDTs)
      with cls have "class P' Object = (D, fs, ms)" by simp
      with Obj show ?case by(auto intro!: has_fields_Object)
    next
      case rec: (has_fields_rec C D fs ms FDTs FDTs')
      then have "P  C * D" by (simp add: r_into_rtrancl[OF subcls1I])
      with converse_rtrancl_into_rtrancl have "x. P  D * x  P  C * x" by simp
      with rec.prems(1) have "x. P  D * x  class P x = class P' x" by simp
      with rec show ?case by(auto intro: has_fields_rec)
    qed
  qed
  with fs cls show ?thesis by simp
qed

lemma classes_above_has_fields_dne:
assumes "classes_above P C  classes_changed P P' = {}"
shows "(FDTs. ¬ P  C has_fields FDTs) = (FDTs. ¬ P'  C has_fields FDTs)"
proof(rule iffI)
  assume asm: "FDTs. ¬ P  C has_fields FDTs"
  from assms classes_changed_sym[where P=P] classes_above_set[OF assms]
   have int': "classes_above P' C  classes_changed P' P = {}" by simp
  from asm classes_above_has_fields[OF int'] show "FDTs. ¬ P'  C has_fields FDTs" by auto
next
  assume "FDTs. ¬ P'  C has_fields FDTs"
  with assms show "FDTs. ¬ P  C has_fields FDTs" by(auto dest: classes_above_has_fields)
qed

lemma classes_above_has_field:
 " classes_above P C  classes_changed P P' = {};
    P  C has F,b:t in C' 
    P'  C has F,b:t in C'"
 by(auto dest: classes_above_has_fields simp: has_field_def)

lemma classes_above_has_field2:
 " classes_above P C  classes_changed P P' = {};
     P'  C has F,b:t in C' 
   P  C has F,b:t in C'"
 by(auto intro: classes_above_has_field dest: classes_above_classes_changed_sym)

lemma classes_above_sees_field:
 " classes_above P C  classes_changed P P' = {};
    P  C sees F,b:t in C' 
    P'  C sees F,b:t in C'"
 by(auto dest: classes_above_has_fields simp: sees_field_def)

lemma classes_above_sees_field2:
 " classes_above P C  classes_changed P P' = {};
     P'  C sees F,b:t in C' 
   P  C sees F,b:t in C'"
 by (auto intro: classes_above_sees_field dest: classes_above_classes_changed_sym)

lemma classes_above_field:
assumes "classes_above P C  classes_changed P P' = {}"
shows "field P C F = field P' C F"
proof(cases "T D b. P  C sees F,b : T in D")
  case True
  with assms show ?thesis by (auto dest: classes_above_sees_field)
next
  case False
  with assms have "¬(T D b. P'  C sees F,b : T in D)"
    by (auto dest: classes_above_sees_field2)
  with False show ?thesis by(simp add: field_def)
qed

lemma classes_above_fields:
assumes "classes_above P C  classes_changed P P' = {}"
shows "fields P C = fields P' C"
proof(cases "FDTs. P  C has_fields FDTs")
  case True
  with assms show ?thesis by(auto dest: classes_above_has_fields)
next
  case False
  with assms show ?thesis by (auto dest: classes_above_has_fields_dne simp: fields_def)
qed

lemma classes_above_ifields:
 " classes_above P C  classes_changed P P' = {} 
 
  ifields P C = ifields P' C"
 by (simp add: ifields_def classes_above_fields)


lemma classes_above_blank:
 " classes_above P C  classes_changed P P' = {} 
 
  blank P C = blank P' C"
 by (simp add: blank_def classes_above_ifields)

lemma classes_above_isfields:
 " classes_above P C  classes_changed P P' = {} 
 
  isfields P C = isfields P' C"
 by (simp add: isfields_def classes_above_fields)

lemma classes_above_sblank:
 " classes_above P C  classes_changed P P' = {} 
 
  sblank P C = sblank P' C"
 by (simp add: sblank_def classes_above_isfields)

(******************************************)
subsection "Other"

lemma classes_above_start_heap:
assumes "classes_above_xcpts P  classes_changed P P' = {}"
shows "start_heap P = start_heap P'"
proof -
  from assms have "C  sys_xcpts. blank P C = blank P' C" by (auto intro: classes_above_blank)
  then show ?thesis by(simp add: start_heap_def)
qed

end

Theory JVMCollectionSemantics

(* File: RTS/JVM_RTS/JVMCollectionSemantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Instantiating @{term CollectionSemantics} with Jinja JVM"

theory JVMCollectionSemantics
imports "../Common/CollectionSemantics" JVMSemantics "../JinjaSuppl/ClassesAbove"

begin

abbreviation JVMcombine :: "cname set  cname set  cname set" where
"JVMcombine C C'  C  C'"

abbreviation JVMcollect_id :: "cname set" where
"JVMcollect_id  {}"

(*******************************************)
subsection ‹ JVM-specific @{text "classes_above"} theory ›

fun classes_above_frames :: "'m prog  frame list  cname set" where
"classes_above_frames P ((stk,loc,C,M,pc,ics)#frs) = classes_above P C  classes_above_frames P frs" |
"classes_above_frames P [] = {}"

lemma classes_above_start_state:
assumes above_xcpts: "classes_above_xcpts P  classes_changed P P' = {}"
shows "start_state P = start_state P'"
using assms classes_above_start_heap by(simp add: start_state_def)

lemma classes_above_matches_ex_entry:
 "classes_above P C  classes_changed P P' = {}
   matches_ex_entry P C pc xcp = matches_ex_entry P' C pc xcp"
using classes_above_subcls classes_above_subcls2
 by(auto simp: matches_ex_entry_def)

lemma classes_above_match_ex_table:
assumes "classes_above P C  classes_changed P P' = {}"
shows "match_ex_table P C pc es = match_ex_table P' C pc es"
using classes_above_matches_ex_entry[OF assms] proof(induct es) qed(auto)

lemma classes_above_find_handler:
assumes "classes_above P (cname_of h a)  classes_changed P P' = {}"
shows "classes_above_frames P frs  classes_changed P P' = {}
   find_handler P a h frs sh = find_handler P' a h frs sh"
proof(induct frs)
  case (Cons fr' frs')
  obtain stk loc C M pc ics where fr': "fr' = (stk,loc,C,M,pc,ics)" by(cases fr')
  with Cons have
       intC: "classes_above P C  classes_changed P P' = {}"
   and int: "classes_above_frames P frs'  classes_changed P P' = {}"  by auto
  show ?case using Cons fr' int classes_above_method[OF intC]
    classes_above_match_ex_table[OF assms(1)] by(auto split: bool.splits)
qed(simp)

lemma find_handler_classes_above_frames:
 "find_handler P a h frs sh = (xp',h',frs',sh')
  classes_above_frames P frs'  classes_above_frames P frs"
proof(induct frs)
  case (Cons f1 frs1)
  then obtain stk loc C M pc ics where f1: "f1 = (stk,loc,C,M,pc,ics)" by(cases f1)
  show ?case
  proof(cases "match_ex_table P (cname_of h a) pc (ex_table_of P C M)")
    case None then show ?thesis using f1 None Cons
     by(auto split: bool.splits list.splits init_call_status.splits)
  next
    case (Some a) then show ?thesis using f1 Some Cons by auto
  qed
qed(simp)

lemma find_handler_pieces:
 "find_handler P a h frs sh = (xp',h',frs',sh')
  h = h'  sh = sh'  classes_above_frames P frs'  classes_above_frames P frs"
using find_handler_classes_above_frames by(auto dest: find_handler_heap find_handler_sheap)

(**************************************)

subsection "Naive RTS algorithm"

fun JVMinstr_ncollect ::
 "[jvm_prog, instr, heap, val list]  cname set" where
"JVMinstr_ncollect P (New C) h stk = classes_above P C" |
"JVMinstr_ncollect P (Getfield F C) h stk =
  (if (hd stk) = Null then {}
   else classes_above P (cname_of h (the_Addr (hd stk))))" |
"JVMinstr_ncollect P (Getstatic C F D) h stk = classes_above P C" |
"JVMinstr_ncollect P (Putfield F C) h stk =
  (if (hd (tl stk)) = Null then {}
   else classes_above P (cname_of h (the_Addr (hd (tl stk)))))" |
"JVMinstr_ncollect P (Putstatic C F D) h stk = classes_above P C" |
"JVMinstr_ncollect P (Checkcast C) h stk =
  (if (hd stk) = Null then {}
   else classes_above P (cname_of h (the_Addr (hd stk))))" |
"JVMinstr_ncollect P (Invoke M n) h stk =
  (if (stk ! n) = Null then {}
   else classes_above P (cname_of h (the_Addr (stk ! n))))" |
"JVMinstr_ncollect P (Invokestatic C M n) h stk = classes_above P C" |
"JVMinstr_ncollect P Throw h stk =
  (if (hd stk) = Null then {}
   else classes_above P (cname_of h (the_Addr (hd stk))))" |
"JVMinstr_ncollect P _ h stk = {}"

fun JVMstep_ncollect ::
 "[jvm_prog, heap, val list, cname, mname, pc, init_call_status]  cname set" where
"JVMstep_ncollect P h stk C M pc (Calling C' Cs) = classes_above P C'" |
"JVMstep_ncollect P h stk C M pc (Called (C'#Cs))
 = classes_above P C'  classes_above P (fst(method P C' clinit))" |
"JVMstep_ncollect P h stk C M pc (Throwing Cs a) = classes_above P (cname_of h a)" |
"JVMstep_ncollect P h stk C M pc ics = JVMinstr_ncollect P (instrs_of P C M ! pc) h stk"

― ‹ naive collection function ›
fun JVMexec_ncollect :: "jvm_prog  jvm_state  cname set" where
"JVMexec_ncollect P (None, h, (stk,loc,C,M,pc,ics)#frs, sh) =
   (JVMstep_ncollect P h stk C M pc ics
        classes_above P C  classes_above_frames P frs  classes_above_xcpts P
   )"
| "JVMexec_ncollect P _ = {}"

(****)

fun JVMNaiveCollect :: "jvm_prog  jvm_state  jvm_state  cname set" where
"JVMNaiveCollect P σ σ' = JVMexec_ncollect P σ"

interpretation JVMNaiveCollectionSemantics:
  CollectionSemantics JVMsmall JVMendset JVMNaiveCollect JVMcombine JVMcollect_id
 by unfold_locales auto

(**************************************)

subsection "Smarter RTS algorithm"

fun JVMinstr_scollect ::
 "[jvm_prog, instr]  cname set" where
"JVMinstr_scollect P (Getstatic C F D)
 = (if ¬(t. P  C has F,Static:t in D) then classes_above P C
    else classes_between P C D - {D})" |
"JVMinstr_scollect P (Putstatic C F D)
 = (if ¬(t. P  C has F,Static:t in D) then classes_above P C
    else classes_between P C D - {D})" |
"JVMinstr_scollect P (Invokestatic C M n)
 = (if ¬(Ts T m D. P  C sees M,Static:Ts  T = m in D) then classes_above P C
    else classes_between P C (fst(method P C M)) - {fst(method P C M)})" |
"JVMinstr_scollect P _ = {}"

fun JVMstep_scollect ::
 "[jvm_prog, instr, init_call_status]  cname set" where
"JVMstep_scollect P i (Calling C' Cs) = {C'}" |
"JVMstep_scollect P i (Called (C'#Cs)) = {}" |
"JVMstep_scollect P i (Throwing Cs a) = {}" |
"JVMstep_scollect P i ics = JVMinstr_scollect P i"

― ‹ smarter collection function ›
fun JVMexec_scollect :: "jvm_prog  jvm_state  cname set" where
"JVMexec_scollect P (None, h, (stk,loc,C,M,pc,ics)#frs, sh) =
   JVMstep_scollect P (instrs_of P C M ! pc) ics"
| "JVMexec_scollect P _ = {}"

(****)

fun JVMSmartCollect :: "jvm_prog  jvm_state  jvm_state  cname set" where
"JVMSmartCollect P σ σ' = JVMexec_scollect P σ"

interpretation JVMSmartCollectionSemantics:
  CollectionSemantics JVMsmall JVMendset JVMSmartCollect JVMcombine JVMcollect_id
 by unfold_locales

(***********************************************)

subsection "A few lemmas using the instantiations"

lemma JVMnaive_csmallD:
"(σ', cset)  JVMNaiveCollectionSemantics.csmall P σ
  JVMexec_ncollect P σ = cset  σ'  JVMsmall P σ"
 by(simp add: JVMNaiveCollectionSemantics.csmall_def)

lemma JVMsmart_csmallD:
"(σ', cset)  JVMSmartCollectionSemantics.csmall P σ
  JVMexec_scollect P σ = cset  σ'  JVMsmall P σ"
 by(simp add: JVMSmartCollectionSemantics.csmall_def)


lemma jvm_naive_to_smart_csmall_nstep_last_eq:
 " (σ',csetn)  JVMNaiveCollectionSemantics.cbig P σ;
    (σ',csetn)  JVMNaiveCollectionSemantics.csmall_nstep P σ n;
    (σ',csets)  JVMSmartCollectionSemantics.csmall_nstep P σ n' 
   n = n'"
proof(induct n arbitrary: n' σ σ' csetn csets)
  case 0
  have "σ' = σ" using "0.prems"(2) JVMNaiveCollectionSemantics.csmall_nstep_base by blast
  then have endset: "σ  JVMendset" using "0.prems"(1) JVMNaiveCollectionSemantics.cbigD by blast
  show ?case
  proof(cases n')
    case Suc then show ?thesis using "0.prems"(3) JVMSmartCollectionSemantics.csmall_nstep_Suc_nend
      endset by blast
  qed(simp)
next
  case (Suc n1)
  then have endset: "σ'  JVMendset" using Suc.prems(1) JVMNaiveCollectionSemantics.cbigD by blast
  have nend: "σ  JVMendset"
   using JVMNaiveCollectionSemantics.csmall_nstep_Suc_nend[OF Suc.prems(2)] by simp
  then have neq: "σ'  σ" using endset by auto
  obtain σ1 cset cset1 where σ1: "(σ1,cset1)  JVMNaiveCollectionSemantics.csmall P σ"
     "csetn = cset1  cset" "(σ',cset)  JVMNaiveCollectionSemantics.csmall_nstep P σ1 n1"
    using JVMNaiveCollectionSemantics.csmall_nstep_SucD[OF Suc.prems(2)] by clarsimp
  then have cbig: "(σ',cset)  JVMNaiveCollectionSemantics.cbig P σ1"
    using endset by(auto simp: JVMNaiveCollectionSemantics.cbig_def)
  show ?case
  proof(cases n')
    case 0 then show ?thesis
      using neq Suc.prems(3) JVMSmartCollectionSemantics.csmall_nstep_base by blast
  next
    case Suc': (Suc n1')
    then obtain σ1' cset2 cset1' where σ1': "(σ1',cset1')  JVMSmartCollectionSemantics.csmall P σ"
      "csets = cset1'  cset2" "(σ',cset2)  JVMSmartCollectionSemantics.csmall_nstep P σ1' n1'"
      using JVMSmartCollectionSemantics.csmall_nstep_SucD[where σ=σ and σ'=σ' and coll'=csets
               and n=n1'] Suc.prems(3) by blast
    then have "σ1=σ1'" using σ1 JVMNaiveCollectionSemantics.csmall_def
      JVMSmartCollectionSemantics.csmall_def by auto
    then show ?thesis using Suc.hyps(1)[OF cbig σ1(3)] σ1'(3) Suc' by blast
  qed
qed

end

Theory JVMExecStepInductive

(*  Title:      RTS/JinjaSuppl/JVMExecStepInductive.thy
    Author:     Susannah Mansky
    2020, UIUC

    Program Execution in the JVM as an inductive
*)

section "Inductive JVM execution"

theory JVMExecStepInductive
imports JinjaDCI.JVMExec
begin

datatype step_input = StepI instr |
                      StepC cname "cname list" | StepC2 cname "cname list" |
                      StepT "cname list" addr


inductive exec_step_ind :: "[step_input, jvm_prog, heap, val list, val list,
                  cname, mname, pc, init_call_status, frame list, sheap,jvm_state]  bool"
where
  exec_step_ind_Load:
"exec_step_ind (StepI (Load n)) P h stk loc C0 M0 pc ics frs sh
   (None, h, ((loc ! n) # stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_Store:
"exec_step_ind (StepI (Store n)) P h stk loc C0 M0 pc ics frs sh
   (None, h, (tl stk, loc[n:=hd stk], C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_Push:
"exec_step_ind (StepI (Push v)) P h stk loc C0 M0 pc ics frs sh
   (None, h, (v # stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

|  exec_step_ind_NewOOM_Called:
"new_Addr h = None
   exec_step_ind (StepI (New C)) P h stk loc C0 M0 pc (Called Cs) frs sh
   (addr_of_sys_xcpt OutOfMemory, h, (stk, loc, C0, M0, pc, No_ics)#frs, sh)"

|  exec_step_ind_NewOOM_Done:
" sh C = Some(obj, Done); new_Addr h = None; Cs. ics  Called Cs 
   exec_step_ind (StepI (New C)) P h stk loc C0 M0 pc ics frs sh
   (addr_of_sys_xcpt OutOfMemory, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

|  exec_step_ind_New_Called:
"new_Addr h = Some a
   exec_step_ind (StepI (New C)) P h stk loc C0 M0 pc (Called Cs) frs sh
   (None, h(ablank P C), (Addr a#stk, loc, C0, M0, Suc pc, No_ics)#frs, sh)"

|  exec_step_ind_New_Done:
" sh C = Some(obj, Done); new_Addr h = Some a; Cs. ics  Called Cs 
   exec_step_ind (StepI (New C)) P h stk loc C0 M0 pc ics frs sh
   (None, h(ablank P C), (Addr a#stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

|  exec_step_ind_New_Init:
" obj. sh C  Some(obj, Done); Cs. ics  Called Cs 
   exec_step_ind (StepI (New C)) P h stk loc C0 M0 pc ics frs sh
   (None, h, (stk, loc, C0, M0, pc, Calling C [])#frs, sh)"

| exec_step_ind_Getfield_Null:
"hd stk = Null
   exec_step_ind (StepI (Getfield F C)) P h stk loc C0 M0 pc ics frs sh
   (addr_of_sys_xcpt NullPointer, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Getfield_NoField:
" v = hd stk; (D,fs) = the(h(the_Addr v)); v  Null; ¬(t b. P  D has F,b:t in C) 
   exec_step_ind (StepI (Getfield F C)) P h stk loc C0 M0 pc ics frs sh
   (addr_of_sys_xcpt NoSuchFieldError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Getfield_Static:
" v = hd stk; (D,fs) = the(h(the_Addr v)); v  Null; P  D has F,Static:t in C 
   exec_step_ind (StepI (Getfield F C)) P h stk loc C0 M0 pc ics frs sh
   (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Getfield:
" v = hd stk; (D,fs) = the(h(the_Addr v)); (D',b,t) = field P C F; v  Null;
   P  D has F,NonStatic:t in C 
   exec_step_ind (StepI (Getfield F C)) P h stk loc C0 M0 pc ics frs sh
   (None, h, (the(fs(F,C))#(tl stk), loc, C0, M0, pc+1, ics)#frs, sh)"

| exec_step_ind_Getstatic_NoField:
"¬(t b. P  C has F,b:t in D)
   exec_step_ind (StepI (Getstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NoSuchFieldError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Getstatic_NonStatic:
"P  C has F,NonStatic:t in D
   exec_step_ind (StepI (Getstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Getstatic_Called:
" (D',b,t) = field P D F; P  C has F,Static:t in D;
   v = the ((fst(the(sh D'))) F) 
   exec_step_ind (StepI (Getstatic C F D)) P h stk loc C0 M0 pc (Called Cs) frs sh
    (None, h, (v#stk, loc, C0, M0, Suc pc, No_ics)#frs, sh)"

| exec_step_ind_Getstatic_Done:
" (D',b,t) = field P D F; P  C has F,Static:t in D;
   Cs. ics  Called Cs; sh D' = Some(sfs,Done);
   v = the (sfs F) 
   exec_step_ind (StepI (Getstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (v#stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_Getstatic_Init:
" (D',b,t) = field P D F; P  C has F,Static:t in D;
   sfs. sh D'  Some(sfs,Done); Cs. ics  Called Cs 
   exec_step_ind (StepI (Getstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Calling D' [])#frs, sh)"

| exec_step_ind_Putfield_Null:
"hd(tl stk) = Null
   exec_step_ind (StepI (Putfield F C)) P h stk loc C0 M0 pc ics frs sh
  (addr_of_sys_xcpt NullPointer, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Putfield_NoField:
" r = hd(tl stk); a = the_Addr r; (D,fs) = the (h a); r  Null; ¬(t b. P  D has F,b:t in C) 
   exec_step_ind (StepI (Putfield F C)) P h stk loc C0 M0 pc ics frs sh
  (addr_of_sys_xcpt NoSuchFieldError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Putfield_Static:
" r = hd(tl stk); a = the_Addr r; (D,fs) = the (h a); r  Null; P  D has F,Static:t in C 
   exec_step_ind (StepI (Putfield F C)) P h stk loc C0 M0 pc ics frs sh
  (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Putfield:
" v = hd stk; r = hd(tl stk); a = the_Addr r; (D,fs) = the (h a); (D',b,t) = field P C F;
   r  Null; P  D has F,NonStatic:t in C 
   exec_step_ind (StepI (Putfield F C)) P h stk loc C0 M0 pc ics frs sh
  (None, h(a  (D, fs((F,C)  v))), (tl (tl stk), loc, C0, M0, pc+1, ics)#frs, sh)"

| exec_step_ind_Putstatic_NoField:
"¬(t b. P  C has F,b:t in D)
   exec_step_ind (StepI (Putstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NoSuchFieldError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Putstatic_NonStatic:
"P  C has F,NonStatic:t in D
   exec_step_ind (StepI (Putstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Putstatic_Called:
" (D',b,t) = field P D F; P  C has F,Static:t in D; the(sh D') = (sfs,i) 
   exec_step_ind (StepI (Putstatic C F D)) P h stk loc C0 M0 pc (Called Cs) frs sh
    (None, h, (tl stk, loc, C0, M0, Suc pc, No_ics)#frs, sh(D':=Some ((sfs(F  hd stk)), i)))"

| exec_step_ind_Putstatic_Done:
" (D',b,t) = field P D F; P  C has F,Static:t in D;
   Cs. ics  Called Cs; sh D' = Some (sfs, Done) 
   exec_step_ind (StepI (Putstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (tl stk, loc, C0, M0, Suc pc, ics)#frs, sh(D':=Some ((sfs(F  hd stk)), Done)))"

| exec_step_ind_Putstatic_Init:
" (D',b,t) = field P D F; P  C has F,Static:t in D;
   sfs. sh D'  Some (sfs, Done); Cs. ics  Called Cs 
   exec_step_ind (StepI (Putstatic C F D)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Calling D' [])#frs, sh)"

| exec_step_ind_Checkcast:
"cast_ok P C h (hd stk)
   exec_step_ind (StepI (Checkcast C)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_Checkcast_Error:
"¬cast_ok P C h (hd stk)
   exec_step_ind (StepI (Checkcast C)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt ClassCast, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke_Null:
"stk!n = Null
   exec_step_ind (StepI (Invoke M n)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NullPointer, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke_NoMethod:
" r = stk!n; C = fst(the(h(the_Addr r))); r  Null;
   ¬(Ts T m D b. P  C sees M,b:Ts  T = m in D) 
   exec_step_ind (StepI (Invoke M n)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NoSuchMethodError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke_Static:
" r = stk!n; C = fst(the(h(the_Addr r)));
   (D,b,Ts,T,mxs,mxl0,ins,xt)= method P C M; r  Null;
   P  C sees M,Static:Ts  T = m in D 
   exec_step_ind (StepI (Invoke M n)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke:
" ps = take n stk; r = stk!n; C = fst(the(h(the_Addr r)));
   (D,b,Ts,T,mxs,mxl0,ins,xt)= method P C M; r  Null;
   P  C sees M,NonStatic:Ts  T = m in D;
   f' = ([],[r]@(rev ps)@(replicate mxl0 undefined),D,M,0,No_ics) 
   exec_step_ind (StepI (Invoke M n)) P h stk loc C0 M0 pc ics frs sh
    (None, h, f'#(stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_NoMethod:
" (D,b,Ts,T,mxs,mxl0,ins,xt)= method P C M; ¬(Ts T m D b. P  C sees M,b:Ts  T = m in D) 
   exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NoSuchMethodError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_NonStatic:
" (D,b,Ts,T,mxs,mxl0,ins,xt)= method P C M; P  C sees M,NonStatic:Ts  T = m in D 
   exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt IncompatibleClassChangeError, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_Called:
" ps  = take n stk; (D,b,Ts,T,mxs,mxl0,ins,xt) = method P C M;
   P  C sees M,Static:Ts  T = m in D;
   f'  = ([],(rev ps)@(replicate mxl0 undefined),D,M,0,No_ics) 
   exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C0 M0 pc (Called Cs) frs sh
    (None, h, f'#(stk, loc, C0, M0, pc, No_ics)#frs, sh)"

| exec_step_ind_Invokestatic_Done:
" ps  = take n stk; (D,b,Ts,T,mxs,mxl0,ins,xt) = method P C M;
   P  C sees M,Static:Ts  T = m in D;
   Cs. ics  Called Cs; sh D = Some (sfs, Done);
   f'  = ([],(rev ps)@(replicate mxl0 undefined),D,M,0,No_ics) 
   exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C0 M0 pc ics frs sh
    (None, h, f'#(stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_Init:
" (D,b,Ts,T,mxs,mxl0,ins,xt) = method P C M;
   P  C sees M,Static:Ts  T = m in D;
   sfs. sh D  Some (sfs, Done); Cs. ics  Called Cs 
   exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Calling D [])#frs, sh)"

| exec_step_ind_Return_Last_Init:
 "exec_step_ind (StepI Return) P h stk0 loc0 C0 clinit pc ics [] sh
    (None, h, [], sh(C0:=Some(fst(the(sh C0)), Done)))"

| exec_step_ind_Return_Last:
 "M0  clinit
    exec_step_ind (StepI Return) P h stk0 loc0 C0 M0 pc ics [] sh (None, h, [], sh)"

| exec_step_ind_Return_Init:
 " (D,b,Ts,T,m) = method P C0 clinit 
    exec_step_ind (StepI Return) P h stk0 loc0 C0 clinit pc ics ((stk',loc',C',m',pc',ics')#frs') sh
     (None, h, (stk',loc',C',m',pc',ics')#frs', sh(C0:=Some(fst(the(sh C0)), Done)))"

| exec_step_ind_Return_NonStatic:
 " (D,NonStatic,Ts,T,m) = method P C0 M0; M0  clinit 
    exec_step_ind (StepI Return) P h stk0 loc0 C0 M0 pc ics ((stk',loc',C',m',pc',ics')#frs') sh
     (None, h, ((hd stk0)#(drop (length Ts + 1) stk'),loc',C',m',Suc pc',ics')#frs', sh)"

| exec_step_ind_Return_Static:
 " (D,Static,Ts,T,m) = method P C0 M0; M0  clinit 
    exec_step_ind (StepI Return) P h stk0 loc0 C0 M0 pc ics ((stk',loc',C',m',pc',ics')#frs') sh
     (None, h, ((hd stk0)#(drop (length Ts) stk'),loc',C',m',Suc pc',ics')#frs', sh)"

| exec_step_ind_Pop:
"exec_step_ind (StepI Pop) P h stk loc C0 M0 pc ics frs sh
  (None, h, (tl stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_IAdd:
"exec_step_ind (StepI IAdd) P h stk loc C0 M0 pc ics frs sh
  (None, h, (Intg (the_Intg (hd (tl stk)) + the_Intg (hd stk))#(tl (tl stk)), loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_IfFalse_False:
"hd stk = Bool False
   exec_step_ind (StepI (IfFalse i)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (tl stk, loc, C0, M0, nat(int pc+i), ics)#frs, sh)"

| exec_step_ind_IfFalse_nFalse:
"hd stk  Bool False
   exec_step_ind (StepI (IfFalse i)) P h stk loc C0 M0 pc ics frs sh
    (None, h, (tl stk, loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_CmpEq:
"exec_step_ind (StepI CmpEq) P h stk loc C0 M0 pc ics frs sh
    (None, h, (Bool (hd (tl stk) = hd stk) # tl (tl stk), loc, C0, M0, Suc pc, ics)#frs, sh)"

| exec_step_ind_Goto:
"exec_step_ind (StepI (Goto i)) P h stk loc C0 M0 pc ics frs sh
   (None, h, (stk, loc, C0, M0, nat(int pc+i), ics)#frs, sh)"

| exec_step_ind_Throw:
"hd stk  Null
   exec_step_ind (StepI Throw) P h stk loc C0 M0 pc ics frs sh
    (the_Addr (hd stk), h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Throw_Null:
"hd stk = Null
   exec_step_ind (StepI Throw) P h stk loc C0 M0 pc ics frs sh
    (addr_of_sys_xcpt NullPointer, h, (stk, loc, C0, M0, pc, ics)#frs, sh)"

| exec_step_ind_Init_None_Called:
" sh C = None 
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Calling C Cs)#frs, sh(C := Some (sblank P C, Prepared)))"

| exec_step_ind_Init_Done:
"sh C = Some (sfs, Done)
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Called Cs)#frs, sh)"

| exec_step_ind_Init_Processing:
"sh C = Some (sfs, Processing)
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Called Cs)#frs, sh)"

| exec_step_ind_Init_Error:
" sh C = Some (sfs, Error) 
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Throwing Cs (addr_of_sys_xcpt NoClassDefFoundError))#frs, sh)"

| exec_step_ind_Init_Prepared_Object:
" sh C = Some (sfs, Prepared);
   sh' = sh(C:=Some(fst(the(sh C)), Processing));
   C = Object 
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Called (C#Cs))#frs, sh')"

| exec_step_ind_Init_Prepared_nObject:
" sh C = Some (sfs, Prepared);
   sh' = sh(C:=Some(fst(the(sh C)), Processing));
   C  Object; D = fst(the(class P C)) 
   exec_step_ind (StepC C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk, loc, C0, M0, pc, Calling D (C#Cs))#frs, sh')"

| exec_step_ind_Init:
"exec_step_ind (StepC2 C Cs) P h stk loc C0 M0 pc ics frs sh
    (None, h, create_init_frame P C#(stk, loc, C0, M0, pc, Called Cs)#frs, sh)"

| exec_step_ind_InitThrow:
"exec_step_ind (StepT (C#Cs) a) P h stk loc C0 M0 pc ics frs sh
    (None, h, (stk,loc,C0,M0,pc,Throwing Cs a)#frs, (sh(C  (fst(the(sh C)), Error))))"

| exec_step_ind_InitThrow_End:
"exec_step_ind (StepT [] a) P h stk loc C0 M0 pc ics frs sh
    (a, h, (stk,loc,C0,M0,pc,No_ics)#frs, sh)"

(** ******* **)

inductive_cases exec_step_ind_cases [cases set]:
 "exec_step_ind (StepI (Load n)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Store n)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Push v)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (New C)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Getfield F C)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Getstatic C F D)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Putfield F C)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Putstatic C F D)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Checkcast C)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Invoke M n)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI Return) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI Pop) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI IAdd) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (IfFalse i)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI CmpEq) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI (Goto i)) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepI Throw) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepC C' Cs) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepC2 C' Cs) P h stk loc C M pc ics frs sh σ"
 "exec_step_ind (StepT Cs a) P h stk loc C M pc ics frs sh σ"


― ‹ Deriving @{term step_input} for @{term exec_step_ind} from @{term exec_step} arguments ›
fun exec_step_input :: "[jvm_prog, cname, mname, pc, init_call_status]  step_input" where
"exec_step_input P C M pc (Calling C' Cs) = StepC C' Cs" |
"exec_step_input P C M pc (Called (C'#Cs)) = StepC2 C' Cs" |
"exec_step_input P C M pc (Throwing Cs a) = StepT Cs a" |
"exec_step_input P C M pc ics = StepI (instrs_of P C M ! pc)"

lemma exec_step_input_StepTD[simp]:
assumes "exec_step_input P C M pc ics = StepT Cs a" shows "ics = Throwing Cs a"
using assms proof(cases ics)
  case (Called Cs) with assms show ?thesis by(cases Cs; simp)
qed(auto)

lemma exec_step_input_StepCD[simp]:
assumes "exec_step_input P C M pc ics = StepC C' Cs" shows "ics = Calling C' Cs"
using assms proof(cases ics)
  case (Called Cs) with assms show ?thesis by(cases Cs; simp)
qed(auto)

lemma exec_step_input_StepC2D[simp]:
assumes "exec_step_input P C M pc ics = StepC2 C' Cs" shows "ics = Called (C'#Cs)"
using assms proof(cases ics)
  case (Called Cs) with assms show ?thesis by(cases Cs; simp)
qed(auto)

lemma exec_step_input_StepID:
assumes "exec_step_input P C M pc ics = StepI i"
shows "(ics = Called []  ics = No_ics)  instrs_of P C M ! pc = i"
using assms proof(cases ics)
  case (Called Cs) with assms show ?thesis by(cases Cs; simp)
qed(auto)

subsection "Equivalence of @{term exec_step} and @{term exec_step_input}"

lemma exec_step_imp_exec_step_ind:
assumes es: "exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')"
shows "exec_step_ind (exec_step_input P C M pc ics) P h stk loc C M pc ics frs sh (xp', h', frs', sh')"
proof(cases "exec_step_input P C M pc ics")
  case (StepT Cs a)
  then have "ics = Throwing Cs a" by simp
  then show ?thesis using exec_step_ind_InitThrow exec_step_ind_InitThrow_End StepT es
   by(cases Cs, auto)
next
  case (StepC C1 Cs)
  then have ics: "ics = Calling C1 Cs" by simp
  obtain D b Ts T m where lets: "method P C1 clinit = (D,b,Ts,T,m)" by(cases "method P C1 clinit")
  then obtain mxs mxl0 ins xt where m: "m = (mxs,mxl0,ins,xt)" by(cases m)
  show ?thesis
  proof(cases "sh C1")
    case None then show ?thesis
     using exec_step_ind_Init_None_Called ics assms by auto
  next
    case (Some a)
    then obtain sfs i where sfsi: "a = (sfs,i)" by(cases a)
    then show ?thesis using exec_step_ind_Init_Done exec_step_ind_Init_Processing
      exec_step_ind_Init_Error m lets Some ics assms
    proof(cases i)
      case Prepared
      show ?thesis
      using exec_step_ind_Init_Prepared_Object[where P=P] exec_step_ind_Init_Prepared_nObject
       sfsi m lets Prepared Some ics assms by(auto split: if_split_asm)
    qed(auto)
  qed
next
  case (StepC2 C1 Cs)
  then have ics: "ics = Called (C1#Cs)" by simp
  then show ?thesis using exec_step_ind_Init assms by auto
next
  case (StepI i)
  then have
    ics: "ics = Called []  ics = No_ics" and
    exec_instr: "exec_instr i P h stk loc C M pc ics frs sh = (xp', h', frs', sh')"
    using assms by(auto dest!: exec_step_input_StepID)
  show ?thesis
  proof(cases i)
    case (Load x1) then show ?thesis using exec_instr exec_step_ind_Load StepI by auto
  next
    case (Store x2) then show ?thesis using exec_instr exec_step_ind_Store StepI by auto
  next
    case (Push x3) then show ?thesis using exec_instr exec_step_ind_Push StepI by auto
  next
    case (New C1)
    then obtain sfs i where sfsi: "the(sh C1) = (sfs,i)" by(cases "the(sh C1)")
    then show ?thesis using exec_step_ind_New_Called exec_step_ind_NewOOM_Called
       exec_step_ind_New_Done exec_step_ind_NewOOM_Done
       exec_step_ind_New_Init sfsi New StepI exec_instr ics by(auto split: init_state.splits)
  next
    case (Getfield F1 C1)
    then obtain D fs D' b t where lets: "the(h(the_Addr (hd stk))) = (D,fs)"
      "field P C1 F1 = (D',b,t)" by(cases "the(h(the_Addr (hd stk)))", cases "field P C1 F1")
    then have "b' t'. P  D has F1,b':t' in C1  (D', b, t) = (C1, b', t')"
      using field_def2 has_field_idemp has_field_sees by fastforce
    then show ?thesis using exec_step_ind_Getfield_Null exec_step_ind_Getfield_NoField
       exec_step_ind_Getfield_Static exec_step_ind_Getfield lets Getfield StepI exec_instr
      by(auto split: if_split_asm staticb.splits) metis+
  next
    case (Getstatic C1 F1 D1)
    then obtain D' b t where lets: "field P D1 F1 = (D',b,t)" by(cases "field P D1 F1")
    then have field: "b' t'. P  C1 has F1,b':t' in D1  (D', b, t) = (D1, b', t')"
      using field_def2 has_field_idemp has_field_sees by fastforce
    show ?thesis
    proof(cases b)
      case NonStatic then show ?thesis
       using exec_step_ind_Getstatic_NoField exec_step_ind_Getstatic_NonStatic
        field lets Getstatic exec_instr StepI by(auto split: if_split_asm) fastforce
    next
      case Static show ?thesis
      proof(cases "ics = Called []")
        case True then show ?thesis using exec_step_ind_Getstatic_NoField
          exec_step_ind_Getstatic_Called exec_step_ind_Getstatic_Init
          Static field lets Getstatic exec_instr StepI ics
         by(auto simp: split_beta split: if_split_asm) metis
      next
        case False
        then have nCalled: "Cs. ics  Called Cs" using ics by simp
        show ?thesis
        proof(cases "sh D1")
          case None
          then have nDone: "sfs. sh D1  Some(sfs, Done)" by simp
          then show ?thesis using exec_step_ind_Getstatic_NoField
            exec_step_ind_Getstatic_Init[where sh=sh, OF _ _ nDone nCalled]
            field lets None False Static Getstatic exec_instr StepI ics
           by(auto split: if_split_asm) metis
        next
          case (Some a)
          then obtain sfs i where sfsi: "a=(sfs,i)" by(cases a)
          show ?thesis using exec_step_ind_Getstatic_NoField
            exec_step_ind_Getstatic_Init sfsi False Static Some field lets Getstatic exec_instr
          proof(cases "i = Done")
            case True then show ?thesis using exec_step_ind_Getstatic_NoField
              exec_step_ind_Getstatic_Done[OF _ _ nCalled] exec_step_ind_Getstatic_Init
              sfsi False Static Some field lets Getstatic exec_instr StepI ics
             by(auto split: if_split_asm) metis
          next
            case nD: False
            then have nDone: "sfs. sh D1  Some(sfs, Done)" using sfsi Some by simp
            show ?thesis using nD
            proof(cases i)
              case Processing then show ?thesis using exec_step_ind_Getstatic_NoField
                exec_step_ind_Getstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Getstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            next
              case Prepared then show ?thesis using exec_step_ind_Getstatic_NoField
                exec_step_ind_Getstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Getstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            next
              case Error then show ?thesis using exec_step_ind_Getstatic_NoField
                exec_step_ind_Getstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Getstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            qed(simp)
          qed
        qed
      qed
    qed
  next
    case (Putfield F1 C1)
    then obtain D fs D' b t where lets: "the(h(the_Addr (hd(tl stk)))) = (D,fs)"
      "field P C1 F1 = (D',b,t)" by(cases "the(h(the_Addr (hd(tl stk))))", cases "field P C1 F1")
    then have "b' t'. P  D has F1,b':t' in C1  (D', b, t) = (C1, b', t')"
      using field_def2 has_field_idemp has_field_sees by fastforce
    then show ?thesis using exec_step_ind_Putfield_Null exec_step_ind_Putfield_NoField
       exec_step_ind_Putfield_Static exec_step_ind_Putfield lets Putfield exec_instr StepI
      by(auto split: if_split_asm staticb.splits) metis+
  next
    case (Putstatic C1 F1 D1)
    then obtain D' b t where lets: "field P D1 F1 = (D',b,t)" by(cases "field P D1 F1")
    then have field: "b' t'. P  C1 has F1,b':t' in D1  (D', b, t) = (D1, b', t')"
      using field_def2 has_field_idemp has_field_sees by fastforce
    show ?thesis
    proof(cases b)
      case NonStatic then show ?thesis
       using exec_step_ind_Putstatic_NoField exec_step_ind_Putstatic_NonStatic
        field lets Putstatic exec_instr StepI by(auto split: if_split_asm) fastforce
    next
      case Static show ?thesis
      proof(cases "ics = Called []")
        case True then show ?thesis using exec_step_ind_Putstatic_NoField
          exec_step_ind_Putstatic_Called exec_step_ind_Putstatic_Init
          Static field lets Putstatic exec_instr StepI ics
         by(cases "the(sh D1)", auto split: if_split_asm) metis
      next
        case False
        then have nCalled: "Cs. ics  Called Cs" using ics by simp
        show ?thesis
        proof(cases "sh D1")
          case None
          then have nDone: "sfs. sh D1  Some(sfs, Done)" by simp
          then show ?thesis using exec_step_ind_Putstatic_NoField
            exec_step_ind_Putstatic_Init[where sh=sh, OF _ _ nDone nCalled]
            field lets None False Static Putstatic exec_instr StepI ics
           by(auto split: if_split_asm) metis
        next
          case (Some a)
          then obtain sfs i where sfsi: "a=(sfs,i)" by(cases a)
          show ?thesis using exec_step_ind_Putstatic_NoField
            exec_step_ind_Putstatic_Init sfsi False Static Some field lets Putstatic exec_instr
          proof(cases "i = Done")
            case True then show ?thesis using exec_step_ind_Putstatic_NoField
              exec_step_ind_Putstatic_Done[OF _ _ nCalled] exec_step_ind_Putstatic_Init
              sfsi False Static Some field lets Putstatic exec_instr StepI ics
             by(auto split: if_split_asm) metis
          next
            case nD: False
            then have nDone: "sfs. sh D1  Some(sfs, Done)" using sfsi Some by simp
            show ?thesis using nD
            proof(cases i)
              case Processing then show ?thesis using exec_step_ind_Putstatic_NoField
                exec_step_ind_Putstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Putstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            next
              case Prepared then show ?thesis using exec_step_ind_Putstatic_NoField
                exec_step_ind_Putstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Putstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            next
              case Error then show ?thesis using exec_step_ind_Putstatic_NoField
                exec_step_ind_Putstatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some field lets Putstatic exec_instr StepI ics
               by(auto split: if_split_asm) metis
            qed(simp)
          qed
        qed
      qed
    qed
  next
    case Checkcast then show ?thesis
     using exec_step_ind_Checkcast exec_step_ind_Checkcast_Error exec_instr StepI
       by(auto split: if_split_asm)
  next
    case (Invoke M1 n) show ?thesis
    proof(cases "stk!n = Null")
      case True then show ?thesis using exec_step_ind_Invoke_Null Invoke exec_instr StepI
       by clarsimp
    next
      case False
      let ?C = "cname_of h (the_Addr (stk ! n))"
      obtain D b Ts T m where method: "method P ?C M1 = (D,b,Ts,T,m)" by(cases "method P ?C M1")
      then obtain mxs mxl0 ins xt where "m = (mxs,mxl0,ins,xt)" by(cases m)
      then show ?thesis using exec_step_ind_Invoke_NoMethod
        exec_step_ind_Invoke_Static exec_step_ind_Invoke method False Invoke exec_instr StepI
       by(auto split: if_split_asm staticb.splits)
    qed
  next
    case (Invokestatic C1 M1 n)
    obtain D b Ts T m where lets: "method P C1 M1 = (D,b,Ts,T,m)" by(cases "method P C1 M1")
    then obtain mxs mxl0 ins xt where m: "m = (mxs,mxl0,ins,xt)" by(cases m)
    have method: "b' Ts' t' m' D'. P  C1 sees M1,b':Ts'  t' = m' in D'
      (D,b,Ts,T,m) = (D',b',Ts',t',m')" using lets by auto
    show ?thesis
    proof(cases b)
      case NonStatic then show ?thesis
       using exec_step_ind_Invokestatic_NoMethod exec_step_ind_Invokestatic_NonStatic
        m method lets Invokestatic exec_instr StepI  by(auto split: if_split_asm)
    next
      case Static show ?thesis
      proof(cases "ics = Called []")
        case True then show ?thesis using exec_step_ind_Invokestatic_NoMethod
          exec_step_ind_Invokestatic_Called exec_step_ind_Invokestatic_Init
          Static m method lets Invokestatic exec_instr StepI ics
         by(auto split: if_split_asm)
      next
        case False
        then have nCalled: "Cs. ics  Called Cs" using ics by simp
        show ?thesis
        proof(cases "sh D")
          case None
          then have nDone: "sfs. sh D  Some(sfs, Done)" by simp
          show ?thesis using exec_step_ind_Invokestatic_NoMethod
            exec_step_ind_Invokestatic_Init[where sh=sh, OF _ _ nDone nCalled]
            method m lets None False Static Invokestatic exec_instr StepI ics
           by(auto split: if_split_asm)
        next
          case (Some a)
          then obtain sfs i where sfsi: "a=(sfs,i)" by(cases a)
          show ?thesis using exec_step_ind_Invokestatic_NoMethod
            exec_step_ind_Invokestatic_Init sfsi False Static Some method lets Invokestatic exec_instr
          proof(cases "i = Done")
            case True then show ?thesis using exec_step_ind_Invokestatic_NoMethod
              exec_step_ind_Invokestatic_Done[OF _ _ _ nCalled] exec_step_ind_Invokestatic_Init
              sfsi False Static Some m method lets Invokestatic exec_instr StepI ics
             by(auto split: if_split_asm)
          next
            case nD: False
            then have nDone: "sfs. sh D  Some(sfs, Done)" using sfsi Some by simp
            show ?thesis using nD
            proof(cases i)
              case Processing then show ?thesis using exec_step_ind_Invokestatic_NoMethod
                exec_step_ind_Invokestatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some m method lets Invokestatic exec_instr StepI ics
               by(auto split: if_split_asm)
            next
              case Prepared then show ?thesis using exec_step_ind_Invokestatic_NoMethod
                exec_step_ind_Invokestatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some m method lets Invokestatic exec_instr StepI ics
               by(auto split: if_split_asm)
            next
              case Error then show ?thesis using exec_step_ind_Invokestatic_NoMethod
                exec_step_ind_Invokestatic_Init[where sh=sh, OF _ _ nDone nCalled]
                sfsi False Static Some m method lets Invokestatic exec_instr StepI ics
               by(auto split: if_split_asm)
            qed(simp)
          qed
        qed
      qed
    qed
  next
    case Return
    obtain D b Ts T m where method: "method P C M = (D,b,Ts,T,m)" by(cases "method P C M")
    then obtain mxs mxl0 ins xt where "m = (mxs,mxl0,ins,xt)" by(cases m)
    then show ?thesis using exec_step_ind_Return_Last_Init exec_step_ind_Return_Last
      exec_step_ind_Return_Init exec_step_ind_Return_NonStatic exec_step_ind_Return_Static
       method Return exec_instr StepI ics
      by(auto split: if_split_asm staticb.splits bool.splits list.splits)
  next
    case Pop then show ?thesis using exec_instr StepI exec_step_ind_Pop by auto
  next
    case IAdd then show ?thesis using exec_instr StepI exec_step_ind_IAdd by auto
  next
    case Goto then show ?thesis using exec_instr StepI exec_step_ind_Goto by auto
  next
    case CmpEq then show ?thesis using exec_instr StepI exec_step_ind_CmpEq by auto
  next
    case (IfFalse x17) then show ?thesis
     using exec_instr StepI exec_step_ind_IfFalse_nFalse exec_step_ind_IfFalse_False
       exec_instr StepI by(auto split: val.splits staticb.splits)
  next
    case Throw then show ?thesis
     using exec_instr StepI exec_step_ind_Throw exec_step_ind_Throw_Null
       by(auto split: val.splits)
  qed
qed

lemma exec_step_ind_imp_exec_step:
assumes esi: "exec_step_ind si P h stk loc C M pc ics frs sh (xp', h', frs', sh')"
  and si: "exec_step_input P C M pc ics = si"
shows "exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')"
proof -
  have StepI:
   "P C M pc Cs i . exec_step_input P C M pc (Called Cs) = StepI i
            instrs_of P C M ! pc = i  Cs = []"
  proof -
    fix P C M pc Cs i show "exec_step_input P C M pc (Called Cs) = StepI i
            instrs_of P C M ! pc = i  Cs = []" by(cases Cs; simp)
  qed
  have StepC:
   "P C M pc ics C' Cs. exec_step_input P C M pc ics = StepC C' Cs  ics = Calling C' Cs"
     by simp
  have StepT:
   "P C M pc ics Cs a. exec_step_input P C M pc ics = StepT Cs a  ics = Throwing Cs a"
     by simp
  show ?thesis using assms
  proof(induct rule: exec_step_ind.induct)
    case (exec_step_ind_NewOOM_Done sh C obj h ics P stk loc C0 M0 pc frs)
    then show ?case by(cases ics, auto)
  next
    case (exec_step_ind_New_Done sh C obj h a ics P stk loc C0 M0 pc frs)
    then show ?case by(cases ics, auto)
  next
    case (exec_step_ind_New_Init sh C ics P h stk loc C0 M0 pc frs)
    then show ?case by(cases ics, auto split: init_state.splits)
  next
    case (exec_step_ind_Getfield_NoField v stk D fs h P F C loc C0 M0 pc ics frs sh)
    then show ?case by(cases "the (h (the_Addr (hd stk)))", cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Getfield_Static v stk D fs h P F t C loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases "the (h (the_Addr (hd stk)))", cases "fst(snd(field P C F))",
        cases ics, auto simp: split_beta dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case (exec_step_ind_Getfield v stk D fs h D' b t P C F loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases "the (h (the_Addr (hd stk)))",
        cases ics; fastforce simp: split_beta dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case (exec_step_ind_Getstatic_NonStatic P C F t D h stk loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases ics; fastforce simp: split_beta split: staticb.splits
                             dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case exec_step_ind_Getstatic_Called
    then show ?case by(fastforce simp: split_beta split: staticb.splits dest!: StepI
                                 dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Getstatic_Done D' b t P D F C ics sh sfs v h stk loc C0 M0 pc frs)
    then show ?case by(cases ics, auto simp: split_beta split: staticb.splits
                                       dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Getstatic_Init D' b t P D F C sh ics h stk loc C0 M0 pc frs)
    then show ?case
       by(cases ics, auto simp: split_beta split: init_state.splits staticb.splits
                          dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Putfield_NoField r stk a D fs h P F C loc C0 M0 pc ics frs sh)
    then show ?case by(cases "the (h (the_Addr (hd(tl stk))))", cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Putfield_Static r stk a D fs h P F t C loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases "the (h (the_Addr (hd(tl stk))))", cases "fst(snd(field P C F))",
        cases ics, auto simp: split_beta dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case (exec_step_ind_Putfield v stk r a D fs h D' b t P C F loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases "the (h (the_Addr (hd(tl stk))))",
        cases ics; fastforce simp: split_beta dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case (exec_step_ind_Putstatic_NonStatic P C F t D h stk loc C0 M0 pc ics frs sh)
    then show ?case
     by(cases ics; fastforce simp: split_beta split: staticb.splits
                             dest: has_field_sees[OF has_field_idemp] dest!: StepI)
  next
    case exec_step_ind_Putstatic_Called
    then show ?case by(fastforce simp: split_beta split: staticb.splits dest!: StepI
                                 dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Putstatic_Done D' b t P D F C ics sh sfs h stk loc C0 M0 pc frs)
    then show ?case by(cases ics, auto simp: split_beta split: staticb.splits
                                       dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Putstatic_Init D' b t P D F C sh ics h stk loc C0 M0 pc frs)
    then show ?case
     by(cases ics, auto simp: split_beta split: staticb.splits init_state.splits
                        dest: has_field_sees[OF has_field_idemp])
  next
    case (exec_step_ind_Invoke ps n stk r C h D b Ts T mxs mxl0 ins xt P M m f' loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics; fastforce dest!: StepI)
  next
    case (exec_step_ind_Invokestatic_Called ps n stk D b Ts T mxs mxl0 ins xt P C M m ics ics' sh)
    then show ?case by(cases ics; fastforce dest!: StepI)
  next
    case (exec_step_ind_Invokestatic_Done ps n stk D b Ts T mxs mxl0 ins xt P C M m ics sh sfs f')
    then show ?case by(cases ics; fastforce)
  next
    case (exec_step_ind_Invokestatic_Init D b Ts T mxs mxl0 ins xt P C M m sh ics n h stk loc C0 M0 pc frs)
    then show ?case by(cases ics; fastforce split: init_state.splits)
  next
    case (exec_step_ind_Return_NonStatic D Ts T m P C0 M0 h stk0 loc0 pc ics stk' loc' C' m' pc' ics' frs' sh)
    then show ?case by(cases "method P C0 M0", cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Return_Static D Ts T m P C0 M0 h stk0 loc0 pc ics stk' loc' C' m' pc' ics' frs' sh)
    then show ?case by(cases "method P C0 M0", cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_IfFalse_nFalse stk i P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases "hd stk"; cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Throw_Null stk P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases "hd stk"; cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Init C Cs P h stk loc C0 M0 pc ics frs sh)
    then have "ics = Called (C#Cs)" by simp
    then show ?case by auto
  (***)
  next
    case (exec_step_ind_Load n P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Store n P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Push v P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_NewOOM_Called h C P stk loc C0 M0 pc frs sh ics')
    then show ?case by(auto dest!: StepI)
  next
    case (exec_step_ind_New_Called h a C P stk loc C0 M0 pc frs sh ics')
    then show ?case by(auto dest!: StepI)
  next
    case (exec_step_ind_Getfield_Null stk F C P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Getstatic_NoField P C F D h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Putfield_Null stk F C P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Putstatic_NoField P C F D h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Checkcast P C h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Checkcast_Error P C h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Invoke_Null stk n M P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Invoke_NoMethod r stk n C h P M loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Invoke_Static r stk n C h D b Ts T mxs mxl0 ins xt P M m loc C0 M0 pc ics)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Invokestatic_NoMethod D b Ts T mxs mxl0 ins xt P C M n h stk loc C0 M0 pc ics)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Invokestatic_NonStatic D b Ts T mxs mxl0 ins xt P C M m n h stk loc C0 M0 pc ics)
    then show ?case by(cases ics, auto dest!: StepI)
  next
  case (exec_step_ind_Return_Last_Init P h stk0 loc0 C0 pc ics sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Return_Last M0 P h stk0 loc0 C0 pc ics sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
  case (exec_step_ind_Return_Init D b Ts T m P C0 h stk0 loc0 pc ics stk' loc' C' m' pc' ics')
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Pop P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_IAdd P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_IfFalse_False stk i P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_CmpEq P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Goto i P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Throw stk P h loc C0 M0 pc ics frs sh)
    then show ?case by(cases ics, auto dest!: StepI)
  next
    case (exec_step_ind_Init_None_Called sh C Cs P h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_Init_Done sh C sfs Cs P h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_Init_Processing sh C sfs Cs P h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_Init_Error sh C sfs Cs P h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_Init_Prepared_Object sh C sfs sh' Cs P h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_Init_Prepared_nObject sh C sfs sh' D P Cs h stk loc C0 M0 pc ics frs)
    then show ?case by(auto dest!: StepC)
  next
    case (exec_step_ind_InitThrow C Cs a P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(auto dest!: StepT)
  next
    case (exec_step_ind_InitThrow_End a P h stk loc C0 M0 pc ics frs sh)
    then show ?case by(auto dest!: StepT)
  qed
qed

― ‹ @{term exec_step} and @{term exec_step_ind} reach the same result given equivalent input ›
lemma exec_step_ind_equiv:
 "exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')
   = exec_step_ind (exec_step_input P C M pc ics) P h stk loc C M pc ics frs sh (xp', h', frs', sh')"
 using exec_step_imp_exec_step_ind exec_step_ind_imp_exec_step by auto

end

Theory JVMCollectionBasedRTS

(* File: RTS/JVM_RTS/JVMCollectionBasedRTS.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)
(* Proof of safety of certain collection based RTS algorithms for Jinja JVM *)

section "Instantiating @{term CollectionBasedRTS} with Jinja JVM"

theory JVMCollectionBasedRTS
imports "../Common/CollectionBasedRTS" JVMCollectionSemantics
   JinjaDCI.BVSpecTypeSafe "../JinjaSuppl/JVMExecStepInductive"

begin

lemma eq_equiv[simp]: "equiv UNIV {(x, y). x = y}"
by(simp add: equiv_def refl_on_def sym_def trans_def)

(**********************************************)
subsection ‹ Some @{text "classes_above"} lemmas ›
(* here because they require ClassAdd/StartProg *)

lemma start_prog_classes_above_Start:
 "classes_above (start_prog P C M) Start = {Object,Start}"
using start_prog_Start_super[of C M P] subcls1_confluent by auto

lemma class_add_classes_above:
assumes ns: "¬ is_class P C" and "¬P  D * C"
shows "classes_above (class_add P (C, cdec)) D = classes_above P D"
using assms by(auto intro: class_add_subcls class_add_subcls_rev)

lemma class_add_classes_above_xcpts:
assumes ns: "¬ is_class P C"
 and ncp: "D. D  sys_xcpts  ¬P  D * C"
shows "classes_above_xcpts (class_add P (C, cdec)) = classes_above_xcpts P"
using assms class_add_classes_above by simp

(*********)
subsection "JVM next-step lemmas for initialization calling"

lemma JVM_New_next_step:
assumes step: "σ'  JVMsmall P σ"
 and nend: "σ  JVMendset"
 and curr: "curr_instr P (hd(frames_of σ)) = New C"
 and nDone: "¬(sfs i. sheap σ C = Some(sfs,i)  i = Done)"
 and ics: "ics_of(hd(frames_of σ)) = No_ics"
shows "ics_of (hd(frames_of σ')) = Calling C []  sheap σ = sheap σ'  σ'  JVMendset"
proof -
  obtain xp h frs sh where σ: "σ=(xp,h,frs,sh)" by(cases σ)
  then obtain f1 frs1 where frs: "frs=f1#frs1" using nend by(cases frs, simp_all add: JVMendset_def)
  then obtain stk loc C' M' pc ics where f1:"f1=(stk,loc,C',M',pc,ics)" by(cases f1)
  have xp: "xp = None" using σ nend by(simp add: JVMendset_def)
  obtain xp' h' frs' sh' where σ': "σ'=(xp',h',frs',sh')" by(cases σ')
  have "ics_of (hd frs') = Calling C []  sh = sh'  frs'  []  xp' = None"
  proof(cases "sh C")
    case None then show ?thesis using σ' xp f1 frs σ assms by auto
  next
    case (Some a)
    then obtain sfs i where a: "a=(sfs,i)" by(cases a)
    then have nDone': "i  Done" using nDone Some f1 frs σ by simp
    show ?thesis using a Some σ' xp f1 frs σ assms by(auto split: init_state.splits)
  qed
  then show ?thesis using ics σ σ' by(cases frs', auto simp: JVMendset_def)
qed

lemma JVM_Getstatic_next_step:
assumes step: "σ'  JVMsmall P σ"
 and nend: "σ  JVMendset"
 and curr: "curr_instr P (hd(frames_of σ)) = Getstatic C F D"
 and fC: "P  C has F,Static:t in D"
 and nDone: "¬(sfs i. sheap σ D = Some(sfs,i)  i = Done)"
 and ics: "ics_of(hd(frames_of σ)) = No_ics"
shows "ics_of (hd(frames_of σ')) = Calling D []  sheap σ = sheap σ'  σ'  JVMendset"
proof -
  obtain xp h frs sh where σ: "σ=(xp,h,frs,sh)" by(cases σ)
  then obtain f1 frs1 where frs: "frs=f1#frs1" using nend by(cases frs, simp_all add: JVMendset_def)
  then obtain stk loc C' M' pc ics where f1:"f1=(stk,loc,C',M',pc,ics)" by(cases f1)
  have xp: "xp = None" using σ nend by(simp add: JVMendset_def)
  obtain xp' h' frs' sh' where σ': "σ'=(xp',h',frs',sh')" by(cases σ')
  have ex': "t b. P  C has F,b:t in D" using fC by auto
  have field: "t. field P D F = (D,Static,t)"
    using fC field_def2 has_field_idemp has_field_sees by blast
  have nCalled': "Cs. ics  Called Cs" using ics f1 frs σ by simp
  have "ics_of (hd frs') = Calling D []  sh = sh'  frs'  []  xp' = None"
  proof(cases "sh D")
    case None then show ?thesis using field ex' σ' xp f1 frs σ assms by auto
  next
    case (Some a)
    then obtain sfs i where a: "a=(sfs,i)" by(cases a)
    show ?thesis using field ex' a Some σ' xp f1 frs σ assms by(auto split: init_state.splits)
  qed
  then show ?thesis using ics σ σ' by(auto simp: JVMendset_def)
qed

lemma JVM_Putstatic_next_step:
assumes step: "σ'  JVMsmall P σ"
 and nend: "σ  JVMendset"
 and curr: "curr_instr P (hd(frames_of σ)) = Putstatic C F D"
 and fC: "P  C has F,Static:t in D"
 and nDone: "¬(sfs i. sheap σ D = Some(sfs,i)  i = Done)"
 and ics: "ics_of(hd(frames_of σ)) = No_ics"
shows "ics_of (hd(frames_of σ')) = Calling D []  sheap σ = sheap σ'  σ'  JVMendset"
proof -
  obtain xp h frs sh where σ: "σ=(xp,h,frs,sh)" by(cases σ)
  then obtain f1 frs1 where frs: "frs=f1#frs1" using nend by(cases frs, simp_all add: JVMendset_def)
  then obtain stk loc C' M' pc ics where f1:"f1=(stk,loc,C',M',pc,ics)" by(cases f1)
  have xp: "xp = None" using σ nend by(simp add: JVMendset_def)
  obtain xp' h' frs' sh' where σ': "σ'=(xp',h',frs',sh')" by(cases σ')
  have ex': "t b. P  C has F,b:t in D" using fC by auto
  have field: "field P D F = (D,Static,t)"
    using fC field_def2 has_field_idemp has_field_sees by blast
  have ics': "ics_of (hd frs') = Calling D []  sh = sh'  frs'  []  xp' = None"
  proof(cases "sh D")
    case None then show ?thesis using field ex' σ' xp f1 frs σ assms by auto
  next
    case (Some a)
    then obtain sfs i where a: "a=(sfs,i)" by(cases a)
    show ?thesis using field ex' a Some σ' xp f1 frs σ assms by(auto split: init_state.splits)
  qed
  then show ?thesis using ics σ σ' by(auto simp: JVMendset_def)
qed

lemma JVM_Invokestatic_next_step:
assumes step: "σ'  JVMsmall P σ"
 and nend: "σ  JVMendset"
 and curr: "curr_instr P (hd(frames_of σ)) = Invokestatic C M n"
 and mC: "P  C sees M,Static:Ts  T = m in D"
 and nDone: "¬(sfs i. sheap σ D = Some(sfs,i)  i = Done)"
 and ics: "ics_of(hd(frames_of σ)) = No_ics"
shows "ics_of (hd(frames_of σ')) = Calling D []  sheap σ = sheap σ'  σ'  JVMendset"
proof -
  obtain xp h frs sh where σ: "σ=(xp,h,frs,sh)" by(cases σ)
  then obtain f1 frs1 where frs: "frs=f1#frs1" using nend by(cases frs, simp_all add: JVMendset_def)
  then obtain stk loc C' M' pc ics where f1:"f1=(stk,loc,C',M',pc,ics)" by(cases f1)
  have xp: "xp = None" using σ nend by(simp add: JVMendset_def)
  obtain xp' h' frs' sh' where σ': "σ'=(xp',h',frs',sh')" by(cases σ')
  have ex': "Ts T m D b. P  C sees M,b:Ts  T = m in D" using mC by fastforce
  have method: "m. method P C M = (D,Static,m)" using mC by(cases m, auto)
  have ics': "ics_of (hd frs') = Calling D []  sh = sh'  frs'  []  xp' = None"
  proof(cases "sh D")
    case None then show ?thesis using method ex' σ' xp f1 frs σ assms by auto
  next
    case (Some a)
    then obtain sfs i where a: "a=(sfs,i)" by(cases a)
    then have nDone': "i  Done" using nDone Some f1 frs σ by simp
    show ?thesis using method ex' a Some σ' xp f1 frs σ assms by(auto split: init_state.splits)
  qed
  then show ?thesis using ics σ σ' by(auto simp: JVMendset_def)
qed

(***********************************************)
subsection "Definitions"

definition main :: "string" where "main = ''main''"
definition Test :: "string" where "Test = ''Test''"
definition test_oracle :: "string" where "test_oracle = ''oracle''"

type_synonym jvm_class = "jvm_method cdecl"
type_synonym jvm_prog_out = "jvm_state × cname set"

text "A deselection algorithm based on classes that have changed from
 @{text P1} to @{text P2}:"
primrec jvm_deselect :: "jvm_prog  jvm_prog_out  jvm_prog  bool" where
"jvm_deselect P1 (σ, cset) P2 = (cset  (classes_changed P1 P2) = {})"

definition jvm_progs :: "jvm_prog set" where
"jvm_progs  {P. wf_jvm_prog P  ¬is_class P Start  ¬is_class P Test
              (b' Ts' T' m' D'. P  Object sees start_m, b' :  Ts'T' = m' in D'
                                             b' = Static  Ts' = []  T' = Void) }"

definition jvm_tests :: "jvm_class set" where
"jvm_tests = {t. fst t = Test
  (P  jvm_progs. wf_jvm_prog (t#P)  (m. t#P  Test sees main,Static: []  Void = m in Test)) }"

abbreviation jvm_make_test_prog :: "jvm_prog  jvm_class  jvm_prog" where
"jvm_make_test_prog P t  start_prog (t#P) (fst t) main"

declare jvm_progs_def [simp]
declare jvm_tests_def [simp]

(*****************************************************************************************)
subsection "Definition lemmas"

lemma jvm_progs_tests_nStart:
assumes P: "P  jvm_progs" and t: "t  jvm_tests"
shows "¬is_class (t#P) Start"
using assms by(simp add: is_class_def class_def Start_def Test_def)

lemma jvm_make_test_prog_classes_above_xcpts:
assumes P: "P  jvm_progs" and t: "t  jvm_tests"
shows "classes_above_xcpts (jvm_make_test_prog P t) = classes_above_xcpts P"
proof -
  have nS: "¬is_class (t#P) Start" by(rule jvm_progs_tests_nStart[OF P t])
  from P have nT: "¬is_class P Test" by simp
  from P t have "wf_syscls (t#P)  wf_syscls P"
    by(simp add: wf_jvm_prog_def wf_jvm_prog_phi_def wf_prog_def)

  then have [simp]: "D. D  sys_xcpts  is_class (t#P) D  is_class P D"
    by(cases t, auto simp: wf_syscls_def is_class_def class_def dest!: weak_map_of_SomeI)
  from wf_nclass_nsub[OF _ _ nS] P t have nspS: "D. D  sys_xcpts  ¬(t#P)  D * Start"
    by(auto simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
  from wf_nclass_nsub[OF _ _ nT] P have nspT: "D. D  sys_xcpts  ¬P  D * Test"
    by(auto simp: wf_jvm_prog_def wf_jvm_prog_phi_def)

  from class_add_classes_above_xcpts[where P="t#P" and C=Start, OF nS nspS]
  have "classes_above_xcpts (jvm_make_test_prog P t) = classes_above_xcpts (t#P)" by simp
  also from class_add_classes_above_xcpts[where P=P and C=Test, OF nT nspT] t
  have " = classes_above_xcpts P" by(cases t, simp)
  finally show ?thesis by simp
qed

lemma jvm_make_test_prog_sees_Test_main:
assumes P: "P  jvm_progs" and t: "t  jvm_tests"
shows "m. jvm_make_test_prog P t  Test sees main, Static :  []Void = m in Test"
proof -
  let ?P = "jvm_make_test_prog P t"
  from P t obtain m where
    meth: "t#P  Test sees main,Static:[]  Void = m in Test" and
    nstart: "¬ is_class (t # P) Start"
   by(auto simp: is_class_def class_def Start_def Test_def)
  from class_add_sees_method[OF meth nstart] show ?thesis by fastforce
qed

(************************************************)
subsection "Naive RTS algorithm"

subsubsection "Definitions"

fun jvm_naive_out :: "jvm_prog  jvm_class  jvm_prog_out set" where
"jvm_naive_out P t = JVMNaiveCollectionSemantics.cbig (jvm_make_test_prog P t) (start_state (t#P))"

abbreviation jvm_naive_collect_start :: "jvm_prog  cname set" where
"jvm_naive_collect_start P  {}"

lemma jvm_naive_out_xcpts_collected:
assumes "o1  jvm_naive_out P t"
shows "classes_above_xcpts (start_prog (t # P) (fst t) main)  snd o1"
using assms
proof -
  obtain σ' coll' where "o1 = (σ', coll')" and
    cbig: "(σ', coll')  JVMNaiveCollectionSemantics.cbig (start_prog (t#P) (fst t) main) (start_state (t#P))"
   using assms by(cases o1, simp)
  with JVMNaiveCollectionSemantics.cbig_stepD[OF cbig start_state_nend]
  show ?thesis by(auto simp: JVMNaiveCollectionSemantics.csmall_def start_state_def)
qed

(***********************************************************)
subsubsection "Naive algorithm correctness"

text "We start with correctness over @{term exec_instr}, then all the
 functions/pieces that are used by naive @{term csmall} (that is, pieces
 used by @{term exec} - such as which frames are used based on @{term ics}
 - and all functions used by the collection function). We then prove that
 @{term csmall} is existence safe, extend this result to @{term cbig}, and
 finally prove the @{term existence_safe} statement over the locale pieces."

― ‹ if collected classes unchanged, @{term exec_instr} unchanged ›
lemma ncollect_exec_instr:
assumes "JVMinstr_ncollect P i h stk  classes_changed P P' = {}"
  and above_C: "classes_above P C  classes_changed P P' = {}"
  and ics: "ics = Called []  ics = No_ics"
  and i: "i = instrs_of P C M ! pc"
shows "exec_instr i P h stk loc C M pc ics frs sh = exec_instr i P' h stk loc C M pc ics frs sh"
using assms proof(cases i)
  case (New C1) then show ?thesis using assms classes_above_blank[of C1 P P']
    by(auto split: init_state.splits option.splits)
next
  case (Getfield F1 C1) show ?thesis
  proof(cases "hd stk = Null")
    case True then show ?thesis using Getfield assms by simp
  next
    case False
    let ?D = "(cname_of h (the_Addr (hd stk)))"
    have D: "classes_above P ?D  classes_changed P P' = {}"
      using False Getfield assms by simp
    show ?thesis
    proof(cases "b t. P  ?D has F1,b:t in C1")
      case True
      then obtain b1 t1 where "P  ?D has F1,b1:t1 in C1" by auto
      then have has: "P'  ?D has F1,b1:t1 in C1"
       using Getfield assms classes_above_has_field[OF D] by auto
      have "P  ?D * C1" using has_field_decl_above True by auto
      then have "classes_above P C1  classes_above P ?D" by(rule classes_above_subcls_subset)
      then have C1: "classes_above P C1  classes_changed P P' = {}" using D by auto
      then show ?thesis using has True Getfield assms classes_above_field[of C1 P P' F1]
        by(cases "field P' C1 F1", cases "the (h (the_Addr (hd stk)))", auto)
    next
      case nex: False
      then have "b t. P'  ?D has F1,b:t in C1"
       using False Getfield assms
         classes_above_has_field2[where C="?D" and P=P and P'=P' and F=F1 and C'=C1]
        by auto
      then show ?thesis using nex Getfield assms classes_above_field[of C1 P P' F1]
        by(cases "field P' C1 F1", cases "the (h (the_Addr (hd stk)))", auto)
    qed
  qed
next
  case (Getstatic C1 F1 D1)
  then have C1: "classes_above P C1  classes_changed P P' = {}" using assms by auto
  show ?thesis
  proof(cases "b t. P  C1 has F1,b:t in D1")
    case True
    then obtain b t where meth: "P  C1 has F1,b:t in D1" by auto
    then have "P  C1 * D1" by(rule has_field_decl_above)
    then have D1: "classes_above P D1  classes_changed P P' = {}"
      using C1 rtrancl_trans by fastforce
    have "P'  C1 has F1,b:t in D1"
     using meth Getstatic assms classes_above_has_field[OF C1] by auto
    then show ?thesis using True D1 Getstatic assms classes_above_field[of D1 P P' F1]
      by(cases "field P' D1 F1", auto)
  next
    case False
    then have "b t. P'  C1 has F1,b:t in D1"
     using Getstatic assms
       classes_above_has_field2[where C=C1 and P=P and P'=P' and F=F1 and C'=D1]
      by auto
    then show ?thesis using False Getstatic assms
      by(cases "field P' D1 F1", auto)
  qed
next
  case (Putfield F1 C1) show ?thesis
  proof(cases "hd(tl stk) = Null")
    case True then show ?thesis using Putfield assms by simp
  next
    case False
    let ?D = "(cname_of h (the_Addr (hd (tl stk))))"
    have D: "classes_above P ?D  classes_changed P P' = {}" using False Putfield assms by simp
    show ?thesis
    proof(cases "b t. P  ?D has F1,b:t in C1")
      case True
      then obtain b1 t1 where "P  ?D has F1,b1:t1 in C1" by auto
      then have has: "P'  ?D has F1,b1:t1 in C1"
       using Putfield assms classes_above_has_field[OF D] by auto
      have "P  ?D * C1" using has_field_decl_above True by auto
      then have "classes_above P C1  classes_above P ?D" by(rule classes_above_subcls_subset)
      then have C1: "classes_above P C1  classes_changed P P' = {}" using D by auto
      then show ?thesis using has True Putfield assms classes_above_field[of C1 P P' F1]
        by(cases "field P' C1 F1", cases "the (h (the_Addr (hd (tl stk))))", auto)
    next
      case nex: False
      then have "b t. P'  ?D has F1,b:t in C1"
       using False Putfield assms
         classes_above_has_field2[where C="?D" and P=P and P'=P' and F=F1 and C'=C1]
        by auto
      then show ?thesis using nex Putfield assms classes_above_field[of C1 P P' F1]
        by(cases "field P' C1 F1", cases "the (h (the_Addr (hd (tl stk))))", auto)
    qed
  qed
next
  case (Putstatic C1 F1 D1)
  then have C1: "classes_above P C1  classes_changed P P' = {}" using Putstatic assms by auto
  show ?thesis
  proof(cases "b t. P  C1 has F1,b:t in D1")
    case True
    then obtain b t where meth: "P  C1 has F1,b:t in D1" by auto
    then have "P  C1 * D1" by(rule has_field_decl_above)
    then have D1: "classes_above P D1  classes_changed P P' = {}"
      using C1 rtrancl_trans by fastforce
    then have "P'  C1 has F1,b:t in D1"
     using meth Putstatic assms classes_above_has_field[OF C1] by auto
    then show ?thesis using True D1 Putstatic assms classes_above_field[of D1 P P' F1]
      by(cases "field P' D1 F1", auto)
  next
    case False
    then have "b t. P'  C1 has F1,b:t in D1"
     using Putstatic assms classes_above_has_field2[where C=C1 and P=P and P'=P' and F=F1 and C'=D1]
      by auto
    then show ?thesis using False Putstatic assms
      by(cases "field P' D1 F1", auto)
  qed
next
  case (Checkcast C1)
  then show ?thesis using assms
  proof(cases "hd stk = Null")
    case False then show ?thesis
     using Checkcast assms classes_above_subcls classes_above_subcls2
      by(simp add: cast_ok_def) blast
  qed(simp add: cast_ok_def)
next
  case (Invoke M n)
  let ?C = "cname_of h (the_Addr (stk ! n))"
  show ?thesis
  proof(cases "stk ! n = Null")
    case True then show ?thesis using Invoke assms by simp
  next
    case False
    then have above: "classes_above P ?C  classes_changed P P' = {}"
      using Invoke assms by simp
    obtain D b Ts T mxs mxl ins xt where meth: "method P' ?C M = (D,b,Ts,T,mxs,mxl,ins,xt)"
      by(cases "method P' ?C M", clarsimp)
    have meq: "method P ?C M = method P' ?C M"
     using classes_above_method[OF above] by simp
    then show ?thesis
    proof(cases "Ts T m D b. P  ?C sees M,b:Ts  T = m in D")
      case nex: False
      then have "¬(Ts T m D b. P'  ?C sees M,b:Ts  T = m in D)"
        using classes_above_sees_method2[OF above, of M] by clarsimp
      then show ?thesis using nex False Invoke by simp
    next
      case True
      then have "Ts T m D b. P'  ?C sees M,b:Ts  T = m in D"
        by(fastforce dest!: classes_above_sees_method[OF above, of M])
      then show ?thesis using meq meth True Invoke by simp
    qed
  qed
next
  case (Invokestatic C1 M n)
  then have above: "classes_above P C1  classes_changed P P' = {}"
    using assms by simp
  obtain D b Ts T mxs mxl ins xt where meth: "method P' C1 M = (D,b,Ts,T,mxs,mxl,ins,xt)"
    by(cases "method P' C1 M", clarsimp)
  have meq: "method P C1 M = method P' C1 M"
   using classes_above_method[OF above] by simp
  show ?thesis
  proof(cases "Ts T m D b. P  C1 sees M,b:Ts  T = m in D")
    case False
    then have "¬(Ts T m D b. P'  C1 sees M,b:Ts  T = m in D)"
      using classes_above_sees_method2[OF above, of M] by clarsimp
    then show ?thesis using False Invokestatic by simp
  next
    case True
    then have "Ts T m D b. P'  C1 sees M,b:Ts  T = m in D"
      by(fastforce dest!: classes_above_sees_method[OF above, of M])
    then show ?thesis using meq meth True Invokestatic by simp
  qed
next
  case Return then show ?thesis using assms classes_above_method[OF above_C]
    by(cases frs, auto)
next
  case (Load x1) then show ?thesis using assms by auto
next
  case (Store x2) then show ?thesis using assms by auto
next
  case (Push x3) then show ?thesis using assms by auto
next
  case (Goto x15) then show ?thesis using assms by auto
next
  case (IfFalse x17) then show ?thesis using assms by auto
qed(auto)


― ‹ if collected classes unchanged, instruction collection unchanged ›
lemma ncollect_JVMinstr_ncollect:
assumes "JVMinstr_ncollect P i h stk  classes_changed P P' = {}"
shows "JVMinstr_ncollect P i h stk = JVMinstr_ncollect P' i h stk"
proof(cases i)
  case (New C1)
  then show ?thesis using assms classes_above_set[of C1 P P'] by auto
next
  case (Getfield F C1) show ?thesis
  proof(cases "hd stk = Null")
    case True then show ?thesis using Getfield assms by simp
  next
    case False
    let ?D = "cname_of h (the_Addr (hd stk))"
    have "classes_above P ?D  classes_changed P P' = {}" using False Getfield assms by auto
    then have "classes_above P ?D = classes_above P' ?D"
      using classes_above_set by blast
    then show ?thesis using assms Getfield by auto
  qed
next
  case (Getstatic C1 P1 D1)
  then have "classes_above P C1  classes_changed P P' = {}" using assms by auto
  then have "classes_above P C1 = classes_above P' C1"
    using classes_above_set assms Getstatic by blast
  then show ?thesis using assms Getstatic  by auto
next
  case (Putfield F C1) show ?thesis
  proof(cases "hd(tl stk) = Null")
    case True then show ?thesis using Putfield assms by simp
  next
    case False
    let ?D = "cname_of h (the_Addr (hd (tl stk)))"
    have "classes_above P ?D  classes_changed P P' = {}" using False Putfield assms by auto
    then have "classes_above P ?D = classes_above P' ?D"
      using classes_above_set by blast
    then show ?thesis using assms Putfield by auto
  qed
next
  case (Putstatic C1 F D1)
  then have "classes_above P C1  classes_changed P P' = {}" using assms by auto
  then have "classes_above P C1 = classes_above P' C1"
    using classes_above_set assms Putstatic by blast
  then show ?thesis using assms Putstatic  by auto
next
  case (Checkcast C1)
  then show ?thesis using assms
   classes_above_set[of "cname_of h (the_Addr (hd stk))" P P'] by auto
next
  case (Invoke M n)
  then show ?thesis using assms
   classes_above_set[of "cname_of h (the_Addr (stk ! n))" P P'] by auto
next
  case (Invokestatic C1 M n)
  then show ?thesis using assms classes_above_set[of C1 P P'] by auto
next
  case Return
  then show ?thesis using assms classes_above_set[of _ P P'] by auto
next
  case Throw
  then show ?thesis using assms
   classes_above_set[of "cname_of h (the_Addr (hd stk))" P P'] by auto
qed(auto)

― ‹ if collected classes unchanged, @{term exec_step} unchanged ›
lemma ncollect_exec_step:
assumes "JVMstep_ncollect P h stk C M pc ics  classes_changed P P' = {}"
  and above_C: "classes_above P C  classes_changed P P' = {}"
shows "exec_step P h stk loc C M pc ics frs sh = exec_step P' h stk loc C M pc ics frs sh"
proof(cases ics)
  case No_ics then show ?thesis
  using ncollect_exec_instr assms classes_above_method[OF above_C, THEN sym]
    by simp
next
  case (Calling C1 Cs)
  then have above_C1: "classes_above P C1  classes_changed P P' = {}"
    using assms(1) by auto
  show ?thesis
  proof(cases "sh C1")
    case None
    then show ?thesis using Calling assms classes_above_sblank[OF above_C1] by simp
  next
    case (Some a)
    then obtain sfs i where sfsi: "a = (sfs, i)" by(cases a)
    then show ?thesis using Calling Some assms
    proof(cases i)
      case Prepared then show ?thesis
       using above_C1 sfsi Calling Some assms classes_above_method[OF above_C1]
         by(simp add: split_beta classes_above_class classes_changed_class[where cn=C1])
    next
      case Error then show ?thesis
       using above_C1 sfsi Calling Some assms classes_above_method[of C1 P P']
         by(simp add: split_beta classes_above_class classes_changed_class[where cn=C1])
    qed(auto)
  qed
next
  case (Called Cs) show ?thesis
  proof(cases Cs)
    case Nil then show ?thesis
    using ncollect_exec_instr assms classes_above_method[OF above_C, THEN sym] Called
      by simp
  next
    case (Cons C1 Cs1)
    then have above_C': "classes_above P C1  classes_changed P P' = {}" using assms Called by auto
    show ?thesis using assms classes_above_method[OF above_C'] Cons Called by simp
  qed
next
  case (Throwing Cs a) then show ?thesis using assms by(cases Cs; simp)
qed

― ‹ if collected classes unchanged, @{term exec_step} collection unchanged ›
lemma ncollect_JVMstep_ncollect:
assumes "JVMstep_ncollect P h stk C M pc ics  classes_changed P P' = {}"
  and above_C: "classes_above P C  classes_changed P P' = {}"
shows "JVMstep_ncollect P h stk C M pc ics = JVMstep_ncollect P' h stk C M pc ics"
proof(cases ics)
  case No_ics then show ?thesis
  using assms ncollect_JVMinstr_ncollect classes_above_method[OF above_C]
   by simp
next
  case (Calling C1 Cs)
  then have above_C: "classes_above P C1  classes_changed P P' = {}"
    using assms(1) by auto
  let ?C = "fst(method P C1 clinit)"
  show ?thesis using Calling assms classes_above_method[OF above_C]
   classes_above_set[OF above_C] by auto
next
  case (Called Cs) show ?thesis
  proof(cases Cs)
    case Nil then show ?thesis
    using assms ncollect_JVMinstr_ncollect classes_above_method[OF above_C] Called
     by simp
  next
    case (Cons C1 Cs1)
    then have above_C1: "classes_above P C1  classes_changed P P' = {}"
      and above_C': "classes_above P (fst (method P C1 clinit))  classes_changed P P' = {}"
     using assms Called by auto
    show ?thesis using assms Cons Called classes_above_set[OF above_C1]
     classes_above_set[OF above_C'] classes_above_method[OF above_C1]
      by simp
  qed
next
  case (Throwing Cs a) then show ?thesis
  using assms classes_above_set[of "cname_of h a" P P'] by simp
qed

― ‹ if collected classes unchanged, @{term classes_above_frames} unchanged ›
lemma ncollect_classes_above_frames:
 "JVMexec_ncollect P (None, h, (stk,loc,C,M,pc,ics)#frs, sh)  classes_changed P P' = {}
  classes_above_frames P frs = classes_above_frames P' frs"
proof(induct frs)
  case (Cons f frs')
  then obtain stk loc C M pc ics where f: "f = (stk,loc,C,M,pc,ics)" by(cases f)
  then have above_C: "classes_above P C  classes_changed P P' = {}" using Cons by auto
  show ?case using f Cons classes_above_subcls[OF above_C]
   classes_above_subcls2[OF above_C] by auto
qed(auto)

― ‹ if collected classes unchanged, @{term classes_above_xcpts} unchanged ›
lemma ncollect_classes_above_xcpts:
assumes "JVMexec_ncollect P (None, h, (stk,loc,C,M,pc,ics)#frs, sh)  classes_changed P P' = {}"
shows "classes_above_xcpts P = classes_above_xcpts P'"
proof -
  have left: "x x'. x'  sys_xcpts  P  x' * x  xasys_xcpts. P'  xa * x"
  proof -
    fix x x'
    assume x': "x'  sys_xcpts" and above: "P  x' * x"
    then show "xasys_xcpts. P'  xa * x" using assms classes_above_subcls[OF _ above]
      by(rule_tac x=x' in bexI) auto
  qed
  have right: "x x'. x'  sys_xcpts  P'  x' * x  xasys_xcpts. P  xa * x"
  proof -
    fix x x'
    assume x': "x'  sys_xcpts" and above: "P'  x' * x"
    then show "xasys_xcpts. P  xa * x" using assms classes_above_subcls2[OF _ above]
      by(rule_tac x=x' in bexI) auto
  qed
  show ?thesis using left right by auto
qed

― ‹ if collected classes unchanged, @{term exec} collection unchanged ›
lemma ncollect_JVMexec_ncollect:
assumes "JVMexec_ncollect P σ  classes_changed P P' = {}"
shows "JVMexec_ncollect P σ = JVMexec_ncollect P' σ"
proof -
  obtain xp h frs sh where σ: "σ = (xp,h,frs,sh)" by(cases σ)
  then show ?thesis using assms
  proof(cases "x. xp = Some x  frs = []")
    case False
    then obtain stk loc C M pc ics frs' where frs: "frs = (stk,loc,C,M,pc,ics)#frs'"
      by(cases frs, auto)
    have step: "JVMstep_ncollect P h stk C M pc ics  classes_changed P P' = {}"
      using False σ frs assms by(cases ics, auto simp: JVMNaiveCollectionSemantics.csmall_def)
    have above_C: "classes_above P C  classes_changed P P' = {}"
      using False σ frs assms by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
    have frames: "classes_above_frames P frs' = classes_above_frames P' frs'"
     using ncollect_classes_above_frames frs σ False assms by simp
    have xcpts: "classes_above_xcpts P = classes_above_xcpts P'"
     using ncollect_classes_above_xcpts frs σ False assms by simp
    show ?thesis using False xcpts frames frs σ ncollect_JVMstep_ncollect[OF step above_C]
        classes_above_subcls[OF above_C] classes_above_subcls2[OF above_C]
      by auto
  qed(auto)
qed

― ‹ if collected classes unchanged, classes above an exception returned
 by @{term exec_instr} unchanged ›
lemma ncollect_exec_instr_xcpts:
assumes collect: "JVMinstr_ncollect P i h stk  classes_changed P P' = {}"
  and xpcollect: "classes_above_xcpts P  classes_changed P P' = {}"
  and prealloc: "preallocated h"
  and σ': "σ' = exec_instr i P h stk loc C M pc ics' frs sh"
  and xp: "fst σ' = Some a"
  and i: "i = instrs_of P C M ! pc"
shows "classes_above P (cname_of h a)  classes_changed P P' = {}"
using assms exec_instr_xcpts[OF σ' xp]
proof(cases i)
  case Throw then show ?thesis using assms by(cases "hd stk", fastforce+)
qed(fastforce+)

― ‹ if collected classes unchanged, classes above an exception returned
 by @{term exec_step} unchanged ›
lemma ncollect_exec_step_xcpts:
assumes collect: "JVMstep_ncollect P h stk C M pc ics  classes_changed P P' = {}"
  and xpcollect: "classes_above_xcpts P  classes_changed P P' = {}"
  and prealloc: "preallocated h"
  and σ': "σ' = exec_step P h stk loc C M pc ics frs sh"
  and xp: "fst σ' = Some a"
shows "classes_above P (cname_of h a)  classes_changed P P' = {}"
proof(cases ics)
  case No_ics then show ?thesis using assms ncollect_exec_instr_xcpts by simp
next
  case (Calling x21 x22)
  then show ?thesis using assms by(clarsimp split: option.splits init_state.splits if_split_asm)
next
  case (Called Cs) then show ?thesis using assms ncollect_exec_instr_xcpts by(cases Cs; simp)
next
  case (Throwing Cs a) then show ?thesis using assms by(cases Cs; simp)
qed

― ‹ if collected classes unchanged, if @{term csmall} returned a result
 under @{term P}, @{term P'} returns the same ›
lemma ncollect_JVMsmall:
assumes collect: "(σ', cset)  JVMNaiveCollectionSemantics.csmall P σ"
  and intersect: "cset  classes_changed P P' = {}"
  and prealloc: "preallocated (fst(snd σ))"
shows "(σ', cset)  JVMNaiveCollectionSemantics.csmall P' σ"
proof -
  obtain xp h frs sh where σ: "σ = (xp,h,frs,sh)" by(cases σ)
  then have prealloc': "preallocated h" using prealloc by simp
  show ?thesis using σ assms
  proof(cases "x. xp = Some x  frs = []")
    case False
    then obtain stk loc C M pc ics frs' where frs: "frs = (stk,loc,C,M,pc,ics)#frs'"
      by(cases frs, auto)
    have step: "JVMstep_ncollect P h stk C M pc ics  classes_changed P P' = {}"
      using False σ frs assms by(cases ics, auto simp: JVMNaiveCollectionSemantics.csmall_def)
    have above_C: "classes_above P C  classes_changed P P' = {}"
      using False σ frs assms by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
    obtain xp1 h1 frs1 sh1 where exec: "exec_step P' h stk loc C M pc ics frs' sh = (xp1,h1,frs1,sh1)"
      by(cases "exec_step P' h stk loc C M pc ics frs' sh")
    have collect: "JVMexec_ncollect P σ = JVMexec_ncollect P' σ"
      using assms ncollect_JVMexec_ncollect by(simp add: JVMNaiveCollectionSemantics.csmall_def)
    have exec_instr: "exec_step P h stk loc C M pc ics frs' sh
      = exec_step P' h stk loc C M pc ics frs' sh"
      using ncollect_exec_step[OF step above_C] σ frs False by simp
    show ?thesis
    proof(cases xp1)
      case None then show ?thesis
      using None σ frs step False assms ncollect_exec_step[OF step above_C] collect exec
        by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
    next
      case (Some a)
      then show ?thesis using σ assms
      proof(cases xp)
        case None
        have frames: "classes_above_frames P (frames_of σ)  classes_changed P P' = {}"
          using None Some frs σ assms by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
        have frsi: "classes_above_frames P frs  classes_changed P P' = {}" using σ frames by simp
        have xpcollect: "classes_above_xcpts P  classes_changed P P' = {}"
          using None Some frs σ assms by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
        have xp: "classes_above P (cname_of h a)  classes_changed P P' = {}"
         using ncollect_exec_step_xcpts[OF step xpcollect prealloc',
             where σ' = "(xp1,h1,frs1,sh1)" and frs=frs' and loc=loc and a=a and sh=sh]
           exec exec_instr Some assms by auto
        show ?thesis using Some exec σ frs False assms exec_instr collect
             classes_above_find_handler[where h=h and sh=sh, OF xp frsi]
         by(auto simp: JVMNaiveCollectionSemantics.csmall_def)
      qed(auto simp: JVMNaiveCollectionSemantics.csmall_def)
    qed
  qed(auto simp: JVMNaiveCollectionSemantics.csmall_def)
qed

― ‹ if collected classes unchanged, if @{term cbig} returned a result
 under @{term P}, @{term P'} returns the same ›
lemma ncollect_JVMbig:
assumes collect: "(σ', cset)  JVMNaiveCollectionSemantics.cbig P σ"
  and intersect: "cset  classes_changed P P' = {}"
  and prealloc: "preallocated (fst(snd σ))"
shows "(σ', cset)  JVMNaiveCollectionSemantics.cbig P' σ"
using JVMNaiveCollectionSemantics.csmall_to_cbig_prop2[where R="λP P' cset. cset  classes_changed P P' = {}"
   and Q="λσ. preallocated (fst(snd σ))" and P=P and P'=P' and σ=σ and σ'=σ' and coll=cset]
   ncollect_JVMsmall JVMsmall_prealloc_pres assms by auto

― ‹ and finally, RTS algorithm based on @{term ncollect} is existence safe ›
theorem jvm_naive_existence_safe:
assumes p: "P  jvm_progs" and "P'  jvm_progs" and t: "t  jvm_tests"
 and out: "o1  jvm_naive_out P t" and "jvm_deselect P o1 P'"
shows "o2  jvm_naive_out P' t. o1 = o2"
using assms
proof -
  let ?P = "start_prog (t#P) (fst t) main"
  let ?P' = "start_prog (t#P') (fst t) main"
  obtain wf_md where wf': "wf_prog wf_md (t#P)" using p t
   by(auto simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
  have ns: "¬is_class (t#P) Start" using p t
   by(clarsimp simp: is_class_def class_def Start_def Test_def)
  obtain σ1 coll1 where o1: "o1 = (σ1, coll1)" by(cases o1)
  then have cbig: "(σ1, coll1)  JVMNaiveCollectionSemantics.cbig ?P (start_state (t # P))"
   using assms by simp
  have "coll1  classes_changed P P' = {}" using cbig o1 assms by auto
  then have changed: "coll1  classes_changed (t#P) (t#P') = {}" by(rule classes_changed_int_Cons)
  then have changed': "coll1  classes_changed ?P ?P' = {}" by(rule classes_changed_int_Cons)
  have "classes_above_xcpts ?P = classes_above_xcpts (t#P)"
    using class_add_classes_above[OF ns wf_sys_xcpt_nsub_Start[OF wf' ns]] by simp
  then have "classes_above_xcpts (t#P)  classes_changed (t#P) (t#P') = {}"
   using jvm_naive_out_xcpts_collected[OF out] o1 changed by auto
  then have ss_eq: "start_state (t#P) = start_state (t#P')"
    using classes_above_start_state by simp
  show ?thesis using ncollect_JVMbig[OF cbig changed']
    preallocated_start_state changed' ss_eq o1 assms by auto
qed

― ‹ ...thus @{term JVMNaiveCollection} is an instance of @{term CollectionBasedRTS}
interpretation JVMNaiveCollectionRTS :
  CollectionBasedRTS "(=)" jvm_deselect jvm_progs jvm_tests
     JVMendset JVMcombine JVMcollect_id JVMsmall JVMNaiveCollect jvm_naive_out
     jvm_make_test_prog jvm_naive_collect_start
 by unfold_locales (rule jvm_naive_existence_safe, auto simp: start_state_def)

(***********************************************************************************************)
subsection "Smarter RTS algorithm"

subsubsection "Definitions and helper lemmas"

fun jvm_smart_out :: "jvm_prog  jvm_class  jvm_prog_out set" where
"jvm_smart_out P t
 = {(σ',coll'). coll. (σ',coll)  JVMSmartCollectionSemantics.cbig
                                       (jvm_make_test_prog P t) (start_state (t#P))
                             coll' = coll  classes_above_xcpts P  {Object,Start}}"

abbreviation jvm_smart_collect_start :: "jvm_prog  cname set" where
"jvm_smart_collect_start P  classes_above_xcpts P  {Object,Start}"


lemma jvm_naive_iff_smart:
"(csetn. (σ',csetn)  jvm_naive_out P t)  (csets. (σ',csets)  jvm_smart_out P t)"
 by(auto simp: JVMNaiveCollectionSemantics.cbig_big_equiv
               JVMSmartCollectionSemantics.cbig_big_equiv)

(**************************************************)

lemma jvm_smart_out_classes_above_xcpts:
assumes s: "(σ',csets)  jvm_smart_out P t" and P: "P  jvm_progs" and t: "t  jvm_tests"
shows "classes_above_xcpts (jvm_make_test_prog P t)  csets"
 using jvm_make_test_prog_classes_above_xcpts[OF P t] s by clarsimp

lemma jvm_smart_collect_start_make_test_prog:
 " P  jvm_progs; t  jvm_tests 
   jvm_smart_collect_start (jvm_make_test_prog P t) = jvm_smart_collect_start P"
 using jvm_make_test_prog_classes_above_xcpts by simp

lemma jvm_smart_out_classes_above_start_heap:
assumes s: "(σ',csets)  jvm_smart_out P t" and h: "start_heap (t#P) a = Some(C,fs)"
 and P: "P  jvm_progs" and t: "t  jvm_tests"
shows "classes_above (jvm_make_test_prog P t) C  csets"
using start_heap_classes[OF h] jvm_smart_out_classes_above_xcpts[OF s P t] by auto

lemma jvm_smart_out_classes_above_start_sheap:
assumes "(σ',csets)  jvm_smart_out P t" and "start_sheap C = Some(sfs,i)"
shows "classes_above (jvm_make_test_prog P t) C  csets"
using assms start_prog_classes_above_Start by(clarsimp split: if_split_asm)

lemma jvm_smart_out_classes_above_frames:
 "(σ',csets)  jvm_smart_out P t
    classes_above_frames (jvm_make_test_prog P t) (frames_of (start_state (t#P)))  csets"
using start_prog_classes_above_Start by(clarsimp split: if_split_asm simp: start_state_def)

(**************************************************)
subsubsection "Additional well-formedness conditions"

― ‹ returns class to be initialized by given instruction, if applicable ›
(* NOTE: similar to exp-taking init_class from J/EConform - but requires field existence checks *)
fun coll_init_class :: "'m prog  instr  cname option" where
"coll_init_class P (New C) = Some C" |
"coll_init_class P (Getstatic C F D) = (if t.