Theory SafeDepthSemantics

(*  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 SafeDepthSemantics
imports SafeRASemantics "../SafeImp/SVMState"
begin



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

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

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

|  var1   :  "E1 x = Some (Val.Loc p) 
              ==> (E1,E2) \<turnstile> h, k,  (VarE x a) \<Down>f h, k, Val.Loc p, 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)|]  
           ==> (E1,E2) \<turnstile> h, k ,  (x @ r a)\<Down>f h', k, Val.Loc p', 0"

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

| let1   : "[| ∀ C as r a'. e1 ≠ ConstrE C as r a'; x1 ∉ dom E1; 
            (E1,E2) \<turnstile> h, k, e1 \<Down>f h', k, v1, n1 ∧
            (E1(x1 \<mapsto> v1),E2) \<turnstile> h', k, e2 \<Down>f h'', k, v2, n2|]  
        ==> (E1,E2) \<turnstile> h, k, Let x1 = e1 In e2 a \<Down>f h'', k, v2, 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, e2 \<Down>f h', k, v2, n|]  
        ==> (E1,E2) \<turnstile> h,k,Let x1 = ConstrE C as r a' In e2 a \<Down>f h',k,v2,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 = int (length vs);
              (E1',E2) \<turnstile> h, k, ei \<Down>f h', k, v, n|]  
          ==> (E1,E2) \<turnstile> h,k, Case (VarE x a) Of alts a' \<Down>f h', k, v, n"

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

|  case1_2: "[|  i < length alts;
                E1 x  = Some (BoolT b);
                alts!i = (pati, ei);
                pati = ConstP (LitB b);
                (E1,E2) \<turnstile> h, k, ei \<Down> f h', k, v, n|]  
            ==> (E1,E2) \<turnstile> h, k, Case (VarE x a) Of alts a' \<Down>f h', k, v, 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 = int (length vs);
                j <= k;
                (E1',E2) \<turnstile> h(p :=None), k, ei \<Down>f h', k, v, n|]  
            ==> (E1,E2) \<turnstile> h, k, CaseD (VarE x a) Of alts a' \<Down>f h', k, v, 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, AppE g [a1,a2] [] a \<Down>f h, k, v, 1"

|  app: "[| Σf 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 = length xs; 
           l = length rs; 
           E2' = (map_of (zip rs  (map (theoE2) rr))) (self \<mapsto> Suc k);
           (E1',E2') \<turnstile> h, (Suc k), e \<Down>f h', (Suc k), v, nf;
            h'' =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}|] 
       ==> (E1,E2) \<turnstile> h, k, (AppE f as rr a) \<Down>f h'', k, v, (nf+1)"

|   app2: "[| Σf 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 = length xs; 
            l = length rs;
            E2' = (map_of (zip rs  (map (theoE2) rr))) (self \<mapsto> Suc k);
            (E1',E2') \<turnstile> h, (Suc k), e \<Down>f h', (Suc k), v, nf;
             h'' =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}|] 
        ==> (E1,E2) \<turnstile>  h, k, AppE g as rr a \<Down>f h'', k, v, nf"



