Theory dem_CALL

(* 
   Title: Lemmas for the translation SVM to JVM. CALL
   Author: Ricardo Pe~na and Javier de Dios
   Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_CALL
imports "../JVMSAFE/JVMExec" "../JVMSAFE/State" SVM2JVM SVMSemantics CertifSVM2JVM 
                             dem_translation
begin

no_translations "Norm s" == "(None,s)"
no_translations "ex_table_of m" == "snd (snd (snd m))"

declare trInstr.simps [simp del]
declare equivS.simps [simp del]
declare extractBytecode_def [simp del]
declare initConsTable_def   [simp del]

axioms pushregion_method:
 "[| s = (None, shp, hp, ihp, 
            ([],vs,safeP, sigSafeMain,pc,z1,z2)#[]);
  shp (stackC,topf) = Some (Intg k);
  shp (stackC,Sf) = Some (Addr l);
  shp (heapC,regionsf) = Some (Addr l');  hp l' = Some  (Arr ty m regS);
  shp (dirCellC,safeDirf) = Some (Addr l''); 
  Invoke_static heapC pushRegion [] = fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc
  |] ==> 
  P' |- s -jvm-> (None, shp ((heapC,kf)\<mapsto> Intg (k+1)), 
                  hp(l' \<mapsto> Arr ty ma (regS (nat k + 1 \<mapsto> Addr lnew)))
                    (lnew \<mapsto> Obj cellC (empty ((izqf,cellC)\<mapsto> Addr lnew)
                                              ((derf,cellC)\<mapsto> Addr lnew))), 
                  ihp, ([],loc,safeP,sigSafeMain,pc+1,z1,z2)#[]) ∧
       lnew ∉ {l,l',l''} ∧
       lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))"

(* Lemmas for activeCells *)

declare equivH.simps [simp del]


(* Lemmas for activeCells *)

declare equivH.simps [simp del]

lemma cellsReg_monotone_3 [rule_format]:
  " x ∈ cellsReg (h(l' \<mapsto> A, l'' \<mapsto> B)) l
    --> x ≠ l
    --> l ≠ l'
    --> l ≠ l''
    --> x = nextCell h l"
apply (rule impI)
apply (erule cellsReg.induct,simp)
by (simp add: nextCell_def)



lemma cellsReg_monotone_4 [rule_format]:
  " x ∈ cellsReg h l
    --> x ≠ l
    --> l ≠ l'
    --> l ≠ l''
    --> x = nextCell (h(l' \<mapsto> A, l'' \<mapsto> B)) l"
apply (rule impI)
apply (erule cellsReg.induct,simp)
by (simp add: nextCell_def)



lemma activeCells_CALL:
  "[| l' ∉ activeCells regS dh (nat (the_Intg (the (sha (heapC, kf)))));
     lnew ∉ activeCells regS dh (nat (the_Intg (the (sha (heapC, kf)))))
    |] 
   ==> activeCells regS dh (nat (the_Intg (the (sha (heapC, kf))))) =
       activeCells (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew))
        (dh(l' \<mapsto> Arr ty m' (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)), lnew \<mapsto>
         Obj cellC [(izqf, cellC) \<mapsto> Addr lnew, (derf, cellC) \<mapsto> Addr lnew]))
        (nat (the_Intg (the (sha (heapC, kf))) + 1))"
apply (frule l_not_in_cellReg)
apply (frule_tac l="lnew" in l_not_in_cellReg)
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: activeCells_def,clarsimp)
 apply (unfold region_def, simp add: Let_def, elim conjE)
 apply (rule_tac x="j" in exI,simp) 
 apply (rule conjI, simp)
 apply (rule cellReg_step) 
  apply (rule cellReg_basic) 
 apply (erule_tac x="j" in allE) 
 apply (rule cellsReg_monotone_1) 
   apply (rule cellReg_step)
    apply (rule cellReg_basic)
   apply (rule cellsReg_monotone_1,assumption+) 
   apply (rule l_not_in_regs)
   apply (erule_tac x="j" in allE,simp,simp)
 apply (rule l_not_in_regs)
 apply (erule_tac x="j" in allE)+
 apply simp 
