# Theory DRF_J

```(*  Title:      JinjaThreads/MM/DRF_J.thy
Author:     Andreas Lochbihler
*)

section ‹JMM Instantiation for J›

theory DRF_J
imports
JMM_Common
JMM_J
SC_Legal
begin

where
"ka (new C) = {}"
| "ka (newA T⌊e⌉) = ka e"
| "ka (Cast T e) = ka e"
| "ka (e instanceof T) = ka e"
| "ka (Val v) = ka_Val v"
| "ka (Var V) = {}"
| "ka (e1 «bop» e2) = ka e1 ∪ ka e2"
| "ka (V := e) = ka e"
| "ka (a⌊e⌉) = ka a ∪ ka e"
| "ka (a⌊e⌉ := e') = ka a ∪ ka e ∪ ka e'"
| "ka (a∙length) = ka a"
| "ka (e∙F{D}) = ka e"
| "ka (e∙F{D} := e') = ka e ∪ ka e'"
| "ka (e∙compareAndSwap(D∙F, e', e'')) = ka e ∪ ka e' ∪ ka e''"
| "ka (e∙M(es)) = ka e ∪ kas es"
| "ka {V:T=vo; e} = ka e ∪ (case vo of None ⇒ {} | Some v ⇒ ka_Val v)"
| "ka (Synchronized x e e') = ka e ∪ ka e'"
| "ka (InSynchronized x a e) = insert a (ka e)"
| "ka (e;; e') = ka e ∪ ka e'"
| "ka (if (e) e1 else e2) = ka e ∪ ka e1 ∪ ka e2"
| "ka (while (b) e) = ka b ∪ ka e"
| "ka (throw e) = ka e"
| "ka (try e catch(C V) e') = ka e ∪ ka e'"

| "kas [] = {}"
| "kas (e # es) = ka e ∪ kas es"

where "ka_locals xs = {a. Addr a ∈ ran xs}"

lemma ka_Val_subset_ka_locals:
"xs V = ⌊v⌋ ⟹ ka_Val v ⊆ ka_locals xs"
by(cases v)(auto simp add: ka_locals_def ran_def)

lemma ka_locals_update_subset:
"ka_locals (xs(V := None)) ⊆ ka_locals xs"
"ka_locals (xs(V ↦ v)) ⊆ ka_Val v ∪ ka_locals xs"

lemma ka_locals_empty [simp]: "ka_locals Map.empty = {}"

lemma kas_append [simp]: "kas (es @ es') = kas es ∪ kas es'"
by(induct es) auto

lemma kas_map_Val [simp]: "kas (map Val vs) = ⋃(ka_Val ` set vs)"
by(induct vs) auto

