Theory Concrete_heap

(*<*)

theory Concrete_heap
imports
  "HOL-Library.Saturated"
  "../Global_Invariants"
begin

(* From 40e16c534243 by Makarius. Doesn't seem to have a huge impact on run time now (2021-01-07) *)
declare subst_all [simp del] [[simproc del: defined_all]]

(*>*)
type_synonym field = "3"
type_synonym mut = "2"
type_synonym payload = "unit"
type_synonym ref = "5"

type_synonym concrete_local_state = "(field, mut, payload, ref) local_state"
type_synonym clsts = "(field, mut, payload, ref) lsts"

abbreviation mut_common_init_state :: concrete_local_state where
  "mut_common_init_state ≡ undefined⦇ ghost_hs_phase := hp_IdleMarkSweep, ghost_honorary_grey := {}, ghost_honorary_root := {}, roots := {}, W := {} ⦈"

context gc_system
begin

abbreviation sys_init_heap :: "ref ⇒ (field, payload, ref) object option" where
  "sys_init_heap ≡
  [   0 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = [ 0 ↦ 5 ],
             obj_payload = Map.empty ⦈,
      1 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = Map.empty,
             obj_payload = Map.empty ⦈,
      2 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = Map.empty,
             obj_payload = Map.empty ⦈,
      3 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = [ 0 ↦ 1 , 1 ↦ 2 ],
             obj_payload = Map.empty ⦈,
      4 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = [ 1 ↦ 0 ],
             obj_payload = Map.empty ⦈,
      5 ↦ ⦇ obj_mark = initial_mark,
             obj_fields = Map.empty,
             obj_payload = Map.empty ⦈
  ]"

abbreviation mut_init_state0 :: concrete_local_state where
  "mut_init_state0 ≡ mut_common_init_state ⦇ roots := {1, 2, 3} ⦈"

abbreviation mut_init_state1 :: concrete_local_state where
  "mut_init_state1 ≡ mut_common_init_state ⦇ roots := {3} ⦈"

abbreviation mut_init_state2 :: concrete_local_state where
  "mut_init_state2 ≡ mut_common_init_state ⦇ roots := {2, 5} ⦈"

end
(*<*)

end
(*>*)