(*  Title:      JinjaThreads/MM/SC.thy
    Author:     David von Oheimb, Andreas Lochbihler

    Based on the Jinja theories Common/Objects.thy and Common/Conform by David von Oheimb
*)

section ‹Sequential consistency›

theory SC
imports 
  "../Common/Conform"
  MM
begin

subsection‹Objects and Arrays›

type_synonym 
  fields = "vname × cname ⇀ addr val"       ― ‹field name, defining class, value›

type_synonym
  cells = "addr val list"

datatype heapobj
  = Obj cname fields
    ― ‹class instance with class name and fields›

  | Arr ty fields cells
    ― ‹element type, fields (from object), and list of each cell's content›

lemma rec_heapobj [simp]: "rec_heapobj = case_heapobj"
by(auto intro!: ext split: heapobj.split)

primrec obj_ty  :: "heapobj → htype"
where
  "obj_ty (Obj C f) = Class_type C"
| "obj_ty (Arr T fs cs) = Array_type T (length cs)"

fun is_Arr :: "heapobj → bool" where
  "is_Arr (Obj C fs) = False"
| "is_Arr (Arr T f el) = True"

lemma is_Arr_conv:
  "is_Arr arrobj = (∃T f el. arrobj = Arr T f el)"
by(cases arrobj, auto)

lemma is_ArrE:
  "[ is_Arr arrobj; ∧T f el. arrobj = Arr T f el ==> thesis ] ==> thesis"
  "[ ¬ is_Arr arrobj; ∧C fs. arrobj = Obj C fs ==> thesis ] ==> thesis"
by(cases arrobj, auto)+

definition init_fields :: "('field_name × (ty × fmod)) list → 'field_name ⇀ addr val"
where "init_fields ≡ map_of ∘ map (λ(FD,(T, fm)). (FD,default_val T))"

primrec
  ― ‹a new, blank object with default values in all fields:›
  blank :: "'m prog → htype → heapobj"
where
  "blank P (Class_type C) = Obj C (init_fields (fields P C))"
| "blank P (Array_type T n) = Arr T (init_fields (fields P Object)) (replicate n (default_val T))"

lemma obj_ty_blank [iff]: 
  "obj_ty (blank P hT) = hT"
by(cases hT)(simp_all)


subsection‹Heap›

type_synonym heap = "addr ⇀ heapobj"

translations
  (type) "heap" <= (type) "nat → heapobj option"

abbreviation sc_empty :: heap
where "sc_empty ≡ Map.empty"

fun the_obj :: "heapobj → cname × fields" where
  "the_obj (Obj C fs) = (C, fs)"

fun the_arr :: "heapobj → ty × fields × cells" where
  "the_arr (Arr T f el) = (T, f, el)"

abbreviation
  cname_of :: "heap → addr → cname" where
  "cname_of hp a == fst (the_obj (the (hp a)))"

definition sc_allocate :: "'m prog → heap → htype → (heap × addr) set"
where
  "sc_allocate P h hT =
   (case new_Addr h of None → {}
                   | Some a → {(h(a ↦ blank P hT), a)})"

definition sc_typeof_addr :: "heap → addr → htype option"
where "sc_typeof_addr h a = map_option obj_ty (h a)"

inductive sc_heap_read :: "heap → addr → addr_loc → addr val → bool"
for h :: heap and a :: addr
where
  Obj: "[ h a = ⌊Obj C fs⌋; fs (F, D) = ⌊v⌋ ] ==> sc_heap_read h a (CField D F) v"
| Arr: "[ h a = ⌊Arr T f el⌋; n < length el ] ==> sc_heap_read h a (ACell n) (el ! n)"
| ArrObj: "[ h a = ⌊Arr T f el⌋; f (F, Object) = ⌊v⌋ ] ==> sc_heap_read h a (CField Object F) v"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_read_cases [elim!]:
  "sc_heap_read h a (CField C F) v"
  "sc_heap_read h a (ACell n) v"

inductive sc_heap_write :: "heap → addr → addr_loc → addr val → heap → bool"
for h :: heap and a :: addr
where
  Obj: "[ h a = ⌊Obj C fs⌋; h' = h(a ↦ Obj C (fs((F, D) ↦ v))) ] ==> sc_heap_write h a (CField D F) v h'"
