Theory Correctness1
section ‹Semantic Correctness of Stage 1›
theory Correctness1 imports
J0J1Bisim
"../J/DefAssPreservation"
begin
lemma finals_map_Val [simp]: "finals (map Val vs)"
by(simp add: finals_iff)
context J_heap_base begin
lemma τred0r_preserves_defass:
assumes wf: "wf_J_prog P"
shows "⟦ τred0r extTA P t h (e, xs) (e', xs'); 𝒟 e ⌊dom xs⌋ ⟧ ⟹ 𝒟 e' ⌊dom xs'⌋"
by(induct rule: rtranclp_induct2)(auto dest: red_preserves_defass[OF wf])
lemma τred0t_preserves_defass:
assumes wf: "wf_J_prog P"
shows "⟦ τred0t extTA P t h (e, xs) (e', xs'); 𝒟 e ⌊dom xs⌋ ⟧ ⟹ 𝒟 e' ⌊dom xs'⌋"
by(rule τred0r_preserves_defass[OF wf])(rule tranclp_into_rtranclp)
end
lemma LAss_lem:
"⟦x ∈ set xs; size xs ≤ size ys ⟧
⟹ m1 ⊆⇩m m2(xs[↦]ys) ⟹ m1(x↦y) ⊆⇩m m2(xs[↦]ys[index xs x := y])"
apply(simp add:map_le_def)
apply(simp add:fun_upds_apply index_less_aux eq_sym_conv)
done
lemma Block_lem:
fixes l :: "'a ⇀ 'b"
assumes 0: "l ⊆⇩m [Vs [↦] ls]"
and 1: "l' ⊆⇩m [Vs [↦] ls', V↦v]"
and hidden: "V ∈ set Vs ⟹ ls ! index Vs V = ls' ! index Vs V"
and size: "size ls = size ls'" "size Vs < size ls'"
shows "l'(V := l V) ⊆⇩m [Vs [↦] ls']"
proof -
have "l'(V := l V) ⊆⇩m [Vs [↦] ls', V↦v](V := l V)"
using 1 by(rule map_le_upd)
also have "… = [Vs [↦] ls'](V := l V)" by simp
also have "… ⊆⇩m [Vs [↦] ls']"
proof (cases "l V")
case None thus ?thesis by simp
next
case (Some w)
hence "[Vs [↦] ls] V = Some w"
using 0 by(force simp add: map_le_def split:if_splits)
hence VinVs: "V ∈ set Vs" and w: "w = ls ! index Vs V"
using size by(auto simp add:fun_upds_apply split:if_splits)
hence "w = ls' ! index Vs V" using hidden[OF VinVs] by simp
hence "[Vs [↦] ls'](V := l V) = [Vs [↦] ls']"
using Some size VinVs by(simp add:index_less_aux map_upds_upd_conv_index)
thus ?thesis by simp
qed
finally show ?thesis .
qed
subsection ‹Correctness proof›
locale J0_J1_heap_base =
J?: J_heap_base +
J1?: J1_heap_base +
constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
begin
lemma ta_bisim01_extTA2J0_extTA2J1:
assumes wf: "wf_J_prog P"
and nt: "⋀n T C M a h. ⟦ n < length ⦃ta⦄⇘t⇙; ⦃ta⦄⇘t⇙ ! n = NewThread T (C, M, a) h ⟧
⟹ typeof_addr h a = ⌊Class_type C⌋ ∧ (∃T meth D. P ⊢ C sees M:[]→T =⌊meth⌋ in D)"
shows "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
apply(simp add: ta_bisim_def ta_upd_simps)
apply(auto intro!: list_all2_all_nthI)
apply(case_tac "⦃ta⦄⇘t⇙ ! n")
apply(auto simp add: bisim_red0_Red1_def)
apply(drule (1) nt)
apply(clarify)
apply(erule bisim_list_extTA2J0_extTA2J1[OF wf, simplified])
done
lemma red_external_ta_bisim01:
"⟦ wf_J_prog P; P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟧ ⟹ ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
apply(rule ta_bisim01_extTA2J0_extTA2J1, assumption)
apply(drule (1) red_external_new_thread_sees, auto simp add: in_set_conv_nth)
apply(drule red_ext_new_thread_heap, auto simp add: in_set_conv_nth)
done
lemmas τred1t_expr =
NewArray_τred1t_xt Cast_τred1t_xt InstanceOf_τred1t_xt BinOp_τred1t_xt1 BinOp_τred1t_xt2 LAss_τred1t
AAcc_τred1t_xt1 AAcc_τred1t_xt2 AAss_τred1t_xt1 AAss_τred1t_xt2 AAss_τred1t_xt3
ALength_τred1t_xt FAcc_τred1t_xt FAss_τred1t_xt1 FAss_τred1t_xt2
CAS_τred1t_xt1 CAS_τred1t_xt2 CAS_τred1t_xt3 Call_τred1t_obj
Call_τred1t_param Block_None_τred1t_xt Block_τred1t_Some Sync_τred1t_xt InSync_τred1t_xt
Seq_τred1t_xt Cond_τred1t_xt Throw_τred1t_xt Try_τred1t_xt
lemmas τred1r_expr =
NewArray_τred1r_xt Cast_τred1r_xt InstanceOf_τred1r_xt BinOp_τred1r_xt1 BinOp_τred1r_xt2 LAss_τred1r
AAcc_τred1r_xt1 AAcc_τred1r_xt2 AAss_τred1r_xt1 AAss_τred1r_xt2 AAss_τred1r_xt3
ALength_τred1r_xt FAcc_τred1r_xt FAss_τred1r_xt1 FAss_τred1r_xt2
CAS_τred1r_xt1 CAS_τred1r_xt2 CAS_τred1r_xt3 Call_τred1r_obj
Call_τred1r_param Block_None_τred1r_xt Block_τred1r_Some Sync_τred1r_xt InSync_τred1r_xt
Seq_τred1r_xt Cond_τred1r_xt Throw_τred1r_xt Try_τred1r_xt
definition sim_move01 ::
"'addr J1_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr ⇒ 'addr expr1 ⇒ 'heap
⇒ 'addr locals1 ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 ⇒ 'heap ⇒ 'addr locals1 ⇒ bool"
where
"sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟷ ¬ final e0 ∧
(if τmove0 P h e0 then h' = h ∧ ta0 = ε ∧ ta = ε ∧ τred1't P t h (e, xs) (e', xs')
else ta_bisim01 ta0 (extTA2J1 P ta) ∧
(if call e0 = None ∨ call1 e = None
then (∃e'' xs''. τred1'r P t h (e, xs) (e'', xs'') ∧ False,P,t ⊢1 ⟨e'', (h, xs'')⟩ -ta→ ⟨e', (h', xs')⟩ ∧
¬ τmove1 P h e'')
else False,P,t ⊢1 ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩ ∧ ¬ τmove1 P h e))"
definition sim_moves01 ::
"'addr J1_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr list ⇒ 'addr expr1 list ⇒ 'heap
⇒ 'addr locals1 ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 list ⇒ 'heap ⇒ 'addr locals1 ⇒ bool"
where
"sim_moves01 P t ta0 es0 es h xs ta es' h' xs' ⟷ ¬ finals es0 ∧
(if τmoves0 P h es0 then h' = h ∧ ta0 = ε ∧ ta = ε ∧ τreds1't P t h (es, xs) (es', xs')
else ta_bisim01 ta0 (extTA2J1 P ta) ∧
(if calls es0 = None ∨ calls1 es = None
then (∃es'' xs''. τreds1'r P t h (es, xs) (es'', xs'') ∧ False,P,t ⊢1 ⟨es'', (h, xs'')⟩ [-ta→] ⟨es', (h', xs')⟩ ∧
¬ τmoves1 P h es'')
else False,P,t ⊢1 ⟨es, (h, xs)⟩ [-ta→] ⟨es', (h', xs')⟩ ∧ ¬ τmoves1 P h es))"
declare τred1t_expr [elim!] τred1r_expr[elim!]
lemma sim_move01_expr:
assumes "sim_move01 P t ta0 e0 e h xs ta e' h' xs'"
shows
"sim_move01 P t ta0 (newA T⌊e0⌉) (newA T⌊e⌉) h xs ta (newA T⌊e'⌉) h' xs'"
"sim_move01 P t ta0 (Cast T e0) (Cast T e) h xs ta (Cast T e') h' xs'"
"sim_move01 P t ta0 (e0 instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs'"
"sim_move01 P t ta0 (e0 «bop» e2) (e «bop» e2') h xs ta (e' «bop» e2') h' xs'"
"sim_move01 P t ta0 (Val v «bop» e0) (Val v «bop» e) h xs ta (Val v «bop» e') h' xs'"
"sim_move01 P t ta0 (V := e0) (V' := e) h xs ta (V' := e') h' xs'"
"sim_move01 P t ta0 (e0⌊e2⌉) (e⌊e2'⌉) h xs ta (e'⌊e2'⌉) h' xs'"
"sim_move01 P t ta0 (Val v⌊e0⌉) (Val v⌊e⌉) h xs ta (Val v⌊e'⌉) h' xs'"
"sim_move01 P t ta0 (e0⌊e2⌉ := e3) (e⌊e2'⌉ := e3') h xs ta (e'⌊e2'⌉ := e3') h' xs'"
"sim_move01 P t ta0 (Val v⌊e0⌉ := e3) (Val v⌊e⌉ := e3') h xs ta (Val v⌊e'⌉ := e3') h' xs'"
"sim_move01 P t ta0 (AAss (Val v) (Val v') e0) (AAss (Val v) (Val v') e) h xs ta (AAss (Val v) (Val v') e') h' xs'"
"sim_move01 P t ta0 (e0∙length) (e∙length) h xs ta (e'∙length) h' xs'"
"sim_move01 P t ta0 (e0∙F{D}) (e∙F'{D'}) h xs ta (e'∙F'{D'}) h' xs'"
"sim_move01 P t ta0 (FAss e0 F D e2) (FAss e F' D' e2') h xs ta (FAss e' F' D' e2') h' xs'"
"sim_move01 P t ta0 (FAss (Val v) F D e0) (FAss (Val v) F' D' e) h xs ta (FAss (Val v) F' D' e') h' xs'"
"sim_move01 P t ta0 (CompareAndSwap e0 D F e2 e3) (CompareAndSwap e D F e2' e3') h xs ta (CompareAndSwap e' D F e2' e3') h' xs'"
"sim_move01 P t ta0 (CompareAndSwap (Val v) D F e0 e3) (CompareAndSwap (Val v) D F e e3') h xs ta (CompareAndSwap (Val v) D F e' e3') h' xs'"
"sim_move01 P t ta0 (CompareAndSwap (Val v) D F (Val v') e0) (CompareAndSwap (Val v) D F (Val v') e) h xs ta (CompareAndSwap (Val v) D F (Val v') e') h' xs'"
"sim_move01 P t ta0 (e0∙M(es)) (e∙M(es')) h xs ta (e'∙M(es')) h' xs'"
"sim_move01 P t ta0 ({V:T=vo; e0}) ({V':T=None; e}) h xs ta ({V':T=None; e'}) h' xs'"
"sim_move01 P t ta0 (sync(e0) e2) (sync⇘V'⇙(e) e2') h xs ta (sync⇘V'⇙(e') e2') h' xs'"
"sim_move01 P t ta0 (insync(a) e0) (insync⇘V'⇙(a') e) h xs ta (insync⇘V'⇙(a') e') h' xs'"
"sim_move01 P t ta0 (e0;;e2) (e;;e2') h xs ta (e';;e2') h' xs'"
"sim_move01 P t ta0 (if (e0) e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs'"
"sim_move01 P t ta0 (throw e0) (throw e) h xs ta (throw e') h' xs'"
"sim_move01 P t ta0 (try e0 catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'"
using assms
apply(simp_all add: sim_move01_def final_iff τred1r_Val τred1t_Val split: if_split_asm split del: if_split)
apply(fastforce simp add: final_iff τred1r_Val τred1t_Val split!: if_splits intro: red1_reds1.intros)+
done
lemma sim_moves01_expr:
"sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟹ sim_moves01 P t ta0 (e0 # es2) (e # es2') h xs ta (e' # es2') h' xs'"
"sim_moves01 P t ta0 es0 es h xs ta es' h' xs' ⟹ sim_moves01 P t ta0 (Val v # es0) (Val v # es) h xs ta (Val v # es') h' xs'"
apply(simp_all add: sim_move01_def sim_moves01_def final_iff finals_iff Cons_eq_append_conv τred1t_Val τred1r_Val split: if_split_asm split del: if_split)
apply(auto simp add: Cons_eq_append_conv τred1t_Val τred1r_Val split!: if_splits intro: List1Red1 List1Red2 τred1t_inj_τreds1t τred1r_inj_τreds1r τreds1t_cons_τreds1t τreds1r_cons_τreds1r)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τreds1r_cons_τreds1r intro!: List1Red2)
apply(force elim!: τreds1r_cons_τreds1r intro!: List1Red2)
done
lemma sim_move01_CallParams:
"sim_moves01 P t ta0 es0 es h xs ta es' h' xs'
⟹ sim_move01 P t ta0 (Val v∙M(es0)) (Val v∙M(es)) h xs ta (Val v∙M(es')) h' xs'"
apply(clarsimp simp add: sim_move01_def sim_moves01_def τreds1r_map_Val τreds1t_map_Val is_vals_conv split: if_split_asm split del: if_split)
apply(fastforce simp add: sim_move01_def sim_moves01_def τreds1r_map_Val τreds1t_map_Val intro: Call_τred1r_param Call1Params)
apply(rule conjI, fastforce)
apply(split if_split)
apply(rule conjI)
apply(clarsimp simp add: finals_iff)
apply(clarify)
apply(split if_split)
apply(rule conjI)
apply(simp del: call.simps calls.simps call1.simps calls1.simps)
apply(fastforce simp add: sim_move01_def sim_moves01_def τred1r_Val τred1t_Val τreds1r_map_Val_Throw intro: Call_τred1r_param Call1Params split: if_split_asm)
apply(fastforce split: if_split_asm simp add: is_vals_conv τreds1r_map_Val τreds1r_map_Val_Throw)
apply(rule conjI, fastforce)
apply(fastforce simp add: sim_move01_def sim_moves01_def τred1r_Val τred1t_Val τreds1t_map_Val τreds1r_map_Val is_vals_conv intro: Call_τred1r_param Call1Params split: if_split_asm)
done
lemma sim_move01_reds:
"⟦ (h', a) ∈ allocate h (Class_type C); ta0 = ⦃NewHeapElem a (Class_type C)⦄; ta = ⦃NewHeapElem a (Class_type C)⦄ ⟧
⟹ sim_move01 P t ta0 (new C) (new C) h xs ta (addr a) h' xs"
"allocate h (Class_type C) = {} ⟹ sim_move01 P t ε (new C) (new C) h xs ε (THROW OutOfMemory) h xs"
"⟦ (h', a) ∈ allocate h (Array_type T (nat (sint i))); 0 <=s i;
ta0 = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄; ta = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄ ⟧
⟹ sim_move01 P t ta0 (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ta (addr a) h' xs"
"i <s 0 ⟹ sim_move01 P t ε (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ε (THROW NegativeArraySize) h xs"
"⟦ allocate h (Array_type T (nat (sint i))) = {}; 0 <=s i ⟧
⟹ sim_move01 P t ε (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ε (THROW OutOfMemory) h xs"
"⟦ typeof⇘h⇙ v = ⌊U⌋; P ⊢ U ≤ T ⟧
⟹ sim_move01 P t ε (Cast T (Val v)) (Cast T (Val v)) h xs ε (Val v) h xs"
"⟦ typeof⇘h⇙ v = ⌊U⌋; ¬ P ⊢ U ≤ T ⟧
⟹ sim_move01 P t ε (Cast T (Val v)) (Cast T (Val v)) h xs ε (THROW ClassCast) h xs"
"⟦ typeof⇘h⇙ v = ⌊U⌋; b ⟷ v ≠ Null ∧ P ⊢ U ≤ T ⟧
⟹ sim_move01 P t ε ((Val v) instanceof T) ((Val v) instanceof T) h xs ε (Val (Bool b)) h xs"
"binop bop v1 v2 = Some (Inl v) ⟹ sim_move01 P t ε ((Val v1) «bop» (Val v2)) (Val v1 «bop» Val v2) h xs ε (Val v) h xs"
"binop bop v1 v2 = Some (Inr a) ⟹ sim_move01 P t ε ((Val v1) «bop» (Val v2)) (Val v1 «bop» Val v2) h xs ε (Throw a) h xs"
"⟦ xs!V = v; V < size xs ⟧ ⟹ sim_move01 P t ε (Var V') (Var V) h xs ε (Val v) h xs"
"V < length xs ⟹ sim_move01 P t ε (V' := Val v) (V := Val v) h xs ε unit h (xs[V := v])"
"sim_move01 P t ε (null⌊Val v⌉) (null⌊Val v⌉) h xs ε (THROW NullPointer) h xs"
"⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
⟹ sim_move01 P t ε (addr a⌊Val (Intg i)⌉) ((addr a)⌊Val (Intg i)⌉) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
"⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n;
heap_read h a (ACell (nat (sint i))) v;
ta0 = ⦃ReadMem a (ACell (nat (sint i))) v⦄;
ta = ⦃ReadMem a (ACell (nat (sint i))) v⦄ ⟧
⟹ sim_move01 P t ta0 (addr a⌊Val (Intg i)⌉) ((addr a)⌊Val (Intg i)⌉) h xs ta (Val v) h xs"
"sim_move01 P t ε (null⌊Val v⌉ := Val v') (null⌊Val v⌉ := Val v') h xs ε (THROW NullPointer) h xs"
"⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
⟹ sim_move01 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
"⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = ⌊U⌋; ¬ (P ⊢ U ≤ T) ⟧
⟹ sim_move01 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayStore) h xs"
"⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = Some U; P ⊢ U ≤ T;
heap_write h a (ACell (nat (sint i))) v h';
ta0 = ⦃WriteMem a (ACell (nat (sint i))) v⦄; ta = ⦃WriteMem a (ACell (nat (sint i))) v ⦄ ⟧
⟹ sim_move01 P t ta0 (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ta unit h' xs"
"typeof_addr h a = ⌊Array_type T n⌋ ⟹ sim_move01 P t ε (addr a∙length) (addr a∙length) h xs ε (Val (Intg (word_of_int (int n)))) h xs"
"sim_move01 P t ε (null∙length) (null∙length) h xs ε (THROW NullPointer) h xs"
"⟦ heap_read h a (CField D F) v; ta0 = ⦃ReadMem a (CField D F) v⦄; ta = ⦃ReadMem a (CField D F) v⦄ ⟧
⟹ sim_move01 P t ta0 (addr a∙F{D}) (addr a∙F{D}) h xs ta (Val v) h xs"
"sim_move01 P t ε (null∙F{D}) (null∙F{D}) h xs ε (THROW NullPointer) h xs"
"⟦ heap_write h a (CField D F) v h'; ta0 = ⦃WriteMem a (CField D F) v⦄; ta = ⦃WriteMem a (CField D F) v⦄ ⟧
⟹ sim_move01 P t ta0 (addr a∙F{D} := Val v) (addr a∙F{D} := Val v) h xs ta unit h' xs"
"sim_move01 P t ε (null∙compareAndSwap(D∙F, Val v, Val v')) (null∙compareAndSwap(D∙F, Val v, Val v')) h xs ε (THROW NullPointer) h xs"
"⟦ heap_read h a (CField D F) v''; heap_write h a (CField D F) v' h'; v'' = v;
ta0 = ⦃ReadMem a (CField D F) v'', WriteMem a (CField D F) v'⦄; ta = ⦃ReadMem a (CField D F) v'', WriteMem a (CField D F) v'⦄ ⟧
⟹ sim_move01 P t ta0 (addr a∙compareAndSwap(D∙F, Val v, Val v')) (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta true h' xs"
"⟦ heap_read h a (CField D F) v''; v'' ≠ v;
ta0 = ⦃ReadMem a (CField D F) v''⦄; ta = ⦃ReadMem a (CField D F) v''⦄ ⟧
⟹ sim_move01 P t ta0 (addr a∙compareAndSwap(D∙F, Val v, Val v')) (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta false h xs"
"sim_move01 P t ε (null∙F{D} := Val v) (null∙F{D} := Val v) h xs ε (THROW NullPointer) h xs"
"sim_move01 P t ε ({V':T=vo; Val u}) ({V:T=None; Val u}) h xs ε (Val u) h xs"
"V < length xs ⟹ sim_move01 P t ε (sync(null) e0) (sync⇘V⇙ (null) e1) h xs ε (THROW NullPointer) h (xs[V := Null])"
"sim_move01 P t ε (Val v;;e0) (Val v;; e1) h xs ε e1 h xs"
"sim_move01 P t ε (if (true) e0 else e0') (if (true) e1 else e1') h xs ε e1 h xs"
"sim_move01 P t ε (if (false) e0 else e0') (if (false) e1 else e1') h xs ε e1' h xs"
"sim_move01 P t ε (throw null) (throw null) h xs ε (THROW NullPointer) h xs"
"sim_move01 P t ε (try (Val v) catch(C V') e0) (try (Val v) catch(C V) e1) h xs ε (Val v) h xs"
"⟦ typeof_addr h a = ⌊Class_type D⌋; P ⊢ D ≼⇧* C; V < length xs ⟧
⟹ sim_move01 P t ε (try (Throw a) catch(C V') e0) (try (Throw a) catch(C V) e1) h xs ε ({V:Class C=None; e1}) h (xs[V := Addr a])"
"sim_move01 P t ε (newA T⌊Throw a⌉) (newA T⌊Throw a⌉) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Cast T (Throw a)) (Cast T (Throw a)) h xs ε (Throw a) h xs"
"sim_move01 P t ε ((Throw a) instanceof T) ((Throw a) instanceof T) h xs ε (Throw a) h xs"
"sim_move01 P t ε ((Throw a) «bop» e0) ((Throw a) «bop» e1) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v «bop» (Throw a)) (Val v «bop» (Throw a)) h xs ε (Throw a) h xs"
"sim_move01 P t ε (V' := Throw a) (V := Throw a) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a⌊e0⌉) (Throw a⌊e1⌉) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v⌊Throw a⌉) (Val v⌊Throw a⌉) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a⌊e0⌉ := e0') (Throw a⌊e1⌉ := e1') h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v⌊Throw a⌉ := e0) (Val v⌊Throw a⌉ := e1) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v⌊Val v'⌉ := Throw a) (Val v⌊Val v'⌉ := Throw a) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a∙length) (Throw a∙length) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a∙F{D}) (Throw a∙F{D}) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a∙F{D} := e0) (Throw a∙F{D} := e1) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v∙F{D} := Throw a) (Val v∙F{D} := Throw a) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a∙compareAndSwap(D∙F, e2, e3)) (Throw a∙compareAndSwap(D∙F, e2', e3')) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v∙compareAndSwap(D∙F, Throw a, e3)) (Val v∙compareAndSwap(D∙F, Throw a, e3')) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Val v∙compareAndSwap(D∙F, Val v', Throw a)) (Val v∙compareAndSwap(D∙F, Val v', Throw a)) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a∙M(es0)) (Throw a∙M(es1)) h xs ε (Throw a) h xs"
"sim_move01 P t ε ({V':T=vo; Throw a}) ({V:T=None; Throw a}) h xs ε (Throw a) h xs"
"sim_move01 P t ε (sync(Throw a) e0) (sync⇘V⇙(Throw a) e1) h xs ε (Throw a) h xs"
"sim_move01 P t ε (Throw a;;e0) (Throw a;;e1) h xs ε (Throw a) h xs"
"sim_move01 P t ε (if (Throw a) e0 else e0') (if (Throw a) e1 else e1') h xs ε (Throw a) h xs"
"sim_move01 P t ε (throw (Throw a)) (throw (Throw a)) h xs ε (Throw a) h xs"
apply(simp_all add: sim_move01_def ta_bisim_def split: if_split_asm split del: if_split)
apply(fastforce intro: red1_reds1.intros)+
done
lemma sim_move01_ThrowParams:
"sim_move01 P t ε (Val v∙M(map Val vs @ Throw a # es0)) (Val v∙M(map Val vs @ Throw a # es1)) h xs ε (Throw a) h xs"
apply(simp add: sim_move01_def split del: if_split)
apply(rule conjI, fastforce)
apply(split if_split)
apply(rule conjI)
apply(fastforce intro: red1_reds1.intros)
apply(fastforce simp add: sim_move01_def intro: red1_reds1.intros)
done
lemma sim_move01_CallNull:
"sim_move01 P t ε (null∙M(map Val vs)) (null∙M(map Val vs)) h xs ε (THROW NullPointer) h xs"
by(fastforce simp add: sim_move01_def map_eq_append_conv intro: red1_reds1.intros)
lemma sim_move01_SyncLocks:
"⟦ V < length xs; ta0 = ⦃Lock→a, SyncLock a⦄; ta = ⦃Lock→a, SyncLock a⦄ ⟧
⟹ sim_move01 P t ta0 (sync(addr a) e0) (sync⇘V⇙ (addr a) e1) h xs ta (insync⇘V⇙ (a) e1) h (xs[V := Addr a])"
"⟦ xs ! V = Addr a'; V < length xs; ta0 = ⦃Unlock→a', SyncUnlock a'⦄; ta = ⦃Unlock→a', SyncUnlock a'⦄ ⟧
⟹ sim_move01 P t ta0 (insync(a') (Val v)) (insync⇘V⇙ (a) (Val v)) h xs ta (Val v) h xs"
"⟦ xs ! V = Addr a'; V < length xs; ta0 = ⦃Unlock→a', SyncUnlock a'⦄; ta = ⦃Unlock→a', SyncUnlock a'⦄ ⟧
⟹ sim_move01 P t ta0 (insync(a') (Throw a'')) (insync⇘V⇙ (a) (Throw a'')) h xs ta (Throw a'') h xs"
by(fastforce simp add: sim_move01_def ta_bisim_def expand_finfun_eq fun_eq_iff finfun_upd_apply ta_upd_simps intro: red1_reds1.intros[simplified] split: if_split_asm)+
lemma sim_move01_TryFail:
"⟦ typeof_addr h a = ⌊Class_type D⌋; ¬ P ⊢ D ≼⇧* C ⟧
⟹ sim_move01 P t ε (try (Throw a) catch(C V') e0) (try (Throw a) catch(C V) e1) h xs ε (Throw a) h xs"
by(auto simp add: sim_move01_def intro!: Red1TryFail)
lemma sim_move01_BlockSome:
"⟦ sim_move01 P t ta0 e0 e h (xs[V := v]) ta e' h' xs'; V < length xs ⟧
⟹ sim_move01 P t ta0 ({V':T=⌊v⌋; e0}) ({V:T=⌊v⌋; e}) h xs ta ({V:T=None; e'}) h' xs'"
"V < length xs ⟹ sim_move01 P t ε ({V':T=⌊v⌋; Val u}) ({V:T=⌊v⌋; Val u}) h xs ε (Val u) h (xs[V := v])"
"V < length xs ⟹ sim_move01 P t ε ({V':T=⌊v⌋; Throw a}) ({V:T=⌊v⌋; Throw a}) h xs ε (Throw a) h (xs[V := v])"
apply(auto simp add: sim_move01_def)
apply(split if_split_asm)
apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_τred1r_Some)
apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_τred1r_Some)
apply(fastforce simp add: sim_move01_def intro!: τred1t_2step[OF Block1Some] τred1r_1step[OF Block1Some] Red1Block Block1Throw)+
done
lemmas sim_move01_intros =
sim_move01_expr sim_move01_reds sim_move01_ThrowParams sim_move01_CallNull sim_move01_TryFail
sim_move01_BlockSome sim_move01_CallParams
declare sim_move01_intros[intro]
lemma sim_move01_preserves_len: "sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟹ length xs' = length xs"
by(fastforce simp add: sim_move01_def split: if_split_asm dest: τred1r_preserves_len τred1t_preserves_len red1_preserves_len)
lemma sim_move01_preserves_unmod:
"⟦ sim_move01 P t ta0 e0 e h xs ta e' h' xs'; unmod e i; i < length xs ⟧ ⟹ xs' ! i = xs ! i"
apply(auto simp add: sim_move01_def split: if_split_asm dest: τred1t_preserves_unmod)
apply(frule (2) τred1'r_preserves_unmod)
apply(frule (1) τred1r_unmod_preserved)
apply(frule τred1r_preserves_len)
apply(auto dest: red1_preserves_unmod)
apply(frule (2) τred1'r_preserves_unmod)
apply(frule (1) τred1r_unmod_preserved)
apply(frule τred1r_preserves_len)
apply(auto dest: red1_preserves_unmod)
done
lemma assumes wf: "wf_J_prog P"
shows red1_simulates_red_aux:
"⟦ extTA2J0 P,P,t ⊢ ⟨e1, S⟩ -TA→ ⟨e1', S'⟩; bisim vs e1 e2 XS; fv e1 ⊆ set vs;
lcl S ⊆⇩m [vs [↦] XS]; length vs + max_vars e1 ≤ length XS;
∀aMvs. call e1 = ⌊aMvs⌋ ⟶ synthesized_call P (hp S) aMvs ⟧
⟹ ∃ta e2' XS'. sim_move01 (compP1 P) t TA e1 e2 (hp S) XS ta e2' (hp S') XS' ∧ bisim vs e1' e2' XS' ∧ lcl S' ⊆⇩m [vs [↦] XS']"
(is "⟦ _; _; _; _; _; ?synth e1 S ⟧ ⟹ ?concl e1 e2 S XS e1' S' TA vs")
and reds1_simulates_reds_aux:
"⟦ extTA2J0 P,P,t ⊢ ⟨es1, S⟩ [-TA→] ⟨es1', S'⟩; bisims vs es1 es2 XS; fvs es1 ⊆ set vs;
lcl S ⊆⇩m [vs [↦] XS]; length vs + max_varss es1 ≤ length XS;
∀aMvs. calls es1 = ⌊aMvs⌋ ⟶ synthesized_call P (hp S) aMvs ⟧
⟹ ∃ta es2' xs'. sim_moves01 (compP1 P) t TA es1 es2 (hp S) XS ta es2' (hp S') xs' ∧ bisims vs es1' es2' xs' ∧ lcl S' ⊆⇩m [vs [↦] xs']"
(is "⟦ _; _; _; _; _; ?synths es1 S ⟧ ⟹ ?concls es1 es2 S XS es1' S' TA vs")
proof(induct arbitrary: vs e2 XS and vs es2 XS rule: red_reds.inducts)
case (BinOpRed1 e s ta e' s' bop e2 Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
with ‹bisim Vs (e «bop» e2) E2 xs› obtain E
where "E2 = E «bop» compE1 Vs e2" and "bisim Vs e E xs" and "¬ contains_insync e2" by auto
with IH[of Vs E xs] ‹fv (e «bop» e2) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e›
‹length Vs + max_vars (e «bop» e2) ≤ length xs› ‹?synth (e «bop» e2) s› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
case (BinOpRed2 e s ta e' s' v bop Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹bisim Vs (Val v «bop» e) E2 xs› obtain E
where "E2 = Val v «bop» E" and "bisim Vs e E xs" by auto
with IH[of Vs E xs] ‹fv (Val v «bop» e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars (Val v «bop» e) ≤ length xs› ‹?synth (Val v «bop» e) s› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
show ?case by(fastforce elim!: sim_move01_expr)
next
case RedVar thus ?case
by(fastforce simp add: index_less_aux map_le_def fun_upds_apply intro!: exI dest: bspec)
next
case RedLAss thus ?case
by(fastforce intro: index_less_aux LAss_lem intro!: exI simp del: fun_upd_apply)
next
case (AAccRed1 a s ta a' s' i Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs a e2 XS; fv a ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars a ≤ length XS;
?synth a s ⟧ ⟹ ?concl a e2 s XS a' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
with ‹bisim Vs (a⌊i⌉) E2 xs› obtain E
where "E2 = E⌊compE1 Vs i⌉" and "bisim Vs a E xs" and "¬ contains_insync i" by auto
with IH[of Vs E xs] ‹fv (a⌊i⌉) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val a›
‹length Vs + max_vars (a⌊i⌉) ≤ length xs› ‹?synth (a⌊i⌉) s› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
show ?case by(cases "is_val a'")(fastforce elim!: sim_move01_expr)+
next
case (AAccRed2 i s ta i' s' a Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs i e2 XS; fv i ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars i ≤ length XS;
?synth i s ⟧ ⟹ ?concl i e2 s XS i' s' ta vs›
from ‹bisim Vs (Val a⌊i⌉) E2 xs› obtain E
where "E2 = Val a⌊E⌉" and "bisim Vs i E xs" by auto
with IH[of Vs E xs] ‹fv (Val a⌊i⌉) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars (Val a⌊i⌉) ≤ length xs› ‹?synth (Val a⌊i⌉) s› ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩›
show ?case by(fastforce elim!: sim_move01_expr)
next
case RedAAcc thus ?case by(auto simp del: split_paired_Ex)
next
case (AAssRed1 a s ta a' s' i e Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs a e2 XS; fv a ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars a ≤ length XS;
?synth a s ⟧ ⟹ ?concl a e2 s XS a' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
with ‹bisim Vs (a⌊i⌉:=e) E2 xs› obtain E
where E2: "E2 = E⌊compE1 Vs i⌉:=compE1 Vs e" and "bisim Vs a E xs"
and sync: "¬ contains_insync i" "¬ contains_insync e" by auto
with IH[of Vs E xs] ‹fv (a⌊i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
‹length Vs + max_vars (a⌊i⌉:=e) ≤ length xs› ‹?synth (a⌊i⌉:=e) s›
obtain ta' e2' xs'
where IH': "sim_move01 (compP1 P) t ta a E (hp s) xs ta' e2' (hp s') xs'"
"bisim Vs a' e2' xs'" "lcl s' ⊆⇩m [Vs [↦] xs']"
by auto
show ?case
proof(cases "is_val a'")
case True
from ‹fv (a⌊i⌉:=e) ⊆ set Vs› sync
have "bisim Vs i (compE1 Vs i) xs'" "bisim Vs e (compE1 Vs e) xs'" by auto
with IH' E2 True sync ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› show ?thesis
by(cases "is_val i")(fastforce elim!: sim_move01_expr)+
next
case False with IH' E2 sync ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
show ?thesis by(fastforce elim!: sim_move01_expr)
qed
next
case (AAssRed2 i s ta i' s' a e Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs i e2 XS; fv i ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars i ≤ length XS;
?synth i s ⟧ ⟹ ?concl i e2 s XS i' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩› have "¬ is_val i" by auto
with ‹bisim Vs (Val a⌊i⌉ := e) E2 xs› obtain E
where "E2 = Val a⌊E⌉:=compE1 Vs e" and "bisim Vs i E xs" and "¬ contains_insync e" by auto
with IH[of Vs E xs] ‹fv (Val a⌊i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val i› ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩›
‹length Vs + max_vars (Val a⌊i⌉:=e) ≤ length xs› ‹?synth (Val a⌊i⌉:=e) s›
show ?case by(cases "is_val i'")(fastforce elim!: sim_move01_expr)+
next
case (AAssRed3 e s ta e' s' a i Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹bisim Vs (Val a⌊Val i⌉ := e) E2 xs› obtain E
where "E2 = Val a⌊Val i⌉:=E" and "bisim Vs e E xs" by auto
with IH[of Vs E xs] ‹fv (Val a⌊Val i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars (Val a⌊Val i⌉:=e) ≤ length xs› ‹?synth (Val a⌊Val i⌉:=e) s›
show ?case by(fastforce elim!: sim_move01_expr)
next
case RedAAssStore thus ?case by(auto intro!: exI)
next
case (FAssRed1 e s ta e' s' F D e2 Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
with ‹bisim Vs (e∙F{D} := e2) E2 xs› obtain E
where "E2 = E∙F{D} := compE1 Vs e2" and "bisim Vs e E xs" and "¬ contains_insync e2" by auto
with IH[of Vs E xs] ‹fv (e∙F{D} := e2) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars (e∙F{D} := e2) ≤ length xs› ‹?synth (e∙F{D} := e2) s›
show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
case (FAssRed2 e s ta e' s' v F D Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹bisim Vs (Val v∙F{D} := e) E2 xs› obtain E
where "E2 = Val v∙F{D} := E" and "bisim Vs e E xs" by auto
with IH[of Vs E xs] ‹fv (Val v∙F{D} := e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars (Val v∙F{D} := e) ≤ length xs› ‹?synth (Val v∙F{D} := e) s›
show ?case by(fastforce elim!: sim_move01_expr)
next
case (CASRed1 e s ta e' s' D F e2 e3 Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
with ‹bisim Vs _ E2 xs› obtain E
where E2: "E2 = E∙compareAndSwap(D∙F, compE1 Vs e2, compE1 Vs e3)" and "bisim Vs e E xs"
and sync: "¬ contains_insync e2" "¬ contains_insync e3" by(auto)
with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
obtain ta' e2' xs'
where IH': "sim_move01 (compP1 P) t ta e E (hp s) xs ta' e2' (hp s') xs'"
"bisim Vs e' e2' xs'" "lcl s' ⊆⇩m [Vs [↦] xs']"
by auto
show ?case
proof(cases "is_val e'")
case True
from ‹fv _ ⊆ set Vs› sync
have "bisim Vs e2 (compE1 Vs e2) xs'" "bisim Vs e3 (compE1 Vs e3) xs'" by auto
with IH' E2 True sync ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› show ?thesis
by(cases "is_val e2")(fastforce elim!: sim_move01_expr)+
next
case False with IH' E2 sync ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
show ?thesis by(fastforce elim!: sim_move01_expr)
qed
next
case (CASRed2 e s ta e' s' v D F e3 Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
with ‹bisim Vs _ E2 xs› obtain E
where "E2 = Val v∙compareAndSwap(D∙F, E, compE1 Vs e3)" and "bisim Vs e E xs" and "¬ contains_insync e3" by(auto)
with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
case (CASRed3 e s ta e' s' v D F v' Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹bisim Vs _ E2 xs› obtain E
where "E2 = Val v∙compareAndSwap(D∙F, Val v', E)" and "bisim Vs e E xs" by auto
with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
show ?case by(fastforce elim!: sim_move01_expr)
next
case (CallObj e s ta e' s' M es Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
with ‹bisim Vs (e∙M(es)) E2 xs› obtain E
where "E2 = E∙M(compEs1 Vs es)" and "bisim Vs e E xs" and "¬ contains_insyncs es"
by(auto simp add: compEs1_conv_map)
with IH[of Vs E xs] ‹fv (e∙M(es)) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars (e∙M(es)) ≤ length xs› ‹?synth (e∙M(es)) s›
show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr split: if_split_asm)+
next
case (CallParams es s ta es' s' v M Vs E2 xs)
note IH = ‹⋀vs es2 XS. ⟦bisims vs es es2 XS; fvs es ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_varss es ≤ length XS;
?synths es s ⟧ ⟹ ?concls es es2 s XS es' s' ta vs›
from ‹bisim Vs (Val v∙M(es)) E2 xs› obtain Es
where "E2 = Val v∙M(Es)" and "bisims Vs es Es xs" by auto
moreover from ‹extTA2J0 P,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩› have "¬ is_vals es" by auto
with ‹?synth (Val v∙M(es)) s› have "?synths es s" by(auto)
moreover note IH[of Vs Es xs] ‹fv (Val v∙M(es)) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars (Val v∙M(es)) ≤ length xs›
ultimately show ?case by(fastforce elim!: sim_move01_CallParams)
next
case (RedCall s a U M Ts T pns body D vs Vs E2 xs)
from ‹typeof_addr (hp s) a = ⌊U⌋›
have "call (addr a∙M(map Val vs)) = ⌊(a, M, vs)⌋" by auto
with ‹?synth (addr a∙M(map Val vs)) s› have "synthesized_call P (hp s) (a, M, vs)" by auto
with ‹typeof_addr (hp s) a = ⌊U⌋› ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D›
have False by(auto simp add: synthesized_call_conv dest: sees_method_fun)
thus ?case ..
next
case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s' Vs E2 xs)
from ‹bisim Vs (addr a∙M(map Val vs)) E2 xs› have "E2 = addr a∙M(map Val vs)" by auto
moreover note ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D› ‹typeof_addr (hp s) a = ⌊T⌋› ‹ta' = extTA2J0 P ta›
‹e' = extRet2J (addr a∙M(map Val vs)) va› ‹s' = (h', lcl s)› ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
‹lcl s ⊆⇩m [Vs [↦] xs]›
moreover from wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
have "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)" by(rule red_external_ta_bisim01)
moreover from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› ‹typeof_addr (hp s) a = ⌊T⌋›
‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D›
have "τexternal_defs D M ⟹ h' = hp s ∧ ta = ε"
by(fastforce dest: τexternal'_red_external_heap_unchanged τexternal'_red_external_TA_empty simp add: τexternal'_def τexternal_def)
ultimately show ?case
by(cases va)(fastforce intro!: exI[where x=ta] intro: Red1CallExternal simp add: map_eq_append_conv sim_move01_def dest: sees_method_fun simp del: split_paired_Ex)+
next
case (BlockRed e h x V vo ta e' h' x' T Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl (h, x(V := vo)) ⊆⇩m [vs [↦] XS];
length vs + max_vars e ≤ length XS; ?synth e (h, (x(V := vo)))⟧
⟹ ?concl e e2 (h, x(V := vo)) XS e' (h', x') ta vs›
note red = ‹extTA2J0 P,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
note len = ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
from ‹fv {V:T=vo; e} ⊆ set Vs› have fv: "fv e ⊆ set (Vs@[V])" by auto
from ‹bisim Vs {V:T=vo; e} E2 xs› show ?case
proof(cases rule: bisim_cases(7)[consumes 1, case_names BlockNone BlockSome BlockSomeNone])
case (BlockNone E')
with red IH[of "Vs@[V]" E' xs] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h xs TA' e2' h' xs'"
and bisim': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto
from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
have "length (Vs@[V]) + max_vars e ≤ length xs'"
by(fastforce simp add: sim_move01_def dest: red1_preserves_len τred1t_preserves_len τred1r_preserves_len split: if_split_asm)
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
moreover
{ assume "V ∈ set Vs"
hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
with ‹bisim (Vs @ [V]) e E' xs› have "unmod E' (index Vs V)"
by -(rule hidden_bisim_unmod)
moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
have "index Vs V < length xs" by(auto intro: index_less_aux)
ultimately have "xs ! index Vs V = xs' ! index Vs V"
using sim_move01_preserves_unmod[OF red'] by(simp) }
moreover from red' have "length xs = length xs'" by(rule sim_move01_preserves_len[symmetric])
ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
by(auto intro: Block_lem)
show ?thesis
proof(cases "x' V")
case None
with red' bisim' BlockNone len
show ?thesis by(fastforce simp del: split_paired_Ex fun_upd_apply intro: rel)
next
case (Some v)
moreover
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v⌋"
by(auto simp add: map_le_def dest: bspec)
moreover
from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
ultimately have "xs' ! length Vs = v" using ‹length xs = length xs'› by(simp)
with red' bisim' BlockNone Some len
show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
qed
next
case (BlockSome E' v)
with red IH[of "Vs@[V]" E' "xs[length Vs := v]"] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h (xs[length Vs := v]) TA' e2' h' xs'"
and bisim': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto
from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
have "length (Vs@[V]) + max_vars e ≤ length xs'" by(auto dest: sim_move01_preserves_len)
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
moreover
{ assume "V ∈ set Vs"
hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
with ‹bisim (Vs @ [V]) e E' (xs[length Vs := v])› have "unmod E' (index Vs V)"
by -(rule hidden_bisim_unmod)
moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
have "index Vs V < length xs" by(auto intro: index_less_aux)
moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
have "(xs[length Vs := v]) ! index Vs V = xs ! index Vs V" by(simp)
ultimately have "xs ! index Vs V = xs' ! index Vs V"
using sim_move01_preserves_unmod[OF red', of "index Vs V"] by(simp) }
moreover from red' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
by(auto intro: Block_lem)
from BlockSome red obtain v' where Some: "x' V = ⌊v'⌋" by(auto dest!: red_lcl_incr)
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v'⌋"
by(auto simp add: map_le_def dest: bspec)
moreover
from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
ultimately have "xs' ! length Vs = v'" using ‹length xs = length xs'› by(simp)
with red' bisim' BlockSome Some ‹length Vs < length xs›
show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
next
case (BlockSomeNone E')
with red IH[of "Vs@[V]" E' xs] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h xs TA' e2' h' xs'"
and IH': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto
from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
have "length (Vs@[V]) + max_vars e ≤ length xs'" by(auto dest: sim_move01_preserves_len)
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
moreover
{ assume "V ∈ set Vs"
hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
with ‹bisim (Vs @ [V]) e E' xs› have "unmod E' (index Vs V)"
by -(rule hidden_bisim_unmod)
moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
have "index Vs V < length xs" by(auto intro: index_less_aux)
moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
have "(xs[length Vs := v]) ! index Vs V = xs ! index Vs V" by(simp)
ultimately have "xs ! index Vs V = xs' ! index Vs V"
using sim_move01_preserves_unmod[OF red', of "index Vs V"] by(simp) }
moreover from red' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
by(auto intro: Block_lem)
from BlockSomeNone red obtain v' where Some: "x' V = ⌊v'⌋" by(auto dest!: red_lcl_incr)
with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v'⌋"
by(auto simp add: map_le_def dest: bspec)
moreover
from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
ultimately have "xs' ! length Vs = v'" using ‹length xs = length xs'› by(simp)
with red' IH' BlockSomeNone Some ‹length Vs < length xs›
show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
qed
next
case (RedBlock V T vo u s Vs E2 xs)
from ‹bisim Vs {V:T=vo; Val u} E2 xs› obtain vo'
where [simp]: "E2 = {length Vs:T=vo'; Val u}" by auto
from RedBlock show ?case
proof(cases vo)
case (Some v)
with ‹bisim Vs {V:T=vo; Val u} E2 xs›
have vo': "case vo' of None ⇒ xs ! length Vs = v | Some v' ⇒ v = v'" by auto
have "sim_move01 (compP1 P) t ε {V:T=vo; Val u} E2 (hp s) xs ε (Val u) (hp s) (xs[length Vs := v])"
proof(cases vo')
case None with vo'
have "xs[length Vs := v] = xs" by auto
thus ?thesis using Some None by auto
next
case Some
from ‹length Vs + max_vars {V:T=vo; Val u} ≤ length xs› have "length Vs < length xs" by simp
with vo' Some show ?thesis using ‹vo = Some v› by auto
qed
thus ?thesis using RedBlock by fastforce
qed fastforce
next
case SynchronizedNull thus ?case by fastforce
next
case (LockSynchronized a e s Vs E2 xs)
from ‹bisim Vs (sync(addr a) e) E2 xs›
have E2: "E2 = sync⇘length Vs⇙ (addr a) (compE1 (Vs@[fresh_var Vs]) e)"
and sync: "¬ contains_insync e" by auto
moreover have "fresh_var Vs ∉ set Vs" by(rule fresh_var_fresh)
with ‹fv (sync(addr a) e) ⊆ set Vs› have "fresh_var Vs ∉ fv e" by auto
from E2 ‹fv (sync(addr a) e) ⊆ set Vs› sync
have "bisim (Vs@[fresh_var Vs]) e (compE1 (Vs@[fresh_var Vs]) e) (xs[length Vs := Addr a])"
by(auto intro!: compE1_bisim)
hence "bisim Vs (insync(a) e) (insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e)) (xs[length Vs := Addr a])"
using ‹fresh_var Vs ∉ fv e› ‹length Vs + max_vars (sync(addr a) e) ≤ length xs› by auto
moreover from ‹length Vs + max_vars (sync(addr a) e) ≤ length xs›
have "False,compP1 P,t ⊢1 ⟨sync⇘length Vs⇙ (addr a) (compE1 (Vs@[fresh_var Vs]) e), (hp s, xs)⟩
-⦃Lock→a, SyncLock a⦄→
⟨insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e), (hp s, xs[length Vs := Addr a])⟩"
by -(rule Lock1Synchronized, auto)
hence "sim_move01 (compP1 P) t ⦃Lock→a, SyncLock a⦄ (sync(addr a) e) E2 (hp s) xs ⦃Lock→a, SyncLock a⦄ (insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e)) (hp s) (xs[length Vs := Addr a])"
using E2 by(fastforce simp add: sim_move01_def ta_bisim_def)
moreover have "zip Vs (xs[length Vs := Addr a]) = (zip Vs xs)[length Vs := (arbitrary, Addr a)]"
by(rule sym)(simp add: update_zip)
hence "zip Vs (xs[length Vs := Addr a]) = zip Vs xs" by simp
with ‹lcl s ⊆⇩m [Vs [↦] xs]› have "lcl s ⊆⇩m [Vs [↦] xs[length Vs := Addr a]]"
by(auto simp add: map_le_def map_upds_def)
ultimately show ?case using ‹lcl s ⊆⇩m [Vs [↦] xs]› by fastforce
next
case (SynchronizedRed2 e s ta e' s' a Vs E2 xs)
note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
from ‹bisim Vs (insync(a) e) E2 xs› obtain E
where E2: "E2 = insync⇘length Vs⇙ (a) E" and bisim: "bisim (Vs@[fresh_var Vs]) e E xs"
and xsa: "xs ! length Vs = Addr a" by auto
from ‹fv (insync(a) e) ⊆ set Vs› fresh_var_fresh[of Vs] have fv: "fresh_var Vs ∉ fv e" by auto
from ‹length Vs + max_vars (insync(a) e) ≤ length xs› have "length Vs < length xs" by simp
{ assume "lcl s (fresh_var Vs) ≠ None"
then obtain v where "lcl s (fresh_var Vs) = ⌊v⌋" by auto
with ‹lcl s ⊆⇩m [Vs [↦] xs]› have "[Vs [↦] xs] (fresh_var Vs) = ⌊v⌋"
by(auto simp add: map_le_def dest: bspec)
hence "fresh_var Vs ∈ set Vs"
by(auto simp add: map_upds_def set_zip dest!: map_of_SomeD )
moreover have "fresh_var Vs ∉ set Vs" by(rule fresh_var_fresh)
ultimately have False by contradiction }
hence "lcl s (fresh_var Vs) = None" by(cases "lcl s (fresh_var Vs)", auto)
hence "(lcl s)(fresh_var Vs := None) = lcl s" by(auto intro: ext)
moreover from ‹lcl s ⊆⇩m [Vs [↦] xs]›
have "(lcl s)(fresh_var Vs := None) ⊆⇩m [Vs [↦] xs, fresh_var Vs ↦ xs ! length Vs]" by(simp)
ultimately have "lcl s ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs]"
using ‹length Vs < length xs› by(auto)
with IH[of "Vs@[fresh_var Vs]" E xs] ‹fv (insync(a) e) ⊆ set Vs› bisim
‹length Vs + max_vars (insync(a) e) ≤ length xs› ‹?synth (insync(a) e) s›
obtain TA' e2' xs' where IH': "sim_move01 (compP1 P) t ta e E (hp s) xs TA' e2' (hp s') xs'"
"bisim (Vs @ [fresh_var Vs]) e' e2' xs'" "lcl s' ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs']" by auto
from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "dom (lcl s') ⊆ dom (lcl s) ∪ fv e" by(auto dest: red_dom_lcl)
with fv ‹lcl s (fresh_var Vs) = None› have "(fresh_var Vs) ∉ dom (lcl s')" by auto
hence "lcl s' (fresh_var Vs) = None" by auto
moreover from IH' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
moreover note ‹lcl s' ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs']› ‹length Vs < length xs›
ultimately have "lcl s' ⊆⇩m [Vs [↦] xs']" by(auto simp add: map_le_def dest: bspec)
moreover from bisim fv have "unmod E (length Vs)" by(auto intro: bisim_fv_unmod)
with IH' ‹length Vs < length xs› have "xs ! length Vs = xs' ! length Vs"
by(auto dest!: sim_move01_preserves_unmod)
with xsa have "xs' ! length Vs = Addr a" by simp
ultimately show ?case using IH' E2 by(fastforce)
next
case (UnlockSynchronized a v s Vs E2 xs)
from ‹bisim Vs (insync(a) Val v) E2 xs› have E2: "E2 = insync⇘length Vs⇙ (a) Val v"
and xsa: "xs ! length Vs = Addr a" by auto
moreover from ‹length Vs + max_vars (insync(a) Val v) ≤ length xs› xsa
have "False,compP1 P,t ⊢1 ⟨insync⇘length Vs⇙ (a) (Val v), (hp s, xs)⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Val v, (hp s, xs)⟩"
by-(rule Unlock1Synchronized, auto)
hence "sim_move01 (compP1 P) t ⦃Unlock→a, SyncUnlock a⦄ (insync(a) Val v) (insync⇘length Vs⇙ (a) Val v) (hp s) xs ⦃Unlock→a, SyncUnlock a⦄ (Val v) (hp s) xs"
by(fastforce simp add: sim_move01_def ta_bisim_def)
ultimately show ?case using ‹lcl s ⊆⇩m [Vs [↦] xs]› by fastforce
next
case (RedWhile b c s Vs E2 xs)
from ‹bisim Vs (while (b) c) E2 xs› have "E2 = while (compE1 Vs b) (compE1 Vs c)"
and sync: "¬ contains_insync b" "