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 :: word32) < 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 :: word32) < 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
104lemma headM_wordsFromPTE[simp]:
105  "headM (wordsFromPTE pte) = (return (hd (wordsFromPTE pte)))"
106  unfolding wordsFromPTE_def
107  by (cases pte; simp)
108
109lemma length_wordsFromPTE:
110  "length (wordsFromPTE pte) = 2"
111  unfolding wordsFromPTE_def
112  by (cases pte; simp)
113
114lemma length_wordsFromPDE:
115  "length (wordsFromPDE pde) = 2"
116  unfolding wordsFromPDE_def
117  by (cases pde; simp)
118
119lemma storePTE_Basic_ccorres':
120  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
121   ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs
122     (storePTE p pte)
123     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
124        (Basic (\<lambda>s. globals_update( t_hrs_'_update
125            (hrs_mem_update (heap_update (f s) pte'))) s)))"
126  using length_wordsFromPTE[where pte=pte]
127  apply (simp add: storePTE_def tailM_def headM_def)
128  apply (case_tac "wordsFromPTE pte"; clarsimp)
129  apply (case_tac list; clarsimp)
130  apply (rule setObject_ccorres_helper)
131    apply (simp_all add: objBits_simps archObjSize_def table_bits_defs)
132  apply (rule conseqPre, vcg)
133  apply (rule subsetI, clarsimp simp: Collect_const_mem)
134  apply (rule cmap_relationE1, erule rf_sr_cpte_relation,
135         erule ko_at_projectKO_opt)
136  apply (rule conjI, fastforce intro: typ_heap_simps)
137  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
138  apply (rule conjI)
139   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
140                         update_pte_map_to_ptes
141                         update_pte_map_tos
142                         carray_map_relation_upd_triv)
143
144   apply (case_tac "f x", simp)
145
146   apply (erule cmap_relation_updI,
147          erule ko_at_projectKO_opt, simp+)
148  apply (simp add: cready_queues_relation_def
149                   carch_state_relation_def
150                   cmachine_state_relation_def
151                   Let_def typ_heap_simps
152                   cteCaps_of_def update_pte_map_tos table_bits_defs
153                   )
154  done
155
156
157lemma storePTE_Basic_ccorres:
158  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
159   ccorres dc xfdc \<top> {s. f s = p} hs
160     (storePTE p pte)
161     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)}
162        (Basic (\<lambda>s. globals_update( t_hrs_'_update
163            (hrs_mem_update (heap_update (pte_Ptr (f s)) pte'))) s)))"
164  apply (rule ccorres_guard_imp2)
165   apply (erule storePTE_Basic_ccorres')
166  apply simp
167  done
168
169lemma pde_stored_asid_update_valid_offset:
170  "valid_pde_mapping_offset' (ptr_val p && mask pdBits)
171      \<Longrightarrow> (pde_stored_asid  \<circ>\<^sub>m (clift (t_hrs_' cstate))(p \<mapsto> pde) \<circ>\<^sub>m pd_pointer_to_asid_slot)
172            = (pde_stored_asid  \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)"
173  apply (rule ext, clarsimp simp add: pd_pointer_to_asid_slot_def map_comp_eq)
174  apply (simp add: valid_pde_mapping_offset'_def mask_add_aligned)
175  apply (simp add: pd_asid_slot_def mask_def table_bits_defs)
176  done
177
178lemma storePDE_Basic_ccorres':
179  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
180   ccorres dc xfdc
181     (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits))
182     {s. ptr_val (f s) = p} hs
183     (storePDE p pde)
184     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
185        (Basic (\<lambda>s. globals_update( t_hrs_'_update
186            (hrs_mem_update (heap_update (f s) pde'))) s)))"
187  using length_wordsFromPDE[where pde=pde]
188  apply (simp add: storePDE_def tailM_def headM_def)
189  apply (case_tac "wordsFromPDE pde"; clarsimp)
190  apply (case_tac list; clarsimp)
191  apply (rule setObject_ccorres_helper)
192    apply (simp_all add: objBits_simps archObjSize_def table_bits_defs)
193  apply (rule conseqPre, vcg)
194  apply (rule subsetI, clarsimp simp: Collect_const_mem)
195  apply (rule cmap_relationE1, erule rf_sr_cpde_relation,
196         erule ko_at_projectKO_opt)
197  apply (rule conjI, fastforce intro: typ_heap_simps)
198  apply (case_tac "f x", clarsimp)
199  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
200  apply (rule conjI)
201   apply (clarsimp simp: cpspace_relation_def typ_heap_simps
202                         update_pde_map_to_pdes
203                         update_pde_map_tos
204                         carray_map_relation_upd_triv)
205   apply (erule cmap_relation_updI,
206          erule ko_at_projectKO_opt, simp+)
207  apply (simp add: cready_queues_relation_def
208                   carch_state_relation_def
209                   cmachine_state_relation_def
210                   Let_def typ_heap_simps table_bits_defs
211                   pde_stored_asid_update_valid_offset
212                   cteCaps_of_def update_pde_map_tos)
213  done
214
215lemma storePDE_Basic_ccorres:
216  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
217   ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. f s = p} hs
218     (storePDE p pde)
219     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)}
220        (Basic (\<lambda>s. globals_update(t_hrs_'_update
221            (hrs_mem_update (heap_update (pde_Ptr (f s)) pde'))) s)))"
222  apply (rule ccorres_guard_imp2)
223   apply (erule storePDE_Basic_ccorres')
224  apply simp
225  done
226
227end
228end
229