apply (rule subsetI)
apply (unfold activeCells_def)
apply (unfold region_def, simp add: Let_def)
apply (erule exE)
apply (case_tac 
  " j < Suc (nat (the_Intg (the (sha (heapC, kf)))))",simp)
 apply (rule_tac x="j" in exI,simp)
 apply (elim conjE)
 apply (rule cellReg_step)
  apply (rule cellReg_basic)
 apply (rule cellsReg_monotone_3,simp,simp)
   apply (rule l_not_in_regs)
  apply (erule_tac x="j" in allE)+ apply simp
   apply (rule l_not_in_regs)
 apply (erule_tac x="j" in allE)+ apply simp
apply (elim conjE)
apply (subgoal_tac
  " j = nat (the_Intg (the (sha (heapC, kf))) + 1)",simp)
 prefer 2 apply simp
apply (subgoal_tac "nat (the_Intg (the (sha (heapC, kf))) + 1) = Suc (nat (the_Intg (the (sha (heapC, kf)))))")
 prefer 2 apply arith
apply simp
apply (subgoal_tac "x=lnew",simp) 
apply (erule cellsReg.induct)
apply simp
by (simp add: nextCell_def)



(* Lemmas for domH *)


lemma domH_CALL:
  "[| l' ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
     lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
     lnew ∉ {la,l',l''};
     ∀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'a. l'a = the (g l) ∧
                equivC (the (H l))
                 (h(l' \<mapsto> Arr ty m' (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)), lnew \<mapsto>
                  Obj cellC [(izqf, cellC) \<mapsto> Addr lnew, (derf, cellC) \<mapsto> Addr lnew]))
                 l'a (the ((h(l' \<mapsto> Arr ty m' (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)), lnew \<mapsto>
                            Obj cellC [(izqf, cellC) \<mapsto> Addr lnew, (derf, cellC) \<mapsto> Addr lnew]))
                            l'a))
                 (nat (the_Intg (the (sha (heapC, kf))) + 1))
                 com (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)) d g"
