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