Theory dem_DECREGION

(* 
   Title: Lemmas for the translation SVM to JVM. DECREGION
   Author:Javier de Dios and Ricardo Pe~na 
   Copyright: January 2009, Universidad Complutense de Madrid
*)

theory dem_DECREGION
imports "../JVMSAFE/JVMExec" SVM2JVM SVMSemantics CertifSVM2JVM 
                             dem_translation
begin

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

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

axioms decregion_method:
 "[| s = (None, shp, hp, ihp,([],vs,safeP, sigSafeMain,pc,z)#[]);
  shp (heapC,kf) = Some (Intg k);
  shp (heapC,k0f) = Some (Intg k0);
  shp (heapC,regionsf) = Some (Addr l);
  hp l = Some  (Arr ty m regS);
  Invoke_static heapC decregion [] = fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc
  |] ==> 
  P' |- s -jvm-> (None, shp ((heapC,kf)\<mapsto> Intg k0), 
                             hp(l \<mapsto> Arr ty ma regS'), 
                             ihp, ([],loc,safeP,sigSafeMain,pc+1,z)#[])
  ∧ (∀ j ≤ nat k0 . region regS' hp j = region regS hp j)"

axioms kf_Some_i:
  "sha (heapC, kf) = Some (Intg jj)"

axioms k0f_Some_i:
  "sha (heapC, k0f) = Some (Intg ii)"

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_5:
  "la ∉ activeCells regS h k
   ==> la ∉ activeCells regS' h' k'"

axioms equivS_DECREGION:
  "equivS S S' n ctm d g
   ==> equivS S S' n ctm d (g |` {l ∈ dom hm. fst (the (hm l)) ≤ nat (the_Intg (the (sha (heapC, k0f))))})"

axioms inj_on_DECREGION:
  "[| ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa); inj_on g (dom H) |]
   ==> inj_on (g |` {l ∈ dom hm. fst (the (hm l)) ≤ nat (the_Intg (the (sha (heapC, k0f))))})
           (dom (hm |` {p ∈ dom hm. fst (the (hm p)) ≤ k0}))"

axioms equivH_DECREGION:
 "[| ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa); equivH (H, ka) h k' com regS d g |] 
  ==>  equivH (hm |` {p ∈ dom hm. fst (the (hm p)) ≤ k0}, k0) (dh(l' \<mapsto> Arr ty ma regS'))
           (nat (the_Intg (the ((sh((heapC, kf) \<mapsto> the (sh (heapC, k0f)))) (heapC, kf))))) com regS' d
           (g |` {l ∈ dom hm. fst (the (hm l)) ≤ nat (the_Intg (the (sha (heapC, k0f))))})"


lemma execSVMInstr_DECREGION :
    "[| (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) = DECREGION;
        execSVMInst DECREGION (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 DECREGION @ bytecode'
      |] ==>   ∃ v' sh' dh' ih' fms' . 
      P' \<turnstile>  S1' -jvm-> (v',sh',dh',ih', fms') ∧
     cdm , ctm, com  \<turnstile>  S2  \<triangleq> (v',sh',dh',ih', fms')"

(* First, we make the tuples explicit *)
apply (case_tac S1')
apply (rename_tac v tup)
apply (case_tac tup)
apply (rename_tac sh tup)
apply (case_tac tup)
apply (rename_tac dh tup)
apply (case_tac tup)
apply (rename_tac ih fms)
apply (simp)

apply (unfold equivState_def)
apply (elim exE,elim conjE)



(* we go on with the main goal. We instantiate the arrival JVM state*)


apply (rule_tac x="None" in exI)
apply (rule_tac x="sh((heapC,kf)\<mapsto> the (sh (heapC, k0f)))" in exI)
apply (rule_tac x="dh(l' \<mapsto> Arr ty ma regS')" in exI)
apply (rule_tac x="ih" in exI)
apply (rule_tac x="[([], vs, safeP, sigSafeMain, pc+1, ref)]" in exI)

apply (rule conjI)

apply (subgoal_tac "sha (heapC, k0f) = Some (Intg ii)")
apply (subgoal_tac "sha (heapC, kf) = Some (Intg jj)")
(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "P' |- (v, sh, dh, ih,fms) -jvm-> 
      (None, sh ((heapC,kf)\<mapsto> Intg (the_Intg (the (sha (heapC, k0f))))), 
       dh (l' \<mapsto> Arr ty ma regS'), 
       ih, ([],vs,safeP,sigSafeMain,pc+1,ref)#[])
  ∧ (∀ j ≤ nat (the_Intg (the (sha (heapC, k0f)))) . region regS' dh j = region regS dh j)")
apply (elim conjE)  apply(simp) 

apply (rule decregion_method)
 apply (simp,simp,simp,simp,simp)

(* We prove that the executed instruction corresponds with the translation *)  
apply (unfold extractBytecode_def)
apply (unfold trInstr.simps)
apply clarify
apply (rule sym)
apply (rule_tac ys="[]" in nth_via_drop_append)
apply simp
apply (rule kf_Some_i)
apply (rule k0f_Some_i)

(* Now we prove the equivalence relation *)
apply (frule nonJumping_Suc_pc)
apply (erule_tac sym [where t="DECREGION"])
apply (simp add: nonJumping.simps)
apply (simp add: trInstr.simps)

apply (rule_tac x="hm |` {p ∈ dom hm. fst (the (hm p)) ≤ k0}" in exI)
apply (rule_tac x="k0" in exI)
apply (rule_tac x="k0" in exI)
apply (rule_tac x="(l,Suc i)" in exI)
apply (rule_tac x="S" in exI)

apply (rule_tac x="sh((heapC, kf) \<mapsto> the (sh (heapC, k0f)))" in exI)
apply (rule_tac x="dh(l' \<mapsto> Arr ty ma regS')" in exI)
apply (rule_tac x="ih" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="pc + 1" in exI)
apply (rule_tac x="ref" in exI)

apply (rule_tac x="nat (the_Intg (the ((sh((heapC, kf) \<mapsto> the (sh (heapC, k0f)))) (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the ((sh((heapC, kf) \<mapsto> the (sh (heapC, k0f)))) (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'" in exI)
apply (rule_tac x="l''" in exI)
apply (rule_tac x="ma" in exI)
apply (rule_tac x="m''" in exI)
apply (rule_tac x="d" in exI)
apply (rule_tac x="g |` {l ∈ dom hm. fst (the (hm l)) ≤ nat (the_Intg (the (sha (heapC, k0f))))}" in exI)

apply (rule conjI, clarsimp)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply (simp add: stackC_def add: heapC_def)
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (rule activeCells_5,assumption)
apply (rule conjI) apply (rule activeCells_5,assumption)
                   apply (rule activeCells_5,assumption)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (simp add: stackC_def add: heapC_def)
apply (rule conjI) apply (simp add: regionsf_def add: kf_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (simp add: dirCellC_def add: heapC_def) 
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply (simp add: inj_on_def) 
apply (rule conjI) apply (rule equivH_DECREGION, assumption+) 
apply (rule conjI) apply simp 
apply (rule conjI) apply (clarsimp, rule equivS_DECREGION,assumption) 
apply (rule conjI) apply clarsimp
by simp 



end