1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11(* Kernel init refinement. Currently axiomatised.
12*)
13
14theory ArchKernelInit_AI
15imports
16  "../ADT_AI"
17  "../Tcb_AI"
18  "../Arch_AI"
19begin
20
21context Arch begin global_naming ARM (*FIXME: arch_split*)
22
23text {*
24  Showing that there is a state that satisfies the abstract invariants.
25*}
26
27lemma [simp]: "is_aligned (0x1000 :: word32) 9" by (simp add: is_aligned_def)
28lemma [simp]: "is_aligned (0x2000 :: word32) 9" by (simp add: is_aligned_def)
29
30lemmas ptr_defs = init_tcb_ptr_def idle_thread_ptr_def init_irq_node_ptr_def
31                  init_globals_frame_def init_global_pd_def
32lemmas state_defs = init_A_st_def init_kheap_def init_arch_state_def ptr_defs
33
34lemma [simp]: "is_tcb (TCB t)" by (simp add: is_tcb_def)
35
36lemma [simp]: "ran (empty_cnode n) = {Structures_A.NullCap}"
37  apply (auto simp: ran_def empty_cnode_def)
38  apply (rule_tac x="replicate n False" in exI)
39  apply simp
40  done
41
42lemma empty_cnode_apply[simp]:
43  "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = Structures_A.NullCap)"
44  by (auto simp add: empty_cnode_def)
45
46lemma valid_cs_size_empty[simp]:
47  "valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits)"
48  apply (simp add: valid_cs_size_def)
49  apply (insert wf_empty_bits [of n])
50  apply fastforce
51  done
52
53lemma init_cdt [simp]:
54  "cdt init_A_st = init_cdt"
55  by (simp add: state_defs)
56
57lemma mdp_parent_empty [simp]:
58  "\<not>Map.empty \<Turnstile> x \<rightarrow> y"
59  apply clarsimp
60  apply (drule tranclD)
61  apply (clarsimp simp: cdt_parent_of_def)
62  done
63
64lemma descendants_empty [simp]:
65  "descendants_of x Map.empty = {}"
66  by (clarsimp simp: descendants_of_def)
67
68lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"
69  by (simp add: is_reply_cap_def)
70
71lemma [simp]: "cap_range Structures_A.NullCap = {}"
72  by (simp add: cap_range_def)
73
74lemma pde_mapping_bits_shift:
75  fixes x :: "12 word"
76  shows "x \<noteq> 0 \<Longrightarrow> 2 ^ pde_mapping_bits - 1 < (ucast x << pde_mapping_bits :: word32)"
77  apply (simp only:shiftl_t2n pde_mapping_bits_def)
78  apply (unfold word_less_alt)
79  apply simp
80  apply (unfold word_mult_def)
81  apply simp
82  apply (subst int_word_uint)
83  apply (subst mod_pos_pos_trivial)
84    apply simp
85   apply simp
86   apply (subst uint_up_ucast)
87    apply (simp add: is_up_def source_size_def target_size_def word_size)
88   apply (cut_tac 'a = "12" and x = x in uint_lt2p)
89   apply simp
90  apply (rule order_less_le_trans)
91   prefer 2
92   apply (rule pos_mult_pos_ge)
93    apply (subst uint_up_ucast)
94     apply (simp add: is_up_def source_size_def target_size_def word_size)
95    apply (simp add: word_neq_0_conv word_less_alt)
96   apply simp
97  apply simp
98  done
99
100lemma mask_pde_mapping_bits:
101  "mask 20 = 2^pde_mapping_bits - 1"
102  by (simp add: mask_def pde_mapping_bits_def)
103
104
105
106lemma init_irq_ptrs_ineqs:
107  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
108  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
109                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
110  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
111                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
112proof -
113  have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)"
114    apply (rule order_le_less_trans[OF
115        ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]])
116    apply (simp add: cte_level_bits_def minus_one_norm)
117    done
118  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
119    apply (rule is_aligned_no_wrap'[where sz=14])
120     apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def)
121    apply (rule shiftl_less_t2n[OF P])
122    apply simp
123    done
124  show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
125                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
126    apply (simp only: add_diff_eq[symmetric] add.assoc)
127    apply (rule word_add_le_mono2)
128     apply (simp only: trans [OF shiftl_t2n mult.commute])
129     apply (rule nasty_split_lt[OF P])
130      apply (simp_all add: cte_level_bits_def
131        word_bits_def kernel_base_def init_irq_node_ptr_def)
132    done
133  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
134                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
135    apply (simp only: add_diff_eq[symmetric])
136    apply (rule word_add_le_mono2)
137     apply (rule minus_one_helper3, rule shiftl_less_t2n[OF P])
138     apply simp
139    apply (simp add: kernel_base_def
140      cte_level_bits_def word_bits_def init_irq_node_ptr_def)
141    done
142qed
143
144lemmas init_irq_ptrs_less_ineqs
145   = init_irq_ptrs_ineqs(1)[THEN order_less_le_trans[rotated]]
146     init_irq_ptrs_ineqs(2-3)[THEN order_le_less_trans]
147
148lemmas init_irq_ptrs_all_ineqs[unfolded init_irq_node_ptr_def cte_level_bits_def]
149   = init_irq_ptrs_ineqs(1)[THEN order_trans[rotated]]
150     init_irq_ptrs_ineqs(2-3)[THEN order_trans]
151     init_irq_ptrs_less_ineqs
152     init_irq_ptrs_less_ineqs[THEN less_imp_neq]
153     init_irq_ptrs_less_ineqs[THEN less_imp_neq, THEN not_sym]
154
155lemmas ucast_le_ucast_10_32 = ucast_le_ucast[where 'a=10 and 'b=32,simplified]
156lemma init_irq_ptrs_eq:
157  "((ucast (irq :: irq) << cte_level_bits)
158        = (ucast (irq' :: irq) << cte_level_bits :: word32))
159      = (irq = irq')"
160  apply safe
161  apply (rule ccontr)
162  apply (erule_tac bnd="ucast (max_word :: irq) + 1"
163              in shift_distinct_helper[rotated 3],
164         safe intro!: plus_one_helper2,
165         simp_all add: ucast_le_ucast_10_32 up_ucast_inj_eq,
166         simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
167                       max_word_def)
168  done
169
170lemma in_kernel_base:
171"\<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF\<rbrakk> \<Longrightarrow> (\<forall>y\<in>{kernel_base + m .. n + kernel_base}.
172              kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)"
173  apply (clarsimp simp:)
174  apply (intro conjI)
175   apply (rule ccontr,simp add:not_le)
176   apply (drule(1) le_less_trans)
177   apply (cut_tac is_aligned_no_wrap'[where ptr = kernel_base and off = m
178     and sz = 28,simplified])
179     apply (drule(1) less_le_trans)
180     apply simp
181    apply (simp add:kernel_base_def is_aligned_def)
182   apply (rule ccontr,simp add:not_less)
183   apply (drule less_le_trans[where z = "0x10000000"])
184    apply simp
185   apply simp
186  apply (erule order_trans)
187  apply (simp add:field_simps)
188  apply (rule word_plus_mono_right)
189   apply simp
190  apply (simp add:kernel_base_def)
191  done
192
193lemma pspace_aligned_init_A:
194  "pspace_aligned init_A_st"
195  apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
196                        dom_if_Some cte_level_bits_def)
197  apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
198           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
199  done
200
201lemma pspace_distinct_init_A:
202  "pspace_distinct init_A_st"
203  apply (clarsimp simp: pspace_distinct_def state_defs pageBits_def
204                        empty_cnode_bits kernel_base_def
205                        linorder_not_le cte_level_bits_def
206                  cong: if_cong)
207  apply (safe,
208         simp_all add: init_irq_ptrs_all_ineqs
209                       [simplified kernel_base_def, simplified])[1]
210  apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
211             and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
212             and sz=cte_level_bits in aligned_neq_into_no_overlap;
213         simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
214    apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
215    apply (simp add: is_aligned_def)
216   apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
217   apply (simp add: is_aligned_def)
218  apply (simp add: linorder_not_le)
219  done
220
221lemma caps_of_state_init_A_st_Null:
222  "caps_of_state (init_A_st::'z::state_ext state) x
223     = (if cte_at x (init_A_st::'z::state_ext state) then Some cap.NullCap else None)"
224  apply (subgoal_tac "\<not> cte_wp_at ((\<noteq>) cap.NullCap) x init_A_st")
225   apply (auto simp add: cte_wp_at_caps_of_state)[1]
226  apply (clarsimp, erule cte_wp_atE)
227   apply (auto simp add: state_defs tcb_cap_cases_def split: if_split_asm)
228  done
229
230lemmas cte_wp_at_caps_of_state_eq
231    = cte_wp_at_caps_of_state[where P="(=) cap" for cap]
232
233declare ptrFormPAddr_addFromPPtr[simp]
234
235lemma pspace_respects_device_region_init[simp]:
236  "pspace_respects_device_region init_A_st"
237   apply (clarsimp simp: pspace_respects_device_region_def init_A_st_def init_machine_state_def device_mem_def
238                         in_device_frame_def obj_at_def init_kheap_def a_type_def)
239   apply (rule ext)
240   apply clarsimp
241   done
242
243lemma cap_refs_respects_device_region_init[simp]:
244  "cap_refs_respects_device_region init_A_st"
245   apply (clarsimp simp: cap_refs_respects_device_region_def)
246   apply (frule cte_wp_at_caps_of_state[THEN iffD1])
247   apply clarsimp
248   apply (subst(asm) caps_of_state_init_A_st_Null)
249   apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def)
250   done
251
252lemma invs_A:
253  "invs init_A_st"
254
255  apply (simp add: invs_def)
256  apply (rule conjI)
257   prefer 2
258   apply (simp add: cur_tcb_def state_defs obj_at_def)
259  apply (simp add: valid_state_def)
260  apply (rule conjI)
261   apply (simp add: valid_pspace_def)
262   apply (rule conjI)
263    apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
264                          valid_obj_def valid_vm_rights_def vm_kernel_only_def
265                          dom_if_Some cte_level_bits_def)
266    apply (rule conjI)
267     apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
268                           valid_cap_def obj_at_def valid_tcb_state_def valid_arch_tcb_def
269                           cap_aligned_def word_bits_def valid_ipc_buffer_cap_simps)+
270    apply (clarsimp simp: valid_cs_def word_bits_def cte_level_bits_def
271                          init_irq_ptrs_all_ineqs valid_tcb_def
272                   split: if_split_asm)
273   apply (rule conjI)
274    apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
275                          dom_if_Some cte_level_bits_def)
276    apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
277           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
278   apply (rule conjI)
279    apply (simp add:pspace_distinct_init_A)
280   apply (rule conjI)
281    apply (clarsimp simp: if_live_then_nonz_cap_def obj_at_def state_defs live_def hyp_live_def)
282   apply (rule conjI)
283    apply (clarsimp simp: zombies_final_def cte_wp_at_cases state_defs
284                          tcb_cap_cases_def is_zombie_def)
285   apply (clarsimp simp: sym_refs_def state_refs_of_def state_defs state_hyp_refs_of_def)
286  apply (rule conjI)
287   apply (clarsimp simp: valid_mdb_def init_cdt_def no_mloop_def
288                         mdb_cte_at_def)
289   apply (clarsimp simp: untyped_mdb_def caps_of_state_init_A_st_Null
290                         untyped_inc_def ut_revocable_def
291                         irq_revocable_def reply_master_revocable_def
292                         reply_mdb_def reply_caps_mdb_def
293                         reply_masters_mdb_def)
294   apply (simp add:descendants_inc_def)
295  apply (rule conjI)
296   apply (simp add: valid_ioc_def init_A_st_def init_ioc_def cte_wp_at_cases2)
297   apply (intro allI impI, elim exE conjE)
298   apply (case_tac obj, simp_all add: cap_of_def)
299   apply (clarsimp simp: init_kheap_def split: if_split_asm)
300  apply (rule conjI)
301   apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs valid_arch_idle_def)
302  apply (rule conjI)
303   apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs)
304  apply (rule conjI)
305   apply (clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null)
306  apply (clarsimp simp: valid_reply_caps_def unique_reply_caps_def
307                        has_reply_cap_def pred_tcb_at_def obj_at_def
308                        caps_of_state_init_A_st_Null
309                        cte_wp_at_caps_of_state_eq
310                        valid_reply_masters_def valid_global_refs_def
311                        valid_refs_def[unfolded cte_wp_at_caps_of_state])
312  apply (rule conjI)
313   apply (clarsimp simp: valid_arch_state_def)
314   apply (rule conjI)
315    apply (clarsimp simp: valid_asid_table_def state_defs)
316   apply (rule conjI)
317    apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs
318                          a_type_def)
319   apply (rule conjI)
320    apply (simp add: valid_global_pts_def state_defs)
321   apply (simp add: state_defs is_inv_def)
322  apply (rule conjI)
323   apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
324                         is_cap_table_def wf_empty_bits
325                         init_irq_ptrs_all_ineqs cte_level_bits_def
326                         init_irq_ptrs_eq[unfolded cte_level_bits_def])
327   apply (intro conjI)
328    apply (rule inj_onI)
329    apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def])
330   apply clarsimp
331   apply word_bitwise
332  apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
333                   ran_def cong: rev_conj_cong)
334  apply (rule conjI)
335   apply (clarsimp simp: valid_irq_states_def init_A_st_def init_machine_state_def valid_irq_masks_def init_irq_masks_def)
336  apply (rule conjI)
337   apply (clarsimp simp: valid_machine_state_def init_A_st_def
338                         init_machine_state_def init_underlying_memory_def)
339  apply (rule conjI)
340   apply (clarsimp simp: obj_at_def state_defs valid_vspace_objs_def)
341   apply (clarsimp simp: vs_lookup_def vs_asid_refs_def)
342  apply (rule conjI)
343   apply (clarsimp simp: valid_arch_caps_def)
344   apply (rule conjI)
345    apply (clarsimp simp: valid_vs_lookup_def)
346    apply (clarsimp simp: vs_lookup_pages_def state_defs vs_asid_refs_def)
347   apply (clarsimp simp: valid_table_caps_def caps_of_state_init_A_st_Null
348                         unique_table_caps_def unique_table_refs_def)
349  apply (rule conjI)
350   apply (clarsimp simp: valid_global_objs_def state_defs)
351   apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
352                         valid_pde_mappings_def valid_vso_at_def)
353   apply (simp add: kernel_base_def kernel_mapping_slots_def
354                    Platform.ARM.addrFromPPtr_def physMappingOffset_def
355                    kernelBase_addr_def physBase_def pageBits_def is_aligned_def)
356  apply (rule conjI)
357   apply (simp add: valid_kernel_mappings_def state_defs
358                         valid_kernel_mappings_if_pd_def pde_ref_def
359                         ran_def)
360   apply (auto simp: pde_ref_def split: if_split_asm)[1]
361  apply (rule conjI)
362   apply (clarsimp simp: equal_kernel_mappings_def state_defs obj_at_def)
363  apply (rule conjI)
364   apply (clarsimp simp: valid_asid_map_def state_defs)
365  apply (rule conjI)
366   apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def state_defs
367                         valid_pd_kernel_mappings_def mask_pde_mapping_bits)
368   apply (simp add: valid_pde_kernel_mappings_def kernel_base_def)
369   apply (rule conjI)
370    apply (fastforce simp:pde_mapping_bits_def)
371   apply (intro ballI impI)
372   apply (clarsimp simp:pde_mapping_bits_def)
373   apply word_bitwise
374   apply clarsimp
375  apply (rule conjI)
376   apply (clarsimp simp: pspace_in_kernel_window_def state_defs mask_def)
377   apply (intro conjI impI)
378            apply (rule in_kernel_base|simp)+
379         apply (erule exE,drule sym,simp add:field_simps)
380         apply (rule in_kernel_base[simplified add.commute])
381          apply (rule word_less_add_right, simp add: cte_level_bits_def)
382           apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
383          apply simp
384         apply (simp add:cte_level_bits_def field_simps)
385         apply (subst add.commute)
386         apply (rule le_plus')
387          apply simp+
388          apply (rule less_imp_le)
389          apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
390     apply (rule in_kernel_base|simp)+
391  apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
392                  valid_refs_def[unfolded cte_wp_at_caps_of_state])
393  done
394
395end
396
397end
398