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