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⇘hv = 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⇘hv = Some Boolean) = (b. v = Bool b)"
by(cases v)(auto)

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

lemma typeof_h_eq_NT [simp]: "(typeof⇘hv = 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⇘hv = 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⇘hv = 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⇘hw = 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⇘hvs = 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