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: "o⇩0 ∈ out (Ps!0) t" and
des: "∀n < (length Ps) - 1. deselect (Ps!n) o⇩0 (Ps!(Suc n))"
shows "∃o⇩n ∈ out (last Ps) t. equiv_out o⇩0 o⇩n"
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"
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 "o⇩0 ∈ 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) o⇩0 (take (Suc x') Ps ! (Suc n))"
using Suc.prems(5) len' by simp
ultimately have "∃o'∈out (last ?Ps) t. equiv_out o⇩0 o'" by(rule Suc'.prems(1)[of ?Ps])
then obtain o' where o': "o' ∈ out (last ?Ps) t" and eo: "equiv_out o⇩0 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)) o⇩0 (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 "∃o⇩n ∈ out (last Ps) t. equiv_out o' o⇩n"
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 o⇩n where oN: "o⇩n ∈ out (last Ps) t" and eo': "equiv_out o' o⇩n" by clarify
moreover from eo eo' have "equiv_out o⇩0 o⇩n" 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 σ"

lemma bigD:
"⟦ σ' ∈ big P σ ⟧ ⟹ ∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset"

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

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"

lemma cbigD':
"⟦ o' ∈ cbig P σ ⟧ ⟹ ∃n. o' ∈ csmall_nstep P σ n ∧ fst o' ∈ endset"

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
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"

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
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"

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')"

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
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'"

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
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 ≡ ⋃x∈sys_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: Ts→T = m in C' ⟧
⟹ P' ⊢ C sees M,b: Ts→T = 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: Ts→T = m in C' ⟧
⟹ P ⊢ C sees M,b: Ts→T = 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 :  Ts→T = 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 :  Ts→T = 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"

lemma classes_above_blank:
"⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
⟹
blank P C = blank P' C"

lemma classes_above_isfields:
"⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
⟹
isfields P C = isfields P' C"

lemma classes_above_sblank:
"⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
⟹
sblank P C = sblank P' C"

(******************************************)
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 σ"

lemma JVMsmart_csmallD:
"(σ', cset) ∈ JVMSmartCollectionSemantics.csmall P σ
⟹ JVMexec_scollect P σ = cset ∧ σ' ∈ JVMsmall P σ"

lemma jvm_naive_to_smart_csmall_nstep_last_eq:
"⟦ (σ',cset⇩n) ∈ JVMNaiveCollectionSemantics.cbig P σ;
(σ',cset⇩n) ∈ JVMNaiveCollectionSemantics.csmall_nstep P σ n;
(σ',cset⇩s) ∈ JVMSmartCollectionSemantics.csmall_nstep P σ n' ⟧
⟹ n = n'"
proof(induct n arbitrary: n' σ σ' cset⇩n cset⇩s)
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 σ"
"cset⇩n = 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 σ"
"cset⇩s = cset1' ∪ cset2" "(σ',cset2) ∈ JVMSmartCollectionSemantics.csmall_nstep P σ1' n1'"
using JVMSmartCollectionSemantics.csmall_nstep_SucD[where σ=σ and σ'=σ' and coll'=cset⇩s
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
begin

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

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 (StepI (Load n)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, ((loc ! n) # stk, loc, C⇩0, M⇩0, Suc pc, ics)#frs, sh)"

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

| exec_step_ind_Push:
"exec_step_ind (StepI (Push v)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, (v # stk, loc, C⇩0, M⇩0, Suc pc, ics)#frs, sh)"

|  exec_step_ind_NewOOM_Called:
⟹ exec_step_ind (StepI (New C)) P h stk loc C⇩0 M⇩0 pc (Called Cs) frs sh
(⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

|  exec_step_ind_New_Called:
⟹ exec_step_ind (StepI (New C)) P h stk loc C⇩0 M⇩0 pc (Called Cs) frs sh
(None, h(a↦blank P C), (Addr a#stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h(a↦blank P C), (Addr a#stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, pc, Calling C [])#frs, sh)"

| exec_step_ind_Getfield_Null:
"hd stk = Null
⟹ exec_step_ind (StepI (Getfield F C)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchFieldError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (the(fs(F,C))#(tl stk), loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchFieldError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc (Called Cs) frs sh
(None, h, (v#stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (v#stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchFieldError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h(a ↦ (D, fs((F,C) ↦ v))), (tl (tl stk), loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchFieldError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc (Called Cs) frs sh
(None, h, (tl stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (tl stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt ClassCast⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke_Null:
"stk!n = Null
⟹ exec_step_ind (StepI (Invoke M n)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchMethodError⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Invoke_Static:
"⟦ r = stk!n; C = fst(the(h(the_Addr r)));
(D,b,Ts,T,mxs,mxl⇩0,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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, 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,mxl⇩0,ins,xt)= method P C M; r ≠ Null;
P ⊢ C sees M,NonStatic:Ts → T = m in D;
f' = ([],[r]@(rev ps)@(replicate mxl⇩0 undefined),D,M,0,No_ics) ⟧
⟹ exec_step_ind (StepI (Invoke M n)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, f'#(stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_NoMethod:
"⟦ (D,b,Ts,T,mxs,mxl⇩0,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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NoSuchMethodError⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_NonStatic:
"⟦ (D,b,Ts,T,mxs,mxl⇩0,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 C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt IncompatibleClassChangeError⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

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

| exec_step_ind_Invokestatic_Done:
"⟦ ps  = take n stk; (D,b,Ts,T,mxs,mxl⇩0,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 mxl⇩0 undefined),D,M,0,No_ics) ⟧
⟹ exec_step_ind (StepI (Invokestatic C M n)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, f'#(stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Invokestatic_Init:
"⟦ (D,b,Ts,T,mxs,mxl⇩0,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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, pc, Calling D [])#frs, sh)"

| exec_step_ind_Return_Last_Init:
"exec_step_ind (StepI Return) P h stk⇩0 loc⇩0 C⇩0 clinit pc ics [] sh
(None, h, [], sh(C⇩0:=Some(fst(the(sh C⇩0)), Done)))"

| exec_step_ind_Return_Last:
"M⇩0 ≠ clinit
⟹ exec_step_ind (StepI Return) P h stk⇩0 loc⇩0 C⇩0 M⇩0 pc ics [] sh (None, h, [], sh)"

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

| exec_step_ind_Return_NonStatic:
"⟦ (D,NonStatic,Ts,T,m) = method P C⇩0 M⇩0; M⇩0 ≠ clinit ⟧
⟹ exec_step_ind (StepI Return) P h stk⇩0 loc⇩0 C⇩0 M⇩0 pc ics ((stk',loc',C',m',pc',ics')#frs') sh
(None, h, ((hd stk⇩0)#(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 C⇩0 M⇩0; M⇩0 ≠ clinit ⟧
⟹ exec_step_ind (StepI Return) P h stk⇩0 loc⇩0 C⇩0 M⇩0 pc ics ((stk',loc',C',m',pc',ics')#frs') sh
(None, h, ((hd stk⇩0)#(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 C⇩0 M⇩0 pc ics frs sh
(None, h, (tl stk, loc, C⇩0, M⇩0, Suc pc, ics)#frs, sh)"

"exec_step_ind (StepI IAdd) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, (Intg (the_Intg (hd (tl stk)) + the_Intg (hd stk))#(tl (tl stk)), loc, C⇩0, M⇩0, Suc pc, ics)#frs, sh)"

| exec_step_ind_IfFalse_False:
"hd stk = Bool False
⟹ exec_step_ind (StepI (IfFalse i)) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, (tl stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (tl stk, loc, C⇩0, M⇩0, Suc pc, ics)#frs, sh)"

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

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

| exec_step_ind_Throw:
"hd stk ≠ Null
⟹ exec_step_ind (StepI Throw) P h stk loc C⇩0 M⇩0 pc ics frs sh
(⌊the_Addr (hd stk)⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Throw_Null:
"hd stk = Null
⟹ exec_step_ind (StepI Throw) P h stk loc C⇩0 M⇩0 pc ics frs sh
(⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc, ics)#frs, sh)"

| exec_step_ind_Init_None_Called:
"⟦ sh C = None ⟧
⟹ exec_step_ind (StepC C Cs) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, 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 C⇩0 M⇩0 pc ics frs sh
(None, h, (stk, loc, C⇩0, M⇩0, pc, Calling D (C#Cs))#frs, sh')"

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

| exec_step_ind_InitThrow:
"exec_step_ind (StepT (C#Cs) a) P h stk loc C⇩0 M⇩0 pc ics frs sh
(None, h, (stk,loc,C⇩0,M⇩0,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 C⇩0 M⇩0 pc ics frs sh
(⌊a⌋, h, (stk,loc,C⇩0,M⇩0,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 mxl⇩0 ins xt where m: "m = (mxs,mxl⇩0,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 mxl⇩0 ins xt where "m = (mxs,mxl⇩0,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 mxl⇩0 ins xt where m: "m = (mxs,mxl⇩0,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 mxl⇩0 ins xt where "m = (mxs,mxl⇩0,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
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 C⇩0 M⇩0 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 C⇩0 M⇩0 pc frs)
then show ?case by(cases ics, auto)
next
case (exec_step_ind_New_Init sh C ics P h stk loc C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 mxl⇩0 ins xt P M m f' loc C⇩0 M⇩0 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 mxl⇩0 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 mxl⇩0 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 mxl⇩0 ins xt P C M m sh ics n h stk loc C⇩0 M⇩0 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 C⇩0 M⇩0 h stk⇩0 loc⇩0 pc ics stk' loc' C' m' pc' ics' frs' sh)
then show ?case by(cases "method P C⇩0 M⇩0", cases ics, auto dest!: StepI)
next
case (exec_step_ind_Return_Static D Ts T m P C⇩0 M⇩0 h stk⇩0 loc⇩0 pc ics stk' loc' C' m' pc' ics' frs' sh)
then show ?case by(cases "method P C⇩0 M⇩0", cases ics, auto dest!: StepI)
next
case (exec_step_ind_IfFalse_nFalse stk i P h loc C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Store n P h stk loc C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Push v P h stk loc C⇩0 M⇩0 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 C⇩0 M⇩0 pc frs sh ics')
then show ?case by(auto dest!: StepI)
next
case (exec_step_ind_New_Called h a C P stk loc C⇩0 M⇩0 pc frs sh ics')
then show ?case by(auto dest!: StepI)
next
case (exec_step_ind_Getfield_Null stk F C P h loc C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Checkcast P C h stk loc C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 mxl⇩0 ins xt P M m loc C⇩0 M⇩0 pc ics)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Invokestatic_NoMethod D b Ts T mxs mxl⇩0 ins xt P C M n h stk loc C⇩0 M⇩0 pc ics)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Invokestatic_NonStatic D b Ts T mxs mxl⇩0 ins xt P C M m n h stk loc C⇩0 M⇩0 pc ics)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Return_Last_Init P h stk⇩0 loc⇩0 C⇩0 pc ics sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Return_Last M⇩0 P h stk⇩0 loc⇩0 C⇩0 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 C⇩0 h stk⇩0 loc⇩0 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 C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_IAdd P h stk loc C⇩0 M⇩0 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 C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_CmpEq P h stk loc C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Goto i P h stk loc C⇩0 M⇩0 pc ics frs sh)
then show ?case by(cases ics, auto dest!: StepI)
next
case (exec_step_ind_Throw stk P h loc C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 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 C⇩0 M⇩0 pc ics frs)
then show ?case by(auto dest!: StepC)
next
case (exec_step_ind_InitThrow C Cs a P h stk loc C⇩0 M⇩0 pc ics frs sh)
then show ?case by(auto dest!: StepT)
next
case (exec_step_ind_InitThrow_End a P h stk loc C⇩0 M⇩0 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

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

assumes ns: "¬ is_class P C" and "¬P ⊢ D ≼⇧* C"
shows "classes_above (class_add P (C, cdec)) D = classes_above P D"

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"

(*********)
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"

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"

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
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 ⟹ ∃xa∈sys_xcpts. P' ⊢ xa ≼⇧* x"
proof -
fix x x'
assume x': "x' ∈ sys_xcpts" and above: "P ⊢ x' ≼⇧* x"
then show "∃xa∈sys_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 ⟹ ∃xa∈sys_xcpts. P ⊢ xa ≼⇧* x"
proof -
fix x x'
assume x': "x' ∈ sys_xcpts" and above: "P' ⊢ x' ≼⇧* x"
then show "∃xa∈sys_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:
"(∃cset⇩n. (σ',cset⇩n) ∈ jvm_naive_out P t) ⟷ (∃cset⇩s. (σ',cset⇩s) ∈ 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: "(σ',cset⇩s) ∈ 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) ⊆ cset⇩s"
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: "(σ',cset⇩s) ∈ 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 ⊆ cset⇩s"
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 "(σ',cset⇩s) ∈ jvm_smart_out P t" and "start_sheap C = Some(sfs,i)"
shows "classes_above (jvm_make_test_prog P t) C ⊆ cset⇩s"
using assms start_prog_classes_above_Start by(clarsimp split: if_split_asm)

lemma jvm_smart_out_classes_above_frames:
"(σ',cset⇩s) ∈ jvm_smart_out P t
⟹ classes_above_frames (jvm_make_test_prog P t) (frames_of (start_state (t#P))) ⊆ cset⇩s"
using start_prog_classes_above_Start by(clarsimp split: if_split_asm simp: start_state_def)

(**************************************************)
"coll_init_class P (Getstatic C F D) = (if ∃t.