(*
Title: Lemmas for the translation SVM to JVM. MATCHN
Author: Javier de Dios and Ricardo Pe~na
Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_MATCHN
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]
(* Axioms *)
axioms equivS_MATCHN:
"n >= int off"
declare extractBytecode_def [simp del]
declare initConsTable_def [simp del]
constdefs if' :: "[bool, 'a, 'a] => 'a"
"if' c a b ≡ if c then a else b"
axioms pc_MATCHN:
"if' (the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) < 0 ∨
int (m + 1) < the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
nat (int (2 + m)))))))))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
nat (the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) -
0)))))))))) =
the (cdm (case S !+ off of Val (IntT i) => let r = nat i - v; p = if 0 ≤ r ∧ r ≤ m - 1 then ps ! r else ps ! m in (p, 0)
| Val (BoolT b) => let p = if ¬ b then ps ! 0 else ps ! 1 in (p, 0)))"
declare if'_def [simp del]
lemma execSVMInstr_MATCHN :
"[| (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) = MATCHN off v m ps;
execSVMInst (MATCHN off v m 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 (MATCHN off v m 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)
apply (unfold equivState_def)
apply (elim exE,elim conjE)
(* we go on with the main goal. We instantiate the arrival JVM state*)
apply (rule_tac x="None" in exI)
apply (rule_tac x="sha" in exI)
apply (rule_tac x="h" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([], vs,
safeP, sigSafeMain,
if' ((the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) < 0) ∨
(the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) > (int (m + 1))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
nat (int (2 + m )))))))))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
(nat (the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) - 0))))))))))),
ref)]" in exI)
(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "∃ vs pc . fms=([],vs,safeP,sigSafeMain,pc,ref)#[]")
prefer 2 apply simp
apply (erule exE)+
apply (rule conjI)
apply (unfold exec_all_def)
apply (subgoal_tac "PC = (l,i)") prefer 2 apply simp
apply simp apply (elim conjE) apply clarsimp
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,[([], vs, safeP, sigSafeMain, the (cdm (l,i)), ag,bd)]) -jvm->
(None,sha,h,inih,[([the (sha (stackC,Sf))], vs, safeP, sigSafeMain, the (cdm (l,i)) + 1, ag,bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
(* We prove the first step of the SVM *)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (unfold extractBytecode_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
the (cdm (l, i))) = Getstatic Sf stackC",simp)
apply (unfold trInstr.simps, unfold Let_def)
apply (erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha, h, inih,
[([the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! Suc (the (cdm (l, i)))) =
Getstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg (int l)) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (int off),
the (sha (stackC,topf)),the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (the (cdm (l, i)))))) =
LitPush (Intg (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),
the (sha (stackC,topf)),the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg ( n - int off),
the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (Suc (the (cdm (l, i))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (n - int off),
the (sha (stackC, Sf))],
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 (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")
(* Equivalencia de entornos *)
apply (case_tac "S !+ off",simp)
apply (case_tac "Vala")
apply (simp,insert RightNotUndefined, erule_tac x= "S2" in allE,force)
apply simp apply (rename_tac n1)
apply (subgoal_tac "n >= int off") prefer 2 apply (rule equivS_MATCHN, simp add: raise_system_xcpt_def) (* Para int *)
apply simp apply (subgoal_tac "n >= int off") prefer 2 apply (rule equivS_MATCHN, simp add: raise_system_xcpt_def) (* Para bool *)
apply (simp,insert RightNotUndefined, erule_tac x= "S2" in allE,force)
apply (simp,insert RightNotUndefined, erule_tac x= "S2" in allE,force)
apply (erule nth_via_drop_append)
(* LitPush (Intg (int v)) *)
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,
[([Intg (int v),
the (S' (nat (n - int off)))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))) =
LitPush (Intg (int v))",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 v),
the (S' (nat (n - int off)))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([Intg (the_Intg (the (S' (nat (n - int off)))) - int v)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* Tableswitch 0 (int (m + 1)) pcs' *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (S' (nat (n - int off)))) - int v)],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, bd)])
-jvm->
(None,sha,h,inih,
[([],
vs, safeP, sigSafeMain,
if' ((the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) < 0) ∨
(the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) > (int (m + 1))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
nat (int (2 + m )))))))))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
(nat (the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) - 0))))))))))),
ag, bd)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) =
Tableswitch 0 (int (m + 1)) (map (λn. trAddr n (the (cdm (l, i)) + incMatchN))
(map (λp. the (cdm' (p, 0))) ps))",simp)
apply (simp add: if'_def)
apply (erule nth_via_drop_append)
apply simp
(* Now we prove the equivalence relation *)
apply (rule_tac x="hm" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="k0" in exI)
apply (rule_tac x="(case S !+ off of
Val (IntT i) => let r = nat i - v;
p = if 0 ≤ r ∧ r ≤ m - 1 then ps ! r else ps ! m
in (p,0)
| Val (BoolT b) => let p = if ¬ b then ps ! 0 else ps ! 1
in (p,0))" in exI)
apply (rule_tac x="S" in exI)
apply (rule_tac x="sha" in exI)
apply (rule_tac x="h" in exI)
apply (rule_tac x="inih" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="if' ((the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) < 0) ∨
(the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) > (int (m + 1))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
nat (int (2 + m )))))))))))
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) +
nat (map (λn. trAddr n (the (cdm (l, i)) + incMatchN)) (map (λp. the (cdm' (p, 0))) ps) !
(nat (the_Intg (Intg (the_Intg (the (S' (nat (n - int off)))) - int v)) - 0)))))))))))" in exI)
apply (rule_tac x="ref" in exI)
apply (rule_tac x="nat (the_Intg (the (sha (heapC, kf))))" in exI)
apply (rule_tac x=" nat (the_Intg (the (sha (heapC, k0f))))" in exI)
apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="ma" in exI)
apply (rule_tac x="S'" in exI)
apply (rule_tac x="n" in exI)
apply (rule_tac x="l'" in exI)
apply (rule_tac x="regS" in exI)
apply (rule_tac x="l''" in exI)
apply (rule_tac x="m'" in exI)
apply (rule_tac x="m''" in exI)
apply (rule_tac x="d" in exI)
apply (rule_tac x="g" in exI)
apply (rule conjI)
apply simp
apply (case_tac "S!+off")
apply simp
apply (case_tac "Vala")
apply simp
apply (insert RightNotUndefined)
apply (erule_tac x= "S2" in allE, force)
apply clarsimp
apply clarsimp
apply clarsimp
apply (insert RightNotUndefined)
apply (erule_tac x= "S2" in allE, force)
apply clarsimp
apply (insert RightNotUndefined)
apply (erule_tac x= "S2" in allE, force)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, simp)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, clarsimp)
by (rule pc_MATCHN)
end
lemma execSVMInstr_MATCHN:
[| (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 = MATCHN off v m ps;
execSVMInst (MATCHN off v m 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 (MATCHN off v m 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')