| Arr: "[ h a = ⌊Arr T f el⌋; h' = h(a ↦ Arr T f (el[n := v])) ] ==> sc_heap_write h a (ACell n) v h'"
| ArrObj: "[ h a = ⌊Arr T f el⌋; h' = h(a ↦ Arr T (f((F, Object) ↦ v)) el) ] ==> sc_heap_write h a (CField Object F) v h'"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_write_cases [elim!]:
  "sc_heap_write h a (CField C F) v h'"
  "sc_heap_write h a (ACell n) v h'"

consts sc_spurious_wakeups :: bool

interpretation sc: 
  heap_base
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
  for P .

text ‹Translate notation from ‹heap_base››

(* FIXME! Why does sc.preallocated need the type token?? *)
abbreviation sc_preallocated :: "'m prog → heap → bool"
where "sc_preallocated == sc.preallocated TYPE('m)"

abbreviation sc_start_tid :: "'md prog → thread_id"
where "sc_start_tid ≡ sc.start_tid TYPE('md)"

abbreviation sc_start_heap_ok :: "'m prog → bool"
where "sc_start_heap_ok ≡ sc.start_heap_ok TYPE('m)"

abbreviation sc_start_heap :: "'m prog → heap"
where "sc_start_heap ≡ sc.start_heap TYPE('m)"

abbreviation sc_start_state :: 
  "(cname → mname → ty list → ty → 'm → addr val list → 'x)
  → 'm prog → cname → mname → addr val list → (addr, thread_id, 'x, heap, addr) state"
where
  "sc_start_state f P ≡ sc.start_state TYPE('m) P f P"

abbreviation sc_wf_start_state :: "'m prog → cname → mname → addr val list → bool"
where "sc_wf_start_state P ≡ sc.wf_start_state TYPE('m) P P"

notation sc.conf (‹_,_ ⊨sc _ :≤ _›  [51,51,51,51] 50)
notation sc.confs (‹_,_ ⊨sc _ [:≤] _› [51,51,51,51] 50)
notation sc.hext (‹_ ⊴sc _› [51,51] 50)

lemma sc_start_heap_ok: "sc_start_heap_ok P"
apply(simp add: sc.start_heap_ok_def sc.start_heap_data_def initialization_list_def sc.create_initial_object_simps sc_allocate_def sys_xcpts_list_def case_option_conv_if new_Addr_SomeI del: blank.simps split del: option.split if_split)
done

lemma sc_wf_start_state_iff:
  "sc_wf_start_state P C M vs ⟷ (∃Ts T meth D. P ⊨ C sees M:Ts→T = ⌊meth⌋ in D ∧ P,sc_start_heap P ⊨sc vs [:≤] Ts)"
by(simp add: sc.wf_start_state.simps sc_start_heap_ok)

lemma sc_heap:
  "heap addr2thread_id thread_id2addr (sc_allocate P) sc_typeof_addr sc_heap_write P"
proof
  fix h' a h hT
  assume "(h', a) ∈ sc_allocate P h hT"
  thus "sc_typeof_addr h' a = ⌊hT⌋"
    by(auto simp add: sc_allocate_def sc_typeof_addr_def dest: new_Addr_SomeD split: if_split_asm)
next
  fix h' h hT a
  assume "(h', a) ∈ sc_allocate P h hT"
  from this[symmetric] show "h ⊴sc h'"
    by(fastforce simp add: sc_allocate_def sc_typeof_addr_def sc.hext_def dest: new_Addr_SomeD intro!: map_leI)
next
  fix h a al v h'
  assume "sc_heap_write h a al v h'"
  thus "h ⊴sc h'"
    by(cases al)(auto intro!: sc.hextI simp add: sc_typeof_addr_def)
qed simp

interpretation sc: 
  heap 
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
  for P by(rule sc_heap)

lemma sc_hext_new:
  "h a = None ==> h ⊴sc h(a ↦ arrobj)"
by(rule sc.hextI)(auto simp add: sc_typeof_addr_def dest!: new_Addr_SomeD)

