Theory SafeDepthSemanticsReal

(*  Title:      Resource-Aware Safe Semantics
    Author:     Ricardo Peña and Javier de Dios
    Copyright:  January 2010, Universidad Complutense de Madrid
*)

header {* Depth-Aware Operational semantics of Safe expressions *}

theory SafeDepthSemanticsReal
imports SafeRASemanticsReal "../SafeImp/SVMState"
begin



inductive
  SafeDepthSem :: "[Environment, HeapMap, nat, real, unit Exp, string, HeapMap, nat, 
                    Val, Resources, nat] => bool"   
  ( "_ \<turnstile> _ , _ , _ , _  \<Down> _  _ , _ , _ , _ , _" [71,71,71,71,71,71,71,71,71,71] 70)
where

   litInt :  "E \<turnstile> h, k, td, (ConstE (LitN i) a) \<Down>f h, k, IntT  i, ([]k,0,1), 0" 

|  litBool:  "E \<turnstile> h , k, td,(ConstE (LitB b) a) \<Down>f h, k, BoolT b, ([]k,0,1), 0" 

|  var1   :  "E1 x = Some (Val.Loc p) 
              ==> (E1,E2) \<turnstile> h, k, td, (VarE x a) \<Down>f h, k, Val.Loc p, ([]k,0,1), 0" 

|  var2   :  "[|E1 x = Some (Val.Loc p); E2 r = Some j;  j <= k;
               copy (h,k) p j = ((h',k),p'); def_copy p (h,k);
               m = real (size h p)|]  
           ==> (E1,E2) \<turnstile> h, k , td, (x @ r a)\<Down>f h', k, Val.Loc p', ([j \<mapsto> m],m,2), 0"

| var3   : "[|E1 x = Some (Val.Loc p); h p = Some c; SafeHeap.fresh q h|]  
        ==> (E1,E2) \<turnstile> h,k, td, (ReuseE x a)\<Down>f 
                      ((h(p:=None))(q \<mapsto> c)),k,Val.Loc q,([]k,0,1),0"

| let1   : "[| ∀ C as r a'. e1 ≠ ConstrE C as r a'; x1 ∉ dom E1; 
            (E1,E2) \<turnstile> h, k, 0, e1 \<Down>f h', k, v1, (δ1,m1,s1), n1 ∧
            (E1(x1 \<mapsto> v1),E2) \<turnstile> h', k, (td+1), e2 \<Down>f h'', k, v2, (δ2,m2,s2), n2|]  
        ==> (E1,E2) \<turnstile> h, k, td, Let x1 = e1 In e2 a \<Down>f h'', k, v2, (δ1⊕δ2,max m1 (m2 + \<parallel>δ1\<parallel>),max (s1+2) (s2+1)), max n1 n2"

| let2   : "[| E2 r = Some j; j ≤ k; fresh p h; x1 ∉ dom E1; r ≠ self;
            (E1(x1 \<mapsto> Val.Loc p),E2) \<turnstile>
            h(p \<mapsto> (j,(C,map (atom2val E1) as))), k, (td+1), e2 \<Down>f h', k, v2, (δ,m,s), n|]  
        ==> (E1,E2) \<turnstile> h,k,td, Let x1 = ConstrE C as r a' In e2 a \<Down>f h',k,v2,(δ⊕(empty(j\<mapsto>1)),m+1,s+1),n"

| case1: "[|   i < length alts;
              E1 x  = Some (Val.Loc p);
              h p  = Some (j,C,vs); 
              alts!i = (pati, ei);
              pati = ConstrP C ps ms;
              xs = (snd (extractP (fst (alts ! i))));
              E1' = extend E1 xs vs; 
              def_extend E1 xs vs;
              nr = real (length vs);
              (E1',E2) \<turnstile> h, k, (td + nr), ei \<Down>f h', k, v, (δ,m,s), n|]  
          ==> (E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down>f h', k, v, (δ,m, (s+nr)),n"

|  case1_1: "[|  i < length alts;
                E1 x  = Some (IntT n);
                alts!i = (pati, ei);
                pati = ConstP (LitN n);
                (E1,E2) \<turnstile> h, k, td, ei \<Down>f h', k, v, (δ,m,s), nf|]  
            ==> (E1,E2) \<turnstile> h, k, td, Case (VarE x a) Of alts a' \<Down>f h', k, v, (δ,m,s),nf"

|  case1_2: "[|  i < length alts;
                E1 x  = Some (BoolT b);
                alts!i = (pati, ei);
                pati = ConstP (LitB b);
                (E1,E2) \<turnstile> h, k, td, ei \<Down> f h', k, v,(δ,m,s),n|]  
            ==> (E1,E2) \<turnstile> h, k, td, Case (VarE x a) Of alts a' \<Down>f h', k, v, (δ,m,s), n"

| case2: "[|     i < length alts;
                E1 x  = Some (Val.Loc p);
                h p  = Some (j,C,vs);
                alts!i = (pati, ei);
                pati = ConstrP C ps ms;
                xs = (snd (extractP (fst (alts ! i))));
                E1' = extend E1 xs vs;
                def_extend E1 xs vs;
                nr = real (length vs);
                j <= k;
                (E1',E2) \<turnstile> h(p :=None), k,(td + nr), ei \<Down>f h', k, v, (δ,m,s), n|]  
            ==> (E1,E2) \<turnstile> h, k, td, CaseD (VarE x a) Of alts a' \<Down>f h', k, v, (δ⊕(empty(j\<mapsto>-1)),max 0 (m - 1),s+nr), n"

|   app_primops: "[| primops g = Some oper;
                    v1 = atom2val E1 a1;
                    v2 = atom2val E1 a2;
                    v = execOp oper v1 v2|] 
               ==> (E1,E2) \<turnstile> h, k, td, AppE g [a1,a2] [] a \<Down>f h, k, v, ([]k,0,2), 1"

