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 CSpace_All
12imports CSpace_RAB_C CSpace_C
13begin
14
15context kernel_m
16begin
17
18
19
20
21abbreviation
22  "lookupCapAndSlot_xf \<equiv> liftxf errstate lookupCapAndSlot_ret_C.status_C
23                             (\<lambda> x . (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x))
24                             ret__struct_lookupCapAndSlot_ret_C_'"
25
26
27
28
29(* FIXME: move *)
30lemma ccorres_return_into_rel:
31  "ccorres (\<lambda>rv rv'. r (f rv) rv') xf G G' hs a c
32  \<Longrightarrow> ccorres r xf G G' hs (a >>= (\<lambda>rv. return (f rv))) c"
33  by (simp add: liftM_def[symmetric] o_def)
34
35lemma lookupCap_ccorres':
36  "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf
37   (valid_pspace' and tcb_at' a)
38   (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) []
39  (lookupCap a b) (Call lookupCap_'proc)"
40  apply (cinit lift: cPtr_' thread_' simp: lookupCapAndSlot_def liftME_def bindE_assoc)
41
42   apply (ctac (no_vcg) add: lookupSlotForThread_ccorres')
43     \<comment> \<open>case where lu_ret.status is EXCEPTION_NONE\<close>
44     apply (simp  add: split_beta cong:call_ignore_cong)
45     apply csymbr  \<comment> \<open>call status_C_update\<close>
46     apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_def
47                 del: Collect_const)
48     apply (rule ccorres_move_c_guard_cte)
49     apply (ctac )
50       apply (rule ccorres_return_CE [unfolded returnOk_def, simplified], simp+)[1]
51      apply wp
52     apply vcg
53    \<comment> \<open>case where lu_ret.status is *not* EXCEPTION_NONE\<close>
54    apply simp
55    apply (rule ccorres_split_throws)
56     apply (rule ccorres_rhs_assoc)+
57     apply csymbr
58     apply csymbr \<comment> \<open>call cap_null_cap_new_'proc\<close>
59     apply csymbr
60     apply (rule ccorres_return_C_errorE, simp+)[1]
61    apply vcg
62   apply (wp | simp)+
63
64  \<comment> \<open>last subgoal\<close>
65  apply (clarsimp simp: valid_pspace_valid_objs')
66  apply (intro impI conjI allI)
67    apply (simp add: lookupSlot_raw_rel_def)
68    apply (rule_tac y="ret___struct_lookupCap_ret_C_' s" for s
69                    in arg_cong, fastforce)
70   apply simp
71  apply (case_tac err, simp+) [1]
72done
73
74lemma lookupCap_ccorres:
75  "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf
76   (\<lambda>s. invs' s \<and> (tcb_at' a s))
77   (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) []
78  (lookupCap a b) (Call lookupCap_'proc)"
79  apply (rule ccorres_guard_imp2, rule lookupCap_ccorres')
80  apply fastforce
81  done
82
83
84lemma lookupCapAndSlot_ccorres :
85  "ccorres
86   (lookup_failure_rel \<currency> (\<lambda>(c,s) (c',s'). ccap_relation c c' \<and> s'= Ptr s)) lookupCapAndSlot_xf
87   (\<lambda>s. invs' s \<and> tcb_at' thread s)
88   (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>cPtr = cPtr\<rbrace> ) []
89  (lookupCapAndSlot thread cPtr)
90  (Call lookupCapAndSlot_'proc)"
91  apply (cinit lift: thread_' cPtr_')
92
93   apply (ctac (no_vcg))
94     \<comment> \<open>case where lu_ret.status is EXCEPTION_NONE\<close>
95     apply (simp  add: split_beta cong:call_ignore_cong)
96     apply csymbr  \<comment> \<open>call status_C_update\<close>
97     apply csymbr  \<comment> \<open>call slot_C_update\<close>
98     apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_bindE
99                 del: Collect_const)
100     apply (rule ccorres_move_c_guard_cte)
101     apply (rule_tac P="cte_at' rv" and P'=UNIV in ccorres_from_vcg_throws)
102     apply (rule allI, rule conseqPre, vcg)
103     apply (clarsimp simp: Bex_def in_monad getSlotCap_def in_getCTE2 cte_wp_at_ctes_of)
104     apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
105     apply (simp add: ccte_relation_ccap_relation typ_heap_simps')
106    \<comment> \<open>case where lu_ret.status is *not* EXCEPTION_NONE\<close>
107    apply simp
108    apply (rule ccorres_split_throws)
109     apply (rule ccorres_rhs_assoc)+
110     apply csymbr+
111     apply (rule ccorres_return_C_errorE, simp+)[1]
112
113    apply vcg
114   apply (wp | simp)+
115
116  \<comment> \<open>last subgoal\<close>
117  apply clarsimp
118  apply (rule conjI, fastforce)
119  apply clarsimp
120  apply (case_tac err, simp+) [1]
121done
122
123
124(* FIXME: move *)
125lemma injection_handler_liftM:
126  "injection_handler f
127    = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)"
128  apply (intro ext, simp add: injection_handler_def liftM_def
129                              handleE'_def)
130  apply (rule bind_apply_cong, rule refl)
131  apply (simp add: throwError_def split: sum.split)
132  done
133
134lemma lookupErrorOnFailure_ccorres:
135  "ccorres (f \<currency> r) xf P P' hs a c
136    \<Longrightarrow> ccorres ((\<lambda>x y z. \<exists>w. x = FailedLookup isSource w \<and> f w y z) \<currency> r)
137             xf P P' hs
138             (lookupErrorOnFailure isSource a) c"
139  apply (simp add: lookupError_injection injection_handler_liftM)
140  apply (erule ccorres_rel_imp)
141  apply (auto split: sum.split)
142  done
143
144
145lemma lookup_failure_rel_fault_lift:
146  " \<lbrakk> st \<noteq> scast EXCEPTION_NONE;
147      lookup_failure_rel err st (errstate t)\<rbrakk>
148     \<Longrightarrow> \<exists>v. lookup_fault_lift (current_lookup_fault_' (globals t)) = Some v \<and> lookup_fault_to_H v = err"
149  apply (case_tac err, clarsimp+)
150  done
151
152lemma le_64_mask_eq:
153  "(bits::machine_word) \<le> 64 \<Longrightarrow> bits && mask 7 = bits"
154  apply (rule less_mask_eq, simp)
155  apply (erule le_less_trans, simp)
156  done
157
158lemma lookupSlotForCNodeOp_ccorres':
159  "ccorres
160   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
161   (\<lambda>s.  valid_pspace' s \<and> s  \<turnstile>' croot \<and> depth < 2 ^ word_bits)
162   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
163            {s. to_bool (isSource_' s) = isSource}  \<inter>
164            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
165            {s. depth_' s = of_nat depth} ) []
166  (lookupSlotForCNodeOp isSource croot capptr depth)
167  (Call lookupSlotForCNodeOp_'proc)"
168  apply (cinit lift: capptr_' isSource_' root___struct_cap_C_' depth_')
169   apply csymbr \<comment> \<open>slot_C_update\<close>
170   apply csymbr \<comment> \<open>cap_get_capType\<close>
171
172   apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2)
173      \<comment> \<open>correspondance of Haskell and C conditions\<close>
174      apply (clarsimp simp: Collect_const_mem cap_get_tag_isCap)
175
176     \<comment> \<open>case where root is *not* a CNode => throw InvalidRoot\<close>
177     apply simp
178     apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws)
179     apply (rule allI, rule conseqPre, vcg)
180     apply (clarsimp simp: throwError_def  return_def syscall_error_rel_def)
181     apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def)
182     apply (drule_tac  lookup_fault_lift_invalid_root)
183     apply clarsimp
184     apply (subst syscall_error_to_H_cases(6), simp+)[1]
185
186    \<comment> \<open>case where root is a CNode\<close>
187    apply (simp add: rangeCheck_def)
188    apply csymbr
189    apply (rule ccorres_Cond_rhs_Seq)
190     apply (rule_tac P="depth < 2 ^ word_bits" in ccorres_gen_asm)
191     apply (drule unat_of_nat64)
192     apply (simp add: unlessE_def fromIntegral_def integral_inv)
193     apply (rule ccorres_cond_true_seq)
194     apply (rule ccorres_split_throws)
195      apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws)
196      apply (rule allI, rule conseqPre, vcg)
197      apply (clarsimp simp: throwError_def  return_def syscall_error_rel_def
198                            word_sle_def syscall_error_to_H_cases
199                            word_size exception_defs)
200     apply vcg
201    apply csymbr
202    apply (rule_tac Q="\<lambda>s. depth < 2 ^ word_bits" and Q'=\<top> in ccorres_split_unless_throwError_cond)
203       \<comment> \<open>correspondance of Haskell and C conditions\<close>
204       apply (clarsimp simp: Collect_const_mem fromIntegral_def integral_inv)
205       apply (simp add: word_size unat_of_nat64 word_less_nat_alt
206                        word_less_1[symmetric] linorder_not_le)
207
208      \<comment> \<open>case of RangeError\<close>
209      apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws)
210      apply (rule allI, rule conseqPre, vcg)
211      apply (clarsimp simp: throwError_def  return_def syscall_error_rel_def)
212      apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def)
213      apply (subst syscall_error_to_H_cases(4), simp+)[1]
214      apply (simp add: word_size word_sle_def)
215
216     \<comment> \<open>case where there is *no* RangeError\<close>
217     apply (rule_tac xf'=lookupSlot_xf in  ccorres_rel_imp)
218      apply (rule_tac r="\<lambda>w w'. w'= Ptr w"
219          and f="\<lambda> st fl es. fl = scast EXCEPTION_SYSCALL_ERROR \<and>
220                           syscall_error_to_H (errsyscall es) (errlookup_fault es) = Some (FailedLookup isSource st)"
221          in lookupErrorOnFailure_ccorres)
222      apply (ctac (no_vcg))  \<comment> \<open>resolveAddressBits\<close>
223        \<comment> \<open>case where resolveAddressBits results in EXCEPTION_NONE\<close>
224        apply clarsimp
225      apply (rule_tac A=\<top> and A'=UNIV in ccorres_guard_imp2)
226         apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2)
227            \<comment> \<open>correspondance of Haskell and C conditions\<close>
228            apply (clarsimp simp: Collect_const_mem unat_gt_0)
229           \<comment> \<open>case where bits are remaining\<close>
230           apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws)
231         apply (rule allI, rule conseqPre, vcg)
232         apply (clarsimp simp: throwError_def return_def)
233         apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def)
234         apply (subst syscall_error_to_H_cases(6), simp+)[1]
235           apply (simp add: lookup_fault_depth_mismatch_lift)
236           apply (erule le_64_mask_eq)
237
238          \<comment> \<open>case where *no* bits are remaining\<close>
239          apply csymbr \<comment> \<open>slot_C_update\<close>
240        apply csymbr \<comment> \<open>status_C_update\<close>
241        apply (rule ccorres_return_CE, simp+)[1]
242
243       apply vcg
244
245        \<comment> \<open>guard_imp subgoal\<close>
246        apply clarsimp
247
248       \<comment> \<open>case where resolveAddressBits does *not* results in EXCEPTION_NONE\<close>
249       apply clarsimp
250     apply (rule_tac P= \<top> and P' ="\<lbrace>\<exists>v. (lookup_fault_lift (\<acute>current_lookup_fault)) = Some v
251                                              \<and> lookup_fault_to_H v = err \<rbrace>"
252                       in ccorres_from_vcg_throws)
253     apply (rule allI, rule conseqPre, vcg)
254     apply (clarsimp simp: throwError_def return_def)
255     apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def)
256     apply (subst syscall_error_to_H_cases(6), simp+)[1]
257      apply wp
258
259     \<comment> \<open>rel_imp\<close>
260     apply clarsimp
261     apply (case_tac x, clarsimp)
262      apply (simp add: syscall_error_rel_def errstate_def)
263     apply (clarsimp simp: word_bits_def word_size fromIntegral_def
264                           integral_inv)
265
266    apply vcg
267   apply vcg
268
269  \<comment> \<open>last subgoal\<close>
270  apply (clarsimp simp: if_1_0_0  to_bool_def true_def word_size
271                        fromIntegral_def integral_inv)
272  apply (case_tac "cap_get_tag root___struct_cap_C = scast cap_cnode_cap")
273   prefer 2 apply clarsimp
274  apply (clarsimp simp: unat_of_nat64 word_sle_def)
275  apply (simp add: Collect_const_mem lookup_failure_rel_fault_lift)
276  done
277
278
279lemma lookupSlotForCNodeOp_ccorres:
280  "ccorres
281   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
282   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and> depth < 2 ^ word_bits)
283   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
284            {s. to_bool (isSource_' s) = isSource}  \<inter>
285            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
286            {s. depth_' s = of_nat depth} ) []
287  (lookupSlotForCNodeOp isSource croot capptr depth)
288  (Call lookupSlotForCNodeOp_'proc)"
289  apply (rule ccorres_guard_imp2, rule lookupSlotForCNodeOp_ccorres')
290  apply fastforce
291  done
292
293lemma lookupSourceSlot_ccorres':
294  "ccorres
295   (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
296   (\<lambda>s.  valid_pspace' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
297   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
298            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
299            {s. depth_' s = of_nat depth} ) []
300  (lookupSourceSlot croot capptr depth)
301  (Call lookupSourceSlot_'proc)"
302  apply (cinit lift: capptr_' root___struct_cap_C_' depth_')
303   apply (rule ccorres_trim_returnE)
304     apply simp
305    apply simp
306   apply (ctac add: lookupSlotForCNodeOp_ccorres')
307  apply (clarsimp simp: to_bool_def true_def false_def)
308  done
309
310lemma lookupSourceSlot_ccorres:
311  "ccorres
312   (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
313   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
314   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
315            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
316            {s. depth_' s = of_nat depth} ) []
317  (lookupSourceSlot croot capptr depth)
318  (Call lookupSourceSlot_'proc)"
319  apply (rule ccorres_guard_imp2, rule lookupSourceSlot_ccorres')
320  apply fastforce
321  done
322
323lemma lookupTargetSlot_ccorres':
324  "ccorres
325   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
326   (\<lambda>s.  valid_pspace' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
327   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
328            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
329            {s. depth_' s = of_nat depth} ) []
330  (lookupTargetSlot croot capptr depth)
331  (Call lookupTargetSlot_'proc)"
332  apply (cinit lift: capptr_' root___struct_cap_C_' depth_')
333   apply (rule ccorres_trim_returnE)
334     apply simp
335    apply simp
336   apply (ctac add: lookupSlotForCNodeOp_ccorres')
337  apply (clarsimp simp: to_bool_def true_def false_def)
338  done
339
340lemma lookupTargetSlot_ccorres:
341  "ccorres
342   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
343   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
344  (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
345            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
346            {s. depth_' s = of_nat depth} ) []
347  (lookupTargetSlot croot capptr depth)
348  (Call lookupTargetSlot_'proc)"
349  apply (rule ccorres_guard_imp2, rule lookupTargetSlot_ccorres')
350  apply fastforce
351  done
352
353lemma lookupPivotSlot_ccorres:
354  "ccorres
355   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
356   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
357   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
358            {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter>
359            {s. depth_' s = of_nat depth} ) []
360  (lookupPivotSlot croot capptr depth)
361  (Call lookupPivotSlot_'proc)"
362  apply (cinit lift: capptr_' root___struct_cap_C_' depth_')
363   apply (rule ccorres_trim_returnE)
364     apply simp
365    apply simp
366   apply (ctac add: lookupSlotForCNodeOp_ccorres)
367  apply (clarsimp simp: to_bool_def true_def false_def)
368  done
369
370end
371end
372