|
25
|
1 |
(* Author: Andrew Boyton, 2012
|
|
|
2 |
Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
|
|
|
3 |
Rafal Kolanski <rafal.kolanski at nicta.com.au>
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
header "Defining some separation logic maps-to predicates on top of the instantiation."
|
|
|
7 |
|
|
|
8 |
theory Separation_D
|
|
|
9 |
imports Abstract_Separation_D
|
|
|
10 |
begin
|
|
|
11 |
|
|
|
12 |
type_synonym sep_pred = "sep_state \<Rightarrow> bool"
|
|
|
13 |
|
|
|
14 |
definition
|
|
|
15 |
state_sep_projection :: "cdl_state \<Rightarrow> sep_state"
|
|
|
16 |
where
|
|
|
17 |
"state_sep_projection \<equiv> \<lambda>s. SepState (cdl_objects s) (cdl_ghost_state s)"
|
|
|
18 |
|
|
|
19 |
(* This turns a separation logic predicate into a predicate on the capDL state. *)
|
|
|
20 |
abbreviation
|
|
|
21 |
lift' :: "(sep_state \<Rightarrow> 'a) \<Rightarrow> cdl_state \<Rightarrow> 'a" ("<_>")
|
|
|
22 |
where
|
|
|
23 |
"<P> s \<equiv> P (state_sep_projection s)"
|
|
|
24 |
|
|
|
25 |
(* The generalisation of the maps to operator for separation logic. *)
|
|
|
26 |
definition
|
|
|
27 |
sep_map_general :: "cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> cdl_components \<Rightarrow> sep_pred"
|
|
|
28 |
where
|
|
|
29 |
"sep_map_general p obj gs \<equiv> \<lambda>s. sep_heap s = [p \<mapsto> obj] \<and> sep_ghost_state s p = gs"
|
|
|
30 |
|
|
|
31 |
(* Alternate definition without the [p \<mapsto> obj] notation. *)
|
|
|
32 |
lemma sep_map_general_def2:
|
|
|
33 |
"sep_map_general p obj gs s =
|
|
|
34 |
(dom (sep_heap s) = {p} \<and> ko_at obj p (sep_heap s) \<and> sep_ghost_state s p = gs)"
|
|
|
35 |
apply (clarsimp simp: sep_map_general_def object_at_def)
|
|
|
36 |
apply (rule)
|
|
|
37 |
apply clarsimp
|
|
|
38 |
apply (clarsimp simp: fun_upd_def)
|
|
|
39 |
apply (rule ext)
|
|
|
40 |
apply (fastforce simp: dom_def split:split_if)
|
|
|
41 |
done
|
|
|
42 |
|
|
|
43 |
(* There is an object there. *)
|
|
|
44 |
definition
|
|
|
45 |
sep_map_i :: "cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> sep_pred" ("_ \<mapsto>i _" [76,71] 76)
|
|
|
46 |
where
|
|
|
47 |
"p \<mapsto>i obj \<equiv> sep_map_general p obj UNIV"
|
|
|
48 |
|
|
|
49 |
(* The fields are there (and there are no caps). *)
|
|
|
50 |
definition
|
|
|
51 |
sep_map_f :: "cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> sep_pred" ("_ \<mapsto>f _" [76,71] 76)
|
|
|
52 |
where
|
|
|
53 |
"p \<mapsto>f obj \<equiv> sep_map_general p (update_slots empty obj) {None}"
|
|
|
54 |
|
|
|
55 |
(* There is that cap there. *)
|
|
|
56 |
definition
|
|
|
57 |
sep_map_c :: "cdl_cap_ref \<Rightarrow> cdl_cap \<Rightarrow> sep_pred" ("_ \<mapsto>c _" [76,71] 76)
|
|
|
58 |
where
|
|
|
59 |
"p \<mapsto>c cap \<equiv> \<lambda>s. let (obj_id, slot) = p; heap = sep_heap s in
|
|
|
60 |
\<exists>obj. sep_map_general obj_id obj {Some slot} s \<and> object_slots obj = [slot \<mapsto> cap]"
|
|
|
61 |
|
|
|
62 |
definition
|
|
|
63 |
sep_any :: "('a \<Rightarrow> 'b \<Rightarrow> sep_pred) \<Rightarrow> ('a \<Rightarrow> sep_pred)" where
|
|
|
64 |
"sep_any m \<equiv> (\<lambda>p s. \<exists>v. (m p v) s)"
|
|
|
65 |
|
|
|
66 |
abbreviation "sep_any_map_i \<equiv> sep_any sep_map_i"
|
|
|
67 |
notation sep_any_map_i ("_ \<mapsto>i -" 76)
|
|
|
68 |
|
|
|
69 |
abbreviation "sep_any_map_c \<equiv> sep_any sep_map_c"
|
|
|
70 |
notation sep_any_map_c ("_ \<mapsto>c -" 76)
|
|
|
71 |
|
|
|
72 |
end
|