lemma ka_blocks:
"⟦ length pns = length Ts; length vs = length Ts ⟧
⟹ ka (blocks pns Ts vs body) = ⋃(ka_Val ` set vs) ∪ ka body"
by(induct pns Ts vs body rule: blocks.induct)(auto)

lemma WT_ka: "P,E ⊢ e :: T ⟹ ka e = {}"
and WTs_kas: "P,E ⊢ es [::] Ts ⟹ kas es = {}"
by(induct rule: WT_WTs.inducts)(auto simp add: typeof_ka)

context J_heap_base begin

lemma assumes wf: "wf_J_prog P"
and ok: "start_heap_ok"
"P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ J_known_addrs t (e', lcl s') ⊆ J_known_addrs t (e, lcl s) ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
"P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ kas es' ∪ ka_locals (lcl s') ⊆ insert (thread_id2addr t) (kas es ∪ ka_locals (lcl s)) ∪ new_obs_addrs ⦃ta⦄⇘o⇙ ∪ set start_addrs"
proof(induct rule: red_reds.inducts)
case RedVar thus ?case by(auto dest: ka_Val_subset_ka_locals)
next
case RedLAss thus ?case by(auto simp add: ka_locals_def ran_def)
next
case RedBinOp thus ?case by(auto dest: binop_known_addrs[OF ok])
next
case RedBinOpFail thus ?case by(auto dest: binop_known_addrs[OF ok])
next
case RedCall thus ?case
next
case (RedCallExternal s a T M Ts T D vs ta va h') thus ?case
next
case (BlockRed e h l V vo ta e' h' l')
thus ?case using ka_locals_update_subset[where xs = l and V=V] ka_locals_update_subset[where xs = l' and V=V]
apply(cases "l V")
apply(auto simp del: fun_upd_apply del: subsetI)
apply(blast dest: ka_Val_subset_ka_locals)+
done

"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧ ⟹ ad ∈ J_known_addrs t (e, lcl s)"
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
proof(induct rule: red_reds.inducts)
next
case (BlockRed e h l V vo ta e' h' l')
thus ?case using ka_locals_update_subset[where xs = l and V=V] ka_locals_update_subset[where xs = l' and V=V]
by(auto simp del: fun_upd_apply)
qed(simp_all, blast+)

"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; ⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr a); n < length ⦃ta⦄⇘o⇙ ⟧
⟹ a ∈ J_known_addrs t (e, lcl s) ∨ a ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; ⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr a); n < length ⦃ta⦄⇘o⇙ ⟧
proof(induct rule: red_reds.inducts)
case RedCASSucceed thus ?case by(auto simp add: nth_Cons split: nat.split_asm)
next
case RedCallExternal thus ?case by simp (blast dest: red_external_known_addrs_WriteMem)
next
case (BlockRed e h l V vo ta e' h' l')
thus ?case using ka_locals_update_subset[where xs = l and V=V] ka_locals_update_subset[where xs = l' and V=V]
by(auto simp del: fun_upd_apply)
qed(simp_all, blast+)

end

context J_heap begin

lemma
assumes wf: "wf_J_prog P"
and ok: "start_heap_ok"
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewThread t' x' h' ∈ set ⦃ta⦄⇘t⇙ ⟧
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t' x' h' ∈ set ⦃ta⦄⇘t⇙ ⟧
proof(induct rule: red_reds.inducts)
case RedCallExternal thus ?case
apply clarsimp
apply clarsimp

apply simp
apply clarsimp
apply(auto 4 4 dest: sees_wf_mdecl[OF wf] WT_ka simp add: wf_mdecl_def)
done
next
case (BlockRed e h l V vo ta e' h' l')
thus ?case using ka_locals_update_subset[where xs = l and V=V] ka_locals_update_subset[where xs = l' and V=V]
by(cases "l V")(auto simp del: fun_upd_apply)
qed(simp_all, blast+)

"⟦ convert_extTA extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩;
⦃ta⦄⇘o⇙ ! i = NewHeapElem a x; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a x'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
"⟦ convert_extTA extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩;
⦃ta⦄⇘o⇙ ! i = NewHeapElem a x; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a x'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
apply(induct rule: red_reds.inducts)
done

end

locale J_allocated_heap = allocated_heap +
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"

sublocale J_allocated_heap < J_heap
by(unfold_locales)

context J_allocated_heap begin

lemma red_allocated_mono: "P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ allocated (hp s) ⊆ allocated (hp s')"
and reds_allocated_mono: "P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ allocated (hp s) ⊆ allocated (hp s')"
by(induct rule: red_reds.inducts)(auto dest: allocate_allocatedD heap_write_allocated_same red_external_allocated_mono del: subsetI)

lemma red_allocatedD:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧ ⟹ ad ∈ allocated (hp s') ∧ ad ∉ allocated (hp s)"
and reds_allocatedD:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧ ⟹ ad ∈ allocated (hp s') ∧ ad ∉ allocated (hp s)"
by(induct rule: red_reds.inducts)(auto dest: allocate_allocatedD heap_write_allocated_same red_external_allocatedD)

lemma red_allocated_NewHeapElemD:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; ad ∈ allocated (hp s'); ad ∉ allocated (hp s) ⟧ ⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
and reds_allocated_NewHeapElemD:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; ad ∈ allocated (hp s'); ad ∉ allocated (hp s) ⟧ ⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
by(induct rule: red_reds.inducts)(auto dest: allocate_allocatedD heap_write_allocated_same red_external_NewHeapElemD)

proof
fix t x m ta x' m'
assume "mred P t (x, m) ta (x', m')"
thus "allocated m ⊆ allocated m'"
by(auto dest: red_allocated_mono del: subsetI simp add: split_beta)
next
fix x t m ta x' m' ad CTn
assume "mred P t (x, m) ta (x', m')"
and "NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
by(auto dest: red_allocatedD simp add: split_beta)
next
fix t x m ta x' m' ad
assume "mred P t (x, m) ta (x', m')"
thus "∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
by(auto dest: red_allocated_NewHeapElemD simp add: split_beta)
next
fix t x m ta x' m' i a CTn j CTn'
assume "mred P t (x, m) ta (x', m')"
and "⦃ta⦄⇘o⇙ ! i = NewHeapElem a CTn" "i < length ⦃ta⦄⇘o⇙"
and "⦃ta⦄⇘o⇙ ! j = NewHeapElem a CTn'" "j < length ⦃ta⦄⇘o⇙"
qed

end

spurious_wakeups
final_expr "mred P"
P

context J_allocated_heap begin

assumes wf: "wf_J_prog P"
and ok: "start_heap_ok"
proof
fix t x m ta x' m'
assume "mred P t (x, m) ta (x', m')"
next
fix t x m ta x' m' t' x'' m''
assume "mred P t (x, m) ta (x', m')"
and "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
next
fix t x m ta x' m' ad al v
assume "mred P t (x, m) ta (x', m')"
next
assume "mred P t (x, m) ta (x', m')"
qed

end

context J_heap begin

"⟦ convert_extTA extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,E,hp s ⊢ e : T; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ∃T'. P,hp s ⊢ ad@al : T'"
"⟦ convert_extTA extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; P,E,hp s ⊢ es [:] Ts; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ∃T'. P,hp s ⊢ ad@al : T'"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
case RedAAcc thus ?case
next
case RedFAcc thus ?case
next
case RedCASSucceed thus ?case
next
case RedCASFail thus ?case
next
case RedCallExternal thus ?case
qed auto

end

primrec new_types :: "('a, 'b, 'addr) exp ⇒ ty set"
and new_typess :: "('a, 'b, 'addr) exp list ⇒ ty set"
where
"new_types (new C) = {Class C}"
| "new_types (newA T⌊e⌉) = insert (T⌊⌉) (new_types e)"
| "new_types (Cast T e) = new_types e"
| "new_types (e instanceof T) = new_types e"
| "new_types (Val v) = {}"
| "new_types (Var V) = {}"
| "new_types (e1 «bop» e2) = new_types e1 ∪ new_types e2"
| "new_types (V := e) = new_types e"
| "new_types (a⌊e⌉) = new_types a ∪ new_types e"
| "new_types (a⌊e⌉ := e') = new_types a ∪ new_types e ∪ new_types e'"
| "new_types (a∙length) = new_types a"
| "new_types (e∙F{D}) = new_types e"
| "new_types (e∙F{D} := e') = new_types e ∪ new_types e'"
| "new_types (e∙compareAndSwap(D∙F, e', e'')) = new_types e ∪ new_types e' ∪ new_types e''"
| "new_types (e∙M(es)) = new_types e ∪ new_typess es"
| "new_types {V:T=vo; e} = new_types e"
| "new_types (Synchronized x e e') = new_types e ∪ new_types e'"
| "new_types (InSynchronized x a e) = new_types e"
| "new_types (e;; e') = new_types e ∪ new_types e'"
| "new_types (if (e) e1 else e2) = new_types e ∪ new_types e1 ∪ new_types e2"
| "new_types (while (b) e) = new_types b ∪ new_types e"
| "new_types (throw e) = new_types e"
| "new_types (try e catch(C V) e') = new_types e ∪ new_types e'"

| "new_typess [] = {}"
| "new_typess (e # es) = new_types e ∪ new_typess es"

lemma new_types_blocks:
"⟦ length pns = length Ts; length vs = length Ts ⟧ ⟹ new_types (blocks pns vs Ts e) = new_types e"
apply(induct rule: blocks.induct)
apply(simp_all)
done

context J_heap_base begin

lemma WTrt_new_types_types: "P,E,h ⊢ e : T ⟹ new_types e ⊆ types P"
and WTrts_new_typess_types: "P,E,h ⊢ es [:] Ts ⟹ new_typess es ⊆ types P"
by(induct rule: WTrt_WTrts.inducts) simp_all

end

lemma WT_new_types_types: "P,E ⊢ e :: T ⟹ new_types e ⊆ types P"
and WTs_new_typess_types: "P,E ⊢ es [::] Ts ⟹ new_typess es ⊆ types P"
by(induct rule: WT_WTs.inducts) simp_all

context J_heap_conf begin

"⟦ convert_extTA extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; new_types e ⊆ types P; hconf (hp s); NewHeapElem a x ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ typeof_addr (hp s') a = Some x"
"⟦ convert_extTA extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; new_typess es ⊆ types P; hconf (hp s); NewHeapElem a x ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ typeof_addr (hp s') a = Some x"
apply(induct rule: red_reds.inducts)
done

proof -
spurious_wakeups
P
show ?thesis by(unfold_locales)
qed

lemma red_non_speculative_vs_conf:
"⟦ convert_extTA extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,E,hp s ⊢ e : T;
non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙))); vs_conf P (hp s) vs; hconf (hp s) ⟧
⟹ vs_conf P (hp s') (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
and reds_non_speculative_vs_conf:
"⟦ convert_extTA extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; P,E,hp s ⊢ es [:] Ts;
non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙))); vs_conf P (hp s) vs; hconf (hp s) ⟧
⟹ vs_conf P (hp s') (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
case (RedAAss h a U n i w V h' xs)
from ‹sint i < int n› ‹0 <=s i› have "nat (sint i) < n"
with ‹typeof_addr h a = ⌊Array_type U n⌋› have "P,h ⊢ a@ACell (nat (sint i)) : U"
moreover from ‹heap_write h a (ACell (nat (sint i))) w h'› have "h ⊴ h'" by(rule hext_heap_write)
ultimately have "P,h' ⊢ a@ACell (nat (sint i)) : U" by(rule addr_loc_type_hext_mono)
moreover from ‹typeof⇘h⇙ w = ⌊V⌋› ‹P ⊢ V ≤ U› have "P,h ⊢ w :≤ U" by(simp add: conf_def)
with ‹h ⊴ h'› have "P,h' ⊢ w :≤ U" by(rule conf_hext)
ultimately have "∃T. P,h' ⊢ a@ACell (nat (sint i)) : T ∧ P,h' ⊢ w :≤ T" by blast
thus ?case using RedAAss
by(auto intro!: vs_confI split: if_split_asm dest: vs_confD simp add: take_Cons')(blast dest: vs_confD hext_heap_write intro: addr_loc_type_hext_mono conf_hext)+
next
case (RedFAss h e D F v h' xs)
hence "∃T. P,h' ⊢ e@CField D F : T ∧ P,h' ⊢ v :≤ T"
thus ?case using RedFAss
by(auto intro!: vs_confI simp add: take_Cons' split: if_split_asm dest: vs_confD)(blast dest: vs_confD hext_heap_write intro: addr_loc_type_hext_mono conf_hext)+
next
case (RedCASSucceed h a D F v v' h' l)
hence "∃T. P,h' ⊢ a@CField D F : T ∧ P,h' ⊢ v' :≤ T"
thus ?case using RedCASSucceed
by(auto simp add: take_Cons' split: if_split_asm dest: vs_confD intro!: vs_confI)
(blast dest: vs_confD hext_heap_write intro: addr_loc_type_hext_mono conf_hext)+
next
case RedCallExternal thus ?case by(auto intro: red_external_non_speculative_vs_conf)
qed(auto dest: vs_conf_allocate hext_allocate intro: vs_conf_hext simp add: take_Cons')

lemma red_non_speculative_typeable:
"⟦ convert_extTA extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,E,hp s ⊢ e : T;
non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)); vs_conf P (hp s) vs; hconf (hp s) ⟧
and reds_non_speculative_typeable:
"⟦ convert_extTA extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; P,E,hp s ⊢ es [:] Ts;
non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)); vs_conf P (hp s) vs; hconf (hp s) ⟧
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
case RedCall thus ?case by(blast intro: J_heap_base.red_reds.RedCall)
next
case RedCallExternal thus ?case
by(auto intro: J_heap_base.red_reds.RedCallExternal red_external_non_speculative_typeable)

end

sublocale J_heap_base < red_mthr:
final_expr
"mred P"
convert_RA
for P
by(unfold_locales)

locale J_allocated_heap_conf =
J_heap_conf
spurious_wakeups
P
+
J_allocated_heap
spurious_wakeups
allocated
P
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and hconf :: "'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
begin

assumes wf: "wf_J_prog P"
and ok: "start_heap_ok"
proof -
spurious_wakeups
final_expr "mred P" P

show ?thesis
proof
fix t x m ta x' m'
assume "mred P t (x, m) ta (x', m')"
thus "m ⊴ m'" by(auto dest: red_hext_incr simp add: split_beta)
next
fix t x m ta x' m' vs
assume red: "mred P t (x, m) ta (x', m')"
and ts_ok: "∃ET. sconf_type_ok ET t x m"
and vs: "vs_conf P m vs"
and ns: "non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙))"

have lift: "lifting_inv final_expr ?mred sconf_type_ok"
moreover
from ts_ok obtain ET where type: "sconf_type_ok ET t x m" ..
with red vs ns have red': "?mred t (x, m) ta (x', m')"
by(auto simp add: split_beta sconf_type_ok_def sconf_def type_ok_def dest: red_non_speculative_typeable)
ultimately have "sconf_type_ok ET t x' m'" using type
by(rule lifting_inv.invariant_red[where r="?mred"])
thus "∃ET. sconf_type_ok ET t x' m'" ..
{ fix t'' x'' m''
assume New: "NewThread t'' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
with red have "m'' = snd (x', m')" by(rule red_mthr.new_thread_memory)
with lift red' type New
show "∃ET. sconf_type_ok ET t'' x'' m''"
{ fix t'' x''
assume "∃ET. sconf_type_ok ET t'' x'' m"
with lifting_inv.invariant_other[where r="?mred", OF lift red' type]
show "∃ET. sconf_type_ok ET t'' x'' m'" by blast }
next
fix t x m ta x' m' vs n
assume red: "mred P t (x, m) ta (x', m')"
and ts_ok: "∃ET. sconf_type_ok ET t x m"
and vs: "vs_conf P m vs"
and ns: "non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
thus "vs_conf P m' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
by(cases x)(auto dest: red_non_speculative_vs_conf simp add: sconf_type_ok_def type_ok_def sconf_def)
next
fix t x m ta x' m' ad al v
assume "mred P t (x, m) ta (x', m')"
and "∃ET. sconf_type_ok ET t x m"
thus "∃T. P,m ⊢ ad@al : T"
next
fix t x m ta x' m' ad hT
assume "mred P t (x, m) ta (x', m')"
and "∃ET. sconf_type_ok ET t x m"
and "NewHeapElem ad hT ∈ set ⦃ta⦄⇘o⇙"
by(auto dest: red_New_typeof_addrD[where x="hT"] dest!: WTrt_new_types_types simp add: split_beta sconf_type_ok_def sconf_def type_ok_def)
qed
qed

end

context J_allocated_heap_conf begin

lemma executions_sc:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and vs2: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "executions_sc_hb (J_ℰ P C M vs status) P"
(is "executions_sc_hb ?E P")
proof -
from wf_start obtain Ts T pns body D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T=⌊(pns, body)⌋ in D"
and vs1: "P,start_heap ⊢ vs [:≤] Ts" by cases auto

spurious_wakeups
final_expr "mred P" "λt x h. ∃ET. sconf_type_ok ET t x h" P

from wf_prog_wf_syscls[OF wf] J_start_state_sconf_type_ok[OF wf wf_start]
show ?thesis
proof(rule executions_sc_hb)
from wf sees have "wf_mdecl wf_J_mdecl P D (M, Ts, T, ⌊(pns, body)⌋)" by(rule sees_wf_mdecl)
then obtain T' where len1: "length pns = length Ts" and wt: "P,[this↦Class D,pns [↦] Ts] ⊢ body :: T'"
from vs1 have len2: "length vs = length Ts" by(rule list_all2_lengthD)
show "J_known_addrs start_tid ((λ(pns, body) vs. (blocks (this # pns) (Class (fst (method P C M)) # fst (snd (method P C M))) (Null # vs) body, Map.empty)) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using sees vs2 len1 len2 WT_ka[OF wt]
qed
qed

end

declare split_paired_Ex [simp del]

context J_progress begin

lemma ex_WTrt_simps:
"P,E,h ⊢ e : T ⟹ ∃E T. P,E,h ⊢ e : T"
by blast

lemma assumes hrt: "heap_read_typeable hconf P"
and vs: "vs_conf P (shr s) vs"
and hconf: "hconf (shr s)"
"⟦ P,t ⊢ ⟨e, (shr s, xs)⟩ -ta→ ⟨e', (h', xs')⟩; ∃E T. P,E,shr s ⊢ e : T;
red_mthr.mthr.if.actions_ok s t ta;
I < length ⦃ta⦄⇘o⇙; ⦃ta⦄⇘o⇙ ! I = ReadMem a'' al'' v; v' ∈ w_values P vs (map NormalAction (take I ⦃ta⦄⇘o⇙)) (a'', al'');
non_speculative P vs (llist_of (map NormalAction (take I ⦃ta⦄⇘o⇙))) ⟧
⟹ ∃ta' e'' xs'' h''. P,t ⊢ ⟨e, (shr s, xs)⟩ -ta'→ ⟨e'', (h'', xs'')⟩ ∧
red_mthr.mthr.if.actions_ok s t ta' ∧
I < length ⦃ta'⦄⇘o⇙ ∧ take I ⦃ta'⦄⇘o⇙ = take I ⦃ta⦄⇘o⇙ ∧
⦃ta'⦄⇘o⇙ ! I = ReadMem a'' al'' v' ∧ length ⦃ta'⦄⇘o⇙ ≤ max J_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
"⟦ P,t ⊢ ⟨es, (shr s, xs)⟩ [-ta→] ⟨es', (h', xs')⟩; ∃E Ts. P,E,shr s ⊢ es [:] Ts;
red_mthr.mthr.if.actions_ok s t ta;
I < length ⦃ta⦄⇘o⇙; ⦃ta⦄⇘o⇙ ! I = ReadMem a'' al'' v; v' ∈ w_values P vs (map NormalAction (take I ⦃ta⦄⇘o⇙)) (a'', al'');
non_speculative P vs (llist_of (map NormalAction (take I ⦃ta⦄⇘o⇙))) ⟧
⟹ ∃ta' es'' xs'' h''. P,t ⊢ ⟨es, (shr s, xs)⟩ [-ta'→] ⟨es'', (h'', xs'')⟩ ∧
red_mthr.mthr.if.actions_ok s t ta' ∧
I < length ⦃ta'⦄⇘o⇙ ∧ take I ⦃ta'⦄⇘o⇙ = take I ⦃ta⦄⇘o⇙ ∧
⦃ta'⦄⇘o⇙ ! I = ReadMem a'' al'' v' ∧ length ⦃ta'⦄⇘o⇙ ≤ max J_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
proof(induct e hxs≡"(shr s, xs)" ta e' hxs'≡"(h', xs')"
and es hxs≡"(shr s, xs)" ta es' hxs'≡"(h', xs')"
arbitrary: xs xs' and xs xs' rule: red_reds.inducts)
case (RedAAcc a U n i v e)
hence [simp]: "I = 0" "al'' = ACell (nat (sint i))" "a'' = a"
and v': "v' ∈ vs (a, ACell (nat (sint i)))" by simp_all
from RedAAcc have adal: "P,shr s ⊢ a@ACell (nat (sint i)) : U"
from v' vs adal have "P,shr s ⊢ v' :≤ U" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with hrt adal have "heap_read (shr s) a (ACell (nat (sint i))) v'" using hconf by(rule heap_read_typeableD)
with ‹typeof_addr (shr s) a = ⌊Array_type U n⌋› ‹0 <=s i› ‹sint i < int n›
‹red_mthr.mthr.if.actions_ok s t ⦃ReadMem a (ACell (nat (sint i))) v⦄›
show ?case by(fastforce intro: red_reds.RedAAcc)
next
case (RedFAcc a D F v)
hence [simp]: "I = 0" "al'' = CField D F" "a'' = a"
and v': "v' ∈ vs (a, CField D F)" by simp_all
from RedFAcc obtain E T where "P,E,shr s ⊢ addr a∙F{D} : T" by blast
with RedFAcc have adal: "P,shr s ⊢ a@CField D F : T" by(auto 4 4 intro: addr_loc_type.intros)
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with ‹red_mthr.mthr.if.actions_ok s t ⦃ReadMem a (CField D F) v⦄›
show ?case by(fastforce intro: red_reds.RedFAcc)
next
case (RedCASSucceed a D F v'' v''')
hence [simp]: "I = 0" "al'' = CField D F" "a'' = a" "v'' = v"
and v': "v' ∈ vs (a, CField D F)" by(auto simp add: take_Cons' split: if_split_asm)
from RedCASSucceed.prems(1) obtain E T where
"P,E,shr s ⊢ addr a∙compareAndSwap(D∙F, Val v'', Val v''') : T" by clarify
then obtain T where adal: "P,shr s ⊢ a@CField D F : T"
and v'': "P,shr s ⊢ v'' :≤ T" and v''': "P,shr s ⊢ v''' :≤ T"
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
show ?case
proof(cases "v' = v''")
case True
then show ?thesis using RedCASSucceed
by(fastforce intro: red_reds.RedCASSucceed)
next
case False
then show ?thesis using read RedCASSucceed
by(fastforce intro: RedCASFail)
qed
next
case (RedCASFail a D F v'' v''' v'''')
hence [simp]: "I = 0" "al'' = CField D F" "a'' = a" "v'' = v"
and v': "v' ∈ vs (a, CField D F)" by(auto simp add: take_Cons' split: if_split_asm)
from RedCASFail.prems(1) obtain E T where
"P,E,shr s ⊢ addr a∙compareAndSwap(D∙F, Val v''', Val v'''') : T" by(iprover)
then obtain T where adal: "P,shr s ⊢ a@CField D F : T"
and v''': "P,shr s ⊢ v''' :≤ T" and v'''': "P,shr s ⊢ v'''' :≤ T"
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
show ?case
proof(cases "v' = v'''")
case True
from heap_write_total[OF hconf adal v''''] obtain h' where
"heap_write (shr s) a (CField D F) v'''' h'" ..
with read RedCASFail True show ?thesis
by(fastforce intro: RedCASSucceed)
next
case False
with read RedCASFail show ?thesis by(fastforce intro: red_reds.RedCASFail)
qed
next
case (RedCallExternal a U M Ts Tr D ps ta' va h' ta e')
from ‹P,t ⊢ ⟨a∙M(ps),hp (shr s, xs)⟩ -ta'→ext ⟨va,h'⟩›
have red: "P,t ⊢ ⟨a∙M(ps),shr s⟩ -ta'→ext ⟨va,h'⟩" by simp
from RedCallExternal have aok: "red_mthr.mthr.if.actions_ok s t ta'" by simp
from RedCallExternal have "I < length ⦃ta'⦄⇘o⇙"
and "⦃ta'⦄⇘o⇙ ! I = ReadMem a'' al'' v"
and "v' ∈ w_values P vs (map NormalAction (take I ⦃ta'⦄⇘o⇙)) (a'', al'')"
and "non_speculative P vs (llist_of (map NormalAction (take I ⦃ta'⦄⇘o⇙)))" by simp_all
from red_external_non_speculative_read[OF hrt vs red aok hconf this]
‹typeof_addr (hp (shr s, xs)) a = ⌊U⌋›
‹P ⊢ class_type_of U sees M: Ts→Tr = Native in D› ‹ta = extTA2J P ta'›
‹I < length ⦃ta⦄⇘o⇙›
show ?case by(fastforce intro: red_reds.RedCallExternal)
next
case NewArrayRed thus ?case by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.NewArrayRed)
next
case CastRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CastRed)
next
case InstanceOfRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.InstanceOfRed)
next
case BinOpRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.BinOpRed1)
next
case BinOpRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.BinOpRed2)
next
case LAssRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.LAssRed)
next
case AAccRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.AAccRed1)
next
case AAccRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.AAccRed2)
next
case AAssRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.AAssRed1)
next
case AAssRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.AAssRed2)
next
case AAssRed3 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.AAssRed3)+
next
case ALengthRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.ALengthRed)
next
case FAccRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.FAccRed)
next
case FAssRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.FAssRed1)
next
case FAssRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.FAssRed2)
next
case CASRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CASRed1)
next
case CASRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CASRed2)
next
case CASRed3 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CASRed3)
next
case CallObj thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CallObj)
next
case CallParams thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CallParams)
next
case BlockRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(fastforce intro: red_reds.BlockRed)+
next
case SynchronizedRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.SynchronizedRed1)
next
case SynchronizedRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.SynchronizedRed2)
next
case SeqRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.SeqRed)
next
case CondRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.CondRed)
next
case ThrowRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.ThrowRed)
next
case TryRed thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.TryRed)
next
case ListRed1 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.ListRed1)
next
case ListRed2 thus ?case
by(clarsimp simp add: split_paired_Ex ex_WTrt_simps)(blast intro: red_reds.ListRed2)
qed(simp_all)

end

final_expr "mred P" convert_RA
.

declare split_paired_Ex [simp]
declare eq_upto_seq_inconsist_simps [simp del]

locale J_allocated_progress =
J_progress
spurious_wakeups
P
+
J_allocated_heap_conf
spurious_wakeups
allocated
P
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and hconf :: "'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
begin

assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
(init_fin_lift_state status (J_start_state P C M vs))
(w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)))"
fix ttas s' t x ta x' m' i ad al v v'
assume τRed: "red_mthr.mthr.if.RedT P ?start_state ttas s'"
and sc: "non_speculative P ?start_vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and ts't: "thr s' t = ⌊(x, no_wait_locks)⌋"
and red: "red_mthr.init_fin P t (x, shr s') ta (x', m')"
and aok: "red_mthr.mthr.if.actions_ok s' t ta"
and i: "i < length ⦃ta⦄⇘o⇙"
and ns': "non_speculative P (w_values P ?start_vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙))"
and v': "v' ∈ w_values P ?start_vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al)"

from wf_start obtain Ts T pns body D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊(pns, body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases auto

let ?conv = "λttas. concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)"
let ?vs' = "w_values P ?start_vs (?conv ttas)"
let ?wt_ok = "init_fin_lift_inv sconf_type_ok"
let ?ET_start = "J_sconf_type_ET_start P C M"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
let ?start_state = "init_fin_lift_state status (J_start_state P C M vs)"

spurious_wakeups
final_expr "mred P" "λt x h. ∃ET. sconf_type_ok ET t x h" P

from wf sees have "wf_mdecl wf_J_mdecl P D (M, Ts, T, ⌊(pns, body)⌋)" by(rule sees_wf_mdecl)
then obtain T' where len1: "length pns = length Ts" and wt: "P,[this↦Class D,pns [↦] Ts] ⊢ body :: T'"
from conf have len2: "length vs = length Ts" by(rule list_all2_lengthD)

from wf wf_start have ts_ok_start: "ts_ok (init_fin_lift (λt x h. ∃ET. sconf_type_ok ET t x h)) (thr ?start_state) (shr ?start_state)"
unfolding ts_ok_init_fin_lift_init_fin_lift_state shr_start_state by(rule J_start_state_sconf_type_ok)
have sc': "non_speculative P ?start_vs (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of ttas))))"
using sc by(simp add: lmap_lconcat llist.map_comp o_def split_def lconcat_llist_of[symmetric])

from start_state_vs_conf[OF wf_prog_wf_syscls[OF wf]]
have vs_conf_start: "vs_conf P (shr ?start_state) ?start_vs"
with τRed ts_ok_start sc
have wt': "ts_ok (init_fin_lift (λt x h. ∃ET. sconf_type_ok ET t x h)) (thr s') (shr s')"
and vs': "vs_conf P (shr s') ?vs'" by(rule if_RedT_non_speculative_invar)+

from red i read obtain e xs e' xs' ta'
where x: "x = (Running, e, xs)" and x': "x' = (Running, e', xs')"
and ta: "ta = convert_TA_initial (convert_obs_initial ta')"
and red': "P,t ⊢ ⟨e, (shr s', xs)⟩ -ta'→ ⟨e', (m', xs')⟩"
by cases fastforce+

from ts't wt' x obtain E T where wte: "P,E,shr s' ⊢ e : T"
and hconf: "hconf (shr s')"
by(auto dest!: ts_okD simp add: sconf_type_ok_def sconf_def type_ok_def)

have aok': "red_mthr.mthr.if.actions_ok s' t ta'" using aok unfolding ta by simp

from i read v' ta ns' have "i < length ⦃ta'⦄⇘o⇙" and "⦃ta'⦄⇘o⇙ ! i = ReadMem ad al v"
and "v' ∈ w_values P ?vs' (map NormalAction (take i ⦃ta'⦄⇘o⇙)) (ad, al)"
and "non_speculative P ?vs' (llist_of (map NormalAction (take i ⦃ta'⦄⇘o⇙)))"

from red_non_speculative_read[OF hrt vs' hconf red' _ aok' this] wte
obtain ta'' e'' xs'' h''
where red'': "P,t ⊢ ⟨e, (shr s', xs)⟩ -ta''→ ⟨e'', (h'', xs'')⟩"
and aok'': "red_mthr.mthr.if.actions_ok s' t ta''"
and i'': "i < length ⦃ta''⦄⇘o⇙"
and eq'': "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta'⦄⇘o⇙"
and len'': "length ⦃ta''⦄⇘o⇙ ≤ max J_non_speculative_read_bound (length ⦃ta'⦄⇘o⇙)" by blast

let ?x' = "(Running, e'', xs'')"
let ?ta' = "convert_TA_initial (convert_obs_initial ta'')"
from red'' have "red_mthr.init_fin P t (x, shr s') ?ta' (?x', h'')"
unfolding x by -(rule red_mthr.init_fin.NormalAction, simp)
moreover from aok'' have "red_mthr.mthr.if.actions_ok s' t ?ta'" by simp
moreover from i'' have "i < length ⦃?ta'⦄⇘o⇙" by simp
moreover from eq'' have "take i ⦃?ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙" unfolding ta by(simp add: take_map)
moreover from len'' have "length ⦃?ta'⦄⇘o⇙ ≤ max J_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
unfolding ta by simp
ultimately
show "∃ta' x'' m''. red_mthr.init_fin P t (x, shr s') ta' (x'', m'') ∧
red_mthr.mthr.if.actions_ok s' t ta' ∧
i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
length ⦃ta'⦄⇘o⇙ ≤ max J_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
by blast
qed

lemma J_cut_and_update:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "red_mthr.if.cut_and_update (init_fin_lift_state status (J_start_state P C M vs))
(mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs)))"
proof -
from wf_start obtain Ts T pns body D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M: Ts→T = ⌊(pns, body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases auto

spurious_wakeups
final_expr "mred P" "λt x h. ∃ET. sconf_type_ok ET t x h" P

let ?start_vs = "w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))"
let ?wt_ok = "init_fin_lift_inv sconf_type_ok"
let ?ET_start = "J_sconf_type_ET_start P C M"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
let ?start_state = "init_fin_lift_state status (J_start_state P C M vs)"

from wf sees have "wf_mdecl wf_J_mdecl P D (M, Ts, T, ⌊(pns, body)⌋)" by(rule sees_wf_mdecl)
then obtain T' where len1: "length pns = length Ts" and wt: "P,[this↦Class D,pns [↦] Ts] ⊢ body :: T'"
from conf have len2: "length vs = length Ts" by(rule list_all2_lengthD)

note wf_prog_wf_syscls[OF wf] non_speculative_read[OF wf hrt wf_start ka]
moreover
from wf wf_start have ts_ok_start: "ts_ok (init_fin_lift (λt x h. ∃ET. sconf_type_ok ET t x h)) (thr ?start_state) (shr ?start_state)"
unfolding ts_ok_init_fin_lift_init_fin_lift_state shr_start_state by(rule J_start_state_sconf_type_ok)
moreover
have ka: "J_known_addrs start_tid ((λ(pns, body) vs. (blocks (this # pns) (Class (fst (method P C M)) # fst (snd (method P C M))) (Null # vs) body, Map.empty)) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using sees ka len1 len2 WT_ka[OF wt]
qed

lemma J_drf:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "drf (J_ℰ P C M vs status) P"
proof -
from wf_start obtain Ts T pns body D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M: Ts→T = ⌊(pns, body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases auto

from J_cut_and_update[OF assms] wf_prog_wf_syscls[OF wf] J_start_state_sconf_type_ok[OF wf wf_start] show ?thesis
from wf sees have "wf_mdecl wf_J_mdecl P D (M, Ts, T, ⌊(pns, body)⌋)" by(rule sees_wf_mdecl)
then obtain T' where len1: "length pns = length Ts" and wt: "P,[this↦Class D,pns [↦] Ts] ⊢ body :: T'"
from conf have len2: "length vs = length Ts" by(rule list_all2_lengthD)
show "J_known_addrs start_tid ((λ(pns, body) vs. (blocks (this # pns) (Class (fst (method P C M)) # fst (snd (method P C M))) (Null # vs) body, Map.empty)) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using sees ka len1 len2 WT_ka[OF wt]
qed
qed

lemma J_sc_legal:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "sc_legal (J_ℰ P C M vs status) P"
proof -
from wf_start obtain Ts T pns body D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M: Ts→T = ⌊(pns, body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases auto
spurious_wakeups
final_expr "mred P" "λt x h. ∃ET. sconf_type_ok ET t x h" P

let ?start_vs = "w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))"
let ?wt_ok = "init_fin_lift_inv sconf_type_ok"
let ?ET_start = "J_sconf_type_ET_start P C M"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
let ?start_state = "init_fin_lift_state status (J_start_state P C M vs)"

from wf sees have "wf_mdecl wf_J_mdecl P D (M, Ts, T, ⌊(pns, body)⌋)" by(rule sees_wf_mdecl)
then obtain T' where len1: "length pns = length Ts" and wt: "P,[this↦Class D,pns [↦] Ts] ⊢ body :: T'"
from conf have len2: "length vs = length Ts" by(rule list_all2_lengthD)

note wf_prog_wf_syscls[OF wf] non_speculative_read[OF wf hrt wf_start ka]
moreover
from wf wf_start have ts_ok_start: "ts_ok (init_fin_lift (λt x h. ∃ET. sconf_type_ok ET t x h)) (thr ?start_state) (shr ?start_state)"
unfolding ts_ok_init_fin_lift_init_fin_lift_state shr_start_state by(rule J_start_state_sconf_type_ok)
moreover have ka_allocated: "J_known_addrs start_tid ((λ(pns, body) vs. (blocks (this # pns) (Class (fst (method P C M)) # fst (snd (method P C M))) (Null # vs) body, Map.empty)) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using sees ka len1 len2 WT_ka[OF wt]
ultimately have "red_mthr.if.hb_completion ?start_state (lift_start_obs start_tid start_heap_obs)"

thus ?thesis using wf_prog_wf_syscls[OF wf] J_start_state_sconf_type_ok[OF wf wf_start]
by(rule sc_legal)(rule ka_allocated)
qed

lemma J_jmm_consistent:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "jmm_consistent (J_ℰ P C M vs status) P"
(is "jmm_consistent ?ℰ P")
proof -
interpret drf "?ℰ" P using assms by(rule J_drf)
interpret sc_legal "?ℰ" P using assms by(rule J_sc_legal)
show ?thesis by unfold_locales
qed

lemma J_ex_sc_exec:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "∃E ws. E ∈ J_ℰ P C M vs status ∧ P ⊢ (E, ws) √ ∧ sequentially_consistent P (E, ws)"
(is "∃E ws. _ ∈ ?ℰ ∧ _")
proof -
interpret jmm: executions_sc_hb ?ℰ P using assms by -(rule executions_sc)

let ?start_state = "init_fin_lift_state status (J_start_state P C M vs)"
let ?start_mrw = "mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs))"

from red_mthr.if.sequential_completion_Runs[OF red_mthr.if.cut_and_update_imp_sc_completion[OF J_cut_and_update[OF assms]] ta_seq_consist_convert_RA]
obtain ttas where Red: "red_mthr.mthr.if.mthr.Runs P ?start_state ttas"
and sc: "ta_seq_consist P ?start_mrw (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) ttas))" by blast
let ?E = "lappend (llist_of (lift_start_obs start_tid start_heap_obs)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
from Red have "?E ∈ ?ℰ" by(blast intro: red_mthr.mthr.if.ℰ.intros)
moreover from Red have tsa: "thread_start_actions_ok ?E"
from sc have "ta_seq_consist P Map.empty (lmap snd ?E)"
unfolding lmap_lappend_distrib lmap_lconcat llist.map_comp split_def o_def lmap_llist_of map_map snd_conv
from ta_seq_consist_imp_sequentially_consistent[OF tsa jmm.ℰ_new_actions_for_fun[OF ‹?E ∈ ?ℰ›] this]
obtain ws where "sequentially_consistent P (?E, ws)" "P ⊢ (?E, ws) √" by iprover
ultimately show ?thesis by blast
qed

theorem J_consistent:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "∃E ws. legal_execution P (J_ℰ P C M vs status) (E, ws)"
proof -
let ?ℰ = "J_ℰ P C M vs status"
interpret sc_legal "?ℰ" P using assms by(rule J_sc_legal)
from J_ex_sc_exec[OF assms]
obtain E ws where "E ∈ ?ℰ" "P ⊢ (E, ws) √" "sequentially_consistent P (E, ws)" by blast
hence "legal_execution P ?ℰ (E, ws)" by(rule SC_is_legal)
thus ?thesis by blast
qed

end

end
```