# 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
```