Up to index of Isabelle/HOL/SafeImp
theory dem_BUILDENV(*
Title: Lemmas for the translation SVM to JVM. BUILDENV
Author: Javier de Dios and Ricardo Pe~na
Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_BUILDENV
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]
fun Item2val :: "entries_ => sheap => Item => val"
where
"Item2val S sh (ItemConst v) = (if (isBool v = True)
then Bool (the_BoolT v)
else Intg (the_IntT v))"
| "Item2val S sh (ItemVar l) = the (S (nat (the_Intg (the (sh (stackC, topf))) - int l)))"
| "Item2val S sh (ItemRegSelf) = the (sh (heapC, kf))"
(* Axioms *)
axioms maxPush_BUILDENV:
"fst (the (map_of svms l)) ! i = BUILDENV items ==> n + int (length items) < int m"
axioms pushAux_instrs:
"P'\<turnstile>
(None,sha,h,inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,
sha,
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), ag, bd)])"
(* Lemmas for equivS *)
axioms equivS_BUILDENV:
"equivS S S' n ctm d g
==> equivS (map (item2Stack k S) items @ S)
(S' ++ map_of (zip (decreasing (nat (n + int (length items)))) (map (Item2val S' sha) items)))
(n + int (length items)) ctm d g"
(* Lemmas for equivH *)
declare equivH.simps [simp del]
lemma activeCells_BUILDENV:
"[|the_Addr (the (sha (stackC, Sf))) ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))|]
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS
(h(the_Addr (the (sha (stackC, Sf))) \<mapsto>
Arr ty m
(S' ++ map_of (zip (decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items))))
(map (Item2val S' sha) items))))) (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_BUILDENV:
"[| 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' ++ map_of (zip (decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items))))
(map (Item2val S' sha) items)))))
l' (the ((h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip (decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items))))
(map (Item2val S' sha) items)))))
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_BUILDENV:
"[| k' = nat (the_Intg (the (sha (heapC, kf))));
((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
equivH (H, ka) h k' com regS d g;
sha (stackC, Sf) = Some (Addr la);
activeCells regS h k' ∩ {la, l', l''} = {}|]
==> equivH (hm, k)
(h(the_Addr (the (sha (stackC, Sf))) \<mapsto>
Arr ty m
(S' ++ map_of (zip (decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items))))
(map (Item2val S' sha) items)))))
(nat (the_Intg (the ((sha((stackC, topf) \<mapsto> vs[Suc 0 := Intg (n + int (length items))] ! Suc 0)) (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 (fold stackC_def)
apply (rule conjI)
apply (subgoal_tac
"the_Addr (the (sha (stackC, Sf))) ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))")
apply (frule activeCells_BUILDENV,simp)
apply simp
apply (rule conjI, assumption)
by (rule domH_BUILDENV,simp,assumption)
lemma execSVMInstr_BUILDENV:
"[| (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) = BUILDENV items;
execSVMInst (BUILDENV items) (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 (BUILDENV items) @ 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 (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> vs[Suc 0 := Intg (n + int (length items))] ! Suc 0)" in exI)
apply (rule_tac x="(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S''))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), 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 (rule conjI)
apply (unfold exec_all_def)
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 (unfold trInstr.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
the (cdm (l, i))) = Getstatic topf stackC",simp)
apply (erule nth_via_drop_append_2)
(* LitPush (Intg (int (length items))) *)
apply (drule drop_Suc_append_2)
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 (int (length items)),
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 (int (length items)))",simp)
apply (erule nth_via_drop_append)
(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (int (length items)),
the (sha (stackC,topf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (n + int (length items))],
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)
(* Store 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (n + int (length items))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
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))))))) =
Store 1",simp)
apply (erule nth_via_drop_append)
(* concat (map pushAux (zip items [0..<length items])) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None, sha,
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), ag, bd)])")
prefer 2 apply (rule pushAux_instrs)
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
(* Load (Suc 0) *)
apply (drule drop_append_length)
apply (subgoal_tac "P'\<turnstile> (None,sha,
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), ag, bd)])
-jvm->
(None,sha,
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([vs[Suc 0 := Intg (n + int (length items))] ! Suc 0],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), 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)))))))) +
length (concat (map pushAux (zip items [0..<length items]))))) =
Load 1",simp)
apply (erule nth_via_drop_append)
(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([vs[Suc 0 := Intg (n + int (length items))] ! Suc 0],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), ag, bd)])
-jvm->
(None,
sha((stackC, topf) \<mapsto> vs[Suc 0 := Intg (n + int (length items))] ! Suc 0),
(let vitems = map (Item2val S' sha) items;
idxs = decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items)));
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih,
[([],
vs[Suc 0 := Intg (n + int (length items))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 +
length (concat (map pushAux (zip items [0..<length items]))), ag, bd)])")
apply (unfold exec_all_def)
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))))))))) +
length (concat (map pushAux (zip items [0..<length items]))))) =
Putstatic topf stackC",simp)
apply (rule nth_via_drop_append, force)
apply simp
(* Now we prove the equivalence relation *)
apply (frule nonJumping_Suc_pc)
apply (erule_tac sym [where t="BUILDENV items"])
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="map (item2Stack k S) items @ S" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> vs[Suc 0 := Intg (n + int (length items))] ! Suc 0)" in exI)
apply (rule_tac x="h(the_Addr (the (sha (stackC, Sf))) \<mapsto> Arr ty m
(S' ++ map_of (zip (decreasing (nat (the_Intg (the (sha (stackC, topf))) + int (length items))))
(map (Item2val S' sha) items))))" in exI)
apply (rule_tac x="inih" in exI)
apply (rule_tac x="vs[Suc 0 := Intg (n + int (length items))]" in exI)
apply (rule_tac x="the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + length (concat (map pushAux (zip items [0..<length items])))" in exI)
apply (rule_tac x="ref" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto>
vs[Suc 0 := Intg (n + int (length items))] ! Suc 0)) (heapC, kf))))" in exI)
apply (rule_tac x=" nat (the_Intg (the ((sha((stackC, topf) \<mapsto>
vs[Suc 0 := Intg (n + int (length items))] ! Suc 0)) (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' ++ map_of (zip (decreasing (nat (n + int (length items)))) (map (Item2val S' sha) items))" in exI)
apply (rule_tac x="(n + int (length items))" 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, erule sym)
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 (erule activeCells)
apply (rule conjI) apply (erule activeCells_2,assumption)
apply (erule activeCells_2,assumption)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (subgoal_tac "length vs = 10")
apply clarsimp
apply (rule length_vs)
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_BUILDENV,assumption+)
apply (rule conjI) apply clarsimp
apply (rule maxPush_BUILDENV,assumption+)
apply (rule conjI) apply clarsimp
apply (erule equivS_BUILDENV)
apply (rule conjI) apply (subgoal_tac "length vs = 10")
apply (simp add: heapC_def add: stackC_def)
apply (rule length_vs)
by simp
end
lemma activeCells_BUILDENV:
the_Addr (the (sha (stackC, Sf)))
∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS
(h(the_Addr (the (sha (stackC, Sf))) |->
Arr ty m
(S' ++
map_of
(zip (decreasing
(nat (the_Intg (the (sha (stackC, topf))) +
int (length items))))
(map (Item2val S' sha) items)))))
(nat (the_Intg (the (sha (heapC, kf)))))
lemma domH_BUILDENV:
[| 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' ++
map_of
(zip (decreasing
(nat (the_Intg (the (sha (stackC, topf))) +
int (length items))))
(map (Item2val S' sha) items)))))
l' (the ((h(la |->
Arr ty m
(S' ++
map_of
(zip (decreasing
(nat (the_Intg (the (sha (stackC, topf))) +
int (length items))))
(map (Item2val S' sha) items)))))
l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma equivH_BUILDENV:
[| k' = nat (the_Intg (the (sha (heapC, kf))));
((hm, k), k0.0, (l, i), S) = ((H, ka), k0a, PC, Sa);
equivH (H, ka) h k' com regS d g; sha (stackC, Sf) = Some (Addr la);
activeCells regS h k' ∩ {la, l', l''} = {} |]
==> equivH (hm, k)
(h(the_Addr (the (sha (stackC, Sf))) |->
Arr ty m
(S' ++
map_of
(zip (decreasing
(nat (the_Intg (the (sha (stackC, topf))) +
int (length items))))
(map (Item2val S' sha) items)))))
(nat (the_Intg
(the ((sha((stackC, topf) |->
vs[Suc 0 := Intg (n + int (length items))] ! Suc 0))
(heapC, kf)))))
com regS d g
lemma execSVMInstr_BUILDENV:
[| (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 = BUILDENV items;
execSVMInst (BUILDENV items) (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 (BUILDENV items) @ 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')