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
11(*
12   CSpace invariants
13*)
14
15theory CSpace_I
16imports ArchAcc_R
17begin
18
19context begin interpretation Arch . (*FIXME: arch_split*)
20
21lemma capUntypedPtr_simps [simp]:
22  "capUntypedPtr (ThreadCap r) = r"
23  "capUntypedPtr (NotificationCap r badge a b) = r"
24  "capUntypedPtr (EndpointCap r badge a b c) = r"
25  "capUntypedPtr (Zombie r bits n) = r"
26  "capUntypedPtr (ArchObjectCap x) = Arch.capUntypedPtr x"
27  "capUntypedPtr (UntypedCap d r n f) = r"
28  "capUntypedPtr (CNodeCap r n g n2) = r"
29  "capUntypedPtr (ReplyCap r m) = r"
30  "Arch.capUntypedPtr (ARM_H.ASIDPoolCap r asid) = r"
31  "Arch.capUntypedPtr (ARM_H.PageCap d r rghts sz mapdata) = r"
32  "Arch.capUntypedPtr (ARM_H.PageTableCap r mapdata2) = r"
33  "Arch.capUntypedPtr (ARM_H.PageDirectoryCap r mapdata3) = r"
34  by (auto simp: capUntypedPtr_def
35                 ARM_H.capUntypedPtr_def)
36
37lemma rights_mask_map_UNIV [simp]:
38  "rights_mask_map UNIV = allRights"
39  by (simp add: rights_mask_map_def allRights_def)
40
41declare insert_UNIV[simp]
42
43lemma maskCapRights_allRights [simp]:
44  "maskCapRights allRights c = c"
45  unfolding maskCapRights_def isCap_defs allRights_def
46            ARM_H.maskCapRights_def maskVMRights_def
47  by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split)
48
49lemma diminished_refl'[simp]:
50  "diminished' cap cap"
51  unfolding diminished'_def
52  by (rule exI[where x=allRights], simp)
53
54lemma getCTE_inv [wp]: "\<lbrace>P\<rbrace> getCTE addr \<lbrace>\<lambda>rv. P\<rbrace>"
55  by (simp add: getCTE_def) wp
56
57lemma getEndpoint_inv [wp]:
58  "\<lbrace>P\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv. P\<rbrace>"
59  by (simp add: getEndpoint_def getObject_inv loadObject_default_inv)
60
61lemma getNotification_inv [wp]:
62  "\<lbrace>P\<rbrace> getNotification ptr \<lbrace>\<lambda>rv. P\<rbrace>"
63  by (simp add: getNotification_def getObject_inv loadObject_default_inv)
64
65lemma getSlotCap_inv [wp]: "\<lbrace>P\<rbrace> getSlotCap addr \<lbrace>\<lambda>rv. P\<rbrace>"
66  by (simp add: getSlotCap_def, wp)
67
68declare resolveAddressBits.simps[simp del]
69
70lemma cap_case_CNodeCap:
71  "(case cap of CNodeCap a b c d \<Rightarrow> P
72         | _ \<Rightarrow> Q)
73      = (if isCNodeCap cap then P else Q)"
74  by (cases cap, simp_all add: isCap_simps)
75
76lemma resolveAddressBits_inv_induct:
77  shows
78  "s \<turnstile> \<lbrace>P\<rbrace>
79     resolveAddressBits cap cref depth
80   \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>"
81proof (induct arbitrary: s rule: resolveAddressBits.induct)
82  case (1 cap fn cref depth)
83  show ?case
84    apply (subst resolveAddressBits.simps)
85    apply (simp add: Let_def split_def cap_case_CNodeCap[unfolded isCap_simps]
86               split del: if_split cong: if_cong)
87    apply (rule hoare_pre_spec_validE)
88     apply ((elim exE | wp_once spec_strengthen_postE[OF "1.hyps"])+,
89              (rule refl conjI | simp add: in_monad split del: if_split)+)
90            apply (wp | simp add: locateSlot_conv split del: if_split
91                      | wp_once hoare_drop_imps)+
92  done
93qed
94
95lemma rab_inv' [wp]:
96  "\<lbrace>P\<rbrace> resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. P\<rbrace>"
97  by (rule validE_valid, rule use_specE', rule resolveAddressBits_inv_induct)
98
99lemmas rab_inv'' [wp] = rab_inv' [folded resolveAddressBits_decl_def]
100
101crunch inv [wp]: lookupCap P
102
103lemma updateObject_cte_inv:
104  "\<lbrace>P\<rbrace> updateObject (cte :: cte) ko x y n \<lbrace>\<lambda>rv. P\<rbrace>"
105  apply (simp add: updateObject_cte)
106  apply (cases ko, simp_all add: typeError_def unless_def
107                      split del: if_split
108                           cong: if_cong)
109   apply (wp | simp)+
110  done
111
112definition
113  "no_mdb cte \<equiv> mdbPrev (cteMDBNode cte) = 0 \<and> mdbNext (cteMDBNode cte) = 0"
114
115lemma mdb_next_update:
116  "m (x \<mapsto> y) \<turnstile> a \<leadsto> b =
117  (if a = x then mdbNext (cteMDBNode y) = b else m \<turnstile> a \<leadsto> b)"
118  by (simp add: mdb_next_rel_def mdb_next_def)
119
120lemma neg_no_loopsI:
121  "m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> no_loops m"
122  unfolding no_loops_def by auto
123
124lemma valid_dlistEp [elim?]:
125  "\<lbrakk> valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0;
126     \<And>cte'. \<lbrakk> m (mdbPrev (cteMDBNode cte)) = Some cte';
127              mdbNext (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
128  P"
129  unfolding valid_dlist_def Let_def by blast
130
131lemma valid_dlistEn [elim?]:
132  "\<lbrakk> valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0;
133     \<And>cte'. \<lbrakk> m (mdbNext (cteMDBNode cte)) = Some cte';
134              mdbPrev (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
135  P"
136  unfolding valid_dlist_def Let_def by blast
137
138lemmas valid_dlistE = valid_dlistEn valid_dlistEp
139
140lemma mdb_next_update_other:
141  "\<lbrakk> m (x \<mapsto> y) \<turnstile> a \<leadsto> b; x \<noteq> a \<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b"
142  by (simp add: mdb_next_rel_def mdb_next_def)
143
144lemma mdb_trancl_update_other:
145  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y"
146  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
147  shows "m \<turnstile> x \<leadsto>\<^sup>+ y"
148  using upd nopath
149proof induct
150  case (base y)
151
152  have "m \<turnstile> x \<leadsto> y"
153  proof (rule mdb_next_update_other)
154    from base show "p \<noteq> x" by clarsimp
155  qed fact+
156
157  thus ?case ..
158next
159  case (step y z)
160  hence ih: "m \<turnstile> x \<leadsto>\<^sup>+ y" by auto
161
162  from ih show ?case
163  proof
164    show "m \<turnstile> y \<leadsto> z"
165    proof (rule mdb_next_update_other)
166      show "p \<noteq> y"
167      proof (cases "x = p")
168        case True thus ?thesis using step.prems by simp
169      next
170        case False thus ?thesis using step.prems ih
171          by - (erule contrapos_nn, rule trancl_into_rtrancl, simp)
172      qed
173    qed fact+
174  qed
175qed
176
177lemma next_unfold':
178  "m \<turnstile> c \<leadsto> y = (\<exists>cte. m c = Some cte \<and> mdbNext (cteMDBNode cte) = y)"
179  unfolding mdb_next_rel_def
180  by (simp add: next_unfold split: option.splits)
181
182lemma no_self_loop_next_noloop:
183  assumes no_loop: "no_loops m"
184  and     lup: "m ptr = Some cte"
185  shows   "mdbNext (cteMDBNode cte) \<noteq> ptr"
186proof -
187  from no_loop have "\<not> m \<turnstile> ptr \<leadsto> ptr"
188    unfolding no_loops_def
189    by - (drule spec, erule contrapos_nn, erule r_into_trancl)
190
191  thus ?thesis using lup
192    by (simp add: next_unfold')
193qed
194
195
196lemma valid_dlistI [intro?]:
197  defines "nxt \<equiv> \<lambda>cte. mdbNext (cteMDBNode cte)"
198  and     "prv \<equiv> \<lambda>cte. mdbPrev (cteMDBNode cte)"
199  assumes r1: "\<And>p cte. \<lbrakk> m p = Some cte; prv cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (prv cte) = Some cte' \<and> nxt cte' = p"
200  and     r2: "\<And>p cte. \<lbrakk> m p = Some cte; nxt cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (nxt cte) = Some cte' \<and> prv cte' = p"
201  shows   "valid_dlist m"
202  unfolding valid_dlist_def
203  by (auto dest: r1 r2 simp: Let_def prv_def nxt_def)
204
205lemma no_loops_tranclE:
206  assumes nl: "no_loops m"
207  and    nxt: "m \<turnstile> x \<leadsto>\<^sup>+ y"
208  shows   "\<not> m \<turnstile> y \<leadsto>\<^sup>* x"
209proof
210  assume "m \<turnstile> y \<leadsto>\<^sup>* x"
211  hence "m \<turnstile> x \<leadsto>\<^sup>+ x" using nxt
212    by simp
213
214  thus False using nl
215    unfolding no_loops_def by auto
216qed
217
218lemma neg_next_rtrancl_trancl:
219  "\<lbrakk> \<not> m \<turnstile> y \<leadsto>\<^sup>* r; m \<turnstile> x \<leadsto> y \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ r"
220  apply (erule contrapos_nn)
221  apply (drule tranclD)
222  apply (clarsimp simp: next_unfold')
223  done
224
225lemma next_trancl_split_tt:
226  assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y"
227  and     p2: "m \<turnstile> x \<leadsto>\<^sup>+ p"
228  and     nm: "\<not> m \<turnstile> p \<leadsto>\<^sup>* y"
229  shows "m \<turnstile> y \<leadsto>\<^sup>* p"
230  using p2 p1 nm
231proof induct
232  case base thus ?case
233    by (clarsimp dest!: tranclD) (drule (1)  next_single_value, simp)
234next
235  case (step q r)
236
237  show ?case
238  proof (cases "q = y")
239    case True thus ?thesis using step
240      by fastforce
241  next
242    case False
243    have "m \<turnstile> y \<leadsto>\<^sup>* q"
244    proof (rule step.hyps)
245      have "\<not> m \<turnstile> q \<leadsto>\<^sup>+ y"
246        by (rule neg_next_rtrancl_trancl) fact+
247      thus "\<not> m \<turnstile> q \<leadsto>\<^sup>* y" using False
248        by (clarsimp dest!: rtranclD)
249    qed fact+
250    thus ?thesis by (rule rtrancl_into_rtrancl) fact+
251  qed
252qed
253
254lemma no_loops_splitat_tt:
255  assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y"
256  and     p2: "m \<turnstile> x \<leadsto>\<^sup>+ p"
257  and     nl: "no_loops m"
258  and  r1: "\<lbrakk> m \<turnstile> p \<leadsto>\<^sup>* y; \<not> m \<turnstile> y \<leadsto>\<^sup>+ p \<rbrakk> \<Longrightarrow> P"
259  and  r2: "\<lbrakk> m \<turnstile> y \<leadsto>\<^sup>* p; \<not> m \<turnstile> p \<leadsto>\<^sup>+ y \<rbrakk> \<Longrightarrow> P"
260  shows "P"
261proof (cases "m \<turnstile> p \<leadsto>\<^sup>* y")
262  case True
263  thus ?thesis
264  proof (rule r1)
265    from nl show "\<not> m \<turnstile> y \<leadsto>\<^sup>+ p"
266    proof (rule contrapos_pn)
267      assume "m \<turnstile> y \<leadsto>\<^sup>+ p"
268      hence "m \<turnstile> p \<leadsto>\<^sup>+ p" using True by simp
269      thus "\<not> no_loops m"
270        by (rule neg_no_loopsI)
271    qed
272  qed
273next
274  case False
275
276  show ?thesis
277  proof (rule r2)
278   from False show "\<not> m \<turnstile> p \<leadsto>\<^sup>+ y"
279     by (rule contrapos_nn) (erule trancl_into_rtrancl)
280
281   show "m \<turnstile> y \<leadsto>\<^sup>* p"
282     by (rule next_trancl_split_tt) fact+
283 qed
284qed
285
286lemma no_loops_next_selfD:
287  "\<lbrakk>no_loops m; m \<turnstile> x \<leadsto> x \<rbrakk> \<Longrightarrow> False"
288   apply (clarsimp simp: next_unfold')
289   apply (drule (1) no_self_loop_next_noloop)
290   apply simp
291   done
292
293lemma no_loops_upd_last:
294  assumes noloop: "no_loops m"
295  and     nxt: "m \<turnstile> x \<leadsto>\<^sup>+ p"
296  shows "m (p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p"
297proof -
298  from noloop nxt have xp: "x \<noteq> p"
299    by (clarsimp dest!: neg_no_loopsI)
300
301  from nxt show ?thesis using xp
302  proof (induct rule: converse_trancl_induct')
303    case (base y)
304    hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> p" using noloop
305      by (auto simp add: mdb_next_update dest!: no_loops_next_selfD)
306    thus ?case ..
307  next
308    case (step y z)
309
310    from noloop step have xp: "z \<noteq> p"
311      by (clarsimp dest!: neg_no_loopsI)
312
313    hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> z" using step
314      by (simp add: mdb_next_update)
315
316    moreover from xp have "m (p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p" using step.hyps assms
317      by (auto simp del: fun_upd_apply)
318    ultimately show ?case by (rule trancl_into_trancl2)
319  qed
320qed
321
322
323lemma no_0_neq [intro?]:
324  "\<lbrakk>m c = Some cte; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> 0"
325  by (auto simp add: no_0_def)
326
327lemma no_0_update:
328  assumes no0: "no_0 m"
329  and     pnz: "p \<noteq> 0"
330  shows "no_0 (m(p \<mapsto> cte))"
331  using no0 pnz unfolding no_0_def by simp
332
333lemma has_loop_update:
334  assumes lp: "m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ c'"
335  and    cn0: "c' \<noteq> 0"
336  and  mnext: "mdbNext (cteMDBNode cte) = 0"
337  and    mn0: "no_0 m"
338  and    pn0: "p \<noteq> 0"
339  shows "m \<turnstile> c \<leadsto>\<^sup>+ c'"
340  using lp cn0
341proof induct
342  case (base y)
343  have "m \<turnstile> c \<leadsto> y"
344  proof (rule mdb_next_update_other)
345    show "p \<noteq> c" using base
346      by (clarsimp intro: contrapos_nn simp: mdb_next_update mnext)
347  qed fact+
348
349  thus ?case ..
350next
351  case (step y z)
352
353  show ?case
354  proof
355    have "y \<noteq> 0" by (rule no_0_lhs [OF _  no_0_update]) fact+
356    thus "m \<turnstile> c \<leadsto>\<^sup>+ y" using step by simp
357  next
358    have "z \<noteq> 0" by fact+
359    hence "p \<noteq> y" using step.hyps mnext
360      by (clarsimp simp: mdb_next_update)
361    thus "m \<turnstile> y \<leadsto> z"
362      by (rule mdb_next_update_other [OF step.hyps(2)])
363  qed
364qed
365
366lemma mdb_rtrancl_update_other:
367  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y"
368  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
369  shows "m \<turnstile> x \<leadsto>\<^sup>* y"
370  using upd
371proof (cases rule: next_rtrancl_tranclE)
372  case eq thus ?thesis by simp
373next
374  case trancl thus ?thesis
375    by (auto intro: trancl_into_rtrancl elim: mdb_trancl_update_other [OF _ nopath])
376qed
377
378lemma mdb_trancl_other_update:
379  assumes upd: "m \<turnstile> x \<leadsto>\<^sup>+ y"
380  and      np: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
381  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y"
382  using upd
383proof induct
384  case (base q)
385  from np have "x \<noteq> p" by clarsimp
386  hence"m (p \<mapsto> cte) \<turnstile> x \<leadsto> q"
387    using base by (simp add: mdb_next_update del: fun_upd_apply)
388  thus ?case ..
389next
390  case (step q r)
391
392  show ?case
393  proof
394    from step.hyps(1) np have "q \<noteq> p"
395      by (auto elim!: contrapos_nn)
396
397    thus x: "m(p \<mapsto> cte) \<turnstile> q \<leadsto> r"
398      using step by (simp add: mdb_next_update del: fun_upd_apply)
399  qed fact+
400qed
401
402lemma mdb_rtrancl_other_update:
403  assumes upd: "m \<turnstile> x \<leadsto>\<^sup>* y"
404  and  nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
405  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y"
406  using upd
407proof (cases rule: next_rtrancl_tranclE)
408  case eq thus ?thesis by simp
409next
410  case trancl thus ?thesis
411    by (auto intro: trancl_into_rtrancl elim: mdb_trancl_other_update [OF _ nopath])
412qed
413
414lemma mdb_chain_0_update:
415  assumes x: "m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0"
416  and    np: "\<not> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* p"
417  assumes p: "p \<noteq> 0"
418  assumes 0: "no_0 m"
419  assumes n: "mdb_chain_0 m"
420  shows "mdb_chain_0 (m(p \<mapsto> cte))"
421   unfolding mdb_chain_0_def
422proof rule
423  fix x
424  assume "x \<in> dom (m(p \<mapsto> cte))"
425  hence x: "x = p \<or> x \<in> dom m" by simp
426
427  have cnxt: "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0"
428    by (rule mdb_rtrancl_other_update) fact+
429
430  from x show "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0"
431  proof
432    assume xp: "x = p"
433    show ?thesis
434    proof (rule rtrancl_into_trancl2 [OF _ cnxt])
435      show "m(p \<mapsto> cte) \<turnstile> x \<leadsto> mdbNext (cteMDBNode cte)" using xp
436        by (simp add: mdb_next_update)
437    qed
438  next
439    assume x: "x \<in> dom m"
440
441    show ?thesis
442    proof (cases "m \<turnstile> x \<leadsto>\<^sup>* p")
443      case False
444      from n have "m \<turnstile> x \<leadsto>\<^sup>+ 0"
445        unfolding mdb_chain_0_def
446        using x by auto
447
448      thus ?thesis
449        by (rule mdb_trancl_other_update) fact+
450    next
451      case True
452      hence "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* p"
453      proof (cases rule: next_rtrancl_tranclE)
454        case eq thus ?thesis by simp
455      next
456        case trancl
457        have "no_loops m" by (rule mdb_chain_0_no_loops) fact+
458        thus ?thesis
459          by (rule trancl_into_rtrancl [OF no_loops_upd_last]) fact+
460      qed
461      moreover
462      have "m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)" by (simp add: mdb_next_update)
463      ultimately show ?thesis using cnxt by simp
464    qed
465  qed
466qed
467
468lemma mdb_chain_0_update_0:
469  assumes x: "mdbNext (cteMDBNode cte) = 0"
470  assumes p: "p \<noteq> 0"
471  assumes 0: "no_0 m"
472  assumes n: "mdb_chain_0 m"
473  shows "mdb_chain_0 (m(p \<mapsto> cte))"
474  using x 0 p
475  apply -
476  apply (rule mdb_chain_0_update [OF _ _ p 0 n])
477  apply (auto elim: next_rtrancl_tranclE dest: no_0_lhs_trancl)
478  done
479
480lemma no_loops_0_update:
481  assumes x: "mdbNext (cteMDBNode cte) = 0"
482  assumes p: "p \<noteq> 0"
483  assumes 0: "no_0 m"
484  assumes n: "no_loops m"
485  shows "no_loops (m(p \<mapsto> cte))"
486  unfolding no_loops_def
487proof (rule, rule contrapos_pn [OF n], rule neg_no_loopsI)
488  fix c
489  assume lp: "m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ c"
490  thus "m \<turnstile> c \<leadsto>\<^sup>+ c"
491  proof (rule has_loop_update)
492    from lp show "c \<noteq> 0" by (rule no_0_lhs_trancl [OF _ no_0_update]) fact+
493  qed fact+
494qed
495
496lemma valid_badges_0_update:
497  assumes nx: "mdbNext (cteMDBNode cte) = 0"
498  assumes pv: "mdbPrev (cteMDBNode cte) = 0"
499  assumes p: "m p = Some cte'"
500  assumes m: "no_mdb cte'"
501  assumes 0: "no_0 m"
502  assumes d: "valid_dlist m"
503  assumes v: "valid_badges m"
504  shows "valid_badges (m(p \<mapsto> cte))"
505proof (unfold valid_badges_def, clarify)
506  fix c c' cap cap' n n'
507  assume c: "(m(p \<mapsto> cte)) c = Some (CTE cap n)"
508  assume c': "(m(p \<mapsto> cte)) c' = Some (CTE cap' n')"
509  assume nxt: "m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'"
510  assume r: "sameRegionAs cap cap'"
511
512  from p 0 have p0: "p \<noteq> 0" by (clarsimp simp: no_0_def)
513
514  from c' p0 0
515  have "c' \<noteq> 0" by (clarsimp simp: no_0_def)
516  with nx nxt
517  have cp: "c \<noteq> p" by (clarsimp simp add: mdb_next_unfold)
518  moreover
519  from pv nx nxt p p0 c d m 0
520  have "c' \<noteq> p"
521    apply clarsimp
522    apply (simp add: mdb_next_unfold split: if_split_asm)
523    apply (erule (1) valid_dlistEn, simp)
524    apply (clarsimp simp: no_mdb_def no_0_def)
525    done
526  moreover
527  with nxt c c' cp
528  have "m \<turnstile> c \<leadsto> c'" by (simp add: mdb_next_unfold)
529  ultimately
530  show "(isEndpointCap cap \<longrightarrow>
531            capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow>
532            capEPBadge cap' \<noteq> 0 \<longrightarrow>
533            mdbFirstBadged n') \<and>
534        (isNotificationCap cap \<longrightarrow>
535            capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow>
536            capNtfnBadge cap' \<noteq> 0 \<longrightarrow>
537            mdbFirstBadged n')"
538    using r c c' v by (fastforce simp: valid_badges_def)
539qed
540
541definition
542  "caps_no_overlap' m S \<equiv>
543  \<forall>p c n. m p = Some (CTE c n) \<longrightarrow> capRange c \<inter> S = {}"
544
545definition
546  fresh_virt_cap_class :: "capclass \<Rightarrow> cte_heap \<Rightarrow> bool"
547where
548 "fresh_virt_cap_class C m \<equiv>
549    C \<noteq> PhysicalClass \<longrightarrow> C \<notin> (capClass \<circ> cteCap) ` ran m"
550
551lemma fresh_virt_cap_class_Physical[simp]:
552  "fresh_virt_cap_class PhysicalClass = \<top>"
553  by (rule ext, simp add: fresh_virt_cap_class_def)+
554
555lemma fresh_virt_cap_classD:
556  "\<lbrakk> m x = Some cte; fresh_virt_cap_class C m \<rbrakk>
557     \<Longrightarrow> C \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap cte) \<noteq> C"
558  by (auto simp: fresh_virt_cap_class_def)
559
560lemma capRange_untyped:
561  "capRange cap' \<inter> untypedRange cap \<noteq> {} \<Longrightarrow> isUntypedCap cap"
562  by (cases cap, auto simp: isCap_simps)
563
564lemma capRange_of_untyped [simp]:
565  "capRange (UntypedCap d r n f) = untypedRange (UntypedCap d r n f)"
566  by (simp add: capRange_def isCap_simps capUntypedSize_def)
567
568lemma caps_contained_no_overlap:
569  "\<lbrakk> caps_no_overlap' m (capRange cap); caps_contained' m\<rbrakk>
570    \<Longrightarrow> caps_contained' (m(p \<mapsto> CTE cap n))"
571  apply (clarsimp simp add: caps_contained'_def)
572  apply (rule conjI)
573   apply clarsimp
574   apply (rule conjI, clarsimp dest!: capRange_untyped)
575   apply clarsimp
576   apply (simp add: caps_no_overlap'_def)
577   apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI)
578   apply (frule capRange_untyped)
579   apply (clarsimp simp add: isCap_simps)
580  apply clarsimp
581  apply (simp add: caps_no_overlap'_def)
582  apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI)
583  apply (frule capRange_untyped)
584  apply (clarsimp simp: isCap_simps)
585  apply blast
586  done
587
588lemma no_mdb_next:
589  "\<lbrakk> m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto> p"
590  apply clarsimp
591  apply (frule vdlist_nextD0)
592    apply clarsimp
593   apply assumption
594  apply (clarsimp simp: mdb_prev_def no_mdb_def mdb_next_unfold)
595  done
596
597lemma no_mdb_rtrancl:
598  "\<lbrakk> m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>* p"
599  apply (clarsimp dest!: rtranclD)
600  apply (drule tranclD2)
601  apply clarsimp
602  apply (drule (3) no_mdb_next)
603  apply fastforce
604  done
605
606lemma isNullCap [simp]:
607  "isNullCap cap = (cap = NullCap)"
608  by (simp add: isCap_simps)
609
610lemma isDomainCap [simp]:
611  "isDomainCap cap = (cap = DomainCap)"
612  by (simp add: isCap_simps)
613
614lemma isPhysicalCap[simp]:
615  "isPhysicalCap cap = (capClass cap = PhysicalClass)"
616  by (simp add: isPhysicalCap_def ARM_H.isPhysicalCap_def
617         split: capability.split arch_capability.split)
618
619definition
620  capMasterCap :: "capability \<Rightarrow> capability"
621where
622 "capMasterCap cap \<equiv> case cap of
623   EndpointCap ref bdg s r g \<Rightarrow> EndpointCap ref 0 True True True
624 | NotificationCap ref bdg s r \<Rightarrow> NotificationCap ref 0 True True
625 | CNodeCap ref bits gd gs \<Rightarrow> CNodeCap ref bits 0 0
626 | ThreadCap ref \<Rightarrow> ThreadCap ref
627 | ReplyCap ref master \<Rightarrow> ReplyCap ref True
628 | UntypedCap d ref n f \<Rightarrow> UntypedCap d ref n 0
629 | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of
630      PageCap d ref rghts sz mapdata \<Rightarrow>
631         PageCap d ref VMReadWrite sz None
632    | ASIDPoolCap pool asid \<Rightarrow>
633         ASIDPoolCap pool 0
634    | PageTableCap ptr data \<Rightarrow>
635         PageTableCap ptr None
636    | PageDirectoryCap ptr data \<Rightarrow>
637         PageDirectoryCap ptr None
638    | _ \<Rightarrow> acap)
639 | _ \<Rightarrow> cap"
640
641lemma capMasterCap_simps[simp]:
642  "capMasterCap (EndpointCap ref bdg s r g) = EndpointCap ref 0 True True True"
643  "capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True"
644  "capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0"
645  "capMasterCap (ThreadCap ref) = ThreadCap ref"
646  "capMasterCap capability.NullCap = capability.NullCap"
647  "capMasterCap capability.DomainCap = capability.DomainCap"
648  "capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq"
649  "capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n"
650  "capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) =
651            capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0)"
652  "capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) =
653         capability.ArchObjectCap arch_capability.ASIDControlCap"
654  "capMasterCap (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size pdata)) =
655            capability.ArchObjectCap (arch_capability.PageCap d word VMReadWrite vmpage_size None)"
656  "capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) =
657            capability.ArchObjectCap (arch_capability.PageTableCap word None)"
658  "capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) =
659            capability.ArchObjectCap (arch_capability.PageDirectoryCap word None)"
660  "capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0"
661  "capMasterCap capability.IRQControlCap = capability.IRQControlCap"
662  "capMasterCap (capability.ReplyCap word m) = capability.ReplyCap word True"
663  by (simp_all add: capMasterCap_def)
664
665lemma capMasterCap_eqDs1:
666  "capMasterCap cap = EndpointCap ref bdg s r g
667     \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g
668          \<and> (\<exists>bdg s r g. cap = EndpointCap ref bdg s r g)"
669  "capMasterCap cap = NotificationCap ref bdg s r
670     \<Longrightarrow> bdg = 0 \<and> s \<and> r
671          \<and> (\<exists>bdg s r. cap = NotificationCap ref bdg s r)"
672  "capMasterCap cap = CNodeCap ref bits gd gs
673     \<Longrightarrow> gd = 0 \<and> gs = 0 \<and> (\<exists>gd gs. cap = CNodeCap ref bits gd gs)"
674  "capMasterCap cap = ThreadCap ref
675     \<Longrightarrow> cap = ThreadCap ref"
676  "capMasterCap cap = NullCap
677     \<Longrightarrow> cap = NullCap"
678  "capMasterCap cap = DomainCap
679     \<Longrightarrow> cap = DomainCap"
680  "capMasterCap cap = IRQControlCap
681     \<Longrightarrow> cap = IRQControlCap"
682  "capMasterCap cap = IRQHandlerCap irq
683     \<Longrightarrow> cap = IRQHandlerCap irq"
684  "capMasterCap cap = Zombie ref tp n
685     \<Longrightarrow> cap = Zombie ref tp n"
686  "capMasterCap cap = UntypedCap d ref bits 0
687     \<Longrightarrow> \<exists>f. cap = UntypedCap d ref bits f"
688  "capMasterCap cap = ReplyCap ref master
689     \<Longrightarrow> \<exists>master. cap = ReplyCap ref master"
690  "capMasterCap cap = ArchObjectCap (PageCap d ref rghts sz mapdata)
691     \<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None
692          \<and> (\<exists>rghts mapdata. cap = ArchObjectCap (PageCap d ref rghts sz mapdata))"
693  "capMasterCap cap = ArchObjectCap ASIDControlCap
694     \<Longrightarrow> cap = ArchObjectCap ASIDControlCap"
695  "capMasterCap cap = ArchObjectCap (ASIDPoolCap pool asid)
696     \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = ArchObjectCap (ASIDPoolCap pool asid))"
697  "capMasterCap cap = ArchObjectCap (PageTableCap ptr data)
698     \<Longrightarrow> data = None \<and> (\<exists>data. cap = ArchObjectCap (PageTableCap ptr data))"
699  "capMasterCap cap = ArchObjectCap (PageDirectoryCap ptr data2)
700     \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = ArchObjectCap (PageDirectoryCap ptr data2))"
701  by (clarsimp simp: capMasterCap_def
702              split: capability.split_asm arch_capability.split_asm)+
703
704lemmas capMasterCap_eqDs[dest!] = capMasterCap_eqDs1 capMasterCap_eqDs1 [OF sym]
705
706definition
707  capBadge :: "capability \<Rightarrow> word32 option"
708where
709 "capBadge cap \<equiv> if isEndpointCap cap then Some (capEPBadge cap)
710                 else if isNotificationCap cap then Some (capNtfnBadge cap)
711                 else None"
712
713lemma capBadge_simps[simp]:
714 "capBadge (UntypedCap d p n f)                 = None"
715 "capBadge (NullCap)                          = None"
716 "capBadge (DomainCap)                        = None"
717 "capBadge (EndpointCap ref badge s r w)      = Some badge"
718 "capBadge (NotificationCap ref badge s r)   = Some badge"
719 "capBadge (CNodeCap ref bits gd gs)          = None"
720 "capBadge (ThreadCap ref)                    = None"
721 "capBadge (Zombie ref b n)                   = None"
722 "capBadge (ArchObjectCap cap)                = None"
723 "capBadge (IRQControlCap)                    = None"
724 "capBadge (IRQHandlerCap irq)                = None"
725 "capBadge (ReplyCap tcb master)              = None"
726  by (simp add: capBadge_def isCap_defs)+
727
728lemma capClass_Master:
729  "capClass (capMasterCap cap) = capClass cap"
730  by (simp add: capMasterCap_def split: capability.split arch_capability.split)
731
732lemma capRange_Master:
733  "capRange (capMasterCap cap) = capRange cap"
734  by (simp add: capMasterCap_def split: capability.split arch_capability.split,
735      simp add: capRange_def)
736
737lemma master_eqI:
738  "\<lbrakk> \<And>cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap') \<rbrakk>
739     \<Longrightarrow> F cap = F cap'"
740  by simp
741
742lemma isCap_Master:
743  "isZombie (capMasterCap cap) = isZombie cap"
744  "isArchObjectCap (capMasterCap cap) = isArchObjectCap cap"
745  "isThreadCap (capMasterCap cap) = isThreadCap cap"
746  "isCNodeCap (capMasterCap cap) = isCNodeCap cap"
747  "isNotificationCap (capMasterCap cap) = isNotificationCap cap"
748  "isEndpointCap (capMasterCap cap) = isEndpointCap cap"
749  "isUntypedCap (capMasterCap cap) = isUntypedCap cap"
750  "isReplyCap (capMasterCap cap) = isReplyCap cap"
751  "isIRQControlCap (capMasterCap cap) = isIRQControlCap cap"
752  "isIRQHandlerCap (capMasterCap cap) = isIRQHandlerCap cap"
753  "isNullCap (capMasterCap cap) = isNullCap cap"
754  "isDomainCap (capMasterCap cap) = isDomainCap cap"
755  "isArchPageCap (capMasterCap cap) = isArchPageCap cap"
756  by (simp add: isCap_simps capMasterCap_def
757         split: capability.split arch_capability.split)+
758
759lemma capUntypedSize_capBits:
760  "capClass cap = PhysicalClass \<Longrightarrow> capUntypedSize cap = 2 ^ (capBits cap)"
761  apply (simp add: capUntypedSize_def objBits_simps
762                   ARM_H.capUntypedSize_def
763                   pteBits_def pdeBits_def
764                   ptBits_def pdBits_def
765            split: capability.splits arch_capability.splits
766                   zombie_type.splits)
767  apply fastforce
768  done
769
770lemma sameRegionAs_def2:
771 "sameRegionAs cap cap' = (\<lambda>cap cap'.
772     (cap = cap'
773          \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
774              \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap)
775          \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
776              \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap'))
777      \<or> (capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap
778                 \<and> (isUntypedCap cap \<or> (isArchPageCap cap \<and> isArchPageCap cap')))
779      \<or> (isIRQControlCap cap \<and> isIRQHandlerCap cap'))
780           (capMasterCap cap) (capMasterCap cap')"
781  apply (cases "isUntypedCap cap")
782   apply (clarsimp simp: sameRegionAs_def Let_def
783                         isCap_Master capRange_Master capClass_Master)
784   apply (clarsimp simp: isCap_simps
785                         capMasterCap_def[where cap="UntypedCap d p n f" for d p n f])
786   apply (simp add: capRange_def capUntypedSize_capBits)
787   apply (intro impI iffI)
788    apply (clarsimp del: subsetI intro!: range_subsetI)
789   apply clarsimp
790   apply (simp add: range_subset_eq2)
791  apply (simp cong: conj_cong)
792  apply (simp     add: capMasterCap_def sameRegionAs_def isArchPageCap_def
793                split: capability.split
794            split del: if_split cong: if_cong)
795  apply (simp    add: ARM_H.sameRegionAs_def isCap_simps
796               split: arch_capability.split
797           split del: if_split cong: if_cong)
798  apply (clarsimp simp: capRange_def Let_def)
799  apply (simp add: range_subset_eq2 cong: conj_cong)
800  by (simp add: conj_comms)
801
802lemma sameObjectAs_def2:
803 "sameObjectAs cap cap' = (\<lambda>cap cap'.
804     (cap = cap'
805          \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
806              \<and> \<not> isUntypedCap cap)
807          \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
808              \<and> \<not> isUntypedCap cap')
809          \<and> (isArchPageCap cap \<longrightarrow> capRange cap \<noteq> {})
810          \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})))
811           (capMasterCap cap) (capMasterCap cap')"
812  apply (simp add: sameObjectAs_def sameRegionAs_def2
813                   isCap_simps capMasterCap_def
814            split: capability.split)
815  apply (clarsimp simp: ARM_H.sameObjectAs_def isCap_simps
816                 split: arch_capability.split cong: if_cong)
817  apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps
818             split del: if_split cong: if_cong)
819  apply (simp add: capRange_def)
820  apply fastforce
821  done
822
823lemmas sameRegionAs_def3 =
824  sameRegionAs_def2 [simplified capClass_Master capRange_Master isCap_Master]
825
826lemmas sameObjectAs_def3 =
827  sameObjectAs_def2 [simplified capClass_Master capRange_Master isCap_Master]
828
829lemma sameRegionAsE:
830  "\<lbrakk> sameRegionAs cap cap';
831     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
832         \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk> \<Longrightarrow> R;
833     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap \<rbrakk> \<Longrightarrow> R;
834     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap;
835          isArchPageCap cap' \<rbrakk> \<Longrightarrow> R;
836     \<lbrakk> isIRQControlCap cap; isIRQHandlerCap cap' \<rbrakk> \<Longrightarrow> R
837      \<rbrakk> \<Longrightarrow> R"
838  by (simp add: sameRegionAs_def3, fastforce)
839
840lemma sameObjectAsE:
841  "\<lbrakk> sameObjectAs cap cap';
842     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
843         \<not> isUntypedCap cap;
844         isArchPageCap cap \<Longrightarrow> capRange cap \<noteq> {} \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
845  by (clarsimp simp add: sameObjectAs_def3)
846
847lemma sameObjectAs_sameRegionAs:
848  "sameObjectAs cap cap' \<Longrightarrow> sameRegionAs cap cap'"
849  by (clarsimp simp add: sameObjectAs_def2 sameRegionAs_def2)
850
851lemma sameObjectAs_sym:
852  "sameObjectAs c d = sameObjectAs d c"
853  by (simp add: sameObjectAs_def2 eq_commute conj_comms)
854
855lemma untypedRange_Master:
856  "untypedRange (capMasterCap cap) = untypedRange cap"
857  by (simp add: capMasterCap_def split: capability.split)
858
859lemma sameObject_untypedRange:
860  "sameObjectAs cap cap' \<Longrightarrow> untypedRange cap' = untypedRange cap"
861  apply (rule master_eqI, rule untypedRange_Master)
862  apply (clarsimp simp: sameObjectAs_def2)
863  done
864
865lemma sameObject_untypedCap:
866  "sameObjectAs cap cap' \<Longrightarrow> isUntypedCap cap' = isUntypedCap cap"
867  apply (rule master_eqI, rule isCap_Master)
868  apply (clarsimp simp: sameObjectAs_def2)
869  done
870
871lemma sameObject_capRange:
872  "sameObjectAs cap cap' \<Longrightarrow> capRange cap' = capRange cap"
873  apply (rule master_eqI, rule capRange_Master)
874  apply (clarsimp simp: sameObjectAs_def2)
875  done
876
877lemma sameRegionAs_Null [simp]:
878  "sameRegionAs c NullCap = False"
879  "sameRegionAs NullCap c = False"
880  by (simp add: sameRegionAs_def3 capRange_def isCap_simps)+
881
882lemma isMDBParent_Null [simp]:
883  "isMDBParentOf c (CTE NullCap m) = False"
884  "isMDBParentOf (CTE NullCap m) c = False"
885  unfolding isMDBParentOf_def by (auto split: cte.splits)
886
887lemma capUntypedSize_simps [simp]:
888  "capUntypedSize (ThreadCap r) = 1 << objBits (undefined::tcb)"
889  "capUntypedSize (NotificationCap r badge a b) = 1 << objBits (undefined::Structures_H.notification)"
890  "capUntypedSize (EndpointCap r badge a b c) = 1 << objBits (undefined::endpoint)"
891  "capUntypedSize (Zombie r zs n) = 1 << (zBits zs)"
892  "capUntypedSize NullCap = 0"
893  "capUntypedSize DomainCap = 1"
894  "capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x"
895  "capUntypedSize (UntypedCap d r n f) = 1 << n"
896  "capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)"
897  "capUntypedSize (ReplyCap r m) = 1 << objBits (undefined :: tcb)"
898  "capUntypedSize IRQControlCap = 1"
899  "capUntypedSize (IRQHandlerCap irq) = 1"
900  by (auto simp add: capUntypedSize_def isCap_simps objBits_simps
901              split: zombie_type.splits)
902
903lemma sameRegionAs_classes:
904  "\<lbrakk> sameRegionAs cap cap' \<rbrakk> \<Longrightarrow> capClass cap = capClass cap'"
905  apply (erule sameRegionAsE)
906      apply (rule master_eqI, rule capClass_Master)
907      apply simp
908     apply (simp add: capRange_def split: if_split_asm)
909    apply (clarsimp simp: isCap_simps)
910   apply (clarsimp simp: isCap_simps)
911  done
912
913lemma sameRegionAs_capRange:
914  "\<lbrakk> sameRegionAs cap cap';
915     \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk>
916      \<Longrightarrow> capRange cap = capRange cap'"
917  apply (rule master_eqI, rule capRange_Master)
918  apply (erule sameRegionAsE, simp_all)
919  apply (clarsimp simp: isCap_simps)
920  apply (simp add: capRange_def capMasterCap_def)
921  done
922
923lemma capAligned_capUntypedPtr:
924  "\<lbrakk> capAligned cap; capClass cap = PhysicalClass \<rbrakk> \<Longrightarrow>
925   capUntypedPtr cap \<in> capRange cap"
926  by (simp add: capRange_def capAligned_def is_aligned_no_overflow)
927
928lemma sameRegionAs_capRange_Int:
929  "\<lbrakk> sameRegionAs cap cap'; capClass cap = PhysicalClass \<or> capClass cap' = PhysicalClass;
930     capAligned cap; capAligned cap' \<rbrakk>
931     \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}"
932  apply (frule sameRegionAs_classes, simp)
933  apply (drule(1) capAligned_capUntypedPtr)+
934  apply (erule sameRegionAsE)
935      apply (subgoal_tac "capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}")
936       apply (simp(no_asm_use) add: capRange_Master)
937      apply (clarsimp simp: capRange_Master)
938     apply blast
939    apply blast
940   apply (clarsimp simp: isCap_simps)
941  done
942
943lemma sameRegionAs_trans:
944  "\<lbrakk> sameRegionAs a b; sameRegionAs b c \<rbrakk> \<Longrightarrow> sameRegionAs a c"
945  apply (simp add: sameRegionAs_def2, elim conjE disjE, simp_all)
946         apply (auto simp: isCap_simps)
947    apply (auto simp: capRange_def)
948  done
949
950lemma capMasterCap_maskCapRights[simp]:
951  "capMasterCap (maskCapRights msk cap)
952    = capMasterCap cap"
953  apply (cases cap;
954         simp add: maskCapRights_def Let_def isCap_simps capMasterCap_def)
955  apply (rename_tac arch_capability)
956  apply (case_tac arch_capability;
957         simp add: ARM_H.maskCapRights_def Let_def isCap_simps)
958  done
959
960lemma capBadge_maskCapRights[simp]:
961  "capBadge (maskCapRights msk cap)
962    = capBadge cap"
963  apply (cases cap;
964         simp add: maskCapRights_def Let_def isCap_simps capBadge_def)
965  apply (rename_tac arch_capability)
966  apply (case_tac arch_capability;
967         simp add: ARM_H.maskCapRights_def Let_def isCap_simps)
968  done
969
970lemma maskCapRights_region [simp]:
971  "sameRegionAs (maskCapRights R cap) cap' = sameRegionAs cap cap'"
972  by (simp add: sameRegionAs_def2)
973
974lemma sameRegionAs_mask2 [simp]:
975  "sameRegionAs cap (maskCapRights R cap') = sameRegionAs cap cap'"
976  by (simp add: sameRegionAs_def2)
977
978lemma getObject_cte_det:
979  "(r::cte,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s"
980  apply (clarsimp simp add: getObject_def bind_def get_def gets_def
981                            return_def loadObject_cte split_def)
982  apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm
983                   simp: in_monad typeError_def alignError_def magnitudeCheck_def)
984       apply (simp_all add: bind_def return_def assert_opt_def split_def
985                            alignCheck_def is_aligned_mask[symmetric]
986                            unless_def when_def magnitudeCheck_def)
987  done
988
989lemma cte_wp_at_obj_cases':
990  "cte_wp_at' P p s =
991    (obj_at' P p s \<or> (\<exists>n \<in> dom tcb_cte_cases. obj_at' (P \<circ> (fst (the (tcb_cte_cases n)))) (p - n) s))"
992  apply (simp add: cte_wp_at_cases' obj_at'_def)
993  apply (rule iffI)
994   apply (erule disjEI
995           | clarsimp simp: objBits_simps' cte_level_bits_def projectKOs
996           | rule rev_bexI, erule domI)+
997  apply fastforce
998  done
999
1000lemma cte_wp_at_valid_objs_valid_cap':
1001  "\<lbrakk> cte_wp_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> s \<turnstile>' (cteCap cte)"
1002  apply (simp add: cte_wp_at_obj_cases')
1003  apply (elim disjE bexE conjE)
1004   apply (drule(1) obj_at_valid_objs')
1005   apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def)
1006  apply (drule(1) obj_at_valid_objs')
1007  apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def valid_tcb'_def)
1008  apply (fastforce dest: bspec [OF _ ranI])
1009  done
1010
1011lemma getCTE_valid_cap:
1012  "\<lbrace>valid_objs'\<rbrace> getCTE t \<lbrace>\<lambda>cte s. s \<turnstile>' (cteCap cte) \<and> cte_at' t s\<rbrace>"
1013  apply (clarsimp simp add: getCTE_def valid_def)
1014  apply (frule in_inv_by_hoareD [OF getObject_cte_inv], clarsimp)
1015  apply (subst conj_commute)
1016  apply (subgoal_tac "cte_wp_at' ((=) a) t s")
1017   apply (rule conjI)
1018    apply (clarsimp elim!: cte_wp_at_weakenE')
1019   apply (drule(1) cte_wp_at_valid_objs_valid_cap')
1020   apply clarsimp
1021  apply (drule getObject_cte_det)
1022  apply (simp add: cte_wp_at'_def)
1023  done
1024
1025lemmas getCTE_valid_cap' [wp] =
1026  getCTE_valid_cap [THEN hoare_conjD1 [unfolded pred_conj_def]]
1027
1028lemma ctes_of_valid_cap':
1029  "\<lbrakk> ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' c"
1030  apply (rule cte_wp_at_valid_objs_valid_cap'[where P="(=) (CTE c n)", simplified])
1031   apply (simp add: cte_wp_at_ctes_of)
1032  apply assumption
1033  done
1034
1035lemma valid_capAligned:
1036  "valid_cap' c s \<Longrightarrow> capAligned c"
1037  by (simp add: valid_cap'_def)
1038
1039lemma capUntypedSize_range:
1040  "\<lbrakk> capAligned cap; capClass cap = PhysicalClass \<rbrakk> \<Longrightarrow>
1041   {capUntypedPtr cap .. capUntypedPtr cap + capUntypedSize cap - 1}
1042            \<subseteq> {capUntypedPtr cap .. capUntypedPtr cap + 2 ^ capBits cap - 1}"
1043  apply (rule range_subsetI)
1044   apply simp
1045  apply (clarsimp simp add: capAligned_def)
1046  apply (erule is_aligned_get_word_bits)
1047   apply (simp add: capUntypedSize_def ARM_H.capUntypedSize_def objBits_simps
1048                 isCap_simps
1049          split: capability.splits arch_capability.split
1050                 zombie_type.splits)
1051   apply (auto simp: is_aligned_no_overflow objBits_simps word_bits_def
1052                     ptBits_def pteBits_def
1053                     pdBits_def pdeBits_def)
1054  done
1055
1056lemma caps_no_overlap'_no_region:
1057  "\<lbrakk> caps_no_overlap' m (capRange cap); valid_objs' s;
1058    m = ctes_of s; s \<turnstile>' cap; fresh_virt_cap_class (capClass cap) m \<rbrakk> \<Longrightarrow>
1059  \<forall>c n p. m p = Some (CTE c n) \<longrightarrow>
1060         \<not> sameRegionAs c cap \<and> \<not> sameRegionAs cap c"
1061  apply (clarsimp simp add: caps_no_overlap'_def)
1062  apply (erule allE)+
1063  apply (erule impE, erule exI)
1064  apply (frule (1) ctes_of_valid_cap')
1065  apply (drule valid_capAligned)+
1066  apply (case_tac "capClass cap = PhysicalClass")
1067   apply (auto dest: sameRegionAs_capRange_Int)[1]
1068  apply (drule(1) fresh_virt_cap_classD)
1069  apply (auto dest: sameRegionAs_classes)
1070  done
1071
1072definition
1073 "initMDBNode \<equiv> MDB nullPointer nullPointer True True"
1074
1075lemma init_next [simp]:
1076  "mdbNext initMDBNode = 0"
1077  by (simp add: initMDBNode_def nullPointer_def)
1078
1079lemma init_prev [simp]:
1080  "mdbPrev initMDBNode = 0"
1081  by (simp add: initMDBNode_def nullPointer_def)
1082
1083lemma mdb_chunked_init:
1084  assumes x: "m x = Some cte"
1085  assumes no_m: "no_mdb cte"
1086  assumes no_c: "caps_no_overlap' m (capRange cap)"
1087  assumes no_v: "fresh_virt_cap_class (capClass cap) m"
1088  assumes no_0: "no_0 m"
1089  assumes dlist: "valid_dlist m"
1090  assumes chain: "mdb_chain_0 m"
1091  assumes chunked: "mdb_chunked m"
1092  assumes valid: "valid_objs' s" "m = ctes_of s" "s \<turnstile>' cap"
1093  shows "mdb_chunked (m(x \<mapsto> CTE cap initMDBNode))"
1094  unfolding mdb_chunked_def
1095proof clarify
1096  fix p p' c c' n n'
1097  define m' where "m' \<equiv> m (x \<mapsto> CTE cap initMDBNode)"
1098  assume p: "m' p = Some (CTE c n)"
1099  assume p': "m' p' = Some (CTE c' n')"
1100  assume r: "sameRegionAs c c'"
1101  assume neq: "p \<noteq> p'"
1102
1103  note no_region = caps_no_overlap'_no_region [OF no_c valid no_v]
1104
1105  from chain x no_0
1106  have chain': "mdb_chain_0 m'"
1107    unfolding m'_def
1108    apply -
1109    apply (rule mdb_chain_0_update, clarsimp)
1110       apply clarsimp
1111       apply (drule rtranclD)
1112       apply (erule disjE, clarsimp)
1113       apply clarsimp
1114       apply (drule tranclD)
1115       apply (clarsimp simp: mdb_next_unfold)
1116      apply clarsimp
1117     apply assumption
1118    apply assumption
1119    done
1120  moreover
1121  from x no_0
1122  have x0 [simp]: "x \<noteq> 0" by clarsimp
1123  with no_0
1124  have "no_0 m'"
1125    unfolding m'_def
1126    by (rule no_0_update)
1127  ultimately
1128  have nl: "no_loops m'" by (rule mdb_chain_0_no_loops)
1129
1130  from p p' r neq no_region
1131  have px: "p \<noteq> x"
1132    by (clarsimp simp: m'_def) blast
1133  moreover
1134  from p p' r neq no_region
1135  have p'x: "p' \<noteq> x"
1136    by (clarsimp simp: m'_def) blast
1137  ultimately
1138  have m:
1139   "(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
1140    (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and>
1141    (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)"
1142    using chunked p p' neq r
1143    unfolding mdb_chunked_def m'_def
1144    by simp
1145
1146  from x no_m px [symmetric] dlist no_0
1147  have npx: "\<not> m \<turnstile> p \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
1148
1149  from x no_m p'x [symmetric] dlist no_0
1150  have np'x: "\<not> m \<turnstile> p' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
1151
1152  show "(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
1153        (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and>
1154        (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)"
1155  proof (cases "m \<turnstile> p \<leadsto>\<^sup>+ p'")
1156    case True
1157    with m
1158    have ch: "is_chunk m c p p'" by simp
1159
1160    from True npx
1161    have "m' \<turnstile> p \<leadsto>\<^sup>+ p'"
1162      unfolding m'_def
1163      by (rule mdb_trancl_other_update)
1164    moreover
1165    with nl
1166    have "\<not> m' \<turnstile> p' \<leadsto>\<^sup>+ p"
1167      apply clarsimp
1168      apply (drule (1) trancl_trans)
1169      apply (simp add: no_loops_def)
1170      done
1171    moreover
1172    have "is_chunk m' c p p'"
1173      unfolding is_chunk_def
1174    proof clarify
1175      fix p''
1176      assume "m' \<turnstile> p \<leadsto>\<^sup>+ p''"
1177      with npx
1178      have "m \<turnstile> p \<leadsto>\<^sup>+ p''"
1179        unfolding m'_def
1180        by - (rule mdb_trancl_update_other)
1181      moreover
1182      then
1183      have p''x: "p'' \<noteq> x"
1184        using dlist x no_m no_0
1185        apply clarsimp
1186        apply (drule tranclD2)
1187        apply clarsimp
1188        apply (frule vdlist_nextD0, simp, assumption)
1189        apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def)
1190        done
1191      moreover
1192      assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p'"
1193      {
1194        moreover
1195        from x no_m p''x [symmetric] dlist no_0
1196        have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
1197        ultimately
1198        have "m \<turnstile> p'' \<leadsto>\<^sup>* p'"
1199          unfolding m'_def
1200          by (rule mdb_rtrancl_update_other)
1201      }
1202      ultimately
1203      have "\<exists>cap'' n''.
1204            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''"
1205        using ch
1206        by (simp add: is_chunk_def)
1207      with p''x
1208      show "\<exists>cap'' n''.
1209             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''"
1210        by (simp add: m'_def)
1211    qed
1212    ultimately
1213    show ?thesis by simp
1214  next
1215    case False
1216    with m
1217    have p'p: "m \<turnstile> p' \<leadsto>\<^sup>+ p" by simp
1218    with m
1219    have ch: "is_chunk m c' p' p" by simp
1220    from p'p np'x
1221    have "m' \<turnstile> p' \<leadsto>\<^sup>+ p"
1222      unfolding m'_def
1223      by (rule mdb_trancl_other_update)
1224    moreover
1225    with nl
1226    have "\<not> m' \<turnstile> p \<leadsto>\<^sup>+ p'"
1227      apply clarsimp
1228      apply (drule (1) trancl_trans)
1229      apply (simp add: no_loops_def)
1230      done
1231    moreover
1232    have "is_chunk m' c' p' p"
1233      unfolding is_chunk_def
1234    proof clarify
1235      fix p''
1236      assume "m' \<turnstile> p' \<leadsto>\<^sup>+ p''"
1237      with np'x
1238      have "m \<turnstile> p' \<leadsto>\<^sup>+ p''"
1239        unfolding m'_def
1240        by - (rule mdb_trancl_update_other)
1241      moreover
1242      then
1243      have p''x: "p'' \<noteq> x"
1244        using dlist x no_m no_0
1245        apply clarsimp
1246        apply (drule tranclD2)
1247        apply clarsimp
1248        apply (frule vdlist_nextD0, simp, assumption)
1249        apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def)
1250        done
1251      moreover
1252      assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p"
1253      {
1254        moreover
1255        from x no_m p''x [symmetric] dlist no_0
1256        have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
1257        ultimately
1258        have "m \<turnstile> p'' \<leadsto>\<^sup>* p"
1259          unfolding m'_def
1260          by (rule mdb_rtrancl_update_other)
1261      }
1262      ultimately
1263      have "\<exists>cap'' n''.
1264            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''"
1265        using ch
1266        by (simp add: is_chunk_def)
1267      with p''x
1268      show "\<exists>cap'' n''.
1269             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''"
1270        by (simp add: m'_def)
1271    qed
1272    ultimately
1273    show ?thesis by simp
1274  qed
1275qed
1276
1277lemma cte_refs_capRange:
1278  "\<lbrakk> s \<turnstile>' c; \<forall>irq. c \<noteq> IRQHandlerCap irq \<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> capRange c"
1279  apply (cases c; simp add: capRange_def isCap_simps)
1280    apply (clarsimp dest!: valid_capAligned
1281                    simp: capAligned_def objBits_simps field_simps)
1282    apply (frule tcb_cte_cases_small)
1283    apply (intro conjI)
1284     apply (erule(1) is_aligned_no_wrap')
1285    apply (rule word_plus_mono_right[where z="2^tcbBlockSizeBits - 1", simplified field_simps])
1286     apply (drule minus_one_helper3, simp)
1287    apply (erule is_aligned_no_wrap'[where off="2^tcbBlockSizeBits - 1", simplified field_simps])
1288    apply (drule minus_one_helper3)
1289    apply simp
1290   defer
1291   \<comment> \<open>CNodeCap\<close>
1292   apply (clarsimp simp: objBits_simps capAligned_def dest!: valid_capAligned)
1293   apply (rename_tac word1 nat1 word2 nat2 x)
1294   apply (subgoal_tac "x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)")
1295    apply (intro conjI)
1296     apply (erule(1) is_aligned_no_wrap')
1297    apply (simp add: add_diff_eq[symmetric])
1298    apply (rule word_plus_mono_right)
1299     apply simp
1300    apply (erule is_aligned_no_wrap')
1301    apply simp
1302   apply (simp add: power_add field_simps)
1303   apply (erule word_mult_less_mono1)
1304    apply (simp add: objBits_defs)
1305   apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z])
1306    apply simp
1307   apply (simp only: power_add)
1308   apply (simp add: word_bits_def)
1309  \<comment> \<open>Zombie\<close>
1310  apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps)
1311  apply (rename_tac word zombie_type nat x)
1312  apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ zBits zombie_type")
1313   apply (intro conjI)
1314    apply (erule(1) is_aligned_no_wrap')
1315   apply (simp add: add_diff_eq[symmetric])
1316   apply (rule word_plus_mono_right)
1317    apply simp
1318   apply (erule is_aligned_no_wrap')
1319   apply simp
1320  apply (case_tac zombie_type)
1321   apply simp
1322   apply (rule div_lt_mult)
1323    apply (simp add: objBits_defs)
1324    apply (erule order_less_le_trans)
1325    apply (simp add: word_le_nat_alt)
1326    apply (subst le_unat_uoi[where z=5])
1327     apply simp
1328    apply simp
1329   apply (simp add: objBits_defs)
1330  apply (simp add: objBits_simps' power_add mult.commute)
1331  apply (rule word_mult_less_mono1)
1332    apply (erule order_less_le_trans)
1333    apply (simp add: word_le_nat_alt)
1334    apply (subst le_unat_uoi)
1335     apply (subst unat_power_lower)
1336      prefer 2
1337      apply assumption
1338     apply (simp add: word_bits_def)
1339    apply (simp add: word_bits_def)
1340   apply simp
1341  apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z])
1342   apply simp
1343  apply (simp only: power_add)
1344  apply (simp add: word_bits_def)
1345  done
1346
1347lemma untypedCapRange:
1348  "isUntypedCap cap \<Longrightarrow> capRange cap = untypedRange cap"
1349  by (clarsimp simp: isCap_simps)
1350
1351lemma no_direct_loop [simp]:
1352  "no_loops m \<Longrightarrow> m (mdbNext node) \<noteq> Some (CTE cap node)"
1353  by (fastforce simp: mdb_next_rel_def mdb_next_def no_loops_def)
1354
1355lemma no_loops_direct_simp:
1356  "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto> x = False"
1357  by (auto simp add: no_loops_def)
1358
1359lemma no_loops_trancl_simp:
1360  "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ x = False"
1361  by (auto simp add: no_loops_def)
1362
1363lemma subtree_mdb_next:
1364  "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ b"
1365  by (erule subtree.induct) (auto simp: mdb_next_rel_def intro: trancl_into_trancl)
1366end
1367
1368context mdb_order
1369begin
1370
1371lemma no_loops: "no_loops m"
1372  using chain no_0 by (rule mdb_chain_0_no_loops)
1373
1374lemma irrefl_direct_simp [iff]:
1375  "m \<turnstile> x \<leadsto> x = False"
1376  using no_loops by (rule no_loops_direct_simp)
1377
1378lemma irrefl_trancl_simp [iff]:
1379  "m \<turnstile> x \<leadsto>\<^sup>+ x = False"
1380  using no_loops by (rule no_loops_trancl_simp)
1381
1382lemma irrefl_rtrancl:
1383  "\<lbrakk> m \<turnstile> x \<leadsto>\<^sup>* y; m \<turnstile> y \<leadsto>\<^sup>* x \<rbrakk> \<Longrightarrow> x = y"
1384  by (fastforce dest: rtranclD trancl_trans)
1385
1386lemma irrefl_subtree [iff]:
1387  "m \<turnstile> x \<rightarrow> x = False"
1388  by (clarsimp dest!: subtree_mdb_next)
1389
1390end (* of context mdb_order *)
1391
1392lemma no_loops_prev_next_0:
1393  fixes m :: cte_heap
1394  assumes src: "m src = Some (CTE src_cap src_node)"
1395  assumes no_loops: "no_loops m"
1396  assumes dlist: "valid_dlist m"
1397  shows "(mdbPrev src_node = mdbNext src_node) =
1398         (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)"
1399proof -
1400  { assume "mdbPrev src_node = mdbNext src_node"
1401    moreover
1402    assume "mdbNext src_node \<noteq> 0"
1403    ultimately
1404    obtain cte where
1405      "m (mdbNext src_node) = Some cte"
1406      "mdbNext (cteMDBNode cte) = src"
1407      using src dlist
1408      by (fastforce simp add: valid_dlist_def Let_def)
1409    hence "m \<turnstile> src \<leadsto>\<^sup>+ src" using src
1410      apply -
1411      apply (rule trancl_trans)
1412       apply (rule r_into_trancl)
1413       apply (simp add: next_unfold')
1414      apply (rule r_into_trancl)
1415      apply (simp add: next_unfold')
1416      done
1417    with no_loops
1418    have False by (simp add: no_loops_def)
1419  }
1420  thus ?thesis by auto blast
1421qed
1422
1423lemma no_loops_next_prev_0:
1424  fixes m :: cte_heap
1425  assumes "m src = Some (CTE src_cap src_node)"
1426  assumes "no_loops m"
1427  assumes "valid_dlist m"
1428  shows "(mdbNext src_node = mdbPrev src_node) =
1429         (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)"
1430  apply (rule iffI)
1431  apply (drule sym)
1432   apply (simp add: no_loops_prev_next_0 [OF assms])
1433  apply clarsimp
1434  done
1435
1436locale vmdb = mdb_next +
1437  assumes valid: "valid_mdb_ctes m"
1438
1439sublocale vmdb < mdb_order
1440  using valid
1441  by (auto simp: greater_def greater_eq_def mdb_order_def valid_mdb_ctes_def)
1442
1443context vmdb
1444begin
1445
1446declare no_0 [intro!]
1447declare no_loops [intro!]
1448
1449lemma dlist [intro!]: "valid_dlist m"
1450  using valid by (simp add: valid_mdb_ctes_def)
1451
1452lemmas m_0_simps [iff] = no_0_simps [OF no_0]
1453
1454lemma prev_next_0_p:
1455  assumes "m p = Some (CTE cap node)"
1456  shows "(mdbPrev node = mdbNext node) =
1457         (mdbPrev node = 0 \<and> mdbNext node = 0)"
1458  using assms by (rule no_loops_prev_next_0) auto
1459
1460lemma next_prev_0_p:
1461  assumes "m p = Some (CTE cap node)"
1462  shows "(mdbNext node = mdbPrev node) =
1463         (mdbPrev node = 0 \<and> mdbNext node = 0)"
1464  using assms by (rule no_loops_next_prev_0) auto
1465
1466lemmas dlistEn = valid_dlistEn [OF dlist]
1467lemmas dlistEp = valid_dlistEp [OF dlist]
1468
1469lemmas dlist_prevD = vdlist_prevD [OF _ _ dlist no_0]
1470lemmas dlist_nextD = vdlist_nextD [OF _ _ dlist no_0]
1471lemmas dlist_prevD0 = vdlist_prevD0 [OF _ _ dlist]
1472lemmas dlist_nextD0 = vdlist_nextD0 [OF _ _ dlist]
1473lemmas dlist_prev_src_unique = vdlist_prev_src_unique [OF _ _ _ dlist]
1474lemmas dlist_next_src_unique = vdlist_next_src_unique [OF _ _ _ dlist]
1475
1476lemma subtree_not_0 [simp]:
1477  "\<not>m \<turnstile> p \<rightarrow> 0"
1478  apply clarsimp
1479  apply (erule subtree.cases)
1480  apply auto
1481  done
1482
1483lemma not_0_subtree [simp]:
1484  "\<not>m \<turnstile> 0 \<rightarrow> p"
1485  apply clarsimp
1486  apply (erule subtree.induct)
1487  apply (auto simp: mdb_next_unfold)
1488  done
1489
1490lemma not_0_next [simp]:
1491  "\<not> m \<turnstile> 0 \<leadsto> p"
1492  by (clarsimp simp: mdb_next_unfold)
1493
1494lemma not_0_trancl [simp]:
1495  "\<not> m \<turnstile> 0 \<leadsto>\<^sup>+ p"
1496  by (clarsimp dest!: tranclD)
1497
1498lemma rtrancl0 [simp]:
1499  "m \<turnstile> 0 \<leadsto>\<^sup>* p = (p = 0)"
1500  by (auto dest!: rtranclD)
1501
1502lemma valid_badges: "valid_badges m"
1503  using valid by (simp add: valid_mdb_ctes_def)
1504
1505lemma nullcaps: "valid_nullcaps m"
1506  using valid by (simp add: valid_mdb_ctes_def)
1507
1508lemma
1509  caps_contained: "caps_contained' m" and
1510  chunked: "mdb_chunked m" and
1511  untyped_mdb: "untyped_mdb' m" and
1512  untyped_inc: "untyped_inc' m" and
1513  class_links: "class_links m" and
1514  irq_control: "irq_control m"
1515  using valid by (simp add: valid_mdb_ctes_def)+
1516
1517lemma zero_next [simp]:
1518  "m \<turnstile> 0 \<leadsto> p' = False"
1519  by (clarsimp simp: mdb_next_unfold)
1520
1521end (* of context vmdb *)
1522
1523lemma no_self_loop_next:
1524  assumes vmdb: "valid_mdb_ctes m"
1525  and     lup: "m ptr = Some cte"
1526  shows   "mdbNext (cteMDBNode cte) \<noteq> ptr"
1527proof -
1528  from vmdb have "no_loops m" ..
1529  thus ?thesis
1530    by (rule no_self_loop_next_noloop) fact+
1531qed
1532
1533lemma no_self_loop_prev:
1534  assumes vmdb: "valid_mdb_ctes m"
1535  and     lup: "m ptr = Some cte"
1536  shows   "mdbPrev (cteMDBNode cte) \<noteq> ptr"
1537proof
1538  assume prev: "mdbPrev (cteMDBNode cte) = ptr"
1539
1540  from vmdb have "no_0 m" ..
1541  with lup have "ptr \<noteq> 0"
1542    by (rule no_0_neq)
1543
1544  moreover have "mdbNext (cteMDBNode cte) \<noteq> ptr"
1545    by (rule no_self_loop_next) fact+
1546
1547  moreover from vmdb have "valid_dlist m" ..
1548
1549  ultimately show False using lup prev
1550    by - (erule (1) valid_dlistEp, simp_all)
1551qed
1552
1553
1554locale mdb_ptr = vmdb +
1555  fixes p cap node
1556  assumes m_p [intro!]: "m p = Some (CTE cap node)"
1557begin
1558
1559lemma p_not_next [simp]:
1560  "(p = mdbNext node) = False"
1561  using valid m_p by (fastforce dest: no_self_loop_next)
1562
1563lemma p_not_prev [simp]:
1564  "(p = mdbPrev node) = False"
1565  using valid m_p by (fastforce dest: no_self_loop_prev)
1566
1567lemmas next_not_p [simp] = p_not_next [THEN x_sym]
1568lemmas prev_not_p [simp] = p_not_prev [THEN x_sym]
1569
1570lemmas prev_next_0 [simp] = prev_next_0_p [OF m_p] next_prev_0_p [OF m_p]
1571
1572lemma p_0 [simp]: "p \<noteq> 0" using m_p by clarsimp
1573
1574lemma p_nextD:
1575  assumes p': "m p' = Some (CTE cap' node')"
1576  assumes eq: "mdbNext node = mdbNext node'"
1577  shows "p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0"
1578proof (cases "mdbNext node = 0")
1579  case True thus ?thesis using eq by simp
1580next
1581  case False
1582  with eq have n': "mdbNext node' \<noteq> 0" by simp
1583
1584  have "p = p'"
1585    apply (rule dlistEn [OF m_p, simplified, OF False])
1586    apply (simp add: eq)
1587    apply (rule dlistEn [OF p', simplified, OF n'])
1588    apply clarsimp
1589    done
1590
1591  thus ?thesis by blast
1592qed
1593
1594lemma p_next_eq:
1595  assumes "m p' = Some (CTE cap' node')"
1596  shows "(mdbNext node = mdbNext node') =
1597         (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0)"
1598  using assms m_p
1599  apply -
1600  apply (rule iffI)
1601   apply (erule (1) p_nextD)
1602  apply auto
1603  done
1604
1605lemma p_prevD:
1606  assumes p': "m p' = Some (CTE cap' node')"
1607  assumes eq: "mdbPrev node = mdbPrev node'"
1608  shows "p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0"
1609proof (cases "mdbPrev node = 0")
1610  case True thus ?thesis using eq by simp
1611next
1612  case False
1613  with eq have n': "mdbPrev node' \<noteq> 0" by simp
1614
1615  have "p = p'"
1616    apply (rule dlistEp [OF m_p, simplified, OF False])
1617    apply (simp add: eq)
1618    apply (rule dlistEp [OF p', simplified, OF n'])
1619    apply clarsimp
1620    done
1621
1622  thus ?thesis by blast
1623qed
1624
1625lemma p_prev_eq:
1626  assumes "m p' = Some (CTE cap' node')"
1627  shows "(mdbPrev node = mdbPrev node') =
1628         (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0)"
1629  using assms m_p
1630  apply -
1631  apply (rule iffI)
1632   apply (erule (1) p_prevD)
1633  apply auto
1634  done
1635
1636lemmas p_prev_qe = p_prev_eq [THEN x_sym]
1637lemmas p_next_qe = p_next_eq [THEN x_sym]
1638
1639lemma m_p_prev [intro!]:
1640  "m \<turnstile> mdbPrev node \<leftarrow> p"
1641  using m_p by (clarsimp simp: mdb_prev_def)
1642
1643lemma m_p_next [intro!]:
1644  "m \<turnstile> p \<leadsto> mdbNext node"
1645  using m_p by (clarsimp simp: mdb_next_unfold)
1646
1647lemma next_p_prev:
1648  "mdbNext node \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext node"
1649  by (rule dlist_nextD0 [OF m_p_next])
1650
1651lemma prev_p_next:
1652  "mdbPrev node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p"
1653  by (rule dlist_prevD0 [OF m_p_prev])
1654
1655lemma p_next:
1656  "(m \<turnstile> p \<leadsto> p') = (p' = mdbNext node)"
1657  using m_p by (auto simp: mdb_next_unfold)
1658
1659end (* of locale mdb_ptr *)
1660
1661lemma no_mdb_not_source:
1662  "no_mdb cte \<Longrightarrow> m \<turnstile> c \<leadsto> c' \<Longrightarrow> m p = Some cte \<Longrightarrow> c = p \<longrightarrow> c' = 0"
1663  by (clarsimp simp add: mdb_next_unfold no_mdb_def)
1664
1665lemma no_mdb_not_target:
1666  "\<lbrakk> m \<turnstile> c \<leadsto> c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk>
1667  \<Longrightarrow> c' \<noteq> p"
1668  apply clarsimp
1669  apply (subgoal_tac "c \<noteq> 0")
1670   prefer 2
1671   apply (clarsimp simp: mdb_next_unfold)
1672  apply (drule (3) vdlist_nextD)
1673  apply (clarsimp simp: mdb_prev_def)
1674  apply (simp add: no_mdb_def)
1675  done
1676
1677context begin interpretation Arch . (*FIXME: arch_split*)
1678lemma valid_dlist_init:
1679  "\<lbrakk> valid_dlist m; m p = Some cte; no_mdb cte \<rbrakk> \<Longrightarrow>
1680  valid_dlist (m (p \<mapsto> CTE cap initMDBNode))"
1681  apply (simp add: initMDBNode_def Let_def nullPointer_def)
1682  apply (clarsimp simp: no_mdb_def valid_dlist_def Let_def)
1683  apply fastforce
1684  done
1685end
1686
1687lemma (in mdb_ptr) descendants_of_init':
1688  assumes n: "no_mdb (CTE cap node)"
1689  shows
1690  "descendants_of' p' (m(p \<mapsto> CTE c initMDBNode)) =
1691   descendants_of' p' m"
1692  apply (rule set_eqI)
1693  apply (simp add: descendants_of'_def)
1694  apply (rule iffI)
1695   apply (erule subtree.induct)
1696    apply (frule no_mdb_not_target [where p=p])
1697        apply simp
1698       apply (simp add: no_mdb_def)
1699      apply (rule valid_dlist_init[OF dlist, OF m_p n])
1700     apply (insert no_0)[1]
1701     apply (clarsimp simp: no_0_def)
1702    apply (clarsimp simp: mdb_next_unfold split: if_split_asm)
1703    apply (rule direct_parent)
1704      apply (clarsimp simp: mdb_next_unfold)
1705     apply assumption
1706    apply (clarsimp simp: parentOf_def split: if_split_asm)
1707   apply (frule no_mdb_not_target [where p=p])
1708       apply simp
1709      apply (simp add: no_mdb_def)
1710     apply (rule valid_dlist_init[OF dlist, OF m_p n])
1711    apply (insert no_0)[1]
1712    apply (clarsimp simp: no_0_def)
1713   apply (subgoal_tac "p' \<noteq> p")
1714    apply (erule trans_parent)
1715      apply (clarsimp simp: mdb_next_unfold split: if_split_asm)
1716     apply assumption
1717    apply (clarsimp simp: parentOf_def m_p split: if_split_asm)
1718   apply clarsimp
1719   apply (drule subtree_mdb_next)+
1720   apply (drule tranclD)+
1721   apply clarsimp
1722   apply (insert n)[1]
1723   apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def)
1724  apply (erule subtree.induct)
1725   apply (frule no_mdb_not_target [where p=p], rule m_p, rule n)
1726     apply (rule dlist)
1727    apply (rule no_0)
1728   apply (subgoal_tac "p'\<noteq>p")
1729    prefer 2
1730    apply (insert n)[1]
1731    apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def)
1732   apply (rule direct_parent)
1733     apply (clarsimp simp: mdb_next_unfold)
1734    apply assumption
1735   apply (clarsimp simp: parentOf_def)
1736  apply (frule no_mdb_not_target [where p=p], rule m_p, rule n)
1737    apply (rule dlist)
1738   apply (rule no_0)
1739  apply (subgoal_tac "c'\<noteq>p")
1740   prefer 2
1741   apply (insert n)[1]
1742   apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def)
1743  apply (subgoal_tac "p'\<noteq>p")
1744   apply (erule trans_parent)
1745     apply (clarsimp simp: mdb_next_unfold)
1746    apply assumption
1747   apply (clarsimp simp: parentOf_def)
1748  apply clarsimp
1749  apply (drule subtree_mdb_next)
1750  apply (drule tranclD)
1751  apply clarsimp
1752  apply (insert n)
1753  apply (clarsimp simp: mdb_next_unfold no_mdb_def m_p)
1754  done
1755
1756lemma untyped_mdb_init:
1757  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
1758     caps_no_overlap' m (capRange cap); untyped_mdb' m;
1759     valid_objs' s; s \<turnstile>' cap;
1760     m = ctes_of s\<rbrakk>
1761    \<Longrightarrow> untyped_mdb' (m(p \<mapsto> CTE cap initMDBNode))"
1762  apply (clarsimp simp add: untyped_mdb'_def)
1763  apply (rule conjI)
1764   apply clarsimp
1765   apply (simp add: caps_no_overlap'_def)
1766   apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI)
1767   apply (drule (1) ctes_of_valid_cap')+
1768   apply (drule valid_capAligned)+
1769   apply (drule untypedCapRange)+
1770   apply simp
1771  apply (cases cte)
1772  apply (rename_tac capability mdbnode)
1773  apply clarsimp
1774  apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode")
1775   prefer 2
1776   apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def)
1777  apply (clarsimp simp: mdb_ptr.descendants_of_init')
1778  apply (simp add: caps_no_overlap'_def)
1779  apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI)
1780  apply (drule (1) ctes_of_valid_cap')+
1781  apply (drule valid_capAligned untypedCapRange)+
1782  apply simp
1783  apply blast
1784  done
1785
1786lemma aligned_untypedRange_non_empty:
1787  "\<lbrakk>capAligned c; isUntypedCap c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {}"
1788  apply (frule untypedCapRange)
1789  apply (drule capAligned_capUntypedPtr)
1790   apply (clarsimp simp: isCap_simps)
1791  apply blast
1792  done
1793
1794lemma untypedRange_not_emptyD: "untypedRange c' \<noteq> {} \<Longrightarrow> isUntypedCap c'"
1795  by (case_tac c'; simp add: isCap_simps)
1796
1797lemma usableRange_subseteq:
1798  "\<lbrakk>capAligned c';isUntypedCap c'\<rbrakk> \<Longrightarrow> usableUntypedRange c' \<subseteq> untypedRange c'"
1799  apply (clarsimp simp:isCap_simps capAligned_def split:if_splits)
1800  apply (erule order_trans[OF is_aligned_no_wrap'])
1801   apply (erule of_nat_power)
1802   apply (simp add:word_bits_def)+
1803 done
1804
1805lemma untypedRange_in_capRange: "untypedRange x \<subseteq> capRange x"
1806  by (case_tac x; simp add: capRange_def)
1807
1808lemma untyped_inc_init:
1809  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
1810     caps_no_overlap' m (capRange cap);
1811     valid_objs' s; s \<turnstile>' cap;
1812     m = ctes_of s\<rbrakk>
1813    \<Longrightarrow> untyped_inc' (m(p \<mapsto> CTE cap initMDBNode))"
1814  apply (clarsimp simp add: valid_mdb_ctes_def untyped_inc'_def)
1815  apply (intro conjI impI)
1816   apply clarsimp
1817   apply (simp add: caps_no_overlap'_def)
1818   apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI)
1819   apply (drule (1) ctes_of_valid_cap')+
1820   apply (drule valid_capAligned)+
1821   apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD])
1822    apply (drule (1) aligned_untypedRange_non_empty)
1823    apply assumption
1824   apply (frule_tac c' = c' in  usableRange_subseteq)
1825    apply (drule (1) aligned_untypedRange_non_empty)
1826    apply assumption
1827   apply (drule(1) aligned_untypedRange_non_empty)+
1828   apply (thin_tac "All P" for P)
1829    apply (subgoal_tac "untypedRange cap \<inter> untypedRange c' = {}")
1830    apply (intro conjI)
1831         apply simp
1832        apply (drule(2) set_inter_not_emptyD2)
1833        apply fastforce
1834       apply (drule(2) set_inter_not_emptyD1)
1835       apply fastforce
1836      apply (drule(2) set_inter_not_emptyD3)
1837      apply simp+
1838   apply (rule disjoint_subset2[OF _ disjoint_subset])
1839     apply (rule untypedRange_in_capRange)+
1840   apply (simp add:Int_ac)
1841  apply clarsimp
1842  apply (cases cte)
1843  apply (rename_tac capability mdbnode)
1844  apply clarsimp
1845  apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode")
1846   prefer 2
1847   apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def valid_mdb_ctes_def untyped_inc'_def)
1848  apply (clarsimp simp: mdb_ptr.descendants_of_init')
1849  apply (simp add: caps_no_overlap'_def)
1850  apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI)
1851  apply (drule (1) ctes_of_valid_cap')+
1852  apply (drule valid_capAligned)+
1853  apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD])
1854   apply (drule (1) aligned_untypedRange_non_empty)
1855   apply assumption
1856  apply (frule_tac c' = c in  usableRange_subseteq)
1857   apply (drule (1) aligned_untypedRange_non_empty)
1858   apply assumption
1859  apply (drule (1) aligned_untypedRange_non_empty)+
1860  apply (drule untypedCapRange)+
1861  apply (thin_tac "All P" for P)
1862   apply (subgoal_tac "untypedRange cap \<inter> untypedRange c = {}")
1863   apply (intro conjI)
1864        apply simp
1865       apply (drule(2) set_inter_not_emptyD1)
1866       apply fastforce
1867      apply (drule(2) set_inter_not_emptyD2)
1868      apply fastforce
1869     apply (drule(2) set_inter_not_emptyD3)
1870     apply simp+
1871  apply (rule disjoint_subset2[OF _ disjoint_subset])
1872    apply (rule untypedRange_in_capRange)+
1873  apply (simp add:Int_ac)
1874  done
1875context begin interpretation Arch . (*FIXME: arch_split*)
1876lemma valid_nullcaps_init:
1877  "\<lbrakk> valid_nullcaps m; cap \<noteq> NullCap \<rbrakk> \<Longrightarrow> valid_nullcaps (m(p \<mapsto> CTE cap initMDBNode))"
1878  by (simp add: valid_nullcaps_def initMDBNode_def nullPointer_def)
1879end
1880
1881lemma class_links_def2:
1882  "class_links m = (\<forall>p cte. m p = Some cte \<longrightarrow> mdbNext (cteMDBNode cte) \<in> dom m
1883         \<longrightarrow> capClass (cteCap cte) = capClass (cteCap (the (m (mdbNext (cteMDBNode cte))))))"
1884  by (auto simp add: class_links_def dom_def mdb_next_unfold)
1885
1886lemma class_links_init:
1887  "\<lbrakk> class_links m; no_0 m; m p = Some cte;
1888     no_mdb cte; valid_dlist m \<rbrakk>
1889   \<Longrightarrow> class_links (m(p \<mapsto> CTE cap initMDBNode))"
1890  apply (simp add: class_links_def split del: if_split)
1891  apply (erule allEI, erule allEI)
1892  apply simp
1893  apply (intro conjI impI)
1894    apply clarsimp
1895    apply (drule no_mdb_not_target[where p=p], simp)
1896       apply (simp add: no_mdb_def)
1897      apply (erule(2) valid_dlist_init)
1898     apply (clarsimp simp add: no_0_def)
1899    apply simp
1900   apply (clarsimp simp: mdb_next_unfold)
1901  apply (clarsimp simp: mdb_next_unfold)
1902  done
1903
1904lemma distinct_zombies_copyE:
1905  "\<lbrakk> distinct_zombies m; m x = Some cte;
1906       capClass (cteCap cte') = PhysicalClass
1907               \<Longrightarrow> isZombie (cteCap cte) = isZombie (cteCap cte');
1908       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte) \<rbrakk>
1909               \<Longrightarrow> isUntypedCap (cteCap cte');
1910       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte) \<rbrakk>
1911               \<Longrightarrow> isArchPageCap (cteCap cte');
1912       isZombie (cteCap cte') \<Longrightarrow> x = y;
1913       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
1914               capBits (cteCap cte') = capBits (cteCap cte);
1915       capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass;
1916       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
1917            capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
1918        \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))"
1919  apply (simp add: distinct_zombies_def distinct_zombie_caps_def)
1920  apply clarsimp
1921  apply (intro allI conjI impI)
1922    apply clarsimp
1923    apply (drule_tac x=y in spec)
1924    apply (drule_tac x=ptr' in spec)
1925    apply (clarsimp simp: isCap_simps)
1926   apply clarsimp
1927   apply (drule_tac x=ptr in spec)
1928   apply (drule_tac x=x in spec)
1929   apply clarsimp
1930   apply auto[1]
1931  apply clarsimp
1932  apply (drule_tac x=ptr in spec)
1933  apply (drule_tac x=ptr' in spec)
1934  apply auto[1]
1935  done
1936
1937lemmas distinct_zombies_sameE
1938    = distinct_zombies_copyE [where y=x and x=x for x, simplified,
1939                              OF _ _ _ _ _]
1940context begin interpretation Arch . (*FIXME: arch_split*)
1941lemma capBits_Master:
1942  "capBits (capMasterCap cap) = capBits cap"
1943  by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split)
1944
1945lemma capUntyped_Master:
1946  "capUntypedPtr (capMasterCap cap) = capUntypedPtr cap"
1947  by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split)
1948
1949lemma distinct_zombies_copyMasterE:
1950  "\<lbrakk> distinct_zombies m; m x = Some cte;
1951          capClass (cteCap cte') = PhysicalClass
1952             \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte');
1953          isZombie (cteCap cte') \<Longrightarrow> x = y \<rbrakk>
1954       \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))"
1955  apply (erule(1) distinct_zombies_copyE, simp_all)
1956       apply (rule master_eqI, rule isCap_Master, simp)
1957      apply (drule_tac f=isUntypedCap in arg_cong)
1958      apply (simp add: isCap_Master)
1959     apply (drule_tac f=isArchPageCap in arg_cong)
1960     apply (simp add: isCap_Master)
1961    apply (rule master_eqI, rule capBits_Master, simp)
1962   apply clarsimp
1963   apply (drule_tac f=capClass in arg_cong, simp add: capClass_Master)
1964  apply (drule_tac f=capUntypedPtr in arg_cong, simp add: capUntyped_Master)
1965  done
1966
1967lemmas distinct_zombies_sameMasterE
1968    = distinct_zombies_copyMasterE[where x=x and y=x for x, simplified,
1969                                   OF _ _ _]
1970
1971lemma isZombie_capClass: "isZombie cap \<Longrightarrow> capClass cap = PhysicalClass"
1972  by (clarsimp simp: isCap_simps)
1973
1974lemma distinct_zombies_unzombieE:
1975  "\<lbrakk> distinct_zombies m; m x = Some cte;
1976        isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte);
1977        isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte');
1978        isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte');
1979        capClass (cteCap cte') = capClass (cteCap cte);
1980        capBits (cteCap cte') = capBits (cteCap cte);
1981        capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
1982          \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte'))"
1983  apply (simp add: distinct_zombies_def distinct_zombie_caps_def
1984                     split del: if_split)
1985  apply (erule allEI, erule allEI)
1986  apply clarsimp
1987  done
1988
1989lemma distinct_zombies_seperateE:
1990  "\<lbrakk> distinct_zombies m;
1991      \<And>y cte. m y = Some cte \<Longrightarrow> x \<noteq> y
1992                \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
1993                \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
1994                \<Longrightarrow> capClass (cteCap cte) = PhysicalClass
1995                \<Longrightarrow> capClass (cteCap cte') = PhysicalClass
1996                \<Longrightarrow> capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte')
1997                \<Longrightarrow> capBits (cteCap cte) = capBits (cteCap cte') \<Longrightarrow> False \<rbrakk>
1998       \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))"
1999  apply (simp add: distinct_zombies_def distinct_zombie_caps_def)
2000  apply (intro impI allI conjI)
2001    apply (clarsimp simp: isZombie_capClass)
2002    apply fastforce
2003   apply clarsimp
2004   apply (frule isZombie_capClass)
2005   apply (subgoal_tac "\<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)")
2006    apply fastforce
2007   apply (clarsimp simp: isCap_simps)
2008  apply clarsimp
2009  apply (erule notE[rotated], elim allE, erule mp)
2010  apply auto[1]
2011  done
2012
2013lemma distinct_zombies_seperate_if_zombiedE:
2014  "\<lbrakk> distinct_zombies m; m x = Some cte;
2015        isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte');
2016        isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte');
2017        capClass (cteCap cte') = capClass (cteCap cte);
2018        capBits (cteCap cte') = capBits (cteCap cte);
2019        capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte);
2020        \<And>y cte''. \<lbrakk> m y = Some cte''; x \<noteq> y;
2021                    isZombie (cteCap cte'); \<not> isZombie (cteCap cte);
2022                    \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte'');
2023                    capClass (cteCap cte'') = PhysicalClass;
2024                    capUntypedPtr (cteCap cte'') = capUntypedPtr (cteCap cte);
2025                    capBits (cteCap cte'') = capBits (cteCap cte)
2026                        \<rbrakk> \<Longrightarrow> False    \<rbrakk>
2027          \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))"
2028  apply (cases "isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)")
2029   apply (erule distinct_zombies_seperateE)
2030   apply auto[1]
2031  apply clarsimp
2032  apply (erule(7) distinct_zombies_unzombieE)
2033  done
2034
2035lemma distinct_zombies_init:
2036  "\<lbrakk> distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte));
2037        capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte) \<rbrakk>
2038       \<Longrightarrow> distinct_zombies (m (p \<mapsto> cte))"
2039  apply (erule distinct_zombies_seperateE)
2040  apply (rename_tac y cte')
2041  apply (clarsimp simp: caps_no_overlap'_def)
2042  apply (drule_tac x=y in spec)+
2043  apply (case_tac cte')
2044  apply (rename_tac capability mdbnode)
2045  apply clarsimp
2046  apply (subgoal_tac "capRange capability \<noteq> capRange (cteCap cte)")
2047   apply (clarsimp simp: capRange_def)
2048  apply (drule(1) capAligned_capUntypedPtr)+
2049  apply clarsimp
2050  done
2051
2052definition
2053  "no_irq' m \<equiv> \<forall>p cte. m p = Some cte \<longrightarrow> cteCap cte \<noteq> IRQControlCap"
2054
2055lemma no_irqD':
2056  "\<lbrakk> m p = Some (CTE IRQControlCap n); no_irq' m \<rbrakk> \<Longrightarrow> False"
2057  unfolding no_irq'_def
2058  apply (erule allE, erule allE, erule (1) impE)
2059  apply auto
2060  done
2061
2062lemma irq_control_init:
2063  assumes no_irq: "cap = IRQControlCap \<longrightarrow> no_irq' m"
2064  assumes ctrl: "irq_control m"
2065  shows "irq_control (m(p \<mapsto> CTE cap initMDBNode))"
2066  using no_irq
2067  apply (clarsimp simp: irq_control_def)
2068  apply (rule conjI)
2069   apply (clarsimp simp: initMDBNode_def)
2070   apply (erule (1) no_irqD')
2071  apply clarsimp
2072  apply (frule irq_revocable, rule ctrl)
2073  apply clarsimp
2074  apply (rule conjI)
2075   apply clarsimp
2076   apply (erule (1) no_irqD')
2077  apply clarsimp
2078  apply (erule (1) irq_controlD, rule ctrl)
2079  done
2080
2081lemma valid_mdb_ctes_init:
2082  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
2083     caps_no_overlap' m (capRange cap); s \<turnstile>' cap;
2084     valid_objs' s; m = ctes_of s; cap \<noteq> NullCap;
2085     fresh_virt_cap_class (capClass cap) (ctes_of s);
2086     cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s) \<rbrakk> \<Longrightarrow>
2087  valid_mdb_ctes (m (p \<mapsto> CTE cap initMDBNode))"
2088  apply (simp add: valid_mdb_ctes_def)
2089  apply (rule conjI, rule valid_dlist_init, simp+)
2090  apply (subgoal_tac "p \<noteq> 0")
2091   prefer 2
2092   apply (erule no_0_neq, clarsimp)
2093  apply (clarsimp simp: no_0_update)
2094  apply (rule conjI, rule mdb_chain_0_update_0, simp+)
2095  apply (rule conjI, rule valid_badges_0_update, simp+)
2096  apply (rule conjI, erule (1) caps_contained_no_overlap)
2097  apply (rule conjI, rule mdb_chunked_init, simp+)
2098  apply (rule conjI)
2099   apply (rule untyped_mdb_init, (simp add: valid_mdb_ctes_def)+)
2100  apply (rule conjI)
2101   apply (rule untyped_inc_init, (simp add: valid_mdb_ctes_def)+)
2102  apply (rule conjI)
2103   apply (erule(1) valid_nullcaps_init)
2104  apply (rule conjI, simp add: ut_revocable'_def initMDBNode_def)
2105  apply (rule conjI, erule(4) class_links_init)
2106  apply (rule conjI)
2107   apply (erule distinct_zombies_init, simp+)
2108    apply (erule valid_capAligned)
2109   apply clarsimp
2110   apply (case_tac ctea, clarsimp)
2111   apply (rule valid_capAligned, erule(1) ctes_of_valid_cap')
2112  apply (rule conjI)
2113   apply (erule (1) irq_control_init)
2114  apply (simp add: ran_def reply_masters_rvk_fb_def)
2115  apply (auto simp: initMDBNode_def)[1]
2116  done
2117
2118lemma setCTE_state_refs_of'[wp]:
2119  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
2120  unfolding setCTE_def
2121  apply (rule setObject_state_refs_of_eq)
2122  apply (clarsimp simp: updateObject_cte in_monad typeError_def
2123                        in_magnitude_check objBits_simps
2124                 split: kernel_object.split_asm if_split_asm)
2125  done
2126
2127lemma setCTE_valid_mdb:
2128  fixes cap
2129  defines "cte \<equiv> CTE cap initMDBNode"
2130  shows
2131  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' no_mdb ptr s \<and>
2132        s \<turnstile>' cap \<and> valid_objs' s \<and> cap \<noteq> NullCap \<and>
2133        caps_no_overlap' (ctes_of s) (capRange cap) \<and>
2134        fresh_virt_cap_class (capClass cap) (ctes_of s) \<and>
2135        (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace>
2136  setCTE ptr cte
2137  \<lbrace>\<lambda>r. valid_mdb'\<rbrace>"
2138  apply (simp add: valid_mdb'_def setCTE_def cte_def cte_wp_at_ctes_of)
2139  apply (wp ctes_of_setObject_cte)
2140  apply (clarsimp simp del: fun_upd_apply)
2141  apply (erule(8) valid_mdb_ctes_init [OF _ _ _ _ _ _ refl])
2142  done
2143
2144lemma setCTE_valid_objs'[wp]:
2145  "\<lbrace>valid_objs' and (valid_cap' (cteCap cte)) \<rbrace>
2146    setCTE p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
2147  unfolding setCTE_def
2148  apply (rule setObject_valid_objs')
2149   apply (clarsimp simp: prod_eq_iff lookupAround2_char1 updateObject_cte objBits_simps)
2150   apply (clarsimp simp: prod_eq_iff lookupAround2_char1
2151                         updateObject_cte in_monad typeError_def
2152                         valid_obj'_def valid_tcb'_def valid_cte'_def
2153                         tcb_cte_cases_def
2154                  split: kernel_object.split_asm if_split_asm)
2155  done
2156
2157lemma setCTE_valid_pspace:
2158  fixes cap
2159  defines "cte \<equiv> CTE cap initMDBNode"
2160  shows
2161  "\<lbrace>\<lambda>s. valid_pspace' s \<and> s \<turnstile>' cap \<and> cte_wp_at' no_mdb ptr s \<and>
2162        caps_no_overlap' (ctes_of s) (capRange cap) \<and>
2163        cap \<noteq> NullCap \<and> fresh_virt_cap_class (capClass cap) (ctes_of s) \<and>
2164        (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace>
2165  setCTE ptr cte
2166  \<lbrace>\<lambda>r. valid_pspace'\<rbrace>"
2167  apply (simp add: valid_pspace'_def setCTE_def cte_def)
2168  apply (rule hoare_pre)
2169   apply (wp setCTE_valid_objs'[unfolded setCTE_def]
2170             setCTE_valid_mdb[unfolded setCTE_def])
2171  apply simp
2172  done
2173
2174lemma getCTE_cte_wp_at:
2175  "\<lbrace>\<top>\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p\<rbrace>"
2176  apply (clarsimp simp: valid_def cte_wp_at'_def getCTE_def)
2177  apply (frule state_unchanged [OF getObject_cte_inv])
2178  apply simp
2179  apply (drule getObject_cte_det, simp)
2180  done
2181
2182lemma getCTE_cte_at:
2183  "\<lbrace>\<top>\<rbrace> getCTE c \<lbrace>\<lambda>_. cte_at' c\<rbrace>"
2184  apply (rule hoare_strengthen_post)
2185   apply (rule getCTE_cte_wp_at)
2186  apply (erule cte_wp_at_weakenE')
2187  apply simp
2188  done
2189
2190lemma getCTE_sp:
2191  "\<lbrace>P\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p and P\<rbrace>"
2192  apply (rule hoare_chain)
2193    apply (rule hoare_vcg_conj_lift)
2194     apply (rule getCTE_cte_wp_at)
2195    apply (rule getCTE_inv)
2196   apply (rule conjI, rule TrueI, assumption)
2197  apply simp
2198  done
2199
2200lemmas setCTE_ad[wp] =
2201  setObject_aligned[where 'a=cte, folded setCTE_def]
2202  setObject_distinct[where 'a=cte, folded setCTE_def]
2203lemmas setCTE_map_to_ctes =
2204  ctes_of_setObject_cte[folded setCTE_def]
2205
2206lemma getCTE_ctes_wp:
2207  "\<lbrace>\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s\<rbrace> getCTE ptr \<lbrace>P\<rbrace>"
2208  apply (rule hoare_strengthen_post, rule getCTE_sp)
2209  apply (clarsimp simp: cte_wp_at_ctes_of)
2210  done
2211
2212lemma updateMDB_valid_objs'[wp]:
2213  "\<lbrace>valid_objs'\<rbrace> updateMDB m p \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
2214  apply (clarsimp simp add: updateMDB_def)
2215  apply (wp | simp)+
2216  done
2217
2218lemma cte_overwrite:
2219  "cteMDBNode_update (\<lambda>x. m) (cteCap_update (\<lambda>x. c) v) = CTE c m"
2220  by (cases v, simp)
2221
2222lemma setCTE_no_0_obj' [wp]:
2223  "\<lbrace>no_0_obj'\<rbrace> setCTE p c \<lbrace>\<lambda>_. no_0_obj'\<rbrace>"
2224  by (simp add: setCTE_def) wp
2225
2226lemma insertInitCap_valid_pspace:
2227  "\<lbrace>valid_pspace' and valid_cap' cap and
2228    (\<lambda>s. caps_no_overlap' (ctes_of s) (capRange cap))
2229    and (\<lambda>s. fresh_virt_cap_class (capClass cap) (ctes_of s)) and
2230    (\<lambda>s. cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace>
2231  insertInitCap ptr cap
2232  \<lbrace>\<lambda>r. valid_pspace'\<rbrace>"
2233  unfolding insertInitCap_def
2234  apply (simp   add: updateCap_def valid_pspace'_def
2235                     valid_mdb'_def bind_assoc
2236          split del: if_split)
2237  apply (wp setCTE_map_to_ctes getCTE_ctes_wp
2238            | simp add: updateMDB_def split del: if_split)+
2239       apply (rule hoare_post_imp)
2240        apply (erule_tac P="pspace_aligned' s \<and> pspace_distinct' s
2241          \<and> no_0_obj' s" in conjunct2)
2242       apply (simp cong: conj_cong)
2243       apply (wp setCTE_map_to_ctes getCTE_ctes_wp)+
2244  apply clarsimp
2245  apply (rule conjI)
2246   apply (clarsimp simp: valid_mdb_ctes_def)
2247  apply (simp add: const_def cte_overwrite nullMDBNode_def
2248                   initMDBNode_def[symmetric]
2249             cong: if_cong)
2250  apply (fold fun_upd_def)
2251  apply (rule impI, rule valid_mdb_ctes_init, simp_all)
2252  apply (simp add: no_mdb_def nullPointer_def)
2253  done
2254
2255
2256declare mresults_fail[simp]
2257
2258crunch idle[wp]: get_object "valid_idle"
2259  (wp: crunch_wps simp: crunch_simps)
2260
2261lemma cte_refs_Master:
2262  "cte_refs' (capMasterCap cap) = cte_refs' cap"
2263  by (rule ext, simp add: capMasterCap_def split: capability.split)
2264end
2265
2266lemma (in vmdb) untyped_mdb': "untyped_mdb' m"
2267  using valid ..
2268
2269lemma (in vmdb) untyped_inc': "untyped_inc' m"
2270  using valid ..
2271
2272lemma diminished_capMaster:
2273  "diminished' cap cap' \<Longrightarrow> capMasterCap cap' = capMasterCap cap"
2274  by (clarsimp simp: diminished'_def)
2275
2276
2277end (* of theory *)
2278