Theory CertifSVM2JVM

(* Title: Certification of the translation from Safe Virtual Machine to JVM
   Author: Javier de Dios and Ricardo Pe~na
   Copyright: January 2009, Universidad Complutense de Madrid
*)


header {* Certification of the translation from SVM to JVM *}

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

subsection{* Equivalence relations between SVM and JVM states *}

types injection = "Location \<rightharpoonup> loc"

-- "Equivalence of values under a cell directory and an injection"

fun equivV :: "Val => val => entries_ => injection => bool"
where
  "equivV (IntT i)  v d g   = (∃ j. v = Intg j ∧ (i = j))"
| "equivV (BoolT b) v d g   = (∃ i. v = Intg i ∧ 
                              ((i ≠ 0 ∧ b) ∨ (i = 0  ∧ ¬ b)))" 
| "equivV (Val.Loc l) v d g = (∃ i l'. v = Intg i 
                              ∧ d (nat i) = Some (Addr l') ∧ g l = Some l')"

-- "Cell to the right of a given one in JVM heap"
constdefs
 nextCell :: "aheap=> loc=> loc"
 "nextCell h l == (case h l of
                    Some (Obj cls flds) =>
                      case flds (derf,cellC) of
                        Some (Addr next) => next)"

-- "Cells belonging to a region in the JVM heap, starting from a given one"
inductive_set
  cellsReg :: "aheap => loc => loc set"
  for h :: aheap and l:: loc
where
  cellReg_basic: "l ∈ cellsReg h l"
| cellReg_step:  " [| l ∈ cellsReg h l; l' = nextCell h l|] 
                   ==> l' ∈ cellsReg h l"

-- "this gives us the set of references belonging to a given region"
constdefs
 region :: "entries_ => aheap => nat => loc set"
 "region rs h j == (
          let header   = the_Addr (the (rs j));
              allcells = cellsReg h header
          in  allcells - {header})"

-- "this gives us the set of references belonging to all regions"
constdefs
 activeCells :: "entries_ => aheap => nat => loc set"
 "activeCells rs h k ≡ {p . ∃ j . j ≤ k ∧ p ∈ region rs h j}"

constdefs
 passiveCells :: "entries_ => nat => loc set"
 "passiveCells rs k ≡ {p. ∃  j. j  ≤ k ∧  p = the_Addr (the (rs j))}"

-- "This gives us the i-th argument of a cell"
constdefs
 argCell :: "fields_ => nat => val"
 "argCell fds i == (
       let arg_i = if i=1 then arg1 else 
                    if i=2 then arg2 else
                     if i=3 then arg3 else
                      if i=4 then arg4 else
                       if i=5 then arg5 else
                        if i=6 then arg6 else
                         if i=7 then arg7 else arg8
       in the (fds (arg_i,cellC)))"

text{* A SVM cell is equivalent to a JVM cell if the JVM object is an
instance of the class Cell, if they live in the same region j, the
constructor name and the global tag are made equivalent by the constructor
map cm, and all the arguments are equivalent.*}

-- "Equivalence of cells under a constructor map, a region stack, a cell directory"
-- "and an injection"

fun
 equivC :: "[Region × Cell,aheap,loc,heap_entry,nat,consMap,entries_,entries_,
            injection] => bool" 
where
  "equivC cell h ref cell' k cm regStack d g = (
      ∃ j C vs Obj cname flds tag n reg_j tag'. 
        cell = (j,C,vs) ∧
        j ≤ k ∧
        cell' = Obj cname flds ∧
        cm C = Some tag ∧
        n = length vs ∧
        reg_j = region regStack h j ∧
        tag' = nat (the_Intg (the (flds (tagGf,cname)))) ∧
        cname = cellC ∧
        ref ∈ reg_j ∧
        tag = tag' ∧
        (∀ i∈ {k . 0≤k & k < n}. equivV (vs!i) (argCell flds i) d g))"


-- "Equivalence between SVM and JVM heaps under a constructor map,"
-- "a region stack, a cell directory and an injection"

fun
 equivH :: "[Heap,aheap,nat,consMap,entries_,entries_,injection] => bool"
where
 "equivH (H,k1) h k2 cm regStack d g = (
        k1=k2 ∧
        ran g = activeCells regStack h k2 ∧
        finite (dom H) ∧
       (∀ l∈ dom H . ∃ l'. l' = the (g l) 
              ∧ equivC (the (H l)) h l' (the (h l')) k2 cm regStack d g))"


-- "Equivalence between SVM and JVM stacks under a continuation map, a cell"
-- "directory and an injection"
fun
 equivS :: "[Stack,entries_,int,contMap,entries_,injection] => bool"
where
  "equivS []     S' n ctm d g         = (n = (-1))"
