Theory JMM_J_Typesafe

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

section ‹JMM type safety for source code›

theory JMM_J_Typesafe imports
  JMM_Typesafe2
  DRF_J
begin

locale J_allocated_heap_conf' = 
  h: J_heap_conf 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write hconf
    P
  +
  h: J_allocated_heap 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write
    allocated
    P
  +
  heap''
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    P
  for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and hconf :: "'heap ⇒ bool"
  and allocated :: "'heap ⇒ 'addr set"
  and P :: "'addr J_prog"

sublocale J_allocated_heap_conf' < h: J_allocated_heap_conf
  addr2thread_id thread_id2addr
  spurious_wakeups
  empty_heap allocate "λ_. typeof_addr" heap_read heap_write hconf allocated
  P
by(unfold_locales)

context J_allocated_heap_conf' begin

lemma red_New_type_match:
  "⟦ h.red' P t e s ta e' s'; NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙; typeof_addr ad ≠ None ⟧
  ⟹ typeof_addr ad = ⌊CTn⌋" 
  and reds_New_type_match:
  "⟦ h.reds' P t es s ta es' s'; NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙; typeof_addr ad ≠ None ⟧
  ⟹ typeof_addr ad = ⌊CTn⌋"
by(induct rule: h.red_reds.inducts)(auto dest: allocate_typeof_addr_SomeD red_external_New_type_match)

lemma mred_known_addrs_typing':
  assumes wf: "wf_J_prog P"
  and ok: "h.start_heap_ok"
  shows "known_addrs_typing' addr2thread_id thread_id2addr empty_heap allocate typeof_addr heap_write allocated h.J_known_addrs final_expr (h.mred P) (λt x h. ∃ET. h.sconf_type_ok ET t x h) P"
proof -
  interpret known_addrs_typing
    addr2thread_id thread_id2addr 
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write
    allocated h.J_known_addrs
    final_expr "h.mred P" "λt x h. ∃ET. h.sconf_type_ok ET t x h"
    P
    using assms by(rule h.mred_known_addrs_typing)

  show ?thesis by unfold_locales(auto dest: red_New_type_match)
qed

lemma J_legal_read_value_typeable:
  assumes wf: "wf_J_prog P"
  and wf_start: "h.wf_start_state P C M vs"
  and legal: "weakly_legal_execution P (h.J_ℰ P C M vs status) (E, ws)"
  and a: "enat a < llength E"
  and read: "action_obs E a = NormalAction (ReadMem ad al v)"
  shows "∃T. P ⊢ ad@al : T ∧ P ⊢ v :≤ T"
proof -
  note wf
  moreover from wf_start have "h.start_heap_ok" by cases
  moreover from wf wf_start
  have "ts_ok (λt x h. ∃ET. h.sconf_type_ok ET t x h) (thr (h.J_start_state P C M vs)) h.start_heap"
    by(rule h.J_start_state_sconf_type_ok)
  moreover from wf have "wf_syscls P" by(rule wf_prog_wf_syscls)
  ultimately show ?thesis using legal a read
    by(rule known_addrs_typing'.weakly_legal_read_value_typeable[OF mred_known_addrs_typing'])
qed

end

subsection ‹Specific part for JMM implementation 2›

abbreviation jmm_J_ℰ
  :: "addr J_prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ status ⇒ (addr × (addr, addr) obs_event action) llist set"
where 
  "jmm_J_ℰ P ≡ 
  J_heap_base.J_ℰ addr2thread_id thread_id2addr jmm_spurious_wakeups jmm_empty jmm_allocate (jmm_typeof_addr P) jmm_heap_read jmm_heap_write P"

abbreviation jmm'_J_ℰ
  :: "addr J_prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ status ⇒ (addr × (addr, addr) obs_event action) llist set"
where 
  "jmm'_J_ℰ P ≡ 
  J_heap_base.J_ℰ addr2thread_id thread_id2addr jmm_spurious_wakeups jmm_empty jmm_allocate (jmm_typeof_addr P) (jmm_heap_read_typed P) jmm_heap_write P"