lemma sc_hext_upd_obj: "h a = Some (Obj C fs) ==> h ⊴sc h(a↦(Obj C fs'))"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def)

lemma sc_hext_upd_arr: "[ h a = Some (Arr T f e); length e = length e' ] ==> h ⊴sc h(a↦(Arr T f' e'))"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def)

subsection ‹Conformance›

definition sc_fconf :: "'m prog → cname → heap → fields → bool" (‹_,_,_ ⊨sc _ √› [51,51,51,51] 50)
where "P,C,h ⊨sc fs √ = (∀F D T fm. P ⊨ C has F:T (fm) in D ⟶ (∃v. fs(F,D) = Some v ∧ P,h ⊨sc v :≤ T))"

primrec sc_oconf :: "'m prog → heap → heapobj → bool"   (‹_,_ ⊨sc _ √› [51,51,51] 50)
where
  "P,h ⊨sc Obj C fs √ ⟷ is_class P C ∧ P,C,h ⊨sc fs √"
| "P,h ⊨sc Arr T fs el √ ⟷ is_type P (T⌊⌉) ∧ P,Object,h ⊨sc fs √ ∧ (∀v ∈ set el. P,h ⊨sc v :≤ T)"

definition sc_hconf :: "'m prog → heap → bool"  (‹_ ⊨sc _ √› [51,51] 50)
where "P ⊨sc h √ ⟷ (∀a obj. h a = Some obj ⟶ P,h ⊨sc obj √)"

interpretation sc: heap_conf_base  
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P .

declare sc.typeof_addr_thread_id2_addr_addr2thread_id [simp del]

