1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11theory AbstractSeparation_SD
12imports
13  AbstractSeparationHelpers_SD
14  "Sep_Algebra.Map_Extra"
15  "DSpec.Types_D"
16begin
17
18datatype cdl_component_id = Fields | Slot nat
19type_synonym cdl_component_ids = "cdl_component_id set"
20
21translations
22  (type) "cdl_component_ids" <=(type) "cdl_component_id set"
23
24(* The cdl_component are the pieces of capDL objects that we are interested in our lifted heap.
25 * These components are either objects without capabilities or capabilities.
26 *)
27datatype cdl_component = CDL_Object cdl_object | CDL_Cap "cdl_cap option"
28
29(* The state for separation logic is an option map
30 * from (obj_id,component) to sep_entities
31 *)
32type_synonym sep_state_heap = "(cdl_object_id \<times> cdl_component_id) \<Rightarrow> cdl_component option"
33type_synonym sep_state_irq_map = "cdl_irq \<Rightarrow> cdl_object_id option"
34
35translations
36  (type) "sep_state_heap" <=(type) "32 word \<times> cdl_component_id \<Rightarrow> cdl_component option"
37  (type) "sep_state_irq_map" <=(type) "8 word \<Rightarrow> 32 word option"
38
39
40(* Our lifted state contains sep_entities and the IRQ table.
41 *)
42datatype sep_state =
43  SepState "(cdl_object_id \<times> cdl_component_id) \<Rightarrow> cdl_component option"
44           "cdl_irq \<Rightarrow> cdl_object_id option"
45
46(* Functions to get the object heap and the irq table from the sep_state. *)
47primrec sep_heap :: "sep_state \<Rightarrow> sep_state_heap"
48where "sep_heap (SepState heap irqs) = heap"
49
50primrec sep_irq_node :: "sep_state \<Rightarrow> sep_state_irq_map"
51where "sep_irq_node (SepState heap irqs) = irqs"
52
53(* Adding states adds the separation entity heap and the IRQ table.
54 *)
55definition
56  sep_state_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> sep_state"
57where
58  "sep_state_add state_a state_b \<equiv>
59  SepState ((sep_heap state_a) ++ (sep_heap state_b))
60           ((sep_irq_node state_a) ++ sep_irq_node state_b)"
61
62
63(* State are disjoint the separation entity heaps and the IRQ tables are dijoint.
64 *)
65definition
66  sep_state_disj :: "sep_state \<Rightarrow> sep_state \<Rightarrow> bool"
67where
68  "sep_state_disj state_a state_b \<equiv>
69   (sep_heap state_a) \<bottom> (sep_heap state_b) \<and>
70   (sep_irq_node state_a) \<bottom> (sep_irq_node state_b)"
71
72lemma sep_state_add_comm:
73  "sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x"
74  by (fastforce simp: sep_state_add_def sep_state_disj_def intro!:map_add_com)
75
76(*********************************************)
77(* Definition of separation logic for capDL. *)
78(*********************************************)
79
80instantiation "sep_state" :: zero
81begin
82  definition "0 \<equiv> SepState (\<lambda>p. None) Map.empty"
83  instance ..
84end
85
86instantiation "sep_state" :: stronger_sep_algebra
87begin
88
89definition "(##) \<equiv> sep_state_disj"
90definition "(+) \<equiv> sep_state_add"
91
92
93
94(************************************************
95 * The proof that this is a separation algebra. *
96 ************************************************)
97
98instance
99  apply standard
100(* x ## 0 *)
101       apply (simp add: sep_disj_sep_state_def sep_state_disj_def zero_sep_state_def)
102(* x ## y \<Longrightarrow> y ## x *)
103      apply (clarsimp simp: sep_disj_sep_state_def sep_state_disj_def Let_unfold
104                            map_disj_com Int_commute)
105(* x + 0 = x *)
106     apply (simp add: plus_sep_state_def sep_state_add_def zero_sep_state_def)
107     apply (case_tac x,simp)
108(* x ## y \<Longrightarrow> x + y = y + x *)
109    apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def)
110    apply (erule sep_state_add_comm)
111(* (x + y) + z = x + (y + z) *)
112   apply (simp add: plus_sep_state_def sep_state_add_def)+
113(* x ## y + z = (x ## y \<and> x ## z) *)
114   apply (clarsimp simp: sep_disj_sep_state_def)
115   apply (auto simp: map_disj_def sep_state_disj_def)
116  done
117end
118
119(*************************************************************
120 * The proof that this is a cancellative separation algebra. *
121 *************************************************************)
122
123instantiation "sep_state" :: cancellative_sep_algebra
124begin
125
126instance
127  apply (standard; simp add: sep_disj_sep_state_def sep_state_disj_def zero_sep_state_def
128                   plus_sep_state_def sep_state_add_def)
129  apply (metis map_add_subsumed1 map_le_refl sep_heap.simps sep_irq_node.simps sep_state.exhaust)
130  by (metis map_add_left_eq sep_heap.simps sep_irq_node.simps sep_state.exhaust)
131end
132
133end
134
135