Up to index of Isabelle/HOL/CoreSafe
theory SafeRASemantics(* Title: Resource-Aware Safe Semantics
Author: Ricardo Peņa and Javier de Dios
Copyright: May 2008, Universidad Complutense de Madrid
*)
header {* Resource-Aware Operational semantics of Safe expressions *}
theory SafeRASemantics
imports SafeExpr "../SafeImp/SVMState"
begin
types
Delta = "(Region \<rightharpoonup> int)"
MinimumFreshCells = int
MinimumWords = int
Resources = "Delta × MinimumFreshCells × MinimumWords"
constdefs sizeVal :: "[HeapMap, Val] => int"
"sizeVal h v ≡ (case v of (Loc p) => int p
| _ => 0)"
constdefs size :: "[HeapMap, Location] => int" where
"size h p ≡ (case h p of
Some (j,C,vs) => (let rp = getRecursiveValuesCell (C,vs)
in 1+ (∑i∈rp. sizeVal h (vs!i))))"
constdefs balanceCells :: "Delta => int" ("\<parallel> _ \<parallel>" [71] 70)
"balanceCells δ ≡ (∑n∈ran δ. n)"
constdefs addDelta :: "Delta => Delta => Delta" (infix "⊕" 110)
"addDelta δ1 δ2 ≡ (%x. (if x ∈ dom δ1 ∩ dom δ2
then (case δ1 x of (Some y) =>
case δ2 x of (Some z) => Some (y + z))
else if x ∈ dom δ1 - dom δ2
then δ1 x
else if x ∈ dom δ2 - dom δ1
then δ2 x
else None))"
constdefs emptyDelta :: "nat => nat \<rightharpoonup> int" ( "[]_" [71] 70)
"[]k ≡ (%i. if i ∈ {0..k}
then Some 0
else None)"
consts def_copy :: "nat => Heap => bool"
inductive
SafeRASem :: "[Environment ,HeapMap, nat, nat, unit Exp, HeapMap, nat, Val, Resources ] => bool"
( "_ \<turnstile> _ , _ , _ , _ \<Down> _ , _ , _ , _ " [71,71,71,71,71,71,71] 70)
where
litInt : "E \<turnstile> h, k, td, (ConstE (LitN i) a) \<Down> h, k, IntT i,([]k,0,1)"
| litBool: "E \<turnstile> h , k, td, (ConstE (LitB b) a) \<Down> h, k, BoolT b,([]k,0,1)"
| var1 : "E1 x = Some (Val.Loc p)
==> (E1,E2) \<turnstile> h, k, td, (VarE x a) \<Down> h, k, Val.Loc p,([]k,0,1)"
| 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 = size h p|]
==> (E1,E2) \<turnstile> h, k , td, (x @ r a)\<Down> h', k, Val.Loc p',([j \<mapsto> m],m,2)"
| 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>((h(p:=None))(q \<mapsto> c)),k,Val.Loc q,([]k,0,1)"
| let1 : "[| ∀ C as r a'. e1 ≠ ConstrE C as r a'; x1 ∉ dom E1;
(E1,E2) \<turnstile> h,k,0,e1\<Down> h',k,v1,(δ1,m1,s1);
(E1(x1 \<mapsto> v1),E2) \<turnstile> h',k,(td+1),e2\<Down>h'',k,v2,(δ2,m2,s2) |]
==> (E1,E2) \<turnstile> h,k, td, Let x1 = e1 In e2 a\<Down>h'',k,v2,
(δ1⊕δ2,max m1 (m2 + \<parallel>δ1\<parallel>),max (s1+2) (s2+1))"
| 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>h',k,v2,(δ,m,s)|]
==> (E1,E2) \<turnstile> h,k, td, Let x1 = ConstrE C as r a' In e2 a\<Down>h',k,v2,
(δ⊕(empty(j\<mapsto>1)),m+1,s+1)"
| 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, nat ((int td)+ nr), ei \<Down> h',k,v,(δ,m,s)|]
==> (E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down> h', k,v,(δ,m, (s+nr))"
| 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> h',k,v,(δ,m,s)|]
==> (E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down> h', k,v,(δ,m,s)"
| 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> h',k,v,(δ,m,s)|]
==> (E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down> h', k,v,(δ,m,s)"
| 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, nat ((int td)+ nr), ei \<Down> h',k,v,(δ,m,s)|]
==> (E1,E2) \<turnstile> h,k, td, CaseD (VarE x a) Of alts a' \<Down> h', k,v,
(δ⊕(empty(j\<mapsto>-1)),max 0 (m - 1),s+nr)"
| app_primops: "[| primops f = Some oper;
v1 = atom2val E1 a1;
v2 = atom2val E1 a2;
v = execOp oper v1 v2|]
==> (E1,E2) \<turnstile> h,k, td, AppE f [a1,a2] [] a \<Down> h, k,v,([]k,0,2)"
| 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), (n+l), e\<Down> h', (Suc k),v,(δ,m,s);
h'' = h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k} |]
==> (E1,E2) \<turnstile> h,k, td, AppE f as rr a \<Down> h'', k,v,
(δ(k+1:=None),m,max((int n)+(int l))(s+ (int n)+(int l) - int td))"
end