lemma eqSemRADepth[rule_format]: "(E1,E2) \<turnstile>  h,k,td,e\<Down>h',k,v,r --> 
                                  (∃ n. (E1,E2) \<turnstile>  h,k,e\<Down>f h',k,v,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)

(* 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,e\<Down>f h',k,v,n -->
                                   (∀ td.∃ r.(E1,E2) \<turnstile> h,k,td,e\<Down>h',k,v,r)"

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

(* Lit Int *)
apply (rule allI)
apply (rule_tac x="([]k,0,1)" in exI)
apply (rule SafeRASem.litInt)

(* Lit Bool *)
apply (rule allI)
apply (rule_tac x="([]k,0,1)" in exI)
apply (rule SafeRASem.litBool)

(* Var *)
apply (rule allI)
apply (rule_tac x="([]k,0,1)" in exI)
apply (rule SafeRASem.var1,assumption)

(* Copy *)
apply (rule allI)
apply (rule_tac x="([j \<mapsto> size h p],size h p,2)" in exI)
apply (rule SafeRASem.var2,assumption+,simp)

(* Reuse *)
apply (rule allI)
apply (rule_tac x="([]k,0,1)" in exI)
apply (rule SafeRASem.var3) apply assumption+

(* Let 1 *)
apply (rule allI)
apply (elim conjE)
apply (erule_tac x=0 in allE)
apply (erule_tac x="td+1" in allE)
apply (elim exE)
apply (rename_tac r1 r2)
apply (case_tac r1)
apply (case_tac r2)
apply (rename_tac δ1 rest1 δ2 rest2)
apply (case_tac rest1)
apply (case_tac rest2)
apply (rename_tac m1 ss1 m2 ss2)
apply (rule_tac x="(δ1⊕δ2,max m1 (m2 + \<parallel>δ1\<parallel>),max (ss1+2) (ss2+1))" in exI)
apply (rule SafeRASem.let1,assumption+,simp,simp)

(* Let 2 *)
apply (rule allI)
apply (erule_tac x="td+1" in allE)
apply (elim exE)
apply (rename_tac r2)
apply (case_tac r2)
apply (rename_tac δ2 rest2)
apply (case_tac rest2)
apply (rename_tac m2 s2)
apply (rule_tac x="(δ2⊕(empty(j\<mapsto>1)),m2+1,s2+1)" in exI)
apply (rule SafeRASem.let2,assumption+,clarify)

(* Case 1 *)
apply (rule allI)
apply (erule_tac x="nat ((int td)+ nr)" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ,m, (ss+nr))" in exI)
apply (rule SafeRASem.case1,assumption+,clarify)

(* Case 1.1 *)
apply (rule allI)
apply (erule_tac x="td" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ,m,ss)" in exI)
apply (rule SafeRASem.case1_1,assumption+,clarify)

(* Case 1.2 *)
apply (rule allI)
apply (erule_tac x="td" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ,m,ss)" in exI)
apply (rule SafeRASem.case1_2,assumption+,clarify)

(* Case 2 *)
apply (rule allI)
apply (erule_tac x="nat ((int td)+ nr)" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ⊕(empty(j\<mapsto>-1)),max 0 (m - 1),ss+nr)" in exI)
apply (rule SafeRASem.case2,assumption+,clarify)

(* App primops *)
apply (rule allI)
apply (rule_tac x="([]k,0,2)" in exI)
apply (rule SafeRASem.app_primops,assumption+)

(* App *)
apply (rule allI)
apply (erule_tac x="length as+ length rs" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ(k+1:=None),m,max((int n)+(int l))(ss+(int n)+(int l) - int td))" in exI)
apply (rule SafeRASem.app)
apply assumption+
apply simp
apply simp

(* App 2 *)
apply (rule allI)
apply (erule_tac x="n+l" in allE)
apply (elim exE)
apply (rename_tac r)
apply (case_tac r)
apply (rename_tac δ rest)
apply (case_tac rest)
apply (rename_tac m ss)
apply (rule_tac x="(δ(k+1:=None),m,max((int n)+(int l))(ss+(int n)+(int l) - int td))" in exI)
apply (rule SafeRASem.app)
apply assumption+
apply simp
apply simp
done

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

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

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

apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
thm eqSemRADepth
 apply (erule_tac x=td in allE)
 apply (elim exE)
 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 (rule allI)
 apply (drule_tac td=td in eqSemDepthRA)
 apply (elim exE)
 apply (rule_tac x=x in exI)
 by assumption


lemma eqSemBoundRA [rule_format]: 
  "∃ n. (E1,E2) \<turnstile> h,k,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_tac td=td in eqSemDepthRA)
 apply (elim exE)
 apply (rule_tac x=x in exI)
 apply assumption
(* backwards implication *)
 apply (elim exE)
 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,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_tac td=td in eqSemDepthRA)
apply (elim exE)
apply (rule_tac x=x in exI)
by assumption



end