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