1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11theory CProof 12imports 13 "umm_heap/SepFrame" 14 "Simpl-VCG.Vcg" 15 "umm_heap/StructSupport" 16 "umm_heap/ArrayAssertion" 17begin 18 19(* name generation is the only thing this theory wants, but that 20 depends on Absyn, which depends on a bunch of other stuff. *) 21ML_file "General.ML" 22ML_file "openUnsynch.ML" 23ML_file "SourcePos.ML" 24ML_file "SourceFile.ML" 25ML_file "Region.ML" 26ML_file "Binaryset.ML" 27ML_file "Feedback.ML" 28ML_file "basics.ML" 29ML_file "MString.ML" 30 31ML_file "TargetNumbers-sig.ML" 32ML_file "./umm_heap/$L4V_ARCH/TargetNumbers.ML" 33 34ML_file "RegionExtras.ML" 35ML_file "Absyn-CType.ML" 36ML_file "Absyn-Expr.ML" 37ML_file "Absyn-StmtDecl.ML" 38ML_file "Absyn.ML" 39ML_file "Absyn-Serial.ML" 40ML_file "name_generation.ML" 41 42 43(* set up hoare package to rewrite state updates more *) 44setup {* 45 Hoare.add_foldcongsimps [@{thm "update_update"}, @{thm "o_def"}] 46*} 47 48 49(* Syntax for apply antiquotation parsing explicitly *) 50syntax 51 "_quote" :: "'b => ('a => 'b)" ("([.[_].])" [0] 1000) 52 53(* Override assertion translation so we can apply the parse translations below 54 and add \<star> syntax. *) 55syntax 56 "_heap" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" 57 "_heap_state" :: "'a" ("\<zeta>") (* FIXME: horrible syntax *) 58 "_heap_stateOld" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<^bsup>_\<^esup>\<zeta>" [100] 100) (* FIXME: horrible syntax *) 59 60 "_derefCur" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<star>_" [100] 100) 61 "_derefOld" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<^bsup>_\<^esup>\<star>_" [100,100] 100) 62 63translations 64 "{|b|}" => "CONST Collect (_quote (_heap b))" 65 66definition sep_app :: "(heap_state \<Rightarrow> bool) \<Rightarrow> heap_state \<Rightarrow> bool" where 67 "sep_app P s \<equiv> P s" 68 69definition hrs_id :: "heap_raw_state \<Rightarrow> heap_raw_state" where 70 "hrs_id \<equiv> id" 71 72declare hrs_id_def [simp add] 73 74parse_translation {* 75let 76 fun ac x = Syntax.const "_antiquoteCur" $ Syntax.const x 77 fun aco x y = Syntax.const y $ (Syntax.const "globals" $ x) 78 fun hd a = a NameGeneration.global_heap_var 79 fun d a = Syntax.const "hrs_htd" $ hd a 80 fun repl (Abs (s,T,t)) = Abs (s,T,repl t) 81 | repl (Const ("_h_t_valid",_)$x) = Syntax.const "h_t_valid" $ d ac $ Syntax.const "c_guard" $ x 82 | repl (Const ("_derefCur",_)$x) = Syntax.const "the" $ 83 (Syntax.const "lift_t" $ hd ac $ x) 84 | repl (Const ("_derefOld",_)$x$y) = Syntax.const "the" $ 85 (Syntax.const "lift_t" $ hd (aco x) $ y) 86 | repl (Const ("_heap_state",_)) = Syntax.const "hrs_id" $ hd ac 87 | repl (Const ("_heap_stateOld",_)$x) = Syntax.const "hrs_id" $ hd (aco x) 88 | repl (x$y) = repl x $ repl y 89 | repl x = x 90 fun heap_assert_tr [b] = repl b 91 | heap_assert_tr ts = raise TERM ("heap_assert_tr", ts); 92in [("_heap",K heap_assert_tr)] end; 93*} 94 95 96(* Separation logic assertion parse translation *) 97parse_translation {* 98let 99 fun ac x = Syntax.const "_antiquoteCur" $ Syntax.const x 100 fun aco x y = Syntax.const y $ (Syntax.const "globals" $ x) 101 fun hd a = Syntax.const "lift_state" $ (a NameGeneration.global_heap_var) 102 fun st2 (Abs (s,T,t)) n = Abs (s,T,st2 t (n+1)) 103 | st2 (Bound k) n = Bound (if k < n then k else k + 1) 104 | st2 (x$y) n = st2 x n $ st2 y n 105 | st2 x _ = x 106 fun st1 (Abs (s,T,t)) n = Abs (s,T,st1 t (n+1)) 107 | st1 (Bound k) n = Bound (if k < n then k else k + 1) 108 | st1 (Const ("sep_empty",_)) n = Syntax.const "sep_empty" $ Bound n 109 | st1 (Const ("sep_map",_)$x$y) n = Syntax.const "sep_map" $ 110 (st2 x n) $ (st2 y n) $ Bound n 111 | st1 (Const ("sep_map'",_)$x$y) n = Syntax.const "sep_map'" $ 112 (st2 x n) $ (st2 y n) $ Bound n 113 | st1 (Const ("sep_conj",_)$x$y) n = Syntax.const "sep_conj" $ 114 (nst2 x n) $ (nst2 y n) $ Bound n 115 | st1 (Const ("sep_impl",_)$x$y) n = Syntax.const "sep_impl" $ 116 (nst2 x n) $ (nst2 y n) $ Bound n 117 | st1 (x$y) n = st1 x n $ st1 y n 118 | st1 x _ = x 119 and new_heap t = Abs ("s",dummyT,st1 t 0) 120 and nst2 x n = new_heap (st2 x n); 121 fun sep_tr [t] = Syntax.const "sep_app" $ (*new_heap *) t $ hd ac 122 | sep_tr ts = raise TERM ("sep_tr", ts); 123in [("_sep_assert",K sep_tr)] end; 124*} 125 126 127definition c_null_guard :: "'a::c_type ptr_guard" where 128 "c_null_guard \<equiv> \<lambda>p. 0 \<notin> {ptr_val p..+size_of TYPE('a)}" 129 130lemma c_null_guard: 131 "c_null_guard (p::'a::mem_type ptr) \<Longrightarrow> p \<noteq> NULL" 132apply(clarsimp simp: c_null_guard_def) 133apply(erule notE) 134apply(rule intvl_self) 135apply simp 136done 137 138overloading c_guard_def \<equiv> c_guard begin 139definition 140c_guard_def: "c_guard_def \<equiv> \<lambda>p. ptr_aligned p \<and> c_null_guard p" 141end 142 143definition 144c_fnptr_guard_def: "c_fnptr_guard (fnptr::unit ptr) \<equiv> ptr_val fnptr \<noteq> 0" 145 146lemma c_guardD: 147 "c_guard (p::'a::mem_type ptr) \<Longrightarrow> ptr_aligned p \<and> p \<noteq> NULL" 148apply(clarsimp simp: c_guard_def) 149apply(drule c_null_guard) 150apply simp 151done 152 153lemma c_guard_ptr_aligned: 154 "c_guard p \<Longrightarrow> ptr_aligned p" 155 by (simp add: c_guard_def) 156 157lemma c_guard_NULL: 158 "c_guard (p::'a::mem_type ptr) \<Longrightarrow> p \<noteq> NULL" 159 by (simp add: c_guardD) 160 161lemma c_guard_NULL_simp [simp]: 162 "\<not> c_guard (NULL::'a::mem_type ptr)" 163 by (force dest: c_guard_NULL) 164 165lemma c_guard_mono: 166 "guard_mono (c_guard::'a::mem_type ptr_guard) (c_guard::'b::mem_type ptr_guard)" 167apply(clarsimp simp: guard_mono_def c_guard_def) 168apply(subgoal_tac "guard_mono (ptr_aligned::'a::mem_type ptr_guard) (ptr_aligned::'b::mem_type ptr_guard)") 169 prefer 2 170 apply(rule ptr_aligned_mono) 171apply(clarsimp simp: guard_mono_def) 172apply(clarsimp simp: ptr_aligned_def) 173apply(clarsimp simp: c_null_guard_def typ_uinfo_t_def) 174apply(frule field_lookup_export_uinfo_Some_rev) 175apply clarsimp 176apply(drule_tac p=p in field_tag_sub) 177apply(clarsimp simp: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def) 178apply(subgoal_tac "size_td k = size_of TYPE('b)") 179 apply simp 180 apply fast 181apply(clarsimp simp: size_of_def) 182apply(subst typ_uinfo_size [symmetric]) 183apply(drule_tac s="export_uinfo k" in sym) 184apply(subst typ_uinfo_t_def) 185apply simp 186done 187 188lemma c_guard_NULL_fl: 189 "\<lbrakk> c_guard (p::'a::mem_type ptr); 190 field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n); 191 export_uinfo t = typ_uinfo_t TYPE('b::mem_type) \<rbrakk> \<Longrightarrow> 0 < &(p\<rightarrow>f)" 192apply(insert c_guard_mono) 193apply(clarsimp simp: guard_mono_def) 194apply((erule allE)+) 195apply(erule impE) 196 apply rule 197 apply assumption 198 apply(drule field_lookup_export_uinfo_Some) 199 apply(simp add: typ_uinfo_t_def) 200apply(drule field_lookup_export_uinfo_Some) 201apply(simp add: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def) 202apply(unfold c_guard_def) 203apply clarsimp 204apply(drule c_null_guard)+ 205apply clarsimp 206done 207 208lemma c_guard_ptr_aligned_fl: 209 "\<lbrakk> c_guard (p::'a::mem_type ptr); 210 field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n); 211 export_uinfo t = typ_uinfo_t TYPE('b::mem_type) \<rbrakk> \<Longrightarrow> 212 ptr_aligned ((Ptr &(p\<rightarrow>f))::'b ptr)" 213apply(insert c_guard_mono) 214apply(clarsimp simp: guard_mono_def) 215apply((erule allE)+) 216apply(erule impE) 217 apply rule 218 apply assumption 219 apply(drule field_lookup_export_uinfo_Some) 220 apply(simp add: typ_uinfo_t_def) 221apply(drule field_lookup_export_uinfo_Some) 222apply(unfold c_guard_def) 223apply(simp add: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def) 224done 225 226(* StrictC guard separation syntax translations *) 227 228(* FIXME: make these abbreviations *) 229syntax 230 "_sep_map" :: "'a::c_type ptr \<Rightarrow> 'a \<Rightarrow> heap_assert" ("_ \<mapsto> _" [56,51] 56) 231 "_sep_map_any" :: "'a::c_type ptr \<Rightarrow> heap_assert" ("_ \<mapsto> -" [56] 56) 232 "_sep_map'" :: "'a::c_type ptr \<Rightarrow> 'a \<Rightarrow> heap_assert" ("_ \<hookrightarrow> _" [56,51] 56) 233 "_sep_map'_any" :: "'a::c_type ptr \<Rightarrow> heap_assert" ("_ \<hookrightarrow> -" [56] 56) 234 "_tagd" :: "'a::c_type ptr \<Rightarrow> heap_assert" ("\<turnstile>\<^sub>s _" [99] 100) 235 236translations 237 "p \<mapsto> v" == "p \<mapsto>\<^sup>i\<^sub>(CONST c_guard) v" 238 "p \<mapsto> -" == "p \<mapsto>\<^sup>i\<^sub>(CONST c_guard) -" 239 "p \<hookrightarrow> v" == "p \<hookrightarrow>\<^sup>i\<^sub>(CONST c_guard) v" 240 "p \<hookrightarrow> -" == "p \<hookrightarrow>\<^sup>i\<^sub>(CONST c_guard) -" 241 "\<turnstile>\<^sub>s p" == "CONST c_guard \<turnstile>\<^sub>s\<^sup>i p" 242 243term "x \<mapsto> y" 244term "(x \<mapsto> y \<and>\<^sup>* y \<mapsto> z) s" 245term "(x \<mapsto> y \<and>\<^sup>* y \<mapsto> z) \<and>\<^sup>* x \<mapsto> y" 246term "\<turnstile>\<^sub>s p" 247 248lemma sep_map_NULL [simp]: 249 "NULL \<mapsto> (v::'a::mem_type) = sep_false" 250 by (force simp: sep_map_def sep_map_inv_def c_guard_def 251 dest: lift_typ_heap_g sep_conjD c_null_guard) 252 253lemma sep_map'_NULL_simp [simp]: 254 "NULL \<hookrightarrow> (v::'a::mem_type) = sep_false" 255apply(simp add: sep_map'_def sep_map'_inv_def sep_conj_ac) 256apply(subst sep_conj_com, subst sep_map_inv_def [symmetric]) 257apply simp 258done 259 260lemma sep_map'_ptr_aligned: 261 "(p \<hookrightarrow> v) s \<Longrightarrow> ptr_aligned p" 262apply(rule c_guard_ptr_aligned) 263apply(erule sep_map'_g) 264done 265 266lemma sep_map'_NULL: 267 "(p \<hookrightarrow> (v::'a::mem_type)) s \<Longrightarrow> p \<noteq> NULL" 268apply(rule c_guard_NULL) 269apply(erule sep_map'_g) 270done 271 272lemma tagd_sep_false [simp]: 273 "\<turnstile>\<^sub>s (NULL::'a::mem_type ptr) = sep_false" 274 by (auto simp: tagd_inv_def tagd_def dest!: sep_conjD s_valid_g) 275 276(* Print translations for pointer dereferencing in program statements and 277 expressions. 278*) 279syntax (output) 280 "_Deref" :: "'b \<Rightarrow> 'b" ("*_" [1000] 1000) 281 "_AssignH" :: "'b => 'b => ('a,'p,'f) com" ("(2*_ :==/ _)" [30, 30] 23) 282 283print_translation {* 284let 285 fun deref (Const ("_antiquoteCur",_)$Const (h,_)) p = 286 if h=NameGeneration.global_heap then Syntax.const "_Deref" $ p else 287 raise Match 288 | deref h p = raise Match 289 fun lift_tr [h,p] = deref h p 290 | lift_tr ts = raise Match 291 fun deref_update (Const ("heap_update",_)$l$r$(Const ("_antiquoteCur",_)$ 292 Const (h,_))) = 293 if h=NameGeneration.global_heap then Syntax.const "_AssignH" $ l $ r 294 else raise Match 295 | deref_update x = raise Match 296 (* First we need to determine if this is a heap update or normal assign *) 297 fun deref_assign (Const ("_antiquoteCur",_)$Const (h,_)) r = 298 if h=NameGeneration.global_heap then deref_update r else 299 raise Match 300 | deref_assign l r = raise Match 301 fun assign_tr [l,r] = deref_assign l r 302 | assign_tr ts = raise Match 303in [("CTypesDefs.lift",K lift_tr),("_Assign",K assign_tr)] end; 304*} 305 306print_translation {* 307let 308 fun sep_app_tr [l,r] = Syntax.const "_sep_assert" $ l 309 | sep_app_tr ts = raise Match 310in [("sep_app",K sep_app_tr)] end; 311*} 312 313syntax "_h_t_valid" :: "'a::c_type ptr \<Rightarrow> bool" ("\<Turnstile>\<^sub>t _" [99] 100) 314 315(* will only work when globals record is defined 316term "\<lbrace> \<Turnstile>\<^sub>t bar \<rbrace>" *) 317 318abbreviation 319 "lift_t_c" :: "heap_mem \<times> heap_typ_desc \<Rightarrow> 'a::c_type typ_heap" 320where 321 "lift_t_c s == lift_t c_guard s" 322 323syntax 324 "_h_t_valid" :: "heap_typ_desc \<Rightarrow> 'a::c_type ptr \<Rightarrow> bool" ("_ \<Turnstile>\<^sub>t _" [99,99] 100) 325translations 326 "d \<Turnstile>\<^sub>t p" == "d,CONST c_guard \<Turnstile>\<^sub>t p" 327 328lemma h_t_valid_c_guard: 329 "d \<Turnstile>\<^sub>t p \<Longrightarrow> c_guard p" 330 by (clarsimp simp: h_t_valid_def) 331 332lemma h_t_valid_NULL [simp]: 333 "\<not> d \<Turnstile>\<^sub>t (NULL::'a::mem_type ptr)" 334 by (clarsimp simp: h_t_valid_def dest!: c_guard_NULL) 335 336lemma h_t_valid_ptr_aligned: 337 "d \<Turnstile>\<^sub>t p \<Longrightarrow> ptr_aligned p" 338 by (auto simp: h_t_valid_def dest: c_guard_ptr_aligned) 339 340lemma lift_t_NULL: 341 "lift_t_c s (NULL::'a::mem_type ptr) = None" 342apply(case_tac s) 343apply(auto simp: lift_t_if) 344done 345 346lemma lift_t_ptr_aligned [simp]: 347 "lift_t_c s p = Some v \<Longrightarrow> ptr_aligned p" 348 by (auto dest: lift_t_g c_guard_ptr_aligned) 349 350lemmas c_typ_rewrs = typ_rewrs h_t_valid_ptr_aligned lift_t_NULL 351 352datatype c_exntype = Break | Return | Continue 353datatype strictc_errortype = 354 Div_0 355 | C_Guard (* merge of Alignment and Null_Dereference *) 356 | MemorySafety 357 | ShiftError 358 | SideEffects 359 | ArrayBounds 360 | SignedArithmetic 361 | DontReach 362 | GhostStateError 363 | UnspecifiedSyntax 364 | OwnershipError 365 | UndefinedFunction 366 | AdditionalError string 367 | ImpossibleSpec 368 369definition 370 unspecified_syntax_error :: "string => bool" 371where 372 "unspecified_syntax_error s = False" 373 374lemmas hrs_simps = hrs_mem_update_def hrs_mem_def hrs_htd_update_def 375 hrs_htd_def 376 377lemma sep_map'_lift_lift: 378 fixes pa :: "'a :: mem_type ptr" and xf :: "'a \<Rightarrow> 'b :: mem_type" 379 assumes fl: "(field_lookup (typ_info_t TYPE('a)) f 0) \<equiv> 380 Some (adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x)), m')" 381 and xf_xfu: "fg_cons xf (xfu \<circ> (\<lambda>x _. x))" 382 shows "(pa \<hookrightarrow> v)(lift_state h) \<Longrightarrow> CTypesDefs.lift (fst h) (Ptr &(pa\<rightarrow>f)) = xf v" 383 using fl xf_xfu 384 apply - 385 apply (clarsimp simp: o_def) 386 apply (rule sep_map'_lift [OF sep_map'_field_map_inv, where g1=c_guard]) 387 apply (subst (asm) surjective_pairing [where t = h]) 388 apply assumption 389 apply fastforce 390 apply (subst export_tag_adjust_ti2 [OF _ wf_lf wf_desc]) 391 apply (simp add: fg_cons_def) 392 apply (rule meta_eq_to_obj_eq [OF typ_uinfo_t_def, symmetric]) 393 apply (rule guard_mono_True) 394 apply (subst access_ti\<^sub>0_update_ti) 395 apply (subst access_ti\<^sub>0_to_bytes) 396 apply (subst o_def) 397 apply (rule inv_p [symmetric]) 398 done 399 400lemma lift_t_update_fld_other: 401 fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr" 402 assumes fl: "field_ti TYPE('a) f = Some (adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x)))" 403 and xf_xfu: "fg_cons xf (xfu \<circ> (\<lambda>x _. x))" 404 and disj: "typ_uinfo_t TYPE('c :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b)" 405 and cl: "lift_t c_guard hp ptr = Some z" 406 shows "(lift_t c_guard (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>f)) val) hp)) = 407 (lift_t c_guard hp :: 'c :: mem_type typ_heap)" 408 (is "?LHS = ?RHS") 409proof - 410 let ?ati = "adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x))" 411 have eui: "typ_uinfo_t TYPE('b) = export_uinfo (?ati)" using xf_xfu 412 apply (subst export_tag_adjust_ti2 [OF _ wf_lf wf_desc]) 413 apply (simp add: fg_cons_def ) 414 apply (rule meta_eq_to_obj_eq [OF typ_uinfo_t_def]) 415 done 416 417 have cl': "lift_t c_guard (fst hp, snd hp) ptr = Some z" using cl by simp 418 419 show ?thesis using fl 420 apply (clarsimp simp add: hrs_mem_update_def split_def field_ti_def split: option.splits) 421 apply (subst typ_rewrs(5)) 422 apply (rule lift_t_mono) 423 apply assumption 424 apply (rule cl') 425 apply (rule eui [symmetric]) 426 apply (rule guard_mono_True) 427 apply (rule disj) 428 apply simp 429 done 430qed 431 432lemma idupdate_compupdate_fold_congE: 433 assumes idu: "\<And>r. upd (\<lambda>x. accr r) r = r" 434 assumes cpu: "\<And>f f' r. upd f (upd f' r) = upd (f o f') r" 435 and r: "r = r'" and v: "accr r' = v'" 436 and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v" 437 shows "upd f r = upd f' r'" 438 apply (subgoal_tac "upd (f o (\<lambda>x. accr r')) r' = upd (f' o (\<lambda>x. accr r')) r'") 439 apply (simp add: cpu[symmetric] idu r) 440 apply (simp add: o_def f v) 441 done 442 443lemma field_lookup_field_ti: 444 "field_lookup (typ_info_t TYPE('a :: c_type)) f 0 \<equiv> Some (a, b) \<Longrightarrow> field_ti TYPE('a) f = Some a" 445 unfolding field_ti_def by simp 446 447definition 448 lvar_nondet_init :: "(('c,'d) state_scheme \<Rightarrow> 'a) \<Rightarrow> (('a \<Rightarrow> 'a) \<Rightarrow> (('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme)) 449 \<Rightarrow> (('c, 'd) state_scheme, 'x, 'e) com" 450where 451 "lvar_nondet_init accessor upd \<equiv> Spec {(s, t). \<exists>v. t = (upd (\<lambda>_. v)) s}" 452 453axiomatization 454 asm_semantics :: "string \<Rightarrow> addr list 455 \<Rightarrow> (heap_mem \<times> 'a) \<Rightarrow> (addr \<times> (heap_mem \<times> 'a)) set" 456and 457 asm_fetch :: "'s \<Rightarrow> (heap_mem \<times> 'a)" 458and 459 asm_store :: "('s \<Rightarrow> 'b) \<Rightarrow> (heap_mem \<times> 'a) \<Rightarrow> 's \<Rightarrow> 's" 460where 461 asm_semantics_enabled: 462 "\<forall>iv. asm_semantics nm addr iv \<noteq> {}" 463and 464 asm_store_eq: 465 "\<forall>x s. ghost_data (asm_store ghost_data x s) = ghost_data s" 466 467definition 468 asm_spec :: "'a itself \<Rightarrow> ('g \<Rightarrow> 'b) \<Rightarrow> bool \<Rightarrow> string 469 \<Rightarrow> (addr \<Rightarrow> ('g, 's) state_scheme \<Rightarrow> ('g, 's) state_scheme) 470 \<Rightarrow> (('g, 's) state_scheme \<Rightarrow> addr list) 471 \<Rightarrow> (('g, 's) state_scheme \<times> ('g, 's) state_scheme) set" 472where 473 "asm_spec ti gdata vol spec lhs vs 474 = {(s, s'). \<exists>(v', (gl' :: (heap_mem \<times> 'a))) 475 \<in> asm_semantics spec (vs s) (asm_fetch (globals s)). 476 s' = lhs v' (globals_update (asm_store gdata gl') s)}" 477 478lemma asm_spec_enabled: 479 "\<exists>s'. (s, s') \<in> asm_spec ti gdata vol spec lhs vs" 480 using asm_semantics_enabled[rule_format, where nm = spec 481 and addr="vs s" and iv="asm_fetch (globals s)"] 482 by (auto simp add: asm_spec_def) 483 484lemma asm_specE: 485 assumes s: "(s, s') \<in> asm_spec (ti :: 'a itself) gdata vol spec lhs vs" 486 and concl: "\<And>v' gl'. \<lbrakk> (v', (gl' :: (heap_mem \<times> 'a))) \<in> asm_semantics spec (vs s) (asm_fetch (globals s)); 487 s' = lhs v' (globals_update (asm_store gdata gl') s); 488 gdata (asm_store gdata gl' (globals s)) = gdata (globals s) \<rbrakk> 489 \<Longrightarrow> P" 490 shows "P" 491 using s concl 492 by (clarsimp simp: asm_spec_def asm_store_eq) 493 494lemmas state_eqE = arg_cong[where f="\<lambda>s. (globals s, state.more s)", elim_format] 495 496lemmas asm_store_eq_helper 497 = arg_cong2[where f="(=)" and a="asm_store f v s"] 498 arg_cong2[where f="(=)" and c="asm_store f v s"] 499 for f v s 500 501definition 502 asm_semantics_ok_to_ignore :: "'a itself \<Rightarrow> bool \<Rightarrow> string \<Rightarrow> bool" 503where 504 "asm_semantics_ok_to_ignore ti volatile specifier 505 = (\<forall>xs gl. snd ` asm_semantics specifier xs (gl :: (heap_mem \<times> 'a)) = {gl})" 506 507end 508