1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory SR_lemmas_C
12imports
13  StateRelation_C
14  "Refine.Invariants_H"
15begin
16
17(* FIXME: move to Word_Lib *)
18lemma sign_extend_0[simp]:
19  "sign_extend a 0 = 0"
20  by (simp add: sign_extend_def)
21
22context begin interpretation Arch . (*FIXME: arch_split*)
23
24(* FIXME: move to ainvs? *)
25lemma sign_extend_canonical_address:
26  "(x = sign_extend 47 x) = canonical_address x"
27  by (fastforce simp: sign_extended_iff_sign_extend canonical_address_sign_extended)
28
29section "ctes"
30
31subsection "capabilities"
32
33lemma cteMDBNode_cte_to_H [simp]:
34  "cteMDBNode (cte_to_H cte) = mdb_node_to_H (cteMDBNode_CL cte)"
35  unfolding cte_to_H_def
36  by simp
37
38lemma cteMDBNode_CL_lift [simp]:
39  "cte_lift cte' = Some ctel \<Longrightarrow>
40  mdb_node_lift (cteMDBNode_C cte') = cteMDBNode_CL ctel"
41  unfolding cte_lift_def
42  by (fastforce split: option.splits)
43
44lemma cteCap_cte_to_H [simp]:
45  "cteCap (cte_to_H cte) = cap_to_H (cap_CL cte)"
46  unfolding cte_to_H_def
47  by simp
48
49lemma cap_CL_lift [simp]:
50  "cte_lift cte' = Some ctel \<Longrightarrow> cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel)"
51  unfolding cte_lift_def
52  by (fastforce split: option.splits)
53
54lemma cteCap_update_cte_to_H [simp]:
55  "\<lbrakk> cte_lift cte' = Some z; cap_lift cap' = Some capl\<rbrakk>
56  \<Longrightarrow> map_option cte_to_H (cte_lift (cte_C.cap_C_update (\<lambda>_. cap') cte')) =
57  Some (cteCap_update (\<lambda>_. cap_to_H capl) (cte_to_H z))"
58  unfolding cte_lift_def
59  by (clarsimp simp: cte_to_H_def split: option.splits)
60
61lemma cteMDBNode_C_update_lift [simp]:
62  "cte_lift cte' = Some ctel \<Longrightarrow>
63  (cte_lift (cteMDBNode_C_update (\<lambda>_. m) cte') = Some x)
64  = (cteMDBNode_CL_update (\<lambda>_. mdb_node_lift m) ctel = x)"
65  unfolding cte_lift_def
66  by (fastforce split: option.splits)
67
68lemma ccap_relationE:
69  "\<lbrakk>ccap_relation c v; \<And>vl. \<lbrakk> cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
70  unfolding ccap_relation_def map_option_case
71  apply clarsimp
72  apply (drule sym)
73  apply (clarsimp split: option.splits)
74  done
75
76
77definition
78  "pageSize cap \<equiv> case cap of ArchObjectCap (PageCap f R ty sz dev m) \<Rightarrow> sz"
79
80definition
81  "isArchCap_tag (n :: machine_word) \<equiv> n mod 2 = 1"
82
83lemma isArchCap_tag_def2:
84  "isArchCap_tag n \<equiv> n && 1 = 1"
85  by (simp add: isArchCap_tag_def word_mod_2p_is_mask[where n=1, simplified] mask_def)
86
87lemma cap_get_tag_isCap0:
88  assumes cr: "ccap_relation cap cap'"
89  shows "(cap_get_tag cap' = scast cap_thread_cap) = isThreadCap cap
90  \<and> (cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)
91  \<and> (cap_get_tag cap' = scast cap_notification_cap) = isNotificationCap cap
92  \<and> (cap_get_tag cap' = scast cap_endpoint_cap) = isEndpointCap cap
93  \<and> (cap_get_tag cap' = scast cap_irq_handler_cap) = isIRQHandlerCap cap
94  \<and> (cap_get_tag cap' = scast cap_irq_control_cap) = isIRQControlCap cap
95  \<and> (cap_get_tag cap' = scast cap_zombie_cap) = isZombie cap
96  \<and> (cap_get_tag cap' = scast cap_reply_cap) = isReplyCap cap
97  \<and> (cap_get_tag cap' = scast cap_untyped_cap) = isUntypedCap cap
98  \<and> (cap_get_tag cap' = scast cap_cnode_cap) = isCNodeCap cap
99  \<and> isArchCap_tag (cap_get_tag cap') = isArchCap \<top> cap
100  \<and> (cap_get_tag cap' = scast cap_frame_cap) = (isArchPageCap cap)
101  \<and> (cap_get_tag cap' = scast cap_domain_cap) = isDomainCap cap
102  \<and> (cap_get_tag cap' = scast cap_io_port_cap) = isArchIOPortCap cap
103  \<and> (cap_get_tag cap' = scast cap_io_port_control_cap) = isIOPortControlCap' cap"
104  using cr
105  apply -
106  apply (erule ccap_relationE)
107  apply (simp add: cap_to_H_def cap_lift_def Let_def isArchCap_tag_def2 isArchCap_def)
108  by (clarsimp simp: isCap_simps cap_tag_defs word_le_nat_alt pageSize_def Let_def
109              split: if_split_asm) \<comment> \<open>takes a while\<close>
110
111
112
113lemma cap_get_tag_isCap:
114  assumes cr: "ccap_relation cap cap'"
115  shows "(cap_get_tag cap' = scast cap_thread_cap) = (isThreadCap cap)"
116  and "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)"
117  and "(cap_get_tag cap' = scast cap_notification_cap) = (isNotificationCap cap)"
118  and "(cap_get_tag cap' = scast cap_endpoint_cap) = (isEndpointCap cap)"
119  and "(cap_get_tag cap' = scast cap_irq_handler_cap) = (isIRQHandlerCap cap)"
120  and "(cap_get_tag cap' = scast cap_irq_control_cap) = (isIRQControlCap cap)"
121  and "(cap_get_tag cap' = scast cap_zombie_cap) = (isZombie cap)"
122  and "(cap_get_tag cap' = scast cap_reply_cap) = isReplyCap cap"
123  and "(cap_get_tag cap' = scast cap_untyped_cap) = (isUntypedCap cap)"
124  and "(cap_get_tag cap' = scast cap_cnode_cap) = (isCNodeCap cap)"
125  and "isArchCap_tag (cap_get_tag cap') = isArchCap \<top> cap"
126  and "(cap_get_tag cap' = scast cap_frame_cap) = (isArchPageCap cap)"
127  and "(cap_get_tag cap' = scast cap_domain_cap) = isDomainCap cap"
128  and "(cap_get_tag cap' = scast cap_io_port_cap) = (isArchIOPortCap cap)"
129  and "(cap_get_tag cap' = scast cap_io_port_control_cap) = (isIOPortControlCap' cap)"
130  using cap_get_tag_isCap0 [OF cr] by auto
131
132lemma cap_get_tag_NullCap:
133  assumes cr: "ccap_relation cap cap'"
134  shows "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)"
135  using cr
136  apply -
137  apply (rule iffI)
138   apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def)
139  apply (simp add: cap_get_tag_isCap isCap_simps)
140  done
141
142lemma cap_get_tag_ThreadCap:
143  assumes cr: "ccap_relation cap cap'"
144  shows "(cap_get_tag cap' = scast cap_thread_cap) =
145  (cap = ThreadCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap')))))"
146  using cr
147  apply -
148  apply (rule iffI)
149   apply (erule ccap_relationE)
150   apply (clarsimp simp add: cap_lifts cap_to_H_def)
151  apply (simp add: cap_get_tag_isCap isCap_simps)
152  done
153
154lemma cap_get_tag_NotificationCap:
155  assumes cr: "ccap_relation cap cap'"
156  shows "(cap_get_tag cap' = scast cap_notification_cap) =
157  (cap = NotificationCap
158         (capNtfnPtr_CL (cap_notification_cap_lift cap'))
159         (capNtfnBadge_CL (cap_notification_cap_lift cap'))
160         (to_bool (capNtfnCanSend_CL (cap_notification_cap_lift cap')))
161         (to_bool (capNtfnCanReceive_CL (cap_notification_cap_lift cap'))))"
162  using cr
163  apply -
164  apply (rule iffI)
165   apply (erule ccap_relationE)
166   apply (clarsimp simp add: cap_lifts cap_to_H_def)
167  apply (simp add: cap_get_tag_isCap isCap_simps)
168  done
169
170lemma cap_get_tag_EndpointCap:
171  assumes cr: "ccap_relation cap cap'"
172  shows "(cap_get_tag cap' = scast cap_endpoint_cap) =
173  (cap = EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift cap'))
174        (capEPBadge_CL (cap_endpoint_cap_lift cap'))
175        (to_bool (capCanSend_CL (cap_endpoint_cap_lift cap')))
176        (to_bool (capCanReceive_CL (cap_endpoint_cap_lift cap')))
177        (to_bool (capCanGrant_CL (cap_endpoint_cap_lift cap'))))"
178  using cr
179  apply -
180  apply (rule iffI)
181   apply (erule ccap_relationE)
182   apply (clarsimp simp add: cap_lifts cap_to_H_def)
183  apply (simp add: cap_get_tag_isCap isCap_simps)
184  done
185
186lemma cap_get_tag_CNodeCap:
187  assumes cr: "ccap_relation cap cap'"
188  shows "(cap_get_tag cap' = scast cap_cnode_cap) =
189  (cap = capability.CNodeCap (capCNodePtr_CL (cap_cnode_cap_lift cap'))
190          (unat (capCNodeRadix_CL (cap_cnode_cap_lift cap')))
191          (capCNodeGuard_CL (cap_cnode_cap_lift cap'))
192          (unat (capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))))"
193  using cr
194  apply -
195  apply (rule iffI)
196   apply (erule ccap_relationE)
197   apply (clarsimp simp add: cap_lifts cap_to_H_def Let_def)
198  apply (simp add: cap_get_tag_isCap isCap_simps Let_def)
199  done
200
201lemma cap_get_tag_IRQHandlerCap:
202  assumes cr: "ccap_relation cap cap'"
203  shows "(cap_get_tag cap' = scast cap_irq_handler_cap) =
204  (cap = capability.IRQHandlerCap (ucast (capIRQ_CL (cap_irq_handler_cap_lift cap'))))"
205  using cr
206  apply -
207  apply (rule iffI)
208   apply (erule ccap_relationE)
209   apply (clarsimp simp add: cap_lifts cap_to_H_def)
210  apply (simp add: cap_get_tag_isCap isCap_simps)
211  done
212
213lemma cap_get_tag_IRQControlCap:
214  assumes cr: "ccap_relation cap cap'"
215  shows "(cap_get_tag cap' = scast cap_irq_control_cap) =
216  (cap = capability.IRQControlCap)"
217  using cr
218  apply -
219  apply (rule iffI)
220   apply (clarsimp simp add: cap_lifts cap_get_tag_isCap isCap_simps cap_to_H_def)
221  apply (simp add: cap_get_tag_isCap isCap_simps)
222  done
223
224lemma cap_get_tag_ZombieCap:
225  assumes cr: "ccap_relation cap cap'"
226  shows "(cap_get_tag cap' = scast cap_zombie_cap) =
227  (cap =
228   (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap'))
229     then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB
230           (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5))
231     else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap'))
232          in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1))
233              (ZombieCNode radix)
234              (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1)))))"
235  using cr
236  apply -
237  apply (rule iffI)
238   apply (erule ccap_relationE)
239   apply (clarsimp simp add: cap_lifts cap_to_H_def)
240  apply (simp add: cap_get_tag_isCap isCap_simps Let_def
241            split: if_split_asm)
242  done
243
244
245
246lemma cap_get_tag_ReplyCap:
247  assumes cr: "ccap_relation cap cap'"
248  shows "(cap_get_tag cap' = scast cap_reply_cap) =
249  (cap =
250      ReplyCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap'))))
251               (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap'))))"
252  using cr
253  apply -
254  apply (rule iffI)
255   apply (erule ccap_relationE)
256   apply (clarsimp simp add: cap_lifts cap_to_H_def)
257  apply (simp add: cap_get_tag_isCap isCap_simps)
258  done
259
260lemma cap_get_tag_UntypedCap:
261  assumes cr: "ccap_relation cap cap'"
262  shows "(cap_get_tag cap' = scast cap_untyped_cap) =
263  (cap = UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift cap')))
264                    (capPtr_CL (cap_untyped_cap_lift cap'))
265                    (unat (capBlockSize_CL (cap_untyped_cap_lift cap')))
266                    (unat (capFreeIndex_CL (cap_untyped_cap_lift cap') << 4)))"
267  using cr
268  apply -
269  apply (rule iffI)
270   apply (erule ccap_relationE)
271   apply (clarsimp simp add: cap_lifts cap_to_H_def)
272  apply (simp add: cap_get_tag_isCap isCap_simps)
273  done
274
275lemma cap_get_tag_DomainCap:
276  assumes cr: "ccap_relation cap cap'"
277  shows "(cap_get_tag cap' = scast cap_domain_cap) = (cap = DomainCap)"
278  using cr
279  apply -
280  apply (rule iffI)
281   apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def)
282  apply (simp add: cap_get_tag_isCap isCap_simps)
283  done
284
285lemmas cap_get_tag_to_H_iffs =
286     cap_get_tag_NullCap
287     cap_get_tag_ThreadCap
288     cap_get_tag_NotificationCap
289     cap_get_tag_EndpointCap
290     cap_get_tag_CNodeCap
291     cap_get_tag_IRQHandlerCap
292     cap_get_tag_IRQControlCap
293     cap_get_tag_ZombieCap
294     cap_get_tag_UntypedCap
295     cap_get_tag_DomainCap
296
297lemmas cap_get_tag_to_H = cap_get_tag_to_H_iffs [THEN iffD1]
298
299subsection "mdb"
300
301lemma cmdbnode_relation_mdb_node_to_H [simp]:
302  "cte_lift cte' = Some y
303  \<Longrightarrow> cmdbnode_relation (mdb_node_to_H (cteMDBNode_CL y)) (cteMDBNode_C cte')"
304  unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def
305  by (fastforce split: option.splits)
306
307(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*)
308lemma tcb_cte_cases_in_range1:
309  assumes tc:"tcb_cte_cases (y - x) = Some v"
310  and     al: "is_aligned x tcbBlockSizeBits"
311  shows   "x \<le> y"
312proof -
313  note objBits_defs [simp]
314
315  from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ 9"
316    unfolding tcb_cte_cases_def
317    by (simp add: diff_eq_eq split: if_split_asm)
318
319  have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
320    by (rule is_aligned_no_overflow)
321
322  hence "x \<le> x + q" using qv
323    apply simp
324    apply unat_arith
325    apply simp
326    done
327
328  thus ?thesis using yq by simp
329qed
330
331lemma tcb_cte_cases_in_range2:
332  assumes tc: "tcb_cte_cases (y - x) = Some v"
333  and     al: "is_aligned x tcbBlockSizeBits"
334  shows   "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
335proof -
336  note objBits_defs [simp]
337
338  from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
339    unfolding tcb_cte_cases_def
340    by (simp add: diff_eq_eq split: if_split_asm)
341
342  have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
343    apply (rule word_plus_mono_right)
344    apply (rule is_aligned_no_overflow' [OF al])
345    done
346
347  thus ?thesis using yq by (simp add: field_simps)
348qed
349
350lemmas tcbSlots =
351  tcbCTableSlot_def tcbVTableSlot_def
352  tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
353
354lemma updateObject_cte_tcb:
355  assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
356  shows   "updateObject ctea (KOTCB tcb) ptr ptr' next =
357   (do alignCheck ptr' (objBits tcb);
358        magnitudeCheck ptr' next (objBits tcb);
359        return (KOTCB (updF (\<lambda>_. ctea) tcb))
360    od)"
361  using tc unfolding tcb_cte_cases_def
362  apply -
363  apply (clarsimp simp add: updateObject_cte Let_def
364    tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
365    split: if_split_asm cong: if_cong)
366  done
367
368definition
369  tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> machine_word \<times> machine_word \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option"
370  where
371  "tcb_no_ctes_proj t \<equiv> (tcbState t, tcbFaultHandler t, tcbIPCBuffer t, tcbArch t, tcbQueued t,
372                            tcbMCP t, tcbPriority t, tcbDomain t, tcbTimeSlice t, tcbFault t, tcbBoundNotification t)"
373
374lemma tcb_cte_cases_proj_eq [simp]:
375  "tcb_cte_cases p = Some (getF, setF) \<Longrightarrow>
376  tcb_no_ctes_proj tcb = tcb_no_ctes_proj (setF f tcb)"
377  unfolding tcb_no_ctes_proj_def tcb_cte_cases_def
378  by (auto split: if_split_asm)
379
380(* NOTE: 5 = cte_level_bits *)
381lemma map_to_ctes_upd_cte':
382  "\<lbrakk> ksPSpace s p = Some (KOCTE cte'); is_aligned p cte_level_bits; ps_clear p cte_level_bits s \<rbrakk>
383  \<Longrightarrow> map_to_ctes (ksPSpace s(p |-> KOCTE cte)) = (map_to_ctes (ksPSpace s))(p |-> cte)"
384  apply (erule (1) map_to_ctes_upd_cte)
385  apply (simp add: field_simps ps_clear_def3 cte_level_bits_def mask_def)
386  done
387
388lemma map_to_ctes_upd_tcb':
389  "[| ksPSpace s p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits;
390   ps_clear p tcbBlockSizeBits s |]
391==> map_to_ctes (ksPSpace s(p |-> KOTCB tcb)) =
392    (%x. if EX getF setF.
393               tcb_cte_cases (x - p) = Some (getF, setF) &
394               getF tcb ~= getF tcb'
395         then case tcb_cte_cases (x - p) of
396              Some (getF, setF) => Some (getF tcb)
397         else ctes_of s x)"
398  apply (erule (1) map_to_ctes_upd_tcb)
399  apply (simp add: field_simps ps_clear_def3 mask_def objBits_defs)
400  done
401
402
403lemma tcb_cte_cases_inv [simp]:
404  "tcb_cte_cases p = Some (getF, setF) \<Longrightarrow> getF (setF (\<lambda>_. v) tcb) = v"
405  unfolding tcb_cte_cases_def
406  by (simp split: if_split_asm)
407
408declare insert_dom [simp]
409
410lemma in_alignCheck':
411  "(z \<in> fst (alignCheck x n s)) = (snd z = s \<and> is_aligned x n)"
412  by (cases z, simp)
413
414lemma fst_alignCheck_empty [simp]:
415   "(fst (alignCheck x n s) = {}) = (\<not> is_aligned x n)"
416  apply (subst all_not_in_conv [symmetric])
417  apply (clarsimp simp: in_alignCheck')
418  done
419
420lemma fst_setCTE0:
421  notes option.case_cong_weak [cong]
422  assumes ct: "cte_at' dest s"
423  shows   "\<exists>(v, s') \<in> fst (setCTE dest cte s).
424           (s' = s \<lparr> ksPSpace := ksPSpace s' \<rparr>)
425           \<and> (dom (ksPSpace s) = dom (ksPSpace s'))
426           \<and> (\<forall>x \<in> dom (ksPSpace s).
427                case (the (ksPSpace s x)) of
428                      KOCTE _ \<Rightarrow> (\<exists>cte. ksPSpace s' x = Some (KOCTE cte))
429                    | KOTCB t \<Rightarrow> (\<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t')
430                    | _       \<Rightarrow> ksPSpace s' x = ksPSpace s x)"
431  using ct
432  apply -
433  apply (clarsimp simp: setCTE_def setObject_def
434    bind_def return_def assert_opt_def gets_def split_beta get_def
435    modify_def put_def)
436  apply (erule cte_wp_atE')
437   apply (rule ps_clear_lookupAround2, assumption+)
438     apply simp
439    apply (erule is_aligned_no_overflow)
440   apply (simp (no_asm_simp) del: fun_upd_apply cong: option.case_cong)
441   apply (simp add: return_def updateObject_cte
442     bind_def assert_opt_def gets_def split_beta get_def
443     modify_def put_def unless_def when_def
444     objBits_simps
445     cong: bex_cong)
446   apply (rule bexI [where x = "((), s)"])
447    apply (frule_tac s' = s in in_magnitude_check [where v = "()"])
448      apply (simp add: cte_level_bits_def)
449     apply assumption
450    apply (simp add: objBits_defs cte_level_bits_def)
451    apply (erule bexI [rotated])
452    apply (simp  cong: if_cong)
453    apply rule
454    apply (simp split: kernel_object.splits)
455    apply (fastforce simp: tcb_no_ctes_proj_def)
456   apply (simp add: cte_level_bits_def objBits_defs)
457  (* clag *)
458  apply (rule ps_clear_lookupAround2, assumption+)
459    apply (erule (1) tcb_cte_cases_in_range1)
460   apply (erule (1) tcb_cte_cases_in_range2)
461  apply (simp add: return_def del: fun_upd_apply cong: bex_cong option.case_cong)
462  apply (subst updateObject_cte_tcb)
463   apply assumption
464  apply (simp add: bind_def return_def assert_opt_def gets_def split_beta get_def when_def
465    modify_def put_def unless_def when_def in_alignCheck')
466  apply (simp add: objBits_simps)
467  apply (simp add: magnitudeCheck_def return_def split: option.splits
468    cong: bex_cong if_cong)
469   apply (simp split: kernel_object.splits)
470   apply (fastforce simp: tcb_no_ctes_proj_def)
471  apply (simp add: magnitudeCheck_def when_def return_def fail_def
472    linorder_not_less
473    split: option.splits
474    cong: bex_cong if_cong)
475  apply rule
476  apply (simp split: kernel_object.splits)
477  apply (fastforce simp: tcb_no_ctes_proj_def)
478  done
479
480
481(* duplicates *)
482lemma pspace_alignedD' [intro?]:
483  assumes  lu: "ksPSpace s x = Some v"
484  and      al: "pspace_aligned' s"
485  shows   "is_aligned x (objBitsKO v)"
486  using al lu unfolding pspace_aligned'_def
487  apply -
488  apply (drule (1) bspec [OF _ domI])
489  apply simp
490  done
491
492declare pspace_distinctD' [intro?]
493
494lemma ctes_of_ksI [intro?]:
495  fixes s :: "kernel_state"
496  assumes ks: "ksPSpace s x = Some (KOCTE cte)"
497  and     pa: "pspace_aligned' s"  (* yuck *)
498  and     pd: "pspace_distinct' s"
499  shows   "ctes_of s x = Some cte"
500proof (rule ctes_of_eq_cte_wp_at')
501  from ks show "cte_wp_at' ((=) cte) x s"
502  proof (rule cte_wp_at_cteI' [OF _ _ _ refl])
503    from ks pa have "is_aligned x (objBitsKO (KOCTE cte))" ..
504    thus "is_aligned x cte_level_bits"
505      unfolding cte_level_bits_def by (simp add: objBits_simps')
506
507    from ks pd have "ps_clear x (objBitsKO (KOCTE cte)) s" ..
508    thus "ps_clear x cte_level_bits s"
509      unfolding cte_level_bits_def by (simp add: objBits_simps')
510  qed
511qed
512
513
514lemma fst_setCTE:
515  assumes ct: "cte_at' dest s"
516  and     rl: "\<And>s'. \<lbrakk> ((), s') \<in> fst (setCTE dest cte s);
517           (s' = s \<lparr> ksPSpace := ksPSpace s' \<rparr>);
518           (ctes_of s' = ctes_of s(dest \<mapsto> cte));
519           (map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'));
520           (map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'));
521           (map_to_pml4es (ksPSpace s) = map_to_pml4es (ksPSpace s'));
522           (map_to_pdptes (ksPSpace s) = map_to_pdptes (ksPSpace s'));
523           (map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'));
524           (map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'));
525           (map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'));
526           (map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'));
527           (map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'));
528           (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s)
529              = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'));
530           \<forall>T p. typ_at' T p s = typ_at' T p s'\<rbrakk> \<Longrightarrow> P"
531  shows   "P"
532proof -
533  (* Unpack the existential and bind x, theorems in this.  Yuck *)
534  from fst_setCTE0 [where cte = cte, OF ct] guess s' by clarsimp
535  note thms = this
536
537  from thms have ceq: "ctes_of s' = ctes_of s(dest \<mapsto> cte)"
538    apply -
539    apply (erule use_valid [OF _ setCTE_ctes_of_wp])
540    apply simp
541    done
542
543  show ?thesis
544  proof (rule rl)
545    show "map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s')"
546    proof (rule map_comp_eqI)
547      fix x
548      assume xin: "x \<in> dom (ksPSpace s')"
549      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
550      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
551      ultimately have "(projectKO_opt ko' :: endpoint option) = projectKO_opt ko" using xin thms(4) ceq
552        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_ep)
553      thus "(projectKO_opt (the (ksPSpace s' x)) :: endpoint option) = projectKO_opt (the (ksPSpace s x))"  using ko ko'
554        by simp
555    qed fact
556
557    (* clag \<dots> *)
558    show "map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s')"
559    proof (rule map_comp_eqI)
560      fix x
561      assume xin: "x \<in> dom (ksPSpace s')"
562      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
563      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
564      ultimately have "(projectKO_opt ko' :: Structures_H.notification option) = projectKO_opt ko" using xin thms(4) ceq
565        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_ntfn)
566      thus "(projectKO_opt (the (ksPSpace s' x)) :: Structures_H.notification option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
567        by simp
568    qed fact
569
570    show "map_to_pml4es (ksPSpace s) = map_to_pml4es (ksPSpace s')"
571    proof (rule map_comp_eqI)
572      fix x
573      assume xin: "x \<in> dom (ksPSpace s')"
574      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
575      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
576      ultimately have "(projectKO_opt ko' :: pml4e option) = projectKO_opt ko" using xin thms(4) ceq
577        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pml4e)
578      thus "(projectKO_opt (the (ksPSpace s' x)) :: pml4e option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
579        by simp
580    qed fact
581
582    show "map_to_pdptes (ksPSpace s) = map_to_pdptes (ksPSpace s')"
583    proof (rule map_comp_eqI)
584      fix x
585      assume xin: "x \<in> dom (ksPSpace s')"
586      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
587      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
588      ultimately have "(projectKO_opt ko' :: pdpte option) = projectKO_opt ko" using xin thms(4) ceq
589        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pdpte)
590      thus "(projectKO_opt (the (ksPSpace s' x)) :: pdpte option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
591        by simp
592    qed fact
593
594    show "map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s')"
595    proof (rule map_comp_eqI)
596      fix x
597      assume xin: "x \<in> dom (ksPSpace s')"
598      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
599      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
600      ultimately have "(projectKO_opt ko' :: pde option) = projectKO_opt ko" using xin thms(4) ceq
601        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pde)
602      thus "(projectKO_opt (the (ksPSpace s' x)) :: pde option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
603        by simp
604    qed fact
605
606    show "map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s')"
607    proof (rule map_comp_eqI)
608      fix x
609      assume xin: "x \<in> dom (ksPSpace s')"
610      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
611      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
612      ultimately have "(projectKO_opt ko' :: pte option) = projectKO_opt ko" using xin thms(4) ceq
613        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pte)
614      thus "(projectKO_opt (the (ksPSpace s' x)) :: pte option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
615        by simp
616    qed fact
617
618    show "map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s')"
619    proof (rule map_comp_eqI)
620      fix x
621      assume xin: "x \<in> dom (ksPSpace s')"
622      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
623      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
624      ultimately have "(projectKO_opt ko' :: asidpool option) = projectKO_opt ko" using xin thms(4) ceq
625        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_asidpool)
626      thus "(projectKO_opt (the (ksPSpace s' x)) :: asidpool option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
627        by simp
628    qed fact
629
630    show "map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s')"
631    proof (rule map_comp_eqI)
632      fix x
633      assume xin: "x \<in> dom (ksPSpace s')"
634      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
635      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
636      ultimately have "(projectKO_opt ko' :: user_data option) = projectKO_opt ko" using xin thms(4) ceq
637        by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_user_data)
638      thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
639        by simp
640    qed fact
641
642    show "map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s')"
643    proof (rule map_comp_eqI)
644      fix x
645      assume xin: "x \<in> dom (ksPSpace s')"
646      then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric])
647      moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp
648      ultimately have "(projectKO_opt ko' :: user_data_device option) = projectKO_opt ko" using xin thms(4) ceq
649             by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_user_data_device)
650      thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data_device option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
651             by simp
652    qed fact
653
654
655    note sta = setCTE_typ_at'[where P="\<lambda>x. x = y" for y]
656    show typ_at: "\<forall>T p. typ_at' T p s = typ_at' T p s'"
657      using use_valid[OF _ sta, OF thms(1), OF refl]
658      by auto
659
660    show "map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) =
661      map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')"
662    proof (rule ext)
663      fix x
664
665      have dm: "dom (map_to_tcbs (ksPSpace s)) = dom (map_to_tcbs (ksPSpace s'))"
666        using thms(3) thms(4)
667        apply -
668        apply (rule set_eqI)
669        apply rule
670        apply (frule map_comp_subset_domD)
671        apply simp
672        apply (drule (1) bspec)
673        apply (clarsimp simp: projectKOs dom_map_comp)
674        apply (frule map_comp_subset_domD)
675        apply (drule (1) bspec)
676        apply (auto simp: dom_map_comp projectKOs split: kernel_object.splits)
677        apply fastforce
678        done
679
680      {
681        assume "x \<in> dom (map_to_tcbs (ksPSpace s))"
682        hence "map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s) x)
683          = map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s') x)"
684          using thms(3) thms(4)
685          apply -
686          apply (frule map_comp_subset_domD)
687          apply simp
688          apply (drule (1) bspec)
689          apply (clarsimp simp: dom_map_comp projectKOs projectKO_opt_tcb)
690          apply (case_tac y)
691          apply simp_all
692          apply clarsimp
693          done
694      } moreover
695      {
696        assume "x \<notin> dom (map_to_tcbs (ksPSpace s))"
697        hence "map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s) x)
698          = map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s') x)"
699          apply -
700          apply (frule subst [OF dm])
701          apply (simp add: dom_def)
702          done
703      } ultimately show "(map_option tcb_no_ctes_proj \<circ> (map_to_tcbs (ksPSpace s))) x
704          = (map_option tcb_no_ctes_proj \<circ> (map_to_tcbs (ksPSpace s'))) x"
705          by auto
706    qed
707  qed fact+
708qed
709
710lemma ctes_of_cte_at:
711  "ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
712  by (simp add: cte_wp_at_ctes_of)
713
714lemma cor_map_relI:
715  assumes dm: "dom am = dom am'"
716  and     rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';
717  rel y z \<rbrakk> \<Longrightarrow> rel y' z"
718  shows "cmap_relation am cm sz rel \<Longrightarrow> cmap_relation am' cm sz rel"
719  unfolding cmap_relation_def
720  apply -
721  apply clarsimp
722  apply rule
723   apply (simp add: dm)
724  apply rule
725  apply (frule_tac P = "\<lambda>s. x \<in> s" in ssubst [OF dm])
726  apply (drule (1) bspec)
727  apply (erule domD [where m = am, THEN exE])
728  apply (rule rl, assumption+)
729   apply (clarsimp simp add: dom_def)
730  apply simp
731  done
732
733lemma setCTE_tcb_case:
734  assumes om: "map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) =
735  map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')"
736  and    rel: "cmap_relation (map_to_tcbs (ksPSpace s)) (clift (t_hrs_' (globals x))) tcb_ptr_to_ctcb_ptr ctcb_relation"
737  shows "cmap_relation (map_to_tcbs (ksPSpace s')) (clift (t_hrs_' (globals x))) tcb_ptr_to_ctcb_ptr ctcb_relation"
738  using om
739proof (rule cor_map_relI [OF map_option_eq_dom_eq])
740  fix x tcb tcb' z
741  assume y: "map_to_tcbs (ksPSpace s) x = Some tcb"
742    and y': "map_to_tcbs (ksPSpace s') x = Some tcb'" and rel: "ctcb_relation tcb z"
743
744  hence "tcb_no_ctes_proj tcb = tcb_no_ctes_proj tcb'" using om
745    apply -
746    apply (simp add: o_def)
747    apply (drule fun_cong [where x = x])
748    apply simp
749    done
750
751  thus "ctcb_relation tcb' z" using rel
752    unfolding tcb_no_ctes_proj_def ctcb_relation_def cfault_rel_def
753    by auto
754qed fact+
755
756lemma lifth_update:
757  "clift (t_hrs_' s) ptr = clift (t_hrs_' s') ptr
758  \<Longrightarrow> lifth ptr s = lifth ptr s'"
759  unfolding lifth_def
760  by simp
761
762lemma getCTE_exs_valid:
763  "cte_at' dest s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE dest \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
764  unfolding exs_valid_def getCTE_def cte_wp_at'_def
765  by clarsimp
766
767lemma cmap_domE1:
768  "\<lbrakk> f ` dom am = dom cm; am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
769  apply (drule equalityD1)
770  apply (drule subsetD)
771   apply (erule imageI [OF domI])
772  apply (clarsimp simp: dom_def)
773  done
774
775lemma cmap_domE2:
776  "\<lbrakk> f ` dom am = dom cm; cm x = Some v'; \<And>x' v. \<lbrakk> x = f x'; am x' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
777  apply (drule equalityD2)
778  apply (drule subsetD)
779  apply (erule domI)
780  apply (clarsimp simp: dom_def)
781  done
782
783lemma cmap_relationE1:
784  "\<lbrakk> cmap_relation am cm f rel; am x = Some y;
785  \<And>y'. \<lbrakk>am x = Some y; rel y y'; cm (f x) = Some y'\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
786  unfolding cmap_relation_def
787  apply clarsimp
788  apply (erule (1) cmap_domE1)
789  apply (drule (1) bspec [OF _ domI])
790  apply clarsimp
791  done
792
793lemma cmap_relationE2:
794  "\<lbrakk> cmap_relation am cm f rel; cm x = Some y';
795  \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
796  unfolding cmap_relation_def
797  apply clarsimp
798  apply (erule (1) cmap_domE2)
799  apply (drule (1) bspec [OF _ domI])
800  apply clarsimp
801  done
802
803lemma cmap_relationI:
804  assumes doms:  "f ` dom am = dom cm"
805  and     rel:   "\<And>x v v'. \<lbrakk>am x = Some v; cm (f x) = Some v' \<rbrakk> \<Longrightarrow> rel v v'"
806  shows "cmap_relation am cm f rel"
807  unfolding cmap_relation_def using doms
808proof (rule conjI)
809  show "\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))"
810  proof
811    fix x
812    assume "x \<in> dom am"
813    then obtain v where "am x = Some v" ..
814    moreover with doms obtain v' where "cm (f x) = Some v'" by (rule cmap_domE1)
815    ultimately show "rel (the (am x)) (the (cm (f x)))"
816      by (simp add: rel)
817  qed
818qed
819
820lemma cmap_relation_relI:
821  assumes "cmap_relation am cm f rel"
822  and     "am x = Some v"
823  and     "cm (f x) = Some v'"
824  shows "rel v v'"
825  using assms
826  by (fastforce elim!: cmap_relationE1)
827
828lemma cspace_cte_relationE:
829  "\<lbrakk> cmap_relation am cm Ptr ccte_relation; am x = Some y;
830  \<And>z k'. \<lbrakk>cm (Ptr x) = Some k'; cte_lift k' = Some z; cte_to_H z = y; c_valid_cte k' \<rbrakk> \<Longrightarrow> P
831  \<rbrakk> \<Longrightarrow> P"
832  apply (erule (1) cmap_relationE1)
833  apply (clarsimp simp: ccte_relation_def map_option_Some_eq2)
834  done
835
836lemma cmdbnode_relationE:
837  "\<lbrakk>cmdbnode_relation m v; m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
838  unfolding cmdbnode_relation_def
839  apply (drule sym)
840  apply clarsimp
841  done
842
843(* Used when the rel changes as well *)
844lemma cmap_relation_upd_relI:
845  fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap"
846  assumes cr: "cmap_relation am cm f rel"
847  and   cof: "am dest = Some v"
848  and   cl:  "cm (f dest) = Some v'"
849  and   cc:  "rel' nv nv'"
850  and   rel: "\<And>x ov ov'. \<lbrakk> x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov' \<rbrakk> \<Longrightarrow> rel' ov ov'"
851  and   inj: "inj f"
852  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel'"
853  using assms
854  apply -
855  apply (rule cmap_relationE1, assumption+)
856  apply clarsimp
857  apply (rule cmap_relationI)
858  apply (simp add: cmap_relation_def)
859  apply (case_tac "x = dest")
860   apply simp
861  apply (simp add: inj_eq split: if_split_asm)
862  apply (erule (2) rel)
863  apply (erule (2) cmap_relation_relI)
864  done
865
866lemma cmap_relation_updI:
867  fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap"
868  assumes cr: "cmap_relation am cm f rel"
869  and   cof: "am dest = Some v"
870  and   cl:  "cm (f dest) = Some v'"
871  and   cc:  "rel nv nv'"
872  and   inj: "inj f"
873  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel"
874  using cr cof cl cc
875  apply (rule cmap_relation_upd_relI)
876   apply simp
877  apply fact
878  done
879
880declare inj_Ptr[simp]
881
882(* Ugh *)
883lemma cpspace_cte_relation_upd_capI:
884  assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation"
885  and   cof: "map_to_ctes am dest = Some cte"
886  and   cl:  "clift cm (Ptr dest) = Some cte'"
887  and   cc:  "ccap_relation capl cap"
888  shows "cmap_relation ((map_to_ctes am)(dest \<mapsto>  (cteCap_update (\<lambda>_. capl) cte)))
889  ((clift cm)(Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) Ptr ccte_relation"
890  using cr cof cl cc
891  apply -
892  apply (frule (2) cmap_relation_relI)
893  apply (erule (2) cmap_relation_updI)
894   apply (clarsimp elim!: ccap_relationE simp: map_comp_Some_iff ccte_relation_def)
895    apply (subst (asm) map_option_Some_eq2)
896    apply clarsimp
897    apply (simp add: c_valid_cte_def cl_valid_cte_def)
898  apply simp
899done
900
901lemma cte_to_H_mdb_node_update [simp]:
902  "cte_to_H (cteMDBNode_CL_update (\<lambda>_. m) cte) =
903  cteMDBNode_update (\<lambda>_. mdb_node_to_H  m) (cte_to_H cte)"
904  unfolding cte_to_H_def
905  by simp
906
907lemma cspace_cte_relation_upd_mdbI:
908  assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation"
909  and   cof: "map_to_ctes am dest = Some cte"
910  and   cl:  "clift cm (Ptr dest) = Some cte'"
911  and   cc:  "cmdbnode_relation mdbl m"
912  shows "cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte))
913  ((clift cm)(Ptr dest \<mapsto> cte_C.cteMDBNode_C_update (\<lambda>_. m) cte')) Ptr ccte_relation"
914  using cr cof cl cc
915  apply -
916  apply (frule (2) cmap_relation_relI)
917  apply (erule (2) cmap_relation_updI)
918   apply (clarsimp elim!: cmdbnode_relationE
919           simp: map_comp_Some_iff ccte_relation_def c_valid_cte_def cl_valid_cte_def map_option_Some_eq2)
920  apply simp
921done
922
923lemma mdb_node_to_H_mdbPrev_update[simp]:
924  "mdb_node_to_H (mdbPrev_CL_update (\<lambda>_. x) m)
925  = mdbPrev_update (\<lambda>_. x) (mdb_node_to_H m)"
926  unfolding mdb_node_to_H_def by simp
927
928lemma mdb_node_to_H_mdbNext_update[simp]:
929  "mdb_node_to_H (mdbNext_CL_update (\<lambda>_. x) m)
930  = mdbNext_update (\<lambda>_. x) (mdb_node_to_H m)"
931  unfolding mdb_node_to_H_def by simp
932
933lemma mdb_node_to_H_mdbRevocable_update[simp]:
934  "mdb_node_to_H (mdbRevocable_CL_update (\<lambda>_. x) m)
935  = mdbRevocable_update (\<lambda>_. to_bool x) (mdb_node_to_H m)"
936  unfolding mdb_node_to_H_def by simp
937
938lemma mdb_node_to_H_mdbFirstBadged_update[simp]:
939  "mdb_node_to_H (mdbFirstBadged_CL_update (\<lambda>_. x) m)
940  = mdbFirstBadged_update (\<lambda>_. to_bool x) (mdb_node_to_H m)"
941  unfolding mdb_node_to_H_def by simp
942
943declare to_bool_from_bool [simp]
944
945lemma mdbNext_to_H [simp]:
946  "mdbNext (mdb_node_to_H n) = mdbNext_CL n"
947  unfolding mdb_node_to_H_def
948  by simp
949
950lemma mdbPrev_to_H [simp]:
951  "mdbPrev (mdb_node_to_H n) = mdbPrev_CL n"
952  unfolding mdb_node_to_H_def
953  by simp
954
955lemmas ctes_of_not_0 [simp] = valid_mdbD3' [of s, rotated] for s
956
957(* For getting rid of the generated guards -- will probably break with c_guard*)
958lemma cte_bits_le_3 [simp]: "3 \<le> cte_level_bits"
959  by (simp add: objBits_defs cte_level_bits_def)
960
961lemma cte_bits_le_tcb_bits: "cte_level_bits \<le> tcbBlockSizeBits"
962  by (simp add: cte_level_bits_def objBits_defs)
963
964lemma ctes_of_aligned_bits:
965  assumes pa: "pspace_aligned' s"
966  and    cof: "ctes_of s p = Some cte"
967  and   bits: "bits \<le> cte_level_bits"
968  shows  "is_aligned p bits"
969proof -
970  from cof have "cte_wp_at' ((=) cte) p s"
971    by (simp add: cte_wp_at_ctes_of)
972  thus ?thesis
973    apply -
974    apply (rule is_aligned_weaken[OF _ bits])
975    apply (erule cte_wp_atE')
976     apply assumption
977    apply (simp add: tcb_cte_cases_def field_simps split: if_split_asm)
978        apply (fastforce elim: aligned_add_aligned[OF _ _ cte_bits_le_tcb_bits]
979                         simp: is_aligned_def cte_level_bits_def)+
980    apply (erule is_aligned_weaken[OF _  cte_bits_le_tcb_bits])
981    done
982qed
983
984lemma mdbNext_not_zero_eq:
985  "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja \<and> (is_aligned (mdbNext n) 3)*)
986  \<longrightarrow> (mdbNext n \<noteq> 0) = (s' \<in> {_. mdbNext_CL (mdb_node_lift n') \<noteq> 0})"
987  by (fastforce elim: cmdbnode_relationE)
988
989lemma mdbPrev_not_zero_eq:
990  "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja\<and> (is_aligned (mdbPrev n) 3)*)
991  \<longrightarrow> (mdbPrev n \<noteq> 0) = (s' \<in> {_. mdbPrev_CL (mdb_node_lift n') \<noteq> 0})"
992  by (fastforce elim: cmdbnode_relationE)
993
994abbreviation
995  "nullCapPointers cte \<equiv> cteCap cte = NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer"
996
997lemma nullCapPointers_def:
998  "is_an_abbreviation" unfolding is_an_abbreviation_def by simp
999
1000lemma valid_mdb_ctes_of_next:
1001  "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbNext (cteMDBNode cte)) s"
1002  unfolding valid_mdb'_def valid_mdb_ctes_def
1003  apply clarsimp
1004  apply (erule (2) valid_dlistE)
1005  apply (simp add: cte_wp_at_ctes_of)
1006  done
1007
1008lemma valid_mdb_ctes_of_prev:
1009  "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbPrev (cteMDBNode cte)) s"
1010  unfolding valid_mdb'_def valid_mdb_ctes_def
1011  apply clarsimp
1012  apply (erule (2) valid_dlistE)
1013  apply (simp add: cte_wp_at_ctes_of)
1014  done
1015
1016end
1017
1018context kernel
1019begin
1020
1021lemma cmap_relation_tcb [intro]:
1022  "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_tcb_relation (ksPSpace s) (t_hrs_' (globals s'))"
1023  unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
1024  by (simp add: Let_def)
1025
1026lemma cmap_relation_ep [intro]:
1027  "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_ep_relation (ksPSpace s) (t_hrs_' (globals s'))"
1028  unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
1029  by (simp add: Let_def)
1030
1031lemma cmap_relation_ntfn [intro]:
1032  "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_ntfn_relation (ksPSpace s) (t_hrs_' (globals s'))"
1033  unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
1034  by (simp add: Let_def)
1035
1036lemma cmap_relation_cte [intro]:
1037  "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_cte_relation (ksPSpace s) (t_hrs_' (globals s'))"
1038  unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
1039  by (simp add: Let_def)
1040
1041lemma rf_sr_cpspace_asidpool_relation:
1042  "(s, s') \<in> rf_sr
1043    \<Longrightarrow> cpspace_asidpool_relation (ksPSpace s) (t_hrs_' (globals s'))"
1044  by (clarsimp simp: rf_sr_def cstate_relation_def
1045                     cpspace_relation_def Let_def)
1046
1047lemma rf_sr_cpte_relation:
1048  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_ptes (ksPSpace s))
1049                         (cslift s') pte_Ptr cpte_relation"
1050  by (clarsimp simp: rf_sr_def cstate_relation_def
1051                     Let_def cpspace_relation_def)
1052lemma rf_sr_cpde_relation:
1053  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pdes (ksPSpace s))
1054                         (cslift s') pde_Ptr cpde_relation"
1055  by (clarsimp simp: rf_sr_def cstate_relation_def
1056                     Let_def cpspace_relation_def)
1057
1058lemma rf_sr_cpdpte_relation:
1059  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pdptes (ksPSpace s))
1060                         (cslift s') pdpte_Ptr cpdpte_relation"
1061  by (clarsimp simp: rf_sr_def cstate_relation_def
1062                     Let_def cpspace_relation_def)
1063
1064lemma rf_sr_cpml4e_relation:
1065  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pml4es (ksPSpace s))
1066                         (cslift s') pml4e_Ptr cpml4e_relation"
1067  by (clarsimp simp: rf_sr_def cstate_relation_def
1068                     Let_def cpspace_relation_def)
1069
1070lemma rf_sr_cte_relation:
1071  "\<lbrakk> (s, s') \<in> rf_sr; ctes_of s src = Some cte; cslift s' (Ptr src) = Some cte' \<rbrakk> \<Longrightarrow> ccte_relation cte cte'"
1072  apply (drule cmap_relation_cte)
1073  apply (erule (2) cmap_relation_relI)
1074  done
1075
1076lemma ccte_relation_ccap_relation:
1077  "ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte')"
1078  unfolding ccte_relation_def ccap_relation_def c_valid_cte_def cl_valid_cte_def c_valid_cap_def cl_valid_cap_def
1079  by (clarsimp simp: map_option_Some_eq2 if_bool_eq_conj)
1080
1081lemma ccte_relation_cmdbnode_relation:
1082  "ccte_relation cte cte' \<Longrightarrow> cmdbnode_relation (cteMDBNode cte) (cte_C.cteMDBNode_C cte')"
1083  unfolding ccte_relation_def ccap_relation_def
1084  by (clarsimp simp: map_option_Some_eq2)
1085
1086lemma rf_sr_ctes_of_clift:
1087  assumes sr: "(s, s') \<in> rf_sr"
1088  and    cof: "ctes_of s p = Some cte"
1089  shows "\<exists>cte'. cslift s' (Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte'))
1090         \<and> c_valid_cte cte'"
1091proof -
1092  from sr have "cpspace_cte_relation (ksPSpace s) (t_hrs_' (globals s'))" ..
1093  thus ?thesis using cof
1094    apply (rule cspace_cte_relationE)
1095    apply clarsimp
1096    done
1097qed
1098
1099lemma c_valid_cte_eq:
1100 "c_valid_cte c = case_option True cl_valid_cte (cte_lift c)"
1101 apply (clarsimp simp: c_valid_cte_def cl_valid_cte_def c_valid_cap_def  split: option.splits)
1102 apply (unfold cte_lift_def)
1103 apply simp
1104done
1105
1106lemma rf_sr_ctes_of_cliftE:
1107  assumes cof: "ctes_of s p = Some cte"
1108  assumes sr: "(s, s') \<in> rf_sr"
1109  and     rl: "\<And>cte' ctel'. \<lbrakk>ctes_of s p = Some (cte_to_H ctel');
1110                        cslift s' (Ptr p) = Some cte';
1111                        cte_lift cte' = Some ctel';
1112                        cte = cte_to_H ctel' ;
1113                        cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> R"
1114  shows "R"
1115  using sr cof
1116  apply -
1117  apply (frule (1) rf_sr_ctes_of_clift)
1118  apply (elim conjE exE)
1119  apply (rule rl)
1120      apply simp
1121     apply assumption
1122    apply clarsimp
1123   apply clarsimp
1124  apply (clarsimp simp: c_valid_cte_eq)
1125  done
1126
1127lemma cstate_relation_only_t_hrs:
1128  "\<lbrakk> t_hrs_' s = t_hrs_' t;
1129  ksReadyQueues_' s = ksReadyQueues_' t;
1130  ksReadyQueuesL1Bitmap_' s = ksReadyQueuesL1Bitmap_' t;
1131  ksReadyQueuesL2Bitmap_' s = ksReadyQueuesL2Bitmap_' t;
1132  ksSchedulerAction_' s = ksSchedulerAction_' t;
1133  ksCurThread_' s = ksCurThread_' t;
1134  ksIdleThread_' s = ksIdleThread_' t;
1135  ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t;
1136  intStateIRQNode_' s = intStateIRQNode_' t;
1137  intStateIRQTable_' s = intStateIRQTable_' t;
1138  x86KSASIDTable_' s = x86KSASIDTable_' t;
1139  x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t;
1140  phantom_machine_state_' s = phantom_machine_state_' t;
1141  ghost'state_' s = ghost'state_' t;
1142  ksDomScheduleIdx_' s = ksDomScheduleIdx_' t;
1143  ksCurDomain_' s = ksCurDomain_' t;
1144  ksDomainTime_' s = ksDomainTime_' t;
1145  num_ioapics_' s = num_ioapics_' t;
1146  x86KSIRQState_' s = x86KSIRQState_' t
1147  \<rbrakk>
1148  \<Longrightarrow> cstate_relation a s = cstate_relation a t"
1149  unfolding cstate_relation_def
1150  by (clarsimp simp add: Let_def carch_state_relation_def cmachine_state_relation_def)
1151
1152lemma rf_sr_upd:
1153  assumes
1154    "(t_hrs_' (globals x)) = (t_hrs_' (globals y))"
1155    "(ksReadyQueues_' (globals x)) = (ksReadyQueues_' (globals y))"
1156    "(ksReadyQueuesL1Bitmap_' (globals x)) = (ksReadyQueuesL1Bitmap_' (globals y))"
1157    "(ksReadyQueuesL2Bitmap_' (globals x)) = (ksReadyQueuesL2Bitmap_' (globals y))"
1158    "(ksSchedulerAction_' (globals x)) = (ksSchedulerAction_' (globals y))"
1159    "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))"
1160    "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))"
1161    "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))"
1162    "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)"
1163    "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)"
1164    "x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)"
1165    "x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)"
1166    "phantom_machine_state_' (globals x) = phantom_machine_state_' (globals y)"
1167    "ghost'state_' (globals x) = ghost'state_' (globals y)"
1168    "ksDomScheduleIdx_' (globals x) = ksDomScheduleIdx_' (globals y)"
1169    "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)"
1170    "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)"
1171    "num_ioapics_' (globals x) = num_ioapics_' (globals y)"
1172    "x86KSIRQState_' (globals x) = x86KSIRQState_' (globals y)"
1173  shows "((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
1174  unfolding rf_sr_def using assms
1175  by simp (rule cstate_relation_only_t_hrs, auto)
1176
1177lemma rf_sr_upd_safe[simp]:
1178  assumes rl: "(t_hrs_' (globals (g y))) = (t_hrs_' (globals y))"
1179  and     rq: "(ksReadyQueues_' (globals (g y))) = (ksReadyQueues_' (globals y))"
1180  and     rqL1: "(ksReadyQueuesL1Bitmap_' (globals (g y))) = (ksReadyQueuesL1Bitmap_' (globals y))"
1181  and     rqL2: "(ksReadyQueuesL2Bitmap_' (globals (g y))) = (ksReadyQueuesL2Bitmap_' (globals y))"
1182  and     sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))"
1183  and     ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))"
1184  and     it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))"
1185  and     isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)"
1186  and     ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)"
1187  and     dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)"
1188  and     cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)"
1189  and     dt: "ksDomainTime_' (globals (g y)) = ksDomainTime_' (globals y)"
1190  and arch:
1191    "x86KSASIDTable_' (globals (g y)) = x86KSASIDTable_' (globals y)"
1192    "x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)"
1193    "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)"
1194    "num_ioapics_' (globals (g y)) = num_ioapics_' (globals y)"
1195    "x86KSIRQState_' (globals (g y)) = x86KSIRQState_' (globals y)"
1196  and    gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)"
1197  and     wu:  "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))"
1198  shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
1199  using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd)
1200
1201(* More of a well-formed lemma, but \<dots> *)
1202lemma valid_mdb_cslift_next:
1203  assumes vmdb: "valid_mdb' s"
1204  and       sr: "(s, s') \<in> rf_sr"
1205  and      cof: "ctes_of s p = Some cte"
1206  and       nz: "mdbNext (cteMDBNode cte) \<noteq> 0"
1207  shows "cslift s' (Ptr (mdbNext (cteMDBNode cte)) :: cte_C ptr) \<noteq> None"
1208proof -
1209  from vmdb cof nz obtain cten where
1210    "ctes_of s (mdbNext (cteMDBNode cte)) = Some cten"
1211    by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_next)
1212
1213  with sr show ?thesis
1214    apply -
1215    apply (drule (1) rf_sr_ctes_of_clift)
1216    apply clarsimp
1217    done
1218qed
1219
1220lemma valid_mdb_cslift_prev:
1221  assumes vmdb: "valid_mdb' s"
1222  and       sr: "(s, s') \<in> rf_sr"
1223  and      cof: "ctes_of s p = Some cte"
1224  and       nz: "mdbPrev (cteMDBNode cte) \<noteq> 0"
1225  shows "cslift s' (Ptr (mdbPrev (cteMDBNode cte)) :: cte_C ptr) \<noteq> None"
1226proof -
1227  from vmdb cof nz obtain cten where
1228    "ctes_of s (mdbPrev (cteMDBNode cte)) = Some cten"
1229    by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_prev)
1230
1231  with sr show ?thesis
1232    apply -
1233    apply (drule (1) rf_sr_ctes_of_clift)
1234    apply clarsimp
1235    done
1236qed
1237
1238lemma rf_sr_cte_at_valid:
1239  "\<lbrakk> cte_wp_at' P (ptr_val p) s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (p :: cte_C ptr)"
1240  apply (clarsimp simp: cte_wp_at_ctes_of)
1241  apply (drule (1) rf_sr_ctes_of_clift)
1242  apply (clarsimp simp add: typ_heap_simps)
1243  done
1244
1245lemma rf_sr_cte_at_validD:
1246  "\<lbrakk> cte_wp_at' P p s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (Ptr p :: cte_C ptr)"
1247  by (simp add: rf_sr_cte_at_valid)
1248
1249(* MOVE *)
1250lemma ccap_relation_NullCap_iff:
1251  "(ccap_relation NullCap cap') = (cap_get_tag cap' = scast cap_null_cap)"
1252  unfolding ccap_relation_def
1253  by (clarsimp simp: map_option_Some_eq2 c_valid_cap_def cl_valid_cap_def
1254                     cap_to_H_def cap_lift_def Let_def cap_tag_defs
1255              split: if_split)
1256
1257(* MOVE *)
1258lemma ko_at_valid_ntfn':
1259  "\<lbrakk> ko_at' ntfn p s; valid_objs' s \<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s"
1260  apply (erule obj_atE')
1261  apply (erule (1) valid_objsE')
1262   apply (simp add: projectKOs valid_obj'_def)
1263   done
1264
1265(* MOVE *)
1266lemma ntfn_blocked_in_queueD:
1267  "\<lbrakk> st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread \<sigma>; ko_at' ntfn' ntfn \<sigma>; invs' \<sigma> \<rbrakk>
1268   \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn')"
1269  apply (drule sym_refs_st_tcb_atD')
1270   apply clarsimp
1271  apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs
1272                        refs_of_rev'[where ko = "KONotification ntfn'", simplified])
1273  apply (cases "ntfnObj ntfn'")
1274    apply (simp_all add: isWaitingNtfn_def)
1275    done
1276
1277(* MOVE *)
1278lemma valid_ntfn_isWaitingNtfnD:
1279  "\<lbrakk> valid_ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn) \<rbrakk>
1280  \<Longrightarrow> (ntfnQueue (ntfnObj ntfn)) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)
1281    \<and> distinct (ntfnQueue (ntfnObj ntfn))"
1282  unfolding valid_ntfn'_def isWaitingNtfn_def
1283  by (clarsimp split: Structures_H.notification.splits ntfn.splits)
1284
1285lemma cmap_relation_ko_atD:
1286  fixes ko :: "'a :: pspace_storable" and  mp :: "word32 \<rightharpoonup> 'a"
1287  assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel"
1288  and     ko: "ko_at' ko ptr s"
1289  shows   "\<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko'"
1290  using ps ko unfolding cmap_relation_def
1291  apply clarsimp
1292  apply (drule bspec [where x = "ptr"])
1293   apply (clarsimp simp: obj_at'_def projectKOs)
1294  apply (clarsimp simp: obj_at'_def projectKOs)
1295  apply (drule equalityD1)
1296  apply (drule subsetD [where c = "f ptr"])
1297   apply (rule imageI)
1298   apply clarsimp
1299  apply clarsimp
1300  done
1301
1302lemma cmap_relation_ko_atE:
1303  fixes ko :: "'a :: pspace_storable" and  mp :: "word32 \<rightharpoonup> 'a"
1304  assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel"
1305  and     ko: "ko_at' ko ptr s"
1306  and     rl: "\<And>ko'. \<lbrakk>cslift s' (f ptr) = Some ko'; rel ko ko'\<rbrakk> \<Longrightarrow> P"
1307  shows   P
1308  using ps ko
1309  apply -
1310  apply (drule (1) cmap_relation_ko_atD)
1311  apply (clarsimp)
1312  apply (erule (1) rl)
1313  done
1314
1315lemma ntfn_to_ep_queue:
1316  assumes ko: "ko_at' ntfn' ntfn s"
1317  and     waiting: "isWaitingNtfn (ntfnObj ntfn')"
1318  and     rf: "(s, s') \<in> rf_sr"
1319  shows "ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn'))
1320              (Ptr (ntfnQueue_head_CL
1321                     (notification_lift (the (cslift s' (Ptr ntfn))))))
1322              (Ptr (ntfnQueue_tail_CL
1323                     (notification_lift (the (cslift s' (Ptr ntfn))))))"
1324proof -
1325  from rf have
1326    "cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') Ptr (cnotification_relation (cslift s'))"
1327    by (rule cmap_relation_ntfn)
1328
1329  thus ?thesis using ko waiting
1330    apply -
1331    apply (erule (1) cmap_relation_ko_atE)
1332    apply (clarsimp simp: cnotification_relation_def Let_def isWaitingNtfn_def
1333                   split: Structures_H.notification.splits ntfn.splits)
1334    done
1335qed
1336
1337lemma map_to_tcbs_from_tcb_at:
1338  "tcb_at' thread s \<Longrightarrow> map_to_tcbs (ksPSpace s) thread \<noteq> None"
1339  unfolding obj_at'_def
1340  by (clarsimp simp: projectKOs)
1341
1342lemma tcb_at_h_t_valid:
1343  "\<lbrakk> tcb_at' thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread"
1344  apply (drule cmap_relation_tcb)
1345  apply (drule map_to_tcbs_from_tcb_at)
1346  apply (clarsimp simp add: cmap_relation_def)
1347  apply (drule (1) bspec [OF _ domI])
1348  apply (clarsimp simp add: dom_def tcb_ptr_to_ctcb_ptr_def image_def)
1349  apply (drule equalityD1)
1350  apply (drule subsetD)
1351   apply simp
1352   apply (rule exI [where x = thread])
1353   apply simp
1354  apply (clarsimp simp: typ_heap_simps)
1355  done
1356
1357lemma st_tcb_at_h_t_valid:
1358  "\<lbrakk> st_tcb_at' P thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread"
1359  apply (drule pred_tcb_at')
1360  apply (erule (1) tcb_at_h_t_valid)
1361  done
1362
1363(* MOVE *)
1364lemma exs_getObject:
1365  assumes x: "\<And>q n ko. loadObject p q n ko =
1366                (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)"
1367  assumes P: "\<And>(v::'a::pspace_storable). (1 :: machine_word) < 2 ^ (objBits v)"
1368  and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s"
1369  shows      "\<lbrace>(=) s\<rbrace> getObject p \<exists>\<lbrace>\<lambda>r :: ('a :: pspace_storable). (=) s\<rbrace>"
1370  using objat unfolding exs_valid_def obj_at'_def
1371  apply clarsimp
1372  apply (rule_tac x = "(the (projectKO_opt ko), s)" in bexI)
1373   apply (clarsimp simp: split_def)
1374  apply (simp add: projectKO_def fail_def split: option.splits)
1375  apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1
1376                        split_def x P lookupAround2_char1 projectKOs
1377                        objBits_def[symmetric] in_magnitude_check project_inject)
1378  done
1379
1380
1381lemma setObject_eq:
1382  fixes ko :: "('a :: pspace_storable)"
1383  assumes x: "\<And>(val :: 'a) old ptr ptr' next. updateObject val old ptr ptr' next =
1384                (updateObject_default val old ptr ptr' next :: kernel_object kernel)"
1385  assumes P: "\<And>(v::'a::pspace_storable). (1 :: machine_word) < 2 ^ (objBits v)"
1386  and     ob: "\<And>(v :: 'a) (v' :: 'a). objBits v = objBits v'"
1387  and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s"
1388  shows  "((), s\<lparr> ksPSpace := (ksPSpace s)(p \<mapsto> injectKO ko)\<rparr>) \<in> fst (setObject p ko s)"
1389  using objat unfolding setObject_def obj_at'_def
1390  apply (clarsimp simp: updateObject_default_def in_monad return_def lookupAround2_char1
1391                        split_def x P lookupAround2_char1 projectKOs
1392                        objBits_def[symmetric] in_magnitude_check project_inject)
1393  apply (frule ssubst [OF ob, where P = "is_aligned p" and v1 = ko])
1394  apply (simp add: P in_magnitude_check)
1395  apply (rule conjI)
1396   apply (rule_tac x = obj in exI)
1397   apply simp
1398  apply (erule ssubst [OF ob])
1399  done
1400
1401lemma getObject_eq:
1402  fixes ko :: "'a :: pspace_storable"
1403  assumes x: "\<And>q n ko. loadObject p q n ko =
1404                (loadObject_default p q n ko :: 'a kernel)"
1405  assumes P: "\<And>(v::'a). (1 :: machine_word) < 2 ^ (objBits v)"
1406  and objat: "ko_at' ko p s"
1407  shows      "(ko, s) \<in> fst (getObject p s)"
1408  using objat unfolding exs_valid_def obj_at'_def
1409  apply clarsimp
1410  apply (simp add: projectKO_def fail_def split: option.splits)
1411  apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1
1412                        split_def x P lookupAround2_char2 projectKOs
1413                        objBits_def[symmetric] in_magnitude_check project_inject)
1414  done
1415
1416lemma threadSet_eq:
1417  "ko_at' tcb thread s \<Longrightarrow>
1418  ((), s\<lparr> ksPSpace := (ksPSpace s)(thread \<mapsto> injectKO (f tcb))\<rparr>) \<in> fst (threadSet f thread s)"
1419  unfolding threadSet_def
1420  apply (clarsimp simp add: in_monad)
1421  apply (rule exI)
1422  apply (rule exI)
1423  apply (rule conjI)
1424   apply (rule getObject_eq)
1425     apply simp
1426    apply (simp add: objBits_simps')
1427   apply assumption
1428  apply (drule setObject_eq [rotated -1])
1429     apply simp
1430    apply (simp add: objBits_simps')
1431   apply (simp add: objBits_simps)
1432  apply simp
1433  done
1434
1435definition
1436  "tcb_null_ep_ptrs a \<equiv> a \<lparr> tcbEPNext_C := NULL, tcbEPPrev_C := NULL \<rparr>"
1437
1438definition
1439  "tcb_null_sched_ptrs a \<equiv> a \<lparr> tcbSchedNext_C := NULL, tcbSchedPrev_C := NULL \<rparr>"
1440
1441definition
1442  "tcb_null_queue_ptrs a \<equiv> a \<lparr> tcbSchedNext_C := NULL, tcbSchedPrev_C := NULL, tcbEPNext_C := NULL, tcbEPPrev_C := NULL\<rparr>"
1443
1444lemma null_sched_queue:
1445  "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'
1446  \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'"
1447  apply (rule ext)
1448  apply (erule_tac x = x in map_option_comp_eqE)
1449   apply simp
1450  apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_sched_ptrs_def)
1451  done
1452
1453lemma null_ep_queue:
1454  "map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp'
1455  \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'"
1456  apply (rule ext)
1457  apply (erule_tac x = x in map_option_comp_eqE)
1458   apply simp
1459  apply (case_tac v, case_tac v')
1460  apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_ep_ptrs_def)
1461  done
1462
1463lemma null_sched_epD:
1464  assumes om: "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'"
1465  shows "map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and>
1466         map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp'"
1467  using om
1468  apply -
1469  apply (rule conjI)
1470   apply (rule ext)
1471   apply (erule_tac x = x in map_option_comp_eqE )
1472    apply simp
1473   apply (case_tac v, case_tac v')
1474   apply (clarsimp simp: tcb_null_sched_ptrs_def)
1475  apply (rule ext)
1476  apply (erule_tac x = x in map_option_comp_eqE )
1477   apply simp
1478  apply (case_tac v, case_tac v')
1479  apply (clarsimp simp: tcb_null_sched_ptrs_def)
1480  done
1481
1482lemma null_ep_schedD:
1483  assumes om: "map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp'"
1484  shows "map_option tcbSchedNext_C \<circ> mp = map_option tcbSchedNext_C \<circ> mp' \<and>
1485         map_option tcbSchedPrev_C \<circ> mp = map_option tcbSchedPrev_C \<circ> mp'"
1486  using om
1487  apply -
1488  apply (rule conjI)
1489   apply (rule ext)
1490   apply (erule_tac x = x in map_option_comp_eqE )
1491    apply simp
1492   apply (case_tac v, case_tac v')
1493   apply (clarsimp simp: tcb_null_ep_ptrs_def)
1494  apply (rule ext)
1495  apply (erule_tac x = x in map_option_comp_eqE )
1496   apply simp
1497  apply (case_tac v, case_tac v')
1498  apply (clarsimp simp: tcb_null_ep_ptrs_def)
1499  done
1500
1501lemma cmap_relation_cong:
1502  assumes adom: "dom am = dom am'"
1503  and     cdom: "dom cm = dom cm'"
1504  and   rel: "\<And>p a a' b b'.
1505  \<lbrakk> am p = Some a; am' p = Some a'; cm (f p) = Some b; cm' (f p) = Some b' \<rbrakk> \<Longrightarrow> rel a b = rel' a' b'"
1506  shows "cmap_relation am cm f rel = cmap_relation am' cm' f rel'"
1507  unfolding cmap_relation_def
1508  apply (clarsimp simp: adom cdom)
1509  apply (rule iffI)
1510   apply simp
1511   apply (erule conjE)
1512   apply (drule equalityD1)
1513   apply (rule ballI)
1514   apply (drule (1) bspec)
1515   apply (erule iffD1 [OF rel, rotated -1])
1516      apply (rule Some_the, erule ssubst [OF adom])
1517     apply (erule Some_the)
1518    apply (rule Some_the [where f = cm])
1519    apply (drule subsetD)
1520     apply (erule imageI)
1521    apply (simp add: cdom)
1522   apply (rule Some_the [where f = cm'])
1523   apply (erule subsetD)
1524   apply (erule imageI)
1525  \<comment> \<open>clag\<close>
1526   apply simp
1527   apply (erule conjE)
1528   apply (drule equalityD1)
1529   apply (rule ballI)
1530   apply (drule (1) bspec)
1531   apply (erule iffD2 [OF rel, rotated -1])
1532      apply (rule Some_the, erule ssubst [OF adom])
1533     apply (erule Some_the)
1534    apply (rule Some_the [where f = cm])
1535    apply (drule subsetD)
1536     apply (erule imageI)
1537    apply (simp add: cdom)
1538   apply (rule Some_the [where f = cm'])
1539   apply (erule subsetD)
1540   apply (erule imageI)
1541   done
1542
1543lemma ctcb_relation_null_queue_ptrs:
1544  assumes rel: "cmap_relation mp mp' tcb_ptr_to_ctcb_ptr ctcb_relation"
1545  and same: "map_option tcb_null_queue_ptrs \<circ> mp'' = map_option tcb_null_queue_ptrs \<circ> mp'"
1546  shows "cmap_relation mp mp'' tcb_ptr_to_ctcb_ptr ctcb_relation"
1547  using rel
1548  apply (rule iffD1 [OF cmap_relation_cong, OF _ map_option_eq_dom_eq, rotated -1])
1549    apply simp
1550   apply (rule same [symmetric])
1551  apply (drule compD [OF same])
1552  apply (case_tac b, case_tac b')
1553  apply (simp add: ctcb_relation_def tcb_null_queue_ptrs_def)
1554  done
1555
1556lemma map_to_ko_atI':
1557  "\<lbrakk>(projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some v; invs' s\<rbrakk> \<Longrightarrow> ko_at' v x s"
1558  apply (clarsimp simp: map_comp_Some_iff)
1559  apply (erule aligned_distinct_obj_atI')
1560    apply clarsimp
1561   apply clarsimp
1562  apply (simp add: project_inject)
1563  done
1564
1565(* FIXME x64: do we still need these?
1566(* Levity: added (20090419 09:44:27) *)
1567declare ntfnQueue_head_mask_4 [simp]
1568
1569lemma ntfnQueue_tail_mask_4 [simp]:
1570  "ntfnQueue_tail_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_tail_CL (notification_lift ko')"
1571  unfolding notification_lift_def
1572  apply (clarsimp simp: mask_def word_bw_assocs sign_extend_def)
1573  apply word_bitwise *)
1574
1575lemma map_to_ctes_upd_tcb_no_ctes:
1576  "\<lbrakk>ko_at' tcb thread s ; \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x \<rbrakk>
1577  \<Longrightarrow> map_to_ctes (ksPSpace s(thread \<mapsto> KOTCB tcb')) = map_to_ctes (ksPSpace s)"
1578  apply (erule obj_atE')
1579  apply (simp add: projectKOs objBits_simps)
1580  apply (subst map_to_ctes_upd_tcb')
1581     apply assumption+
1582  apply (rule ext)
1583  apply (clarsimp split: if_split)
1584  apply (drule (1) bspec [OF _ ranI])
1585  apply simp
1586  done
1587
1588lemma update_ntfn_map_tos:
1589  fixes P :: "Structures_H.notification \<Rightarrow> bool"
1590  assumes at: "obj_at' P p s"
1591  shows   "map_to_eps (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_eps (ksPSpace s)"
1592  and     "map_to_tcbs (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_tcbs (ksPSpace s)"
1593  and     "map_to_ctes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_ctes (ksPSpace s)"
1594  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pml4es (ksPSpace s)"
1595  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pdptes (ksPSpace s)"
1596  and     "map_to_pdes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pdes (ksPSpace s)"
1597  and     "map_to_ptes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_ptes (ksPSpace s)"
1598  and     "map_to_asidpools (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_asidpools (ksPSpace s)"
1599  and     "map_to_user_data (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_user_data (ksPSpace s)"
1600  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_user_data_device (ksPSpace s)"
1601  using at
1602  by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
1603    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+
1604
1605lemma update_ep_map_tos:
1606  fixes P :: "endpoint \<Rightarrow> bool"
1607  assumes at: "obj_at' P p s"
1608  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ntfns (ksPSpace s)"
1609  and     "map_to_tcbs (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_tcbs (ksPSpace s)"
1610  and     "map_to_ctes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ctes (ksPSpace s)"
1611  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pml4es (ksPSpace s)"
1612  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pdptes (ksPSpace s)"
1613  and     "map_to_pdes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pdes (ksPSpace s)"
1614  and     "map_to_ptes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ptes (ksPSpace s)"
1615  and     "map_to_asidpools (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_asidpools (ksPSpace s)"
1616  and     "map_to_user_data (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_user_data (ksPSpace s)"
1617  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_user_data_device (ksPSpace s)"
1618  using at
1619  by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
1620    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+
1621
1622lemma update_tcb_map_tos:
1623  fixes P :: "tcb \<Rightarrow> bool"
1624  assumes at: "obj_at' P p s"
1625  shows   "map_to_eps (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s)"
1626  and     "map_to_ntfns (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s)"
1627  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pml4es (ksPSpace s)"
1628  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pdptes (ksPSpace s)"
1629  and     "map_to_pdes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)"
1630  and     "map_to_ptes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s)"
1631  and     "map_to_asidpools (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)"
1632  and     "map_to_user_data (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s)"
1633  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_user_data_device (ksPSpace s)"
1634  using at
1635  by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
1636    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+
1637
1638lemma update_asidpool_map_tos:
1639  fixes P :: "asidpool \<Rightarrow> bool"
1640  assumes at: "obj_at' P p s"
1641  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ntfns (ksPSpace s)"
1642  and     "map_to_tcbs (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_tcbs (ksPSpace s)"
1643  and     "map_to_ctes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ctes (ksPSpace s)"
1644  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ko))) = map_to_pml4es (ksPSpace s)"
1645  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ko))) = map_to_pdptes (ksPSpace s)"
1646  and     "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_pdes (ksPSpace s)"
1647  and     "map_to_ptes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ptes (ksPSpace s)"
1648  and     "map_to_eps  (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_eps (ksPSpace s)"
1649  and     "map_to_user_data (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data (ksPSpace s)"
1650  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data_device (ksPSpace s)"
1651
1652  using at
1653  by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
1654      simp: projectKOs projectKO_opts_defs
1655     split: if_split if_split_asm Structures_H.kernel_object.split_asm
1656            arch_kernel_object.split_asm)
1657
1658lemma update_asidpool_map_to_asidpools:
1659  "map_to_asidpools (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap)))
1660             = (map_to_asidpools (ksPSpace s))(p \<mapsto> ap)"
1661  by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)
1662
1663lemma update_pte_map_to_ptes:
1664  "map_to_ptes (ksPSpace s(p \<mapsto> KOArch (KOPTE pte)))
1665             = (map_to_ptes (ksPSpace s))(p \<mapsto> pte)"
1666  by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)
1667
1668lemma update_pte_map_tos:
1669  fixes P :: "pte \<Rightarrow> bool"
1670  assumes at: "obj_at' P p s"
1671  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ntfns (ksPSpace s)"
1672  and     "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_tcbs (ksPSpace s)"
1673  and     "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ctes (ksPSpace s)"
1674  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPTE ko))) = map_to_pml4es (ksPSpace s)"
1675  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPTE ko))) = map_to_pdptes (ksPSpace s)"
1676  and     "map_to_pdes (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_pdes (ksPSpace s)"
1677  and     "map_to_eps  (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_eps (ksPSpace s)"
1678  and     "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_asidpools (ksPSpace s)"
1679  and     "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data (ksPSpace s)"
1680  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data_device (ksPSpace s)"
1681  using at
1682  by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
1683           split: if_split_asm if_split
1684            simp: projectKOs,
1685       auto simp: projectKO_opts_defs)
1686
1687lemma update_pde_map_to_pdes:
1688  "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPDE pde)))
1689             = (map_to_pdes (ksPSpace s))(p \<mapsto> pde)"
1690  by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)
1691
1692lemma update_pde_map_tos:
1693  fixes P :: "pde \<Rightarrow> bool"
1694  assumes at: "obj_at' P p s"
1695  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ntfns (ksPSpace s)"
1696  and     "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_tcbs (ksPSpace s)"
1697  and     "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ctes (ksPSpace s)"
1698  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPDE ko))) = map_to_pml4es (ksPSpace s)"
1699  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPDE ko))) = map_to_pdptes (ksPSpace s)"
1700  and     "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ptes (ksPSpace s)"
1701  and     "map_to_eps  (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_eps (ksPSpace s)"
1702  and     "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_asidpools (ksPSpace s)"
1703  and     "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data (ksPSpace s)"
1704  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data_device (ksPSpace s)"
1705  using at
1706  by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
1707           split: if_split_asm if_split
1708            simp: projectKOs,
1709       auto simp: projectKO_opts_defs)
1710
1711lemma update_pdpte_map_to_pdptes:
1712  "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPDPTE pdpte)))
1713             = (map_to_pdptes (ksPSpace s))(p \<mapsto> pdpte)"
1714  by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)
1715
1716lemma update_pdpte_map_tos:
1717  fixes P :: "pdpte \<Rightarrow> bool"
1718  assumes at: "obj_at' P p s"
1719  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ntfns (ksPSpace s)"
1720  and     "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_tcbs (ksPSpace s)"
1721  and     "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ctes (ksPSpace s)"
1722  and     "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPDPTE ko))) = map_to_pml4es (ksPSpace s)"
1723  and     "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPDPTE ko))) = map_to_pdes (ksPSpace s)"
1724  and     "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ptes (ksPSpace s)"
1725  and     "map_to_eps  (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_eps (ksPSpace s)"
1726  and     "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_asidpools (ksPSpace s)"
1727  and     "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_user_data (ksPSpace s)"
1728  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_user_data_device (ksPSpace s)"
1729  using at
1730  by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
1731           split: if_split_asm if_split
1732            simp: projectKOs,
1733       auto simp: projectKO_opts_defs)
1734
1735lemma update_pml4e_map_to_pml4es:
1736  "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPML4E pml4e)))
1737             = (map_to_pml4es (ksPSpace s))(p \<mapsto> pml4e)"
1738  by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)
1739
1740lemma update_pml4e_map_tos:
1741  fixes P :: "pml4e \<Rightarrow> bool"
1742  assumes at: "obj_at' P p s"
1743  shows   "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ntfns (ksPSpace s)"
1744  and     "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_tcbs (ksPSpace s)"
1745  and     "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ctes (ksPSpace s)"
1746  and     "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPML4E ko))) = map_to_pdptes (ksPSpace s)"
1747  and     "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPML4E ko))) = map_to_pdes (ksPSpace s)"
1748  and     "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ptes (ksPSpace s)"
1749  and     "map_to_eps  (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_eps (ksPSpace s)"
1750  and     "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_asidpools (ksPSpace s)"
1751  and     "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_user_data (ksPSpace s)"
1752  and     "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_user_data_device (ksPSpace s)"
1753  using at
1754  by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
1755           split: if_split_asm if_split
1756            simp: projectKOs,
1757       auto simp: projectKO_opts_defs)
1758
1759lemma heap_to_page_data_cong [cong]:
1760  "\<lbrakk> map_to_user_data ks = map_to_user_data ks'; bhp = bhp' \<rbrakk>
1761  \<Longrightarrow> heap_to_user_data ks bhp = heap_to_user_data ks' bhp'"
1762  unfolding heap_to_user_data_def by simp
1763
1764lemma heap_to_device_data_cong [cong]:
1765  "\<lbrakk> map_to_user_data_device ks = map_to_user_data_device ks'; bhp = bhp' \<rbrakk>
1766  \<Longrightarrow> heap_to_device_data ks bhp = heap_to_device_data ks' bhp'"
1767  unfolding heap_to_device_data_def by simp
1768
1769lemma map_leD:
1770  "\<lbrakk> map_le m m'; m x = Some y \<rbrakk> \<Longrightarrow> m' x = Some y"
1771  by (simp add: map_le_def dom_def)
1772
1773lemma region_is_bytes_disjoint:
1774  assumes cleared: "region_is_bytes' p n (hrs_htd hrs)"
1775    and not_byte: "typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)"
1776  shows "hrs_htd hrs \<Turnstile>\<^sub>t (p' :: 'a ptr)
1777    \<Longrightarrow> {p ..+ n} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}"
1778  apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
1779  apply (clarsimp simp: set_eq_iff dest!: intvlD[where p="ptr_val p'"])
1780  apply (drule_tac x="of_nat k" in spec, clarsimp simp: size_of_def)
1781  apply (cut_tac m=k in typ_slice_t_self[where td="typ_uinfo_t TYPE('a)"])
1782  apply (clarsimp simp: in_set_conv_nth)
1783  apply (drule_tac x=i in map_leD, simp)
1784  apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def)
1785  done
1786
1787lemma region_actually_is_bytes:
1788  "region_actually_is_bytes' ptr len htd
1789    \<Longrightarrow> region_is_bytes' ptr len htd"
1790  by (simp add: region_is_bytes'_def region_actually_is_bytes'_def
1791         split: if_split)
1792
1793lemma zero_ranges_are_zero_update[simp]:
1794  "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr)
1795    \<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)
1796    \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update ptr v) hrs)
1797        = zero_ranges_are_zero rs hrs"
1798  apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update
1799        intro!: ball_cong[OF refl] conj_cong[OF refl])
1800  apply (drule region_actually_is_bytes)
1801  apply (drule(2) region_is_bytes_disjoint)
1802  apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute)
1803  done
1804
1805lemma inj_tcb_ptr_to_ctcb_ptr [simp]:
1806  "inj tcb_ptr_to_ctcb_ptr"
1807  apply (rule injI)
1808  apply (simp add: tcb_ptr_to_ctcb_ptr_def)
1809  done
1810
1811lemmas tcb_ptr_to_ctcb_ptr_eq [simp] = inj_eq [OF inj_tcb_ptr_to_ctcb_ptr]
1812
1813lemma obj_at_cslift_tcb:
1814  fixes P :: "tcb \<Rightarrow> bool"
1815  shows "\<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
1816  \<exists>ko ko'. ko_at' ko thread s \<and> P ko \<and>
1817        cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and>
1818        ctcb_relation ko ko'"
1819  apply (frule obj_at_ko_at')
1820  apply clarsimp
1821  apply (frule cmap_relation_tcb)
1822  apply (drule (1) cmap_relation_ko_atD)
1823  apply fastforce
1824  done
1825
1826fun
1827  thread_state_to_tsType :: "thread_state \<Rightarrow> machine_word"
1828where
1829  "thread_state_to_tsType (Structures_H.Running) = scast ThreadState_Running"
1830  | "thread_state_to_tsType (Structures_H.Restart) = scast ThreadState_Restart"
1831  | "thread_state_to_tsType (Structures_H.Inactive) = scast ThreadState_Inactive"
1832  | "thread_state_to_tsType (Structures_H.IdleThreadState) = scast ThreadState_IdleThreadState"
1833  | "thread_state_to_tsType (Structures_H.BlockedOnReply) = scast ThreadState_BlockedOnReply"
1834  | "thread_state_to_tsType (Structures_H.BlockedOnReceive oref) = scast ThreadState_BlockedOnReceive"
1835  | "thread_state_to_tsType (Structures_H.BlockedOnSend oref badge cg isc) = scast ThreadState_BlockedOnSend"
1836  | "thread_state_to_tsType (Structures_H.BlockedOnNotification oref) = scast ThreadState_BlockedOnNotification"
1837
1838
1839lemma ctcb_relation_thread_state_to_tsType:
1840  "ctcb_relation tcb ctcb \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = thread_state_to_tsType (tcbState tcb)"
1841  unfolding ctcb_relation_def cthread_state_relation_def
1842  by (cases "(tcbState tcb)", simp_all)
1843
1844
1845lemma tcb_ptr_to_tcb_ptr [simp]:
1846  "tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x) = x"
1847  unfolding tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def
1848  by simp
1849
1850lemma ctcb_ptr_to_ctcb_ptr [simp]:
1851  "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x) = x"
1852  unfolding ctcb_ptr_to_tcb_ptr_def tcb_ptr_to_ctcb_ptr_def
1853  by simp
1854
1855declare ucast_id [simp]
1856
1857definition
1858  cap_rights_from_word_canon :: "machine_word \<Rightarrow> seL4_CapRights_CL"
1859  where
1860  "cap_rights_from_word_canon wd \<equiv>
1861    \<lparr> capAllowGrant_CL = from_bool (wd !! 2),
1862      capAllowRead_CL = from_bool (wd !! 1),
1863      capAllowWrite_CL = from_bool (wd !! 0)\<rparr>"
1864
1865definition
1866  cap_rights_from_word :: "machine_word \<Rightarrow> seL4_CapRights_CL"
1867  where
1868  "cap_rights_from_word wd \<equiv> SOME cr.
1869   to_bool (capAllowGrant_CL cr) = wd !! 2 \<and>
1870   to_bool (capAllowRead_CL cr) = wd !! 1 \<and>
1871   to_bool (capAllowWrite_CL cr) = wd !! 0"
1872
1873lemma cap_rights_to_H_from_word [simp]:
1874  "cap_rights_to_H (cap_rights_from_word wd) = rightsFromWord wd"
1875  unfolding cap_rights_from_word_def rightsFromWord_def
1876  apply (rule someI2_ex)
1877   apply (rule exI [where x = "cap_rights_from_word_canon wd"])
1878   apply (simp add: cap_rights_from_word_canon_def)
1879  apply (simp add: cap_rights_to_H_def)
1880  done
1881
1882lemma cmap_relation_updI2:
1883  fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap"
1884  assumes cr: "cmap_relation am cm f rel"
1885  and   cof: "am dest = None"
1886  and   cc:  "rel nv nv'"
1887  and   inj: "inj f"
1888  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel"
1889  using cr cof cc inj
1890  by (clarsimp simp add: cmap_relation_def inj_eq split: if_split)
1891
1892definition
1893  user_word_at :: "machine_word \<Rightarrow> machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
1894where
1895 "user_word_at x p \<equiv> \<lambda>s. is_aligned p 3
1896       \<and> pointerInUserData p s
1897       \<and> x = word_rcat (map (underlying_memory (ksMachineState s))
1898                                [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])"
1899
1900definition
1901  device_word_at :: "machine_word \<Rightarrow> machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
1902where
1903 "device_word_at x p \<equiv> \<lambda>s. is_aligned p 3
1904       \<and> pointerInDeviceData p s
1905       \<and> x = word_rcat (map (underlying_memory (ksMachineState s))
1906                                [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])"
1907
1908lemma rf_sr_heap_user_data_relation:
1909  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation
1910      (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))
1911      (cslift s') Ptr cuser_user_data_relation"
1912  by (clarsimp simp: user_word_at_def rf_sr_def
1913                     cstate_relation_def Let_def
1914                     cpspace_relation_def)
1915
1916lemma rf_sr_heap_device_data_relation:
1917  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation
1918      (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)))
1919      (cslift s') Ptr cuser_user_data_device_relation"
1920  by (clarsimp simp: user_word_at_def rf_sr_def
1921                     cstate_relation_def Let_def
1922                     cpspace_relation_def)
1923
1924lemma ko_at_projectKO_opt:
1925  "ko_at' ko p s \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m ksPSpace s) p = Some ko"
1926  by (clarsimp elim!: obj_atE' simp: projectKOs)
1927
1928lemma word_shift_by_3:
1929  "x * 8 = (x::'a::len word) << 3"
1930  by (simp add: shiftl_t2n)
1931
1932(* FIXME x64: move *)
1933lemma mask_shiftr_times_simp:
1934  "\<lbrakk>x > n;is_aligned p n\<rbrakk> \<Longrightarrow> (p && mask x >> n) * (2^n) = (p && mask x)"
1935  apply (subst mult.commute)
1936  apply (simp add: shiftl_t2n[symmetric])
1937  by (simp add: is_aligned_andI1 is_aligned_shiftr_shiftl)
1938
1939lemma user_word_at_cross_over:
1940  "\<lbrakk> user_word_at x p s; (s, s') \<in> rf_sr; p' = Ptr p \<rbrakk>
1941   \<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p'
1942         \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x"
1943  apply (drule rf_sr_heap_user_data_relation)
1944  apply (erule cmap_relationE1)
1945   apply (clarsimp simp: heap_to_user_data_def Let_def
1946                         user_word_at_def pointerInUserData_def
1947                         typ_at_to_obj_at'[where 'a=user_data, simplified])
1948   apply (drule obj_at_ko_at', clarsimp)
1949   apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
1950   apply (rule refl)
1951  apply (thin_tac "heap_to_user_data a b c = d" for a b c d)
1952  apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2)
1953  apply (rule conjI)
1954   apply (clarsimp simp: user_word_at_def pointerInUserData_def)
1955   apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def)
1956   apply (drule lift_t_g)
1957   apply (clarsimp simp: )
1958   apply (simp add: align_of_def size_of_def)
1959   apply (fold is_aligned_def[where n=3, simplified], simp)
1960   apply (erule contra_subsetD[rotated])
1961   apply (rule order_trans[rotated])
1962    apply (rule_tac x="p && mask pageBits" and y=8 in intvl_sub_offset)
1963    apply (cut_tac y=p and a="mask pageBits && (~~ mask 3)" in word_and_le1)
1964    apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq,
1965           erule is_aligned_andI1)
1966    apply (simp add: word_le_nat_alt mask_def pageBits_def)
1967   apply simp
1968  apply (clarsimp simp: cuser_user_data_relation_def user_word_at_def)
1969  apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift],
1970         simp+)
1971  apply (drule_tac n="uint (p && mask pageBits >> 3)" in h_t_valid_Array_element)
1972    apply simp
1973   apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and)
1974   apply (insert int_and_leR [where a="uint (p >> 3)" and b=511], clarsimp)[1]
1975  apply (simp add: field_lvalue_def
1976            field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse]
1977            word_shift_by_3 shiftr_shiftl1 is_aligned_andI1)
1978  apply (drule_tac x="ucast (p >> 3)" in spec)
1979  apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask)
1980  apply (fold shiftl_t2n[where n=3, simplified, simplified mult.commute mult.left_commute])
1981  apply (simp add: aligned_shiftr_mask_shiftl pageBits_def)
1982  apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))"
1983                                   and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])"
1984                                    in access_in_array)
1985     apply (rule trans)
1986      apply (erule typ_heap_simps)
1987       apply simp+
1988    apply (rule order_less_le_trans, rule unat_lt2p)
1989    apply simp
1990   apply (fastforce simp add: typ_info_word)
1991  apply simp
1992  apply (rule_tac f="h_val hp" for hp in arg_cong)
1993  apply simp
1994  apply (simp add: field_lvalue_def)
1995  apply (simp add: ucast_nat_def ucast_ucast_mask)
1996  apply (fold shiftl_t2n[where n=3, simplified, simplified mult.commute mult.left_commute])
1997  apply (simp add: aligned_shiftr_mask_shiftl)
1998  done
1999
2000(* FIXME: Because the following lemma is correct, writing to device memory refines from c to abstract.
2001          But because we ignore what are written to decice memory, read does not refine from c to abstract.
2002lemma device_word_at_cross_over:
2003  "\<lbrakk> device_word_at x p s; (s, s') \<in> rf_sr; p' = Ptr p \<rbrakk>
2004   \<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p'
2005         \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x"
2006  apply (drule rf_sr_heap_device_data_relation)
2007  apply (erule cmap_relationE1)
2008   apply (clarsimp simp: heap_to_device_data_def Let_def
2009                         device_word_at_def pointerInDeviceData_def
2010                         typ_at_to_obj_at'[where 'a=user_data_device, simplified])
2011   apply (drule obj_at_ko_at', clarsimp)
2012   apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
2013   apply (rule refl)
2014  apply (thin_tac "heap_to_device_data a b c = d" for a b c d)
2015  apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2)
2016  apply (rule conjI)
2017   apply (clarsimp simp: device_word_at_def pointerInDeviceData_def)
2018   apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def)
2019   apply (drule lift_t_g)
2020   apply (clarsimp simp: )
2021   apply (simp add: align_of_def size_of_def)
2022   apply (fold is_aligned_def[where n=2, simplified], simp)
2023   apply (erule contra_subsetD[rotated])
2024   apply (rule order_trans[rotated])
2025    apply (rule_tac x="p && mask pageBits" and y=4 in intvl_sub_offset)
2026    apply (cut_tac y=p and a="mask pageBits && (~~ mask 2)" in word_and_le1)
2027    apply (subst(asm) word_bw_assocs[symmetric], subst(asm) aligned_neg_mask,
2028           erule is_aligned_andI1)
2029    apply (simp add: word_le_nat_alt mask_def pageBits_def)
2030   apply simp
2031  apply (clarsimp simp: cuser_user_data_device_relation_def device_word_at_def)
2032  apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift],
2033         simp+)
2034  apply (drule_tac n="uint (p && mask pageBits >> 2)" in h_t_valid_Array_element)
2035    apply simp
2036   apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and)
2037   apply (insert int_and_leR [where a="uint (p >> 2)" and b=1023], clarsimp)[1]
2038  apply (simp add: field_lvalue_def
2039            field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse]
2040            word32_shift_by_2 shiftr_shiftl1 is_aligned_andI1)
2041  apply (drule_tac x="ucast (p >> 2)" in spec)
2042  apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask)
2043  apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute])
2044  apply (simp add: aligned_shiftr_mask_shiftl pageBits_def)
2045  apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))"
2046                                   and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])"
2047                                    in access_in_array)
2048     apply (rule trans)
2049      apply (erule typ_heap_simps)
2050       apply simp+
2051    apply (rule order_less_le_trans, rule unat_lt2p)
2052    apply simp
2053   apply (fastforce simp add: typ_info_word)
2054  apply simp
2055  apply (rule_tac f="h_val hp" for hp in arg_cong)
2056  apply simp
2057  apply (simp add: field_lvalue_def)
2058  apply (simp add: ucast_nat_def ucast_ucast_mask)
2059  apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute])
2060  apply (simp add: aligned_shiftr_mask_shiftl)
2061  done
2062*)
2063
2064(* FIXME: move to GenericLib *)
2065lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]
2066
2067lemma unat_mask_3_less_8:
2068  "unat (p && mask 3 :: word64) < 8"
2069  apply (rule unat_less_helper)
2070  apply (rule order_le_less_trans, rule word_and_le1)
2071  apply (simp add: mask_def)
2072  done
2073
2074lemma memory_cross_over:
2075  "\<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>;
2076    pointerInUserData ptr \<sigma>\<rbrakk>
2077   \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr"
2078  apply (subgoal_tac " c_guard (Ptr (ptr && ~~ mask 3)::machine_word ptr) \<and>
2079    s \<Turnstile>\<^sub>c (Ptr (ptr && ~~ mask 3)::machine_word ptr) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (Ptr (ptr && ~~ mask 3)) = x" for x)
2080  prefer 2
2081   apply (drule_tac p="ptr && ~~ mask 3" in user_word_at_cross_over[rotated])
2082     apply simp
2083    apply (simp add: user_word_at_def Aligned.is_aligned_neg_mask
2084                     pointerInUserData_def pageBits_def mask_lower_twice)
2085    apply assumption
2086  apply (clarsimp simp: h_val_def from_bytes_def typ_info_word)
2087  apply (drule_tac f="word_rsplit :: machine_word \<Rightarrow> word8 list" in arg_cong)
2088  apply (simp add: word_rsplit_rcat_size word_size)
2089  apply (drule_tac f="\<lambda>xs. xs ! unat (ptr && mask 3)" in arg_cong)
2090  apply (simp add: heap_list_nth unat_mask_3_less_8
2091                   word_plus_and_or_coroll2 add.commute
2092                   hrs_mem_def)
2093  apply (cut_tac p=ptr in unat_mask_3_less_8)
2094  apply (subgoal_tac "(ptr && ~~ mask 3) + (ptr && mask 3) = ptr")
2095   apply (subgoal_tac "!n x. n < 8 \<longrightarrow> (unat (x::machine_word) = n) = (x = of_nat n)")
2096    apply (auto simp add: eval_nat_numeral unat_eq_0 add.commute
2097                elim!: less_SucE)[1]
2098    apply (clarsimp simp add: unat64_eq_of_nat word_bits_def)
2099  apply (simp add: add.commute word_plus_and_or_coroll2)
2100  done
2101
2102lemma cap_get_tag_isCap_ArchObject0:
2103  assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'"
2104  shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap
2105  \<and> (cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap
2106  \<and> (cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap
2107  \<and> (cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap
2108  \<and> (cap_get_tag cap' = scast cap_pdpt_cap) = isPDPointerTableCap cap
2109  \<and> (cap_get_tag cap' = scast cap_pml4_cap) = isPML4Cap cap
2110  \<and> (cap_get_tag cap' = scast cap_io_port_cap) = isIOPortCap cap
2111  \<and> (cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap)
2112  \<and> (cap_get_tag cap' = scast cap_io_port_control_cap) = (isIOPortControlCap cap)"
2113  using cr
2114  apply -
2115  apply (erule ccap_relationE)
2116  apply (simp add: cap_to_H_def cap_lift_def Let_def isArchCap_def)
2117  by (clarsimp simp: isCap_simps cap_tag_defs word_le_nat_alt pageSize_def Let_def split: if_split_asm) \<comment> \<open>takes a while\<close>
2118
2119lemma cap_get_tag_isCap_ArchObject:
2120  assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'"
2121  shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap"
2122  and "(cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap"
2123  and "(cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap"
2124  and "(cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap"
2125  and "(cap_get_tag cap' = scast cap_pdpt_cap) = isPDPointerTableCap cap"
2126  and "(cap_get_tag cap' = scast cap_pml4_cap) = isPML4Cap cap"
2127  and "(cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap)"
2128  and "(cap_get_tag cap' = scast cap_io_port_cap) = isIOPortCap cap"
2129  and "(cap_get_tag cap' = scast cap_io_port_control_cap) = isIOPortControlCap cap"
2130  using cap_get_tag_isCap_ArchObject0 [OF cr] by auto
2131
2132lemma cap_get_tag_isCap_unfolded_H_cap:
2133  shows "ccap_relation (capability.ThreadCap v0) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_thread_cap)"
2134  and "ccap_relation (capability.NullCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_null_cap)"
2135  and "ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_notification_cap) "
2136  and "ccap_relation (capability.EndpointCap v8 v9 v10 v11 v12) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_endpoint_cap)"
2137  and "ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_handler_cap)"
2138  and "ccap_relation (capability.IRQControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_control_cap)"
2139  and "ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_zombie_cap)"
2140  and "ccap_relation (capability.ReplyCap v17 v18) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_reply_cap)"
2141  and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_untyped_cap)"
2142  and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_cnode_cap)"
2143  and "ccap_relation (capability.DomainCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_domain_cap)"
2144
2145  and "ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_control_cap)"
2146  and "ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_pool_cap)"
2147  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v31)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_table_cap)"
2148  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v32 v33)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_directory_cap)"
2149  and "ccap_relation (capability.ArchObjectCap (arch_capability.PDPointerTableCap v34 v35)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_pdpt_cap)"
2150  and "ccap_relation (capability.ArchObjectCap (arch_capability.PML4Cap v36 v37)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_pml4_cap)"
2151  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v101 v44 v45 v46 v47 v48)) cap'  \<Longrightarrow> (cap_get_tag cap' = scast cap_frame_cap)"
2152  and "ccap_relation (capability.ArchObjectCap (arch_capability.IOPortCap v60 v61)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_io_port_cap)"
2153  and "ccap_relation (capability.ArchObjectCap arch_capability.IOPortControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_io_port_control_cap)"
2154  apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps)
2155  apply (frule cap_get_tag_isCap(2), simp)
2156  apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps pageSize_def)+
2157  done
2158
2159lemma cap_get_tag_isCap_ArchObject2_worker:
2160  "\<lbrakk> \<And>cap''. ccap_relation (ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap'';
2161                ccap_relation cap cap'; isArchCap_tag n \<rbrakk>
2162        \<Longrightarrow> (cap_get_tag cap' = n)
2163              = (isArchObjectCap cap \<and> P (capCap cap))"
2164  apply (rule iffI)
2165   apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
2166  apply (clarsimp simp: isCap_simps)
2167  done
2168
2169lemma cap_get_tag_isCap_ArchObject2:
2170  assumes cr: "ccap_relation cap cap'"
2171  shows "(cap_get_tag cap' = scast cap_asid_control_cap)
2172           = (isArchObjectCap cap \<and> isASIDControlCap (capCap cap))"
2173  and   "(cap_get_tag cap' = scast cap_asid_pool_cap)
2174           = (isArchObjectCap cap \<and> isASIDPoolCap (capCap cap))"
2175  and   "(cap_get_tag cap' = scast cap_page_table_cap)
2176           = (isArchObjectCap cap \<and> isPageTableCap (capCap cap))"
2177  and   "(cap_get_tag cap' = scast cap_page_directory_cap)
2178           = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap))"
2179  and   "(cap_get_tag cap' = scast cap_pdpt_cap)
2180           = (isArchObjectCap cap \<and> isPDPointerTableCap (capCap cap))"
2181  and   "(cap_get_tag cap' = scast cap_pml4_cap)
2182           = (isArchObjectCap cap \<and> isPML4Cap (capCap cap))"
2183  and   "(cap_get_tag cap' = scast cap_frame_cap)
2184           = (isArchObjectCap cap \<and> isPageCap (capCap cap))"
2185  and   "(cap_get_tag cap' = scast cap_io_port_cap)
2186           = (isArchObjectCap cap \<and> isIOPortCap (capCap cap))"
2187  and   "(cap_get_tag cap' = scast cap_io_port_control_cap)
2188           = (isArchObjectCap cap \<and> isIOPortControlCap (capCap cap))"
2189  by (rule cap_get_tag_isCap_ArchObject2_worker [OF _ cr],
2190      simp add: cap_get_tag_isCap_ArchObject,
2191      simp add: isArchCap_tag_def2 cap_tag_defs)+
2192
2193schematic_goal cap_io_port_cap_lift_def':
2194  "cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap
2195    \<Longrightarrow> cap_io_port_cap_lift cap =
2196          \<lparr> capIOPortFirstPort_CL = ?first,
2197            capIOPortLastPort_CL = ?last \<rparr>"
2198  by (simp add: cap_io_port_cap_lift_def cap_lift_def cap_tag_defs)
2199
2200schematic_goal cap_frame_cap_lift_def':
2201  "cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_frame_cap
2202    \<Longrightarrow> cap_frame_cap_lift cap =
2203          \<lparr> capFMappedASID_CL = ?mapped_asid,
2204            capFBasePtr_CL = ?base_ptr,
2205            capFSize_CL = ?frame_size,
2206            capFMapType_CL = ?map_type,
2207            capFMappedAddress_CL = ?mapped_address,
2208            capFVMRights_CL = ?vm_rights,
2209            capFIsDevice_CL = ?is_device \<rparr>"
2210  by (simp add: cap_frame_cap_lift_def cap_lift_def cap_tag_defs)
2211
2212lemmas ccap_rel_cap_get_tag_cases_generic =
2213  cap_get_tag_isCap_unfolded_H_cap(1-11)
2214    [OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']]
2215
2216lemmas ccap_rel_cap_get_tag_cases_arch =
2217  cap_get_tag_isCap_unfolded_H_cap(12-20)
2218    [OF back_subst[of "\<lambda>cap. ccap_relation (ArchObjectCap cap) cap'" for cap'],
2219     OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']]
2220
2221lemmas ccap_rel_cap_get_tag_cases_arch' =
2222  ccap_rel_cap_get_tag_cases_arch[OF _ refl]
2223
2224lemmas cap_lift_defs =
2225       cap_untyped_cap_lift_def
2226       cap_endpoint_cap_lift_def
2227       cap_notification_cap_lift_def
2228       cap_reply_cap_lift_def
2229       cap_cnode_cap_lift_def
2230       cap_thread_cap_lift_def
2231       cap_irq_handler_cap_lift_def
2232       cap_zombie_cap_lift_def
2233       cap_frame_cap_lift_def
2234       cap_page_table_cap_lift_def
2235       cap_page_directory_cap_lift_def
2236       cap_pdpt_cap_lift_def
2237       cap_pml4_cap_lift_def
2238       cap_asid_pool_cap_lift_def
2239       cap_io_port_cap_lift_def
2240
2241lemma cap_lift_Some_CapD:
2242  "\<And>c'. cap_lift c = Some (Cap_untyped_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_untyped_cap"
2243  "\<And>c'. cap_lift c = Some (Cap_endpoint_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_endpoint_cap"
2244  "\<And>c'. cap_lift c = Some (Cap_notification_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_notification_cap"
2245  "\<And>c'. cap_lift c = Some (Cap_reply_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_reply_cap"
2246  "\<And>c'. cap_lift c = Some (Cap_cnode_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_cnode_cap"
2247  "\<And>c'. cap_lift c = Some (Cap_thread_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_thread_cap"
2248  "\<And>c'. cap_lift c = Some (Cap_irq_handler_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_irq_handler_cap"
2249  "\<And>c'. cap_lift c = Some (Cap_zombie_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_zombie_cap"
2250  "\<And>c'. cap_lift c = Some (Cap_frame_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_frame_cap"
2251  "\<And>c'. cap_lift c = Some (Cap_page_table_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_table_cap"
2252  "\<And>c'. cap_lift c = Some (Cap_page_directory_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_directory_cap"
2253  "\<And>c'. cap_lift c = Some (Cap_pdpt_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pdpt_cap"
2254  "\<And>c'. cap_lift c = Some (Cap_pml4_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pml4_cap"
2255  "\<And>c'. cap_lift c = Some (Cap_asid_pool_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_asid_pool_cap"
2256  "\<And>c'. cap_lift c = Some (Cap_io_port_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap"
2257  by (auto simp: cap_lifts cap_lift_defs)
2258
2259lemma rf_sr_x64KSSKIMPML4:
2260  "(s, s') \<in> rf_sr \<Longrightarrow> x64KSSKIMPML4 (ksArchState s) = symbol_table ''x64KSSKIMPML4''"
2261  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
2262
2263lemma ghost_assertion_size_logic':
2264  "unat (sz :: machine_word) \<le> gsMaxObjectSize s
2265    \<Longrightarrow> cstate_relation s gs
2266    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs) = 0 \<or>
2267            sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs)"
2268  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def ghost_size_rel_def
2269                     linorder_not_le word_less_nat_alt)
2270
2271lemma ghost_assertion_size_logic:
2272  "unat (sz :: machine_word) \<le> gsMaxObjectSize s
2273    \<Longrightarrow> (s, \<sigma>) \<in> rf_sr
2274    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or>
2275            sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>))"
2276  by (clarsimp simp: rf_sr_def ghost_assertion_size_logic')
2277
2278lemma gs_set_assn_Delete_cstate_relation:
2279  "cstate_relation s (ghost'state_'_update (gs_set_assn cteDeleteOne_'proc v) gs)
2280    = cstate_relation s gs"
2281  apply (cases "ghost'state_' gs")
2282  by (auto simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
2283                 cmachine_state_relation_def ghost_assertion_data_set_def
2284                 ghost_size_rel_def ghost_assertion_data_get_def
2285                 cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def)
2286
2287lemma update_typ_at:
2288  assumes at: "obj_at' P p s"
2289      and tp: "\<forall>obj. P obj \<longrightarrow> koTypeOf (injectKOS obj) = koTypeOf ko"
2290  shows "typ_at' T p' (s \<lparr>ksPSpace := ksPSpace s(p \<mapsto> ko)\<rparr>) = typ_at' T p' s"
2291  using at
2292  by (auto elim!: obj_atE' simp: typ_at'_def ko_wp_at'_def
2293           dest!: tp[rule_format]
2294            simp: project_inject projectKO_eq split: kernel_object.splits if_split_asm,
2295      simp_all add: objBits_def objBitsT_koTypeOf[symmetric] ps_clear_upd
2296               del: objBitsT_koTypeOf)
2297
2298lemma ptr_val_tcb_ptr_mask:
2299  "obj_at' (P :: tcb \<Rightarrow> bool) thread s
2300      \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits)
2301                  = thread"
2302  apply (clarsimp simp: obj_at'_def tcb_ptr_to_ctcb_ptr_def projectKOs)
2303  apply (simp add: is_aligned_add_helper ctcb_offset_defs objBits_simps')
2304  done
2305
2306lemmas ptr_val_tcb_ptr_mask'[simp]
2307    = ptr_val_tcb_ptr_mask[unfolded mask_def tcbBlockSizeBits_def, simplified]
2308
2309lemma typ_uinfo_t_diff_from_typ_name:
2310  "typ_name (typ_info_t TYPE ('a :: c_type)) \<noteq> typ_name (typ_info_t TYPE('b :: c_type))
2311    \<Longrightarrow> typ_uinfo_t (aty :: 'a itself) \<noteq> typ_uinfo_t (bty :: 'b itself)"
2312  by (clarsimp simp: typ_uinfo_t_def td_diff_from_typ_name)
2313
2314declare ptr_add_assertion'[simp] typ_uinfo_t_diff_from_typ_name[simp]
2315
2316lemma clift_array_assertion_imp:
2317  "clift hrs (p :: (('a :: wf_type)['b :: finite]) ptr) = Some v
2318    \<Longrightarrow> htd = hrs_htd hrs
2319    \<Longrightarrow> n \<noteq> 0
2320    \<Longrightarrow> \<exists>i. p' = ptr_add (ptr_coerce p) (int i)
2321        \<and> i + n \<le> CARD('b)
2322    \<Longrightarrow> array_assertion (p' :: 'a ptr) n htd"
2323  apply clarsimp
2324  apply (drule h_t_valid_clift)
2325  apply (drule array_ptr_valid_array_assertionD)
2326  apply (drule_tac j=i in array_assertion_shrink_leftD, simp)
2327  apply (erule array_assertion_shrink_right)
2328  apply simp
2329  done
2330
2331lemma page_map_l4_at_carray_map_relation:
2332  "\<lbrakk> page_map_l4_at' pml4 s; cpspace_pml4e_array_relation (ksPSpace s) hp \<rbrakk>
2333    \<Longrightarrow> clift hp (pml4_Ptr pml4) \<noteq> None"
2334  apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
2335  apply (drule spec, erule iffD1)
2336  apply (clarsimp simp: page_map_l4_at'_def)
2337  apply (drule_tac x="p' && mask pml4Bits >> 3" in spec)
2338  apply (clarsimp simp: shiftr_shiftl1)
2339  apply (drule mp)
2340   apply (simp add: shiftr_over_and_dist mask_def bit_simps
2341                    order_le_less_trans[OF word_and_le1])
2342  apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps
2343                        is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric]
2344                 dest!: obj_at_ko_at' ko_at_projectKO_opt)
2345  done
2346
2347lemma page_map_l4_at_rf_sr:
2348   "\<lbrakk> page_map_l4_at' pml4 s; (s, s') \<in> rf_sr \<rbrakk>
2349    \<Longrightarrow> cslift s' (pml4_Ptr pml4) \<noteq> None"
2350  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2351                     cpspace_relation_def page_map_l4_at_carray_map_relation)
2352
2353lemma pd_pointer_table_at_carray_map_relation:
2354  "\<lbrakk> pd_pointer_table_at' pdpt s; cpspace_pdpte_array_relation (ksPSpace s) hp \<rbrakk>
2355    \<Longrightarrow> clift hp (pdpt_Ptr pdpt) \<noteq> None"
2356  apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
2357  apply (drule spec, erule iffD1)
2358  apply (clarsimp simp: pd_pointer_table_at'_def)
2359  apply (drule_tac x="p' && mask pdptBits >> 3" in spec)
2360  apply (clarsimp simp: shiftr_shiftl1)
2361  apply (drule mp)
2362   apply (simp add: shiftr_over_and_dist mask_def bit_simps
2363                    order_le_less_trans[OF word_and_le1])
2364  apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps
2365                        is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric]
2366                 dest!: obj_at_ko_at' ko_at_projectKO_opt)
2367  done
2368
2369lemma pd_pointer_table_at_rf_sr:
2370   "\<lbrakk> pd_pointer_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
2371    \<Longrightarrow> cslift s' (Ptr pd :: (pdpte_C[512]) ptr) \<noteq> None"
2372  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2373                     cpspace_relation_def pd_pointer_table_at_carray_map_relation)
2374
2375lemma page_directory_at_carray_map_relation:
2376  "\<lbrakk> page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp \<rbrakk>
2377    \<Longrightarrow> clift hp (pd_Ptr pd) \<noteq> None"
2378  apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
2379  apply (drule spec, erule iffD1)
2380  apply (clarsimp simp: page_directory_at'_def)
2381  apply (drule_tac x="p' && mask pdBits >> 3" in spec)
2382  apply (clarsimp simp: shiftr_shiftl1)
2383  apply (drule mp)
2384   apply (simp add: shiftr_over_and_dist mask_def bit_simps
2385                    order_le_less_trans[OF word_and_le1])
2386  apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps
2387                        is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric]
2388                 dest!: obj_at_ko_at' ko_at_projectKO_opt)
2389  done
2390
2391lemma page_directory_at_rf_sr:
2392   "\<lbrakk> page_directory_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
2393    \<Longrightarrow> cslift s' (Ptr pd :: (pde_C[512]) ptr) \<noteq> None"
2394  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2395                     cpspace_relation_def page_directory_at_carray_map_relation)
2396
2397lemma page_table_at_carray_map_relation:
2398  "\<lbrakk> page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp \<rbrakk>
2399    \<Longrightarrow> clift hp (pt_Ptr pt) \<noteq> None"
2400  apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
2401  apply (drule spec, erule iffD1)
2402  apply (clarsimp simp: page_table_at'_def)
2403  apply (drule_tac x="p' && mask ptBits >> 3" in spec)
2404  apply (clarsimp simp: shiftr_shiftl1)
2405  apply (drule mp)
2406   apply (simp add: shiftr_over_and_dist bit_simps mask_def
2407                    order_le_less_trans[OF word_and_le1])
2408  apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def
2409                        bit_simps and_not_mask[symmetric]
2410                        is_aligned_andI1 add.commute word_plus_and_or_coroll2
2411                 dest!: obj_at_ko_at' ko_at_projectKO_opt)
2412  done
2413
2414lemma page_table_at_rf_sr:
2415   "\<lbrakk> page_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
2416    \<Longrightarrow> cslift s' (Ptr pd :: (pte_C[512]) ptr) \<noteq> None"
2417  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2418                     cpspace_relation_def page_table_at_carray_map_relation)
2419
2420lemma gsUntypedZeroRanges_rf_sr:
2421  "\<lbrakk> (start, end) \<in> gsUntypedZeroRanges s; (s, s') \<in> rf_sr \<rbrakk>
2422    \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
2423  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2424                        zero_ranges_are_zero_def)
2425  apply (drule(1) bspec)
2426  apply clarsimp
2427  done
2428
2429lemma ctes_of_untyped_zero_rf_sr:
2430  "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
2431      untyped_ranges_zero' s;
2432      untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk>
2433    \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
2434  apply (erule gsUntypedZeroRanges_rf_sr[rotated])
2435  apply (clarsimp simp: untyped_ranges_zero_inv_def)
2436  apply (rule_tac a=p in ranI)
2437  apply (simp add: map_comp_def cteCaps_of_def)
2438  done
2439
2440lemma heap_list_is_zero_mono:
2441  "heap_list_is_zero hmem p n \<Longrightarrow> n' \<le> n
2442    \<Longrightarrow> heap_list_is_zero hmem p n'"
2443  apply (induct n arbitrary: n' p)
2444   apply simp
2445  apply clarsimp
2446  apply (case_tac n', simp_all)
2447  done
2448
2449lemma heap_list_h_eq_better:
2450  "\<And>p. \<lbrakk> x \<in> {p..+q}; heap_list h q p = heap_list h' q p \<rbrakk>
2451      \<Longrightarrow> h x = h' x"
2452proof (induct q)
2453  case 0 thus ?case by simp
2454next
2455  case (Suc n) thus ?case by (force dest: intvl_neq_start)
2456qed
2457
2458lemma heap_list_is_zero_mono2:
2459  "heap_list_is_zero hmem p n
2460    \<Longrightarrow> {p' ..+ n'} \<le> {p ..+ n}
2461    \<Longrightarrow> heap_list_is_zero hmem p' n'"
2462  using heap_list_h_eq2[where h'="\<lambda>_. 0"]
2463      heap_list_h_eq_better[where h'="\<lambda>_. 0"]
2464  apply (simp(no_asm_use) add: heap_list_rpbs)
2465  apply blast
2466  done
2467
2468lemma invs_urz[elim!]:
2469  "invs' s \<Longrightarrow> untyped_ranges_zero' s"
2470  by (clarsimp simp: invs'_def valid_state'_def)
2471
2472lemma arch_fault_tag_not_fault_tag_simps [simp]:
2473  "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_CapFault) = False"
2474  "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_UserException) = False"
2475  "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_UnknownSyscall) = False"
2476  by (cases arch_fault ; simp add: seL4_Faults seL4_Arch_Faults)+
2477
2478lemma capTCBPtr_eq:
2479  "\<lbrakk> ccap_relation cap cap'; isThreadCap cap \<rbrakk>
2480     \<Longrightarrow> cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap')
2481           = ptr_val (tcb_ptr_to_ctcb_ptr (capTCBPtr cap))"
2482  apply (simp add: cap_get_tag_isCap[symmetric])
2483  apply (drule(1) cap_get_tag_to_H)
2484  apply clarsimp
2485  done
2486
2487lemma rf_sr_sched_action_relation:
2488  "(s, s') \<in> rf_sr
2489   \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))"
2490  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
2491
2492lemma canonical_address_tcb_ptr:
2493  "\<lbrakk>canonical_address t; is_aligned t tcbBlockSizeBits\<rbrakk> \<Longrightarrow>
2494     canonical_address (ptr_val (tcb_ptr_to_ctcb_ptr t))"
2495  apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def)
2496  apply (erule canonical_address_add)
2497    apply (clarsimp simp: objBits_simps' ctcb_offset_defs)+
2498  done
2499
2500lemma canonical_address_ctcb_ptr:
2501  assumes "canonical_address (ctcb_ptr_to_tcb_ptr t)" "is_aligned (ctcb_ptr_to_tcb_ptr t) tcbBlockSizeBits"
2502  shows "canonical_address (ptr_val t)"
2503proof -
2504  from assms(2)[unfolded ctcb_ptr_to_tcb_ptr_def]
2505  have "canonical_address ((ptr_val t - ctcb_offset) + ctcb_offset)"
2506    apply (rule canonical_address_add; simp add: objBits_simps' ctcb_offset_defs)
2507    using assms(1)
2508    by (simp add: ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs)
2509  thus ?thesis by simp
2510qed
2511
2512lemma tcb_and_not_mask_canonical:
2513  "\<lbrakk>pspace_canonical' s; tcb_at' t s; n < tcbBlockSizeBits\<rbrakk> \<Longrightarrow>
2514    tcb_Ptr (sign_extend 47 (ptr_val (tcb_ptr_to_ctcb_ptr t) && ~~ mask n)) =
2515        tcb_ptr_to_ctcb_ptr t"
2516  apply (frule (1) obj_at'_is_canonical)
2517  apply (drule canonical_address_tcb_ptr)
2518   apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' split: if_splits)
2519  apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend)
2520  apply (subgoal_tac "ptr_val (tcb_ptr_to_ctcb_ptr t) && ~~ mask n = ptr_val (tcb_ptr_to_ctcb_ptr t)")
2521   prefer 2
2522   apply (simp add: tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs)
2523   apply (rule is_aligned_neg_mask_eq)
2524   apply (clarsimp simp: obj_at'_def projectKOs objBits_simps')
2525   apply (rule is_aligned_add)
2526    apply (erule is_aligned_weaken, simp)
2527   apply (rule is_aligned_weaken[where x="tcbBlockSizeBits - 1"])
2528    apply (simp add: is_aligned_def objBits_simps')
2529   apply (simp add: objBits_simps')
2530  apply simp
2531  done
2532
2533lemmas tcb_ptr_sign_extend_canonical =
2534      tcb_and_not_mask_canonical[where n=0, simplified mask_def objBits_simps', simplified]
2535
2536lemma fpu_null_state_typ_heap_preservation:
2537  assumes "fpu_null_state_relation s"
2538  assumes "(clift t :: user_fpu_state_C typ_heap) = clift s"
2539  shows "fpu_null_state_relation t"
2540  using assms by (simp add: fpu_null_state_relation_def)
2541
2542(* FIXME: move up to TypHeap? *)
2543lemma lift_t_Some_iff:
2544  "lift_t g hrs p = Some v \<longleftrightarrow> hrs_htd hrs, g \<Turnstile>\<^sub>t p \<and> h_val (hrs_mem hrs) p = v"
2545  unfolding hrs_htd_def hrs_mem_def by (cases hrs) (auto simp: lift_t_if)
2546
2547context
2548  fixes p :: "'a::mem_type ptr"
2549  fixes q :: "'b::c_type ptr"
2550  fixes d g\<^sub>p g\<^sub>q
2551  assumes val_p: "d,g\<^sub>p \<Turnstile>\<^sub>t p"
2552  assumes val_q: "d,g\<^sub>q \<Turnstile>\<^sub>t q"
2553  assumes disj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b)"
2554begin
2555
2556lemma h_val_heap_same_typ_disj:
2557  "h_val (heap_update p v h) q = h_val h q"
2558  using disj by (auto intro: h_val_heap_same[OF val_p val_q]
2559                       simp: tag_disj_def sub_typ_proper_def field_of_t_def typ_tag_lt_def
2560                             field_of_def typ_tag_le_def)
2561
2562lemma h_val_heap_same_hrs_mem_update_typ_disj:
2563  "h_val (hrs_mem (hrs_mem_update (heap_update p v) s)) q = h_val (hrs_mem s) q"
2564  by (simp add: hrs_mem_update h_val_heap_same_typ_disj)
2565
2566end
2567
2568lemma global_ioport_bitmap_relation_def2:
2569  "global_ioport_bitmap_relation (clift hrs) htable \<equiv>
2570      \<exists>ctable. hrs_htd hrs \<Turnstile>\<^sub>t (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts''))
2571        \<and> h_val (hrs_mem hrs) (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts'')) = ctable
2572        \<and> cioport_bitmap_to_H ctable = htable
2573        \<and> ptr_span (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts'')) \<subseteq> kernel_data_refs"
2574  by (clarsimp simp: global_ioport_bitmap_relation_def lift_t_Some_iff)
2575
2576lemma fpu_null_state_relation_def2:
2577  "fpu_null_state_relation hrs \<equiv>
2578    hrs_htd hrs \<Turnstile>\<^sub>t fpu_state_Ptr (symbol_table ''x86KSnullFpuState'')
2579     \<and> h_val (hrs_mem hrs) (fpu_state_Ptr (symbol_table ''x86KSnullFpuState''))
2580         = user_fpu_state_C (ARRAY i. FPUNullState (finite_index i))
2581     \<and> ptr_span (fpu_state_Ptr (symbol_table ''x86KSnullFpuState'')) \<subseteq> kernel_data_refs"
2582  by (clarsimp simp: fpu_null_state_relation_def lift_t_Some_iff)
2583
2584lemma global_ioport_bitmap_heap_update_tag_disj':
2585  fixes p :: "'a::mem_type ptr"
2586  assumes valid: "hrs_htd h, g \<Turnstile>\<^sub>t p"
2587  assumes disj: "typ_uinfo_t TYPE(ioport_table_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
2588  shows "global_ioport_bitmap_relation (clift (hrs_mem_update (heap_update p v) h)) = global_ioport_bitmap_relation (clift h)"
2589  unfolding global_ioport_bitmap_relation_def
2590  using lift_t_heap_update_same[OF valid disj]
2591  by (clarsimp simp: global_ioport_bitmap_relation_def hrs_mem_update_def hrs_htd_def
2592              split: prod.splits)
2593
2594lemma fpu_null_state_heap_update_tag_disj':
2595  fixes p :: "'a::mem_type ptr"
2596  assumes valid: "hrs_htd h, g \<Turnstile>\<^sub>t p"
2597  assumes disj: "typ_uinfo_t TYPE(user_fpu_state_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
2598  shows "fpu_null_state_relation (hrs_mem_update (heap_update p v) h) = fpu_null_state_relation h"
2599  unfolding fpu_null_state_relation_def
2600  using lift_t_heap_update_same[OF valid disj]
2601  by (clarsimp simp: fpu_null_state_relation_def hrs_mem_update_def hrs_htd_def
2602              split: prod.splits)
2603
2604lemmas h_t_valid_nested_fields =
2605  h_t_valid_field[OF h_t_valid_field[OF h_t_valid_field]]
2606  h_t_valid_field[OF h_t_valid_field]
2607  h_t_valid_field
2608
2609lemmas h_t_valid_fields_clift =
2610  h_t_valid_nested_fields[OF h_t_valid_clift]
2611  h_t_valid_clift
2612
2613lemmas global_ioport_bitmap_heap_update_tag_disj_simps =
2614  h_t_valid_fields_clift[THEN global_ioport_bitmap_heap_update_tag_disj'[OF _ tag_disj_via_td_name]]
2615
2616lemmas fpu_null_state_heap_update_tag_disj_simps =
2617  h_t_valid_fields_clift[THEN fpu_null_state_heap_update_tag_disj'[OF _ tag_disj_via_td_name]]
2618
2619end
2620end
2621