| "equivS (Cont (k,p)#S) S' n ctm d g = (n >= 1 
            ∧ k = nat (the_Intg (the (S' (nat n )))) 
            ∧ the (ctm p) = nat (the_Intg (the (S' ((nat n - 1))))) 
            ∧ equivS S S' (n - 2) ctm d g)"
| "equivS (Reg j#S) S' n ctm d g      = (n >= 0 
            ∧ j = nat (the_Intg (the (S' (nat n)))) 
            ∧ equivS S S' (n - 1) ctm d g)"
| "equivS (Val v#S) S' n ctm d g      = (n >= 0 
            ∧ equivV v (the (S' (nat n))) d g 
            ∧ equivS S S' (n - 1) ctm d g)"

-- "Equivalence between SVM and JVM states"
constdefs
 equivState :: "[codeMap,contMap,consMap,SVMState,jvm_state] => bool"
                     ("_ , _, _ \<turnstile> _ \<triangleq> _" [71,71,71,71,71] 70)
 "equivState cdm ctm com st1 st2 == (
  ∃ H k k0 PC S sh h inih vs pc ref k' k0' l ty m S' n l' regS l'' 
   m' m'' d g .
         st1 = ((H,k),k0,PC,S) ∧
         st2 = (None,sh,h,inih,([],vs,safeP,sigSafeMain,pc,ref)#[]) ∧ 
         k'  = nat (the_Intg (the (sh (heapC,kf)))) ∧
         k0' = nat (the_Intg (the (sh (heapC,k0f)))) ∧
         sh (stackC,Sf) = Some (Addr l) ∧ 
         distinct [l,l',l''] ∧
         activeCells regS h k' ∩ {l,l',l''} = {} ∧
         h l = Some (Arr ty m S') ∧
         sh (stackC,topf) = Some (Intg n) ∧ 
         sh (heapC,regionsf) = Some (Addr l') ∧ 
         h l' = Some (Arr ty m' regS) ∧ 
         sh (dirCellC,safeDirf) = Some (Addr l'') ∧  
         h l'' = Some (Arr ty m'' d) ∧ 
         dom g = dom H ∧
         inj_on g (dom H) ∧
         equivH (H,k) h k' com regS d g ∧
         n < int m ∧
         equivS S S' n ctm d g ∧ 
         k0 = k0' ∧
         pc = the (cdm PC))"

axioms PC_good:
 "[| (P',cdm,ctm,com) = trSVM2JVM ((svms, ctmap), ini, ct, st);
   equivState cdm ctm com ((H,k),k0,(l,i),S) st2 
  |] ==>  l : dom (map_of svms)
            ∧ i < length (fst (the (map_of svms l)))"

axioms RightNotUndefined : "∀ x . ¬ (undefined = Right x)"

axioms execSVMInstr_COPY :
  "[| (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) = COPY;
   execSVMInst COPY (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 COPY @ 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')"


axioms execSVMInstr_MATCHD :
  "[| (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) = MATCHD off ps;
   execSVMInst (MATCHD 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 (MATCHD off ps) @ 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')"


(** Auxiliary lemmas **)

axioms equivS_ge_n:
  "equivS S S' n ctm d g ==> 
      (∀  p > 0. equivS S (S'(nat (p + n)  \<mapsto> A)) n ctm d g)"

axioms equivS_length:
  "equivS S S' n ctm d g ==> n = int (length S) - 1"

axioms length_vs:
 "length vs = 10"

lemma l_not_in_cellReg:
 "[| l ∉ activeCells regS h k; l ∉ passiveCells regS k |] 
  ==> ∀ j ≤ k. l ∉ cellsReg h (the_Addr (the (regS j)))"
apply (simp add: activeCells_def)
apply (simp add: passiveCells_def)
apply (simp add: region_def)
done

axioms safeDir_bounds:
 "the_Intg (the (S' i)) < int m ∧ 0 ≤ the_Intg (the (S' i))"

axioms l_not_in_cellReg:
 "l ∉ activeCells regS h k
  ==> ∀ j . l ∉ cellsReg h (the_Addr (the (regS j)))"

axioms activeCells:
  "l ∉ activeCells regS h k
   ==> l ∉ activeCells regS (h(l \<mapsto> A)) k"


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

axioms method_safeMain:
  "(P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc)
   ==> (safeP,PrimT Void,10,10,(instrConsTable @ instrSizeTable @ instrs,[])) =  
       (the (method' (P', safeP) (safeMain, [])))"


(* Lemmas for activeCells *)

declare equivH.simps [simp del]

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

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

lemma l_not_in_regs:
 "l ∉ cellsReg h (the_Addr (the (regS j)))
  ==> the_Addr (the (regS j)) ≠ l"
apply (subgoal_tac "the_Addr (the (regS j)) ∈  cellsReg h (the_Addr (the (regS j)))") 
apply blast
by (rule cellReg_basic)


end