lemma sc_conf_upd_obj: "h a = Some(Obj C fs) ==> (P,h(a↦(Obj C fs')) ⊨sc x :≤ T) = (P,h ⊨sc x :≤ T)"
apply (unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
apply (auto simp add: sc_typeof_addr_def split: if_split_asm)
done

lemma sc_conf_upd_arr: "h a = Some(Arr T f el) ==> (P,h(a↦(Arr T f' el')) ⊨sc x :≤ T') = (P,h ⊨sc x :≤ T')"
apply(unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
apply(auto simp add: sc_typeof_addr_def split: if_split_asm)
done

lemma sc_oconf_hext: "P,h ⊨sc obj √ ==> h ⊴sc h' ==> P,h' ⊨sc obj √"
by(cases obj)(fastforce elim: sc.conf_hext simp add: sc_fconf_def)+

lemma sc_oconf_init_fields:
  assumes "P ⊨ C has_fields FDTs"
  shows "P,h ⊨sc (Obj C (init_fields FDTs)) √"
using assms has_fields_is_class[OF assms]
by(auto simp add: has_field_def init_fields_def sc_fconf_def split_def o_def map_of_map[simplified split_def, where f="λp. default_val (fst p)"] dest: has_fields_fun)

lemma sc_oconf_init:
 "is_htype P hT ==> P,h ⊨sc blank P hT √"
by(cases hT)(auto simp add: sc_fconf_def has_field_def init_fields_def split_def o_def map_of_map[simplified split_def, where f="λp. default_val (fst p)"] dest: has_fields_fun)

lemma sc_oconf_fupd [intro?]:
  "[ P ⊨ C has F:T (fm) in D; P,h ⊨sc v :≤ T; P,h ⊨sc (Obj C fs) √ ]
  ==> P,h ⊨sc (Obj C (fs((F,D)↦v))) √"
unfolding has_field_def
by(auto simp add: sc_fconf_def has_field_def dest: has_fields_fun)

lemma sc_oconf_fupd_arr [intro?]:
  "[ P,h ⊨sc v :≤ T; P,h ⊨sc (Arr T f el) √ ]
  ==> P,h ⊨sc (Arr T f (el[i := v])) √"
by(auto dest: subsetD[OF set_update_subset_insert])

lemma sc_oconf_fupd_arr_fields:
  "[ P ⊨ Object has F:T (fm) in Object; P,h ⊨sc v :≤ T; P,h ⊨sc (Arr T' f el) √ ]
  ==> P,h ⊨sc (Arr T' (f((F, Object) ↦ v)) el) √"
by(auto dest: has_fields_fun simp add: sc_fconf_def has_field_def)

lemma sc_oconf_new: "[ P,h ⊨sc obj √; h a = None ] ==> P,h(a ↦ arrobj) ⊨sc obj √"
by(erule sc_oconf_hext)(rule sc_hext_new)

lemmas sc_oconf_upd_obj = sc_oconf_hext [OF _ sc_hext_upd_obj]

lemma sc_oconf_upd_arr:
  assumes "P,h ⊨sc obj √"
  and ha: "h a = ⌊Arr T f el⌋"
  shows "P,h(a ↦ Arr T f' el') ⊨sc obj √"
using assms
by(cases obj)(auto simp add: sc_conf_upd_arr[where h=h, OF ha] sc_fconf_def)

lemma sc_hconfD: "[ P ⊨sc h √; h a = Some obj ] ==> P,h ⊨sc obj √"
unfolding sc_hconf_def by blast

lemmas sc_preallocated_new = sc.preallocated_hext[OF _ sc_hext_new]
lemmas sc_preallocated_upd_obj = sc.preallocated_hext [OF _ sc_hext_upd_obj]
lemmas sc_preallocated_upd_arr = sc.preallocated_hext [OF _ sc_hext_upd_arr]

lemma sc_hconf_new: "[ P ⊨sc h √; h a = None; P,h ⊨sc obj √ ] ==> P ⊨sc h(a↦obj) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_new)

lemma sc_hconf_upd_obj: "[ P ⊨sc h √; h a = Some (Obj C fs); P,h ⊨sc (Obj C fs') √ ] ==> P ⊨sc h(a↦(Obj C fs')) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_obj simp del: sc_oconf.simps)

lemma sc_hconf_upd_arr: "[ P ⊨sc h √; h a = Some(Arr T f el); P,h ⊨sc (Arr T f' el') √ ] ==> P ⊨sc h(a↦(Arr T f' el')) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_arr simp del: sc_oconf.simps)

lemma sc_heap_conf: 
  "heap_conf addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_write (sc_hconf P) P"
proof
  show "P ⊨sc sc_empty √" by(simp add: sc_hconf_def)
next
  fix h a hT
  assume "sc_typeof_addr h a = ⌊hT⌋" "P ⊨sc h √"
  thus "is_htype P hT"
    by(auto simp add: sc_typeof_addr_def sc_oconf_def dest!: sc_hconfD split: heapobj.split_asm)
next
  fix h h' hT a
  assume "P ⊨sc h √" "(h', a) ∈ sc_allocate P h hT" "is_htype P hT"
  thus "P ⊨sc h' √"
    by(auto simp add: sc_allocate_def dest!: new_Addr_SomeD intro: sc_hconf_new sc_oconf_init split: if_split_asm)
next
  fix h a al T v h'
  assume "P ⊨sc h √"
    and "sc.addr_loc_type P h a al T"
    and "P,h ⊨sc v :≤ T"
    and "sc_heap_write h a al v h'"
  thus "P ⊨sc h' √"
    by(cases al)(fastforce elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def intro: sc_hconf_upd_obj sc_oconf_fupd sc_hconfD sc_hconf_upd_arr sc_oconf_fupd_arr sc_oconf_fupd_arr_fields)+
qed

interpretation sc: heap_conf
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P 
by(rule sc_heap_conf)

lemma sc_heap_progress:
  "heap_progress addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
proof
  fix h a al T
  assume hconf: "P ⊨sc h √"
    and alt: "sc.addr_loc_type P h a al T"
  from alt obtain arrobj where arrobj: "h a = ⌊arrobj⌋"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  from alt show "∃v. sc_heap_read h a al v ∧ P,h ⊨sc v :≤ T"
  proof(cases)
    case (addr_loc_type_field U F fm D) 
    note [simp] = ‹al = CField D F›
    show ?thesis
    proof(cases "arrobj")
      case (Obj C' fs)
      with ‹sc_typeof_addr h a = ⌊U⌋› arrobj
      have [simp]: "C' = class_type_of U" by(auto simp add: sc_typeof_addr_def)
      from hconf arrobj Obj have "P,h ⊨sc Obj (class_type_of U) fs √" by(auto dest: sc_hconfD)
      with ‹P ⊨ class_type_of U has F:T (fm) in D› obtain v 
        where "fs (F, D) = ⌊v⌋" "P,h ⊨sc v :≤ T" by(fastforce simp add: sc_fconf_def)
      thus ?thesis using Obj arrobj by(auto intro: sc_heap_read.intros)
    next
      case (Arr T' f el)
      with ‹sc_typeof_addr h a = ⌊U⌋› arrobj
      have [simp]: "U = Array_type T' (length el)" by(auto simp add: sc_typeof_addr_def)
      from hconf arrobj Arr have "P,h ⊨sc Arr T' f el √" by(auto dest: sc_hconfD)
      from ‹P ⊨ class_type_of U has F:T (fm) in D› have [simp]: "D = Object"
        by(auto dest: has_field_decl_above)
      with ‹P,h ⊨sc Arr T' f el √› ‹P ⊨ class_type_of U has F:T (fm) in D›
      obtain v where "f (F, Object) = ⌊v⌋" "P,h ⊨sc v :≤ T"
        by(fastforce simp add: sc_fconf_def)
      thus ?thesis using Arr arrobj by(auto intro: sc_heap_read.intros)
    qed
  next
    case (addr_loc_type_cell n' n)
    with arrobj obtain f el
      where [simp]: "arrobj = Arr T f el"
      by(cases arrobj)(auto simp add: sc_typeof_addr_def)
    from addr_loc_type_cell arrobj
    have [simp]: "al = ACell n" "n < length el" by(auto simp add: sc_typeof_addr_def)
    from hconf arrobj have "P,h ⊨sc Arr T f el √" by(auto dest: sc_hconfD)
    hence "P,h ⊨sc el ! n :≤ T" by(fastforce)
    thus ?thesis using arrobj by(fastforce intro: sc_heap_read.intros)
  qed
next
  fix h a al T v
  assume alt: "sc.addr_loc_type P h a al T"
  from alt obtain arrobj where arrobj: "h a = ⌊arrobj⌋"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  thus "∃h'. sc_heap_write h a al v h'" using alt
    by(cases arrobj)(fastforce intro: sc_heap_write.intros elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def dest: has_field_decl_above)+
qed

interpretation sc: heap_progress
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P
by(rule sc_heap_progress)

lemma sc_heap_conf_read:
  "heap_conf_read addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
proof
  fix h a al v T
  assume read: "sc_heap_read h a al v"
    and alt: "sc.addr_loc_type P h a al T"
    and hconf: "P ⊨sc h √"
  thus "P,h ⊨sc v :≤ T"
    by(auto elim!: sc_heap_read.cases sc.addr_loc_type.cases simp add: sc_typeof_addr_def)(fastforce dest!: sc_hconfD simp add: sc_fconf_def)+
qed

interpretation sc: heap_conf_read
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P
by(rule sc_heap_conf_read)

abbreviation sc_deterministic_heap_ops :: "'m prog → bool"
where "sc_deterministic_heap_ops ≡ sc.deterministic_heap_ops TYPE('m)"

lemma sc_deterministic_heap_ops: "¬ sc_spurious_wakeups ==> sc_deterministic_heap_ops P"
by(rule sc.deterministic_heap_opsI)(auto elim: sc_heap_read.cases sc_heap_write.cases simp add: sc_allocate_def)

subsection ‹Code generation›

code_pred 
  (modes: i → i → i → i → bool, i → i → i → o → bool)
  sc_heap_read .

code_pred 
  (modes: i → i → i → i → i → bool, i → i → i → i → o → bool)
  sc_heap_write .

lemma eval_sc_heap_read_i_i_i_o:
  "Predicate.eval (sc_heap_read_i_i_i_o h ad al) = sc_heap_read h ad al"
by(auto elim: sc_heap_read_i_i_i_oE intro: sc_heap_read_i_i_i_oI intro!: ext)

lemma eval_sc_heap_write_i_i_i_i_o:
  "Predicate.eval (sc_heap_write_i_i_i_i_o h ad al v) = sc_heap_write h ad al v"
by(auto elim: sc_heap_write_i_i_i_i_oE intro: sc_heap_write_i_i_i_i_oI intro!: ext)

end