Theory JMM_Heap

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

section ‹Locales for heap operations with set of allocated addresses›

theory JMM_Heap 
imports
  "../Common/WellForm"
  SC_Completion
  HB_Completion
begin

definition w_addrs :: "('addr × addr_loc ⇒ 'addr val set) ⇒ 'addr set"
where "w_addrs vs = {a. ∃adal. Addr a ∈ vs adal}"

lemma w_addrs_empty [simp]: "w_addrs (λ_. {}) = {}"
by(simp add: w_addrs_def)

locale allocated_heap_base = heap_base +
  constrains 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 :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  fixes allocated :: "'heap ⇒ 'addr set"

locale allocated_heap = 
  allocated_heap_base +
  heap +
  constrains 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 :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and allocated :: "'heap ⇒ 'addr set"
  and P :: "'m prog"

  assumes allocated_empty: "allocated empty_heap = {}"
  and allocate_allocatedD:
  "(h', a) ∈ allocate h hT ⟹ allocated h' = insert a (allocated h) ∧ a ∉ allocated h"
  and heap_write_allocated_same:
  "heap_write h a al v h' ⟹ allocated h' = allocated h"
begin

lemma allocate_allocated_mono: "(h', a) ∈ allocate h C ⟹ allocated h ⊆ allocated h'"
by(simp_all add: allocate_allocatedD)

lemma
  shows start_addrs_allocated: "allocated start_heap = set start_addrs"
  and distinct_start_addrs': "distinct start_addrs"
proof -
  { fix h ads b and xs :: "cname list"
    let "?start_addrs h ads b xs" = "fst (snd (foldl create_initial_object (h, ads, b) xs))"
    let "?start_heap h ads b xs" = "fst (foldl create_initial_object (h, ads, b) xs)"
    assume "allocated h = set ads"
    hence "allocated (?start_heap h ads b xs) = set (?start_addrs h ads b xs) ∧
           (distinct ads ⟶ distinct (?start_addrs h ads b xs))"
      (is "?concl xs h ads b")
    proof(induct xs arbitrary: h ads b)
      case Nil thus ?case by auto
    next
      case (Cons x xs)
      note ads = ‹allocated h = set ads›
      show ?case
      proof(cases "b ∧ allocate h (Class_type x) ≠ {}")
        case False thus ?thesis using ads
          by(simp add: create_initial_object_simps zip_append1)
      next
        case [simp]: True
        then obtain h' a' 
          where h'a': "(SOME ha. ha ∈ allocate h (Class_type x)) = (h', a')"
          and new_obj: "(h', a') ∈ allocate h (Class_type x)"
          by(cases "(SOME ha. ha ∈ allocate h (Class_type x))")(auto simp del: True dest: allocate_Eps)

        from new_obj have "allocated h' = insert a' (allocated h)" "a' ∉ allocated h"
          by(auto dest: allocate_allocatedD)
        with ads have "allocated h' = set (ads @ [a'])" by auto
        hence "?concl xs h' (ads @ [a']) True" by(rule Cons)
        moreover have "a' ∉ set ads" using ‹a' ∉ allocated h› ads by blast
        ultimately show ?thesis by(simp add: create_initial_object_simps new_obj h'a')
      qed
    qed }
  from this[of empty_heap "[]" True initialization_list]
  show "allocated start_heap = set start_addrs"
    and distinct_start_addrs: "distinct start_addrs"
    unfolding start_heap_def start_addrs_def start_heap_data_def
    by(auto simp add: allocated_empty)
qed

lemma w_addrs_start_heap_obs: "w_addrs (w_values P vs (map NormalAction start_heap_obs)) ⊆ w_addrs vs"
proof -
  { fix xs
    let ?NewObj = "λa C. NewHeapElem a (Class_type C) :: ('addr, 'thread_id) obs_event"
    let "?start_heap_obs xs" = "map (λ(C, a). ?NewObj a C) xs"
    have "w_addrs (w_values P vs (map NormalAction (?start_heap_obs xs))) ⊆ w_addrs vs"
      (is "?concl xs")
    proof(induct xs arbitrary: vs)
      case Nil thus ?case by simp
    next
      case (Cons x xs)
      have "w_addrs (w_values P vs (map NormalAction (map (λ(C, a). ?NewObj a C) (x # xs))))
        = w_addrs (w_values P (w_value P vs (NormalAction (?NewObj (snd x) (fst x)))) (map NormalAction (map (λ(C, a). ?NewObj a C) xs)))"
        by(simp add: split_beta)
      also have "… ⊆ w_addrs (w_value P vs (NormalAction (?NewObj (snd x) (fst x))))" by(rule Cons)
      also have "… ⊆ w_addrs vs"
        by(auto simp add: w_addrs_def default_val_not_Addr Addr_not_default_val)
      finally show ?case .
    qed }
  thus ?thesis by(simp add: start_heap_obs_def)
qed

end

context heap_base begin

lemma addr_loc_default_conf:
  "P ⊢ class_type_of CTn has F:T (fm) in C 
  ⟹ P,h ⊢ addr_loc_default P CTn (CField C F) :≤ T"
apply(cases CTn)
 apply simp
apply(frule has_field_decl_above)
apply simp
done

definition vs_conf :: "'m prog ⇒ 'heap ⇒ ('addr × addr_loc ⇒ 'addr val set) ⇒ bool"
where "vs_conf P h vs ⟷ (∀ad al v. v ∈ vs (ad, al) ⟶ (∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T))"

lemma vs_confI:
  "(⋀ad al v. v ∈ vs (ad, al) ⟹ ∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T) ⟹ vs_conf P h vs"
unfolding vs_conf_def by blast

lemma vs_confD:
  "⟦ vs_conf P h vs; v ∈ vs (ad, al) ⟧ ⟹ ∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T"
