1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory AsmSemanticsRespects 8 9imports "GlobalsSwap" 10 11begin 12 13definition 14 asm_semantics_protects_globs 15 :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> ((heap_raw_state \<Rightarrow> heap_raw_state) \<Rightarrow> 'g \<Rightarrow> 'g) 16 \<Rightarrow> ('g \<Rightarrow> 'a) 17 \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> ('g global_data list) 18 \<Rightarrow> bool" 19where 20 "asm_semantics_protects_globs mem memu ms symtab xs 21 \<equiv> (let sw = globals_swap mem memu symtab xs 22 in (\<forall>v v' s m' ms' specname. (v', m', ms') 23 \<in> asm_semantics specname v 24 (hrs_mem (mem (sw s)), ms s) 25 \<longrightarrow> const_globals_in_memory symtab xs 26 (hrs_mem (mem (sw (sw s)))) 27 \<longrightarrow> const_globals_in_memory symtab xs 28 (hrs_mem (mem (sw (memu (hrs_mem_update (\<lambda>_. m')) (sw s)))))))" 29 30abbreviation(input) 31 asm_ops_are_swap 32 :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> ((heap_raw_state \<Rightarrow> heap_raw_state) \<Rightarrow> 'g \<Rightarrow> 'g) 33 \<Rightarrow> ('g \<Rightarrow> 'a) \<Rightarrow> (('a \<Rightarrow> 'a) \<Rightarrow> 'g \<Rightarrow> 'g) 34 \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> ('g \<Rightarrow> 'b) \<Rightarrow> ('g global_data list) 35 \<Rightarrow> bool" 36where 37 "asm_ops_are_swap mem memu ms msu symtab gdata xs 38 \<equiv> (let sw = globals_swap mem memu symtab xs 39 in (\<forall>s. asm_fetch s = (hrs_mem (mem (sw s)), ms (sw s))) 40 \<and> (\<forall>v s. asm_store gdata v s = sw (msu (\<lambda>_. snd v) 41 (memu (hrs_mem_update (\<lambda>_. fst v)) (sw s)))) 42 \<and> asm_semantics_protects_globs mem memu ms symtab xs)" 43 44lemma asm_semantics_protects_globs_revD[OF refl]: 45 "sw = globals_swap mem memu symtab xs 46 \<Longrightarrow> (v', m', ms') 47 \<in> asm_semantics specname v 48 (hrs_mem (mem (sw s)), ms s) 49 \<Longrightarrow> asm_semantics_protects_globs mem memu ms symtab xs 50 \<longrightarrow> const_globals_in_memory symtab xs 51 (hrs_mem (mem (sw (sw s)))) 52 \<longrightarrow> const_globals_in_memory symtab xs 53 (hrs_mem (mem (sw (memu (hrs_mem_update (\<lambda>_. m')) (sw s)))))" 54 apply (simp add: asm_semantics_protects_globs_def Let_def) 55 apply blast 56 done 57 58end 59