Theory mainTheoremSVM2JVM

(* 
   Title: Main correctness theorem of the translation SVM to JVM
   Author: Ricardo Pe~na and Javier de Dios
   Copyright: March 2009, Universidad Complutense de Madrid
*)


header {* Main correctness theorem of the translation SVM to JVM *}

theory mainTheoremSVM2JVM
imports CertifSVM2JVM dem_translation dem_PUSHCONT dem_POPCONT dem_PRIMOP
                      dem_SLIDE dem_MATCHN dem_BUILDENV dem_CALL dem_DECREGION
                      dem_BUILDCLS dem_REUSE dem_MATCH
begin


text{* This theorem certifies that, whenever the SVM and the JVM are 
started in equivalent states, the SVM executes its next instruction, 
and the JVM executes its translation to bytecode, then both machines 
arive at equivalent states. *}

theorem correctSVM2JVM :
         "[| (P',cdm,ctm,com) = trSVM2JVM P; 
            cdm, ctm, com  \<turnstile> S1 \<triangleq> S1';                              
            execSVM P S1 = Either.Right S2 
          |] ==> 
          ∃ S2' . P' \<turnstile>  S1' -jvm-> S2' ∧ cdm, ctm, com \<turnstile> S2 \<triangleq> S2'"

(* First we unfold some definitions and tuples *)
apply (case_tac P)
apply (rename_tac cs triple)
apply (case_tac cs)
apply (rename_tac svms ctmap)
apply (case_tac triple)
apply (rename_tac ini pair)
apply (case_tac pair)
apply (rename_tac ct st)
apply (unfold execSVM_def)
apply (case_tac S1)
apply (rename_tac h rest1)
apply (case_tac rest1)
apply (rename_tac k0 rest2)
apply (case_tac rest2)
apply (rename_tac pc S)
apply (case_tac pc)
apply (rename_tac l i)
apply (case_tac h)
apply (rename_tac hm k)
apply (clarsimp)

(* We search the SVM instruction executed and its translation *)
apply (subgoal_tac " l : dom (map_of svms)
      ∧ i < length (fst (the (map_of svms l)))")
 prefer 2 apply (erule PC_good,simp)
apply (elim conjE)
apply (subgoal_tac "∃ j . 
      j < length svms ∧ (l,the (map_of svms l)) = svms ! j")
 prefer 2 apply (rule map_of_distinct2)  apply force
apply (erule exE,elim conjE)
apply (case_tac "the (map_of svms l)",rename_tac seq fn,clarify)
apply (subgoal_tac "(∃ cdm' ctm' pcc inss bytecode' .
      inss = trInstr (the (cdm (l,i))) cdm' ctm' com pcc 
             (fst (the (map_of svms l)) ! i) 
      ∧ drop (the (cdm (l,i))) (extractBytecode P') = inss @ bytecode' 
      ∧ cdm' ⊆m cdm)")
 prefer 2 apply (rule fun_SVM2JVM)
 apply simp 
 apply simp 
 apply (rule sym,simp)
 apply simp 
 apply simp 
 apply simp 
 apply simp 

(* we return to the main goal *)
apply (elim exE, elim conjE)
apply (simp,elim conjE, clarify)

(* We make case distinction on the executed svm instruction *)
apply (case_tac "fst (the (map_of svms l)) ! i")

(* proof for DECREGION *)
apply (erule execSVMInstr_DECREGION)
apply (simp,simp,simp,force)

(* proof for POPCONT *) 
apply (erule execSVMInstr_POPCONT)
apply (simp,simp,simp,force)

(* proof for PUSHCONT *)
apply (erule execSVMInstr_PUSHCONT)
apply (simp,simp,simp,force)

(* proof for COPY *)
apply (erule execSVMInstr_COPY)
apply (simp,simp,simp,force)

(* proof for REUSE *)
apply (erule execSVMInstr_REUSE)
apply (simp,simp,simp,force)

(* proof for CALL *)
apply (erule execSVMInstr_CALL)
apply (simp,simp,simp,force,simp)

(* proof for PRIMOP *)
apply (erule execSVMInstr_PRIMOP)
apply (simp,simp,simp,force)

(* proof for MATCH *)
apply (erule execSVMInstr_MATCH)
apply (simp,force,simp,force,simp)

(* proof for MATCHD *)
apply (erule execSVMInstr_MATCHD)
apply (simp,force,simp,force)

(* proof for MATCHN *)
apply (erule execSVMInstr_MATCHN)
apply (simp,force,simp,force,simp)

(* proof for BUILDENV *)
apply (erule execSVMInstr_BUILDENV)
apply (simp,simp,simp,force)

(* proof for BUILDCLS *)
apply (erule execSVMInstr_BUILDCLS)
apply (simp,force,simp,force)

(* proof for SLIDE *)
apply (frule_tac m="nat1" and 
                 n="nat2" in execSVMInstr_SLIDE) 
apply (simp+)
done

end