unfolding vs_conf_def by blast

lemma vs_conf_insert_iff:
  "vs_conf P h (vs((ad, al) := insert v (vs (ad, al)))) 
  ⟷ vs_conf P h vs ∧ (∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T)"
by(auto 4 3 elim: vs_confD intro: vs_confI split: if_split_asm)

end

context heap begin

lemma vs_conf_hext: "⟦ vs_conf P h vs; h ⊴ h' ⟧ ⟹ vs_conf P h' vs"
by(blast intro!: vs_confI intro: conf_hext addr_loc_type_hext_mono dest: vs_confD)

lemma vs_conf_allocate:
  "⟦ vs_conf P h vs; (h', a) ∈ allocate h hT; is_htype P hT ⟧ 
  ⟹ vs_conf P h' (w_value P vs (NormalAction (NewHeapElem a hT)))"
apply(drule vs_conf_hext)
 apply(erule hext_allocate)
apply(auto intro!: vs_confI simp add: addr_locs_def split: if_split_asm htype.split_asm)
apply(auto 3 3 intro: addr_loc_type.intros defval_conf dest: allocate_SomeD elim: has_field_is_class vs_confD)
apply(rule exI conjI addr_loc_type.intros|drule allocate_SomeD|erule has_field_is_class|simp)+
done

end

text ‹
  ‹heap_read_typeable› must not be defined in @{term heap_conf_base} (where it should be) because
  this would lead to duplicate definitions of ‹heap_read_typeable› in contexts where @{term heap_conf_base} 
  is imported twice with different parameters, e.g., @{term P} and @{term "J2JVM P"} in @{term "J_JVM_heap_conf_read"}.
›

context heap_base begin

definition heap_read_typeable :: "('heap ⇒ bool) ⇒ 'm prog ⇒ bool"
where "heap_read_typeable hconf P ⟷ (∀h ad al v T. hconf h ⟶ P,h ⊢ ad@al : T ⟶ P,h ⊢ v :≤ T ⟶ heap_read h ad al v)"

lemma heap_read_typeableI:
  "(⋀h ad al v T. ⟦ P,h ⊢ ad@al : T; P,h ⊢ v :≤ T; hconf h ⟧ ⟹ heap_read h ad al v) ⟹ heap_read_typeable hconf P"
unfolding heap_read_typeable_def by blast

lemma heap_read_typeableD:
  "⟦ heap_read_typeable hconf P; P,h ⊢ ad@al : T; P,h ⊢ v :≤ T; hconf h ⟧ ⟹ heap_read h ad al v"
unfolding heap_read_typeable_def by blast

end

context heap_base begin

definition heap_read_typed :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
where "heap_read_typed P h ad al v ⟷ heap_read h ad al v ∧ (∀T. P,h ⊢ ad@al : T ⟶ P,h ⊢ v :≤ T)"

lemma heap_read_typedI:
  "⟦ heap_read h ad al v; ⋀T. P,h ⊢ ad@al : T ⟹ P,h ⊢ v :≤ T ⟧ ⟹ heap_read_typed P h ad al v"
unfolding heap_read_typed_def by blast

lemma heap_read_typed_into_heap_read:
  "heap_read_typed P h ad al v ⟹ heap_read h ad al v"
unfolding heap_read_typed_def by blast

lemma heap_read_typed_typed:
  "⟦ heap_read_typed P h ad al v; P,h ⊢ ad@al : T ⟧ ⟹ P,h ⊢ v :≤ T"
unfolding heap_read_typed_def by blast

end

context heap_conf begin

lemma heap_conf_read_heap_read_typed:
  "heap_conf_read addr2thread_id thread_id2addr empty_heap allocate typeof_addr (heap_read_typed P) heap_write hconf P"
proof
  fix h a al v T
  assume "heap_read_typed P h a al v" "P,h ⊢ a@al : T" 
  thus "P,h ⊢ v :≤ T" by(rule heap_read_typed_typed)
qed

end

context heap begin

lemma start_addrs_dom_w_values:
  assumes wf: "wf_syscls P"
  and a: "a ∈ set start_addrs"
  and adal: "P,start_heap ⊢ a@al : T"
  shows "w_values P (λ_. {}) (map NormalAction start_heap_obs) (a, al) ≠ {}"
proof -
  from a obtain CTn where CTn: "NewHeapElem a CTn ∈ set start_heap_obs"
    unfolding in_set_start_addrs_conv_NewHeapElem ..
  then obtain obs obs' where obs: "start_heap_obs = obs @ NewHeapElem a CTn # obs'" by(auto dest: split_list)
  have "w_value P (w_values P (λ_. {}) (map NormalAction obs)) (NormalAction (NewHeapElem a CTn)) (a, al) ≠ {}"
  proof(cases CTn)
    case [simp]: (Class_type C)
    with wf CTn have "typeof_addr start_heap a = ⌊Class_type C⌋"
      by(auto intro: NewHeapElem_start_heap_obsD)
    with adal show ?thesis by cases auto
  next
    case [simp]: (Array_type T n)
    with wf CTn have "typeof_addr start_heap a = ⌊Array_type T n⌋"
      by(auto dest: NewHeapElem_start_heap_obsD)
    with adal show ?thesis by cases(auto dest: has_field_decl_above)
  qed
  moreover have "w_value P (w_values P (λ_. {}) (map NormalAction obs)) (NormalAction (NewHeapElem a CTn :: ('addr, 'thread_id) obs_event))
    (a, al) ⊆ w_values P (λ_. {}) (map NormalAction start_heap_obs) (a, al)"
    by(simp add: obs del: w_value.simps)(rule w_values_mono)
  ultimately show ?thesis by blast
qed

end

end