1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory PSpace_C
12imports Ctac_lemmas_C
13begin
14
15context kernel begin
16
17lemma koTypeOf_injectKO:
18  fixes v :: "'a :: pspace_storable" shows
19  "koTypeOf (injectKO v) = koType TYPE('a)"
20  apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
21  apply (simp add: project_koType[symmetric])
22  done
23
24lemma setObject_obj_at_pre:
25  "\<lbrakk> updateObject ko = updateObject_default ko;
26       (1 :: machine_word) < 2 ^ objBits ko \<rbrakk>
27   \<Longrightarrow>
28   setObject p ko
29     = (stateAssert (typ_at' (koTypeOf (injectKO ko)) p) []
30           >>= (\<lambda>_. setObject p ko))"
31  apply (rule ext)
32  apply (case_tac "typ_at' (koTypeOf (injectKO ko)) p x")
33   apply (simp add: stateAssert_def bind_def
34                    get_def return_def)
35  apply (simp add: stateAssert_def bind_def
36                   get_def assert_def fail_def)
37  apply (simp add: setObject_def exec_gets split_def
38                   assert_opt_def split: option.split)
39  apply (clarsimp simp add: fail_def)
40  apply (simp add: bind_def simpler_modify_def split_def)
41  apply (rule context_conjI)
42   apply (clarsimp simp: updateObject_default_def
43                         in_monad)
44   apply (clarsimp simp: projectKOs in_magnitude_check)
45   apply (frule iffD1[OF project_koType, OF exI])
46   apply (clarsimp simp: typ_at'_def ko_wp_at'_def)
47   apply (simp only: objBitsT_koTypeOf[symmetric] objBits_def)
48   apply simp
49   apply (simp add: koTypeOf_injectKO)
50  apply (rule empty_failD[OF empty_fail_updateObject_default])
51  apply (rule ccontr, erule nonemptyE)
52  apply clarsimp
53  done
54
55
56
57lemma setObject_ccorres_helper:
58  fixes ko :: "'a :: pspace_storable"
59  assumes valid: "\<And>\<sigma> (ko' :: 'a).
60        \<Gamma> \<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ko_at' ko' p \<sigma>}
61              c {s. (\<sigma>\<lparr>ksPSpace := ksPSpace \<sigma> (p \<mapsto> injectKO ko)\<rparr>, s) \<in> rf_sr}"
62  shows "\<lbrakk> \<And>ko :: 'a. updateObject ko = updateObject_default ko;
63           \<And>ko :: 'a. (1 :: machine_word) < 2 ^ objBits ko \<rbrakk>
64    \<Longrightarrow> ccorres dc xfdc P P' hs (setObject p ko) c"
65  apply (rule ccorres_guard_imp2)
66   apply (subst setObject_obj_at_pre)
67     apply simp+
68   apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. P'"])
69      defer
70      apply (rule stateAssert_inv)
71     apply (rule stateAssert_sp[where P=P])
72    apply (rule empty_fail_stateAssert)
73   apply simp
74  apply (rule ccorres_from_vcg)
75  apply (rule allI)
76  apply (rule hoare_complete)
77  apply (clarsimp simp: HoarePartialDef.valid_def)
78  apply (simp add: typ_at_to_obj_at' koTypeOf_injectKO)
79  apply (drule obj_at_ko_at', clarsimp)
80  apply (cut_tac \<sigma>1=\<sigma> and ko'1=koa in valid)
81  apply (drule hoare_sound,
82         clarsimp simp: cvalid_def HoarePartialDef.valid_def)
83  apply (elim allE, drule(1) mp)
84  apply (drule mp, simp)
85  apply clarsimp
86  apply (rule imageI[OF CollectI])
87  apply (rule rev_bexI)
88   apply (rule setObject_eq, simp+)
89    apply (simp add: objBits_def)
90    apply (simp only: objBitsT_koTypeOf[symmetric]
91                      koTypeOf_injectKO)
92   apply assumption
93  apply simp
94  done
95
96
97lemma carray_map_relation_upd_triv:
98  "f x = Some (v :: 'a :: pspace_storable)
99    \<Longrightarrow> carray_map_relation n (f (x \<mapsto> y)) hp ptrf = carray_map_relation n f hp ptrf"
100  by (simp add: carray_map_relation_def objBits_def objBitsT_koTypeOf[symmetric]
101                koTypeOf_injectKO
102           del: objBitsT_koTypeOf)
103
104
105lemma storePTE_Basic_ccorres':
106  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
107   ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs
108     (storePTE p pte)
109     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
110        (Basic (\<lambda>s. globals_update( t_hrs_'_update
111            (hrs_mem_update (heap_update (f s) pte'))) s)))"
112  apply (simp add: storePTE_def)
113  apply (rule setObject_ccorres_helper)
114    apply (simp_all add: objBits_simps archObjSize_def bit_simps)
115  apply (rule conseqPre, vcg)
116  apply (rule subsetI, clarsimp simp: Collect_const_mem)
117  apply (rule cmap_relationE1, erule rf_sr_cpte_relation,
118         erule ko_at_projectKO_opt)
119  apply (rule conjI, fastforce intro: typ_heap_simps)
120  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
121  apply (rule conjI)
122   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
123                         update_pte_map_to_ptes
124                         update_pte_map_tos
125                         carray_map_relation_upd_triv)
126
127   apply (case_tac "f x", simp)
128
129   apply (erule cmap_relation_updI,
130          erule ko_at_projectKO_opt, simp+)
131  apply (simp add: cready_queues_relation_def
132                   carch_state_relation_def
133                   fpu_null_state_heap_update_tag_disj_simps
134                   cmachine_state_relation_def
135                   Let_def typ_heap_simps
136                   cteCaps_of_def update_pte_map_tos bit_simps)
137  done
138
139
140lemma storePTE_Basic_ccorres:
141  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
142   ccorres dc xfdc \<top> {s. f s = p} hs
143     (storePTE p pte)
144     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)}
145        (Basic (\<lambda>s. globals_update( t_hrs_'_update
146            (hrs_mem_update (heap_update (pte_Ptr (f s)) pte'))) s)))"
147  apply (rule ccorres_guard_imp2)
148   apply (erule storePTE_Basic_ccorres')
149  apply simp
150  done
151
152lemma storePDE_Basic_ccorres':
153  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
154   ccorres dc xfdc
155     \<top>
156     {s. ptr_val (f s) = p} hs
157     (storePDE p pde)
158     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
159        (Basic (\<lambda>s. globals_update( t_hrs_'_update
160            (hrs_mem_update (heap_update (f s) pde'))) s)))"
161  apply (simp add: storePDE_def)
162  apply (rule setObject_ccorres_helper)
163    apply (simp_all add: objBits_simps archObjSize_def bit_simps)
164  apply (rule conseqPre, vcg)
165  apply (rule subsetI, clarsimp simp: Collect_const_mem)
166  apply (rule cmap_relationE1, erule rf_sr_cpde_relation,
167         erule ko_at_projectKO_opt)
168  apply (rule conjI, fastforce intro: typ_heap_simps)
169  apply (case_tac "f x", clarsimp)
170  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
171  apply (rule conjI)
172   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
173                         update_pde_map_to_pdes
174                         update_pde_map_tos
175                         carray_map_relation_upd_triv)
176   apply (erule cmap_relation_updI,
177          erule ko_at_projectKO_opt, simp+)
178  apply (simp add: cready_queues_relation_def
179                   carch_state_relation_def
180                   fpu_null_state_heap_update_tag_disj_simps
181                   cmachine_state_relation_def
182                   Let_def typ_heap_simps bit_simps
183                   cteCaps_of_def update_pde_map_tos)
184  done
185
186lemma storePDE_Basic_ccorres:
187  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
188   ccorres dc xfdc \<top> {s. f s = p} hs
189     (storePDE p pde)
190     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)}
191        (Basic (\<lambda>s. globals_update(t_hrs_'_update
192            (hrs_mem_update (heap_update (pde_Ptr (f s)) pde'))) s)))"
193  apply (rule ccorres_guard_imp2)
194   apply (erule storePDE_Basic_ccorres')
195  apply simp
196  done
197
198lemma storePDPTE_Basic_ccorres':
199  "\<lbrakk> cpdpte_relation pdpte pdpte' \<rbrakk> \<Longrightarrow>
200   ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs
201     (storePDPTE p pdpte)
202     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
203        (Basic (\<lambda>s. globals_update( t_hrs_'_update
204            (hrs_mem_update (heap_update (f s) pdpte'))) s)))"
205  apply (simp add: storePDPTE_def)
206  apply (rule setObject_ccorres_helper)
207    apply (simp_all add: objBits_simps archObjSize_def bit_simps)
208  apply (rule conseqPre, vcg)
209  apply (rule subsetI, clarsimp simp: Collect_const_mem)
210  apply (rule cmap_relationE1, erule rf_sr_cpdpte_relation,
211         erule ko_at_projectKO_opt)
212  apply (rule conjI, fastforce intro: typ_heap_simps)
213  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
214  apply (rule conjI)
215   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
216                         update_pdpte_map_to_pdptes
217                         update_pdpte_map_tos
218                         carray_map_relation_upd_triv)
219
220   apply (case_tac "f x", simp)
221
222   apply (erule cmap_relation_updI,
223          erule ko_at_projectKO_opt, simp+)
224  apply (simp add: cready_queues_relation_def
225                   carch_state_relation_def
226                   fpu_null_state_heap_update_tag_disj_simps
227                   cmachine_state_relation_def
228                   Let_def typ_heap_simps
229                   cteCaps_of_def update_pdpte_map_tos bit_simps)
230  done
231
232
233lemma storePDPTE_Basic_ccorres:
234  "\<lbrakk> cpdpte_relation pdpte pdpte' \<rbrakk> \<Longrightarrow>
235   ccorres dc xfdc \<top> {s. f s = p} hs
236     (storePDPTE p pdpte)
237     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pdpte_Ptr (f s)}
238        (Basic (\<lambda>s. globals_update( t_hrs_'_update
239            (hrs_mem_update (heap_update (pdpte_Ptr (f s)) pdpte'))) s)))"
240  apply (rule ccorres_guard_imp2)
241   apply (erule storePDPTE_Basic_ccorres')
242  apply simp
243  done
244
245lemma storePML4E_Basic_ccorres':
246  "\<lbrakk> cpml4e_relation pml4e pml4e' \<rbrakk> \<Longrightarrow>
247   ccorres dc xfdc
248     \<top>
249     {s. ptr_val (f s) = p} hs
250     (storePML4E p pml4e)
251     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
252        (Basic (\<lambda>s. globals_update( t_hrs_'_update
253            (hrs_mem_update (heap_update (f s) pml4e'))) s)))"
254  apply (simp add: storePML4E_def)
255  apply (rule setObject_ccorres_helper)
256    apply (simp_all add: objBits_simps archObjSize_def bit_simps)
257  apply (rule conseqPre, vcg)
258  apply (rule subsetI, clarsimp simp: Collect_const_mem)
259  apply (rule cmap_relationE1, erule rf_sr_cpml4e_relation,
260         erule ko_at_projectKO_opt)
261  apply (rule conjI, fastforce intro: typ_heap_simps)
262  apply (case_tac "f x", clarsimp)
263  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
264  apply (rule conjI)
265   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
266                         update_pml4e_map_to_pml4es
267                         update_pml4e_map_tos
268                         carray_map_relation_upd_triv)
269   apply (erule cmap_relation_updI,
270          erule ko_at_projectKO_opt, simp+)
271  apply (simp add: cready_queues_relation_def
272                   carch_state_relation_def
273                   fpu_null_state_heap_update_tag_disj_simps
274                   cmachine_state_relation_def
275                   Let_def typ_heap_simps bit_simps
276                   cteCaps_of_def update_pml4e_map_tos)
277  done
278
279lemma storePML4E_Basic_ccorres:
280  "\<lbrakk> cpml4e_relation pml4e pml4e' \<rbrakk> \<Longrightarrow>
281   ccorres dc xfdc \<top> {s. f s = p} hs
282     (storePML4E p pml4e)
283     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pml4e_Ptr (f s)}
284        (Basic (\<lambda>s. globals_update(t_hrs_'_update
285            (hrs_mem_update (heap_update (pml4e_Ptr (f s)) pml4e'))) s)))"
286  apply (rule ccorres_guard_imp2)
287   apply (erule storePML4E_Basic_ccorres')
288  apply simp
289  done
290
291end
292end
293