Up to index of Isabelle/HOL/SafeImp
theory dem_PRIMOP(*
Title: Lemmas for the translation SVM to JVM. PRIMOP
Author: Javier de Dios and Ricardo Pe~na
Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_PRIMOP
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]
declare extractBytecode_def [simp del]
declare initConsTable_def [simp del]
declare exec_instr.simps [simp del]
(* Lemmas for equivS *)
lemma equivS_PRIMOP:
"equivS (Val v1 # Val v2 # S) S' n ctm d g ==> n >= 1"
apply (induct S)
apply (unfold equivS.simps, clarsimp)
by (case_tac a,simp_all)
lemma equivS2_PRIMOP:
"[| 2 < length vs; equivS (Val (IntT i) # Val (IntT i') # S') S'a n ctm d g|]
==> equivS (Val (execOp oper (IntT i) (IntT i')) # S')
(S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0))) (n - 1) ctm d g"
apply (simp add: equivS.simps, clarsimp)
apply (rule conjI)
apply (case_tac "oper",simp_all)
apply (drule equivS_ge_n)
apply (erule_tac x="1" in allE,simp)
by (subgoal_tac "-1 + n= n - 1",simp,simp)
lemma activeCells_PRIMOP:
"[| 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'a(nat (n - 1) \<mapsto>
applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
(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)
lemma domH_PRIMOP:
"[| 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'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
l' (the ((h(la \<mapsto>
Arr ty m
(S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
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)
lemma equivH_PRIMOP:
"[|S = Val (IntT ia) # Val (IntT i') # S'; ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
k' = nat (the_Intg (the (sha (heapC, kf)))); k0' = nat (the_Intg (the (sha (heapC, k0f)))); sha (stackC, Sf) = Some (Addr la);
distinct [la, l', l'']; activeCells regS h k' ∩ {la, l', l''} = {}; h la = Some (Arr ty m S'a);
sha (stackC, topf) = Some (Intg n); sha (heapC, regionsf) = Some (Addr l'); h l' = Some (Arr ty m' regS);
sha (dirCellC, safeDirf) = Some (Addr l''); h l'' = Some (Arr ty m'' d); inj_on g (dom H); equivH (H, ka) h k' com regS d g
|]
==> equivH (hm, k)
(h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
(nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n - 1))) (heapC, kf))))) com regS d g"
apply (simp add: heapC_def add: stackC_def)
apply (simp add: kf_def add: k0f_def)
apply (fold heapC_def, fold kf_def)
apply (unfold equivH.simps, elim conjE)
apply (rule conjI, assumption)
apply (rule conjI, frule activeCells_PRIMOP,simp)
apply (rule conjI, assumption)
by (rule domH_PRIMOP,assumption+)
declare exec_instr.simps [simp]
lemma execSVMInstr_PRIMOP :
"[| (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) = PRIMOP oper;
execSVMInst (PRIMOP oper) (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 (PRIMOP oper) @ 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 "∃ i i' S'. S = Val (IntT i) # Val (IntT i') #S'")
prefer 2
(* We now prove the subgoal *)
apply (case_tac S,simp_all)
apply (insert RightNotUndefined, erule_tac x= "S2" in allE,force)
apply clarsimp
apply (case_tac af,simp_all)
apply (case_tac Vala,simp_all)
apply (erule_tac x= "S2" in allE,force)
apply (case_tac list,simp,simp_all)
apply clarsimp
apply (case_tac a,simp_all)
apply (case_tac Vala,simp_all)
apply (insert RightNotUndefined, erule_tac x= "S2" in allE,force)
apply (erule_tac x= "S2" in allE,force)
apply (erule_tac x= "S2" in allE,force)
apply (erule_tac x= "S2" in allE,force)
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))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0))))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([], vs[Suc 0 := the (S'a (nat (n - 1)))], safeP, sigSafeMain, the (cdm (l, i)) +
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,Sf))], 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 Sf stackC",simp)
apply (unfold trInstr.simps)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha, h, inih,
[([the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),
the (sha (stackC,Sf))],
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)))) =
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,h,inih,
[([the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf)),
the (sha (stackC,Sf))],
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)))))) =
LitPush (Intg 1)",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,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, 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))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* Dup2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,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, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
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)))))))) =
Dup2",simp)
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (S'a (nat (n - 1))),
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))))))))) =
ArrLoad",simp)
(* Equivalencia de entornos *)
apply (frule equivS_PRIMOP, simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Store 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (S'a (nat (n - 1))),
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,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)))))))))) =
Store 1",simp)
apply (erule nth_via_drop_append)
(* Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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))))))))))) =
Getstatic Sf stackC",simp)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),
the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),
the (sha (stackC,Sf)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (S'a (nat n)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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))))))))))))) =
ArrLoad",simp)
(* Equivalencia de entornos *)
apply (frule equivS_PRIMOP, simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Load 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (S'a (nat n)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0,
the (S'a (nat n)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)))))))))))))) =
Load 1",simp)
apply (erule nth_via_drop_append)
(* BinOp oper *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0,
the (S'a (nat n)),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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))))))))))))))) =
BinOp oper",simp)
apply (erule nth_via_drop_append)
(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0),
Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)))))))))))))))) =
ArrStore",simp)
apply (simp add: raise_system_xcpt_def)
apply (frule equivS_PRIMOP,simp)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([],
vs[Suc 0 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([the (sha (stackC,topf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)
(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([the (sha (stackC,topf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([Intg 1,
the (sha (stackC,topf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)))))))))))))))))) =
LitPush (Intg 1)",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([Intg 1,
the (sha (stackC,topf))],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([Intg (n - 1)],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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))))))))))))))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([Intg (n - 1)],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)),
h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] !
Suc 0)))),
inih,
[([],
vs[Suc 0 := the (S'a (nat (n - 1)))],
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)))))))))))))))))))) =
Putstatic topf stackC",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="PRIMOP oper"])
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="k0" in exI)
apply (rule_tac x="(l,Suc i)" in exI)
apply (rule_tac x="Val (execOp oper (IntT ia) (IntT i')) # S'" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (n - 1))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat (n - 1) \<mapsto> applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0))))" in exI)
apply (rule_tac x="inih" in exI)
apply (rule_tac x="vs[Suc 0 := the (S'a (nat (n - 1)))]" 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" in exI)
apply (rule_tac x="ref" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n - 1))) (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n - 1))) (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> applyBinOp oper (the (S'a (nat n))) (vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))" in exI)
apply (rule_tac x="n - 1" 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, clarsimp)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply clarsimp
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
apply (simp add: heapC_def add: stackC_def)
apply (rule conjI) apply (rule activeCells,assumption)
apply (rule conjI) apply (rule activeCells_2,assumption+)
apply (rule activeCells_2,assumption+)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (rule equivH_PRIMOP, assumption+)
apply (rule conjI) apply simp
apply (rule conjI) apply clarsimp
apply (subgoal_tac "length vs = 10")
apply (rule equivS2_PRIMOP,simp, assumption+)
apply (rule length_vs)
apply (rule conjI) apply simp
apply (simp add: heapC_def add: stackC_def)
by simp
end
lemma equivS_PRIMOP:
equivS (Val v1.0 # Val v2.0 # S) S' n ctm d g ==> 1 ≤ n
lemma equivS2_PRIMOP:
[| 2 < length vs; equivS (Val (IntT i) # Val (IntT i') # S') S'a n ctm d g |]
==> equivS (Val (execOp oper (IntT i) (IntT i')) # S')
(S'a(nat (n - 1) |->
applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))
(n - 1) ctm d g
lemma activeCells_PRIMOP:
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'a(nat (n - 1) |->
applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
(nat (the_Intg (the (sha (heapC, kf)))))
lemma domH_PRIMOP:
[| 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'a(nat (n - 1) |->
applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
l' (the ((h(la |->
Arr ty m
(S'a(nat (n - 1) |->
applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma equivH_PRIMOP:
[| S = Val (IntT ia) # Val (IntT i') # S';
((hm, k), k0.0, (l, i), S) = ((H, ka), k0a, PC, Sa);
k' = nat (the_Intg (the (sha (heapC, kf))));
k0' = nat (the_Intg (the (sha (heapC, k0f))));
sha (stackC, Sf) = Some (Addr la); distinct [la, l', l''];
activeCells regS h k' ∩ {la, l', l''} = {}; h la = Some (Arr ty m S'a);
sha (stackC, topf) = Some (Intg n); sha (heapC, regionsf) = Some (Addr l');
h l' = Some (Arr ty m' regS); sha (dirCellC, safeDirf) = Some (Addr l'');
h l'' = Some (Arr ty m'' d); inj_on g (dom H);
equivH (H, ka) h k' com regS d g |]
==> equivH (hm, k)
(h(la |->
Arr ty m
(S'a(nat (n - 1) |->
applyBinOp oper (the (S'a (nat n)))
(vs[Suc 0 := the (S'a (nat (n - 1)))] ! Suc 0)))))
(nat (the_Intg (the ((sha((stackC, topf) |-> Intg (n - 1))) (heapC, kf)))))
com regS d g
lemma execSVMInstr_PRIMOP:
[| (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 = PRIMOP oper;
execSVMInst (PRIMOP oper) (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 (PRIMOP oper) @ 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')