|
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 |