Theory Heap

(*  Title:      JinjaThreads/Common/Heap.thy
    Author:     Andreas Lochbihler

    Reminiscent of the Jinja theory Common/Objects.thy
*)

section ‹An abstract heap model›

theory Heap
imports 
  Value
begin

primrec typeof :: "'addr val ⇀ ty"
where
  "typeof  Unit    = Some Void"
| "typeof  Null    = Some NT"
| "typeof (Bool b) = Some Boolean"
| "typeof (Intg i) = Some Integer"
| "typeof (Addr a) = None"

datatype addr_loc =
    CField cname vname
  | ACell nat

lemma rec_addr_loc [simp]: "rec_addr_loc = case_addr_loc"
by(auto simp add: fun_eq_iff split: addr_loc.splits)

primrec is_volatile :: "'m prog ⇒ addr_loc ⇒ bool"
where 
  "is_volatile P (ACell n) = False"
| "is_volatile P (CField D F) = volatile (snd (snd (field P D F)))"

locale heap_base =
  addr_base addr2thread_id thread_id2addr 
  for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  +
  fixes 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"
begin

fun typeof_h :: "'heap ⇒ 'addr val ⇒ ty option"  (‹typeof⇘_⇙›)
where
  "typeof⇘h⇙ (Addr a) = map_option ty_of_htype (typeof_addr h a)"
| "typeof⇘h⇙  v = typeof v"

definition cname_of :: "'heap ⇒ 'addr ⇒ cname"
where "cname_of h a = the_Class (ty_of_htype (the (typeof_addr h a)))"

definition hext :: "'heap ⇒ 'heap ⇒ bool" (‹_ ⊴ _› [51,51] 50)
where
  "h ⊴ h' ≡ typeof_addr h ⊆⇩m typeof_addr h'"

context
  notes [[inductive_internals]]
begin

inductive addr_loc_type :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ addr_loc ⇒ ty ⇒ bool"
  (‹_,_ ⊢ _@_ : _› [50, 50, 50, 50, 50] 51)
for P :: "'m prog" and h :: 'heap and a :: 'addr
where
  addr_loc_type_field:
  "⟦ typeof_addr h a = ⌊U⌋; P ⊢ class_type_of U has F:T (fm) in D ⟧ 
  ⟹ P,h ⊢ a@CField D F : T"

| addr_loc_type_cell:
  "⟦ typeof_addr h a = ⌊Array_type T n'⌋; n < n' ⟧
  ⟹ P,h ⊢ a@ACell n : T"

end

definition typeof_addr_loc :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ addr_loc ⇒ ty"
where "typeof_addr_loc P h a al = (THE T. P,h ⊢ a@al : T)"

