Up to index of Isabelle/HOL/arrays
theory Correct = BVSpec + JVMExec:(* Title: HOL/MicroJava/BV/Correct.thy
ID: $Id: Correct.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
The invariant for the type safety proof.
*)
header {* \isaheader{BV Type Safety Invariant} *}
theory Correct = BVSpec + JVMExec:
text {*
The fields of all objects contain only fully initialized objects:
*}
constdefs
l_init :: "'c prog \<Rightarrow> aheap \<Rightarrow> init_heap \<Rightarrow> ('a \<leadsto> val) \<Rightarrow> ('a \<leadsto> ty) \<Rightarrow> bool"
"l_init G hp ih vs Ts \<equiv>
\<forall>n T. Ts n = Some T \<longrightarrow> (\<exists>v. vs n = Some v \<and> is_init hp ih v)"
o_init :: "'c prog \<Rightarrow> aheap \<Rightarrow> init_heap \<Rightarrow> heap_entry \<Rightarrow> bool"
"o_init G hp ih entry \<equiv> case entry of Obj C fs \<Rightarrow> l_init G hp ih fs (map_of (fields (G,C)))
| Arr T l en \<Rightarrow> l_init G hp ih en (\<lambda>x. if x < l then Some T else None)"
h_init :: "'c prog \<Rightarrow> aheap \<Rightarrow> init_heap \<Rightarrow> bool"
"h_init G h ih \<equiv> \<forall>a obj. h a = Some obj \<longrightarrow> o_init G h ih obj"
text {*
Type and init information conforms.
For uninitialized objects dynamic+static type must be the same
*}
constdefs
iconf :: "'c prog \<Rightarrow> aheap \<Rightarrow> init_heap \<Rightarrow> val \<Rightarrow> init_ty \<Rightarrow> bool"
("_,_,_ \<turnstile> _ ::\<preceq>i _" [51,51,51,51,51] 50)
"G,h,ih \<turnstile> v ::\<preceq>i T ==
case T of Init ty \<Rightarrow> G,h\<turnstile>v::\<preceq>ty \<and> is_init h ih v
| UnInit C pc \<Rightarrow> G,h\<turnstile>v::\<preceq>(Class C) \<and>
(\<exists>l fs. v = Addr l \<and> h l = Some (Obj C fs) \<and> ih l = T)
| PartInit C \<Rightarrow> G,h\<turnstile>v::\<preceq>(Class C) \<and>
(\<exists>l D fs. v = Addr l \<and> h l = Some (Obj D fs) \<and> ih l = T)"
text {*
Alias analysis for uninitialized objects is correct.
If two values have the same uninitialized type, they must be equal and marked
with this type on the type tag heap.
*}
constdefs
corr_val :: "[val, init_ty, init_heap] \<Rightarrow> bool"
"corr_val v T ihp == \<exists>l. v = Addr l \<and> ihp l = T"
corr_loc :: "[val list, locvars_type, init_heap, val, init_ty] \<Rightarrow> bool"
"corr_loc loc LT ihp v T ==
list_all2 (\<lambda>l t. t = OK T \<longrightarrow> l = v \<and> corr_val v T ihp) loc LT"
corr_stk :: "[opstack, opstack_type, init_heap, val, init_ty] \<Rightarrow> bool"
"corr_stk stk ST ihp v T == corr_loc stk (map OK ST) ihp v T"
corresponds :: "[opstack,val list,state_type,init_heap,val,init_ty] \<Rightarrow> bool"
"corresponds stk loc s ihp v T ==
corr_stk stk (fst s) ihp v T \<and> corr_loc loc (snd s) ihp v T"
consistent_init :: "[opstack, val list, state_type, init_heap] \<Rightarrow> bool"
"consistent_init stk loc s ihp ==
(\<forall>C pc. \<exists>v. corresponds stk loc s ihp v (UnInit C pc)) \<and>
(\<forall>C. \<exists>v. corresponds stk loc s ihp v (PartInit C))"
text {*
The values on stack and local variables conform to their static type:
*}
constdefs
approx_val :: "[jvm_prog,aheap,init_heap,val,init_ty err] \<Rightarrow> bool"
"approx_val G h i v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h,i \<turnstile> v ::\<preceq>i T"
approx_loc :: "[jvm_prog,aheap,init_heap,val list,locvars_type] \<Rightarrow> bool"
"approx_loc G hp i loc LT == list_all2 (approx_val G hp i) loc LT"
approx_stk :: "[jvm_prog,aheap,init_heap,opstack,opstack_type] \<Rightarrow> bool"
"approx_stk G hp i stk ST == approx_loc G hp i stk (map OK ST)"
text {*
A call frame is correct, if stack and local variables conform, if the
types UnInit and PartInit are used consistently, if the {\tt this} pointer in
constructors is tagged correctly and its type is only used for the
{\tt this} pointer, if the @{term pc} is inside the method, and if
the number of local variables is correct.
*}
constdefs
correct_frame :: "[jvm_prog,aheap,init_heap,state_type,nat,bytecode]
\<Rightarrow> frame \<Rightarrow> bool"
"correct_frame G hp i == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc,r).
approx_stk G hp i stk ST \<and>
approx_loc G hp i loc LT \<and>
consistent_init stk loc (ST,LT) i \<and>
(fst sig = init \<longrightarrow>
corresponds stk loc (ST,LT) i (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and>
(i l = PartInit C \<or> (\<exists>C'. i l = Init (Class C'))))) \<and>
pc < length ins \<and>
length loc=length(snd sig)+maxl+1"
text {*
The reference update between constructors must be correct.
In this predicate,
\begin{description}
\item [a]
is the this pointer of the calling constructor (the reference to be
initialized), it must be of type UnInit or PartInit.
\item [b]
is the this pointer of the current constructor,
it must be partly initialized up to the current class.
\item [c]
is the fully initialized object it can be null (before super is
called), or must be a fully initialized object with type of the
original (calling) class (z from the BV is true iff c contains an
object)
\item [C]
is the class where the current constructor is declared
\end{description}
*}
constdefs
constructor_ok :: "[jvm_prog,aheap,init_heap,val,cname,bool,ref_upd] \<Rightarrow> bool"
"constructor_ok G hp ih a C z == \<lambda>(b,c).
z = (c \<noteq> Null) \<and> (\<exists>C' D pc l l' fs1 fs2. a = Addr l \<and> b = Addr l' \<and>
(ih l = UnInit C' pc \<or> ih l = PartInit D) \<and> hp l = Some (Obj C' fs1) \<and>
(ih l' = PartInit C \<or> ih l' = Init (Class C')) \<and> hp l' = Some (Obj C' fs2) \<and>
(c \<noteq> Null \<longrightarrow>
(\<exists>loc. c = Addr loc \<and> (\<exists>fs3. hp loc = Some (Obj C' fs3)) \<and> ih loc = Init (Class C'))))"
text {*
The whole call frame stack must be correct (the topmost frame is
handled separately)
*}
consts
correct_frames :: "[jvm_prog,aheap,init_heap,prog_type,ty,sig,
bool,ref_upd,frame list] \<Rightarrow> bool"
primrec
"correct_frames G hp i phi rT0 sig0 z r [] = True"
"correct_frames G hp i phi rT0 sig0 z0 r0 (f#frs) =
(let (stk,loc,C,sig,pc,r) = f in
(\<exists>ST LT z rT maxs maxl ins et.
((ST,LT),z) \<in> phi C sig ! pc \<and> is_class G C \<and>
method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
(\<exists>C' mn pTs. (ins!pc = Invoke C' mn pTs \<or> ins!pc = Invoke_special C' mn pTs) \<and>
(mn,pTs) = sig0 \<and>
(\<exists>apTs T ST'.
ST = (rev apTs) @ T # ST' \<and>
length apTs = length pTs \<and>
(\<exists>D' rT' body'. method (G,C') sig0 = Some(D',rT',body') \<and> G \<turnstile> rT0 \<preceq> rT') \<and>
(mn = init \<longrightarrow> constructor_ok G hp i (stk!length apTs) C' z0 r0) \<and>
correct_frame G hp i (ST, LT) maxl ins f \<and>
correct_frames G hp i phi rT sig z r frs))))"
text {*
Invariant for the whole program state:
*}
constdefs
correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
("_,_ |-JVM _ [ok]" [51,51] 50)
"correct_state G phi == \<lambda>(xp,hp,ihp,frs).
case xp of
None \<Rightarrow> (case frs of
[] \<Rightarrow> True
| (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> h_init G hp ihp \<and> preallocated hp ihp \<and>
(let (stk,loc,C,sig,pc,r) = f
in \<exists>rT maxs maxl ins et s z.
is_class G C \<and>
method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
(s,z) \<in> phi C sig ! pc \<and>
correct_frame G hp ihp s maxl ins f \<and>
correct_frames G hp ihp phi rT sig z r fs))
| Some x \<Rightarrow> frs = []"
syntax (xsymbols)
correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
lemma constructor_ok_field_update:
"\<lbrakk> constructor_ok G hp ihp x C' z r; hp a = Some (Obj C od) \<rbrakk>
\<Longrightarrow> constructor_ok G (hp(a\<mapsto>Obj C od')) ihp x C' z r"
apply (cases r)
apply (unfold constructor_ok_def)
apply (cases "\<exists>y. x = Addr y")
defer
apply simp
apply clarify
apply simp
apply (rule conjI)
apply clarsimp
apply blast
apply (rule impI)
apply (rule conjI)
apply clarsimp
apply blast
apply (rule impI)
apply (rule conjI)
apply blast
apply (rule impI, erule impE, assumption)
apply (elim exE conjE)
apply simp
apply (rule exI)
apply (rule conjI)
defer
apply (rule impI)
apply (rule conjI)
apply (rule refl)
apply blast
apply (rule impI)
apply simp
done
lemma constructor_ok_array_update:
"\<lbrakk> constructor_ok G hp ihp x C' z r; hp a = Some (Arr T l en) \<rbrakk>
\<Longrightarrow> constructor_ok G (hp(a\<mapsto>Arr T l en')) ihp x C' z r"
apply (cases r)
apply (unfold constructor_ok_def)
apply (cases "\<exists>y. x = Addr y")
defer
apply simp
apply clarify
apply simp
apply (rule conjI)
apply clarsimp
apply (rule impI)
apply (rule conjI)
apply clarsimp
apply (rule impI)
apply (rule conjI)
apply blast
apply (rule impI, erule impE, assumption)
apply (elim exE conjE)
apply simp
apply (rule exI)
apply (rule conjI)
defer
apply (rule impI)
apply (rule conjI)
apply (rule refl)
apply blast
apply auto
done
lemma constructor_ok_newref:
"\<lbrakk> hp x = None; constructor_ok G hp ihp v C' z r \<rbrakk>
\<Longrightarrow> constructor_ok G (hp(x\<mapsto>obj)) (ihp(x := T)) v C' z r"
apply (cases r)
apply (unfold constructor_ok_def)
apply clarify
apply (rule conjI)
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule impI)
apply (rule conjI)
apply clarsimp
apply (rule impI)
apply (rule conjI)
apply blast
apply (rule impI, erule impE, assumption)
apply (elim exE conjE)
apply (intro exI)
apply (rule conjI)
defer
apply (rule impI)
apply (rule conjI, assumption)
apply blast
apply clarsimp
done
lemma constructor_ok_pass_val:
"\<lbrakk> constructor_ok G hp ihp x C' True r;
constructor_ok G hp ihp v C z0 r0; x = fst r0 \<rbrakk>
\<Longrightarrow> constructor_ok G hp ihp v C True (x, snd r)"
apply (cases r, cases r0)
apply (unfold constructor_ok_def)
apply simp
apply (elim conjE exE)
apply simp
apply (erule disjE)
apply clarsimp
apply clarsimp
done
lemma is_init_default_val:
"is_init hp ihp (default_val T)"
apply (simp add: is_init_def)
apply (cases T)
apply (case_tac prim_ty)
apply auto
done
section {* approx-val *}
lemma iconf_widen:
"G,hp,ihp \<turnstile> xcp ::\<preceq>i T \<Longrightarrow> G \<turnstile> T \<preceq>i T' \<Longrightarrow> wf_prog wf_mb G
\<Longrightarrow> G,hp,ihp \<turnstile> xcp ::\<preceq>i T'"
apply (cases T')
apply (auto simp add: init_le_Init2 iconf_def elim: conf_widen)
done
lemma is_init [elim!]:
"G,hp,ihp \<turnstile> v ::\<preceq>i Init T \<Longrightarrow> is_init hp ihp v"
by (simp add: iconf_def)
lemma approx_val_Err:
"approx_val G hp ihp x Err"
by (simp add: approx_val_def)
lemma approx_val_Null:
"approx_val G hp ihp Null (OK (Init (RefT x)))"
by (auto simp add: approx_val_def iconf_def is_init_def)
lemma approx_val_widen:
"wf_prog wt G \<Longrightarrow> approx_val G hp ihp v (OK T) \<Longrightarrow> G \<turnstile> T \<preceq>i T'
\<Longrightarrow> approx_val G hp ihp v (OK T')"
by (unfold approx_val_def) (auto intro: iconf_widen)
lemma conf_notNone:
"G,hp \<turnstile> Addr loc ::\<preceq> ty \<Longrightarrow> hp loc \<noteq> None"
by (unfold conf_def) auto
lemma approx_val_imp_approx_val_sup_heap [rule_format]:
"approx_val G hp ihp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' ihp v at"
apply (simp add: approx_val_def iconf_def is_init_def
split: err.split init_ty.split)
apply (fast dest: conf_notNone elim: hextE intro: conf_hext)
done
lemma approx_val_heap_update:
"\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk>
\<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
by (cases v, auto simp add: obj_ty_def conf_def)
section {* approx-loc *}
lemma approx_loc_Cons [iff]:
"approx_loc G hp ihp (s#xs) (l#ls) =
(approx_val G hp ihp s l \<and> approx_loc G hp ihp xs ls)"
by (simp add: approx_loc_def)
lemma approx_loc_Nil [simp,intro!]:
"approx_loc G hp ihp [] []"
by (simp add: approx_loc_def)
lemma approx_loc_len [elim]:
"approx_loc G hp ihp loc LT \<Longrightarrow> length loc = length LT"
by (unfold approx_loc_def list_all2_def) simp
lemma approx_loc_replace_Err:
"approx_loc G hp ihp loc LT \<Longrightarrow> approx_loc G hp ihp loc (replace v Err LT)"
by (clarsimp simp add: approx_loc_def list_all2_conv_all_nth replace_def
approx_val_Err)
lemma assConv_approx_stk_imp_approx_loc [rule_format]:
"wf_prog wt G \<Longrightarrow> (\<forall>(t,t')\<in>set (zip tys_n ts). G \<turnstile> t \<preceq>i t')
\<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp ihp s tys_n \<longrightarrow>
approx_loc G hp ihp s (map OK ts)"
apply (unfold approx_stk_def approx_loc_def list_all2_def)
apply (clarsimp simp add: all_set_conv_all_nth)
apply (rule approx_val_widen)
apply auto
done
lemma approx_loc_imp_approx_loc_sup_heap:
"\<lbrakk> approx_loc G hp ihp lvars lt; hp \<le>| hp' \<rbrakk>
\<Longrightarrow> approx_loc G hp' ihp lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (auto intro: approx_val_imp_approx_val_sup_heap)
done
lemma approx_val_newref:
"h loc = None \<Longrightarrow>
approx_val G (h(loc\<mapsto>(Obj C fs))) (ih(loc:=UnInit C pc)) (Addr loc) (OK (UnInit C pc))"
by (auto simp add: approx_val_def iconf_def is_init_def intro: conf_obj_AddrI)
lemma approx_val_newref_false:
"\<lbrakk> h l = None; approx_val G h ih (Addr l) (OK T) \<rbrakk> \<Longrightarrow> False"
by (simp add: approx_val_def iconf_def conf_def
split: init_ty.split_asm ty.split_asm)
lemma approx_val_imp_approx_val_newref:
"\<lbrakk> approx_val G hp ihp v T; hp loc = None \<rbrakk>
\<Longrightarrow> approx_val G hp (ihp(loc:=X)) v T"
apply (cases "v = Addr loc")
apply (auto simp add: approx_val_def iconf_def is_init_def conf_def
split: err.split init_ty.split val.split)
apply (erule allE, erule disjE)
apply auto
done
lemma approx_loc_newref:
"\<lbrakk> approx_loc G hp ihp lvars lt; hp loc = None \<rbrakk>
\<Longrightarrow> approx_loc G hp (ihp(loc:=X)) lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (auto intro: approx_val_imp_approx_val_newref)
done
lemma approx_loc_newref_Err:
"\<lbrakk> approx_loc G hp ihp loc LT; hp l = None; i < length loc; loc!i=Addr l \<rbrakk>
\<Longrightarrow> LT!i = Err"
apply (cases "LT!i", simp)
apply (clarsimp simp add: approx_loc_def list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply (erule approx_val_newref_false)
apply simp
done
lemma approx_loc_newref_all_Err:
"\<lbrakk> approx_loc G hp ihp loc LT; hp l = None \<rbrakk>
\<Longrightarrow> list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT"
apply (simp only: list_all2_conv_all_nth)
apply (rule conjI)
apply (simp add: approx_loc_def list_all2_def)
apply clarify
apply (rule approx_loc_newref_Err, assumption+)
done
lemma approx_loc_imp_approx_loc_subst [rule_format]:
"\<forall>loc idx x X. (approx_loc G hp ihp loc LT) \<longrightarrow> (approx_val G hp ihp x X)
\<longrightarrow> (approx_loc G hp ihp (loc[idx:=x]) (LT[idx:=X]))"
apply (unfold approx_loc_def list_all2_def)
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
done
lemma approx_loc_Err [iff]:
"approx_loc G hp ihp (replicate n v) (replicate n Err)"
by (induct n) (auto simp add: approx_val_def)
lemmas [cong] = conj_cong
lemma approx_loc_append [rule_format]:
"\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow>
approx_loc G hp ihp (l1@l2) (L1@L2) =
(approx_loc G hp ihp l1 L1 \<and> approx_loc G hp ihp l2 L2)"
apply (unfold approx_loc_def list_all2_def)
apply simp
apply blast
done
lemmas [cong del] = conj_cong
lemma approx_val_Err_or_same:
"\<lbrakk> approx_val G hp ihp v (OK X); X = UnInit C pc \<or> X = PartInit D;
approx_val G hp ihp v X' \<rbrakk>
\<Longrightarrow> X' = Err \<or> X' = OK X"
apply (simp add: approx_val_def split: err.split_asm)
apply (erule disjE)
apply (clarsimp simp add: iconf_def is_init_def split: init_ty.split_asm)
apply (clarsimp simp add: iconf_def is_init_def split: init_ty.split_asm)
done
lemma approx_loc_replace:
"\<lbrakk> approx_loc G hp ihp loc LT; approx_val G hp ihp x' (OK X');
approx_val G hp ihp x (OK X);
X = UnInit C pc \<or> X = PartInit D; corr_loc loc LT ihp x X \<rbrakk>
\<Longrightarrow> approx_loc G hp ihp (replace x x' loc) (replace (OK X) (OK X') LT)"
apply (simp add: approx_loc_def corr_loc_def replace_def list_all2_conv_all_nth)
apply clarsimp
apply (erule allE, erule impE, assumption)+
apply simp
apply (drule approx_val_Err_or_same, assumption+)
apply (simp add: approx_val_Err)
done
section {* approx-stk *}
lemma list_all2_approx:
"\<And>s. list_all2 (approx_val G hp ihp) s (map OK S) =
list_all2 (iconf G hp ihp) s S"
apply (induct S)
apply (auto simp add: list_all2_Cons2 approx_val_def)
done
lemma list_all2_iconf_widen:
"wf_prog mb G \<Longrightarrow>
list_all2 (iconf G hp ihp) a b \<Longrightarrow>
list_all2 (\<lambda>x y. G \<turnstile> x \<preceq>i Init y) b c \<Longrightarrow>
list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T \<and> is_init hp ihp v) a c"
apply (rule list_all2_trans)
defer
apply assumption
apply assumption
apply (drule iconf_widen, assumption+)
apply (simp add: iconf_def)
done
lemma approx_stk_rev_lem:
"approx_stk G hp ihp (rev s) (rev t) = approx_stk G hp ihp s t"
apply (unfold approx_stk_def approx_loc_def list_all2_def)
apply (auto simp add: zip_rev sym [OF rev_map])
done
lemma approx_stk_rev:
"approx_stk G hp ihp (rev s) t = approx_stk G hp ihp s (rev t)"
by (auto intro: subst [OF approx_stk_rev_lem])
lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
"\<forall>lvars. approx_stk G hp ihp lvars lt \<longrightarrow> hp \<le>| hp'
\<longrightarrow> approx_stk G hp' ihp lvars lt"
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
lemma approx_stk_Nil [iff]:
"approx_stk G hp ihp [] []"
by (simp add: approx_stk_def approx_loc_def)
lemma approx_stk_Cons [iff]:
"approx_stk G hp ihp (x # stk) (S#ST) =
(approx_val G hp ihp x (OK S) \<and> approx_stk G hp ihp stk ST)"
by (simp add: approx_stk_def approx_loc_def)
lemma approx_stk_Cons_lemma [iff]:
"approx_stk G hp ihp stk (S#ST') =
(\<exists>s stk'. stk = s#stk' \<and> approx_val G hp ihp s (OK S) \<and>
approx_stk G hp ihp stk' ST')"
by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
lemma approx_stk_len [elim]:
"approx_stk G hp ihp stk ST \<Longrightarrow> length stk = length ST"
by (unfold approx_stk_def) (simp add: approx_loc_len)
lemma approx_stk_append_lemma:
"approx_stk G hp ihp stk (S@ST') \<Longrightarrow>
(\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and>
approx_stk G hp ihp s S \<and> approx_stk G hp ihp stk' ST')"
by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
lemma approx_stk_newref:
"\<lbrakk> approx_stk G hp ihp lvars lt; hp loc = None \<rbrakk>
\<Longrightarrow> approx_stk G hp (ihp(loc:=X)) lvars lt"
by (auto simp add: approx_stk_def intro: approx_loc_newref)
lemma newref_notin_stk:
"\<lbrakk> approx_stk G hp ihp stk ST; hp l = None \<rbrakk>
\<Longrightarrow> Addr l \<notin> set stk"
proof
assume "Addr l \<in> set stk"
then obtain a b where
stk: "stk = a @ (Addr l) # b"
by (clarsimp simp add: in_set_conv_decomp)
hence "stk!(length a) = Addr l" by (simp add: nth_append)
with stk obtain i where
"stk!i = Addr l" and i: "i < length stk" by clarsimp
moreover
assume "approx_stk G hp ihp stk ST"
hence l: "approx_loc G hp ihp stk (map OK ST)" by (unfold approx_stk_def)
moreover
assume "hp l = None"
moreover
from l
have "length stk = length ST" by (simp add: approx_loc_def list_all2_def)
with i
have "map OK ST ! i \<noteq> Err" by simp
ultimately
show False by (auto dest: approx_loc_newref_Err)
qed
section "corresponds"
lemma corr_loc_empty [simp]:
"corr_loc [] [] ihp v T"
by (simp add: corr_loc_def)
lemma corr_loc_cons:
"corr_loc (s#loc) (L#LT) ihp v T =
((L = OK T \<longrightarrow> s = v \<and> corr_val v T ihp) \<and> corr_loc loc LT ihp v T)"
by (simp add: corr_loc_def)
lemma corr_loc_start:
"\<And>loc.
\<lbrakk> \<forall>x \<in> set LT. x = Err \<or> (\<exists>t. x = OK (Init t));
length loc = length LT; T = UnInit C pc \<or> T = PartInit C'\<rbrakk>
\<Longrightarrow> corr_loc loc LT ihp v T" (is "PROP ?P LT")
proof (induct LT)
show "PROP ?P []" by (simp add: corr_loc_def)
fix L LS assume IH: "PROP ?P LS"
show "PROP ?P (L#LS)"
proof -
fix loc::"val list"
assume "length loc = length (L # LS)"
then obtain l ls where
loc: "loc = l#ls" and len:"length ls = length LS"
by (auto simp add: length_Suc_conv)
assume "\<forall>x\<in>set (L#LS). x = Err \<or> (\<exists>t. x = OK (Init t))"
then obtain
first: "L = Err \<or> (\<exists>t. L = OK (Init t))" and
rest: "\<forall>x\<in>set LS. x = Err \<or> (\<exists>t. x = OK (Init t))"
by auto
assume T: "T = UnInit C pc \<or> T = PartInit C'"
with rest len IH
have "corr_loc ls LS ihp v T" by blast
with T first
have "corr_loc (l#ls) (L # LS) ihp v T"
by (clarsimp simp add: corr_loc_def)
with loc
show "corr_loc loc (L # LS) ihp v T" by simp
qed
qed
lemma consistent_init_start:
"\<lbrakk> LT0 = OK (Init (Class C)) # map OK (map Init pTs) @ replicate mxl' Err;
loc = (oX # rev opTs @ replicate mxl' arbitrary);
length pTs = length opTs \<rbrakk>
\<Longrightarrow> consistent_init [] loc ([], LT0) ihp"
(is "\<lbrakk> PROP ?LT0; PROP ?loc; PROP _ \<rbrakk> \<Longrightarrow> PROP _")
proof -
assume LT0: "PROP ?LT0" and "PROP ?loc" "length pTs = length opTs"
hence len: "length loc = length LT0" by simp
from LT0 have no_UnInit: "\<forall>x \<in> set LT0. x = Err \<or> (\<exists>t. x = OK (Init t))"
by (auto dest: in_set_replicateD)
with len show ?thesis
by (simp add: consistent_init_def corresponds_def corr_stk_def)
(blast intro: corr_loc_start)
qed
lemma corresponds_stk_cons:
"corresponds (s#stk) loc (S#ST,LT) ihp v T =
((S = T \<longrightarrow> s = v \<and> corr_val v T ihp) \<and> corresponds stk loc (ST,LT) ihp v T)"
by (simp add: corresponds_def corr_stk_def corr_loc_def)
lemma corresponds_loc_nth:
"\<lbrakk> corresponds stk loc (ST,LT) ihp v T; n < length LT; LT!n = OK X \<rbrakk> \<Longrightarrow>
X = T \<longrightarrow> (loc!n) = v \<and> corr_val v T ihp"
by (simp add: corresponds_def corr_loc_def list_all2_conv_all_nth)
lemma consistent_init_loc_nth:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp; n < length LT; LT!n = OK X \<rbrakk>
\<Longrightarrow> consistent_init (loc!n#stk) loc (X#ST,LT) ihp"
apply (simp add: consistent_init_def corresponds_stk_cons)
apply (intro strip conjI)
apply (elim allE exE conjE)
apply (intro exI conjI corresponds_loc_nth)
apply assumption+
apply (elim allE exE conjE)
apply (intro exI conjI corresponds_loc_nth)
apply assumption+
done
lemma consistent_init_corresponds_stk_cons:
"\<lbrakk> consistent_init (s#stk) loc (S#ST,LT) ihp;
S = UnInit C pc \<or> S = PartInit C' \<rbrakk>
\<Longrightarrow> corresponds (s#stk) loc (S#ST, LT) ihp s S"
by (simp add: consistent_init_def corresponds_stk_cons) blast
lemma consistent_init_corresponds_loc:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp; LT!n = OK T;
T = UnInit C pc \<or> T = PartInit C'; n < length LT \<rbrakk>
\<Longrightarrow> corresponds stk loc (ST,LT) ihp (loc!n) T"
proof -
assume "consistent_init stk loc (ST,LT) ihp"
"T = UnInit C pc \<or> T = PartInit C'"
then obtain v where
corr: "corresponds stk loc (ST,LT) ihp v T"
by (simp add: consistent_init_def) blast
moreover
assume "LT!n = OK T" "n < length LT"
ultimately
have "v = (loc!n)" by (simp add: corresponds_loc_nth)
with corr
show ?thesis by simp
qed
lemma consistent_init_pop:
"consistent_init (s#stk) loc (S#ST,LT) ihp
\<Longrightarrow> consistent_init stk loc (ST,LT) ihp"
by (simp add: consistent_init_def corresponds_stk_cons) fast
lemma consistent_init_Init_stk:
"consistent_init stk loc (ST,LT) ihp \<Longrightarrow>
consistent_init (s#stk) loc ((Init T')#ST,LT) ihp"
by (simp add: consistent_init_def corresponds_def corr_stk_def corr_loc_def)
lemma corr_loc_set:
"\<lbrakk> corr_loc loc LT ihp v T; OK T \<in> set LT \<rbrakk> \<Longrightarrow> corr_val v T ihp"
by (auto simp add: corr_loc_def in_set_conv_decomp list_all2_append2
list_all2_Cons2)
lemma corresponds_var_upd_UnInit:
"\<lbrakk> corresponds stk loc (ST,LT) ihp v T; n < length LT;
OK T \<in> set (map OK ST) \<union> set LT \<rbrakk>
\<Longrightarrow> corresponds stk (loc[n:= v]) (ST,LT[n:= OK T]) ihp v T"
proof -
assume "corresponds stk loc (ST,LT) ihp v T"
then obtain
stk: "corr_stk stk ST ihp v T" and
loc: "corr_loc loc LT ihp v T"
by (simp add: corresponds_def)
from loc
obtain
len: "length loc = length LT" and
"\<forall>i. i < length loc \<longrightarrow> LT ! i = OK T \<longrightarrow> loc ! i = v \<and> corr_val v T ihp"
(is "?all loc LT")
by (simp add: corr_loc_def list_all2_conv_all_nth)
moreover
assume "OK T \<in> set (map OK ST) \<union> set LT"
hence ihp: "corr_val v T ihp"
proof
assume "OK T \<in> set LT"
with loc show ?thesis by (rule corr_loc_set)
next
assume "OK T \<in> set (map OK ST)"
with stk show ?thesis by (unfold corr_stk_def) (rule corr_loc_set)
qed
moreover
assume "n < length LT"
ultimately
have "?all (loc[n:= v]) (LT[n:= OK T])"
by (simp add: nth_list_update)
with len
have "corr_loc (loc[n:= v]) (LT[n:= OK T]) ihp v T"
by (simp add: corr_loc_def list_all2_conv_all_nth)
with stk
show ?thesis
by (simp add: corresponds_def)
qed
lemma corresponds_var_upd_UnInit2:
"\<lbrakk> corresponds stk loc (ST,LT) ihp v T; n < length LT; T' \<noteq> T \<rbrakk>
\<Longrightarrow> corresponds stk (loc[n:= v']) (ST,LT[n:= OK T']) ihp v T"
by (auto simp add: corresponds_def corr_loc_def
list_all2_conv_all_nth nth_list_update)
lemma corresponds_var_upd:
"\<lbrakk> corresponds (s#stk) loc (S#ST, LT) ihp v T; idx < length LT \<rbrakk>
\<Longrightarrow> corresponds stk (loc[idx := s]) (ST, LT[idx := OK S]) ihp v T"
apply (cases "S = T")
apply (drule corresponds_var_upd_UnInit, assumption)
apply simp
apply (simp only: corresponds_stk_cons)
apply (drule corresponds_var_upd_UnInit2, assumption+)
apply (simp only: corresponds_stk_cons)
apply blast
done
lemma consistent_init_conv:
"consistent_init stk loc s ihp =
(\<forall>T. ((\<exists>C pc. T = UnInit C pc) \<or> (\<exists>C. T = PartInit C)) \<longrightarrow>
(\<exists>v. corresponds stk loc s ihp v T))"
by (unfold consistent_init_def) blast
lemma consistent_init_store:
"\<lbrakk> consistent_init (s#stk) loc (S#ST,LT) ihp; n < length LT \<rbrakk>
\<Longrightarrow> consistent_init stk (loc[n:= s]) (ST,LT[n:= OK S]) ihp"
apply (simp only: consistent_init_conv)
apply (blast intro: corresponds_var_upd)
done
lemma corr_loc_newT:
"\<lbrakk> OK T \<notin> set LT; length loc = length LT \<rbrakk> \<Longrightarrow> corr_loc loc LT ihp v T"
by (auto dest: nth_mem simp add: corr_loc_def list_all2_conv_all_nth)
lemma corr_loc_new_val:
"\<lbrakk> corr_loc loc LT ihp v T; Addr l \<notin> set loc \<rbrakk>
\<Longrightarrow> corr_loc loc LT (ihp(l:= T')) v T"
proof -
assume new: "Addr l \<notin> set loc"
assume "corr_loc loc LT ihp v T"
then obtain
len: "length loc = length LT" and
all: "\<forall>i. i < length loc \<longrightarrow> LT ! i = OK T \<longrightarrow> loc ! i = v \<and> corr_val v T ihp"
by (simp add: corr_loc_def list_all2_conv_all_nth)
show ?thesis
proof (unfold corr_loc_def, simp only: list_all2_conv_all_nth,
intro strip conjI)
from len show "length loc = length LT" .
fix i assume i: "i < length loc" and "LT!i = OK T"
with all
have l: "loc!i = v \<and> corr_val v T ihp" by blast
thus "loc!i = v" by blast
from i l new
have "v \<noteq> Addr l" by (auto dest: nth_mem)
with l
show "corr_val v T (ihp(l:= T'))"
by (auto simp add: corr_val_def split: init_ty.split)
qed
qed
lemma corr_loc_Err_val:
"\<lbrakk> corr_loc loc LT ihp v T; list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT \<rbrakk>
\<Longrightarrow> corr_loc loc LT (ihp(l:= T')) v T"
apply (simp add: corr_loc_def);
apply (simp only: list_all2_conv_all_nth)
apply clarify
apply (simp (no_asm))
apply clarify
apply (erule_tac x = i in allE, erule impE)
apply simp
apply (erule impE, assumption)
apply simp
apply (unfold corr_val_def)
apply (elim conjE exE)
apply (rule_tac x = la in exI)
apply clarsimp
done
lemma corr_loc_len:
"corr_loc loc LT ihp v T \<Longrightarrow> length loc = length LT"
by (simp add: corr_loc_def list_all2_conv_all_nth)
lemma corresponds_newT:
"\<lbrakk> corresponds stk loc (ST,LT) ihp' v' T'; OK T \<notin> set (map OK ST) \<union> set LT \<rbrakk>
\<Longrightarrow> corresponds stk loc (ST,LT) ihp v T"
apply (clarsimp simp add: corresponds_def corr_stk_def)
apply (rule conjI)
apply (rule corr_loc_newT, simp)
apply (simp add: corr_loc_len)
apply (rule corr_loc_newT, assumption)
apply (simp add: corr_loc_len)
done
lemma corresponds_new_val:
"\<lbrakk> corresponds stk loc (ST,LT) ihp v T; Addr l \<notin> set stk;
list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT \<rbrakk>
\<Longrightarrow> corresponds stk loc (ST,LT) (ihp(l:= T')) v T"
apply (simp add: corresponds_def corr_stk_def)
apply (blast intro: corr_loc_new_val corr_loc_Err_val)
done
lemma corresponds_newref:
"\<lbrakk> corresponds stk loc (ST, LT) ihp v T;
OK (UnInit C pc) \<notin> set (map OK ST) \<union> set LT;
Addr l \<notin> set stk; list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT \<rbrakk>
\<Longrightarrow> \<exists>v. corresponds (Addr l#stk) loc ((UnInit C pc)#ST,LT)
(ihp(l:= UnInit C pc)) v T"
apply (simp add: corresponds_stk_cons)
apply (cases "T = UnInit C pc")
apply simp
apply (rule conjI)
apply (unfold corr_val_def)
apply simp
apply (rule corresponds_newT, assumption)
apply simp
apply (blast intro: corresponds_new_val)
done
lemma consistent_init_new_val_lemma:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp;
Addr l \<notin> set stk; list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT \<rbrakk>
\<Longrightarrow> consistent_init stk loc (ST,LT) (ihp(l:= T'))"
by (unfold consistent_init_def) (blast intro: corresponds_new_val)
lemma consistent_init_newref_lemma:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp;
OK (UnInit C pc) \<notin> set (map OK ST) \<union> set LT;
Addr l \<notin> set stk; list_all2 (\<lambda>v T. v = Addr l \<longrightarrow> T = Err) loc LT \<rbrakk>
\<Longrightarrow> consistent_init (Addr l#stk) loc ((UnInit C pc)#ST,LT) (ihp(l:= UnInit C pc))"
by (unfold consistent_init_def) (blast intro: corresponds_newref)
lemma consistent_init_newref:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp;
approx_loc G hp ihp loc LT;
hp l = None;
approx_stk G hp ihp stk ST;
OK (UnInit C pc) \<notin> set (map OK ST) \<union> set LT \<rbrakk>
\<Longrightarrow> consistent_init (Addr l#stk) loc ((UnInit C pc)#ST,LT) (ihp(l:= UnInit C pc))"
apply (drule approx_loc_newref_all_Err, assumption)
apply (drule newref_notin_stk, assumption)
apply (rule consistent_init_newref_lemma)
apply assumption+
done
lemma corresponds_new_val2:
"\<lbrakk>corresponds stk loc (ST, LT) ihp v T; approx_loc G hp ihp loc LT; hp l = None;
approx_stk G hp ihp stk ST\<rbrakk>
\<Longrightarrow> corresponds stk loc (ST, LT) (ihp(l := T')) v T"
apply (drule approx_loc_newref_all_Err, assumption)
apply (drule newref_notin_stk, assumption)
apply (rule corresponds_new_val)
apply assumption+
done
lemma consistent_init_new_val:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp;
approx_loc G hp ihp loc LT; hp l = None;
approx_stk G hp ihp stk ST \<rbrakk>
\<Longrightarrow> consistent_init stk loc (ST,LT) (ihp(l:= T'))"
apply (drule approx_loc_newref_all_Err, assumption)
apply (drule newref_notin_stk, assumption)
apply (rule consistent_init_new_val_lemma)
apply assumption+
done
lemma corr_loc_replace_type:
"\<lbrakk> corr_loc loc LT ihp v T; T \<noteq> (Init T'') \<rbrakk>
\<Longrightarrow> corr_loc loc (replace (OK T') (OK (Init T'')) LT) ihp v T"
apply (unfold corr_loc_def replace_def)
apply (simp add: list_all2_conv_all_nth)
apply blast
done
lemma corr_stk_replace_type:
"\<lbrakk> corr_stk loc ST ihp v T; T \<noteq> (Init T'') \<rbrakk>
\<Longrightarrow> corr_stk loc (replace T' (Init T'') ST) ihp v T"
proof -
assume "corr_stk loc ST ihp v T"
hence "corr_loc loc (map OK ST) ihp v T" by (unfold corr_stk_def)
moreover
assume "T \<noteq> (Init T'')"
ultimately
have "corr_loc loc (replace (OK T') (OK (Init T'')) (map OK ST)) ihp v T"
by (rule corr_loc_replace_type)
moreover
have "replace (OK T') (OK (Init T'')) (map OK ST) =
map OK (replace T' (Init T'') ST)"
by (rule replace_map_OK)
ultimately
have "corr_loc loc (map OK (replace T' (Init T'') ST)) ihp v T" by simp
thus ?thesis by (unfold corr_stk_def)
qed
lemma consistent_init_replace_type:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp \<rbrakk>
\<Longrightarrow> consistent_init stk loc
(replace T (Init T') ST, replace (OK T) (OK (Init T')) LT) ihp"
apply (unfold consistent_init_def corresponds_def)
apply simp
apply (blast intro: corr_stk_replace_type corr_loc_replace_type)
done
lemma corr_loc_replace:
"\<And>loc.
\<lbrakk> corr_loc loc LT ihp v T; approx_loc G hp ihp loc LT;
approx_val G hp ihp oX (OK T0); T \<noteq> T'; T = UnInit C pc \<or> T = PartInit D \<rbrakk>
\<Longrightarrow> corr_loc (replace oX x loc) (replace (OK T0) (OK T') LT) ihp v T"
apply (frule corr_loc_len)
apply (induct LT)
apply (simp add: replace_def)
apply (clarsimp simp add: length_Suc_conv)
apply (clarsimp simp add: corr_loc_cons replace_Cons split del: split_if)
apply (simp split: split_if_asm)
apply clarify
apply (drule approx_val_Err_or_same, assumption+)
apply simp
done
lemma corr_stk_replace:
"\<lbrakk> corr_stk stk ST ihp v T; approx_stk G hp ihp stk ST;
approx_val G hp ihp oX (OK T0); T \<noteq> T';
T = UnInit C pc \<or> T = PartInit D \<rbrakk>
\<Longrightarrow> corr_stk (replace oX x stk) (replace T0 T' ST) ihp v T"
apply (unfold corr_stk_def approx_stk_def)
apply (drule corr_loc_replace, assumption+)
apply (simp add: replace_map_OK)
done
lemma corresponds_replace:
"\<lbrakk> corresponds stk loc (ST,LT) ihp v T;
approx_loc G hp ihp loc LT;
approx_stk G hp ihp stk ST;
approx_val G hp ihp oX (OK T0);
T \<noteq> T'; T = UnInit C pc \<or> T = PartInit D \<rbrakk>
\<Longrightarrow> corresponds (replace oX x stk) (replace oX x loc)
(replace T0 T' ST, replace (OK T0) (OK T') LT) ihp v T"
apply (clarsimp simp add: corresponds_def)
apply (rule conjI)
apply (rule corr_stk_replace)
apply assumption+
apply (rule corr_loc_replace)
apply assumption+
done
lemma consisten_init_replace:
"\<lbrakk> consistent_init stk loc (ST,LT) ihp;
approx_loc G hp ihp loc LT;
approx_stk G hp ihp stk ST;
approx_val G hp ihp oX (OK T0);
T' = Init C' \<rbrakk>
\<Longrightarrow> consistent_init (replace oX x stk) (replace oX x loc)
(replace T0 T' ST, replace (OK T0) (OK T') LT) ihp"
apply (simp only: consistent_init_conv)
apply clarify apply (blast intro: corresponds_replace)
done
lemma corr_loc_replace_Err:
"corr_loc loc LT ihp v T \<Longrightarrow> corr_loc loc (replace T' Err LT) ihp v T"
by (simp add: corr_loc_def list_all2_conv_all_nth replace_def)
lemma corresponds_replace_Err:
"corresponds stk loc (ST, LT) ihp v T
\<Longrightarrow> corresponds stk loc (ST, replace T' Err LT) ihp v T"
by (simp add: corresponds_def corr_loc_replace_Err)
lemma consistent_init_replace_Err:
"consistent_init stk loc (ST, LT) ihp
\<Longrightarrow> consistent_init stk loc (ST, replace T' Err LT) ihp"
by (unfold consistent_init_def, blast intro: corresponds_replace_Err)
lemma corresponds_append:
"\<And>X. \<lbrakk> corresponds (x@stk) loc (X@ST,LT) ihp v T; length X = length x \<rbrakk>
\<Longrightarrow> corresponds stk loc (ST,LT) ihp v T"
apply (induct x)
apply simp
apply (clarsimp simp add: length_Suc_conv)
apply (simp add: corresponds_stk_cons)
apply blast
done
lemma consistent_init_append:
"\<And>X. \<lbrakk> consistent_init (x@stk) loc (X@ST,LT) ihp; length X = length x \<rbrakk>
\<Longrightarrow> consistent_init stk loc (ST,LT) ihp"
apply (induct x)
apply simp
apply (clarsimp simp add: length_Suc_conv)
apply (drule consistent_init_pop)
apply blast
done
lemma corresponds_xcp:
"corresponds stk loc (ST, LT) ihp v T \<Longrightarrow> T = UnInit C pc \<or> T = PartInit D
\<Longrightarrow> corresponds [x] loc ([Init X], LT) ihp v T"
apply (simp add: corresponds_def corr_stk_def corr_loc_def)
apply blast
done
lemma consistent_init_xcp:
"consistent_init stk loc (ST,LT) ihp
\<Longrightarrow> consistent_init [x] loc ([Init X], LT) ihp"
apply (unfold consistent_init_def)
apply (blast intro: corresponds_xcp)
done
lemma corresponds_pop:
"corresponds (s#stk) loc (S#ST,LT) ihp v T
\<Longrightarrow> corresponds stk loc (ST,LT) ihp v T"
by (simp add: corresponds_stk_cons)
lemma consistent_init_Dup:
"consistent_init (s#stk) loc (S#ST,LT) ihp
\<Longrightarrow> consistent_init (s#s#stk) loc (S#S#ST,LT) ihp"
apply (simp only: consistent_init_conv)
apply clarify
apply (simp add: corresponds_stk_cons)
apply blast
done
lemma corresponds_Dup:
"corresponds (s#stk) loc (S#ST,LT) ihp v T
\<Longrightarrow> corresponds (s#s#stk) loc (S#S#ST,LT) ihp v T"
by (simp add: corresponds_stk_cons)
lemma corresponds_Dup_x1:
"corresponds (s1#s2#stk) loc (S1#S2#ST,LT) ihp v T
\<Longrightarrow> corresponds (s1#s2#s1#stk) loc (S1#S2#S1#ST,LT) ihp v T"
by (simp add: corresponds_stk_cons)
lemma consistent_init_Dup_x1:
"consistent_init (s1#s2#stk) loc (S1#S2#ST,LT) ihp
\<Longrightarrow> consistent_init (s1#s2#s1#stk) loc (S1#S2#S1#ST,LT) ihp"
by (unfold consistent_init_def, blast intro: corresponds_Dup_x1)
lemma corresponds_Dup_x2:
"corresponds (s1#s2#s3#stk) loc (S1#S2#S3#ST,LT) ihp v T
\<Longrightarrow> corresponds (s1#s2#s3#s1#stk) loc (S1#S2#S3#S1#ST,LT) ihp v T"
by (simp add: corresponds_stk_cons)
lemma consistent_init_Dup_x2:
"consistent_init (s1#s2#s3#stk) loc (S1#S2#S3#ST,LT) ihp
\<Longrightarrow> consistent_init (s1#s2#s3#s1#stk) loc (S1#S2#S3#S1#ST,LT) ihp"
by (unfold consistent_init_def, blast intro: corresponds_Dup_x2)
lemma corresponds_Swap:
"corresponds (s1#s2#stk) loc (S1#S2#ST,LT) ihp v T
\<Longrightarrow> corresponds (s2#s1#stk) loc (S2#S1#ST,LT) ihp v T"
by (simp add: corresponds_stk_cons)
lemma consistent_init_Swap:
"consistent_init (s1#s2#stk) loc (S1#S2#ST,LT) ihp
\<Longrightarrow> consistent_init (s2#s1#stk) loc (S2#S1#ST,LT) ihp"
by (unfold consistent_init_def, blast intro: corresponds_Swap)
section "oconf"
lemma oconf_blank:
"\<lbrakk> is_class G D; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> G,hp \<turnstile> blank G D \<surd>"
by (auto simp add: oconf_def blank_def dest: fields_is_type)
lemma oconf_field_update:
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(Obj oT fs)\<surd> \<rbrakk>
\<Longrightarrow> G,hp\<turnstile> Obj oT (fs(FD\<mapsto>v)) \<surd>"
by (simp add: oconf_def lconf_def)
lemma oconf_imp_oconf_heap_newref [rule_format]:
"\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>"
apply (unfold oconf_def lconf_def)
apply (simp split: heap_entry.splits)
apply (fast intro: conf_hext hext_new)+
done
lemma oconf_imp_oconf_heap_update [rule_format]:
"hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd>
\<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
apply (simp split: heap_entry.splits)
apply (force intro: approx_val_heap_update)
done
section "hconf"
lemma hconf_imp_hconf_newref [rule_format]:
"hp oref = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
apply (simp add: hconf_def)
apply (fast intro: oconf_imp_oconf_heap_newref)
done
lemma hconf_imp_hconf_field_update [rule_format]:
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some (Obj oT fs) \<and>
G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> Obj oT (fs((F,D)\<mapsto>v)))\<surd>"
apply (simp add: hconf_def)
apply (force intro: oconf_imp_oconf_heap_update oconf_field_update
simp add: obj_ty_def)
done
section "h-init"
lemma h_init_field_update:
"\<lbrakk> h_init G hp ihp; hp x = Some (Obj C fs); is_init hp ihp v \<rbrakk>
\<Longrightarrow> h_init G (hp(x\<mapsto>Obj C (fs(X\<mapsto>v)))) ihp"
apply (unfold h_init_def o_init_def l_init_def)
apply clarsimp
apply (rule conjI)
apply clarify
apply (rule conjI)
apply (clarsimp simp add: is_init_def)
apply clarsimp
apply (elim allE, erule impE, assumption)
apply clarsimp
apply (elim allE,
erule impE, rule exI, assumption)
apply (clarsimp simp add: is_init_def)
apply (clarsimp split: heap_entry.split)
apply (rule conjI)
apply clarify
apply (elim allE, erule impE, assumption, simp,
elim allE,
erule impE, rule exI, assumption)
apply (clarsimp simp add: is_init_def)
apply clarify
apply (elim allE, erule impE, assumption) back
apply simp
apply (erule allE, erule impE, simp)
apply (clarsimp simp add: is_init_def)
done
lemma oconf_arrD:
"\<lbrakk>G,h \<turnstile> Arr T len en \<surd>; n < len\<rbrakk>
\<Longrightarrow> \<exists>v. en n = Some v \<and> G,h \<turnstile> v ::\<preceq> T"
by (unfold oconf_def) simp
lemma h_init_newref:
"\<lbrakk> hp r = None; G \<turnstile>h hp \<surd>; h_init G hp ihp \<rbrakk>
\<Longrightarrow> h_init G (hp(r\<mapsto>blank G X)) (ihp(r := T'))"
apply (unfold h_init_def o_init_def l_init_def blank_def)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (simp add: init_vars_def map_of_map)
apply (rule is_init_default_val)
apply (clarsimp split: heap_entry.split)
apply (rule conjI)
apply clarify
apply (elim allE, erule impE, assumption)
apply simp
apply (elim allE, erule impE)
apply fastsimp
apply clarsimp
apply (simp add: is_init_def)
apply (drule hconfD, assumption)
apply (drule oconf_objD, assumption)
apply clarsimp
apply (drule new_locD, assumption)
apply simp
apply clarify
apply (elim allE, erule impE, assumption)
apply simp
apply (elim allE, erule impE)
apply fastsimp
apply clarsimp
apply (simp add: is_init_def)
apply (drule hconfD, assumption)
apply (drule oconf_arrD, assumption)
apply clarsimp
apply (drule new_locD, assumption)
apply simp
done
section {* preallocated *}
lemma preallocated_field_update:
"\<lbrakk> hp a = Some (Obj oT fs); G\<turnstile>h hp\<surd>; preallocated hp ihp \<rbrakk>
\<Longrightarrow> preallocated (hp(a \<mapsto> Obj oT fs')) ihp"
apply (unfold preallocated_def)
apply (rule allI)
apply (erule_tac x=x in allE)
apply (simp add: is_init_def)
apply (rule ccontr)
apply (unfold hconf_def)
apply (erule allE, erule allE, erule impE, assumption)
apply (unfold oconf_def lconf_def)
apply (simp del: split_paired_All)
done
lemma preallocated_array_update:
"\<lbrakk> hp a = Some (Arr T l en);
G\<turnstile>h hp\<surd>; preallocated hp ihp \<rbrakk>
\<Longrightarrow> preallocated (hp(a \<mapsto> Arr T l en')) ihp"
apply (unfold preallocated_def)
apply (rule allI)
apply (erule_tac x=x in allE)
apply (simp add: is_init_def)
apply (rule ccontr)
apply (unfold hconf_def)
apply (erule allE, erule allE, erule impE, assumption)
apply (unfold oconf_def lconf_def)
apply (simp del: split_paired_All)
done
lemma preallocated_newref:
assumes none: "hp oref = None" and alloc: "preallocated hp ihp"
shows "preallocated (hp(oref\<mapsto>obj)) (ihp(oref:=T)) "
proof (cases oref)
case (XcptRef x)
with none alloc have "False" by (auto elim: preallocatedE [of _ _ x])
thus ?thesis ..
next
case (Loc l)
with alloc show ?thesis by (simp add: preallocated_def is_init_def)
qed
section "constructor-ok"
lemma correct_frames_ctor_ok:
"correct_frames G hp ihp phi rT sig z r frs
\<Longrightarrow> frs = [] \<or> (fst sig = init \<longrightarrow> (\<exists>a C'. constructor_ok G hp ihp a C' z r))"
apply (cases frs)
apply simp
apply simp
apply clarify
apply simp
apply blast
done
section "correct-frame"
lemma correct_frameE [elim?]:
"correct_frame G hp ihp (ST,LT) maxl ins (stk, loc, C, sig, pc, r) \<Longrightarrow>
(\<lbrakk>approx_stk G hp ihp stk ST; approx_loc G hp ihp loc LT;
consistent_init stk loc (ST, LT) ihp;
fst sig = init \<longrightarrow>
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))));
pc < length ins; length loc = length (snd sig) + maxl + 1\<rbrakk>
\<Longrightarrow> P)
\<Longrightarrow> P"
apply (unfold correct_frame_def)
apply fast
done
section {* correct-frames *}
lemmas [simp del] = fun_upd_apply
lemmas [split del] = split_if
lemma correct_frames_imp_correct_frames_field_update [rule_format]:
"\<forall>rT C sig z r. correct_frames G hp ihp phi rT sig z r frs \<longrightarrow>
hp a = Some (Obj C od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v::\<preceq>fd \<longrightarrow>
correct_frames G (hp(a \<mapsto> Obj C (od(fl\<mapsto>v)))) ihp phi rT sig z r frs"
apply (induct frs)
apply simp
apply clarify
apply simp
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
apply clarify
apply (intro exI conjI)
apply assumption
apply assumption+
apply (rule refl)
apply assumption+
apply (rule impI)
apply (rule constructor_ok_field_update)
apply (erule impE, assumption)
apply simp
apply assumption
apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
apply (rule hext_upd_obj, assumption)
apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
apply (rule hext_upd_obj, assumption)
apply assumption+
apply (rule impI)
apply (erule impE, assumption, erule conjE)
apply (rule conjI)
apply assumption
apply (elim exE conjE)
apply (rule exI)
apply (rule conjI)
apply assumption
apply (rule conjI)
apply (simp add: fun_upd_apply)
apply (case_tac "l = a")
apply simp
apply simp
apply assumption+
apply blast
done
lemma correct_frames_array_update [rule_format]:
"\<forall>rT C sig z r. correct_frames G hp ihp phi rT sig z r frs \<longrightarrow>
hp a = Some (Arr T l en) \<longrightarrow>
G,hp\<turnstile>v::\<preceq>fd \<longrightarrow>
correct_frames G (hp(a \<mapsto> Arr T l en')) ihp phi rT sig z r frs"
apply (induct frs)
apply simp
apply clarify
apply simp
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
apply clarify
apply (intro exI conjI)
apply assumption
apply assumption+
apply (rule refl)
apply assumption+
apply (rule impI)
apply (rule constructor_ok_array_update)
apply (erule impE, assumption)
apply simp
apply assumption
apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
apply (rule hext_upd_arr, assumption)
apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
apply (rule hext_upd_arr, assumption)
apply assumption+
apply (rule impI)
apply (erule impE, assumption, erule conjE)
apply (rule conjI)
apply assumption
apply (elim exE conjE)
apply (rule exI)
apply (rule conjI)
apply assumption
apply (rule conjI)
apply (simp add: fun_upd_apply)
apply (case_tac "la = a")
apply simp
apply simp
apply assumption+
apply blast
done
lemma correct_frames_imp_correct_frames_newref [rule_format]:
"\<forall>rT sig z r. hp x = None \<longrightarrow> correct_frames G hp ihp phi rT sig z r frs
\<longrightarrow> correct_frames G (hp(x\<mapsto>obj)) (ihp(x:=T)) phi rT sig z r frs"
apply (induct frs)
apply simp
apply clarify
apply simp
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
apply clarify
apply (intro exI conjI)
apply assumption+
apply (rule refl)
apply assumption+
apply (rule impI)
apply (erule impE, assumption)
apply (rule constructor_ok_newref, assumption)
apply simp
apply (drule approx_stk_newref, assumption)
apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
apply (rule hext_new, assumption)
apply (drule approx_loc_newref, assumption)
apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
apply (rule hext_new, assumption)
apply (rule consistent_init_new_val, assumption+)
apply (rule impI, erule impE, assumption, erule conjE)
apply (rule conjI)
apply (rule corresponds_new_val2, assumption+)
apply (elim conjE exE)
apply (simp add: fun_upd_apply)
apply (case_tac "l = x")
apply simp
apply simp
apply assumption+
apply blast
done
lemmas [simp add] = fun_upd_apply
lemmas [split add] = split_if
section "correct-state"
lemma correct_stateE [elim?]:
"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<Longrightarrow>
(\<And>rT maxs maxl ins et ST LT z.
\<lbrakk>G \<turnstile>h hp \<surd>; h_init G hp ihp; preallocated hp ihp; is_class G C; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
((ST,LT), z) \<in> phi C sig ! pc; correct_frame G hp ihp (ST,LT) maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs\<rbrakk> \<Longrightarrow> P)
\<Longrightarrow> P"
apply (unfold correct_state_def)
apply simp
apply blast
done
lemma correct_stateE2 [elim?]:
"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<Longrightarrow>
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<Longrightarrow>
(\<And>ST LT z.
\<lbrakk>G \<turnstile>h hp \<surd>; h_init G hp ihp; preallocated hp ihp; is_class G C;
((ST,LT), z) \<in> phi C sig ! pc;
correct_frame G hp ihp (ST,LT) maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs\<rbrakk> \<Longrightarrow> P)
\<Longrightarrow> P"
apply (erule correct_stateE)
apply simp
done
lemma correct_stateI [intro?]:
"\<lbrakk>G \<turnstile>h hp \<surd>; h_init G hp ihp; preallocated hp ihp; is_class G C;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
(s',z) \<in> phi C sig ! pc;
correct_frame G hp ihp s' maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs\<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
apply (unfold correct_state_def)
apply (cases s')
apply simp
apply fast
done
end
lemma constructor_ok_field_update:
[| constructor_ok G hp ihp x C' z r; hp a = Some (Obj C od) |] ==> constructor_ok G (hp(a|->Obj C od')) ihp x C' z r
lemma constructor_ok_array_update:
[| constructor_ok G hp ihp x C' z r; hp a = Some (Arr T l en) |] ==> constructor_ok G (hp(a|->Arr T l en')) ihp x C' z r
lemma constructor_ok_newref:
[| hp x = None; constructor_ok G hp ihp v C' z r |] ==> constructor_ok G (hp(x|->obj)) (ihp(x := T)) v C' z r
lemma constructor_ok_pass_val:
[| constructor_ok G hp ihp x C' True r; constructor_ok G hp ihp v C z0 r0;
x = fst r0 |]
==> constructor_ok G hp ihp v C True (x, snd r)
lemma is_init_default_val:
is_init hp ihp (default_val T)
lemma iconf_widen:
[| G,hp,ihp \<turnstile> xcp ::\<preceq>i T; G |- T <=i T'; wf_prog wf_mb G |] ==> G,hp,ihp \<turnstile> xcp ::\<preceq>i T'
lemma is_init:
G,hp,ihp \<turnstile> v ::\<preceq>i Init T ==> is_init hp ihp v
lemma approx_val_Err:
approx_val G hp ihp x Err
lemma approx_val_Null:
approx_val G hp ihp Null (OK (Init (RefT x)))
lemma approx_val_widen:
[| wf_prog wt G; approx_val G hp ihp v (OK T); G |- T <=i T' |] ==> approx_val G hp ihp v (OK T')
lemma conf_notNone:
G,hp |- Addr loc ::<= ty ==> hp loc ~= None
lemma approx_val_imp_approx_val_sup_heap:
[| approx_val G hp ihp v at; hp <=| hp' |] ==> approx_val G hp' ihp v at
lemma approx_val_heap_update:
[| hp a = Some obj'; G,hp |- v ::<= T; obj_ty obj = obj_ty obj' |] ==> G,hp(a|->obj) |- v ::<= T
lemma approx_loc_Cons:
approx_loc G hp ihp (s # xs) (l # ls) = (approx_val G hp ihp s l & approx_loc G hp ihp xs ls)
lemma approx_loc_Nil:
approx_loc G hp ihp [] []
lemma approx_loc_len:
approx_loc G hp ihp loc LT ==> length loc = length LT
lemma approx_loc_replace_Err:
approx_loc G hp ihp loc LT ==> approx_loc G hp ihp loc (replace v Err LT)
lemma assConv_approx_stk_imp_approx_loc:
[| wf_prog wt G; !!x. x : set (zip tys_n ts) ==> split (init_le G) x;
length tys_n = length ts; approx_stk G hp ihp s tys_n |]
==> approx_loc G hp ihp s (map OK ts)
lemma approx_loc_imp_approx_loc_sup_heap:
[| approx_loc G hp ihp lvars lt; hp <=| hp' |] ==> approx_loc G hp' ihp lvars lt
lemma approx_val_newref:
h loc = None
==> approx_val G (h(loc|->Obj C fs)) (ih(loc := UnInit C pc)) (Addr loc)
(OK (UnInit C pc))
lemma approx_val_newref_false:
[| h l = None; approx_val G h ih (Addr l) (OK T) |] ==> False
lemma approx_val_imp_approx_val_newref:
[| approx_val G hp ihp v T; hp loc = None |] ==> approx_val G hp (ihp(loc := X)) v T
lemma approx_loc_newref:
[| approx_loc G hp ihp lvars lt; hp loc = None |] ==> approx_loc G hp (ihp(loc := X)) lvars lt
lemma approx_loc_newref_Err:
[| approx_loc G hp ihp loc LT; hp l = None; i < length loc; loc ! i = Addr l |] ==> LT ! i = Err
lemma approx_loc_newref_all_Err:
[| approx_loc G hp ihp loc LT; hp l = None |] ==> list_all2 (%v T. v = Addr l --> T = Err) loc LT
lemma approx_loc_imp_approx_loc_subst:
[| approx_loc G hp ihp loc LT; approx_val G hp ihp x X |] ==> approx_loc G hp ihp (loc[idx := x]) (LT[idx := X])
lemma approx_loc_Err:
approx_loc G hp ihp (replicate n v) (replicate n Err)
lemmas
[| P = P'; P' ==> Q = Q' |] ==> (P & Q) = (P' & Q')
lemma approx_loc_append:
length l1 = length L1
==> approx_loc G hp ihp (l1 @ l2) (L1 @ L2) =
(approx_loc G hp ihp l1 L1 & approx_loc G hp ihp l2 L2)
lemmas
[| P = P'; P' ==> Q = Q' |] ==> (P & Q) = (P' & Q')
lemma approx_val_Err_or_same:
[| approx_val G hp ihp v (OK X); X = UnInit C pc | X = PartInit D;
approx_val G hp ihp v X' |]
==> X' = Err | X' = OK X
lemma approx_loc_replace:
[| approx_loc G hp ihp loc LT; approx_val G hp ihp x' (OK X');
approx_val G hp ihp x (OK X); X = UnInit C pc | X = PartInit D;
corr_loc loc LT ihp x X |]
==> approx_loc G hp ihp (replace x x' loc) (replace (OK X) (OK X') LT)
lemma list_all2_approx:
list_all2 (approx_val G hp ihp) s (map OK S) = list_all2 (iconf G hp ihp) s S
lemma list_all2_iconf_widen:
[| wf_prog mb G; list_all2 (iconf G hp ihp) a b;
list_all2 (%x y. G |- x <=i Init y) b c |]
==> list_all2 (%v T. G,hp |- v ::<= T & is_init hp ihp v) a c
lemma approx_stk_rev_lem:
approx_stk G hp ihp (rev s) (rev t) = approx_stk G hp ihp s t
lemma approx_stk_rev:
approx_stk G hp ihp (rev s) t = approx_stk G hp ihp s (rev t)
lemma approx_stk_imp_approx_stk_sup_heap:
[| approx_stk G hp ihp lvars lt; hp <=| hp' |] ==> approx_stk G hp' ihp lvars lt
lemma approx_stk_Nil:
approx_stk G hp ihp [] []
lemma approx_stk_Cons:
approx_stk G hp ihp (x # stk) (S # ST) = (approx_val G hp ihp x (OK S) & approx_stk G hp ihp stk ST)
lemma approx_stk_Cons_lemma:
approx_stk G hp ihp stk (S # ST') =
(EX s stk'.
stk = s # stk' &
approx_val G hp ihp s (OK S) & approx_stk G hp ihp stk' ST')
lemma approx_stk_len:
approx_stk G hp ihp stk ST ==> length stk = length ST
lemma approx_stk_append_lemma:
approx_stk G hp ihp stk (S @ ST')
==> EX s stk'.
stk = s @ stk' &
length s = length S &
length stk' = length ST' &
approx_stk G hp ihp s S & approx_stk G hp ihp stk' ST'
lemma approx_stk_newref:
[| approx_stk G hp ihp lvars lt; hp loc = None |] ==> approx_stk G hp (ihp(loc := X)) lvars lt
lemma newref_notin_stk:
[| approx_stk G hp ihp stk ST; hp l = None |] ==> Addr l ~: set stk
lemma corr_loc_empty:
corr_loc [] [] ihp v T
lemma corr_loc_cons:
corr_loc (s # loc) (L # LT) ihp v T = ((L = OK T --> s = v & corr_val v T ihp) & corr_loc loc LT ihp v T)
lemma corr_loc_start:
[| ALL x:set LT. x = Err | (EX t. x = OK (Init t)); length loc = length LT;
T = UnInit C pc | T = PartInit C' |]
==> corr_loc loc LT ihp v T
lemma consistent_init_start:
[| LT0 = OK (Init (Class C)) # map OK (map Init pTs) @ replicate mxl' Err;
loc = oX # rev opTs @ replicate mxl' arbitrary; length pTs = length opTs |]
==> consistent_init [] loc ([], LT0) ihp
lemma corresponds_stk_cons:
corresponds (s # stk) loc (S # ST, LT) ihp v T = ((S = T --> s = v & corr_val v T ihp) & corresponds stk loc (ST, LT) ihp v T)
lemma corresponds_loc_nth:
[| corresponds stk loc (ST, LT) ihp v T; n < length LT; LT ! n = OK X |] ==> X = T --> loc ! n = v & corr_val v T ihp
lemma consistent_init_loc_nth:
[| consistent_init stk loc (ST, LT) ihp; n < length LT; LT ! n = OK X |] ==> consistent_init (loc ! n # stk) loc (X # ST, LT) ihp
lemma consistent_init_corresponds_stk_cons:
[| consistent_init (s # stk) loc (S # ST, LT) ihp;
S = UnInit C pc | S = PartInit C' |]
==> corresponds (s # stk) loc (S # ST, LT) ihp s S
lemma consistent_init_corresponds_loc:
[| consistent_init stk loc (ST, LT) ihp; LT ! n = OK T;
T = UnInit C pc | T = PartInit C'; n < length LT |]
==> corresponds stk loc (ST, LT) ihp (loc ! n) T
lemma consistent_init_pop:
consistent_init (s # stk) loc (S # ST, LT) ihp ==> consistent_init stk loc (ST, LT) ihp
lemma consistent_init_Init_stk:
consistent_init stk loc (ST, LT) ihp ==> consistent_init (s # stk) loc (Init T' # ST, LT) ihp
lemma corr_loc_set:
[| corr_loc loc LT ihp v T; OK T : set LT |] ==> corr_val v T ihp
lemma corresponds_var_upd_UnInit:
[| corresponds stk loc (ST, LT) ihp v T; n < length LT;
OK T : set (map OK ST) Un set LT |]
==> corresponds stk (loc[n := v]) (ST, LT[n := OK T]) ihp v T
lemma corresponds_var_upd_UnInit2:
[| corresponds stk loc (ST, LT) ihp v T; n < length LT; T' ~= T |] ==> corresponds stk (loc[n := v']) (ST, LT[n := OK T']) ihp v T
lemma corresponds_var_upd:
[| corresponds (s # stk) loc (S # ST, LT) ihp v T; idx < length LT |] ==> corresponds stk (loc[idx := s]) (ST, LT[idx := OK S]) ihp v T
lemma consistent_init_conv:
consistent_init stk loc s ihp =
(ALL T. (EX C pc. T = UnInit C pc) | (EX C. T = PartInit C) -->
(EX v. corresponds stk loc s ihp v T))
lemma consistent_init_store:
[| consistent_init (s # stk) loc (S # ST, LT) ihp; n < length LT |] ==> consistent_init stk (loc[n := s]) (ST, LT[n := OK S]) ihp
lemma corr_loc_newT:
[| OK T ~: set LT; length loc = length LT |] ==> corr_loc loc LT ihp v T
lemma corr_loc_new_val:
[| corr_loc loc LT ihp v T; Addr l ~: set loc |] ==> corr_loc loc LT (ihp(l := T')) v T
lemma corr_loc_Err_val:
[| corr_loc loc LT ihp v T; list_all2 (%v T. v = Addr l --> T = Err) loc LT |] ==> corr_loc loc LT (ihp(l := T')) v T
lemma corr_loc_len:
corr_loc loc LT ihp v T ==> length loc = length LT
lemma corresponds_newT:
[| corresponds stk loc (ST, LT) ihp' v' T'; OK T ~: set (map OK ST) Un set LT |] ==> corresponds stk loc (ST, LT) ihp v T
lemma corresponds_new_val:
[| corresponds stk loc (ST, LT) ihp v T; Addr l ~: set stk;
list_all2 (%v T. v = Addr l --> T = Err) loc LT |]
==> corresponds stk loc (ST, LT) (ihp(l := T')) v T
lemma corresponds_newref:
[| corresponds stk loc (ST, LT) ihp v T;
OK (UnInit C pc) ~: set (map OK ST) Un set LT; Addr l ~: set stk;
list_all2 (%v T. v = Addr l --> T = Err) loc LT |]
==> EX v. corresponds (Addr l # stk) loc (UnInit C pc # ST, LT)
(ihp(l := UnInit C pc)) v T
lemma consistent_init_new_val_lemma:
[| consistent_init stk loc (ST, LT) ihp; Addr l ~: set stk;
list_all2 (%v T. v = Addr l --> T = Err) loc LT |]
==> consistent_init stk loc (ST, LT) (ihp(l := T'))
lemma consistent_init_newref_lemma:
[| consistent_init stk loc (ST, LT) ihp;
OK (UnInit C pc) ~: set (map OK ST) Un set LT; Addr l ~: set stk;
list_all2 (%v T. v = Addr l --> T = Err) loc LT |]
==> consistent_init (Addr l # stk) loc (UnInit C pc # ST, LT)
(ihp(l := UnInit C pc))
lemma consistent_init_newref:
[| consistent_init stk loc (ST, LT) ihp; approx_loc G hp ihp loc LT;
hp l = None; approx_stk G hp ihp stk ST;
OK (UnInit C pc) ~: set (map OK ST) Un set LT |]
==> consistent_init (Addr l # stk) loc (UnInit C pc # ST, LT)
(ihp(l := UnInit C pc))
lemma corresponds_new_val2:
[| corresponds stk loc (ST, LT) ihp v T; approx_loc G hp ihp loc LT;
hp l = None; approx_stk G hp ihp stk ST |]
==> corresponds stk loc (ST, LT) (ihp(l := T')) v T
lemma consistent_init_new_val:
[| consistent_init stk loc (ST, LT) ihp; approx_loc G hp ihp loc LT;
hp l = None; approx_stk G hp ihp stk ST |]
==> consistent_init stk loc (ST, LT) (ihp(l := T'))
lemma corr_loc_replace_type:
[| corr_loc loc LT ihp v T; T ~= Init T'' |] ==> corr_loc loc (replace (OK T') (OK (Init T'')) LT) ihp v T
lemma corr_stk_replace_type:
[| corr_stk loc ST ihp v T; T ~= Init T'' |] ==> corr_stk loc (replace T' (Init T'') ST) ihp v T
lemma consistent_init_replace_type:
consistent_init stk loc (ST, LT) ihp
==> consistent_init stk loc
(replace T (Init T') ST, replace (OK T) (OK (Init T')) LT) ihp
lemma corr_loc_replace:
[| corr_loc loc LT ihp v T; approx_loc G hp ihp loc LT;
approx_val G hp ihp oX (OK T0); T ~= T'; T = UnInit C pc | T = PartInit D |]
==> corr_loc (replace oX x loc) (replace (OK T0) (OK T') LT) ihp v T
lemma corr_stk_replace:
[| corr_stk stk ST ihp v T; approx_stk G hp ihp stk ST;
approx_val G hp ihp oX (OK T0); T ~= T'; T = UnInit C pc | T = PartInit D |]
==> corr_stk (replace oX x stk) (replace T0 T' ST) ihp v T
lemma corresponds_replace:
[| corresponds stk loc (ST, LT) ihp v T; approx_loc G hp ihp loc LT;
approx_stk G hp ihp stk ST; approx_val G hp ihp oX (OK T0); T ~= T';
T = UnInit C pc | T = PartInit D |]
==> corresponds (replace oX x stk) (replace oX x loc)
(replace T0 T' ST, replace (OK T0) (OK T') LT) ihp v T
lemma consisten_init_replace:
[| consistent_init stk loc (ST, LT) ihp; approx_loc G hp ihp loc LT;
approx_stk G hp ihp stk ST; approx_val G hp ihp oX (OK T0); T' = Init C' |]
==> consistent_init (replace oX x stk) (replace oX x loc)
(replace T0 T' ST, replace (OK T0) (OK T') LT) ihp
lemma corr_loc_replace_Err:
corr_loc loc LT ihp v T ==> corr_loc loc (replace T' Err LT) ihp v T
lemma corresponds_replace_Err:
corresponds stk loc (ST, LT) ihp v T ==> corresponds stk loc (ST, replace T' Err LT) ihp v T
lemma consistent_init_replace_Err:
consistent_init stk loc (ST, LT) ihp ==> consistent_init stk loc (ST, replace T' Err LT) ihp
lemma corresponds_append:
[| corresponds (x @ stk) loc (X @ ST, LT) ihp v T; length X = length x |] ==> corresponds stk loc (ST, LT) ihp v T
lemma consistent_init_append:
[| consistent_init (x @ stk) loc (X @ ST, LT) ihp; length X = length x |] ==> consistent_init stk loc (ST, LT) ihp
lemma corresponds_xcp:
[| corresponds stk loc (ST, LT) ihp v T; T = UnInit C pc | T = PartInit D |] ==> corresponds [x] loc ([Init X], LT) ihp v T
lemma consistent_init_xcp:
consistent_init stk loc (ST, LT) ihp ==> consistent_init [x] loc ([Init X], LT) ihp
lemma corresponds_pop:
corresponds (s # stk) loc (S # ST, LT) ihp v T ==> corresponds stk loc (ST, LT) ihp v T
lemma consistent_init_Dup:
consistent_init (s # stk) loc (S # ST, LT) ihp ==> consistent_init (s # s # stk) loc (S # S # ST, LT) ihp
lemma corresponds_Dup:
corresponds (s # stk) loc (S # ST, LT) ihp v T ==> corresponds (s # s # stk) loc (S # S # ST, LT) ihp v T
lemma corresponds_Dup_x1:
corresponds (s1 # s2 # stk) loc (S1 # S2 # ST, LT) ihp v T ==> corresponds (s1 # s2 # s1 # stk) loc (S1 # S2 # S1 # ST, LT) ihp v T
lemma consistent_init_Dup_x1:
consistent_init (s1 # s2 # stk) loc (S1 # S2 # ST, LT) ihp ==> consistent_init (s1 # s2 # s1 # stk) loc (S1 # S2 # S1 # ST, LT) ihp
lemma corresponds_Dup_x2:
corresponds (s1 # s2 # s3 # stk) loc (S1 # S2 # S3 # ST, LT) ihp v T
==> corresponds (s1 # s2 # s3 # s1 # stk) loc (S1 # S2 # S3 # S1 # ST, LT) ihp v
T
lemma consistent_init_Dup_x2:
consistent_init (s1 # s2 # s3 # stk) loc (S1 # S2 # S3 # ST, LT) ihp
==> consistent_init (s1 # s2 # s3 # s1 # stk) loc (S1 # S2 # S3 # S1 # ST, LT)
ihp
lemma corresponds_Swap:
corresponds (s1 # s2 # stk) loc (S1 # S2 # ST, LT) ihp v T ==> corresponds (s2 # s1 # stk) loc (S2 # S1 # ST, LT) ihp v T
lemma consistent_init_Swap:
consistent_init (s1 # s2 # stk) loc (S1 # S2 # ST, LT) ihp ==> consistent_init (s2 # s1 # stk) loc (S2 # S1 # ST, LT) ihp
lemma oconf_blank:
[| is_class G D; wf_prog wf_mb G |] ==> G,hp |- blank G D [ok]
lemma oconf_field_update:
[| map_of (fields (G, oT)) FD = Some T; G,hp |- v ::<= T;
G,hp |- Obj oT fs [ok] |]
==> G,hp |- Obj oT (fs(FD|->v)) [ok]
lemma oconf_imp_oconf_heap_newref:
[| hp oref = None; G,hp |- obj [ok]; G,hp |- obj' [ok] |] ==> G,hp(oref|->obj') |- obj [ok]
lemma oconf_imp_oconf_heap_update:
[| hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp |- obj [ok] |] ==> G,hp(a|->obj'') |- obj [ok]
lemma hconf_imp_hconf_newref:
[| hp oref = None; G |-h hp [ok]; G,hp |- obj [ok] |] ==> G |-h hp(oref|->obj) [ok]
lemma hconf_imp_hconf_field_update:
map_of (fields (G, oT)) (F, D) = Some T & hp oloc = Some (Obj oT fs) & G,hp |- v ::<= T & G |-h hp [ok] ==> G |-h hp(oloc|->Obj oT (fs((F, D)|->v))) [ok]
lemma h_init_field_update:
[| h_init G hp ihp; hp x = Some (Obj C fs); is_init hp ihp v |] ==> h_init G (hp(x|->Obj C (fs(X|->v)))) ihp
lemma oconf_arrD:
[| G,h |- Arr T len en [ok]; n < len |] ==> EX v. en n = Some v & G,h |- v ::<= T
lemma h_init_newref:
[| hp r = None; G |-h hp [ok]; h_init G hp ihp |] ==> h_init G (hp(r|->blank G X)) (ihp(r := T'))
lemma preallocated_field_update:
[| hp a = Some (Obj oT fs); G |-h hp [ok]; preallocated hp ihp |] ==> preallocated (hp(a|->Obj oT fs')) ihp
lemma preallocated_array_update:
[| hp a = Some (Arr T l en); G |-h hp [ok]; preallocated hp ihp |] ==> preallocated (hp(a|->Arr T l en')) ihp
lemma
[| hp oref = None; preallocated hp ihp |] ==> preallocated (hp(oref|->obj)) (ihp(oref := T))
lemma correct_frames_ctor_ok:
correct_frames G hp ihp phi rT sig z r frs ==> frs = [] | (fst sig = init --> (EX a C'. constructor_ok G hp ihp a C' z r))
lemma correct_frameE:
[| correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
[| approx_stk G hp ihp stk ST; approx_loc G hp ihp loc LT;
consistent_init stk loc (ST, LT) ihp;
fst sig = init -->
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) &
(EX l. fst r = Addr l &
hp l ~= None &
(ihp l = PartInit C | (EX C'. ihp l = Init (Class C'))));
pc < length ins; length loc = length (snd sig) + maxl + 1 |]
==> P |]
==> P
lemmas
(f(x := y)) z = (if z = x then y else f z)
lemmas
P (if Q then x else y) = ((Q --> P x) & (¬ Q --> P y))
lemma correct_frames_imp_correct_frames_field_update:
[| correct_frames G hp ihp phi rT sig z r frs; hp a = Some (Obj C od);
map_of (fields (G, C)) fl = Some fd; G,hp |- v ::<= fd |]
==> correct_frames G (hp(a|->Obj C (od(fl|->v)))) ihp phi rT sig z r frs
lemma correct_frames_array_update:
[| correct_frames G hp ihp phi rT sig z r frs; hp a = Some (Arr T l en);
G,hp |- v ::<= fd |]
==> correct_frames G (hp(a|->Arr T l en')) ihp phi rT sig z r frs
lemma correct_frames_imp_correct_frames_newref:
[| hp x = None; correct_frames G hp ihp phi rT sig z r frs |] ==> correct_frames G (hp(x|->obj)) (ihp(x := T)) phi rT sig z r frs
lemmas
(f(x := y)) z = (if z = x then y else f z)
lemmas
P (if Q then x else y) = ((Q --> P x) & (¬ Q --> P y))
lemma correct_stateE:
[| G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
!!rT maxs maxl ins et ST LT z.
[| G |-h hp [ok]; h_init G hp ihp; preallocated hp ihp; is_class G C;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
((ST, LT), z) : phi C sig ! pc;
correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs |]
==> P |]
==> P
lemma correct_stateE2:
[| G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
!!ST LT z.
[| G |-h hp [ok]; h_init G hp ihp; preallocated hp ihp; is_class G C;
((ST, LT), z) : phi C sig ! pc;
correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs |]
==> P |]
==> P
lemma correct_stateI:
[| G |-h hp [ok]; h_init G hp ihp; preallocated hp ihp; is_class G C;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
(s', z) : phi C sig ! pc;
correct_frame G hp ihp s' maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs |]
==> G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok]