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