Up to index of Isabelle/HOL/SafeImp
theory dem_PUSHCONT(*
Title: Lemmas for the translation SVM to JVM. PUSHCONT
Author: Javier de Dios and Ricardo Pe~na
Copyright: January 2009, Universidad Complutense de Madrid
*)
header {* Lemmas on the dynamic properties of the translation SVM to JVM *}
theory dem_PUSHCONT
imports "../JVMSAFE/JVMExec" SVM2JVM SVMSemantics CertifSVM2JVM
dem_translation
begin
no_translations "Norm s" == "(None,s)"
no_translations "ex_table_of m" == "snd (snd (snd m))"
declare trInstr.simps [simp del]
declare equivS.simps [simp del]
(* Axioms *)
axioms maxPush_PUSHCONT:
"2 + n < int m"
(* Lemmas for equivS *)
lemma equivS_PUSHCONT_aux:
"equivS (v1#S) S' n ctm d g
==> n + 1 >= 0"
apply (induct S)
apply (case_tac v1,simp_all)
apply (unfold equivS.simps)
apply (case_tac "(nat n)", simp, simp)
apply (case_tac "nata", simp, simp)
apply (case_tac x,simp)
apply (simp add: equivS.simps)
apply (case_tac v1,simp_all)
apply (simp add: equivS.simps)
apply (simp add: equivS.simps)
apply (case_tac x)
by (simp add: equivS.simps)
lemma equivS_PUSHCONT:
"equivS (drop (Suc 0) S) S' n ctm d g ==> n + 1 >= 0"
apply (induct S)
apply (simp add: equivS.simps,simp)
apply (case_tac S,simp)
by (simp,erule equivS_PUSHCONT_aux)
lemma equivS_good:
" equivS S S' n ctm d g ==> 1 ≤ 2 + n"
apply (induct S)
apply (unfold equivS.simps, simp, clarsimp)
apply (case_tac a, simp_all)
apply (simp add: equivS.simps)
apply (simp add: equivS.simps)
apply (case_tac x)
by (simp add: equivS.simps)
axioms equiv_ctm:
"the (ctm p) = the (ctm' p)"
lemma equivS_PUSHCONT_S2:
"[| equivS S S' n ctm d g |]
==> equivS (Cont (nat (the_Intg (the (sha (heapC, k0f)))), p) # S)
(S'(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f)))) (2 + n) ctm d g"
apply (frule equivS_good)
apply (unfold equivS.simps)
apply (rule conjI, simp)
apply (rule conjI, clarsimp)
apply (rule conjI, auto)
apply (rule equiv_ctm)
apply (drule equivS_ge_n, erule_tac x="1" in allE,simp)
apply (subgoal_tac "1 + n = n + 1",simp) prefer 2 apply simp
by (drule equivS_ge_n, erule_tac x="2" in allE,simp)
(* Lemmas for activeCells *)
lemma activeCells_PUSHCONT:
"[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))|]
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS (h(la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg (int (the (ctm p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))))
(nat (the_Intg (the (sha (heapC, kf)))))"
apply (frule l_not_in_cellReg)
apply (unfold activeCells_def,auto)
apply (unfold region_def, simp add: Let_def, elim conjE)
apply (rule_tac x="j" in exI,simp)
apply (rule cellReg_step)
apply (rule cellReg_basic)
apply (erule_tac x="j" in allE)
apply (rule cellsReg_monotone_1,assumption+)
apply (erule l_not_in_regs)
apply (simp add: Let_def, elim conjE)
apply (rule_tac x="j" in exI, simp)
apply (rule cellReg_step)
apply (rule cellReg_basic)
apply (erule_tac x="j" in allE)
apply (erule cellsReg_monotone_2,assumption+)
by (erule l_not_in_regs)
(* Lemmas for domH *)
lemma domH_PUSHCONT:
"[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
∀l∈dom H. ∃l'. l' = the (g l) ∧ equivC (the (H l)) h l' (the (h l')) (nat (the_Intg (the (sha (heapC, kf))))) com regS d g |]
==> ∀l∈dom H.
∃l'. l' = the (g l) ∧
equivC (the (H l)) (h(la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg (int (the (ctm p))),
nat (2 + n) \<mapsto> the (sha (heapC, k0f))))))
l' (the ((h(la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg (int (the (ctm p))),
nat (2 + n) \<mapsto> the (sha (heapC, k0f)))))) l'))
(nat (the_Intg (the (sha (heapC, kf)))))
com regS d g"
apply (frule l_not_in_cellReg)
apply (rule ballI)
apply (erule_tac x="l" in ballE)
prefer 2 apply simp
apply (erule exE)
apply (rule_tac x="l'" in exI) apply (elim conjE)
apply (rule conjI, assumption)
apply clarsimp
apply (rule conjI) apply (rule impI)
apply clarsimp apply (simp add: region_def)
apply clarsimp
apply (rule_tac x="Obj" in exI)
apply (rule_tac x="flds" in exI) apply simp
apply (simp add: region_def) apply (elim conjE)
apply (rule cellReg_step)
apply (rule cellReg_basic)
apply (erule_tac x="j" in allE)
apply (rule cellsReg_monotone_1,assumption+)
by (erule l_not_in_regs)
(* Lemmas for equivH *)
declare equivH.simps [simp del]
lemma equivH_PUSHCONT:
"[| ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
k' = nat (the_Intg (the (sha (heapC, kf))));
equivH (H, ka) h k' com regS d g;
activeCells regS h k' ∩ {la, l', l''} = {}|]
==> equivH (hm, k) (h(la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg (int (the (ctm p))),
nat (2 + n) \<mapsto> the (sha (heapC, k0f))))))
(nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n + 1 + 1),
(heapC, k0f) \<mapsto> the (sha (heapC, kf)))) (heapC, kf))))) com regS d g"
apply simp apply (elim conjE)
apply (frule l_not_in_cellReg)
apply (simp add: heapC_def add: stackC_def)
apply (simp add: kf_def add: k0f_def)
apply (fold heapC_def, fold kf_def, fold k0f_def)
apply (unfold equivH.simps)
apply (elim conjE)
apply (rule conjI, simp)
apply (rule conjI) apply (frule activeCells_PUSHCONT,simp)
apply (rule conjI, assumption)
by (rule domH_PUSHCONT,assumption+)
declare exec_instr.simps [simp]
lemma execSVMInstr_PUSHCONT :
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
cdm , ctm, com \<turnstile> ((hm, k), k0, (l, i), S) \<triangleq> S1';
(fst (the (map_of svms l)) ! i) = PUSHCONT p;
execSVMInst (PUSHCONT p) (map_of ct) (hm, k) k0 (l, i) S = Either.Right S2;
drop (the (cdm (l, i))) (extractBytecode P') =
trInstr (the (cdm (l, i))) cdm' ctm' com pcc (PUSHCONT p) @ bytecode'
|] ==> ∃ v' sh' dh' ih' fms' .
P' \<turnstile> S1' -jvm-> (v',sh',dh',ih', fms') ∧
cdm , ctm, com \<turnstile> S2 \<triangleq> (v',sh',dh',ih', fms')"
(* First, we make the tuples explicit *)
apply (case_tac S1')
apply (rename_tac v tup)
apply (case_tac tup)
apply (rename_tac sh tup)
apply (case_tac tup)
apply (rename_tac dh tup)
apply (case_tac tup)
apply (rename_tac ih fms)
apply (simp)
apply (subgoal_tac "∃ S'. S = drop (Suc 0) S'")
prefer 2 apply (rule_tac x="snd (snd (snd S2))" in exI, clarsimp)
apply (unfold equivState_def)
apply (elim exE,elim conjE)
(* we go on with the main goal. We instantiate the arrival JVM state*)
apply (rule_tac x="None" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (n + 1 + 1), (heapC, k0f) \<mapsto> the (sha (heapC, kf)))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f)))))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([], vs, safeP, sigSafeMain, the (cdm (l, i)) +
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)]" in exI)
(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "∃ vs pc . fms=([],vs,safeP,sigSafeMain,pc,ref)#[]")
prefer 2 apply simp
apply (erule exE)+
apply (unfold exec_all_def)
apply (rule conjI)
apply (subgoal_tac "PC = (l,i)") prefer 2 apply simp
apply simp apply (elim conjE) apply clarsimp
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,[([], vs, safeP, sigSafeMain, the (cdm (l,i)), ag,bd)]) -jvm->
(None,sha,h,inih,[([the (sha (stackC,topf))], vs, safeP, sigSafeMain, the (cdm (l,i)) + 1, ag,bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
(* We prove the first step of the SVM *)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (unfold extractBytecode_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
the (cdm (l, i))) = Getstatic topf stackC",simp)
apply (unfold trInstr.simps, unfold Let_def)
apply (erule nth_via_drop_append)
(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha, h, inih,
[([the (sha (stackC, topf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! Suc (the (cdm (l, i)))) =
LitPush (Intg 1)",simp)
apply (erule nth_via_drop_append)
(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (the (cdm (l, i)))))) =
BinOp Add",simp)
apply (erule nth_via_drop_append)
(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (Suc (the (cdm (l, i))))))) =
Putstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))) =
Getstatic Sf stackC",simp)
apply (simp add: Sf_def add: topf_def)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) + 1), the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))) =
Getstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg (int (the (ctm' p)))) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) + 1), the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([Intg (int (the (ctm' p))),
Intg (the_Intg (the (sha (stackC, topf))) + 1),
the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))) =
LitPush (Intg (int (the (ctm' p))))",simp)
apply (erule nth_via_drop_append)
(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),h,inih,
[([Intg (int (the (ctm' p))),
Intg (the_Intg (the (sha (stackC, topf))) + 1),
the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) =
ArrStore",simp)
apply (simp add: raise_system_xcpt_def)
apply (frule equivS_PUSHCONT,simp)
apply (subgoal_tac "2 + n < int m",simp)
apply (rule maxPush_PUSHCONT)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([ Intg (n + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))) =
Getstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg (n + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg 1,
Intg (n + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))) =
LitPush (Intg 1)",simp)
apply (erule nth_via_drop_append)
(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg 1,
Intg (n + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg (n + 1 + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))) =
BinOp Add",simp)
apply (erule nth_via_drop_append)
(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile>(None,sha((stackC, topf) \<mapsto> Intg (n + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg (n + 1 + 1)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))) =
Putstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))) =
Getstatic Sf stackC",simp)
apply (simp add: Sf_def add: topf_def)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg (n + 1 + 1),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))) =
Getstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* Getstatic k0f heapC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([Intg (n + 1 + 1),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([the (sha (heapC,k0f)),
Intg (n + 1 + 1),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))) =
Getstatic k0f heapC",simp)
apply (simp add: heapC_def add: stackC_def add: k0f_def add: topf_def)
apply (erule nth_via_drop_append)
(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p)))))),inih,
[([the (sha (heapC,k0f)),
Intg (n + 1 + 1),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))),
inih,
[([],
vs, safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))) =
ArrStore",simp)
apply (simp add: raise_system_xcpt_def)
apply (subgoal_tac "int m > 2 + n",simp)
prefer 2 apply (rule maxPush_PUSHCONT)
apply (rule conjI, rule impI)
apply (frule equivS_PUSHCONT,simp)
apply (rule impI)
apply (frule equivS_PUSHCONT,simp)
apply (erule nth_via_drop_append)
(* Getstatic kf heapC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))),
inih,
[([],
vs, safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))),
inih,
[([the (sha (heapC, kf))],
vs, safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))) =
Getstatic kf heapC",simp)
apply (simp add: heapC_def add: stackC_def add: kf_def add: topf_def)
apply (erule nth_via_drop_append)
(* Putstatic k0f heapC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1)),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))),
inih,
[([the (sha (heapC, kf))],
vs, safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha((stackC, topf) \<mapsto> Intg (n + 1 + 1), (heapC, k0f) \<mapsto> the (sha (heapC, kf))),
h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))), nat (2 + n) \<mapsto> the (sha (heapC, k0f))))),
inih,
[([],
vs, safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))) =
Putstatic k0f heapC",simp)
apply (erule nth_via_drop_append)
apply simp
(* Now we prove the equivalence relation *)
apply (frule nonJumping_Suc_pc)
apply (erule_tac sym [where t="PUSHCONT p"])
apply (simp add: nonJumping.simps)
apply (simp add: trInstr.simps)
apply (rule_tac x="hm" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="(l,Suc i)" in exI)
apply (rule_tac x="Cont (k0, p) # S" in exI)
apply (rule_tac x=" sha((stackC, topf) \<mapsto> Intg (n + 1 + 1), (heapC, k0f) \<mapsto> the (sha (heapC, kf)))" in exI)
apply (rule_tac x=" h(la \<mapsto> Arr ty m (S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))),
nat (2 + n) \<mapsto> the (sha (heapC, k0f)))))" in exI)
apply (rule_tac x="inih" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1" in exI)
apply (rule_tac x="ref" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n + 1 + 1),
(heapC, k0f) \<mapsto> the (sha (heapC, kf)))) (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n + 1 + 1),
(heapC, k0f) \<mapsto> the (sha (heapC, kf)))) (heapC, k0f))))" in exI)
apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="S'a(nat (n + 1) \<mapsto> Intg (int (the (ctm' p))),
nat (2 + n) \<mapsto> the (sha (heapC, k0f)))" in exI)
apply (rule_tac x="(2 + n)" in exI)
apply (rule_tac x="l'" in exI)
apply (rule_tac x="regS" in exI)
apply (rule_tac x="l''" in exI)
apply (rule_tac x="m'" in exI)
apply (rule_tac x="m''" in exI)
apply (rule_tac x="d" in exI)
apply (rule_tac x="g" in exI)
apply (rule conjI, drule_tac t="S2" in sym, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply clarsimp
apply (simp add: Sf_def add: topf_def)
apply (simp add: stackC_def add: heapC_def)
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
apply (simp add: stackC_def add: heapC_def)
apply (simp add: kf_def add: k0f_def)
apply (rule conjI) apply (erule activeCells)
apply (rule conjI) apply (erule activeCells_2,assumption)
apply (erule activeCells_2,assumption)
apply (rule conjI, simp)
apply (rule conjI) apply clarsimp
apply (simp add: stackC_def add: heapC_def)
apply (rule conjI) apply clarsimp
apply (simp add: stackC_def add: heapC_def)
apply (simp add: regionsf_def add: k0f_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (simp add: dirCellC_def add: stackC_def)
apply (simp add: heapC_def add: safeDirf_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (rule equivH_PUSHCONT,assumption+)
apply (rule conjI) apply (rule maxPush_PUSHCONT)
apply (rule conjI) apply (simp, rule equivS_PUSHCONT_S2,simp)
apply (rule conjI) apply (unfold equivH.simps,simp)
by simp
end
lemma equivS_PUSHCONT_aux:
equivS (v1.0 # S) S' n ctm d g ==> 0 ≤ n + 1
lemma equivS_PUSHCONT:
equivS (drop (Suc 0) S) S' n ctm d g ==> 0 ≤ n + 1
lemma equivS_good:
equivS S S' n ctm d g ==> 1 ≤ 2 + n
lemma equivS_PUSHCONT_S2:
equivS S S' n ctm d g
==> equivS (Cont (nat (the_Intg (the (sha (heapC, k0f)))), p) # S)
(S'(nat (n + 1) |-> Intg (int (the (ctm' p))), nat (2 + n) |->
the (sha (heapC, k0f))))
(2 + n) ctm d g
lemma activeCells_PUSHCONT:
la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS
(h(la |->
Arr ty m
(S'(nat (n + 1) |-> Intg (int (the (ctm p))), nat (2 + n) |->
the (sha (heapC, k0f))))))
(nat (the_Intg (the (sha (heapC, kf)))))
lemma domH_PUSHCONT:
[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
∀l∈dom H.
∃l'. l' = the (g l) ∧
equivC (the (H l)) h l' (the (h l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g |]
==> ∀l∈dom H.
∃l'. l' = the (g l) ∧
equivC (the (H l))
(h(la |->
Arr ty m
(S'(nat (n + 1) |-> Intg (int (the (ctm p))), nat (2 + n) |->
the (sha (heapC, k0f))))))
l' (the ((h(la |->
Arr ty m
(S'(nat (n + 1) |-> Intg (int (the (ctm p))),
nat (2 + n) |-> the (sha (heapC, k0f))))))
l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma equivH_PUSHCONT:
[| ((hm, k), k0.0, (l, i), S) = ((H, ka), k0a, PC, Sa);
k' = nat (the_Intg (the (sha (heapC, kf))));
equivH (H, ka) h k' com regS d g;
activeCells regS h k' ∩ {la, l', l''} = {} |]
==> equivH (hm, k)
(h(la |->
Arr ty m
(S'(nat (n + 1) |-> Intg (int (the (ctm p))), nat (2 + n) |->
the (sha (heapC, k0f))))))
(nat (the_Intg
(the ((sha((stackC, topf) |-> Intg (n + 1 + 1), (heapC, k0f) |->
the (sha (heapC, kf))))
(heapC, kf)))))
com regS d g
lemma execSVMInstr_PUSHCONT:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
cdm , ctm, com \<turnstile> ((hm, k), k0.0, (l, i), S) \<triangleq> S1';
fst (the (map_of svms l)) ! i = PUSHCONT p;
execSVMInst (PUSHCONT p) (map_of ct) (hm, k) k0.0 (l, i) S =
Either.Right S2.0;
drop (the (cdm (l, i))) (extractBytecode P') =
trInstr (the (cdm (l, i))) cdm' ctm' com pcc (PUSHCONT p) @ bytecode' |]
==> ∃v' sh' dh' ih' fms'.
P' |- S1' -jvm-> (v', sh', dh', ih', fms') ∧
cdm , ctm, com \<turnstile> S2.0 \<triangleq> (v', sh', dh', ih', fms')