-
Notifications
You must be signed in to change notification settings - Fork 0
/
CSpaceAcc_C.thy
261 lines (229 loc) · 9.24 KB
/
CSpaceAcc_C.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
(* collects lemmas common to the various CSpace branches *)
theory CSpaceAcc_C
imports "../refine/EmptyFail" "../../lib/clib/Ctac"
begin
(* For resolving schematics *)
lemma lift_t_cslift:
"cslift x p = Some y \<Longrightarrow>
lift_t c_guard (hrs_mem (t_hrs_' (globals x)), hrs_htd (t_hrs_' (globals x))) p = Some y"
by (simp add: hrs_htd_def hrs_mem_def)
context kernel begin
lemma ccorres_pre_getAsyncEP:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. \<forall>aep. ko_at' aep p s \<longrightarrow> P aep s)
({s'. \<forall>aep s. (s, s') \<in> rf_sr \<and> ko_at' aep p s \<longrightarrow> s' \<in> P' aep})
hs (getAsyncEP p >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
apply wp[1]
apply (rule get_aep_sp')
apply simp
apply assumption
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply simp
apply assumption
apply fastforce
done
lemma ccorres_pre_getCTE:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s))
{s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte') }
hs (getCTE p >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
apply wp[1]
apply (rule getCTE_sp)
apply simp
apply assumption
apply clarsimp
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply (simp add: cte_wp_at_ctes_of)
apply assumption
apply (simp add: cte_wp_at_ctes_of)
apply (drule (1) rf_sr_ctes_of_clift)
apply clarsimp
apply (simp add: c_valid_cte_eq)
done
lemmas ccorres_getCTE = ccorres_pre_getCTE
lemma getCurThread_sp:
"\<lbrace>P\<rbrace> getCurThread \<lbrace>\<lambda>rv s. ksCurThread s = rv \<and> P s\<rbrace>"
apply wp
apply simp
done
lemma rf_sr_ksCurThread:
"(s, s') \<in> rf_sr \<Longrightarrow> ksCurThread_' (globals s')
= tcb_ptr_to_ctcb_ptr (ksCurThread s)"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
lemma ccorres_pre_getCurThread:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. (\<forall>rv. ksCurThread s = rv \<longrightarrow> P rv s))
{s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv
\<longrightarrow> s \<in> P' rv }
hs (getCurThread >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
apply wp[1]
apply (rule getCurThread_sp)
apply (clarsimp simp: empty_fail_def getCurThread_def simpler_gets_def)
apply assumption
apply clarsimp
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply clarsimp
apply assumption
apply (clarsimp simp: rf_sr_ksCurThread)
done
lemma cd_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma curDomain_sp:
"\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>"
apply wp
apply simp
done
lemma rf_sr_ksCurDomain:
"(s, s') \<in> rf_sr \<Longrightarrow> ksCurDomain_' (globals s')
= ucast (ksCurDomain s)"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
lemma ccorres_pre_curDomain:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. (\<forall>rv. ksCurDomain s = rv \<longrightarrow> P rv s))
{s. \<forall>rv. ksCurDomain_' (globals s) = ucast rv
\<longrightarrow> s \<in> P' rv }
hs (curDomain >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
apply wp[1]
apply (rule curDomain_sp)
apply (clarsimp simp: empty_fail_def curDomain_def simpler_gets_def)
apply assumption
apply clarsimp
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply clarsimp
apply assumption
apply (clarsimp simp: rf_sr_ksCurDomain)
done
lemma scast_EXCPT_NONE [simp]: "scast EXCEPTION_NONE = EXCEPTION_NONE"
unfolding scast_def EXCEPTION_NONE_def
by simp
lemma pageBitsForSize_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>pagesize && mask 2 = \<acute>pagesize\<rbrace> Call pageBitsForSize_'proc
\<lbrace> \<acute>ret__unsigned = of_nat (pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>pagesize)) \<rbrace>"
apply vcg
apply clarsimp
apply (clarsimp simp: pageBitsForSize_def gen_framesize_to_H_def
ARMSmallPageBits_def ARMLargePageBits_def ARMSectionBits_def
ARMSuperSectionBits_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def Kernel_C.ARMSection_def
Kernel_C.ARMSuperSection_def)
apply (subst (asm) mask_eq_iff_w2p, simp add: word_size)
apply simp
apply (drule word_less_cases [where y=4])
apply (erule disjE, simp, simp)
apply (drule word_less_cases [where y=3])
apply (erule disjE, simp, simp)
apply (drule word_less_cases [where y=2])
apply auto
done
lemma updateMDB_pre_cte_at:
"\<lbrace>\<lambda>s. \<not> (p \<noteq> 0 \<longrightarrow> cte_at' p s) \<rbrace> updateMDB p f \<lbrace> \<lambda>_ _. False \<rbrace>"
unfolding updateMDB_def Let_def
apply simp
apply (intro impI)
apply (wp getCTE_wp)
apply clarsimp
done
lemma getSlotCap_pre_cte_at:
"\<lbrace>\<lambda>s. \<not> cte_at' p s \<rbrace> getSlotCap p \<lbrace> \<lambda>_ _. False \<rbrace>"
unfolding getSlotCap_def
apply simp
apply (wp getCTE_wp)
apply clarsimp
done
lemmas ccorres_updateMDB_cte_at = ccorres_guard_from_wp [OF updateMDB_pre_cte_at empty_fail_updateMDB]
ccorres_guard_from_wp_bind [OF updateMDB_pre_cte_at empty_fail_updateMDB]
lemmas ccorres_getSlotCap_cte_at = ccorres_guard_from_wp [OF getSlotCap_pre_cte_at empty_fail_getSlotCap]
ccorres_guard_from_wp_bind [OF getSlotCap_pre_cte_at empty_fail_getSlotCap]
lemma wordFromRights_spec:
defines "crl s \<equiv> (cap_rights_lift \<^bsup>s\<^esup>cap_rights)"
shows "\<forall>s. \<Gamma> \<turnstile> {s} \<acute>ret__unsigned_long :== PROC wordFromRights(\<acute>cap_rights)
\<lbrace> \<acute>ret__unsigned_long =
((capAllowGrant_CL (crl s) << 2)
|| (capAllowRead_CL (crl s) << 1)
|| capAllowWrite_CL (crl s)) \<rbrace>"
unfolding crl_def
apply vcg
apply (simp add: word_sle_def word_sless_def)
apply (simp add: cap_rights_lift_def shiftr_over_and_dist)
apply (simp add: mask_shift_simps)
apply (simp add: word_ao_dist2[symmetric])
done
lemma errlookup_fault_errstate [simp]:
"errlookup_fault (errstate s) = lookup_fault_lift (current_lookup_fault_' (globals s))"
unfolding errstate_def
by simp
lemma errfault_errstate [simp]:
"errfault (errstate s) = fault_lift (current_fault_' (globals s))"
unfolding errstate_def
by simp
lemma errsyscall_errstate [simp]:
"errsyscall (errstate s) = (current_syscall_error_' (globals s))"
unfolding errstate_def
by simp
lemma locateSlot_ccorres [corres]:
assumes gl: "\<And>v s. globals (xfu v s) = globals s" -- "for state rel. preservation"
and fg: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v"
shows "ccorres (\<lambda>v v'. v' = Ptr v) xf \<top> {_. cnode = cnode' \<and> offset = offset'} hs (locateSlot cnode offset)
(Basic (\<lambda>s. xfu (\<lambda>_. Ptr (cnode' + offset' * of_nat (size_of TYPE(cte_C))) :: cte_C ptr) s))"
unfolding locateSlot_def using gl fg
apply -
apply (simp add: size_of_def split del: split_if)
apply (rule ccorres_return)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: fg objBits_simps)
done
lemma getSlotCap_h_val_ccorres [corres]:
fixes p :: "cstate \<Rightarrow> cte_C ptr"
assumes gl: "\<And>v s. globals (xfu v s) = globals s" -- "for state rel. preservation"
and fg: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v"
shows "ccorres ccap_relation xf \<top> {s. p s = Ptr a} hs
(getSlotCap a) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (Ptr &(p s\<rightarrow>[''cap_C'']) :: cap_C ptr)) s))"
unfolding getSlotCap_def
apply (rule ccorres_add_UNIV_Int)
apply (cinitlift p) -- "EVIL!"
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE)
apply (rule_tac R = "\<lambda>s. ctes_of s a = Some rva" in ccorres_return [where R' = UNIV])
apply vcg
apply (clarsimp simp: gl fg cte_wp_at_ctes_of)
apply (erule (1) rf_sr_ctes_of_cliftE)
apply (clarsimp simp add: typ_heap_simps ccap_relation_def cte_to_H_def cl_valid_cte_def c_valid_cap_def)
apply simp
done
end
end