1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory GlobalsSwap 8imports 9 "Lib.Lib" 10 "CParser.CTranslation" 11 "CParser.PackedTypes" 12begin 13 14datatype 'g global_data = 15 GlobalData "string" "nat" "addr \<Rightarrow> bool" "'g \<Rightarrow> word8 list" 16 "word8 list \<Rightarrow> 'g \<Rightarrow> 'g" 17 | ConstGlobalData "string" "nat" "addr \<Rightarrow> bool" 18 "word8 list" "word8 list \<Rightarrow> bool" 19 | AddressedGlobalData "string" "nat" "addr \<Rightarrow> bool" 20 (* in each case the symbol name, length in bytes, tag and constraint on 21 address. for active globals a getter/setter, for const globals 22 a sample value and a way to check a value *) 23 24definition 25 is_const_global_data :: "'g global_data \<Rightarrow> bool" 26where 27 "is_const_global_data gd = 28 (case gd of ConstGlobalData nm m ok v chk \<Rightarrow> True | _ \<Rightarrow> False)" 29 30definition 31 is_addressed_global_data :: "'g global_data \<Rightarrow> bool" 32where 33 "is_addressed_global_data gd = 34 (case gd of AddressedGlobalData _ _ _ \<Rightarrow> True | _ \<Rightarrow> False)" 35 36definition 37 is_global_data :: "'g global_data \<Rightarrow> bool" 38where 39 "is_global_data gd = 40 (case gd of GlobalData _ _ _ _ _ \<Rightarrow> True | _ \<Rightarrow> False)" 41 42definition 43 "global_data_region symtab gd = (case gd of 44 GlobalData name m b g s \<Rightarrow> {symtab name ..+ m} 45 | ConstGlobalData name m b v chk \<Rightarrow> {symtab name ..+ m} 46 | AddressedGlobalData name m b \<Rightarrow> {})" 47 48definition 49 "global_data_ok symtab gd = 50 (case gd of GlobalData nm _ ok _ _ \<Rightarrow> ok (symtab nm) 51 | ConstGlobalData nm _ ok _ _ \<Rightarrow> ok (symtab nm) 52 | AddressedGlobalData nm _ ok \<Rightarrow> ok (symtab nm))" 53 54definition 55 global_data :: "string \<Rightarrow> 56 ('g \<Rightarrow> ('a :: packed_type)) \<Rightarrow> 57 (('a \<Rightarrow> 'a) \<Rightarrow> 'g \<Rightarrow> 'g) \<Rightarrow> 'g global_data" 58where 59 "global_data name getter updator 60 = GlobalData name (size_of TYPE('a)) 61 (\<lambda>addr. c_guard (Ptr addr :: 'a ptr)) 62 (to_bytes_p o getter) 63 (updator o K o from_bytes)" 64 65type_synonym 'g hrs_update = "(heap_raw_state \<Rightarrow> heap_raw_state) \<Rightarrow> 'g \<Rightarrow> 'g" 66 67definition 68 global_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update 69 \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> 'g global_data \<Rightarrow> 'g \<Rightarrow> 'g" 70where 71 "global_swap g_hrs g_hrs_upd symtab gd \<equiv> 72 (case gd of GlobalData name len n g p \<Rightarrow> \<lambda>gs. 73 g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab name) 74 (take len (g (g_hrs_upd (K undefined) gs)))) (g_hrs gs)) 75 (p (heap_list (hrs_mem (g_hrs gs)) len (symtab name)) 76 (g_hrs_upd (K undefined) gs)) 77 | _ \<Rightarrow> id)" 78 79definition 80 globals_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update 81 \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> 'g global_data list \<Rightarrow> 'g \<Rightarrow> 'g" 82where 83 "globals_swap g_hrs g_hrs_upd symtab gds 84 = foldr (global_swap g_hrs g_hrs_upd symtab) gds" 85 86lemma foldr_does_nothing_to_xf: 87 "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s \<rbrakk> 88 \<Longrightarrow> xf (foldr f xs s) = xf s" 89 by (induct xs, simp_all) 90 91lemma intvl_empty2: 92 "({p ..+ n} = {}) = (n = 0)" 93 by (auto simp add: intvl_def) 94 95lemma heap_update_list_commute: 96 "{p ..+ length xs} \<inter> {q ..+ length ys} = {} 97 \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) 98 = heap_update_list q ys (heap_update_list p xs hp)" 99 apply (cases "length xs < addr_card") 100 apply (cases "length ys < addr_card") 101 apply (rule ext, simp add: heap_update_list_value) 102 apply blast 103 apply (simp_all add: addr_card intvl_overflow intvl_empty2) 104 done 105 106lemma heap_update_commute: 107 "\<lbrakk>d,g \<Turnstile>\<^sub>t p; d,g' \<Turnstile>\<^sub>t q; \<not> TYPE('a) <\<^sub>\<tau> TYPE('b); \<not> field_of_t q p; 108 wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)) \<rbrakk> 109 \<Longrightarrow> heap_update p v (heap_update q (u :: 'b :: c_type) h) 110 = heap_update q u (heap_update p (v :: 'a :: c_type) h)" 111 apply (drule(3) h_t_valid_neq_disjoint) 112 apply (simp add: heap_update_def) 113 apply (simp add: heap_update_list_commute heap_list_update_disjoint_same 114 to_bytes_def length_fa_ti size_of_def Int_commute) 115 done 116 117definition 118 global_data_swappable :: "'g global_data \<Rightarrow> 'g global_data \<Rightarrow> bool" 119where 120 "global_data_swappable gd gd' \<equiv> case (gd, gd') of 121 (GlobalData _ _ _ g s, GlobalData _ _ _ g' s') \<Rightarrow> 122 (\<forall>v v' gs. s v (s' v' gs) = s' v' (s v gs)) 123 \<and> (\<forall>v gs. g (s' v gs) = g gs) 124 \<and> (\<forall>v gs. g' (s v gs) = g' gs) 125 | _ \<Rightarrow> True" 126 127definition 128 global_data_valid :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update 129 \<Rightarrow> 'g global_data \<Rightarrow> bool" 130where 131 "global_data_valid g_hrs g_hrs_upd gd \<equiv> 132 (case gd of GlobalData _ l _ g s \<Rightarrow> 133 (\<forall>gs. length (g gs) = l) 134 \<and> (\<forall>v v' gs. s v (s v' gs) = s v gs) 135 \<and> (\<forall>gs. s (g gs) gs = gs) 136 \<and> (\<forall>v gs. length v = l \<longrightarrow> g (s v gs) = v) 137 \<and> (\<forall>v f gs. (s v (g_hrs_upd f gs)) = g_hrs_upd f (s v gs)) 138 \<and> (\<forall>v gs. g_hrs (s v gs) = g_hrs gs) 139 \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) 140 \<and> l < addr_card 141 | _ \<Rightarrow> True)" 142 143definition 144 "global_acc_valid g_hrs g_hrs_upd \<equiv> 145 (\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s)) 146 \<and> (\<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f o f') s) 147 \<and> (\<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s)" 148 149lemma global_swap_swap: 150 "\<lbrakk> global_data_region symtab gd \<inter> global_data_region symtab gd' = {}; 151 global_acc_valid g_hrs g_hrs_upd; global_data_swappable gd gd'; 152 global_data_valid g_hrs g_hrs_upd gd; global_data_valid g_hrs g_hrs_upd gd' \<rbrakk> 153 \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab gd (global_swap g_hrs g_hrs_upd symtab gd' gs) 154 = global_swap g_hrs g_hrs_upd symtab gd' (global_swap g_hrs g_hrs_upd symtab gd gs)" 155 apply (clarsimp simp add: global_swap_def hrs_mem_update 156 global_data_swappable_def global_data_valid_def 157 global_acc_valid_def o_def 158 split: global_data.split_asm) 159 apply (clarsimp simp: global_data_region_def K_def) 160 apply (simp add: heap_list_update_disjoint_same Int_commute) 161 apply (simp add: hrs_mem_update_def split_def) 162 apply (subst heap_update_list_commute, simp_all) 163 done 164 165lemma heap_update_list_double_id: 166 "\<lbrakk> heap_list hp n ptr = xs; length xs' = length xs; 167 length xs < addr_card \<rbrakk> \<Longrightarrow> 168 heap_update_list ptr xs (heap_update_list ptr xs' hp) = hp" 169 apply (rule ext, simp add: heap_update_list_value') 170 apply (clarsimp simp: heap_list_nth intvl_def) 171 done 172 173lemma global_swap_cancel: 174 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 175 global_data_valid g_hrs g_hrs_upd gd \<rbrakk> 176 \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab gd (global_swap g_hrs g_hrs_upd symtab gd gs) = gs" 177 apply (insert heap_list_update[where 178 v="case gd of GlobalData _ _ _ g _ \<Rightarrow> g gs"]) 179 apply (clarsimp simp: global_swap_def hrs_mem_update 180 global_data_valid_def global_acc_valid_def 181 split: global_data.split) 182 apply (simp add: hrs_mem_update_def split_def o_def) 183 apply (simp add: heap_update_list_double_id hrs_mem_def) 184 done 185 186lemma foldr_update_commutes: 187 "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> f (g x s) = g x (f s) \<rbrakk> 188 \<Longrightarrow> f (foldr g xs s) = foldr g xs (f s)" 189 by (induct xs, simp_all) 190 191definition 192 "globals_list_valid symtab g_hrs g_hrs_upd xs = 193 (distinct_prop global_data_swappable xs 194 \<and> (\<forall>x \<in> set xs. global_data_valid g_hrs g_hrs_upd x) 195 \<and> (\<forall>x \<in> set xs. global_data_ok symtab x))" 196 197lemma global_data_swappable_sym: 198 "global_data_swappable x y = global_data_swappable y x" 199 by (auto simp add: global_data_swappable_def 200 split: global_data.split) 201 202lemma hrs_htd_globals_swap: 203 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 204 \<forall>x \<in> set xs. global_data_valid g_hrs g_hrs_upd x \<rbrakk> 205 \<Longrightarrow> hrs_htd (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)) 206 = hrs_htd (g_hrs gs)" 207 unfolding globals_swap_def 208 apply (rule foldr_does_nothing_to_xf) 209 apply (simp add: global_swap_def global_acc_valid_def 210 split: global_data.split prod.split bool.split) 211 done 212 213lemmas foldr_hrs_htd_global_swap = hrs_htd_globals_swap[unfolded globals_swap_def] 214 215definition 216 globals_list_distinct :: "addr set \<Rightarrow> (string \<Rightarrow> addr) 217 \<Rightarrow> 'g global_data list \<Rightarrow> bool" 218where 219 "globals_list_distinct D symtab gds = distinct_prop (\<lambda>S T. S \<inter> T = {}) 220 (D # map (global_data_region symtab) gds)" 221 222lemma globals_swap_twice_helper: 223 "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd xs; 224 global_acc_valid g_hrs g_hrs_upd; 225 globals_list_distinct D symtab xs \<rbrakk> 226 \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (globals_swap g_hrs g_hrs_upd symtab xs gs) = gs" 227 apply (simp add: globals_swap_def) 228 apply (clarsimp simp: foldr_hrs_htd_global_swap globals_list_valid_def) 229 apply (induct xs) 230 apply simp 231 apply (clarsimp simp: globals_list_distinct_def) 232 apply (subst foldr_update_commutes[where f="global_swap g_hrs g_hrs_upd symtab v" for v]) 233 apply (rule global_swap_swap, auto)[1] 234 apply (simp add: global_swap_cancel foldr_hrs_htd_global_swap) 235 done 236 237lemma disjoint_int_intvl_min: 238 "\<lbrakk> S \<inter> {p ..+ n} = {} \<rbrakk> 239 \<Longrightarrow> S \<inter> {p ..+ min m n} = {}" 240 using intvl_start_le[where x="min m n" and y=n] 241 by auto 242 243lemma ptr_set_disjoint_footprint: 244 "(s_footprint (p :: ('a :: c_type) ptr) \<inter> (S \<times> UNIV) = {}) 245 \<Longrightarrow> ({ptr_val p ..+ size_of TYPE('a)} \<inter> S = {})" 246 by (auto simp add: s_footprint_intvl[symmetric]) 247 248lemma disjoint_heap_list_globals_swap_filter: 249 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 250 globals_list_distinct D symtab (filter is_global_data xs); 251 {p ..+ n} \<subseteq> D \<rbrakk> 252 \<Longrightarrow> heap_list (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) n p 253 = heap_list (hrs_mem (g_hrs gs)) n p" 254 apply (clarsimp simp: globals_swap_def) 255 apply (rule foldr_does_nothing_to_xf) 256 apply (clarsimp simp: global_swap_def hrs_mem_update 257 global_acc_valid_def globals_list_distinct_def 258 split: global_data.split) 259 apply (subst heap_list_update_disjoint_same, simp_all) 260 apply (drule spec, drule mp, erule conjI, simp add: is_global_data_def) 261 apply (simp add: Int_commute global_data_region_def) 262 apply (rule disjoint_int_intvl_min) 263 apply blast 264 done 265 266lemma disjoint_h_val_globals_swap_filter: 267 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 268 globals_list_distinct D symtab (filter is_global_data xs); 269 s_footprint p \<subseteq> D \<times> UNIV \<rbrakk> 270 \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) p 271 = h_val (hrs_mem (g_hrs gs)) p" 272 apply (clarsimp simp: h_val_def) 273 apply (subst disjoint_heap_list_globals_swap_filter[where g_hrs=g_hrs], assumption+) 274 apply (auto simp: s_footprint_intvl[symmetric])[1] 275 apply simp 276 done 277 278lemma distinct_prop_filter: 279 "distinct_prop P (filter Q xs) 280 = distinct_prop (\<lambda>x y. Q x \<and> Q y \<longrightarrow> P x y) xs" 281 by (induct xs, auto) 282 283lemma distinct_prop_weaken: 284 "\<lbrakk> distinct_prop P xs; \<And>x y. P x y \<Longrightarrow> Q x y \<rbrakk> 285 \<Longrightarrow> distinct_prop Q xs" 286 by (induct xs, simp_all) 287 288lemma globals_list_distinct_filter: 289 "globals_list_distinct D symtab xs 290 \<Longrightarrow> globals_list_distinct D symtab (filter P xs)" 291 by (clarsimp simp: globals_list_distinct_def 292 distinct_prop_map distinct_prop_filter 293 elim!: distinct_prop_weaken) 294 295lemmas disjoint_h_val_globals_swap 296 = disjoint_h_val_globals_swap_filter[OF _ globals_list_distinct_filter] 297 298lemma disjoint_heap_update_globals_swap_filter: 299 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 300 globals_list_distinct D symtab (filter is_global_data xs); 301 s_footprint (p :: ('a :: wf_type) ptr) \<subseteq> D \<times> UNIV \<rbrakk> 302 \<Longrightarrow> g_hrs_upd (hrs_mem_update (heap_update p v)) (globals_swap g_hrs g_hrs_upd symtab xs gs) 303 = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update p v)) gs)" 304 apply (clarsimp simp: globals_swap_def global_acc_valid_def) 305 apply (rule foldr_update_commutes) 306 apply (clarsimp simp: global_swap_def hrs_mem_update h_val_def 307 heap_update_def o_def K_def 308 globals_list_distinct_def 309 split: global_data.split) 310 apply (drule spec, drule mp, erule conjI, simp add: is_global_data_def) 311 apply (rule_tac f="g_hrs_upd" in arg_cong2[rotated]) 312 313 apply (subst heap_list_update_disjoint_same, simp_all) 314 apply (rule ptr_set_disjoint_footprint) 315 apply (simp add: global_data_region_def) 316 apply blast 317 318 apply (clarsimp simp: hrs_mem_update_def split_def) 319 apply (subst heap_update_list_commute) 320 apply (simp add: to_bytes_def length_fa_ti size_of_def 321 global_data_region_def) 322 apply (intro disjoint_int_intvl_min 323 ptr_set_disjoint_footprint[unfolded size_of_def]) 324 apply blast 325 326 apply (subst heap_list_update_disjoint_same, 327 simp_all add: global_data_region_def) 328 apply (simp add: Int_commute) 329 apply (intro disjoint_int_intvl_min 330 ptr_set_disjoint_footprint) 331 apply blast 332 done 333 334lemmas disjoint_heap_update_globals_swap 335 = disjoint_heap_update_globals_swap_filter[OF _ globals_list_distinct_filter] 336 337lemma to_bytes_p_from_bytes: 338 "length xs = size_of TYPE ('a :: packed_type) 339 \<Longrightarrow> to_bytes_p (from_bytes xs :: 'a) = xs" 340 by (simp add: to_bytes_p_def to_bytes_def from_bytes_def 341 update_ti_t_def size_of_def 342 field_access_update_same td_fafu_idem) 343 344lemma to_bytes_p_inj: 345 "inj (to_bytes_p :: ('a :: packed_type) \<Rightarrow> _)" 346 apply (rule inj_onI) 347 apply (drule_tac f=from_bytes in arg_cong) 348 apply (simp add: to_bytes_p_def) 349 apply (subst(asm) CTypes.inv | simp)+ 350 done 351 352lemma global_data_valid: 353 "global_data_valid g_hrs g_hrs_upd (global_data p (g :: 'g \<Rightarrow> ('a :: packed_type)) s) 354 = ( 355 (\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) 356 \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) 357 \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) 358 \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) 359 \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) 360 \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v))" 361proof - 362 have all_to_xs: "\<And>P. (\<forall>(v :: 'a). P v) = (\<forall>xs. P (from_bytes xs))" 363 apply (safe, simp_all) 364 apply (drule_tac x="to_bytes_p v" in spec) 365 apply (simp add: to_bytes_p_from_bytes) 366 done 367 show ?thesis 368 apply (simp add: global_data_valid_def global_data_def) 369 apply (simp add: all_to_xs order_less_imp_le[OF max_size] 370 inj_eq[OF to_bytes_p_inj] conj_comms K_def) 371 apply (safe, simp_all add: to_bytes_p_from_bytes) 372 apply (drule_tac x="to_bytes_p (from_bytes xs :: 'a)" in spec, drule mp) 373 apply simp 374 apply (simp add: inj_eq[OF to_bytes_p_inj]) 375 done 376qed 377 378lemma globals_swap_reorder_append: 379 "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd (xs @ ys); 380 global_acc_valid g_hrs g_hrs_upd; 381 globals_list_distinct D symtab (xs @ ys) \<rbrakk> 382 \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab (xs @ ys) = globals_swap g_hrs g_hrs_upd symtab (ys @ xs)" 383 apply (induct xs) 384 apply simp 385 apply (rule ext) 386 apply (clarsimp simp: globals_swap_def foldr_hrs_htd_global_swap 387 fun_eq_iff) 388 apply (drule meta_mp, simp add: globals_list_valid_def) 389 apply (clarsimp simp: globals_list_distinct_def) 390 apply (rule foldr_update_commutes) 391 apply (clarsimp simp: ball_Un globals_list_valid_def) 392 apply (rule global_swap_swap, simp_all) 393 done 394 395lemma globals_swap_reorder_append_n: 396 "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd; 397 globals_list_distinct D symtab xs \<rbrakk> \<Longrightarrow> 398 globals_swap g_hrs g_hrs_upd symtab xs = globals_swap g_hrs g_hrs_upd symtab (drop n xs @ take n xs)" 399 using globals_swap_reorder_append 400 [where xs="take n xs" and ys="drop n xs"] 401 by simp 402 403lemma heap_update_list_overwrite: 404 "\<lbrakk> length xs = length ys; length ys < addr_card \<rbrakk> 405 \<Longrightarrow> heap_update_list w xs (heap_update_list w ys hp) 406 = heap_update_list w xs hp" 407 by (rule ext, simp add: heap_update_list_value) 408 409lemma heap_list_update_eq: 410 "\<lbrakk> n = length v; n \<le> addr_card \<rbrakk> 411 \<Longrightarrow> heap_list (heap_update_list p v h) n p = v" 412 by (simp add: heap_list_update) 413 414lemma globals_swap_absorb_update: 415 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 416 \<forall>s. v (g_hrs s) = v'; length v' = m; 417 globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); 418 globals_list_distinct D symtab (GlobalData nm m ok g s # xs) \<rbrakk> 419 \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) 420 = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) 421 (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)" 422 apply (induct xs) 423 apply (simp add: globals_swap_def global_acc_valid_def) 424 apply (simp add: global_swap_def global_data_def hrs_mem_update) 425 apply (simp add: globals_list_valid_def global_data_valid_def K_def o_def) 426 apply (simp add: hrs_mem_def hrs_mem_update_def split_def 427 heap_update_def h_val_def heap_update_list_overwrite 428 heap_list_update_eq order_less_imp_le 429 del: SepCode.inv_p) 430 apply (drule meta_mp, simp add: globals_list_valid_def globals_list_distinct_def)+ 431 apply (rename_tac x xs) 432 apply (subgoal_tac "\<forall>gs. 433 globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs 434 = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)") 435 apply (subgoal_tac "\<forall>gs. s v' (global_swap g_hrs g_hrs_upd symtab x gs) = global_swap g_hrs g_hrs_upd symtab x (s v' gs)") 436 apply (simp add: global_acc_valid_def) 437 apply (clarsimp simp: globals_list_valid_def global_data_swappable_def 438 global_data_def global_swap_def K_def 439 global_data_valid_def order_less_imp_le 440 simp del: SepCode.inv_p split: global_data.split_asm prod.split bool.split) 441 apply (clarsimp simp: globals_swap_def globals_list_distinct_def 442 global_data_def globals_list_valid_def) 443 apply (rule global_swap_swap, simp+) 444 done 445 446lemma append_2nd_simp_backward: 447 "xs @ y # ys = (xs @ [y]) @ ys" 448 by simp 449 450lemma globals_swap_access_mem_raw: 451 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 452 globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs; 453 GlobalData nm m ok g s \<in> set xs; size_of TYPE('a) = m \<rbrakk> 454 \<Longrightarrow> h_val (hrs_mem (g_hrs gs)) (Ptr (symtab nm) :: ('a :: c_type) ptr) 455 = from_bytes (g (globals_swap g_hrs g_hrs_upd symtab xs gs))" 456 apply (clarsimp simp: in_set_conv_decomp) 457 apply (subst append_2nd_simp_backward) 458 apply (subst globals_swap_reorder_append, simp+) 459 apply (simp add: globals_swap_def del: foldr_append split del: if_split) 460 apply (subgoal_tac "global_data_valid g_hrs g_hrs_upd 461 (GlobalData nm (size_of TYPE('a)) ok g s)") 462 apply (subst append_assoc[symmetric], subst foldr_append) 463 apply (subst foldr_does_nothing_to_xf[where xf=g]) 464 apply (subgoal_tac "global_data_swappable (GlobalData nm (size_of TYPE('a)) ok g s) x") 465 apply (clarsimp simp: global_data_swappable_def global_data_def 466 global_swap_def global_data_valid_def 467 split: global_data.split_asm prod.split bool.split) 468 apply (simp add: globals_list_valid_def distinct_prop_append) 469 apply (auto simp: global_data_swappable_sym)[1] 470 apply (simp add: global_data_valid_def) 471 apply (simp add: global_data_def global_swap_def h_val_def K_def 472 ) 473 apply (simp_all add: globals_list_valid_def) 474 done 475 476lemma globals_swap_access_mem: 477 "\<lbrakk> global_data nm g u \<in> set xs; 478 global_acc_valid g_hrs g_hrs_upd; 479 globals_list_valid symtab g_hrs g_hrs_upd xs; 480 globals_list_distinct D symtab xs \<rbrakk> 481 \<Longrightarrow> g (globals_swap g_hrs g_hrs_upd symtab xs gs) = h_val (hrs_mem (g_hrs gs)) (Ptr (symtab nm))" 482 by (simp add: global_data_def globals_swap_access_mem_raw) 483 484lemma globals_swap_access_mem2: 485 "\<lbrakk> global_data nm g u \<in> set xs; 486 global_acc_valid g_hrs g_hrs_upd; 487 globals_list_valid symtab g_hrs g_hrs_upd xs; 488 globals_list_distinct D symtab xs \<rbrakk> 489 \<Longrightarrow> g gs = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (Ptr (symtab nm))" 490 using globals_swap_twice_helper globals_swap_access_mem 491 by metis 492 493lemma globals_swap_update_mem_raw: 494 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 495 \<forall>hmem. (v hmem) = v'; length v' = m; 496 globals_list_valid symtab g_hrs g_hrs_upd xs; 497 globals_list_distinct D symtab xs; 498 GlobalData nm m ok g st \<in> set xs \<rbrakk> 499 \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update 500 (\<lambda>hmem. heap_update_list (symtab nm) (v hmem) hmem)) gs) 501 = st v' (globals_swap g_hrs g_hrs_upd symtab xs gs)" 502 apply (clarsimp simp: in_set_conv_decomp) 503 apply (subst globals_swap_reorder_append, simp+)+ 504 apply (rule globals_swap_absorb_update[symmetric, where D=D], simp_all) 505 apply (simp add: globals_list_valid_def distinct_prop_append) 506 apply (insert global_data_swappable_sym) 507 apply blast 508 apply (simp add: globals_list_distinct_def ball_Un distinct_prop_append) 509 apply blast 510 done 511 512lemma to_bytes_p_from_bytes_eq: 513 "\<lbrakk> from_bytes ys = (v :: 'a :: packed_type); length ys = size_of TYPE('a) \<rbrakk> 514 \<Longrightarrow> to_bytes_p v = ys" 515 by (clarsimp simp: to_bytes_p_from_bytes) 516 517lemma globals_swap_update_mem: 518 "\<lbrakk> global_data nm g u \<in> set xs; 519 global_acc_valid g_hrs g_hrs_upd; 520 globals_list_valid symtab g_hrs g_hrs_upd xs; 521 globals_list_distinct D symtab xs \<rbrakk> 522 \<Longrightarrow> u (\<lambda>_. v) (globals_swap g_hrs g_hrs_upd symtab xs gs) 523 = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update 524 (\<lambda>hrs. heap_update (Ptr (symtab nm)) v hrs)) gs)" 525 unfolding global_data_def 526 apply (simp add: heap_update_def) 527 apply (subst globals_swap_update_mem_raw[where v'="to_bytes_p v", rotated -1], 528 assumption, simp_all add: K_def o_def) 529 apply clarsimp 530 apply (rule to_bytes_p_from_bytes_eq[symmetric], simp+) 531 done 532 533lemma globals_swap_update_mem2: 534 assumes prems: "global_data nm g u \<in> set xs" 535 "global_acc_valid g_hrs g_hrs_upd" 536 "globals_list_valid symtab g_hrs g_hrs_upd xs" 537 "globals_list_distinct D symtab xs" 538 shows "globals_swap g_hrs g_hrs_upd symtab xs (u (\<lambda>_. v) gs) 539 = g_hrs_upd (hrs_mem_update (\<lambda>hrs. heap_update (Ptr (symtab nm)) v hrs)) 540 (globals_swap g_hrs g_hrs_upd symtab xs gs)" 541 using prems globals_swap_twice_helper globals_swap_update_mem 542 by metis 543 544lemma globals_swap_hrs_htd_update: 545 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 546 globals_list_valid symtab g_hrs g_hrs_upd xs \<rbrakk> 547 \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (globals_swap g_hrs g_hrs_upd symtab xs gs) 548 = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_htd_update ufn) gs)" 549 apply (clarsimp simp: globals_swap_def hrs_htd_update 550 global_acc_valid_def) 551 apply (rule foldr_update_commutes) 552 apply (clarsimp simp: globals_list_valid_def, drule(1) bspec) 553 apply (simp add: global_swap_def o_def global_data_valid_def 554 hrs_htd_update 555 split: global_data.split_asm prod.split bool.split) 556 apply (simp add: hrs_htd_update_def hrs_mem_update_def split_def) 557 done 558 559definition 560 const_global_data :: "string \<Rightarrow> ('a :: c_type) \<Rightarrow> 'g global_data" 561where 562 "const_global_data name v = ConstGlobalData name (size_of TYPE('a)) 563 (\<lambda>addr. c_guard (Ptr addr :: 'a ptr)) 564 (to_bytes_p v) (\<lambda>xs. from_bytes xs = v)" 565 566definition 567 addressed_global_data :: "string \<Rightarrow> ('a :: c_type) itself \<Rightarrow> 'g global_data" 568where 569 "addressed_global_data name tp = 570 AddressedGlobalData name (size_of tp) (\<lambda>addr. c_guard (Ptr addr :: 'a ptr))" 571 572lemma is_global_data_simps[simp]: 573 "is_global_data (global_data nm g s)" 574 "\<not> is_global_data (const_global_data nm v)" 575 "\<not> is_global_data (addressed_global_data nm tp)" 576 by (simp_all add: global_data_def const_global_data_def 577 is_global_data_def addressed_global_data_def) 578 579lemma is_const_global_data_simps[simp]: 580 "is_const_global_data (const_global_data nm v)" 581 "\<not> is_const_global_data (global_data nm g s)" 582 "\<not> is_const_global_data (addressed_global_data nm tp)" 583 by (simp_all add: global_data_def const_global_data_def 584 is_const_global_data_def addressed_global_data_def) 585 586lemma distinct_prop_swappable_optimisation: 587 "distinct_prop global_data_swappable (filter is_global_data gs) 588 \<Longrightarrow> distinct_prop (\<lambda>x y. global_data_swappable x y) gs" 589 apply (simp add: distinct_prop_filter is_global_data_def 590 global_data_swappable_def) 591 apply (erule distinct_prop_weaken) 592 apply (simp split: global_data.splits) 593 done 594 595lemma globals_list_valid_optimisation: 596 "distinct_prop global_data_swappable (filter is_global_data gs) 597 \<Longrightarrow> \<forall>g \<in> set gs. global_data_valid g_hrs g_hrs_upd g 598 \<Longrightarrow> \<forall>g \<in> set gs. global_data_ok symtab g 599 \<Longrightarrow> globals_list_valid symtab g_hrs g_hrs_upd gs" 600 using globals_list_valid_def distinct_prop_swappable_optimisation 601 by blast 602 603definition 604 const_globals_in_memory :: "(string \<Rightarrow> addr) \<Rightarrow> 'g global_data list 605 \<Rightarrow> heap_mem \<Rightarrow> bool" 606where 607 "const_globals_in_memory symtab xs hmem = 608 (\<forall>gd \<in> set xs. case gd of 609 ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) 610 | _ \<Rightarrow> True)" 611 612lemma const_globals_in_memory_h_val_eq: 613 "const_globals_in_memory symtab (const_global_data nm v # xs) hmem 614 = (h_val hmem (Ptr (symtab nm)) = v \<and> const_globals_in_memory symtab xs hmem)" 615 by (simp add: const_globals_in_memory_def const_global_data_def h_val_def) 616 617lemma const_globals_in_memory_other_eqs: 618 "const_globals_in_memory symtab (global_data nm g s # xs) hmem 619 = const_globals_in_memory symtab xs hmem" 620 "const_globals_in_memory symtab (addressed_global_data nm tp # xs) hmem 621 = const_globals_in_memory symtab xs hmem" 622 "const_globals_in_memory symtab [] hmem" 623 by (auto simp add: const_globals_in_memory_def 624 global_data_def addressed_global_data_def) 625 626lemmas const_globals_in_memory_eqs 627 = const_globals_in_memory_h_val_eq const_globals_in_memory_other_eqs 628 629lemma const_globals_in_memory_h_val: 630 "\<lbrakk> const_global_data nm v \<in> set xs; 631 const_globals_in_memory symtab xs hmem \<rbrakk> 632 \<Longrightarrow> h_val hmem (Ptr (symtab nm)) = v" 633 apply (simp add: const_globals_in_memory_def const_global_data_def) 634 apply (drule (1) bspec) 635 apply (clarsimp simp: h_val_def) 636 done 637 638lemma const_globals_in_memory_heap_update_list: 639 "\<lbrakk> const_globals_in_memory symtab xs hmem; 640 globals_list_distinct D symtab (filter is_const_global_data xs); 641 {p ..+ length ys} \<subseteq> D \<rbrakk> 642 \<Longrightarrow> const_globals_in_memory symtab xs (heap_update_list p ys hmem)" 643 apply (clarsimp simp: const_globals_in_memory_def globals_list_distinct_def 644 split: global_data.split) 645 apply (drule(1) bspec) 646 apply (drule spec, drule mp, erule conjI, simp add: is_const_global_data_def) 647 apply (simp add: global_data_region_def) 648 apply (subst heap_list_update_disjoint_same) 649 apply blast 650 apply simp 651 done 652 653definition 654 htd_safe :: "addr set \<Rightarrow> heap_typ_desc \<Rightarrow> bool" 655where 656 "htd_safe D htd = (dom_s htd \<subseteq> D \<times> UNIV)" 657 658lemma const_globals_in_memory_heap_update: 659 "\<lbrakk> const_globals_in_memory symtab gs hmem; 660 globals_list_distinct D symtab gs; 661 ptr_safe (p :: ('a :: wf_type) ptr) htd; htd_safe D htd \<rbrakk> 662 \<Longrightarrow> const_globals_in_memory symtab gs (heap_update p val hmem)" 663 apply (simp add: split_def heap_update_def) 664 apply (erule const_globals_in_memory_heap_update_list, 665 erule globals_list_distinct_filter) 666 apply (clarsimp simp: ptr_safe_def htd_safe_def s_footprint_intvl[symmetric]) 667 apply blast 668 done 669 670lemma distinct_prop_memD: 671 "\<lbrakk> x \<in> set zs; y \<in> set zs; distinct_prop P zs \<rbrakk> 672 \<Longrightarrow> x = y \<or> P x y \<or> P y x" 673 by (induct zs, auto) 674 675lemma const_globals_in_memory_heap_update_global: 676 "\<lbrakk> const_globals_in_memory symtab gs hmem; 677 global_data nm (getter :: 'g \<Rightarrow> 'a) setter \<in> set gs; 678 globals_list_distinct D symtab gs \<rbrakk> 679 \<Longrightarrow> const_globals_in_memory symtab gs 680 (heap_update (Ptr (symtab nm)) (v :: 'a :: packed_type) hmem)" 681 apply (simp add: heap_update_def split_def) 682 apply (erule const_globals_in_memory_heap_update_list[OF _ _ order_refl]) 683 apply (clarsimp simp: globals_list_distinct_def distinct_prop_map 684 distinct_prop_filter) 685 apply (simp add: distinct_prop_weaken) 686 apply clarsimp 687 apply (drule(2) distinct_prop_memD) 688 apply (auto simp: global_data_region_def global_data_def 689 is_const_global_data_def) 690 done 691 692lemma const_globals_in_memory_after_swap: 693 "global_acc_valid t_hrs_' t_hrs_'_update 694 \<Longrightarrow> globals_list_distinct D symbol_table gxs 695 \<Longrightarrow> const_globals_in_memory symbol_table gxs 696 (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs))) 697 = const_globals_in_memory symbol_table gxs (hrs_mem (t_hrs_' gs))" 698 apply (simp add: const_globals_in_memory_def) 699 apply (rule ball_cong, simp_all) 700 apply (clarsimp split: global_data.split) 701 apply (subst disjoint_heap_list_globals_swap_filter[OF _ _ order_refl], 702 assumption+, simp_all) 703 apply (clarsimp simp: globals_list_distinct_def distinct_prop_map 704 distinct_prop_filter distinct_prop_weaken) 705 apply (drule(2) distinct_prop_memD) 706 apply (clarsimp simp: is_global_data_def ball_Un distinct_prop_append 707 global_data_region_def Int_commute 708 split: global_data.split_asm) 709 done 710 711ML \<open> 712structure DefineGlobalsList = struct 713 714fun dest_conjs t = (t RS @{thm conjunct1}) 715 :: dest_conjs (t RS @{thm conjunct2}) 716 handle THM _ => [t] 717 718fun define_globals_list (mungedb:CalculateState.mungedb) globloc globty thy = let 719 open CalculateState NameGeneration 720 721 val sT = @{typ string} 722 val gdT = Type (@{type_name global_data}, [globty]) 723 724 val ctxt = Named_Target.begin (globloc, Position.none) thy 725 726 fun glob (_, _, _, Local _) = error "define_globals_list: Local" 727 | glob (nm, typ, _, UntouchedGlobal) = let 728 val cname = NameGeneration.untouched_global_name nm 729 val init = Syntax.read_term ctxt (MString.dest cname) 730 in Const (@{const_name "const_global_data"}, sT --> typ --> gdT) 731 $ HOLogic.mk_string (MString.dest nm) $ init end 732 | glob (nm, typ, _, NSGlobal) = let 733 (* FIXME: _' hackery (or more generally, hackery) *) 734 val acc = (Sign.intern_const thy (global_rcd_name ^ "." ^ 735 MString.dest nm ^ "_'"), 736 globty --> typ) 737 val upd = (Sign.intern_const thy 738 (global_rcd_name ^ "." ^ MString.dest nm ^ "_'" ^ 739 Record.updateN), 740 (typ --> typ) --> globty --> globty) 741 in Const (@{const_name "global_data"}, sT 742 --> snd acc --> snd upd --> gdT) 743 $ HOLogic.mk_string (MString.dest nm) $ Const acc $ Const upd end 744 | glob (nm, typ, _, AddressedGlobal) = 745 Const (@{const_name "addressed_global_data"}, 746 sT --> Term.itselfT typ --> gdT) 747 $ HOLogic.mk_string (MString.dest nm) $ Logic.mk_type typ 748 749 val naming = Binding.name o NameGeneration.global_data_name 750 val globs = CNameTab.dest mungedb |> map snd 751 |> filter (fn v => case #4 v of Local _ => false | _ => true) 752 |> map (fn g => (g |> #1 |> MString.dest |> naming, glob g)) 753 754 val (xs, ctxt) = fold_map (fn (nm, tm) => Local_Theory.define 755 ((nm, NoSyn), ((Thm.def_binding nm, []), tm))) globs ctxt 756 757 val gdTs = HOLogic.mk_list gdT (map fst xs) 758 759 val ((gdl, (_, gdl_def)), ctxt) = Local_Theory.define 760 ((@{binding global_data_list}, NoSyn), 761 ((@{binding global_data_list_def}, []), gdTs)) ctxt 762 763 val (_, ctxt) = Local_Theory.note ((@{binding "global_data_defs"}, []), 764 map (snd #> snd) xs) ctxt 765 766 val lT = HOLogic.listT gdT 767 val setT = HOLogic.mk_setT gdT 768 val setC = Const (@{const_name set}, lT --> setT) 769 val thm = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop 770 (Const (@{const_name less_eq}, setT --> setT --> HOLogic.boolT) 771 $ (setC $ gdTs) $ (setC $ gdl))) 772 (K (simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms order_refl} 773 addsimps [gdl_def]) 1)) 774 775 val mems = simplify (put_simpset HOL_basic_ss ctxt addsimps 776 @{thms set_simps insert_subset empty_subsetI simp_thms}) thm 777 |> dest_conjs 778 779 val (_, ctxt) = Local_Theory.note ((@{binding "global_data_mems"}, []), 780 mems) ctxt 781 782 in Local_Theory.exit_global ctxt end 783 784fun define_globals_list_i s globty thy = let 785 val {base = localename,...} = OS.Path.splitBaseExt (OS.Path.file s) 786 val globloc = suffix HPInter.globalsN localename 787 in define_globals_list (CalculateState.get_mungedb thy s |> the) 788 globloc globty thy 789 end 790 791end 792 793\<close> 794 795lemma globals_list_distinct_filter_member: 796 "x \<in> set xs \<Longrightarrow> globals_list_distinct D symtab xs 797 \<Longrightarrow> \<not> P x 798 \<Longrightarrow> globals_list_distinct (global_data_region symtab x) symtab 799 (filter P xs)" 800 apply (clarsimp simp: globals_list_distinct_def) 801 apply (rule conjI) 802 apply (clarsimp simp: in_set_conv_decomp[where x="x"] 803 distinct_prop_append) 804 apply auto[1] 805 apply (simp add: distinct_prop_map distinct_prop_filter) 806 apply (erule distinct_prop_weaken, simp) 807 done 808 809lemma s_footprint_intvl_subset: 810 "s_footprint (p :: 'a ptr) \<subseteq> {ptr_val p ..+ size_of TYPE ('a :: c_type)} \<times> UNIV" 811 by (auto simp: s_footprint_def s_footprint_untyped_def 812 intvl_def size_of_def) 813 814lemma h_val_globals_swap_in_const_global: 815 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 816 globals_list_distinct D symtab xs; 817 const_global_data s (v :: 'a :: c_type) \<in> set xs; 818 unat offs + size_of TYPE('b) \<le> size_of TYPE('a) \<rbrakk> 819 \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) 820 (Ptr (symtab s + offs) :: ('b :: c_type) ptr) 821 = h_val (hrs_mem (g_hrs gs)) (Ptr (symtab s + offs))" 822 apply (erule disjoint_h_val_globals_swap_filter, 823 erule(1) globals_list_distinct_filter_member) 824 apply simp 825 apply (rule order_trans, rule s_footprint_intvl_subset) 826 apply (simp add: global_data_region_def const_global_data_def 827 Times_subset_cancel2) 828 apply (erule intvl_sub_offset) 829 done 830 831lemmas h_val_globals_swap_in_const_global_both 832 = h_val_globals_swap_in_const_global 833 h_val_globals_swap_in_const_global[where offs=0, simplified] 834 835lemma const_globals_in_memory_to_h_val_with_swap: 836 "\<lbrakk> global_acc_valid g_hrs g_hrs_upd; 837 globals_list_distinct D symtab xs; 838 const_global_data nm v \<in> set xs; 839 const_globals_in_memory symtab xs (hrs_mem (g_hrs gs)) \<rbrakk> 840 \<Longrightarrow> v = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) 841 (Ptr (symtab nm))" 842 apply (subst disjoint_h_val_globals_swap_filter, assumption, 843 erule(1) globals_list_distinct_filter_member) 844 apply simp 845 apply (simp add: global_data_region_def const_global_data_def) 846 apply (rule order_trans, rule s_footprint_intvl_subset) 847 apply simp 848 apply (erule(1) const_globals_in_memory_h_val[symmetric]) 849 done 850 851text \<open>This alternative ptr_safe definition will apply to all 852 global pointers given globals_list_distinct etc. It supports 853 the same nonoverlapping properties with h_t_valid as h_t_valid 854 itself.\<close> 855definition 856 ptr_inverse_safe :: "('a :: mem_type) ptr \<Rightarrow> heap_typ_desc \<Rightarrow> bool" 857where 858 "ptr_inverse_safe p htd = (c_guard p 859 \<and> (fst ` s_footprint p \<inter> fst ` dom_s htd = {}))" 860 861lemma global_data_implies_ptr_inverse_safe: 862 "\<lbrakk> global_data nm (accr :: 'a \<Rightarrow> ('b :: packed_type)) updr \<in> set glist; 863 globals_list_distinct D symtab glist; 864 globals_list_valid symtab t_hrs t_hrs_upd glist; 865 htd_safe D htd 866 \<rbrakk> 867 \<Longrightarrow> ptr_inverse_safe (Ptr (symtab nm) :: 'b ptr) htd" 868 apply (clarsimp simp add: ptr_inverse_safe_def globals_list_valid_def 869 htd_safe_def globals_list_distinct_def) 870 apply (drule(1) bspec)+ 871 apply (simp add: global_data_region_def global_data_ok_def global_data_def) 872 apply (auto dest!: s_footprint_intvl_subset[THEN subsetD]) 873 done 874 875ML \<open> 876fun add_globals_swap_rewrites member_thms ctxt = let 877 fun cpat pat = Thm.cterm_of ctxt (Proof_Context.read_term_pattern ctxt pat) 878 val gav = Proof_Context.get_thm ctxt "global_acc_valid" 879 val glv = Proof_Context.get_thm ctxt "globals_list_valid" 880 val gld = Proof_Context.get_thm ctxt "globals_list_distinct" 881 val acc = [Thm.trivial (cpat "PROP ?P"), gav, glv, gld] 882 MRS @{thm globals_swap_access_mem2} 883 val upd = [Thm.trivial (cpat "PROP ?P"), gav, glv, gld] 884 MRS @{thm globals_swap_update_mem2} 885 val cg_with_swap = [gav, gld] 886 MRS @{thm const_globals_in_memory_to_h_val_with_swap} 887 val pinv_safe = [Thm.trivial (cpat "PROP ?P"), gld, glv] 888 MRS @{thm global_data_implies_ptr_inverse_safe} 889 val empty_ctxt = put_simpset HOL_basic_ss ctxt 890 fun unfold_mem thm = let 891 val (x, _) = HOLogic.dest_mem (HOLogic.dest_Trueprop (Thm.concl_of thm)) 892 val (s, _) = dest_Const (head_of x) 893 in if s = @{const_name global_data} orelse s = @{const_name const_global_data} 894 orelse s = @{const_name addressed_global_data} 895 then thm 896 else simplify (empty_ctxt addsimps [Proof_Context.get_thm ctxt (s ^ "_def")]) thm 897 end 898 899 val member_thms = map unfold_mem member_thms 900 901 val globals_swap_rewrites = member_thms RL [acc, upd] 902 val const_globals_rewrites = member_thms RL @{thms const_globals_in_memory_h_val[symmetric]} 903 val const_globals_swap_rewrites = member_thms RL [cg_with_swap] 904 val pinv_safe_intros = member_thms RL [pinv_safe] 905 in ctxt 906 |> Local_Theory.note ((@{binding "globals_swap_rewrites"}, []), 907 globals_swap_rewrites) 908 |> snd 909 |> Local_Theory.note ((@{binding "const_globals_rewrites"}, []), 910 const_globals_rewrites) 911 |> snd 912 |> Local_Theory.note ((@{binding "const_globals_rewrites_with_swap"}, []), 913 const_globals_swap_rewrites) 914 |> snd 915 |> Local_Theory.note ((@{binding "pointer_inverse_safe_global_rules"}, []), 916 pinv_safe_intros) 917 |> snd 918 end 919\<close> 920 921end 922