apply (frule l_not_in_cellReg)
apply (frule_tac l="lnew" in 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'a" in exI) apply (elim conjE)
 apply (rule conjI, assumption)
apply clarsimp
apply (rule conjI, rule impI)
apply (simp add: activeCells_def)
apply (simp add: activeCells_def)
apply (erule_tac x="j" in allE) apply simp
apply (subgoal_tac "the (g l) ≠ lnew",simp)
 prefer 2 apply blast
apply (rule impI)
apply (rule conjI, simp)
apply (rule_tac x="Obja" in exI)
apply (rule_tac x="flds" in exI) apply simp
apply (simp add: region_def)
apply clarsimp
apply (rule cellReg_step) 
 apply (rule cellReg_basic)
 apply (rule cellsReg_monotone_4) apply assumption+
 apply (rule l_not_in_regs)
 apply (erule_tac x="j" in allE) apply simp
apply (rule l_not_in_regs)
apply (erule_tac x="j" in allE)
apply (erule_tac x="j" in allE)
apply (erule_tac x="j" in allE)
by simp



axioms kf_ge_0:
  "the_Intg (the (sha (heapC, kf))) >= 0"

lemma equivH_CALL:
  "[|((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
    (v, sh, dh, ih, fms) = (None, sha, h, inih, [([], vs, safeP, sigSafeMain, pc, ref)]);
    k' = nat (the_Intg (the (sha (heapC, kf)))); 
    k0' = nat (the_Intg (the (sha (heapC, k0f)))); 
    sha (stackC, Sf) = Some (Addr la);
    lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
    distinct [la, l', l'']; activeCells regS h k' ∩ {la, l', l''} = {}; h la = Some (Arr ty m S');
    sha (stackC, topf) = Some (Intg n); sha (heapC, regionsf) = Some (Addr l'); h l' = Some (Arr ty m' regS);
    lnew ∉ {la,l',l''};
     inj_on g (dom H); equivH (H, ka) h k' com regS d g|]
       ==> equivH (hm, Suc k)
           (dh(l' \<mapsto> Arr ty m' (regS(k' + 1 \<mapsto> Addr lnew)), lnew \<mapsto> Obj cellC [(izqf, cellC) \<mapsto> Addr lnew, (derf, cellC) \<mapsto> Addr lnew]))
           (nat (the_Intg (the ((sh((heapC, kf) \<mapsto> Intg (the_Intg (the (sh (heapC, kf))) + 1))) (heapC, kf))))) com
           (regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)) d g"
apply (simp add: heapC_def add: stackC_def)
apply (fold heapC_def)
apply (unfold equivH.simps, elim conjE)
apply (rule conjI, clarsimp) 
apply (subgoal_tac "the_Intg (the (sha (heapC, kf))) >= 0",simp) 
 apply (rule kf_ge_0)
apply (rule conjI, frule_tac l'="l'" in activeCells_CALL,assumption+,simp) 
apply (rule conjI, assumption)
apply (subgoal_tac "lnew ∉ {la,l',l''}")
apply (rule domH_CALL,assumption+)
by clarsimp


axioms activeCells_3:
  "[| l' ∉ activeCells regS h k; l ≠ l'; l ≠ l'' |] 
   ==> l' ∉ activeCells regS (h(l \<mapsto> A, l''\<mapsto> B)) k"

axioms activeCells_3_1:
  "[| l' ∉ activeCells regS h k |] 
   ==> l' ∉ activeCells regS (h(l' \<mapsto> A, l''\<mapsto> B)) k"

axioms activeCells_4:
  "la ∉ activeCells regS h k
   ==> la ∉ activeCells regS' h k'"



axioms kf_Intg:
  "sha (heapC, kf) = Some (Intg j)"

axioms p_in_dom_cdm':
  "(p, 0) ∈ dom cdm'"


axioms lnew_notin_activeCells:
  "lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))"


lemma execSVMInstr_CALL :
   "[| (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) = CALL p;
       execSVMInst (CALL p) (map_of ct) (hm, k) k0 (l, i) S = Either.Right S2;
       drop (the (cdm (l, i))) (extractBytecode P') =
       trInstr (the (cdm (l, i))) cdm' ctm' com pcc (CALL p) @ 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 v tup)
apply (case_tac tup)
apply (rename_tac sh tup)
apply (case_tac tup)
apply (rename_tac dh tup)
apply (case_tac tup)
apply (rename_tac ih fms)
apply (simp)

(* We unfold the equivalence relation definition *)
apply (unfold equivState_def)
apply (elim exE,elim conjE)

(* We instantiate the arrival JVM state*)
apply (rule_tac x="None" in exI)
apply (rule_tac x="sh((heapC, kf) \<mapsto> Intg (the_Intg (the (sh (heapC, kf)))+1))" in exI)
apply (rule_tac x="dh(l' \<mapsto> Arr ty m' (regS (k'+1 \<mapsto> Addr lnew)))
      (lnew \<mapsto> Obj cellC (empty ((izqf,cellC)\<mapsto> Addr lnew)
                                       ((derf,cellC)\<mapsto> Addr lnew)))" in exI)
apply (rule_tac x=ih in exI)
apply (rule_tac x="[([], vs, safeP, sigSafeMain, the (cdm (p, 0)), ref)]" in exI)
apply (rule conjI)
apply (unfold extractBytecode_def)


(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "P'\<turnstile>  (v,sh,dh,ih,fms)  -jvm->
      (None, sh ((heapC,kf)\<mapsto> Intg (the_Intg (the (sh (heapC, kf)))+1)), 
             dh (l' \<mapsto> Arr ty m' (regS (nat (the_Intg (the (sh (heapC, kf))))+1 \<mapsto> Addr lnew)))
                (lnew \<mapsto> Obj cellC (empty ((izqf,cellC)\<mapsto> Addr lnew)
                                                 ((derf,cellC)\<mapsto> Addr lnew))), 
             ih, ([],vs,safeP,sigSafeMain,pc+1,ref)#[])")
apply (unfold exec_all_def )
apply (erule rtrancl_trans)

(* We prove the first step of the SVM *)
prefer 2 
 apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
                      the (cdm (l, i))) = Invoke_static heapC pushRegion []")
 apply (fold exec_all_def)
 apply clarify
 apply (subgoal_tac
 "P' |- 
     (None, sha, h, inih, [([], vs, safeP, sigSafeMain, the (cdm (l, i)), ag,bd)])
   -jvm-> 
     (None, sha ((heapC,kf)\<mapsto> Intg (n+1)), 
                  h(l' \<mapsto> Arr ty m' (regS (nat n + 1 \<mapsto> Addr lnew)))
                    (lnew \<mapsto> Obj cellC (empty ((izqf,cellC)\<mapsto> Addr lnew)
                                              ((derf,cellC)\<mapsto> Addr lnew))), 
                  inih, [([],vs,safeP,sigSafeMain,the (cdm (l,i))+1,ag,bd)]) ∧
       lnew ∉ {la,l',l''} ∧
       lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))")
 prefer 2 apply (rule pushregion_method,simp,assumption+,simp)
 apply simp apply (subgoal_tac "sha (heapC, kf)=Some (Intg n)")
  prefer 2 apply (rule kf_Intg) 
 apply simp 

(* We prove that the executed instruction corresponds with the translation *)  
 apply (unfold trInstr.simps)
 apply (unfold Let_def) 
 apply (erule nth_via_drop_append) 

(* Goto (trAddr pc1 (pc + incCall)) *)
apply (drule drop_Suc_append)
apply (unfold exec_all_def)
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)))) =  Goto (trAddr (the(cdm(p,0))) (the (cdm (l, i)) + incCall))") apply (simp)
apply (simp add: trAddr_def incCall_def) 
apply (rule_tac ys="[]" in nth_via_drop_append)
apply simp
apply (rule conjI)
 apply (subgoal_tac "cdm' (p, 0)=cdm (p, 0)",simp)
 apply (subgoal_tac "(p,0)∈ dom cdm'")
 apply (simp add: map_le_def)
 apply (rule p_in_dom_cdm')
 apply simp
(* Now we prove the equivalence relation *)


apply (rule_tac x="hm" in exI)
apply (rule_tac x="Suc k" in exI)
apply (rule_tac x="k0" in exI)
apply (rule_tac x="(p,0)" in exI)
apply (rule_tac x="S" in exI)

apply (rule_tac x="sh((heapC, kf) \<mapsto> Intg (the_Intg (the (sh (heapC, kf))) + 1))" in exI)
apply (rule_tac x="dh(l' \<mapsto> Arr ty m' (regS(k' + 1 \<mapsto> Addr lnew)), 
                            lnew \<mapsto> Obj cellC [(izqf, cellC) \<mapsto> Addr lnew, 
                            (derf, cellC) \<mapsto> Addr lnew])" in exI)
apply (rule_tac x="ih" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="the (cdm (p, 0))" in exI)
apply (rule_tac x="ref" in exI)

apply (rule_tac x="nat (the_Intg (the ((sh((heapC, kf) \<mapsto> 
                   Intg (the_Intg (the (sh (heapC, kf))) + 1))) (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the ((sh((heapC, kf) \<mapsto> 
                   Intg (the_Intg (the (sh (heapC, kf))) + 1))) (heapC, k0f))))" in exI)

apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="S'" in exI)

apply (rule_tac x="n" in exI)
apply (rule_tac x="l'" in exI)
apply (rule_tac x=" regS(Suc (nat (the_Intg (the (sha (heapC, kf))))) \<mapsto> Addr lnew)" 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 (subgoal_tac
  "la ≠ lnew ∧ l' ≠ lnew ∧ l'' ≠ lnew")
prefer 2 
apply (case_tac "ref",simp)
apply (frule_tac lnew="lnew" 
                 in pushregion_method, assumption+)
apply (clarsimp, rule sym)
apply (erule nth_via_drop)
apply clarsimp

apply (rule conjI, clarsimp)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply (simp add: heapC_def add: stackC_def)
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
                   apply (simp add: heapC_def add: stackC_def)
apply (rule conjI) apply (rule activeCells_3)
                   apply (rule activeCells_4)
                   apply simp apply force
                   apply (assumption+)
apply (rule conjI) apply (rule activeCells_3_1)
                   apply (rule activeCells_4)
                   apply simp
                   apply (rule activeCells_3)
                   apply (rule activeCells_4)
                   apply simp apply force
                   apply (assumption+)
apply (rule conjI) apply simp
apply (rule conjI) apply (simp add: heapC_def add: stackC_def)
apply (rule conjI) apply (simp add: regionsf_def add: kf_def)
apply (rule conjI) apply simp 
apply (rule conjI) apply (simp add: safeDirf_def add: kf_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply simp
apply (rule conjI) apply (subgoal_tac
                    "lnew ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))")
                   apply (elim conjE)
                   apply (rule equivH_CALL) apply assumption+
                   apply simp apply assumption+
                   apply (rule lnew_notin_activeCells)
apply (rule conjI) apply simp  
apply (rule conjI) apply simp 
apply (rule conjI) apply simp
                   apply (simp add: k0f_def add: kf_def)
by simp

end