Up to index of Isabelle/HOL/CoreSafe
theory SafeRegion_definitions(* Title: Safe Region Definitions
Author: Javier de Dios and Ricardo Peņa
Copyright: February 2009, Universidad Complutense de Madrid
*)
header {* Region Definitions *}
theory SafeRegion_definitions imports SafeRASemantics
SafeDepthSemantics
"../SafeImp/ClosureHeap"
begin
(* Auxiliary definitions *)
(* ρ *)
types RegionTypeVariable = "string"
(* ρself *)
constdefs
ρself :: string
"ρself ≡ ''rho_self''"
types VarType = "string"
(* Type Expressions *)
datatype TypeExpression = VarT VarType
| ConstrT string "TypeExpression list" "VarType list"
(* ϑ (x) = T ti ρi *)
types TypeMapping = "(string \<rightharpoonup> TypeExpression)"
types RegMapping = "(string \<rightharpoonup> string)"
types ThetaMapping = "TypeMapping × RegMapping"
(* η *)
types InstantiationMapping = "VarType \<rightharpoonup> nat"
(* (μ1,μ2) *)
types TypeMu = "(string \<rightharpoonup> TypeExpression) × (string \<rightharpoonup> string)"
(* mu_ext *)
consts mu_ext :: "TypeMu => TypeExpression => TypeExpression"
mu_exts :: "TypeMu => TypeExpression list => TypeExpression list"
primrec
"mu_ext μ (VarT a) = the ((fst μ) a)"
"mu_ext μ (ConstrT T tm ρs) = (ConstrT T (mu_exts μ tm) (map (the o (snd μ)) ρs))"
"mu_exts μ [] = []"
"mu_exts μ (x#xs) = mu_ext μ x # (mu_exts μ xs)"
(* atoms *)
fun atoms :: "('a Exp) list => bool"
where
"atoms as = (∀ i < length as. (∃ c a. as!i = ConstE (LitN c) a) ∨
(∃ b a. as!i = ConstE (LitB b) a) ∨
(∃ x a. as!i = VarE x a))"
(* argP_aux *)
fun argP_aux :: "(string \<rightharpoonup> TypeExpression) => 'a Exp => TypeExpression => bool"
where
"argP_aux ϑ (ConstE (LitN _) _) t = (t = (ConstrT intType [] []))"
| "argP_aux ϑ (ConstE (LitB _) _) t = (t = (ConstrT boolType [] []))"
| "argP_aux ϑ (VarE x _) t = (ϑ x = Some t)"
(* argP *)
fun
argP ::
"TypeExpression list => VarType => ('a Exp) list => RegVar => ThetaMapping => bool"
where
"argP ti ρ as r (ϑ1,ϑ2) = (
length ti = length as ∧
atoms as ∧
(∀ i < length as. argP_aux ϑ1 (as!i) (ti!i)) ∧
ϑ2 r = Some ρ)"
(* constructorSignature *)
types
ConstructorSignatureFun = "string \<rightharpoonup> TypeExpression list × VarType × TypeExpression"
consts constructorSignature :: ConstructorSignatureFun
(* coherent ConstructorTable & constructorSignature *)
constdefs coherentC :: "Constructor => bool"
"coherentC C ≡
(let (nargs,n,largs) = the (ConstructorTable C);
(ts,ρl,t) = the (constructorSignature C)
in length ts = length largs ∧
(∃ T tm ρs. t = ConstrT T tm ρs) ∧
(∀ i < length ts. (ts!i = ConstrT intType [] [] -->
(snd (snd (the (ConstructorTable C))))!i = IntArg)
∧ (ts!i = ConstrT boolType [] [] -->
(snd (snd (the (ConstructorTable C))))!i = BoolArg)
∧ ((∃ T' tm' ρs'. (ts!i = ConstrT T' tm' ρs' ∧ ts!i ≠ t) ∨
(∃ a. ts!i = VarT a)) -->
(snd (snd (the (ConstructorTable C))))!i = NonRecursive)
∧ (ts!i = t --> (snd (snd (the (ConstructorTable C))))!i = Recursive)))"
constdefs coherent :: "ConstructorSignatureFun => ConstructorTableFun => bool"
"coherent Γc Tc ≡ dom Γc = dom Tc ∧ (∀ C ∈ dom Γc. coherentC C)"
(* Definitions for APP *)
definition
map_f_comp :: "('b => 'c) => ('a ~=> 'b) => ('a ~=> 'c)" where
"map_f_comp f g = (λ k. case g k of None => None | Some v => Some (f v))"
notation (xsymbols)
map_f_comp (infixl "of" 55)
(* argP_app *)
fun
argP_app ::
"TypeExpression list => RegVar list => ('a Exp) list => RegVar list => ThetaMapping => bool"
where
"argP_app ti ρs as rs (ϑ1,ϑ2) = (
length ti = length as ∧
length ρs = length rs ∧
atoms as ∧
(∀ i < length as. argP_aux ϑ1 (as!i) (ti!i)) ∧
(∀ i < length rs. ϑ2 (rs!i) = Some (ρs!i)))"
declare argP_app.simps [simp del]
(* functionSignature *)
consts functionSignature :: "string \<rightharpoonup> TypeExpression list × VarType list × TypeExpression"
(* regions *)
consts regions :: "TypeExpression => string set"
regions' :: "TypeExpression list => string set"
primrec
"regions (VarT a) = {}"
"regions (ConstrT T tm ρs) = (regions' tm) ∪ set ρs"
"regions' [] = {}"
"regions' (t#ts) = regions t ∪ regions' ts"
constdefs regionV :: "HeapMap => Location => nat"
"regionV h p ≡ (case h p of Some (j,C,vs) => j)"
constdefs regionsV :: "HeapMap => Location set => nat set"
"regionsV h ps ≡ \<Union> p ∈ ps. {regionV h p}"
(* variables *)
consts variables :: "TypeExpression => string set"
variables' :: "TypeExpression list => string set"
primrec
"variables (VarT a) = {a}"
"variables (ConstrT T tm ρs) = (variables' tm)"
"variables' [] = {}"
"variables' (t#ts) = variables t ∪ variables' ts"
(* wellT *)
fun
wellT :: " TypeExpression list => VarType => TypeExpression => bool"
where
"wellT tn ρ (ConstrT T tm ρs) =
((length ρs > 0 ∧ ρ = last ρs ∧ distinct ρs ∧ last ρs ∉ regions' tm)
∧ (∀ i < length tn. regions (tn!i) ⊆ regions (ConstrT T tm ρs) ∧
variables (tn!i) ⊆ variables (ConstrT T tm ρs)))"
(* Auxiliary definitions for APP *)
constdefs
ρfake :: string
"ρfake ≡ ''rho_fake''"
constdefs ρ_ren :: "string => string"
"ρ_ren ρ ≡ (if ρ = ρself then ρfake else ρ)"
(* t_ren *)
consts t_ren :: "TypeExpression => TypeExpression"
t_rens :: "TypeExpression list => TypeExpression list"
primrec
"t_ren (VarT a) = (VarT a)"
"t_ren (ConstrT T tm ρs) = ConstrT T (t_rens tm) (map ρ_ren ρs)"
"t_rens [] = []"
"t_rens (x#xs) = t_ren x # (t_rens xs)"
(* ρ_ren_inv *)
constdefs ρ_ren_inv :: "string => string"
"ρ_ren_inv ρ ≡ (if ρ = ρfake then ρself else ρ)"
(* t_ren_inv *)
consts t_ren_inv :: "TypeExpression => TypeExpression"
t_ren_invs :: "TypeExpression list => TypeExpression list"
primrec
"t_ren_inv (VarT a) = (VarT a)"
"t_ren_inv (ConstrT T ts rs) = ConstrT T (t_ren_invs ts) (map ρ_ren_inv rs)"
"t_ren_invs [] = []"
"t_ren_invs (t#tm) = (t_ren_inv t) # t_ren_invs tm"
(* notFake *)
consts notFake :: "TypeExpression => bool"
notFakes :: "TypeExpression list => bool"
primrec
"notFake (VarT a) = (a ≠ ρfake)"
"notFake (ConstrT T tm ρs) = ((notFakes tm) ∧ (∀ ρ ∈ set ρs. ρ ≠ ρfake))"
"notFakes [] = True"
"notFakes (x#xs) = (notFake x ∧ notFakes xs)"
(* mu_ext_def *)
constdefs mu_ext_def :: "TypeMu => TypeExpression => bool"
"mu_ext_def μ t ≡ notFake (mu_ext μ t)"
consts mu_exts_def :: "TypeMu => TypeExpression list => bool"
primrec
"mu_exts_def μ [] = True"
"mu_exts_def μ (x#xs) = (mu_ext_def μ x ∧ mu_exts_def μ xs)"
fun μ_ren :: "TypeMu => TypeMu"
where
"μ_ren (μ1,μ2) = (λ x. Some (t_ren (the (μ1 x))),
λ ρ. Some (ρ_ren (the (μ2 ρ))))"
constdefs η_ren :: "InstantiationMapping => InstantiationMapping"
"η_ren η ≡ (λ x. if x = ρself then None else η x) ++
(if (ρself ∈ dom η) then [ρfake \<mapsto> the (η ρself)] else empty)"
(* consistent_v *)
inductive
consistent_v :: "[TypeExpression, InstantiationMapping, Val, HeapMap ] => bool"
where
primitiveI : "consistent_v (ConstrT intType [] []) η (IntT i) h"
| primitiveB : "consistent_v (ConstrT boolType [] []) η (BoolT b) h"
| variable : "consistent_v (VarT a) η v h"
| algebraic_None : "p ∉ dom h ==> consistent_v t η (Loc p) h"
| algebraic : "[| h p = Some (j,C,vn);
ρl = last ρs;
ρl ∈ dom η; η (ρl) = Some j;
constructorSignature C = Some (tn',ρ',ConstrT T tm' ρs');
wellT tn' (last ρs') (TypeExpression.ConstrT T tm' ρs');
length vn = length tn';
∃ μ1 μ2. (((the (μ2 (last ρs'))), mu_ext (μ1,μ2) (ConstrT T tm' ρs')) =
(ρl,ConstrT T tm ρs) ∧
(∀ i < length vn. consistent_v ((map (mu_ext (μ1,μ2)) tn')!i) η (vn!i) h)) |]
==> consistent_v (ConstrT T tm ρs) η (Loc p) h"
(* consistent *)
fun
consistent :: "ThetaMapping => InstantiationMapping => Environment => HeapMap => bool"
where
"consistent (ϑ1,ϑ2) η (E1,E2) h =
((∀ x ∈ dom E1. ∃ t v. ϑ1 x = Some t
∧ E1 x = Some v
∧ consistent_v t η v h)
∧ (∀ r ∈ dom E2 . ∃ r' r''. ϑ2 r = Some r'
∧ η r' = Some r''
∧ E2 r = Some r'')
∧ self ∈ dom E2
∧ ϑ2 self = Some ρself)"
(* admissible *)
constdefs
admissible :: "InstantiationMapping => nat => bool"
"admissible η k ≡
ρself ∈ dom η ∧
(∀ ρ ∈ dom η.
∃ k'.
η ρ = Some k' ∧
(ρ = ρself --> k' = k) ∧
(ρ ≠ ρself --> k' < k))"
(* extend_heaps *)
fun extend_heaps :: "Heap => Heap => bool" ("_ \<sqsubseteq> _" 1000)
where
"(h,k) \<sqsubseteq> (h',k') = (∀ p ∈ dom h. (dom h' - dom h) ∩ closureL p (h,k) = {}
∧ h p = h' p)"
(* Region Enviroment type *)
types RegionEnv = "string \<rightharpoonup> TypeExpression list × VarType list × TypeExpression"
constdefs typesArgAPP :: "RegionEnv => string => TypeExpression list"
"typesArgAPP Σ f == (case Σ f of Some (ti,ρs,tf) => ti)"
constdefs regionsArgAPP :: "RegionEnv => string => string list"
"regionsArgAPP Σ f ≡ (case Σ f of Some (ti,ρs,tf) => ρs)"
constdefs typeResAPP :: "RegionEnv => string => TypeExpression"
"typeResAPP Σ f ≡ (case Σ f of Some (ti,ρs,tf) => tf)"
(* e satisfies the static assertion \<lbrace>ϑ,t\<rbrace> *)
fun
SafeRegionDAss::"unit Exp => ThetaMapping => TypeExpression => bool"
("_ : \<lbrace> _ , _ \<rbrace>" 1000)
where
"SafeRegionDAss e (ϑ1,ϑ2) t =
(∀ E1 E2 h k td h' v r η.
(E1,E2) \<turnstile> h, k, td, e \<Down> h', k, v, r (* P1 *)
∧ fv e ⊆ dom E1 ∧ fvReg e ⊆ dom E2 (* P1' *)
∧ dom E1 ⊆ dom ϑ1 ∧ dom E2 ⊆ dom ϑ2 (* P2 *)
∧ admissible η k (* P3 *)
∧ consistent (ϑ1,ϑ2) η (E1,E2) h (* P4 *)
--> consistent_v t η v h')" (* P5 *)
(* A region environment ΣT is valid. \<Turnstile> ΣT *)
inductive
ValidGlobalRegionEnv :: "RegionEnv => bool" ("\<Turnstile> _ " 1000)
where
base: " \<Turnstile> empty"
| step: "[| \<Turnstile> Σt; f ∉ dom Σt;
ϑ1 = map_of (zip (varsAPP Σf f) ti);
ϑ2 = map_of (zip (regionsAPP Σf f) ρs) ++ [self \<mapsto> ρself];
(bodyAPP Σf f) : \<lbrace> (ϑ1,ϑ2) , tf \<rbrace>|] ==> \<Turnstile> Σt(f\<mapsto>(ti,ρs,tf))"
(* e satisfies the static assertion \<lbrace>ϑ,t\<rbrace> in the context of ΣT *)
constdefs SafeRegionDAssCntxt ::
"unit Exp => RegionEnv => ThetaMapping => TypeExpression => bool" ("_ , _ : \<lbrace> _ , _ \<rbrace>" 1000)
"SafeRegionDAssCntxt e Σt ϑ t ≡ (\<Turnstile> Σt --> e : \<lbrace> ϑ , t \<rbrace>)"
(* The subexpresion e of f's body satisfies the static assertion \<lbrace>ϑ,t\<rbrace>
up to depth n *)
fun
SafeRegionDAssDepth::"unit Exp => string => nat => ThetaMapping => TypeExpression => bool"
("_ :_ , _ \<lbrace> _ , _ \<rbrace>" 1000)
where
"SafeRegionDAssDepth e f n (ϑ1,ϑ2) t =
(∀ E1 E2 h k h' v η.
(E1,E2) \<turnstile> h, k, e \<Down>(f,n) h', k, v (* P1 *)
∧ fv e ⊆ dom E1 ∧ fvReg e ⊆ dom E2 (* P1' *)
∧ dom E1 ⊆ dom ϑ1 ∧ dom E2 ⊆ dom ϑ2 (* P2 *)
∧ admissible η k (* P3 *)
∧ consistent (ϑ1,ϑ2) η (E1,E2) h (* P4 *)
--> consistent_v t η v h')" (* P5 *)
(* A region environment ΣT is valid up to depth n for function f.
\<Turnstile>f,n ΣT *)
inductive ValidGlobalRegionEnvDepth :: "string => nat => RegionEnv => bool"
("\<Turnstile>_ , _ _ " 1000)
where
base : "[| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,n Σt"
| depth0 : "[| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,0 Σt(f\<mapsto>(ti,ρs,tf))"
| step : "[| \<Turnstile> Σt; f ∉ dom Σt;
ϑ1 = map_of (zip (varsAPP Σf f) ti);
ϑ2 = map_of (zip (regionsAPP Σf f) ρs) ++ [self \<mapsto> ρself];
(bodyAPP Σf f) :f,n \<lbrace> (ϑ1,ϑ2) , tf \<rbrace> |] ==>
\<Turnstile>f,Suc n Σt(f\<mapsto>(ti,ρs,tf))"
| g : "[| \<Turnstile>f,n Σt; g ∉ dom Σt; g≠f;
ϑ1 = map_of (zip (varsAPP Σf g) ti);
ϑ2 = map_of (zip (regionsAPP Σf g) ρs) ++ [self \<mapsto> ρself];
(bodyAPP Σf g) : \<lbrace> (ϑ1,ϑ2) , tf \<rbrace> |] ==>
\<Turnstile>f, n Σt(g\<mapsto>(ti,ρs,tf))"
(* The subexpresion e of f's body satisfies the static assertion \<lbrace>ϑ,t\<rbrace>
up to depth n in the context of ΣT *)
constdefs SafeRegionDAssDepthCntxt ::
"unit Exp => RegionEnv => string => nat => ThetaMapping => TypeExpression =>
bool" ("_ , _ :_ , _ \<lbrace> _ , _ \<rbrace>" 1000)
"SafeRegionDAssDepthCntxt e Σm f n ϑ t ≡
( \<Turnstile>f,n Σm --> e :f,n \<lbrace> ϑ , t \<rbrace>)"
end