|  app: "[| Σd f = Some (xs,rs,e); primops f = None;
           distinct xs; distinct rs;  dom E1 ∩ set xs = {};
           length xs = length as; length rs = length rr;
           E1' = map_of (zip xs (map (atom2val E1) as));
           n = real (length xs); 
           l = real (length rs); 
           E2' = (map_of (zip rs  (map (theoE2) rr))) (self \<mapsto> Suc k);
           (E1',E2') \<turnstile> h, (Suc k), (n+l), e \<Down>f h', (Suc k), v, (δ,m,s), nf;
            h'' =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}|] 
       ==> (E1,E2) \<turnstile> h, k, td, (AppE f as rr a) \<Down>f h'', k, v, (δ(k+1:=None),m,max (n +l) (s+n+l-td)), (nf+1)"

|   app2: "[| Σd g = Some (xs,rs,e); primops g = None; f ≠ g;
            distinct xs; distinct rs;  dom E1 ∩ set xs = {};
            length xs = length as; length rs = length rr;
            E1' = map_of (zip xs (map (atom2val E1) as)); 
            n = real (length xs); 
            l = real (length rs);
            E2' = (map_of (zip rs  (map (theoE2) rr))) (self \<mapsto> Suc k);
            (E1',E2') \<turnstile> h, (Suc k), (n+l), e \<Down>f h', (Suc k), v, (δ,m,s), nf;
             h'' =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}|] 
        ==> (E1,E2) \<turnstile>  h, k, td, AppE g as rr a \<Down>f h'', k, v, (δ(k+1:=None),m,max (n +l) (s+n+l-td)), nf"



