Theory Separation_D

(* Author: Andrew Boyton, 2012
   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
                Rafal Kolanski <rafal.kolanski at nicta.com.au>
*)

section "Defining some separation logic maps-to predicates on top of the instantiation."

theory Separation_D
imports Abstract_Separation_D
begin

type_synonym sep_pred = "sep_state ⇒ bool"

definition
  state_sep_projection :: "cdl_state ⇒ sep_state"
where
  "state_sep_projection ≡ λs. SepState (cdl_objects s) (cdl_ghost_state s)"

(* This turns a separation logic predicate into a predicate on the capDL state. *)
abbreviation
  lift' :: "(sep_state ⇒ 'a) ⇒ cdl_state ⇒ 'a" ("<_>")
where
  "<P> s ≡ P (state_sep_projection s)"

(* The generalisation of the maps to operator for separation logic. *)
definition
  sep_map_general :: "cdl_object_id ⇒ cdl_object ⇒ cdl_components ⇒ sep_pred"
where
  "sep_map_general p obj gs ≡ λs. sep_heap s = [p ↦ obj] ∧ sep_ghost_state s p = gs"

(* Alternate definition without the [p ↦ obj] notation. *)
lemma sep_map_general_def2:
  "sep_map_general p obj gs s =
   (dom (sep_heap s) = {p} ∧ ko_at obj p (sep_heap s) ∧ sep_ghost_state s p = gs)"
  apply (clarsimp simp: sep_map_general_def object_at_def)
  apply (rule)
   apply clarsimp
  apply (clarsimp simp: fun_upd_def)
  apply (rule ext)
  apply (fastforce simp: dom_def split:if_split)
  done

(* There is an object there. *)
definition
  sep_map_i :: "cdl_object_id ⇒ cdl_object ⇒ sep_pred" ("_ ↦i _" [76,71] 76)
where
  "p ↦i obj ≡ sep_map_general p obj UNIV"

(* The fields are there (and there are no caps). *)
definition
  sep_map_f :: "cdl_object_id ⇒ cdl_object ⇒ sep_pred" ("_ ↦f _" [76,71] 76)
where
  "p ↦f obj ≡ sep_map_general p (update_slots Map.empty obj) {None}"

(* There is that cap there. *)
definition
  sep_map_c :: "cdl_cap_ref ⇒ cdl_cap ⇒ sep_pred" ("_ ↦c _" [76,71] 76)
where
  "p ↦c cap ≡ λs. let (obj_id, slot) = p; heap = sep_heap s in
  ∃obj. sep_map_general obj_id obj {Some slot} s ∧ object_slots obj = [slot ↦ cap]"

definition
  sep_any :: "('a ⇒ 'b ⇒ sep_pred) ⇒ ('a ⇒ sep_pred)" where
  "sep_any m ≡ (λp s. ∃v. (m p v) s)"

abbreviation "sep_any_map_i ≡ sep_any sep_map_i"
notation sep_any_map_i ("_ ↦i -" 76)

abbreviation "sep_any_map_c ≡ sep_any sep_map_c"
notation sep_any_map_c ("_ ↦c -" 76)

end