definition deterministic_heap_ops :: bool
where
  "deterministic_heap_ops ⟷
  (∀h ad al v v'. heap_read h ad al v ⟶ heap_read h ad al v' ⟶ v = v') ∧
  (∀h ad al v h' h''. heap_write h ad al v h' ⟶ heap_write h ad al v h'' ⟶ h' = h'') ∧
  (∀h hT h' a h'' a'. (h', a) ∈ allocate h hT ⟶ (h'', a') ∈ allocate h hT ⟶ h' = h'' ∧ a = a') ∧
  ¬ spurious_wakeups"

end

lemma typeof_lit_eq_Boolean [simp]: "(typeof v = Some Boolean) = (∃b. v = Bool b)"
by(cases v)(auto)

lemma typeof_lit_eq_Integer [simp]: "(typeof v = Some Integer) = (∃i. v = Intg i)"
by(cases v)(auto)

lemma typeof_lit_eq_NT [simp]: "(typeof v = Some NT) = (v = Null)"
by(cases v)(auto)

lemma typeof_lit_eq_Void [simp]: "typeof v = Some Void ⟷ v = Unit"
by(cases v)(auto)

lemma typeof_lit_neq_Class [simp]: "typeof v ≠ Some (Class C)"
by(cases v) auto

lemma typeof_lit_neq_Array [simp]: "typeof v ≠ Some (Array T)"
by(cases v) auto

lemma typeof_NoneD [simp,dest]:
  "typeof v = Some x ⟹ ¬ is_Addr v"
  by (cases v) auto

lemma typeof_lit_is_type:
  "typeof v = Some T ⟹ is_type P T"
by(cases v) auto

context heap_base begin

lemma typeof_h_eq_Boolean [simp]: "(typeof⇘h⇙ v = Some Boolean) = (∃b. v = Bool b)"
by(cases v)(auto)

lemma typeof_h_eq_Integer [simp]: "(typeof⇘h⇙ v = Some Integer) = (∃i. v = Intg i)"
by(cases v)(auto)

lemma typeof_h_eq_NT [simp]: "(typeof⇘h⇙ v = Some NT) = (v = Null)"
by(cases v)(auto)


lemma hextI:
  "⟦ ⋀a C. typeof_addr h a = ⌊Class_type C⌋ ⟹ typeof_addr h' a = ⌊Class_type C⌋;
     ⋀a T n. typeof_addr h a = ⌊Array_type T n⌋ ⟹ typeof_addr h' a = ⌊Array_type T n⌋ ⟧
  ⟹ h ⊴ h'"
unfolding hext_def 
by(rule map_leI)(case_tac v, simp_all)

lemma hext_objD:
  assumes "h ⊴ h'"
  and "typeof_addr h a = ⌊Class_type C⌋"
  shows "typeof_addr h' a = ⌊Class_type C⌋"
using assms unfolding hext_def by(auto dest: map_le_SomeD)

lemma hext_arrD:
  assumes "h ⊴ h'" "typeof_addr h a = ⌊Array_type T n⌋"
  shows "typeof_addr h' a = ⌊Array_type T n⌋"
using assms unfolding hext_def by(blast dest: map_le_SomeD)

lemma hext_refl [iff]: "h ⊴ h"
by (rule hextI) blast+

lemma hext_trans [trans]: "⟦ h ⊴ h'; h' ⊴ h'' ⟧ ⟹ h ⊴ h''"
unfolding hext_def by(rule map_le_trans)

lemma typeof_lit_typeof:
  "typeof v = ⌊T⌋ ⟹ typeof⇘h⇙ v = ⌊T⌋"
by(cases v)(simp_all)

lemma addr_loc_type_fun:
  "⟦ P,h ⊢ a@al : T; P,h ⊢ a@al : T' ⟧ ⟹ T = T'"
by(auto elim!: addr_loc_type.cases dest: has_field_fun)

lemma THE_addr_loc_type:
  "P,h ⊢ a@al : T ⟹ (THE T. P,h ⊢ a@al : T) = T"
by(rule the_equality)(auto dest: addr_loc_type_fun)

lemma typeof_addr_locI [simp]:
  "P,h ⊢ a@al : T ⟹ typeof_addr_loc P h a al = T"
by(auto simp add: typeof_addr_loc_def dest: addr_loc_type_fun)

lemma deterministic_heap_opsI:
  "⟦ ⋀h ad al v v'. ⟦ heap_read h ad al v; heap_read h ad al v' ⟧ ⟹ v = v';
     ⋀h ad al v h' h''. ⟦ heap_write h ad al v h'; heap_write h ad al v h'' ⟧ ⟹ h' = h'';
     ⋀h hT h' a h'' a'. ⟦ (h', a) ∈ allocate h hT; (h'', a') ∈ allocate h hT ⟧ ⟹ h' = h'' ∧ a = a';
     ¬ spurious_wakeups ⟧
  ⟹ deterministic_heap_ops"
unfolding deterministic_heap_ops_def by blast

lemma deterministic_heap_ops_readD:
  "⟦ deterministic_heap_ops; heap_read h ad al v; heap_read h ad al v' ⟧ ⟹ v = v'"
unfolding deterministic_heap_ops_def by blast

lemma deterministic_heap_ops_writeD:
  "⟦ deterministic_heap_ops; heap_write h ad al v h'; heap_write h ad al v h'' ⟧ ⟹ h' = h''"
unfolding deterministic_heap_ops_def by blast

lemma deterministic_heap_ops_allocateD:
  "⟦ deterministic_heap_ops; (h', a) ∈ allocate h hT; (h'', a') ∈ allocate h hT ⟧ ⟹ h' = h'' ∧ a = a'"
unfolding deterministic_heap_ops_def by blast

lemma deterministic_heap_ops_no_spurious_wakeups:
  "deterministic_heap_ops ⟹ ¬ spurious_wakeups"
unfolding deterministic_heap_ops_def by blast

end

locale addr_conv =
  heap_base
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
  +
  prog 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 :: "'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 P :: "'m prog"
  +
  assumes addr2thread_id_inverse: 
  "⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧ ⟹ thread_id2addr (addr2thread_id a) = a"
begin

lemma typeof_addr_thread_id2_addr_addr2thread_id [simp]:
  "⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧ ⟹ typeof_addr h (thread_id2addr (addr2thread_id a)) = ⌊Class_type C⌋"
by(simp add: addr2thread_id_inverse)

end

locale heap =
  addr_conv
    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 :: "'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 P :: "'m prog"
  +
  assumes allocate_SomeD: "⟦ (h', a) ∈ allocate h hT; is_htype P hT ⟧ ⟹ typeof_addr h' a = Some hT"

  and hext_allocate: "⋀a. (h', a) ∈ allocate h hT ⟹ h ⊴ h'"

  and hext_heap_write:
  "heap_write h a al v h' ⟹ h ⊴ h'"

begin

lemmas hext_heap_ops = hext_allocate hext_heap_write

lemma typeof_addr_hext_mono:
  "⟦ h ⊴ h'; typeof_addr h a = ⌊hT⌋ ⟧ ⟹ typeof_addr h' a = ⌊hT⌋"
unfolding hext_def by(rule map_le_SomeD)

lemma hext_typeof_mono:
  "⟦ h ⊴ h'; typeof⇘h⇙ v = Some T ⟧ ⟹ typeof⇘h'⇙ v = Some T"
by (cases v)(auto intro: typeof_addr_hext_mono)

lemma addr_loc_type_hext_mono:
  "⟦ P,h ⊢ a@al : T; h ⊴ h' ⟧ ⟹ P,h' ⊢ a@al : T"
by(force elim!: addr_loc_type.cases intro: addr_loc_type.intros elim: typeof_addr_hext_mono dest: hext_arrD)

lemma type_of_hext_type_of: ― ‹FIXME: What's this rule good for?›
  "⟦ typeof⇘h⇙ w = ⌊T⌋; hext h h' ⟧ ⟹ typeof⇘h'⇙ w = ⌊T⌋"
by(rule hext_typeof_mono)

lemma hext_None: "⟦ h ⊴ h'; typeof_addr h' a = None ⟧ ⟹ typeof_addr h a = None"
by(rule ccontr)(auto dest: typeof_addr_hext_mono)

lemma map_typeof_hext_mono:
  "⟦ map typeof⇘h⇙ vs = map Some Ts; h ⊴ h' ⟧ ⟹  map typeof⇘h'⇙ vs = map Some Ts"
apply(induct vs arbitrary: Ts)
apply(auto simp add: Cons_eq_map_conv intro: hext_typeof_mono)
done

lemma hext_typeof_addr_map_le:
  "h ⊴ h' ⟹ typeof_addr h ⊆⇩m typeof_addr h'"
by(auto simp add: map_le_def dest: typeof_addr_hext_mono)

lemma hext_dom_typeof_addr_subset:
  "h ⊴ h' ⟹ dom (typeof_addr h) ⊆ dom (typeof_addr h')"
by (metis hext_typeof_addr_map_le map_le_implies_dom_le)

end

declare heap_base.typeof_h.simps [code]
declare heap_base.cname_of_def [code]

end