lemma eqSemRADepth[rule_format]: "(E1,E2) \<turnstile>  h,k,td,e\<Down>h',k,v,r --> 
                                  (∃ n. (E1,E2) \<turnstile>  h,k,td,e\<Down>f h',k,v,r,n)"
apply (rule impI)
apply (erule SafeRASem.induct)

(* LitN *)
apply (rule_tac x=0 in exI)
apply (rule SafeDepthSem.litInt)

(* LitB *)
apply (rule_tac x=0 in exI)
apply (rule SafeDepthSem.litBool)

(* Var *)
apply (rule_tac x=0 in exI)
apply (rule SafeDepthSem.var1,assumption)

(* Copy *)
apply (rule_tac x=0 in exI)
apply (rule SafeDepthSem.var2,simp,simp,assumption,assumption,assumption,assumption)

(* Reuse *)
apply (rule_tac x=0 in exI)
apply (rule SafeDepthSem.var3,assumption+)

(* Let1 *)
apply (erule exE)+
apply (rename_tac n1 n2)
apply (rule_tac x="max n1 n2" in exI)
apply (rule SafeDepthSem.let1)
apply (assumption+)
apply (rule conjI,simp,simp)

(* Let2 *)
apply (erule exE)+
apply (rename_tac n2)
apply (rule_tac x=n2 in exI)
apply (rule SafeDepthSem.let2)
apply (assumption+)

(* Case1 *)
apply (elim exE)
apply (rename_tac ni)
apply (rule_tac x=ni in exI)
apply (rule SafeDepthSem.case1)
apply (assumption+)

(* Case1_1 *)
apply (elim exE)
apply (rename_tac ni)
apply (rule_tac x=ni in exI)
apply (rule SafeDepthSem.case1_1)
apply (assumption+)

(* Case1_2 *)
apply (elim exE)
apply (rename_tac ni)
apply (rule_tac x=ni in exI)
apply (rule SafeDepthSem.case1_2)
apply (assumption+)

(* Case2 *)
apply (elim exE)
apply (rename_tac ni)
apply (rule_tac x=ni in exI)
apply (rule SafeDepthSem.case2)
apply (assumption+)

(* App_primops *)
apply (rule_tac x=1 in exI)
apply (rule SafeDepthSem.app_primops)
apply assumption+

(* App *)
apply (elim exE)
apply (rename_tac nf)
apply (case_tac "fa=f")

(* case in which f is calling itself *)
apply (rule_tac x="nf+1" in exI)
apply (rule_tac s=f and t=fa in subst)
apply simp
apply (rule_tac s="h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}" and t=h'' in subst)
apply simp
apply clarify
apply (rule_tac h'=h' in SafeDepthSem.app)
apply assumption+
apply simp
apply simp
apply simp
apply simp
apply assumption
apply simp

(* case in which f is calling a different function *)
apply (rule_tac x=nf in exI)
apply (rule_tac s="h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}" and t=h'' in subst)
apply simp
apply (rule SafeDepthSem.app2)
apply assumption+
apply simp
apply assumption+
apply simp
done


lemma eqSemDepthRA[rule_format]: "(E1,E2) \<turnstile>  h,k,td,e\<Down>f h',k,v,r,n -->
                                   (E1,E2) \<turnstile> h,k,td,e\<Down>h',k,v,r"

apply (rule impI)
apply (erule SafeDepthSem.induct)

(* Lit Int *)
apply (rule SafeRASem.litInt)

(* Lit Bool *)
apply (rule SafeRASem.litBool)

(* Var *)
apply (rule SafeRASem.var1,assumption)

(* Copy *)
apply (rule SafeRASem.var2,assumption+)

(* Reuse *)
apply (rule SafeRASem.var3,assumption+)

(* Let 1 *)
apply (elim conjE)
apply (rule SafeRASem.let1,assumption+)

(* Let 2 *)
apply (rule SafeRASem.let2,assumption+)

(* Case 1 *)
apply (rule SafeRASem.case1,assumption+)

(* Case 1.1 *)
apply (rule SafeRASem.case1_1,assumption+)

(* Case 1.2 *)
apply (rule SafeRASem.case1_2,assumption+)

(* Case 2 *)
apply (rule SafeRASem.case2,assumption+)

(* App primops *)
apply (rule SafeRASem.app_primops,assumption+)

(* App *)
apply (rule SafeRASem.app,assumption+)

(* App 2 *)
apply (rule SafeRASem.app,assumption+)
done



constdefs
  SafeBoundSem :: "[Environment, HeapMap, nat, real, unit Exp, string × nat,
                    HeapMap, nat, Val, Resources] => bool"   
   ("_ \<turnstile> _ , _ , _ , _ \<Down> _  _ , _ , _ , _ " [71,71,71,71,71,71,71,71,71] 70)

    "E \<turnstile> h, k, td, e \<Down>tup h', k', v, r  ≡ 
     (let (f,n) = tup in k=k' ∧ (∃ nf . E \<turnstile> h, k, td, e \<Down>f h', k, v, r, nf 
                              ∧ nf ≤ n))"

lemma eqSemRABound [rule_format]: 
  "(E1,E2) \<turnstile> h,k,td,e\<Down>h',k,v,r ≡   
   (∃ n.(E1,E2) \<turnstile> h,k,td,e\<Down>(f,n) h',k,v,r)"

apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (simp add: SafeBoundSem_def)
 apply (drule_tac ?f=f in eqSemRADepth)
 apply (elim exE)
 apply (rule_tac x=x in exI)
 apply (rule_tac x=x in exI)
 apply (rule conjI,assumption,simp)
(* backwards implication *)
 apply (simp add: SafeBoundSem_def del:Product_Type.split_paired_Ex)
 apply (elim exE)
 apply (elim conjE)
 apply (drule eqSemDepthRA)
 by assumption



lemma eqSemBoundRA [rule_format]: 
  "∃ n. (E1,E2) \<turnstile> h,k,td,e\<Down>(f,n) h',k,v,r ≡ 
   (E1,E2) \<turnstile> h,k,td,e\<Down>h',k,v,r"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (simp add: SafeBoundSem_def del:Product_Type.split_paired_Ex)
 apply (elim exE)
 apply (elim conjE)
 apply (drule eqSemDepthRA)
 apply assumption
(* backwards implication *)
 apply (simp add: SafeBoundSem_def)
 apply (drule_tac ?f=f in eqSemRADepth)
 apply (elim exE)
 apply (rule_tac x=x in exI)
 apply (rule_tac x=x in exI)
 apply (rule conjI,assumption,simp)
done

lemma impSemBoundRA [rule_format]: 
  "(E1,E2) \<turnstile> h,k,td,e\<Down>(f,n) h',k,v,r ==> 
   (E1,E2) \<turnstile> h,k,td,e\<Down>h',k,v,r"
apply (simp add: SafeBoundSem_def del:Product_Type.split_paired_Ex)
apply (elim exE,elim conjE)
apply (drule eqSemDepthRA)
by assumption



end