(*
Title: Lemmas for the translation SVM to JVM. MATCH
Author: Ricardo Pe~na and Javier de Dios
Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_MATCH
imports "../JVMSAFE/JVMExec" SVM2JVM SVMSemantics CertifSVM2JVM
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]
consts
upt_rev :: "nat => nat => nat list" ("(1[_>/.._'])")
primrec
upt_0_rev: "[0>..i] = []"
upt_Suc_rev: "[(Suc j)>..i] = (if i <= j then j # [j>..i] else [])"
lemma length_upt_rev: "length [i>..j] = i - j"
by (induct i) (auto simp add: Suc_diff_le)
lemma nth_upt_2: "k < j ∧ k >= i ==> [i..<j] ! (k - i) = k"
apply (induct j)
apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
done
constdefs diff :: "jvm_state => nat"
"diff s ≡ (case s of (none, sh, h, inih,[([], vs, C, M, pc, ref)])
=> case vs!5 of Intg i =>
case vs!4 of Intg nargs =>
nat (nargs - i))"
constdefs oneStep :: "jvm_prog => jvm_state => jvm_state"
"oneStep P s ≡ (THE s'. P \<turnstile> s -jvm-> s' ∧
(case s of (none, sh, h, inih,[([], vs, C, M, pc, ref)])
=> (case s' of (none', sh', h', inih',[([], vs', C', M', pc', ref')])
=> case vs!5 of Intg i
=> case sh (stackC, Sf) of Some (Addr la)
=> case h la of Some (Arr ty m S')
=> case vs!6 of Addr l
=> case vs!4 of Intg nargs
=> case h l of Some (Obj cell fs) =>
vs' = vs[5 := Intg (i + 1)] ∧
none' = none ∧
sh' = sh ∧
h' = h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m
(S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1)))) ∧
inih' = inih ∧
C' = C ∧
M' = M ∧
pc' = pc ∧
ref' = ref)))"
consts
steps :: "nat => jvm_prog => jvm_state => jvm_state"
primrec
"steps 0 P s = s"
"steps (Suc n) P s = steps n P (oneStep P s)"
constdefs lastState :: "jvm_prog => jvm_state => jvm_state"
"lastState P s ≡ steps (diff s) P s"
axioms undefined_false:
"undefined ==> False"
axioms i_0:
" i = 0"
axioms top_good:
"(¬ int m ≤ the_Intg (the (sh (stackC, topf))) - i ∧ ¬ the_Intg (the (sh (stackC, topf))) < i )"
lemma drop_append_3:
"drop n xs = [] @ (ys @ zs) ==> drop n xs = ys @ zs"
by simp
lemma drop_length_append:
"drop n xs = (ys @ zs) ==> drop (n + length ys) xs = zs"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma drop_endlabel1:
"[| drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
[Goto endlabel1] @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @ InstLabel6 @
InstLabel7 @ InstLabel8 @ Match2 @ bytecode |]
==> drop (nat (12 + int pc + endlabel1)) (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match2 @ bytecode"
apply (drule drop_Suc_append)
apply (drule drop_append_3)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (simp add: endlabel1_def)
apply (simp add: nlab2_def)
apply (simp add: nlab3_def)
apply (simp add: nlab4_def)
apply (simp add: nlab5_def)
apply (simp add: nlab6_def)
apply (simp add: nlab7_def)
apply (simp add: nlab8_def)
apply (simp add: InstLabel2_def)
apply (simp add: InstLabel3_def)
apply (simp add: InstLabel4_def)
apply (simp add: InstLabel5_def)
apply (simp add: InstLabel6_def)
apply (simp add: InstLabel7_def)
apply (simp add: InstLabel8_def)
apply (subgoal_tac
"(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
pc))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = nat (69 + (int pc))")
by auto
lemma oneStep_MATCH:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
l ≠ la;
sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih, [([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)]);
i < nargs |]
==> P' \<turnstile> (None, sh, h, inih, [([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
-jvm-> (None, sh, h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m
(S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1)))),
inih, [([], vs[4:= Intg nargs, 5:= Intg (i + 1)], safeP, sigSafeMain, pc, ref)])"
apply (unfold Match12_def)
(* Load 4 *)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
-jvm->
(None,sh,h,inih,[([Intg nargs],vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1, ref)])")
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)))))) !
pc) = Load 4") apply simp
apply (rule nth_via_drop_append) apply force
(* Load 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([Intg nargs], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1, ref)])
-jvm->
(None, sh, h, inih, [([Intg i, Intg nargs], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1, ref)])")
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 pc) = Load 5") apply simp
apply (rule nth_via_drop_append) apply force
(* Ifcmp GreaterEqual labelEndLoop *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([Intg i, Intg nargs], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1, ref)])
-jvm->
(None, sh, h, inih, [([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1, ref)])")
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 pc)) = Ifcmp GreaterEqual labelEndLoop") apply simp
apply (rule nth_via_drop_append) apply force
(* Load 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1, ref)])
-jvm->
(None, sh, h, inih, [([Intg i], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1 + 1, ref)])")
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 pc))) = Load 5") apply simp
apply (rule nth_via_drop_append) apply force
(* Tableswitch 0 7 [label1, label2, label3, label4, label5, label6, label7, label8]] *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([Intg i], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1 + 1, ref)])
-jvm->
(None, sh, h, inih, [([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1, ref)])")
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 pc)))) =
Tableswitch 0 7 [label1, label2, label3, label4, label5, label6, label7, label8]") apply simp
apply (subgoal_tac "i = 0")
prefer 2 apply (rule i_0) apply simp apply (simp add: label1_def)
apply (rule nth_via_drop_append) apply force
(* Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (unfold InstLabel1_def)
apply (drule drop_append_3)
apply (subgoal_tac
"P'\<turnstile> (None,sh,h,inih,[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1, ref)])
-jvm->
(None, sh, h, inih, [([the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, Suc (Suc (Suc (Suc (Suc (Suc pc))))), ref)])")
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 pc))))) =
Getstatic Sf stackC") apply simp
apply (rule nth_via_drop_append) apply force
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc pc))))), ref)])
-jvm->
(None, sh, h, inih,
[([the (sh (stackC, topf)), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))), ref)])")
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 pc)))))) =
Getstatic topf stackC") apply simp
apply (rule nth_via_drop_append) apply force
(* Load 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([the (sh (stackC, topf)), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))), ref)])
-jvm->
(None, sh, h, inih,
[([Intg i, the (sh (stackC, topf)), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))), ref)])")
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 pc))))))) =
Load 5") apply simp
apply (rule nth_via_drop_append) apply force
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([Intg i, the (sh (stackC, topf)), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))), ref)])
-jvm->
(None, sh, h, inih,
[([Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))))), ref)])")
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 pc)))))))) =
BinOp Substract") apply simp
apply (rule nth_via_drop_append) apply force
(* Load 6 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))))), ref)])
-jvm->
(None, sh, h, inih,
[([Addr l, Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))), ref)])")
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 pc))))))))) =
Load 6") apply simp
apply (rule nth_via_drop_append) apply force
(* Getfield arg1 cellC *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([Addr l, Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))), ref)])
-jvm->
(None, sh, h, inih,
[([the (fs (arg1, cellC)), Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))))))), ref)])")
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 pc)))))))))) =
Getfield arg1 cellC") apply simp
apply (simp add: raise_system_xcpt_def)
apply (rule nth_via_drop_append) apply force
(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h, inih,
[([the (fs (arg1, cellC)), Intg (the_Intg (the (sh (stackC, topf))) - i), the (sh (stackC, Sf))],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc)))))))))), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))))), ref)])")
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 pc))))))))))) =
ArrStore") apply simp
apply (subgoal_tac "(¬ int m ≤ the_Intg (the (sh (stackC, topf))) - i ∧ ¬ the_Intg (the (sh (stackC, topf))) < i)")
apply (simp add: raise_system_xcpt_def)
apply (subgoal_tac "i=0")
prefer 2 apply (rule i_0)
apply (subgoal_tac "the (fs (arg1, cellC)) = argCell fs (Suc (nat i))",simp)
apply (simp add: argCell_def)
apply (rule top_good)
apply (rule nth_via_drop_append) apply force
(* Goto endlabel1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))))), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, nat (12 + int pc + endlabel1), ref)])")
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 pc)))))))))))) =
Goto endlabel1") apply simp
apply (rule nth_via_drop_append) apply force
(* Load 5 *)
apply (frule drop_endlabel1)
apply (unfold Match2_def)
apply (subgoal_tac
"P'\<turnstile> (None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, nat (12 + int pc + endlabel1), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg i],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (nat (12 + int pc + endlabel1)), ref)])")
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)))))) !
(nat (12 + int pc + endlabel1))) =
Load 5") apply simp
apply (rule nth_via_drop_append) apply force
(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg i],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (nat (12 + int pc + endlabel1)), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg 1, Intg i],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (nat (12 + int pc + endlabel1))), ref)])")
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 (nat (12 + int pc + endlabel1))) =
LitPush (Intg 1)") apply simp
apply (rule nth_via_drop_append) apply force
(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg 1, Intg i],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (nat (12 + int pc + endlabel1))), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg (i + 1)],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (nat (12 + int pc + endlabel1)))), ref)])")
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 (nat (12 + int pc + endlabel1)))) =
BinOp Add") apply simp
apply (rule nth_via_drop_append) apply force
(* Store 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([Intg (i + 1)],
vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain,
Suc (Suc (Suc (nat (12 + int pc + endlabel1)))), ref)])
-jvm->
(None, sh, h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([],
vs[4:= Intg nargs, 5:= Intg (i + 1)], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (nat (12 + int pc + endlabel1))))), ref)])")
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 (nat (12 + int pc + endlabel1))))) =
Store 5") apply simp
apply (rule nth_via_drop_append) apply force
(* Goto labelLoop *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None, sh, h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([],
vs[4:= Intg nargs, 5:= Intg (i + 1)], safeP, sigSafeMain,
Suc (Suc (Suc (Suc (nat (12 + int pc + endlabel1))))), ref)])
-jvm->
(None, sh,
h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i)
\<mapsto> argCell fs (nat i + 1)))),
inih,
[([],
vs[4:= Intg nargs, 5:= Intg (i + 1)],
safeP, sigSafeMain,
nat (16 + (int pc + endlabel1) + labelLoop), ref)])")
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 (nat (12 + int pc + endlabel1)))))) =
Goto labelLoop") apply simp
apply (simp add: endlabel1_def)
apply (rule nth_via_drop_append) apply force
apply (simp add: endlabel1_def)
apply (simp add: labelLoop_def)
apply (simp add: nlab1_def)
apply (simp add: InstLabel1_def)
apply (simp add: nMatch2_def)
apply (simp add: nMatch12_def)
by (simp add: Match12_def)
lemma oneStep_state:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
sh (stackC, Sf) = Some (Addr la);
l ≠ la;
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
i < nargs |]
==> oneStep P' (None, sh, h, inih, [([], vs[4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
= (None, sh, h(the_Addr (the (sh (stackC, Sf))) \<mapsto>
Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1)))),
inih, [([], vs[4:= Intg nargs, 5:= Intg (i + 1)], safeP, sigSafeMain, pc, ref)])"
apply (simp (no_asm) only: oneStep_def)
apply (rule the_equality)
apply (rule conjI)
apply (rule oneStep_MATCH,assumption+,simp)
apply auto
apply (rename_tac v1' sh' dh' ih' frms')
apply (case_tac frms',simp)
apply (frule undefined_false,simp)
apply simp
apply (case_tac a,simp)
apply (case_tac aa,simp)
apply (case_tac b,simp)
apply (case_tac ba,simp)
apply (case_tac bb,simp)
apply (case_tac bca,simp)
apply (case_tac list,simp)
apply (simp,frule undefined_false,simp)
apply (simp,frule undefined_false,simp)
apply (case_tac y,simp)
apply (frule undefined_false,simp)
apply simp
apply (case_tac a,simp)
apply (case_tac aa,simp)
apply (case_tac b,simp)
apply (case_tac ba,simp)
apply (case_tac bb,simp)
apply (case_tac bca,simp)
apply (case_tac list,simp)
apply (simp,frule undefined_false,simp)
apply (simp,frule undefined_false,simp)
apply (case_tac y,simp)
apply (frule undefined_false,simp)
apply simp
apply (case_tac a,simp)
apply (case_tac aa,simp)
apply (case_tac b,simp)
apply (case_tac ba,simp)
apply (case_tac bb,simp)
apply (case_tac bca,simp)
apply (case_tac list,simp)
apply (simp,frule undefined_false,simp)
apply (simp,frule undefined_false,simp)
apply (rename_tac v1' sh' dh' ih' frms')
apply (case_tac frms')
apply simp
apply (frule undefined_false,simp)
apply simp
apply (case_tac a,simp)
apply (case_tac aa,simp)
apply (case_tac b,simp)
apply (case_tac ba,simp)
apply (case_tac bb,simp)
apply (case_tac bca,simp)
apply (case_tac list,simp)
apply (simp,frule undefined_false,simp)
apply (simp,frule undefined_false,simp)
apply (case_tac y)
apply simp
apply (frule undefined_false,simp)
apply simp
apply (case_tac a,simp)
apply (case_tac aa,simp)
apply (case_tac b,simp)
apply (case_tac ba,simp)
apply (case_tac bb,simp)
apply (case_tac bca,simp)
apply (case_tac list,simp)
apply (simp,frule undefined_false,simp)
by (simp,frule undefined_false,simp)
lemma diff_monotone:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
l ≠ la;
i < nargs;
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
Suc n = diff (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) |]
==> n = diff (oneStep P' (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]))"
apply (simp add: diff_def)
apply (subgoal_tac
"oneStep P' (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) =
(None, sh, h(the_Addr (the (sh (stackC, Sf))) \<mapsto>
Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1)))),
inih, [([], vs[4:= Intg nargs, 5:= Intg (i + 1)], safeP, sigSafeMain, pc, ref)])",simp)
by (rule oneStep_state,assumption+)
lemma steps_monotone:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
l ≠ la;
i < nargs;
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
Suc n = diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) |]
==> steps (diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)])) P'
(None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) =
steps (diff (oneStep P' (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]))) P'
(oneStep P' (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]))"
apply (frule diff_monotone,assumption+)
by (case_tac "(diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]))",simp,simp)
lemma MATCH_loop [rule_format]:
"∀ sh h inih vs i pc ref S'.
n = diff (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
--> (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc)
--> length vs = 10
--> vs ! 6 = Addr l
--> sh (stackC, Sf) = Some (Addr la)
--> h la = Some (Arr ty m S')
--> h l = Some (Obj cellC fs)
--> l ≠ la
--> drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode
--> P' \<turnstile> (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
-jvm-> steps n P' (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])"
apply (induct n)
apply (simp add: steps.simps)
apply (simp add: exec_all_def)
apply (rule allI)+
apply (rule impI)
(* case i < nargs *)
apply (case_tac "i < nargs")
apply (erule_tac x="sh" in allE)
apply (erule_tac x="h(the_Addr (the (sh (stackC, Sf))) \<mapsto>
Arr ty m (S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto>
argCell fs (nat i + 1))))" in allE)
apply (erule_tac x="inih" in allE)
apply (erule_tac x="vs" in allE)
apply (erule_tac x="i + 1" in allE)
apply (erule_tac x="pc" in allE)
apply (erule_tac x="ref" in allE)
apply (erule_tac x="S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1))" in allE)
apply (rule impI)+
apply (drule mp)
apply (frule diff_monotone,assumption+)
apply (frule_tac inih="inih" and nargs="nargs" and i="i" and ref="ref" in oneStep_state,assumption+)
apply (simp add: diff_def)
apply (drule mp,force)+
apply (frule diff_monotone,assumption+)
apply (frule_tac
inih="inih" and nargs="nargs" and i="i" and ref="ref"
in oneStep_MATCH,assumption+,simp,assumption)
apply (frule_tac
inih="inih" and nargs="nargs" and i="i" and ref="ref"
in oneStep_state,assumption+)
apply (drule_tac
s="oneStep P' (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)])" in sym)
apply clarify
apply simp
apply (frule steps_monotone, assumption+)
apply (drule_tac
s="steps (diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, a, b)])) P'
(None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, a, b)])" in sym,simp)
apply (simp add: exec_all_def)
(* case i ≥ nargs *)
apply (rule impI)+
by (simp add: diff_def)
lemma execSVMInstr_MATCH_loop:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
l ≠ la;
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)]) |]
==> P' \<turnstile> s -jvm-> lastState P' s"
apply (simp add: lastState_def)
apply (intro MATCH_loop)
apply (simp add: diff_def)
by assumption+
axioms map_of_update_add:
"x ∉ set xs
==> S(x \<mapsto> y) ++ map_of (zip xs ys) = S ++ map_of (zip (xs@[x]) (ys@[y]))"
axioms map_upt_rev:
"m < n ==> map f [n>..Suc m] @ [f m] = map f [n>..m]"
lemma map_argCell_upt_rev:
"[| i < nargs; i ≥ 0 |]
==> (map (λj. argCell fs (Suc j)) [nat nargs>..nat (i + 1)] @ [argCell fs (Suc (nat i))])
= (map (λj. argCell fs (Suc j)) [nat nargs>..nat i])"
apply (subgoal_tac "nat (i + 1) = Suc (nat i)",simp)
apply (subgoal_tac "nat i < nat nargs")
apply (rule_tac f="(λj. argCell fs (Suc j))" in map_upt_rev,assumption)
by force+
lemma empty_map_add_2: "m ++ empty = m"
by (rule ext) (simp add: map_add_def split: option.split)
lemma upt_Suc_append_topf:
"[| i < nargs; i >= 0; (the_Intg (the (sh (stackC, topf))) - nargs) >= 0 |]
==> [Suc (nat (the_Intg (the (sh (stackC, topf))) - nargs))..<nat (the_Intg (the (sh (stackC, topf))) - i)] @
[nat (the_Intg (the (sh (stackC, topf))) - i)]
= [Suc (nat (the_Intg (the (sh (stackC, topf))) - nargs))..<nat (the_Intg (the (sh (stackC, topf))) - i + 1)]"
apply (rule sym)
apply (subgoal_tac
"nat (the_Intg (the (sh (stackC, topf))) - i + 1) =
Suc (nat (the_Intg (the (sh (stackC, topf))) - i))",simp)
by arith+
lemma execSVMInstr_MATCH_loop_post [rule_format]:
"∀ sh h inih vs i pc ref S'.
n = diff (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)])
--> (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc)
--> length vs = 10
--> i >= 0
--> (the_Intg (the (sh (stackC, topf))) - nargs) >= 0
--> nargs ≥ i
--> vs ! 6 = Addr l
--> sh (stackC, Sf) = Some (Addr la)
--> h la = Some (Arr ty m S')
--> h l = Some (Obj cellC fs)
--> l ≠ la
--> drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode
--> steps n P' (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)]) =
(None, sh,
(let vitems = map (%j. argCell fs (j + 1)) [nat nargs>..nat i];
idxs = map (%j. j)
[nat (the_Intg (the (sh (stackC, topf))) - nargs) + 1..<nat (the_Intg (the (sh (stackC, topf))) - i + 1) ];
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih, [([], vs[ 4:= Intg nargs, 5:= Intg nargs],
safeP, sigSafeMain, pc, ref)])"
apply (induct n)
apply (simp add: steps.simps,clarsimp)
apply (simp add: diff_def)
apply (subgoal_tac "nargs = i",clarsimp)
apply (subst upt_conv_Nil,simp)+
apply (subst zip_Nil)
apply (subst map_of.simps, subst empty_map_add_2)
apply (rule ext,force)
apply simp
apply (rule allI)+
apply (rule impI)+
apply (case_tac "i < nargs")
(* case i < nargs *)
apply (erule_tac x="sh" in allE)
apply (erule_tac x="h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m
(S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1))))" in allE)
apply (erule_tac x="inih" in allE)
apply (erule_tac x="vs" in allE)
apply (erule_tac x="i + 1" in allE)
apply (erule_tac x="pc" in allE)
apply (erule_tac x="ref" in allE)
apply (erule_tac x="(S'(nat (the_Intg (the (sh (stackC, topf))) - i) \<mapsto> argCell fs (nat i + 1)))" in allE)
apply (drule mp)
apply (frule diff_monotone,assumption+)
apply (frule_tac inih="inih" and nargs="nargs" and i="i" and ref="ref" in oneStep_state,assumption+)
apply (simp add: diff_def)
apply (drule mp,force)+
apply (frule diff_monotone,assumption+)
apply (frule_tac
inih="inih" and nargs="nargs" and i="i" and ref="ref"
in oneStep_MATCH,assumption+,simp,assumption)
apply (frule_tac
inih="inih" and nargs="nargs" and i="i" and ref="ref"
in oneStep_state,assumption+)
apply (drule_tac
s="oneStep P' (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)])" in sym)
apply clarify
apply simp
apply (frule steps_monotone, assumption+)
apply (drule_tac
s="steps (diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, a, b)])) P'
(None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, a, b)])" in sym,simp)
apply (drule_tac
t="oneStep P' (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, a, b)])" in sym)
apply (simp add: diff_def)
apply (subst map_of_update_add,simp)
apply (subst upt_Suc_append_topf,assumption+)
apply (subst map_argCell_upt_rev,assumption+)
apply (rule refl)
(* case i >= nargs *)
by (simp add: diff_def)
lemma execSVMInstr_MATCH_loop_state:
"[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10;
vs ! 6 = Addr l;
sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S');
h l = Some (Obj cellC fs);
l ≠ la;
0 ≤ i;
0 ≤ the_Intg (the (sh (stackC, topf))) - nargs;
i ≤ nargs;
drop pc (fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @ InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @ InstLabel5 @
InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih, [([], vs[ 4:= Intg nargs, 5:= Intg i], safeP, sigSafeMain, pc, ref)]) |]
==> P' \<turnstile> s -jvm-> (None, sh,
(let vitems = map (%j. argCell fs (j + 1)) [nat nargs>..nat i];
idxs = map (%j. j)
[nat (the_Intg (the (sh (stackC, topf))) - nargs) + 1..<nat (the_Intg (the (sh (stackC, topf))) - i + 1) ];
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sh (stackC, Sf))) \<mapsto> Arr ty m S'')),
inih, [([], vs[ 4:= Intg nargs, 5:= Intg nargs],
safeP, sigSafeMain, pc, ref)])"
apply (frule execSVMInstr_MATCH_loop,assumption+)
apply (simp add: lastState_def)
apply (subgoal_tac
"(nat (nargs - i)) = diff (None, sh, h, inih, [([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)])")
apply (frule execSVMInstr_MATCH_loop_post,assumption+)
apply (simp only: diff_def,force)
by (simp add: diff_def)
(* Axioms *)
axioms equivS_MATCH_bound:
"[| (fst (the (map_of svms l)) ! i) = MATCH off ps;
sh (stackC,topf) = Some (Intg n) |] ==> int off ≤ n"
axioms maxPush_MATCH:
"fst (the (map_of svms l)) ! i = MATCH off ps ==> n + nargs' < int m"
axioms equivS_S'_n_minus_off:
"[| equivS S S' n ctm d g; int off ≤ n; h l' = Some (Arr ty m S') |]
==> ∃ l fs_S'_n_minus_off.
the (d (nat (the_Intg (the (S' (nat (n - int off))))))) = Addr l ∧
h l = Some (Obj cellC fs_S'_n_minus_off) ∧
l' ≠ l"
axioms consTableC_def:
"sha (consTableC, tablef) = Some (Addr l''') ∧
h l''' = Some (Arr ty m''' consTableS)"
axioms consTableC_n_minus_off:
"[| sha (consTableC, tablef) = Some (Addr l''');
h l''' = Some (Arr ty m''' consTableS)|]
==> ∃ l' fs_consTableS_S'_n_minus_off_tagGf.
the (consTableS (nat
(the_Intg (the (fs_S'_n_minus_off (tagGf, cellC)))))) = Addr l' ∧
h l' = Some (Obj cellC fs_consTableS_S'_n_minus_off_tagGf) ∧
the (fs_consTableS_S'_n_minus_off_tagGf (nargsf, consDataC))
= Intg nargs' ∧
nargs' ≥ 0"
axioms consTable_bounds:
"int m''' > the_Intg (the (fs_S'_n_minus_off (tagGf, cellC))) ∧
the_Intg (the (fs_S'_n_minus_off (tagGf, cellC))) ≥ 0"
axioms MATCH_bounds:
"0 ≤ i ∧
0 ≤ the_Intg (the (sh (stackC, topf))) - nargs ∧
i ≤ nargs"
axioms tag_bounds:
"¬ the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf
(tagLf, consDataC))) < 0 ∧
¬ int (length ps - Suc 0) <
the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf
(tagLf, consDataC)))"
lemma drop_append_3:
"drop n xs = [] @ (ys @ zs) ==> drop n xs = ys @ zs"
by simp
lemma drop_Suc_2:
"drop n xs = (y # ys) ==> drop (Suc n) xs = ys"
apply (induct xs arbitrary: n, simp)
apply(simp add:drop_Cons nth_Cons split:nat.splits)
done
lemma drop_length_append:
"drop n xs = (ys @ zs) ==> drop (n + length ys) xs = zs"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma go_End:
"drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
[Ifcmp GreaterEqual labelEndLoop, Load 5, Tableswitch 0 7
[label1, label2, label3, label4, label5, label6, label7, label8]] @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @
InstLabel6 @
InstLabel7 @
InstLabel8 @
Match2 @
Load 3 #
Tableswitch 0 (int (length ps - Suc 0))
(map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0))) ps)) #
bytecode' ==>
drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop))))))))))))))))))))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))))
= Load 3 #
Tableswitch 0 (int (length ps - Suc 0))
(map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0))) ps)) #
bytecode'"
apply (drule drop_Suc_append)+
apply (drule drop_append_3)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (drule drop_length_append)
apply (simp add: labelEndLoop_def)
apply (simp add: nlab1_def)
apply (simp add: nlab2_def)
apply (simp add: nlab3_def)
apply (simp add: nlab4_def)
apply (simp add: nlab5_def)
apply (simp add: nlab6_def)
apply (simp add: nlab7_def)
apply (simp add: nlab8_def)
apply (simp add: nMatch2_def)
apply (simp add: InstLabel1_def)
apply (simp add: InstLabel2_def)
apply (simp add: InstLabel3_def)
apply (simp add: InstLabel4_def)
apply (simp add: InstLabel5_def)
apply (simp add: InstLabel6_def)
apply (simp add: InstLabel7_def)
apply (simp add: InstLabel8_def)
apply (drule drop_length_append)
apply (simp add: Match2_def)
apply (subgoal_tac
"(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))
= (101 + the (cdm (l, i)))")
by simp+
axioms equivS_MATCH:
"equivS S S' n ctm d g
==> equivS (map Val vsa @ S)
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))
(n + nargs') ctm d g"
axioms pc_MATCH:
"Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatch)) (map (λp. the (cdm' (p, 0))) ps) !
nat (the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)))))))))))))))
)))))))))))))))))))) =
the (cdm (ps ! r, 0))"
(* Lemmas for equivS *)
axioms Obj_cells_equals:
" Obj cellC fs_S'_n_minus_off = Obja cellC flds
==> flds = fs_S'_n_minus_off"
lemma equivV_MATCH:
"[| hm b = Some (j,C,vs);
equivH (hm, k) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g;
g b = Some l;
h l = Some (Obj cellC fs_S'_n_minus_off) |]
==> ∀i<length vs. equivV (vs ! i) (argCell fs_S'_n_minus_off i) d g"
apply (simp add: equivH.simps)
apply clarsimp
apply (erule_tac x="b" in ballE)
apply clarsimp
apply (frule Obj_cells_equals,simp)
by (simp add: dom_def)
axioms equivS_extend:
"equivS (map Val vs @ S)
(S' ++ map_of (zip [Suc (nat n)..<nat (2 + (n + int (length vs)))]
(argCell fs_S'_n_minus_off (Suc (length vs)) #
map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(n + int (length vs)) ctm d g"
axioms argCell_Suc_j:
"argCell fs_S'_n_minus_off 0 =
(argCell fs_S'_n_minus_off (Suc (length vs)) # map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0]) !
(nat (1 + (n + int (length vs))) - Suc (nat n))"
lemma S'_map_of_0:
" n ≥ 0
==> (S' ++ map_of (zip [Suc (nat n)..<nat (2 + (n + int (length vs)))]
(argCell fs_S'_n_minus_off (Suc (length vs)) #
map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(nat (n + (1 + int (length vs)))) = Some (argCell fs_S'_n_minus_off 0)"
apply (subst map_add_Some_iff)
apply (rule disjI1)
apply (rule map_of_is_SomeI )
apply (subst map_fst_zip)
apply (subst length_upt,simp)
apply (subst length_upt_rev)
apply arith
apply simp
apply (subst set_zip)
apply simp
apply (rule_tac x="nat (1 + (n + int (length vs))) - Suc (nat n)" in exI)
apply (rule conjI)
apply (subst nth_upt_2)
apply simp apply simp
apply (rule conjI)
apply (rule argCell_Suc_j)
apply (rule conjI)
apply simp
by (subst length_upt_rev,simp)
axioms equivV_HI:
"[| ∀i<Suc (length vs). equivV ((a # vs) ! i) (argCell fs_S'_n_minus_off i) d g |]
==> (∀i<length vs. equivV (vs! i) (argCell fs_S'_n_minus_off i) d g)"
lemma equivS_MATCH [rule_format]:
" equivS S S' n ctm d g
--> n ≥ 0
--> (∀i<length vs. equivV (vs ! i) (argCell fs_S'_n_minus_off i) d g)
--> equivS (map Val vs @ S)
(S' ++ map_of (zip [Suc (nat n)..<nat (n + int (length vs) + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(n + int (length vs)) ctm d g"
apply (induct vs)
apply (simp add: equivS.simps)
apply clarsimp
apply (simp add: equivS.simps)
apply (rule conjI)
apply (subgoal_tac
"equivV a (argCell fs_S'_n_minus_off 0) d g")
apply (subgoal_tac
"the ((S' ++ map_of (zip [Suc (nat n)..<nat (2 + (n + int (length vs)))]
(argCell fs_S'_n_minus_off (Suc (length vs)) #
map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(nat (n + (1 + int (length vs))))) = argCell fs_S'_n_minus_off 0",simp)
apply (subst S'_map_of_0,assumption,simp)
apply (erule_tac x="0" in allE,simp)
apply (frule equivV_HI,simp)
by (rule equivS_extend)
axioms equivS_MATCH_axiom:
"equivS (map Val vsa @ S)
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))
(n + nargs') ctm d g"
(* Lemmas for equivH *)
declare equivH.simps [simp del]
lemma activeCells_MATCH:
"[|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' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)] (map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..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)
(* Lemmas for domH *)
lemma domH_MATCH:
"[| 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 [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))))
l' (the ((h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..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_MATCH:
"[| k' = nat (the_Intg (the (sha (heapC, kf))));
equivH (hm, k) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g;
sha (stackC, Sf) = Some (Addr la);
activeCells regS h k' ∩ {la, l', l''} = {}|]
==> equivH (hm, k)
(h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)] (map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))))
(nat (the_Intg (the (sha (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
"la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))")
apply (frule activeCells_MATCH,simp,simp)
apply (rule conjI, assumption)
by (rule domH_MATCH,assumption,simp)
lemma execSVMInstr_MATCH :
"[| (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) = MATCH off ps;
execSVMInst (MATCH off ps) (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 (MATCH off ps) @ bytecode';
cdm' ⊆m cdm
|] ==> ∃ 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 v1 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 del: execSVMInst.simps)
apply (unfold equivState_def)
apply (elim exE,elim conjE)
apply (subgoal_tac "int off ≤ n")
prefer 2 apply (erule equivS_MATCH_bound, simp)
apply clarify
(* we execute the SVM instruction *)
apply (simp only: execSVMInst.simps)
apply (insert RightNotUndefined)
apply (erule_tac x=S2 in allE)
apply (case_tac "S!+ off")
defer apply (force,force)
apply (case_tac Vala)
defer apply (force, force)
apply (case_tac "hm nata")
apply force
apply (case_tac aha,rename_tac j rest,case_tac rest,rename_tac C vsa)
apply (case_tac "map_of ct C")
apply force
apply (rename_tac tup, case_tac tup,
rename_tac nargs rest', case_tac rest', rename_tac r xa)
apply clarsimp
(* Preconditions *)
apply (frule equivS_S'_n_minus_off,assumption+)
apply (elim exE, elim conjE)
apply (subgoal_tac
"sha (consTableC, tablef) = Some (Addr l''') ∧
h l''' = Some (Arr ty m''' consTableS)")
prefer 2 apply (rule consTableC_def)
apply (erule conjE)
apply (subgoal_tac
"∃ l' fs_consTableS_S'_n_minus_off_tagGf.
the (consTableS (nat (the_Intg (the (fs_S'_n_minus_off (tagGf, cellC)))))) = Addr l' ∧
h l' = Some (Obj cellC fs_consTableS_S'_n_minus_off_tagGf) ∧
the (fs_consTableS_S'_n_minus_off_tagGf (nargsf, consDataC)) = Intg nargs' ∧
nargs' ≥ 0")
apply (elim exE, elim conjE)
prefer 2
apply (rule_tac l'''="l'''" in consTableC_n_minus_off,assumption+)
(* we go on with the main goal. We instantiate the arrival JVM state*)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (n + nargs'))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j))
[nat nargs'>..0]))))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([],vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0))) ps) !
nat (the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))
))))))))))))))))))))))))))))))))),
ag,bd)]" in exI)
(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "length vs = 10")
prefer 2 apply (rule length_vs)
apply (rule conjI)
apply (subgoal_tac
"P'\<turnstile> (None,sha,h,inih,[([],
vs, safeP, sigSafeMain, the (cdm (l,i)), ag,bd)])
-jvm->
(None,sha,h,inih,[([Addr la],
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: GetStatic Sf StackC *)
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") apply simp
apply (unfold trInstr.simps, unfold Let_def)
apply (unfold Match11_def)
apply (rule nth_via_drop_append) apply force
(* Getstatic topf stackC *)
apply (drule_tac ?ms="bytecode'" and ?y= "Getstatic Sf stackC"
in drop_Suc_append_2)
apply (subgoal_tac
"P'\<turnstile> (None, sha, h, inih,
[([Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg n,Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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 (int l)) *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sha,h,inih,
[([Intg n,Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (int off),
Intg n,Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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 (int off))",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (int off),
Intg n,Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg ( n - int off),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (n - int off),
Addr la],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (S' (nat (n - int off)))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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)))))))) = ArrLoad")
apply (simp del: Let_def execSVMInst.simps)
apply (simp (no_asm) add: raise_system_xcpt_def)
apply (rule conjI) apply (force,force)
apply (erule nth_via_drop_append)
(* Store 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,sha,h,inih,[([the (S' (nat (n - int off)))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,[([],vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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))))))))) =
Store (Suc 0)") apply (simp)
apply (erule nth_via_drop_append)
(* Getstatic safeDirf dirCellC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha, h, inih,
[([], vs[Suc 0 := the (S' (nat (n - int off)))], safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Addr l''], vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del:append.append_Cons)
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)))))))))) =
Getstatic safeDirf dirCellC",simp)
apply (erule nth_via_drop_append)
(* Load 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr l''], vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (S' (nat (n - int off))), Addr l''],
vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
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))))))))) =
Load (Suc 0)") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (S' (nat (n - int off))), Addr l''],
vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Addr laa],
vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
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)))))))))) =
ArrLoad") apply (simp (no_asm_simp) add: raise_system_xcpt_def)
apply (subgoal_tac "the_Intg (the (S' (nat (n - int off)))) < int m''
∧ 0 ≤ the_Intg (the (S' (nat (n - int off))))")
prefer 2 apply (rule safeDir_bounds)
apply (rule conjI) apply (force,force)
apply (erule nth_via_drop_append)
(* Store 6 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr laa],
vs[Suc 0 := the (S' (nat (n - int off)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
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)))))))))))) =
Store 6") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Load 6 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Addr laa],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
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 (simp del: append.append_Cons)
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 6") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Getfield tagGf cellC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr laa],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (fs_S'_n_minus_off (tagGf, cellC))],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
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 (simp del: append.append_Cons)
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)))))))))))))) =
Getfield tagGf cellC") apply (simp (no_asm_simp) add: raise_system_xcpt_def)
apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Store 2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (fs_S'_n_minus_off (tagGf, cellC))],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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))))))))))))))) =
Store 2") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Getstatic tablef consTableC *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"sha (consTableC, tablef) = Some (Addr l''') ∧
h l''' = Some (Arr ty m''' consTableS)")
apply (elim conjE)
prefer 2 apply (rule consTableC_def)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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,inih,
[([Addr l'''],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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 tablef consTableC") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Load 2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr l'''],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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,inih,
[([the (fs_S'_n_minus_off (tagGf, cellC)),
Addr l'''],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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))))))))))))))))) =
Load 2") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (fs_S'_n_minus_off (tagGf, cellC)),
Addr l'''],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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,inih,
[([Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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)))))))))))))))))) =
ArrLoad") apply (simp (no_asm_simp) add: raise_system_xcpt_def)
apply (subgoal_tac
"int m''' > the_Intg (the (fs_S'_n_minus_off (tagGf, cellC))) ∧
the_Intg (the (fs_S'_n_minus_off (tagGf, cellC))) ≥ 0")
apply (simp (no_asm_simp))
apply simp
apply (rule consTable_bounds)
apply (erule nth_via_drop_append)
(* Dup *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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,h,inih,
[([Addr l'a,
Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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))))))))))))))))))) =
Dup") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Getfield tagLf consDataC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr l'a,
Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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,h,inih,
[([the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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 (simp del: append.append_Cons)
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)))))))))))))))))))) =
Getfield tagLf consDataC") apply (simp (no_asm_simp) add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Store 3 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC))],
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)])
-jvm->
(None,sha,h,inih,
[([Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 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 (simp del: append.append_Cons)
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 (Suc (the (cdm (l, i))))))))))))))))))))) =
Store 3") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Getfield nargsf consDataC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Addr l'a],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (the (cdm (l, i)))))))))))))))))))))) =
Getfield nargsf consDataC") apply (simp (no_asm_simp) add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Store 4 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := the (fs_consTableS_S'_n_minus_off_tagGf (nargsf, consDataC))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))) =
Store 4") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* LitPush (Intg 0) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg 0],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))) =
LitPush (Intg 0)") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Store 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 0],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))) =
Store 5") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg n],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))) =
Getstatic topf stackC") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Load 4 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg n],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg nargs',
Intg n],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))) =
Load 4") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg nargs',
Intg n],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (n + nargs')],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))))) =
BinOp Add") apply (simp (no_asm_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 (n + nargs')],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 + nargs')),
h,inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg 0],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))))) =
Putstatic topf stackC") apply (simp (no_asm_simp))
apply (erule nth_via_drop_append)
(* Match12 *)
apply (drule drop_Suc_append)
apply (drule drop_append_3)
apply (subgoal_tac
"0 ≤ the_Intg (vs!5) ∧
0 ≤ the_Intg (the (sh (stackC, topf))) - the_Intg (vs!4) ∧
the_Intg (vs!5) ≤ the_Intg (vs!4)")
apply (elim conjE)
prefer 2 apply (rule MATCH_bounds)
apply (frule_tac inih="inih" and
ref="(ag,bd)" and
nargs="nargs'" and
i ="0" and
l ="laa" and
h = "h" and
ty = "ty" and
m = "m" and
S' = "S'" and
vs="vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))]" and
sh="sha((stackC, topf) \<mapsto> Intg (n + nargs'))"
in execSVMInstr_MATCH_loop_state)
apply (simp,simp)
apply (simp add: Sf_def add: topf_def)
apply (simp,simp,simp,simp,simp,simp,simp,simp)
apply (unfold exec_all_def)
apply (simp,erule rtrancl_trans)
(* Load 4 *)
apply (simp del: append.append_Cons
add: Match12_def add: Sf_def add: topf_def)
apply (fold topf_def)
apply (subgoal_tac
"P'\<turnstile> (None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))))))) =
Load 4") apply (simp (no_asm_simp))
apply (simp, erule nth_via_drop)
(* Load 5 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([Intg nargs',
Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))))))) =
Load 5") apply (simp (no_asm_simp))
apply (simp, erule nth_via_drop)
(* Ifcmp GreaterEqual labelEndLoop *)
apply (drule drop_Suc_append)
apply (subgoal_tac
"P'\<turnstile> (None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([Intg nargs',
Intg nargs'],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 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 + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + nat labelEndLoop,
ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
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
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))))))))) =
Ifcmp GreaterEqual labelEndLoop") apply (simp (no_asm_simp))
apply (simp add: labelEndLoop_def)
apply (simp, erule nth_via_drop)
(* Load 3 *)
apply (frule go_End)
apply (subgoal_tac
"P'\<turnstile> (None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + nat labelEndLoop,
ag, bd)])
-jvm->
(None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + nat labelEndLoop + 1,
ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop)))))))))))))))))))))))))))))) =
Load 3") apply (simp (no_asm_simp))
apply (simp, erule nth_via_drop)
(* Tableswitch 0 (int (length ps - Suc 0)) (map (λn. trAddr n (the (cdm (l, i)) + incMatch)) (map (λp. the (cdm' (p, 0))) ps)) *)
apply (thin_tac "drop ?x ?xs = ?ys") thm drop_Suc_2
apply (drule drop_Suc_2)
apply (subgoal_tac
"P'\<turnstile> (None,
sha((stackC, topf) \<mapsto> Intg (n + nargs')),
h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih,
[([the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))],
vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs'],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + nat labelEndLoop + 1,
ag, bd)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n + nargs')), h(la \<mapsto>
Arr ty m
(S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)] (map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))),
inih, [([], vs[Suc 0 := the (S' (nat (n - int off))), 6 := Addr laa, 2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)), 4 := Intg nargs', 5 := Intg nargs'],
safeP, sigSafeMain,
Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatch)) (map (λp. the (cdm' (p, 0))) ps) !
nat (the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))))))))))))))))))))))))))))))))))),
ag, bd)])")
apply (unfold exec_all_def)
apply (simp del: append.append_Cons)
apply simp
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop))))))))))))))))))))))))))))))) =
Tableswitch 0 (int (length ps - Suc 0))
(map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0))) ps))") apply (simp (no_asm_simp))
apply (subgoal_tac
"¬ the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))) < 0 ∧
¬ int (length ps - Suc 0) < the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)))",simp)
apply (rule tag_bounds)
apply (simp, erule nth_via_drop)
(* Now we prove the equivalence relation *)
apply (rule_tac x="vs[Suc 0 := the (S' (nat (n - int off))),
6 := Addr laa,
2 := the (fs_S'_n_minus_off (tagGf, cellC)),
3 := the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC)),
4 := Intg nargs',
5 := Intg nargs']" in exI)
apply (rule_tac x="Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)) + nat labelEndLoop +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0))) ps) !
nat (the_Intg (the (fs_consTableS_S'_n_minus_off_tagGf (tagLf, consDataC))
)))))))))))))))))))))))))))))))))" in exI)
apply (rule conjI)
apply (rule_tac x="ag" in exI)
apply (rule_tac x="bd" in exI)
apply (rule refl)
apply (rule_tac x="la" in exI)
apply (rule conjI, simp add: Sf_def add: topf_def)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="S' ++ map_of (zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j))
[nat nargs'>..0]))" in exI)
apply (rule_tac x="(n + nargs')" in exI)
apply (rule_tac x="l'" in exI)
apply (rule conjI, assumption)
apply (rule_tac x="regS" in exI)
apply (rule_tac x="l''" in exI)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI) apply (rule activeCells)
apply (simp add: heapC_def add: stackC_def)
apply (rule conjI) apply (rule activeCells_2)
apply (simp add: heapC_def add: stackC_def,simp)
apply (rule conjI) apply (rule activeCells_2)
apply (simp add: heapC_def add: stackC_def,simp)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, simp add: heapC_def add: stackC_def)
apply (rule conjI)
apply (rule_tac x="m'" in exI,simp)
apply (rule conjI, simp add: dirCellC_def add: stackC_def)
apply (rule_tac x="m''" in exI)
apply (rule_tac x="d" in exI)
apply (rule conjI,simp)
apply (rule_tac x="g" in exI,simp add: heapC_def add: stackC_def)
apply (fold heapC_def, fold stackC_def)
apply (rule conjI) apply (rule equivH_MATCH,simp,assumption+,force) (* equivH *)
apply (rule conjI) apply (rule maxPush_MATCH,assumption)
apply (rule conjI) apply (rule equivS_MATCH_axiom)
apply (rule pc_MATCH) (* pc *)
done
end
lemma length_upt_rev:
length [i>..j] = i - j
lemma nth_upt_2:
k < j ∧ i ≤ k ==> [i..<j] ! (k - i) = k
lemma drop_append_3:
drop n xs = [] @ ys @ zs ==> drop n xs = ys @ zs
lemma drop_length_append:
drop n xs = ys @ zs ==> drop (n + length ys) xs = zs
lemma drop_endlabel1:
drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc pc))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
[Goto endlabel1] @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode
==> drop (nat (12 + int pc + endlabel1))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match2 @ bytecode
lemma oneStep_MATCH:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; l ≠ la; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs);
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]);
i < nargs |]
==> P' |- (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) -jvm-> (None, sh, h(the_Addr (the (sh (stackC, Sf))) |->
Arr ty m
(S'(nat (the_Intg (the (sh (stackC, topf))) - i)
|-> argCell fs (nat i + 1)))),
inih,
[([], vs[4 := Intg nargs, 5 := Intg (i + 1)], safeP,
sigSafeMain, pc, ref)])
lemma oneStep_state:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la); l ≠ la;
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs);
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
i < nargs |]
==> oneStep P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) =
(None, sh, h(the_Addr (the (sh (stackC, Sf))) |->
Arr ty m
(S'(nat (the_Intg (the (sh (stackC, topf))) - i) |->
argCell fs (nat i + 1)))),
inih,
[([], vs[4 := Intg nargs, 5 := Intg (i + 1)], safeP, sigSafeMain, pc,
ref)])
lemma diff_monotone:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la; i < nargs;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
Suc n =
diff (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) |]
==> n = diff (oneStep P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]))
lemma steps_monotone:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la; i < nargs;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
Suc n =
diff (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) |]
==> steps
(diff (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]))
P' (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) =
steps
(diff (oneStep P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)])))
P' (oneStep P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]))
lemma MATCH_loop:
[| n = diff (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]);
(P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode |]
==> P' |- (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) -jvm-> steps n P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP,
sigSafeMain, pc, ref)])
lemma execSVMInstr_MATCH_loop:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) |]
==> P' |- s -jvm-> lastState P' s
lemma map_argCell_upt_rev:
[| i < nargs; 0 ≤ i |]
==> map (λj. argCell fs (Suc j)) [nat nargs>..nat (i + 1)] @
[argCell fs (Suc (nat i))] =
map (λj. argCell fs (Suc j)) [nat nargs>..nat i]
lemma empty_map_add_2:
m ++ empty = m
lemma upt_Suc_append_topf:
[| i < nargs; 0 ≤ i; 0 ≤ the_Intg (the (sh (stackC, topf))) - nargs |]
==> [Suc (nat (the_Intg (the (sh (stackC, topf))) - nargs))..<
nat (the_Intg (the (sh (stackC, topf))) - i)] @
[nat (the_Intg (the (sh (stackC, topf))) - i)] =
[Suc (nat (the_Intg (the (sh (stackC, topf))) - nargs))..<
nat (the_Intg (the (sh (stackC, topf))) - i + 1)]
lemma execSVMInstr_MATCH_loop_post:
[| n = diff (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]);
(P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; 0 ≤ i; 0 ≤ the_Intg (the (sh (stackC, topf))) - nargs;
i ≤ nargs; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode |]
==> steps n P'
(None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc, ref)]) =
(None, sh,
let vitems = map (λj. argCell fs (j + 1)) [nat nargs>..nat i];
idxs =
map (λj. j)
[nat (the_Intg (the (sh (stackC, topf))) - nargs) + 1..<
nat (the_Intg (the (sh (stackC, topf))) - i + 1)];
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sh (stackC, Sf))) |-> Arr ty m S''),
inih,
[([], vs[4 := Intg nargs, 5 := Intg nargs], safeP, sigSafeMain, pc, ref)])
lemma execSVMInstr_MATCH_loop_state:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
length vs = 10; vs ! 6 = Addr l; sh (stackC, Sf) = Some (Addr la);
h la = Some (Arr ty m S'); h l = Some (Obj cellC fs); l ≠ la; 0 ≤ i;
0 ≤ the_Intg (the (sh (stackC, topf))) - nargs; i ≤ nargs;
drop pc
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Match12 @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @ Match2 @ bytecode;
s = (None, sh, h, inih,
[([], vs[4 := Intg nargs, 5 := Intg i], safeP, sigSafeMain, pc,
ref)]) |]
==> P' |- s -jvm-> (None, sh,
let vitems =
map (λj. argCell fs (j + 1)) [nat nargs>..nat i];
idxs =
map (λj. j)
[nat (the_Intg (the (sh (stackC, topf))) - nargs) +
1..<
nat (the_Intg (the (sh (stackC, topf))) - i + 1)];
S'' = S' ++ map_of (zip idxs vitems)
in h(the_Addr (the (sh (stackC, Sf))) |-> Arr ty m S''),
inih,
[([], vs[4 := Intg nargs, 5 := Intg nargs], safeP,
sigSafeMain, pc, ref)])
lemma drop_append_3:
drop n xs = [] @ ys @ zs ==> drop n xs = ys @ zs
lemma drop_Suc_2:
drop n xs = y # ys ==> drop (Suc n) xs = ys
lemma drop_length_append:
drop n xs = ys @ zs ==> drop (n + length ys) xs = zs
lemma go_End:
drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
[Ifcmp GreaterEqual labelEndLoop, Load 5,
Tableswitch 0 7
[label1, label2, label3, label4, label5, label6, label7, label8]] @
InstLabel1 @
InstLabel2 @
InstLabel3 @
InstLabel4 @
InstLabel5 @
InstLabel6 @
InstLabel7 @
InstLabel8 @
Match2 @
Load 3 #
Tableswitch 0 (int (length ps - Suc 0))
(map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0::'g))) ps)) #
bytecode'
==> drop (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat labelEndLoop))))))))))))))))))))))))))))))
(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) =
Load 3 #
Tableswitch 0 (int (length ps - Suc 0))
(map (λn. trAddr n (the (cdm (l, i)) + incMatch))
(map (λp. the (cdm' (p, 0::'g))) ps)) #
bytecode'
lemma equivV_MATCH:
[| hm b = Some (j, C, vs);
equivH (hm, k) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g;
g b = Some l; h l = Some (Obj cellC fs_S'_n_minus_off) |]
==> ∀i<length vs. equivV (vs ! i) (argCell fs_S'_n_minus_off i) d g
lemma S'_map_of_0:
0 ≤ n
==> (S' ++
map_of
(zip [Suc (nat n)..<nat (2 + (n + int (length vs)))]
(argCell fs_S'_n_minus_off (Suc (length vs)) #
map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(nat (n + (1 + int (length vs)))) =
Some (argCell fs_S'_n_minus_off 0)
lemma equivS_MATCH:
[| equivS S S' n ctm d g; 0 ≤ n;
!!i. i < length vs ==> equivV (vs ! i) (argCell fs_S'_n_minus_off i) d g |]
==> equivS (map Val vs @ S)
(S' ++
map_of
(zip [Suc (nat n)..<nat (n + int (length vs) + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [length vs>..0])))
(n + int (length vs)) ctm d g
lemma activeCells_MATCH:
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' ++
map_of
(zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))))
(nat (the_Intg (the (sha (heapC, kf)))))
lemma domH_MATCH:
[| 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 [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j))
[nat nargs'>..0])))))
l' (the ((h(la |->
Arr ty m
(S' ++
map_of
(zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j))
[nat nargs'>..0])))))
l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma equivH_MATCH:
[| k' = nat (the_Intg (the (sha (heapC, kf))));
equivH (hm, k) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g;
sha (stackC, Sf) = Some (Addr la);
activeCells regS h k' ∩ {la, l', l''} = {} |]
==> equivH (hm, k)
(h(la |->
Arr ty m
(S' ++
map_of
(zip [Suc (nat n)..<nat (n + nargs' + 1)]
(map (λj. argCell fs_S'_n_minus_off (Suc j)) [nat nargs'>..0])))))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma execSVMInstr_MATCH:
[| (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 = MATCH off ps;
execSVMInst (MATCH off ps) (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 (MATCH off ps) @ bytecode';
cdm' ⊆m cdm |]
==> ∃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')