lemma jmm_J_heap_conf:
  "J_heap_conf addr2thread_id thread_id2addr jmm_empty jmm_allocate (jmm_typeof_addr P) jmm_heap_write jmm_hconf P"
by(unfold_locales)

lemma jmm_J_allocated_heap_conf: "J_allocated_heap_conf addr2thread_id thread_id2addr jmm_empty jmm_allocate (jmm_typeof_addr P) jmm_heap_write jmm_hconf jmm_allocated P"
by(unfold_locales)


lemma jmm_J_allocated_heap_conf':
  "J_allocated_heap_conf' addr2thread_id thread_id2addr jmm_empty jmm_allocate (jmm_typeof_addr' P) jmm_heap_write jmm_hconf jmm_allocated P"
apply(rule J_allocated_heap_conf'.intro)
apply(unfold jmm_typeof_addr'_conv_jmm_typeof_addr)
apply(unfold_locales)
done


lemma red_heap_read_typedD:
  "J_heap_base.red' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) (heap_base.heap_read_typed (λ_ :: 'heap. typeof_addr) heap_read P) heap_write P t e s ta e' s' ⟷
   J_heap_base.red' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) heap_read heap_write P t e s ta e' s' ∧
  (∀ad al v T. ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟶ heap_base'.addr_loc_type TYPE('heap) typeof_addr P ad al T ⟶ heap_base'.conf TYPE('heap) typeof_addr P v T)"
  (is "?lhs1 ⟷ ?rhs1a ∧ ?rhs1b")
  and reds_heap_read_typedD:
  "J_heap_base.reds' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) (heap_base.heap_read_typed (λ_ :: 'heap. typeof_addr) heap_read P) heap_write P t es s ta es' s' ⟷
   J_heap_base.reds' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) heap_read heap_write P t es s ta es' s' ∧
  (∀ad al v T. ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟶ heap_base'.addr_loc_type TYPE('heap) typeof_addr P ad al T ⟶ heap_base'.conf TYPE('heap) typeof_addr P v T)"
  (is "?lhs2 ⟷ ?rhs2a ∧ ?rhs2b")
proof -
  have "(?lhs1 ⟶ ?rhs1a ∧ ?rhs1b) ∧ (?lhs2 ⟶ ?rhs2a ∧ ?rhs2b)"
    apply(induct rule: J_heap_base.red_reds.induct)
    prefer 50 (* RedCallExternal *)
    apply(subst (asm) red_external_heap_read_typed)
    apply(fastforce intro!: J_heap_base.red_reds.RedCallExternal simp add: convert_extTA_def)

    prefer 49 (* RedCall *)
    apply(fastforce dest: J_heap_base.red_reds.RedCall)

    apply(auto intro: J_heap_base.red_reds.intros dest: heap_base.heap_read_typed_into_heap_read heap_base.heap_read_typed_typed dest: heap_base'.addr_loc_type_conv_addr_loc_type[THEN fun_cong, THEN fun_cong, THEN fun_cong, THEN iffD2] heap_base'.conf_conv_conf[THEN fun_cong, THEN fun_cong, THEN iffD1])
    done
  moreover have "(?rhs1a ⟶ ?rhs1b ⟶ ?lhs1) ∧ (?rhs2a ⟶ ?rhs2b ⟶ ?lhs2)"
    apply(induct rule: J_heap_base.red_reds.induct)
    prefer 50 (* RedCallExternal *)
    apply simp
    apply(intro strip)
    apply(erule (1) J_heap_base.red_reds.RedCallExternal)
    apply(subst red_external_heap_read_typed, erule conjI)
    apply(blast+)[4]

    prefer 49 (* RedCall *)
    apply(fastforce dest: J_heap_base.red_reds.RedCall)

    apply(auto intro: J_heap_base.red_reds.intros intro!: heap_base.heap_read_typedI dest: heap_base'.addr_loc_type_conv_addr_loc_type[THEN fun_cong, THEN fun_cong, THEN fun_cong, THEN iffD1] intro: heap_base'.conf_conv_conf[THEN fun_cong, THEN fun_cong, THEN iffD2])
    done
  ultimately show "?lhs1 ⟷ ?rhs1a ∧ ?rhs1b" "?lhs2 ⟷ ?rhs2a ∧ ?rhs2b" by blast+
