Up to index of Isabelle/HOL/SafeImp
theory basic_properties(* Title: Basic Properties
Author: Javier de Dios and Ricardo Peņa
Copyright: December 2008, Universidad Complutense de Madrid
*)
header {* Certification of the translation CoreSafe to SVM. Basic properties *}
theory basic_properties
imports Main "../CoreSafe/SafeRASemantics" SVMSemantics CertifSafeToSVM_definitions
begin
text{* This set of axioms reflects basic properties of the Core-Safe
expressions. The abstract syntax of Safe is general enough to admit both
Full-Safe and Core-Safe programs, but the latter has severe restrictions
which are needed in order to prove some of the theorems. These properties are
guaranteed by the compiler and cannot be proved. The most important
ones are:
\begin{itemize}
\item The arguments of function and constructor
applications are atoms (i.e.\ either literals or variables)
\item All the bound variables are distinct. Also, 'self' is a reserved
identifier denoting the working region of the function at hand.
\item The lengths of formal and actual argument lists are equal.
\end{itemize}
In a future, perhaps the valid Core-Safe expressions could be defined as
an inductive set.
*}
consts
core :: "'a Exp => bool"
fun atom :: "'a Exp => bool"
where
"atom (ConstE c _) = True"
| "atom (VarE x _) = True"
| "atom _ = False"
(* All expressions in these scripts are Core-Safe ones *)
axioms all_exp_core: "core e"
axioms x_not_self:
"core e
==> (∀ x∈ varProg e. x≠ self)"
axioms app_distinct_boundVar:
"Σ f = Some (xs,rs,e)
==> core e
∧ distinct (xs @ rs)
∧ self ∉ set xs
∧ self ∉ set rs"
axioms app_atoms:
"core (AppE f as rr a)
==> (∀ a ∈ set as. atom a)"
axioms app_arguments_good:
"[| core (AppE f as rr a);
Σ f = Some (xs,rs,e)|]
==> length xs = length as ∧ length rs = length rr"
axioms let_atoms:
"core (Let x1 = ConstrE C as r a1 In e2 a2)
==> (∀ a ∈ set as. atom a) ∧ x1 ∉ fvs as"
(* ================================================================ *)
text{* This group are obvious theorems of the translation, but tedious to
prove. For the moment, we have concentrated on proving the theorems
related to the semantics, both at the Core-Safe and at the SVM levels,
which are more important for the correctness. *}
axioms codestore_extend:
"[| ((p, funm, contm), codes) = mapAccumL trF (1, empty, []) defs;
(q,ls,is,cs1) = trE p' fun funame rho e;
cs = concat codes |]
==> (cs1 @ [(q, is, fname)]) \<sqsubseteq> cs"
axioms codestore_let_disjoint:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Let x1 = e1 In e2 a);
(q1, ls1, is1, cs1') = trE p1' funm fname rho1 e1;
(q2, ls2, is2, cs2) = trE p' funm fname rho2 e2;
cs1 = cs2 @ (q2, is2, fname) # cs1';
drop j is' = is|]
==> disjointList cs1 [(q, is', fname)]
∧ disjointList (cs2 @ [(q2, is2, fname)]) (cs1' @ [(q1, is', fname)])"
axioms codestore_let2_disjoint:
"[| (q, ls, is1, cs1) = trE p' funm fname rho e |]
==> q ∉ dom (map_of cs1)"
axioms codestore_case_alts_disjoint:
"[| (q, ls, is, cs1) = trE p' funm fname rho e;
e = (Case VarE x a Of alts a') ∨ e = (CaseD VarE x a Of alts a');
(q, rss) = trAlts p' funm fname rho alts;
(lss, qs, css) = unzip3 rss;
i < length alts;
alts!i = (pati, ei);
pati = ConstrP C ps ms;
xs = map pat2var ps;
(qs ! i, lss !i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei|]
==> q ∉ dom (map_of (concat css)) ∧ qs!i ∉ dom (map_of (concat css))"
axioms codestore_caseL_alts_disjoint:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a');
(q, rss) = trAlts p' funm fname rho alts;
(lss, qs, css) = unzip3 rss;
i < length alts;
alts!i = (pati, ei);
(qs ! i, lss !i, isi, csi) = trE p' funm fname rho ei|]
==> q ∉ dom (map_of (concat css)) ∧ qs!i ∉ dom (map_of (concat css))"
axioms trE_let:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Let x1 = e1 In e2 a);
e1 ≠ ConstrE C as r a|]
==>
∃ q1 ls1 is1 cs1' q2 ls2 is2 cs2 .
(q1,ls1,is1,cs1') = trE (q2+1) funm fname (rho++) e1
∧ (q2,ls2,is2,cs2) = trE p' funm fname (rho+[(x1,1)]) e2
∧ cs1 = cs2 @ ((q2,is2,fname) # cs1')
∧ q=q1 ∧ ls = q2#(ls1 @ ls2) ∧ is = PUSHCONT q2 # is1"
axioms trE_let2:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Let x1 = ConstrE C as r a' In e2 a)|]
==>
∃ q2 ls2 is2 cs2 items item .
(q2,ls2,is2,cs2) = trE p' funm fname (rho+[(x1,1)]) e2
∧ items = map (atom2item rho) as
∧ item = region2item rho r
∧ q = q2
∧ ls = ls2
∧ is = BUILDCLS C items item # is2
∧ cs1 = cs2"
axioms trE_case:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a');
i < length alts; alts!i = (pati, ei); pati = ConstrP C ps ms;
xs = map pat2var ps |]
==>
∃ rss lss qs css isi csi.
(q,rss) = trAlts p' funm fname rho alts
∧ (lss,qs,css) = unzip3 rss
∧ ls = concat lss
∧ is = [MATCH (rho |> x) qs]
∧ cs1 = concat css
∧ subList (csi @ [(qs!i,isi,fname)]) cs1
∧ (qs ! i, lss !i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei"
axioms trE_case_1_1:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a');
i < length alts; alts!i = (pati, ei); pati = ConstP (LitN n) |]
==>
∃ rss lss qs css v' m' isi csi.
(q,rss) = trAlts p' funm fname rho alts
∧ (lss,qs,css) = unzip3 rss
∧ ls = concat lss
∧ is = [MATCHN (rho |> x) v' m' qs]
∧ cs1 = concat css
∧ subList (csi @ [(qs!i,isi,fname)]) cs1
∧ (qs ! i, lss !i, isi, csi) = trE p' funm fname rho ei"
axioms trE_case_1_2:
"[| (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a');
i < length alts; alts!i = (pati, ei); pati = ConstP (LitB b) |]
==>
∃ rss lss qs css isi csi.
(q,rss) = trAlts p' funm fname rho alts
∧ (lss,qs,css) = unzip3 rss
∧ ls = concat lss
∧ is = [MATCHN (rho |> x) 0 2 qs]
∧ cs1 = concat css
∧ subList (csi @ [(qs!i,isi,fname)]) cs1
∧ (qs ! i, lss !i, isi, csi) = trE p' funm fname rho ei"
axioms trE_cased:
"[| (q, ls, is, cs1) = trE p' funm fname rho (CaseD VarE x a Of alts a');
i < length alts; alts!i = (pati, ei); pati = ConstrP C ps ms;
xs = map pat2var ps |]
==>
∃ rss lss qs css isi csi.
(q,rss) = trAlts p' funm fname rho alts
∧ (lss,qs,css) = unzip3 rss
∧ ls = concat lss
∧ is = [MATCHD (rho |> x) qs]
∧ cs1 = concat css
∧ subList (csi @ [(qs!i,isi,fname)]) cs1
∧ (qs ! i, lss !i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei"
axioms trE_app:
"[| Σ f = Some (xs, rs, e);
(q, ls, is, cs1) = trE p' funm fname rho (AppE f as rr a) |]
==>
∃ qf lsf csf.
(qf, lsf, is, csf) = trE p' funm fname ([(empty,0,0)] + (zip (xs @ rs) (decreasing (length xs + length rs)))) e
∧ xs = fst (the (Σ f))
∧ rs = fst (snd (the (Σ f)))
∧ e = snd (snd (the (Σ f)))
∧ qf = the (funm f)"
(* all the codelabels are distinct *)
axioms p_Fresh:
"((p,funm,contm),cs) = mapAccumL trF (Suc 0,empty,[]) defs
==> ∀ q ∈ dom (map_of (concat cs)). q < p"
constdefs
goodPC :: "CodeLabel × nat => SVMCode => bool"
"goodPC pc cs ≡ (case pc of (p,j) =>
case map_of cs p of Some (is,f) =>
j < length is)"
(* all the pc's generated by the translation are good *)
axioms goodPCtranslation:
"[| P\<turnstile>s0 , td#tds -svm-> s # ss, Suc 0#tds;
P = ((cs,cm),p,ct,sz);
s0 = ((h,k),k0,pc,S);
s = ((h',k'),k0',pc',S')|]
==>
goodPC pc cs ∧ goodPC pc' cs"
axioms rho_good:
"(q, ls, is, cs1) = trE p' funm fname rho e
==> length rho > 0 ∧ rho_good rho"
(* ================================================================== *)
text{* This group are real axioms in the sense that either the properties
must be guaranteed outside these scripts, or they depend on not controlable
issues, as it is the case of fresh names generation *}
(* the domain of the initial heap must be finite, and the value and
region environments must be disjoint *)
axioms finite_dom_h [rule_format]:
"(E1,E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r
--> finite (dom h)
∧ dom E1 ∩ dom E2 = {}
∧ fvReg e ⊆ dom E2
∧ fv e ⊆ dom E1
∧ self ∈ dom E2
∧ boundVar e ∩ dom E2 = {}"
(* The case branch i chosen at runtime must be the same in the SVM than in the semantics *)
axioms case_constructor_good:
"[|(E1',E2) \<turnstile> h,k, nat ((int td)+ nr), ei \<Down> h',k,v,r;
E1' = extend E1 xs vs;
E1 x = Some (Val.Loc p);
h p = Some (j,C,vs);
alts!i = (pati, ei);
pati = ConstrP C ps ms|]
==> ct C = Some (g1,i,g2)"
axioms cased_constructor_good:
"[|(E1',E2) \<turnstile> h(p := None),k, nat ((int td)+ nr), ei \<Down> h',k,v,r;
E1 x = Some (Val.Loc p);
E1' = extend E1 xs vs;
h p = Some (j,C,vs);
alts!i = (pati, ei);
pati = ConstrP C ps ms|]
==> ct C = Some (g1,i,g2)"
(* The branch chosen in a case of literals by the SVM is consistent with the branch
chosen by the semantics *)
axioms SVM_Semantic_branch_Nat_consistent:
"[| is = [MATCHN (rho |> x) v' m' qs];
E1 x = Some (IntT n);
i < length alts |]
==> (nat n - v' >= 0 ∧ nat n - v' <= m' - 1 --> nat n - v' = i) ∧
( ¬ (nat n - v' >= 0 ∧ nat n - v' <= m' - 1) --> m' = i)"
axioms SVM_Semantic_branch_Bool_consistent:
"[| is = [MATCHN (rho |> x) 0 2 qs];
E1 x = Some (BoolT b);
i < length alts |]
==> (¬ b --> qs ! 0 = qs ! i) ∧ (b --> qs ! Suc 0 = qs ! i)"
(* The name of the fresh variable obtained in the semantics must be the same
as the fresh name obtained by the machine *)
axioms getFresh_fresh:
"SafeHeap.fresh q h ==> getFresh h = q"
(* =======================================================================
aqui estan los antiguos, algunos con el nombre ligeramente cambiado.
El objetivo es que desparezcan todos, bien porque se utilicen los de arriba,
bien porque se conviertan en teoremas demostrados,
=================================================================== *)
axioms finite_dom_h':
"[|(E1,E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r; finite (dom h)|]
==> finite (dom h')"
(* maxFreshWords_App *)
axioms app1_1:
"∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v"
axioms app1_2:
"∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'"
(************* CertifSafeToSVM Theorems ***************)
lemma closureCalled_app:
"closureCalled e defs ⊆ closureCalled (AppE f as rs' a) defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
apply (rule closureCalled.init) apply simp defer
apply (simp, rule closureCalled.step, assumption+,simp)
oops
axioms closureCalled_app:
"closureCalled e defs ⊆ closureCalled (AppE f as rs' a) defs"
axioms j_length:
"j < length (fst (the (map_of (concat codes) p')))"
axioms j_length_2:
" j < length is'"
axioms lengthS_topDepth:
"E \<Join> (rho,S) ==> topDepth rho < length S"
axioms resources_gre_0:
"(E1, E2) \<turnstile> h , k , td , e \<Down> h', k , v , r ==> ∃ δ m s. r=(δ ,m,s) ∧ m >= 0 ∧ s > 0"
axioms addEnv_rho_good:
"addEnv_good rho (zip xs (decreasing (length xs)))"
(********************** execSVMBalanced_lemmas Theorems ***************)
axioms identityEnvironment_good:
"(E1,E2) \<Join> (ρ,S)
==> (∀x∈ dom E1. S!+(ρ |> x) = Val v) ∧ (∀x∈ dom E2. S!+(ρ |> x) = Reg r) ∧ dom E1 ∩ dom E2 = {}"
(****************** maxFreshWords_lemmas Theorems *************)
(* maxFreshWords_App *)
axioms continuations_bueno:
"[|(E1, E2) \<Join> (rho,S); td = topDepth rho|]
==> sizeST (drop td S) - sizeST S = - int td"
(****************** maxFreshCells_lemmas Theorems *************)
(* maxFreshCells_Let1 *)
axioms let1_3:
"sizeH ((h' |` {p ∈ (dom h'). ((fst (the (h' p))) ≤ k)}), k) - (sizeH (h, k)) =
\<parallel> diff k (h,k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<parallel>"
(****************** identityEnvironment_lemmas Theorems *************)
axioms xi2: "S !+ (rho |> (ai)) =
append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
(drop td S) !+ i"
axioms ri2: "S !+ (rho |> (rs ! i)) =
append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
(drop td S) !+ (length xs + i)"
axioms xi3: "([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (xs!i) = i"
axioms ri3: "(length xs + i) = ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (rs!i)"
axioms xiConstE:
"Val (the (map_of (zip xs (map (atom2val E1) as)) (xs ! i))) =
(map (item2Stack k S) (map (atom2item rho) as) @ map (item2Stack k S) (map (region2item rho) rr) @ drop td S) !+
(([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (xs ! i))"
(********* Lemas que ***)
axioms good_app_region_arguments:
"∀ r ∈ set rr. r ∈ dom E2 - {self}"
end