qed

lemma if_mred_heap_read_typedD:
  "multithreaded_base.init_fin final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) (heap_base.heap_read_typed (λ_ :: 'heap. typeof_addr) heap_read P) heap_write P) t xh ta x'h' ⟷
   if_heap_read_typed final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) heap_read heap_write P) typeof_addr P t xh ta x'h'"
unfolding multithreaded_base.init_fin.simps
by(subst red_heap_read_typedD) fastforce

lemma J_ℰ_heap_read_typedI:
  "⟦ E ∈ J_heap_base.J_ℰ addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) heap_read heap_write P C M vs status;
     ⋀ad al v T. ⟦ NormalAction (ReadMem ad al v) ∈ snd ` lset E; heap_base'.addr_loc_type TYPE('heap) typeof_addr P ad al T ⟧ ⟹ heap_base'.conf TYPE('heap) typeof_addr P v T ⟧
  ⟹ E ∈ J_heap_base.J_ℰ addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_ :: 'heap. typeof_addr) (heap_base.heap_read_typed (λ_ :: 'heap. typeof_addr) heap_read P) heap_write P C M vs status"
apply(erule imageE, hypsubst)
apply(rule imageI)
apply(erule multithreaded_base.ℰ.cases, hypsubst)
apply(rule multithreaded_base.ℰ.intros)
apply(subst if_mred_heap_read_typedD[abs_def])
apply(erule if_mthr_Runs_heap_read_typedI)
apply(auto simp add: image_Un lset_lmap[symmetric] lmap_lconcat llist.map_comp o_def split_def simp del: lset_lmap)
done

lemma jmm'_redI:
  "⟦ J_heap_base.red' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr jmm_heap_read jmm_heap_write P t e s ta e' s'; 
     final_thread.actions_ok (final_thread.init_fin_final final_expr) S t ta ⟧
  ⟹ ∃ta e' s'. J_heap_base.red' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_base.heap_read_typed typeof_addr jmm_heap_read P) jmm_heap_write P t e s ta e' s' ∧ final_thread.actions_ok (final_thread.init_fin_final final_expr) S t ta"
  (is "⟦ ?red'; ?aok ⟧ ⟹ ?concl")
  and jmm'_redsI:
  "⟦ J_heap_base.reds' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr jmm_heap_read jmm_heap_write P t es s ta es' s';
     final_thread.actions_ok (final_thread.init_fin_final final_expr) S t ta ⟧
  ⟹ ∃ta es' s'. J_heap_base.reds' addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_base.heap_read_typed typeof_addr jmm_heap_read P) jmm_heap_write P t es s ta es' s' ∧ 
     final_thread.actions_ok (final_thread.init_fin_final final_expr) S t ta"
  (is "⟦ ?reds'; ?aoks ⟧ ⟹ ?concls")
proof -
  note [simp del] = split_paired_Ex
    and [simp add] = final_thread.actions_ok_iff heap_base.THE_addr_loc_type heap_base.defval_conf
    and [intro] = jmm_heap_read_typed_default_val

  let ?v = "λh a al. default_val (THE T. heap_base.addr_loc_type typeof_addr P h a al T)"

  have "(?red' ⟶ ?aok ⟶ ?concl) ∧ (?reds' ⟶ ?aoks ⟶ ?concls)"
  proof(induct rule: J_heap_base.red_reds.induct)
    case (23 h a T n i v l) (* RedAAcc *)
    thus ?case by(auto 4 6 intro: J_heap_base.red_reds.RedAAcc[where v="?v h a (ACell (nat (sint i)))"])
  next
    case (35 h a D F v l) (* RedFAcc *)
    thus ?case by(auto 4 5 intro: J_heap_base.red_reds.RedFAcc[where v="?v h a (CField D F)"])
  next
    case RedCASSucceed: (45 h a D F v v' h') (* RedCASSucceed *)
    thus ?case
    proof(cases "v = ?v h a (CField D F)")
      case True
      with RedCASSucceed show ?thesis
        by(fastforce intro: J_heap_base.red_reds.RedCASSucceed[where v="?v h a (CField D F)"])
    next
      case False
      with RedCASSucceed show ?thesis
        by(fastforce intro: J_heap_base.red_reds.RedCASFail[where v''="?v h a (CField D F)"])
    qed
  next
    case RedCASFail: (46 h a D F v'' v v' l)
    thus ?case
    proof(cases "v = ?v h a (CField D F)")
      case True
      with RedCASFail show ?thesis
        by(fastforce intro: J_heap_base.red_reds.RedCASSucceed[where v="?v h a (CField D F)"] jmm_heap_write.intros)
    next
      case False
      with RedCASFail show ?thesis
        by(fastforce intro: J_heap_base.red_reds.RedCASFail[where v''="?v h a (CField D F)"])
    qed
  next
    case (50 s a hU M Ts T D vs ta va h' ta' e' s') (* RedCallExternal *)
    thus ?case
      apply clarify
      apply(drule jmm'_red_externalI, simp)
      apply(auto 4 4 intro: J_heap_base.red_reds.RedCallExternal)
      done
  next
    case (52 e h l V vo ta e' h' l' T) (* BlockRed *)
    thus ?case
      by(clarify)(iprover intro: J_heap_base.red_reds.BlockRed)
  qed(blast intro: J_heap_base.red_reds.intros)+
  thus "⟦ ?red'; ?aok ⟧ ⟹ ?concl" and "⟦ ?reds'; ?aoks ⟧ ⟹ ?concls" by blast+
qed

lemma if_mred_heap_read_not_stuck:
  "⟦ multithreaded_base.init_fin final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr jmm_heap_read jmm_heap_write P) t xh ta x'h';
    final_thread.actions_ok (final_thread.init_fin_final final_expr) s t ta ⟧
  ⟹
  ∃ta x'h'. multithreaded_base.init_fin final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_base.heap_read_typed typeof_addr jmm_heap_read P) jmm_heap_write P) t xh ta x'h' ∧ final_thread.actions_ok (final_thread.init_fin_final final_expr) s t ta"
apply(erule multithreaded_base.init_fin.cases)
  apply hypsubst
  apply clarify
  apply(drule jmm'_redI)
   apply(simp add: final_thread.actions_ok_iff)
  apply clarify
  apply(subst (2) split_paired_Ex)
  apply(subst (2) split_paired_Ex)
  apply(subst (2) split_paired_Ex)
  apply(rule exI conjI)+
   apply(rule multithreaded_base.init_fin.intros)
   apply(simp)
  apply(simp add: final_thread.actions_ok_iff)
 apply(blast intro: multithreaded_base.init_fin.intros)
apply(blast intro: multithreaded_base.init_fin.intros)
done

lemma if_mredT_heap_read_not_stuck:
  "multithreaded_base.redT (final_thread.init_fin_final final_expr) (multithreaded_base.init_fin final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr jmm_heap_read jmm_heap_write P)) convert_RA' s tta s'
  ⟹ ∃tta s'. multithreaded_base.redT (final_thread.init_fin_final final_expr) (multithreaded_base.init_fin final_expr (J_heap_base.mred addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_base.heap_read_typed typeof_addr jmm_heap_read P) jmm_heap_write P)) convert_RA' s tta s'"
apply(erule multithreaded_base.redT.cases)
 apply hypsubst
 apply(drule (1) if_mred_heap_read_not_stuck)
 apply(erule exE)+
 apply(rename_tac ta' x'h')
 apply(insert redT_updWs_total)
 apply(erule_tac x="t" in meta_allE)
 apply(erule_tac x="wset s" in meta_allE)
 apply(erule_tac x="⦃ta'⦄⇘w⇙" in meta_allE)
 apply clarsimp
 apply(rule exI)+
 apply(auto intro!: multithreaded_base.redT.intros)[1]
apply hypsubst
apply(rule exI conjI)+
apply(rule multithreaded_base.redT.redT_acquire)
apply assumption+
done

lemma J_ℰ_heap_read_typedD:
  "E ∈ J_heap_base.J_ℰ addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_. typeof_addr) (heap_base.heap_read_typed (λ_. typeof_addr) jmm_heap_read P) jmm_heap_write P C M vs status
  ⟹ E ∈ J_heap_base.J_ℰ addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate (λ_. typeof_addr) jmm_heap_read jmm_heap_write P C M vs status"
apply(erule imageE, hypsubst)
apply(rule imageI)
apply(erule multithreaded_base.ℰ.cases, hypsubst)
apply(rule multithreaded_base.ℰ.intros)
apply(subst (asm) if_mred_heap_read_typedD[abs_def])
apply(erule if_mthr_Runs_heap_read_typedD)
apply(erule if_mredT_heap_read_not_stuck[where typeof_addr="λ_. typeof_addr", unfolded if_mred_heap_read_typedD[abs_def]])
done

lemma J_ℰ_typesafe_subset: "jmm'_J_ℰ P C M vs status ⊆ jmm_J_ℰ P C M vs status"
unfolding jmm_typeof_addr_def[abs_def]
by(rule subsetI)(erule J_ℰ_heap_read_typedD)

lemma J_legal_typesafe1:
  assumes wfP: "wf_J_prog P"
  and ok: "jmm_wf_start_state P C M vs"
  and legal: "legal_execution P (jmm_J_ℰ P C M vs status) (E, ws)"
  shows "legal_execution P (jmm'_J_ℰ P C M vs status) (E, ws)"
proof -
  let ?ℰ = "jmm_J_ℰ P C M vs status"
  let ?ℰ' = "jmm'_J_ℰ P C M vs status"
  from legal obtain J 
    where justified: "P ⊢ (E, ws) justified_by J"
    and range: "range (justifying_exec ∘ J) ⊆ ?ℰ"
    and E: "E ∈ ?ℰ" and wf: "P ⊢ (E, ws) √" by(auto simp add: gen_legal_execution.simps)
  let ?J = "J(0 := ⦇committed = {}, justifying_exec = justifying_exec (J 1), justifying_ws = justifying_ws (J 1), action_translation = id⦈)"

  from wfP have wf_sys: "wf_syscls P" by(rule wf_prog_wf_syscls)

  from justified have "P ⊢ (justifying_exec (J 1), justifying_ws (J 1)) √"
    by(simp add: justification_well_formed_def)
  with justified have "P ⊢ (E, ws) justified_by ?J" by(rule drop_0th_justifying_exec)
  moreover have "range (justifying_exec ∘ ?J) ⊆ ?ℰ'"
  proof
    fix ξ
    assume "ξ ∈ range (justifying_exec ∘ ?J)"
    then obtain n where "ξ = justifying_exec (?J n)" by auto
    then obtain n where ξ: "ξ = justifying_exec (J n)" and n: "n > 0" by(auto split: if_split_asm)
    from range ξ have "ξ ∈ ?ℰ" by auto
    thus "ξ ∈ ?ℰ'" unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
    proof(rule J_ℰ_heap_read_typedI)
      fix ad al v T
      assume read: "NormalAction (ReadMem ad al v) ∈ snd ` lset ξ"
        and adal: "P ⊢jmm ad@al : T"
      from read obtain a where a: "enat a < llength ξ" "action_obs ξ a = NormalAction (ReadMem ad al v)"
        unfolding lset_conv_lnth by(auto simp add: action_obs_def)
      with J_allocated_heap_conf'.mred_known_addrs_typing'[OF jmm_J_allocated_heap_conf' wfP jmm_start_heap_ok]
        J_heap_conf.J_start_state_sconf_type_ok[OF jmm_J_heap_conf wfP ok]
        wf_sys is_justified_by_imp_is_weakly_justified_by[OF justified wf] range n
      have "∃T. P ⊢jmm ad@al : T ∧ P ⊢jmm v :≤ T"
        unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def] ξ
        by(rule known_addrs_typing'.read_value_typeable_justifying)
      thus "P ⊢jmm v :≤ T" using adal
        by(auto dest: jmm.addr_loc_type_fun[unfolded jmm_typeof_addr_conv_jmm_typeof_addr', unfolded heap_base'.addr_loc_type_conv_addr_loc_type])
    qed
  qed
  moreover from E have "E ∈ ?ℰ'"
    unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
  proof(rule J_ℰ_heap_read_typedI)
    fix ad al v T
    assume read: "NormalAction (ReadMem ad al v) ∈ snd ` lset E"
      and adal: "P ⊢jmm ad@al : T"
    from read obtain a where a: "enat a < llength E" "action_obs E a = NormalAction (ReadMem ad al v)"
      unfolding lset_conv_lnth by(auto simp add: action_obs_def)
    with jmm_J_allocated_heap_conf' wfP ok legal_imp_weakly_legal_execution[OF legal]
    have "∃T. P ⊢jmm ad@al : T ∧ P ⊢jmm v :≤ T"
      unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
      by(rule J_allocated_heap_conf'.J_legal_read_value_typeable)
    thus "P ⊢jmm v :≤ T" using adal
      by(auto dest: jmm.addr_loc_type_fun[unfolded jmm_typeof_addr_conv_jmm_typeof_addr', unfolded heap_base'.addr_loc_type_conv_addr_loc_type])
  qed
  ultimately show ?thesis using wf unfolding gen_legal_execution.simps by blast
qed

lemma J_weakly_legal_typesafe1:
  assumes wfP: "wf_J_prog P"
  and ok: "jmm_wf_start_state P C M vs"
  and legal: "weakly_legal_execution P (jmm_J_ℰ P C M vs status) (E, ws)"
  shows "weakly_legal_execution P (jmm'_J_ℰ P C M vs status) (E, ws)"
proof -
  let ?ℰ = "jmm_J_ℰ P C M vs status"
  let ?ℰ' = "jmm'_J_ℰ P C M vs status"
  from legal obtain J 
    where justified: "P ⊢ (E, ws) weakly_justified_by J"
    and range: "range (justifying_exec ∘ J) ⊆ ?ℰ"
    and E: "E ∈ ?ℰ" and wf: "P ⊢ (E, ws) √" by(auto simp add: gen_legal_execution.simps)
  let ?J = "J(0 := ⦇committed = {}, justifying_exec = justifying_exec (J 1), justifying_ws = justifying_ws (J 1), action_translation = id⦈)"

  from wfP have wf_sys: "wf_syscls P" by(rule wf_prog_wf_syscls)

  from justified have "P ⊢ (justifying_exec (J 1), justifying_ws (J 1)) √"
    by(simp add: justification_well_formed_def)
  with justified have "P ⊢ (E, ws) weakly_justified_by ?J" by(rule drop_0th_weakly_justifying_exec)
  moreover have "range (justifying_exec ∘ ?J) ⊆ ?ℰ'"
  proof
    fix ξ
    assume "ξ ∈ range (justifying_exec ∘ ?J)"
    then obtain n where "ξ = justifying_exec (?J n)" by auto
    then obtain n where ξ: "ξ = justifying_exec (J n)" and n: "n > 0" by(auto split: if_split_asm)
    from range ξ have "ξ ∈ ?ℰ" by auto
    thus "ξ ∈ ?ℰ'" unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
    proof(rule J_ℰ_heap_read_typedI)
      fix ad al v T
      assume read: "NormalAction (ReadMem ad al v) ∈ snd ` lset ξ"
        and adal: "P ⊢jmm ad@al : T"
      from read obtain a where a: "enat a < llength ξ" "action_obs ξ a = NormalAction (ReadMem ad al v)"
        unfolding lset_conv_lnth by(auto simp add: action_obs_def)
      with J_allocated_heap_conf'.mred_known_addrs_typing'[OF jmm_J_allocated_heap_conf' wfP jmm_start_heap_ok]
        J_heap_conf.J_start_state_sconf_type_ok[OF jmm_J_heap_conf wfP ok]
        wf_sys justified range n
      have "∃T. P ⊢jmm ad@al : T ∧ P ⊢jmm v :≤ T"
        unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def] ξ
        by(rule known_addrs_typing'.read_value_typeable_justifying)
      thus "P ⊢jmm v :≤ T" using adal
        by(auto dest: jmm.addr_loc_type_fun[unfolded jmm_typeof_addr_conv_jmm_typeof_addr', unfolded heap_base'.addr_loc_type_conv_addr_loc_type])
    qed
  qed
  moreover from E have "E ∈ ?ℰ'"
    unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
  proof(rule J_ℰ_heap_read_typedI)
    fix ad al v T
    assume read: "NormalAction (ReadMem ad al v) ∈ snd ` lset E"
      and adal: "P ⊢jmm ad@al : T"
    from read obtain a where a: "enat a < llength E" "action_obs E a = NormalAction (ReadMem ad al v)"
      unfolding lset_conv_lnth by(auto simp add: action_obs_def)
    with jmm_J_allocated_heap_conf' wfP ok legal
    have "∃T. P ⊢jmm ad@al : T ∧ P ⊢jmm v :≤ T"
      unfolding jmm_typeof_addr'_conv_jmm_type_addr[symmetric, abs_def]
      by(rule J_allocated_heap_conf'.J_legal_read_value_typeable)
    thus "P ⊢jmm v :≤ T" using adal
      by(auto dest: jmm.addr_loc_type_fun[unfolded jmm_typeof_addr_conv_jmm_typeof_addr', unfolded heap_base'.addr_loc_type_conv_addr_loc_type])
  qed
  ultimately show ?thesis using wf unfolding gen_legal_execution.simps by blast
qed

lemma J_legal_typesafe2:
  assumes legal: "legal_execution P (jmm'_J_ℰ P C M vs status) (E, ws)"
  shows "legal_execution P (jmm_J_ℰ P C M vs status) (E, ws)"
proof -
  let ?ℰ = "jmm_J_ℰ P C M vs status"
  let ?ℰ' = "jmm'_J_ℰ P C M vs status"
  from legal obtain J 
    where justified: "P ⊢ (E, ws) justified_by J"
    and range: "range (justifying_exec ∘ J) ⊆ ?ℰ'"
    and E: "E ∈ ?ℰ'" and wf: "P ⊢ (E, ws) √" by(auto simp add: gen_legal_execution.simps)
  from range E have "range (justifying_exec ∘ J) ⊆ ?ℰ" "E ∈ ?ℰ"
    using J_ℰ_typesafe_subset[of P status C M vs] by blast+
  with justified wf
  show ?thesis by(auto simp add: gen_legal_execution.simps)
qed

lemma J_weakly_legal_typesafe2:
  assumes legal: "weakly_legal_execution P (jmm'_J_ℰ P C M vs status) (E, ws)"
  shows "weakly_legal_execution P (jmm_J_ℰ P C M vs status) (E, ws)"
proof -
  let ?ℰ = "jmm_J_ℰ P C M vs status"
  let ?ℰ' = "jmm'_J_ℰ P C M vs status"
  from legal obtain J 
    where justified: "P ⊢ (E, ws) weakly_justified_by J"
    and range: "range (justifying_exec ∘ J) ⊆ ?ℰ'"
    and E: "E ∈ ?ℰ'" and wf: "P ⊢ (E, ws) √" by(auto simp add: gen_legal_execution.simps)
  from range E have "range (justifying_exec ∘ J) ⊆ ?ℰ" "E ∈ ?ℰ"
    using J_ℰ_typesafe_subset[of P status C M vs] by blast+
  with justified wf
  show ?thesis by(auto simp add: gen_legal_execution.simps)
qed

theorem J_weakly_legal_typesafe:
  assumes "wf_J_prog P"
  and "jmm_wf_start_state P C M vs"
  shows "weakly_legal_execution P (jmm_J_ℰ P C M vs status) = weakly_legal_execution P (jmm'_J_ℰ P C M vs status)"
apply(rule ext iffI)+
 apply(clarify, erule J_weakly_legal_typesafe1[OF assms])
apply(clarify, erule J_weakly_legal_typesafe2)
done

theorem J_legal_typesafe:
  assumes "wf_J_prog P"
  and "jmm_wf_start_state P C M vs"
  shows "legal_execution P (jmm_J_ℰ P C M vs status) = legal_execution P (jmm'_J_ℰ P C M vs status)"
apply(rule ext iffI)+
 apply(clarify, erule J_legal_typesafe1[OF assms])
apply(clarify, erule J_legal_typesafe2)
done

end