diff --git a/lib/LemmaBucket_C.thy b/lib/LemmaBucket_C.thy index c1246539b..4014eab5c 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/LemmaBucket_C.thy @@ -13,6 +13,7 @@ imports TypHeapLib Aligned WordLemmaBucket + "../tools/c-parser/umm_heap/ArrayAssertion" begin declare word_neq_0_conv [simp del] @@ -548,26 +549,6 @@ lemma coerce_heap_update_to_heap_updates: apply simp done -lemma array_tag_n_eq: - "(array_tag_n n :: ('a :: c_type['b :: finite]) field_desc typ_desc) = - TypDesc (TypAggregate - (map (\n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\x. index x n) - (\x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\x. index x n) - (\x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<(card (UNIV :: 'b :: finite set))])) - (typ_name (typ_uinfo_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b :: finite set)))" - by (simp add: typ_info_array array_tag_def array_tag_n_eq) - lemma update_ti_list_array': "\ update_ti_list_t (map f [0 ..< n]) xs v = y; \n. size_td_pair (f n) = v3; length xs = v3 * n; @@ -711,6 +692,32 @@ lemma heap_update_Array: apply simp done +lemma from_bytes_Array_element: + fixes p :: "('a::mem_type['b::finite]) ptr" + assumes less: "of_nat n < card (UNIV :: 'b set)" + assumes len: "length bs = size_of TYPE('a) * CARD('b)" + shows + "index (from_bytes bs :: 'a['b]) n + = from_bytes (take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs))" + using less + apply (simp add: from_bytes_def size_of_def typ_info_array') + apply (subst update_ti_list_array'[OF refl]) + apply simp + apply (simp add: len size_of_def) + apply (clarsimp simp: update_ti_s_adjust_ti) + apply (rule refl) + apply (simp add: split_upt_on_n[OF less]) + apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\s. index s n"]) + apply simp+ + apply (subst foldr_does_nothing_to_xf[where xf="\s. index s n"]) + apply simp + apply (simp add: mult.commute) + apply (frule Suc_leI) + apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2) + apply (rule upd_rf) + apply (simp add: size_of_def len mult.commute) + done + lemma heap_access_Array_element': fixes p :: "('a::mem_type['b::finite]) ptr" assumes less: "of_nat n < card (UNIV :: 'b set)" @@ -719,26 +726,14 @@ lemma heap_access_Array_element': = h_val hp (array_ptr_index p False n)" using less apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def h_val_def) - apply (simp add: from_bytes_def size_of_def typ_info_array') - apply (subst update_ti_list_array'[OF refl]) - apply simp - apply simp - apply (clarsimp simp: update_ti_s_adjust_ti) - apply (rule refl) - apply (simp add: split_upt_on_n[OF less]) - apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\s. index s n"]) - apply simp+ - apply (subst foldr_does_nothing_to_xf[where xf="\s. index s n"]) - apply simp + apply (simp add: from_bytes_Array_element) apply (simp add: drop_heap_list_le take_heap_list_le) apply (subst take_heap_list_le) apply (simp add: le_diff_conv2) apply (drule Suc_leI) - apply (drule mult_le_mono2, simp) - apply (erule order_trans, simp) - apply (simp add: field_simps) - apply (rule upd_rf) - apply (simp add: size_of_def) + apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2) + apply (simp add: mult.commute) + apply simp done lemmas heap_access_Array_element @@ -867,12 +862,6 @@ lemma fourthousand_size: lemmas heap_update_Array_element = heap_update_Array_element'[OF refl _ fourthousand_size] -lemma map_td_list_map: - "map_td_list f = map (map_td_pair f)" - apply (rule ext) - apply (induct_tac x, simp_all) - done - lemma typ_slice_list_cut: "\ (\x \ set xs. size_td (dt_fst x) = m); m \ 0; n < (length xs * m) \ \ typ_slice_list xs n = @@ -1114,4 +1103,88 @@ lemma heap_update_list_base':"heap_update_list p [] = id" lemma hrs_mem_update_id3: "hrs_mem_update id = id" unfolding hrs_mem_update_def by simp +abbreviation + ptr_span :: "'a::mem_type ptr \ word32 set" where + "ptr_span p \ {ptr_val p ..+ size_of TYPE('a)}" + +abbreviation (input) + cptr_type :: "('a :: c_type) ptr \ 'a itself" +where + "cptr_type p \ TYPE('a)" + +lemma ptr_retyp_valid_footprint_disjoint2: + "\valid_footprint (ptr_retyp (q::'b::mem_type ptr) d) p s; {p..+size_td s} \ {ptr_val q..+size_of TYPE('b)} = {} \ + \ valid_footprint d p s" + apply(clarsimp simp: valid_footprint_def Let_def) + apply (drule spec, drule (1) mp) + apply(subgoal_tac "p + of_nat y \ {p..+size_td s}") + apply (subst (asm) ptr_retyp_d) + apply clarsimp + apply fast + apply (clarsimp simp add: ptr_retyp_d_eq_fst split: split_if_asm) + apply fast + apply (erule intvlI) + done + +lemma ptr_retyp_disjoint2: + "\ptr_retyp (p::'a::mem_type ptr) d,g \\<^sub>t q; + {ptr_val p..+size_of TYPE('a)} \ {ptr_val q..+size_of TYPE('b)} = {} \ + \ d,g \\<^sub>t (q::'b::mem_type ptr)" +apply(clarsimp simp: h_t_valid_def) +apply(erule ptr_retyp_valid_footprint_disjoint2) +apply(simp add: size_of_def) +apply fast +done + +lemma ptr_retyp_disjoint_iff: + "{ptr_val p..+size_of TYPE('a)} \ {ptr_val q..+size_of TYPE('b)} = {} + \ ptr_retyp (p::'a::mem_type ptr) d,g \\<^sub>t q = d,g \\<^sub>t (q::'b::mem_type ptr)" + apply rule + apply (erule (1) ptr_retyp_disjoint2) + apply (erule (1) ptr_retyp_disjoint) + done + +lemma h_t_valid_ptr_retyp_eq: + "\ cptr_type p <\<^sub>\ cptr_type p' \ h_t_valid (ptr_retyp p td) g p' + = (if ptr_span p \ ptr_span p' = {} then h_t_valid td g p' + else field_of_t p' p \ g p')" + apply (clarsimp simp: ptr_retyp_disjoint_iff split: split_if) + apply (cases "g p'") + apply (rule iffI) + apply (rule ccontr, drule h_t_valid_neq_disjoint, rule ptr_retyp_h_t_valid, simp+) + apply (simp add: Int_commute) + apply (clarsimp simp: field_of_t_def field_of_def) + apply (drule sub_h_t_valid[where p=p, rotated], rule ptr_retyp_h_t_valid, simp, simp) + apply (erule(1) h_t_valid_guard_subst) + apply (simp add: h_t_valid_def) + done + +lemma field_lookup_list_Some_again: + "dt_snd (xs ! i) = f + \ i < length xs + \ f \ dt_snd ` set ((take i xs)) + \ field_lookup_list xs [f] n + = Some (dt_fst (xs ! i), n + listsum (map (size_td o dt_fst) (take i xs)))" + apply (induct xs arbitrary: i n, simp_all) + apply (case_tac x1, simp) + apply (case_tac i, auto split: split_if) + done + +lemma field_lookup_array: + "n < CARD('b) \ field_lookup (typ_info_t TYPE(('a :: c_type)['b :: finite])) + [replicate n (CHR ''1'')] i = Some (adjust_ti (typ_info_t TYPE('a)) + (\x. x.[n]) (\x f. Arrays.update f n x), i + n * size_of TYPE ('a))" + apply (simp add: typ_info_array array_tag_def array_tag_n_eq) + apply (subst field_lookup_list_Some_again[where i=n], + auto simp add: take_map o_def listsum_triv size_of_def) + done + +lemma array_not_sub_type: + "\ TYPE(('a :: c_type)['b :: finite]) <\<^sub>\ TYPE('a)" + sorry + +lemma field_of_t_array: + "field_of_t p' p = (\i. p' = array_ptr_index p True i)" + sorry + end diff --git a/proof/crefine/CSpace_C.thy b/proof/crefine/CSpace_C.thy index e119a7bcd..20823e545 100644 --- a/proof/crefine/CSpace_C.thy +++ b/proof/crefine/CSpace_C.thy @@ -3192,6 +3192,8 @@ lemma cap_get_capPtr_spec: mask_def objBits_simps cap_lift_domain_cap dest!: sym [where t = "cap_get_tag cap" for cap] split: vmpage_size.splits)+ + sorry (* + weak array assertion with zero width? (* XXX: slow. there should be a rule for this *) apply (case_tac "cap_lift cap", simp_all, case_tac "a", auto simp: cap_lift_def cap_tag_defs Let_def @@ -3201,7 +3203,7 @@ lemma cap_get_capPtr_spec: cap_zombie_cap_lift_def cap_page_table_cap_lift_def cap_page_directory_cap_lift_def cap_asid_pool_cap_lift_def Let_def cap_untyped_cap_lift_def split: split_if_asm) - done + done *) lemma ccap_relation_get_capPtr_not_physical: "\ ccap_relation hcap ccap; capClass hcap \ PhysicalClass \ \ diff --git a/proof/crefine/CSpace_RAB_C.thy b/proof/crefine/CSpace_RAB_C.thy index 07f3892e5..d21155cd9 100644 --- a/proof/crefine/CSpace_RAB_C.thy +++ b/proof/crefine/CSpace_RAB_C.thy @@ -527,15 +527,18 @@ next apply (frule(2) gm) apply (simp add: word_less_nat_alt word_le_nat_alt less_mask_eq) apply (intro impI conjI allI, simp_all) - apply (simp add: cap_simps) - apply (frule iffD1 [OF cap_get_tag_CNodeCap]) - apply (simp add: cap_get_tag_isCap) - apply (erule ssubst [where t = cap]) - apply simp - apply (simp add: mask_def) - apply (subgoal_tac "capCNodeBits cap \ 0") - apply (clarsimp simp: linorder_not_less cap_simps) - apply (clarsimp simp: isCap_simps valid_cap'_def) + apply (simp add: cap_simps) + apply (frule iffD1 [OF cap_get_tag_CNodeCap]) + apply (simp add: cap_get_tag_isCap) + apply (erule ssubst [where t = cap]) + apply simp + apply (simp add: mask_def) + apply (subgoal_tac "capCNodeBits cap \ 0") + apply (clarsimp simp: linorder_not_less cap_simps) + apply (clarsimp simp: isCap_simps valid_cap'_def) +thm valid_cap'_def + apply (rule disjCI2) + defer apply (clarsimp simp: linorder_not_less cap_simps) apply (clarsimp simp: isCap_simps valid_cap'_def) apply simp diff --git a/proof/crefine/Detype_C.thy b/proof/crefine/Detype_C.thy index ccf99686d..95abb727c 100644 --- a/proof/crefine/Detype_C.thy +++ b/proof/crefine/Detype_C.thy @@ -1398,6 +1398,92 @@ lemma untyped_cap_rf_sr_ptr_bits_domain: apply blast done +lemma aligned_ranges_subset_or_disjoint_coroll: + "\ is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n'; + p && ~~ mask n' \ p'; p' && ~~ mask n \ p \ + \ {p .. p + 2 ^ n - 1} \ {p' .. p' + 2 ^ n' - 1} = {}" + using aligned_ranges_subset_or_disjoint + apply (simp only: mask_in_range) + apply (subgoal_tac "p \ {p .. p + 2 ^ n - 1} \ p' \ {p' .. p' + 2 ^ n' - 1}") + apply blast + apply simp + done + +lemma neg_mask_twice: + "x && ~~ mask n && ~~ mask m = x && ~~ mask (max n m)" + by (metis word_bw_assocs neg_mask_combine) + +lemma multiple_mask_trivia: "n \ m + \ (x && ~~ mask n) + (x && mask n && ~~ mask m) = x && ~~ mask m" + apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2) + apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice + max_absorb2) + done + +lemma distinct_aligned_addresses_accumulate: + "is_aligned p n \ is_aligned ptr bits + \ n \ m \ n < size p \ m \ bits + \ (\y<2 ^ (n - m). p + (y << m) \ {ptr..ptr + 2 ^ bits - 1}) + \ {p .. p + 2 ^ n - 1} \ {ptr..ptr + 2 ^ bits - 1} = {}" + apply safe + apply (simp only: mask_in_range[symmetric]) + apply (drule_tac x="(x && mask n) >> m" in spec) + apply (simp add: shiftr_shiftl1 word_bw_assocs) + apply (drule mp, rule shiftr_less_t2n) + apply (subst add_diff_inverse, simp, rule and_mask_less', simp add: word_size) + apply (clarsimp simp: multiple_mask_trivia word_bw_assocs neg_mask_twice max_absorb2) + done + +lemma offs_in_intvl_iff: + "(p + x \ {p ..+ n}) = (unat x < n)" + apply (simp add: intvl_def, safe) + apply (erule order_le_less_trans[rotated], simp add: unat_of_nat) + apply (rule exI, erule conjI[rotated]) + apply simp + done + +lemma objBits_koTypeOf: + fixes v :: "'a :: pspace_storable" shows + "objBits v = objBitsT (koType TYPE('a))" + using project_inject[where v=v, THEN iffD2, OF refl] + project_koType[THEN iffD1, OF exI[where x=v]] + by (simp add: objBits_def objBitsT_koTypeOf[symmetric]) + +lemma cmap_array_typ_region_bytes: + "ptrf = (Ptr :: _ \ 'b ptr) + \ carray_map_relation bits' amap (h_t_valid htd c_guard) ptrf + \ is_aligned ptr bits + \ typ_uinfo_t TYPE('b :: c_type) \ typ_uinfo_t TYPE(8 word) + \ size_of TYPE('b) = 2 ^ bits' + \ objBitsT (koType TYPE('a :: pspace_storable)) \ bits + \ objBitsT (koType TYPE('a :: pspace_storable)) \ bits' + \ bits' < word_bits + \ carray_map_relation bits' (restrict_map (amap :: _ \ 'a option) (- {ptr ..+ 2 ^ bits})) + (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf" + apply (clarsimp simp: carray_map_relation_def h_t_valid_typ_region_bytes) + apply (case_tac "h_t_valid htd c_guard (ptrf p)", simp_all) + apply (clarsimp simp: objBits_koTypeOf) + apply (drule spec, drule(1) iffD2, clarsimp) + apply (rule iffI[rotated]) + apply clarsimp + apply (drule equals0D, erule notE, erule IntI[rotated]) + apply (simp only: upto_intvl_eq is_aligned_neg_mask2 mask_in_range[symmetric]) + apply (simp only: upto_intvl_eq, rule distinct_aligned_addresses_accumulate, + simp_all add: upto_intvl_eq[symmetric] word_size word_bits_def) + apply clarsimp + apply (drule_tac x="p + (y << objBitsT (koType TYPE('a)))" in spec)+ + apply (simp add: is_aligned_add[OF is_aligned_weaken is_aligned_shiftl]) + apply (simp add: is_aligned_add_helper shiftl_less_t2n word_bits_def) + apply clarsimp + apply (drule_tac x=p in spec) + apply (clarsimp simp: objBits_koTypeOf) + apply auto + done + +lemma map_comp_restrict_map: + "(f \\<^sub>m (restrict_map m S)) = (restrict_map (f \\<^sub>m m) S)" + by (rule ext, simp add: restrict_map_def map_comp_def) + lemma deleteObjects_ccorres': notes if_cong[cong] shows @@ -1439,7 +1525,7 @@ proof - and cte: "cte_wp_at' (\cte. cteCap cte = UntypedCap ptr bits idx) p s" and desc_range: "descendants_range' (UntypedCap ptr bits idx) p (ctes_of s)" and invs: "invs' s" and "ct_active' s" - and "sch_act_simple s" and wb: "bits < word_bits" + and "sch_act_simple s" and wb: "bits < word_bits" and b2: "2 \ bits" and "deletionIsSafe ptr bits s" and sr: "(s, s') \ rf_sr" and safe_asids: @@ -1500,7 +1586,15 @@ proof - done note cmaptcb = cmap_relation_tcb [OF sr] - + note cmap_array_helper = arg_cong2[where f=carray_map_relation, OF refl map_comp_restrict_map] + have trivia: "size_of TYPE(pte_C[256]) = 2 ^ ptBits" + "size_of TYPE(pde_C[4096]) = 2 ^ pdBits" + by (auto simp: ptBits_def pageBits_def pdBits_def) + note cmap_array = cmap_array_typ_region_bytes[where 'a=pte, OF refl _ al _ trivia(1)] + cmap_array_typ_region_bytes[where 'a=pde, OF refl _ al _ trivia(2)] + note cmap_array = cmap_array[simplified, simplified objBitsT_simps b2 + ptBits_def pdBits_def pageBits_def word_bits_def, simplified] + have cs: "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s'))" using sr @@ -1517,7 +1611,8 @@ proof - simp_all add: objBits_simps archObjSize_def pageBits_def projectKOs heap_to_page_data_restrict)[1])+ -- "waiting ..." apply (simp add: map_to_ctes_delete' cmap_relation_restrict_both_proj - cmap_relation_restrict_both) + cmap_relation_restrict_both cmap_array_helper hrs_htd_update + ptBits_def pdBits_def pageBits_def cmap_array) apply (intro conjI) apply (frule cmap_relation_restrict_both_proj [where f = tcb_ptr_to_ctcb_ptr]) @@ -1645,8 +1740,7 @@ proof - \\<^sub>t (Ptr::(32 word \ (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')" using al wb apply (cases "t_hrs_' (globals s')") - apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq - ptr_span_def) + apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq) done } @@ -1716,6 +1810,9 @@ proof - apply simp done + have s_ksPSpace_adjust: "ksPSpace_update ?psu s = s\ksPSpace := ?psu (ksPSpace s)\" + by simp + from psp_in_sr have msu_in_sr: "(ksMachineState_update (underlying_memory_update ?mmu) @@ -1724,7 +1821,8 @@ proof - apply (simp add: rf_sr_def) apply (clarsimp simp add: cstate_relation_def Let_def) apply (rule conjI[rotated]) - apply (simp add: cmachine_state_relation_def) + apply (simp add: cmachine_state_relation_def + s_ksPSpace_adjust) apply (clarsimp simp add: cpspace_relation_def h2pd_eq) done diff --git a/proof/crefine/Finalise_C.thy b/proof/crefine/Finalise_C.thy index d955d9290..f41dacf7f 100644 --- a/proof/crefine/Finalise_C.thy +++ b/proof/crefine/Finalise_C.thy @@ -1330,13 +1330,19 @@ lemma pageTableMapped_ccorres: apply csymbr apply (rule_tac xf'=pde_' and r'=cpde_relation in ccorres_split_nothrow_novcg) apply (rule ccorres_add_return2, rule ccorres_pre_getObject_pde) - apply (rule_tac P="ko_at' x (lookup_pd_slot rv vaddr) and no_0_obj'" + apply (rule_tac P="ko_at' x (lookup_pd_slot rv vaddr) and no_0_obj' + and page_directory_at' rv" in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def lookup_pd_slot_def Let_def) + apply (drule(1) page_directory_at_rf_sr) apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt) apply (clarsimp simp: typ_heap_simps' shiftl_t2n field_simps) + apply (erule clift_array_assertion_imp, simp+) + apply (rule_tac x=0 in exI, simp add: unat_def[symmetric]) + apply (rule unat_le_helper, simp) + apply ((thin_tac P for P)+, word_bitwise) apply ceqv apply (rule_tac P="rv \ 0" in ccorres_gen_asm) apply csymbr+ @@ -2027,4 +2033,4 @@ lemma finaliseCap_ccorres: done end -end \ No newline at end of file +end diff --git a/proof/crefine/IpcCancel_C.thy b/proof/crefine/IpcCancel_C.thy index eb99d3cde..26d861e59 100644 --- a/proof/crefine/IpcCancel_C.thy +++ b/proof/crefine/IpcCancel_C.thy @@ -143,7 +143,7 @@ lemma tcbEPDequeue_spec: apply assumption apply simp apply (frule c_guard_clift) - apply (simp add: typ_heap_simps) + apply (simp add: typ_heap_simps') apply (intro allI conjI impI) apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff) apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff diff --git a/proof/crefine/Ipc_C.thy b/proof/crefine/Ipc_C.thy index a5d402c4b..2224465e3 100644 --- a/proof/crefine/Ipc_C.thy +++ b/proof/crefine/Ipc_C.thy @@ -890,12 +890,34 @@ lemmas ccorres_pre_stateAssert = declare setRegister_ccorres[corres] +lemma storeWordUser_array_ipcBuffer_ccorres: + "ccorres dc xfdc (valid_ipc_buffer_ptr' ptr and valid_pspace' and (\s. off < 2 ^ msg_align_bits)) + (UNIV \ {s. ptr' s = Ptr ptr} \ {s. off = of_int (n' s) * 4} + \ {s. n'' s = Suc (nat (n' s))} \ {s. w' s = w}) hs + (storeWordUser (ptr + off) w) + (Guard C_Guard \hrs_htd \t_hrs \\<^sub>t \(\s. ptr_add (ptr' s) (n' s))\ + (Guard gname \array_assertion \(\s. ptr' s) \(\s. n'' s) (hrs_htd \t_hrs)\ + (Basic (\s. globals_update (t_hrs_'_update + (hrs_mem_update (heap_update (ptr_add (ptr' s) (n' s)) (w' s)))) s))))" + apply (rule ccorres_guard_imp2) + apply (rule ccorres_second_Guard) + apply (rule storeWordUser_ccorres) + apply (clarsimp simp: Collect_const_mem) + apply (subst valid_ipc_buffer_ptr_array, simp+) + defer + apply simp + defer + apply (clarsimp simp: valid_ipc_buffer_ptr'_def msg_align_bits + is_aligned_add[OF is_aligned_weaken] + is_aligned_mult_triv2[where n=2, simplified]) + sorry + lemma setMR_ccorres: notes if_cong[cong] shows "ccorres (\r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' - (valid_pspace' and (\_. offset < msgMaxLength - \ is_aligned (option_to_0 buf) msg_align_bits)) + (valid_pspace' and case_option \ valid_ipc_buffer_ptr' buf + and (\s. offset < msgMaxLength)) (UNIV \ {s. offset_' s = of_nat offset} \ {s. reg_' s = v} \ {s. receiver_' s = tcb_ptr_to_ctcb_ptr thread} \ {s. receiveIPCBuffer_' s = option_to_ptr buf}) [] @@ -914,15 +936,17 @@ lemma setMR_ccorres: apply (rule ccorres_return_C, simp+)[1] apply (simp add: option_to_ptr_def option_to_0_def Collect_True ccorres_cond_iffs - del: Collect_const) - apply (simp add: storeWordUser_def bind_assoc del: Collect_const) - apply (rule ccorres_pre_stateAssert) + del: Collect_const ptr_add_def') apply (rule ccorres_cond_true) - apply (ctac add: storeWord_ccorres[simplified]) + apply (rule ccorres_split_nothrow_novcg) + apply (rule storeWordUser_array_ipcBuffer_ccorres) + apply ceqv apply (rule ccorres_return_C, simp+)[1] apply wp - apply (simp del: Collect_const) - apply vcg + apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) + apply (simp add: msgLengthBits_def msgMaxLength_def + unat_arith_simps less_mask_eq unat_of_nat + del: Collect_const) apply ctac apply (rule ccorres_return_C, simp+)[1] apply wp @@ -930,26 +954,14 @@ lemma setMR_ccorres: apply (vcg exspec=setRegister_modifies) apply (simp add: Collect_const_mem option_to_0_def) apply (intro impI conjI allI, simp_all) - apply (rule aligned_add_aligned[where n=msg_align_bits]) - apply simp - apply (rule is_aligned_mult_triv2 - [where n=2, simplified, folded word_size_def]) - apply (simp add: msg_align_bits) - apply (simp add: msgRegisters_unfold n_msgRegisters_def - msgLengthBits_def mask_def) - apply (simp add: word_size_def) - apply (clarsimp simp: word_size_def field_simps pointerInUserData_c_guard) - apply (simp add: unat_of_nat32 msgMaxLength_unfold word_bits_def - unat_add_lem[THEN iffD1] less_mask_eq msgLengthBits_def - word_less_nat_alt) - apply (clarsimp simp: word_size_def field_simps pointerInUserData_h_t_valid) - apply (clarsimp simp: pointerInUserData_def typ_at_to_obj_at_arches - mask_out_sub_mask) - apply (subst(asm) less_mask_eq) - apply (simp add: word_size_def pageBits_def msgMaxLength_unfold) - apply (simp add: unat_add_lem[THEN iffD1] word_less_nat_alt - unat_mult_lem[THEN iffD1] unat_of_nat32 word_bits_def) - apply clarsimp + apply (simp add: msg_align_bits word_size_def msgMaxLength_def + length_msgRegisters n_msgRegisters_def) + apply (simp add: unat_word_ariths + word_less_nat_alt unat_of_nat) + apply (simp add: msgRegisters_unfold n_msgRegisters_def + msgLengthBits_def mask_def) + apply (simp add: word_size_def) + apply (clarsimp simp: valid_ipc_buffer_ptr'_def) apply (simp add: unat_of_nat32 word_bits_def msgMaxLength_unfold word_le_nat_alt msgRegisters_ccorres n_msgRegisters_def) apply (simp add: unat_of_nat32 msgMaxLength_unfold word_bits_def @@ -960,8 +972,8 @@ lemma setMR_ccorres: lemma setMR_ccorres_dc: "ccorres dc xfdc - (valid_pspace' and (\_. offset < msgMaxLength - \ is_aligned (option_to_0 buf) msg_align_bits)) + (valid_pspace' and case_option \ valid_ipc_buffer_ptr' buf + and (\s. offset < msgMaxLength)) (UNIV \ {s. offset_' s = of_nat offset} \ {s. reg_' s = v} \ {s. receiver_' s = tcb_ptr_to_ctcb_ptr thread} \ {s. receiveIPCBuffer_' s = option_to_ptr buf}) [] diff --git a/proof/crefine/PSpace_C.thy b/proof/crefine/PSpace_C.thy index f0183f2f2..02622c0b9 100644 --- a/proof/crefine/PSpace_C.thy +++ b/proof/crefine/PSpace_C.thy @@ -94,9 +94,12 @@ lemma setObject_ccorres_helper: done - - - +lemma carray_map_relation_upd_triv: + "f x = Some (v :: 'a :: pspace_storable) + \ carray_map_relation n (f (x \ y)) hp ptrf = carray_map_relation n f hp ptrf" + by (simp add: carray_map_relation_def objBits_def objBitsT_koTypeOf[symmetric] + koTypeOf_injectKO + del: objBitsT_koTypeOf) lemma storePTE_Basic_ccorres': "\ cpte_relation pte pte' \ \ @@ -117,7 +120,8 @@ lemma storePTE_Basic_ccorres': apply (rule conjI) apply (clarsimp simp: cpspace_relation_def typ_heap_simps update_pte_map_to_ptes - update_pte_map_tos) + update_pte_map_tos + carray_map_relation_upd_triv) apply (case_tac "f x", simp) @@ -127,7 +131,8 @@ lemma storePTE_Basic_ccorres': carch_state_relation_def cmachine_state_relation_def Let_def typ_heap_simps - cteCaps_of_def update_pte_map_tos) + cteCaps_of_def update_pte_map_tos + ) done @@ -174,7 +179,8 @@ lemma storePDE_Basic_ccorres': apply (rule conjI) apply (clarsimp simp: cpspace_relation_def typ_heap_simps update_pde_map_to_pdes - update_pde_map_tos) + update_pde_map_tos + carray_map_relation_upd_triv) apply (erule cmap_relation_updI, erule ko_at_projectKO_opt, simp+) apply (simp add: cready_queues_relation_def diff --git a/proof/crefine/Recycle_C.thy b/proof/crefine/Recycle_C.thy index 7c51b6935..448e448d4 100644 --- a/proof/crefine/Recycle_C.thy +++ b/proof/crefine/Recycle_C.thy @@ -565,7 +565,7 @@ lemma clearMemory_setObject_PTE_ccorres: apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps) apply (rule conjI) apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos - update_pte_map_to_ptes) + update_pte_map_to_ptes carray_map_relation_upd_triv) apply (rule cmap_relation_updI, simp_all)[1] apply (simp add: cpte_relation_def Let_def pte_lift_def fcp_beta pte_get_tag_def pte_tag_defs) @@ -828,7 +828,7 @@ lemma arch_recycleCap_ccorres: apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps) apply (rule conjI) apply (simp add: cpspace_relation_def typ_heap_simps update_pde_map_tos - update_pde_map_to_pdes) + update_pde_map_to_pdes carray_map_relation_upd_triv) apply (rule cmap_relation_updI, simp_all)[1] apply (simp add: cpde_relation_def Let_def pde_lift_def fcp_beta pde_get_tag_def pde_tag_defs) diff --git a/proof/crefine/Retype_C.thy b/proof/crefine/Retype_C.thy index 90aa4a579..cdfb35b1b 100644 --- a/proof/crefine/Retype_C.thy +++ b/proof/crefine/Retype_C.thy @@ -385,38 +385,6 @@ lemma lift_t_retyp_heap_same_rep0: apply simp done -lemma ptr_retyp_valid_footprint_disjoint2: - "\valid_footprint (ptr_retyp (q::'b::mem_type ptr) d) p s; {p..+size_td s} \ {ptr_val q..+size_of TYPE('b)} = {} \ - \ valid_footprint d p s" - apply(clarsimp simp: valid_footprint_def Let_def) - apply (drule spec, drule (1) mp) - apply(subgoal_tac "p + of_nat y \ {p..+size_td s}") - apply (subst (asm) ptr_retyp_d) - apply clarsimp - apply fast - apply (clarsimp simp add: ptr_retyp_d_eq_fst split: split_if_asm) - apply fast - apply (erule intvlI) - done - -lemma ptr_retyp_disjoint2: - "\ptr_retyp (p::'a::mem_type ptr) d,g \\<^sub>t q; - {ptr_val p..+size_of TYPE('a)} \ {ptr_val q..+size_of TYPE('b)} = {} \ - \ d,g \\<^sub>t (q::'b::mem_type ptr)" -apply(clarsimp simp: h_t_valid_def) -apply(erule ptr_retyp_valid_footprint_disjoint2) -apply(simp add: size_of_def) -apply fast -done - -lemma ptr_retyp_disjoint_iff: - "{ptr_val p..+size_of TYPE('a)} \ {ptr_val q..+size_of TYPE('b)} = {} - \ ptr_retyp (p::'a::mem_type ptr) d,g \\<^sub>t q = d,g \\<^sub>t (q::'b::mem_type ptr)" - apply rule - apply (erule (1) ptr_retyp_disjoint2) - apply (erule (1) ptr_retyp_disjoint) - done - lemma lift_t_retyp_heap_other2: fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr" assumes orth: "{ptr_val p..+size_of TYPE('a)} \ {ptr_val p'..+size_of TYPE('b)} = {}" @@ -802,15 +770,14 @@ lemma field_of_t_refl: apply (simp add: unat_eq_0) done + lemma ptr_retyp_same_cleared_region: fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr" assumes ht: "ptr_retyp p td, g \\<^sub>t p'" shows "p = p' \ {ptr_val p..+ size_of TYPE('a)} \ {ptr_val p' ..+ size_of TYPE('a)} = {}" - apply (rule disjCI2) - apply (rule h_t_valid_neq_disjoint[OF ptr_retyp_h_t_valid ht, OF TrueI]) - apply simp - apply (simp add: field_of_t_refl) - done + using ht + by (simp add: h_t_valid_ptr_retyp_eq[where p=p and p'=p'] field_of_t_refl + split: split_if_asm) lemma h_t_valid_ptr_retyp_inside_eq: fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr" @@ -1403,6 +1370,103 @@ lemma cslift_ptr_retyp_memset_same': apply (simp add:range_cover_def word_bits_def) done +lemma cslift_ptr_retyp_memset_same_array: + assumes guard: "c_guard (Ptr p :: (('a :: oneMB_size)['b :: fourthousand_count]) ptr)" + and align: "is_aligned p m" + and size_of_m: "size_of TYPE('a) = 2 ^ m'" + and m': "CARD('b) * 2 ^ m' = 2 ^ m" + and clift_al: "\x \ dom (clift hp :: 'a typ_heap). is_aligned (ptr_val x) m'" + shows "(clift (hrs_htd_update (ptr_retyps 1 (Ptr p :: ('a['b]) ptr)) + (hrs_mem_update (heap_update_list p (replicate (2^m) 0)) + hp )) :: 'a typ_heap) + = (\y. if y \ (CTypesDefs.ptr_add (Ptr p :: 'a ptr) o of_nat) ` {k. k < CARD('b)} + then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else clift hp y)" + (is "clift ?hp = ?clift2") +proof (rule ext, split split_if, safe) + let ?v = "from_bytes (replicate (size_of TYPE('a)) 0) :: 'a" + let ?p = "Ptr p :: ('a['b]) ptr" + let ?p' = "Ptr p :: 'a ptr" + + note addr_card = mem_type_class.max_size[where 'a="'a['b]"] + + from addr_card have m_32: "m < 32" + apply (simp add: addr_card_def size_of_m m') + apply (rule ccontr, simp add: linorder_not_less) + apply (drule power_increasing[where 'a=nat and a=2], simp) + apply (simp add: card_word) + done + + from m'[THEN arg_cong[where f="\x. 2 ^ m' dvd x"]] + have m'_ineq: "m' \ m" + by (auto dest: power_dvd_imp_le) + + from m'_ineq m'[THEN arg_cong[where f="\x. x div 2 ^ m'"]] + have m'_card_eq: "CARD('b) = 2 ^ (m - m')" + by (simp add: power_sub) + + { + fix x + assume x: "x < CARD ('b)" + + note lookup = field_lookup_array[OF x, where 'a='a] + note field_ti = field_lookup_field_ti[OF eq_reflection, OF lookup] + + have clift_retyp: "clift ?hp ?p = Some (from_bytes (replicate (2 ^ m) 0))" + using addr_card + apply (simp add: hrs_htd_update_def hrs_mem_update_def split_def) + apply (rule trans, rule lift_t_retyp_heap_same, rule guard) + apply (simp add: m' size_of_m heap_list_update_eq) + done + + show "clift ?hp ((op +\<^sub>p ?p' \ int) x) = + Some (from_bytes (replicate (size_of TYPE('a)) 0) :: 'a)" + apply (rule trans[OF arg_cong[where f="clift hp" for hp], rotated]) + apply (rule trans, rule clift_field[OF clift_retyp field_ti]) + apply (simp add: x) + apply simp + apply (simp add: from_bytes_Array_element x size_of_m m'[symmetric]) + apply (cut_tac k="2 ^ m'" in mult_le_mono1[OF Suc_leI[OF x]]) + apply simp + apply (clarsimp simp: field_lvalue_def field_lookup_offset_eq[OF lookup]) + done + } + + { + fix y :: "'a ptr" + assume y: "y \ (op +\<^sub>p (Ptr p) \ int) ` {k. k < CARD('b)}" + + hence span: "h_t_valid (hrs_htd hp) c_guard y \ ptr_span y \ {p ..+ 2 ^ m} = {}" + apply (clarsimp simp: size_of_m h_t_valid_clift_Some_iff) + apply (frule clift_al[rule_format, OF domI]) + apply (simp only: upto_intvl_eq align) + apply (rule aligned_ranges_subset_or_disjoint_coroll, simp_all add: align) + apply clarsimp + apply (erule notE, rule_tac x="unat ((ptr_val y && mask m) >> m')" in image_eqI) + apply (clarsimp simp: size_of_m shiftl_t2n[simplified mult.commute, symmetric] + shiftr_shiftl1 is_aligned_andI1 add.commute + word_plus_and_or_coroll2) + apply (simp add: m'_card_eq) + apply (rule unat_less_helper, simp) + apply (rule shiftr_less_t2n, simp add: m'_ineq) + apply (rule and_mask_less_size, simp add: word_size m_32) + apply clarsimp + apply (erule notE, rule_tac x=0 in image_eqI, simp_all) + apply (case_tac y, clarsimp simp: is_aligned_weaken[OF align] m'_ineq) + done + + thus "clift ?hp y = clift hp y" + using y + apply (simp add: liftt_if hrs_htd_update_def hrs_mem_update_def split_def) + apply (simp add: h_t_valid_ptr_retyp_eq array_not_sub_type + h_val_def heap_list_update_disjoint_same + size_of_m m' Int_commute field_of_t_array + split: split_if) + apply (auto simp: array_ptr_index_def o_def ptr_add_def image_eqI[where x=0] + hrs_htd_def + split: if_splits) + done + } +qed lemma projectKO_opt_retyp_other: assumes cover: "range_cover ptr sz (objBitsKO ko) n" @@ -1565,83 +1629,79 @@ lemma cmap_relation_retype: lemma update_ti_t_word32_0s: "update_ti_t (typ_info_t TYPE(word32)) [0,0,0,0] X = 0" - apply (simp add: typ_info_word word_rcat_def bin_rcat_def) - done + "word_rcat [0, 0, 0, (0 :: word8)] = (0 :: word32)" + by (simp_all add: typ_info_word word_rcat_def bin_rcat_def) lemma is_aligned_ptr_aligned: - fixes p :: "'a :: mem_type ptr" + fixes p :: "'a :: c_type ptr" assumes al: "is_aligned (ptr_val p) n" and alignof: "align_of TYPE('a) = 2 ^ n" shows "ptr_aligned p" using al unfolding is_aligned_def ptr_aligned_def by (simp add: alignof) +lemma is_aligned_c_guard: + "is_aligned (ptr_val p) n + \ ptr_val p \ 0 + \ align_of TYPE('a) = 2 ^ m + \ size_of TYPE('a) \ 2 ^ n + \ m \ n + \ c_guard (p :: ('a :: c_type) ptr)" + apply (clarsimp simp: c_guard_def c_null_guard_def) + apply (rule conjI) + apply (rule is_aligned_ptr_aligned, erule(1) is_aligned_weaken, simp) + apply (erule is_aligned_get_word_bits, simp_all) + apply (rule intvl_nowrap[where x=0, simplified], simp) + apply (erule is_aligned_no_wrap_le, simp+) + done lemma retype_guard_helper: assumes cover: "range_cover p sz (objBitsKO ko) n" and ptr0: "p \ 0" - and szo: "size_of TYPE('a :: mem_type) = 2 ^ objBitsKO ko" + and szo: "size_of TYPE('a :: c_type) = 2 ^ objBitsKO ko" and lt2: "m \ objBitsKO ko" - and ala: "align_of TYPE('a :: mem_type) = 2 ^ m" - shows "\b < n. c_guard (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) (of_nat b))" + and ala: "align_of TYPE('a :: c_type) = 2 ^ m" + shows "\b < n. c_guard (CTypesDefs.ptr_add (Ptr p :: 'a ptr) (of_nat b))" proof (rule allI, rule impI) fix b :: nat assume nv: "b < n" - let ?p = "(Ptr p :: 'a :: mem_type ptr)" + let ?p = "(Ptr p :: 'a ptr)" + + have "of_nat b * of_nat (size_of TYPE('a)) = (of_nat (b * 2 ^ objBitsKO ko) :: word32)" + by (simp add: szo) + + also have "\ < (2 :: word32) ^ sz" using nv cover + apply simp + apply (rule word_less_power_trans_ofnat) + apply (erule less_le_trans) + apply (erule range_cover.range_cover_n_le(2)) + apply (erule range_cover.sz)+ + done + + finally have ofn: "of_nat b * of_nat (size_of TYPE('a)) < (2 :: word32) ^ sz" . + + have le: "p \ p + of_nat b * 2 ^ objBitsKO ko" + using ofn szo nv + apply - + apply (cases b,clarsimp+) + apply (cut_tac n = nat in range_cover_ptr_le) + apply (rule range_cover_le[OF cover]) + apply simp + apply (simp add:ptr0) + apply (simp add:shiftl_t2n field_simps) + done + show "c_guard (CTypesDefs.ptr_add ?p (of_nat b))" - unfolding c_guard_def - proof (rule conjI) - show "ptr_aligned (CTypesDefs.ptr_add ?p (of_nat b))" - using cover lt2 ala - apply - - apply (rule ptr_aligned_plus) - apply (rule is_aligned_ptr_aligned) - apply (rule is_aligned_weaken[OF _ lt2]) - apply (fastforce simp:range_cover_def) - apply simp - done - - have "of_nat b * of_nat (size_of TYPE('a)) = (of_nat (b * 2 ^ objBitsKO ko) :: word32)" - by (simp add: szo) - - also have "\ < (2 :: word32) ^ sz" using nv cover - apply simp - apply (rule word_less_power_trans_ofnat) - apply (erule less_le_trans) - apply (erule range_cover.range_cover_n_le(2)) - apply (erule range_cover.sz)+ - done - - finally have ofn: "of_nat b * of_nat (size_of TYPE('a)) < (2 :: word32) ^ sz" . - - have Sucn: "Suc b * 2 ^ objBitsKO ko \ 2 ^ sz" using cover nv - apply - - apply (subst mult.commute, rule nat_le_power_trans) - apply (erule le_trans[OF Suc_leI]) - apply (erule range_cover.range_cover_n_le) - apply (erule range_cover.sz) - done - - show "c_null_guard (CTypesDefs.ptr_add ?p (of_nat b))" - unfolding c_null_guard_def using ofn szo nv - apply - - apply (rule intvl_nowrap [where x = 0, simplified]) - apply simp - apply (rule neq_0_no_wrap) - apply (case_tac b,clarsimp+) - apply (cut_tac n = nat in range_cover_ptr_le) - apply (rule range_cover_le[OF cover]) - apply simp - apply (simp add:ptr0) - apply (simp add:shiftl_t2n field_simps) - apply (simp add:ptr0) - apply simp - apply (erule range_cover_bound'[where 'a=32, simplified, OF cover]) - done - qed + apply (rule is_aligned_c_guard[OF _ _ ala _ lt2]) + apply (simp add: szo) + apply (rule is_aligned_add) + apply (rule range_cover.aligned, rule cover) + apply (rule is_aligned_mult_triv2) + apply (simp add: szo neq_0_no_wrap[OF le ptr0]) + apply (simp add: szo) + done qed - (* When we are retyping, CTEs in the system do not change, * unless we happen to be retyping into a CNode or a TCB, * in which case new CTEs only pop up in the new object. *) @@ -1718,10 +1778,10 @@ where (* Ugh *) lemma cslift_ptr_retyp_memset_other_inst: - assumes bytes: "region_is_bytes p (n * (2 ^ objBitsKO ko)) x" - and cover: "range_cover p sz (objBitsKO ko) n" + assumes bytes: "region_is_bytes p (n * (2 ^ bits)) x" + and cover: "range_cover p sz bits n" and sz: "region_sz = n * size_of TYPE('a :: mem_type)" - and sz2: "size_of TYPE('a :: mem_type) = (2 ^ objBitsKO ko)" + and sz2: "size_of TYPE('a :: mem_type) = 2 ^ bits" and tdisj: "typ_uinfo_t TYPE('a :: mem_type) \\<^sub>t typ_uinfo_t TYPE('b :: mem_type)" and not_byte: "typ_uinfo_t TYPE('b :: mem_type) \ typ_uinfo_t TYPE(word8)" shows "(clift (hrs_htd_update (ptr_retyps n (Ptr p :: 'a :: mem_type ptr)) @@ -1744,6 +1804,12 @@ lemma cslift_ptr_retyp_memset_other_inst: apply simp done +lemma clift_eq_h_t_valid_eq: + "clift hp = (clift hp' :: ('a :: c_type) ptr \ _) + \ (h_t_valid (hrs_htd hp) c_guard :: 'a ptr \ _) + = h_t_valid (hrs_htd hp') c_guard" + by (rule ext, simp add: h_t_valid_clift_Some_iff) + lemma createObjects_ccorres_ep: defines "ko \ (KOEndpoint (makeObject :: endpoint))" shows "\\ x. (\, x) \ rf_sr \ range_cover ptr sz (objBitsKO ko) n @@ -1795,11 +1861,11 @@ proof (intro impI allI) size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def) apply (simp add: typ_info_array array_tag_def eval_nat_numeral) - apply (simp add: array_tag_n.simps) - apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine Let_def + apply (simp add: array_tag_n_eq) + apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti - ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def) - apply (simp add: update_ti_t_word32_0s EPState_Idle_def) + ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def) + apply (simp add: EPState_Idle_def update_ti_t_word32_0s) done (* /obj specific *) @@ -1815,8 +1881,9 @@ proof (intro impI allI) note rl = projectKO_opt_retyp_other [OF rc pal pno] note cterl = retype_ctes_helper [OF pal pdst pno al sz szb mko rc, simplified] + note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] - have guard: + have guard: "\b < n. c_guard (CTypesDefs.ptr_add ?ptr (of_nat b))" apply (rule retype_guard_helper [where m = 2, OF cover ptr0 szo]) apply (simp add: ko_def objBits_simps) @@ -1839,7 +1906,7 @@ proof (intro impI allI) apply (simp add: ko_def projectKO_opt_ep) apply ((fastforce simp:objBitsKO_def projectKO_opt_ep ko_def split:kernel_object.split)+)[1] - apply (simp add: ptr_add_to_new_cap_addrs [OF szo]) + apply (simp add: ptr_add_to_new_cap_addrs [OF szo] ht_rl) apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def cong: if_cong) apply (simp add: rl[where 'a = tcb, unfolded ko_def projectKOs, simplified] @@ -1935,6 +2002,7 @@ proof (intro impI allI) (* rest is generic *) note rl = projectKO_opt_retyp_other [OF rc pal pno] note cterl = retype_ctes_helper [OF pal pdst pno al sz szb mko rc, simplified] + note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have guard: "\bb< n. c_guard (CTypesDefs.ptr_add ?ptr (of_nat b))" @@ -2093,7 +2162,7 @@ proof (intro impI allI) apply (rule pspace_aligned_to_C_cte[OF pal]) apply assumption apply (simp add: projectKOs ko_def) - apply (simp add: ptr_add_to_new_cap_addrs [OF szo]) + apply (simp add: ptr_add_to_new_cap_addrs [OF szo] ht_rl) apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def) apply (simp add: rl[where 'a=tcb, unfolded ko_def projectKOs, simplified] rl[where 'a=endpoint, unfolded ko_def projectKOs, simplified] @@ -2115,7 +2184,9 @@ proof (intro impI allI) apply (simp add: carch_state_relation_def cmachine_state_relation_def) apply (simp add: rl' cterl tag_disj_via_td_name h_t_valid_clift_Some_iff ) apply (clarsimp simp: hrs_htd_update ptr_retyps_htd_safe_neg szo - kernel_data_refs_domain_eq_rotate) + kernel_data_refs_domain_eq_rotate + +) done qed @@ -2186,18 +2257,74 @@ shows "{ptr..+n * 2 ^ us} = {ptr..ptr + (of_nat n * 2 ^ us - 1)}" done qed +lemma aligned_new_cap_addrs_eq_base: + "is_aligned p bits \ is_aligned ptr bits + \ n = 2 ^ (bits - objBitsKO ko) + \ objBitsKO ko = shft + \ y < of_nat n + \ (p + (y << shft) \ set (new_cap_addrs n ptr ko)) = (p = ptr)" + apply (erule is_aligned_get_word_bits) + apply (rule iffI) + apply (clarsimp simp: new_cap_addrs_def) + apply (rule ccontr, drule(2) aligned_neq_into_no_overlap) + apply (simp only: field_simps upto_intvl_eq[symmetric]) + apply (drule equals0D, erule notE, rule_tac c="p + (y << shft)" in IntI) + apply (simp(no_asm) add: offs_in_intvl_iff) + apply (rule unat_less_helper, simp, rule shiftl_less_t2n; simp) + apply (simp add: offs_in_intvl_iff) + apply (rule unat_less_helper, simp, rule shiftl_less_t2n; simp add: word_of_nat_less) + apply (simp add: new_cap_addrs_def) + apply (rule_tac x="unat y" in image_eqI; simp add: unat_less_helper) + apply (erule is_aligned_get_word_bits; simp) + apply (simp add: new_cap_addrs_def) + apply (rule_tac x="unat y" in image_eqI; simp add: unat_less_helper) + done + +lemma cmap_relation_array_add_array[OF refl]: + "ptrf = Ptr \ carray_map_relation n ahp chp ptrf + \ is_aligned p n + \ ahp' = (\x. if x \ set (new_cap_addrs sz p ko) then Some v else ahp x) + \ (\x. chp x \ is_aligned (ptr_val x) n \ \y. chp' y = (y = ptrf p | chp y)) + \ sz = 2 ^ (n - objBits v) + \ objBitsKO ko = objBitsKO (injectKOS v) + \ objBits v \ n \ n < word_bits + \ carray_map_relation n ahp' chp' ptrf" + apply (clarsimp simp: carray_map_relation_def objBits_koTypeOf + objBitsT_koTypeOf[symmetric] + koTypeOf_injectKO + simp del: objBitsT_koTypeOf) + apply (drule meta_mp) + apply auto[1] + apply (case_tac "pa = p"; clarsimp) + apply (subst if_P; simp add: new_cap_addrs_def) + apply (rule_tac x="unat ((p' && mask n) >> objBitsKO ko)" in image_eqI) + apply (simp add: shiftr_shiftl1 is_aligned_andI1 add.commute + word_plus_and_or_coroll2) + apply (simp, rule unat_less_helper, simp, rule shiftr_less_t2n) + apply (simp add: and_mask_less_size word_size word_bits_def) + apply (case_tac "chp (ptrf pa)", simp_all) + apply (drule spec, drule(1) iffD2) + apply (auto split: split_if)[1] + apply (drule_tac x=pa in spec, clarsimp) + apply (drule_tac x=p' in spec, clarsimp split: split_if_asm) + apply (clarsimp simp: new_cap_addrs_def) + apply (subst(asm) is_aligned_add_helper, simp_all) + apply (rule shiftl_less_t2n, rule word_of_nat_less, simp_all add: word_bits_def) + done + lemma createObjects_ccorres_pte: defines "ko \ (KOArch (KOPTE (makeObject :: pte)))" shows "\\ x. (\, x) \ rf_sr \ ptr \ 0 \ pspace_aligned' \ \ pspace_distinct' \ - \ pspace_no_overlap' ptr sz \ \ (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x) \ range_cover ptr sz (objBitsKO ko) n - \ n \ 0 \ valid_global_refs' s - \ kernel_data_refs \ {ptr..+n * 2 ^ objBitsKO ko} = {} \ - (\\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \)\, + \ pspace_no_overlap' ptr sz \ \ (region_is_bytes ptr (2 ^ ptBits) x) + \ range_cover ptr sz ptBits 1 + \ valid_global_refs' s + \ kernel_data_refs \ {ptr..+ 2 ^ ptBits} = {} \ + (\\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs 256 ptr ko) (ksPSpace \)\, x\globals := globals x - \t_hrs_' := hrs_htd_update (ptr_retyps n (Ptr ptr :: pte_C ptr)) + \t_hrs_' := hrs_htd_update (ptr_retyps 1 (Ptr ptr :: (pte_C[256]) ptr)) (hrs_mem_update - (heap_update_list ptr (replicate (n * 2^ objBitsKO ko) 0)) + (heap_update_list ptr (replicate (2 ^ ptBits) 0)) (t_hrs_' (globals x)))\\) \ rf_sr" (is "\\ x. ?P \ x \ (\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr") @@ -2206,20 +2333,19 @@ proof (intro impI allI) let ?thesis = "(\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr" let ?ks = "?ks \" let ?ks' = "?ks' x" - let ?ptr = "Ptr ptr :: pte_C ptr" + let ?ptr = "Ptr ptr :: (pte_C[256]) ptr" assume "?P \ x" hence rf: "(\, x) \ rf_sr" - and cover: "range_cover ptr sz (objBitsKO ko) n" - and al: "is_aligned ptr (objBitsKO ko)" + and cover: "range_cover ptr sz ptBits 1" + and al: "is_aligned ptr ptBits" and ptr0: "ptr \ 0" - and n0 :"n\ 0" - and sz: "objBitsKO ko \ sz" + and sz: "ptBits \ sz" and szb: "sz < word_bits" and pal: "pspace_aligned' \" and pdst: "pspace_distinct' \" and pno: "pspace_no_overlap' ptr sz \" - and empty: "region_is_bytes ptr (n * (2 ^ objBitsKO ko)) x" - and kernel_data_refs_disj : "kernel_data_refs \ {ptr..+n * 2 ^ objBitsKO ko} = {}" + and empty: "region_is_bytes ptr (2 ^ ptBits) x" + and kernel_data_refs_disj : "kernel_data_refs \ {ptr..+ 2 ^ ptBits} = {}" by (clarsimp simp:range_cover_def[where 'a=32, folded word_bits_def])+ note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff @@ -2249,39 +2375,74 @@ proof (intro impI allI) (* /obj specific *) (* s/obj/obj'/ *) - have szo: "size_of TYPE(pte_C) = 2 ^ objBitsKO ko" by (simp add: size_of_def objBits_simps archObjSize_def ko_def) - have szo': "n * 2 ^ objBitsKO ko = n * size_of TYPE(pte_C)" using sz - apply (subst szo) - apply (simp add: power_add [symmetric]) - done + have szo: "size_of TYPE(pte_C[256]) = 2 ^ ptBits" + by (simp add: size_of_def size_td_array ptBits_def pageBits_def) + have szo': "size_of TYPE(pte_C) = 2 ^ objBitsKO ko" + by (simp add: objBits_simps ko_def archObjSize_def ptBits_def pageBits_def) - note rl' = cslift_ptr_retyp_memset_other_inst[OF empty cover szo' szo] + note rl' = cslift_ptr_retyp_memset_other_inst[where n=1, + simplified, OF empty cover[simplified] szo[symmetric] szo] - (* rest is generic *) - - note rl = projectKO_opt_retyp_other [OF _ pal pno] - note cterl = retype_ctes_helper [OF pal pdst pno al sz szb mko cover, simplified] - - have guard: - "\b < n. c_guard (CTypesDefs.ptr_add ?ptr (of_nat b))" - apply (rule retype_guard_helper [where m = 2, OF cover ptr0 szo]) - apply (simp add: ko_def objBits_simps archObjSize_def) - apply (simp add: align_of_def) + have sz_weaken: "objBitsKO ko \ ptBits" + by (simp add: objBits_simps ko_def archObjSize_def ptBits_def pageBits_def) + have cover': "range_cover ptr sz (objBitsKO ko) 256" + apply (rule range_cover_rel[OF cover sz_weaken]) + apply (simp add: ptBits_def objBits_simps ko_def archObjSize_def pageBits_def) done + from sz sz_weaken have sz': "objBitsKO ko \ sz" by simp + note al' = is_aligned_weaken[OF al sz_weaken] + + have koT: "koTypeOf ko = ArchT PTET" + by (simp add: ko_def) + + (* rest used to be generic, but PT arrays are complicating everything *) + + note rl = projectKO_opt_retyp_other [OF cover' pal pno] + note cterl = retype_ctes_helper [OF pal pdst pno al' sz' szb mko cover'] + + have guard: "c_guard ?ptr" + apply (rule is_aligned_c_guard[where n=ptBits and m=2]) + apply (simp_all add: al ptr0 align_of_def align_td_array) + apply (simp_all add: ptBits_def pageBits_def) + done + + note ptr_retyps.simps[simp del] + + from rf have pterl: "cmap_relation (map_to_ptes (ksPSpace \)) (cslift x) Ptr cpte_relation" + unfolding rf_sr_def cstate_relation_def by (simp add: Let_def cpspace_relation_def) + + guess + apply (rule meta_mp[rotated], rule cslift_ptr_retyp_memset_same_array[OF guard al szo']) + apply (simp add: objBits_simps ko_def archObjSize_def ptBits_def pageBits_def) + apply (rule pspace_aligned_to_C[OF pal pterl]) + apply (simp add: projectKOs ko_def) + apply (simp add: projectKOs ko_def objBits_simps archObjSize_def) + apply simp + done + note rl'' = this + + note rl''' = cslift_ptr_retyp_memset_same'[OF _ cover szo, simplified szo, + simplified, OF guard] + note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] + + have pte_arr: "cpspace_pte_array_relation (ksPSpace \) (t_hrs_' (globals x)) + \ cpspace_pte_array_relation ?ks ?ks'" + apply (erule cmap_relation_array_add_array[OF _ al]) + apply (simp add: foldr_upd_app_if[folded data_map_insert_def]) + apply (rule projectKO_opt_retyp_same, simp add: ko_def projectKOs) + apply (simp add: h_t_valid_clift_Some_iff rl''' dom_def split: split_if) + apply (simp_all add: objBits_simps archObjSize_def ptBits_def + pageBits_def ko_def word_bits_def) + done from rf have "cpspace_relation (ksPSpace \) (underlying_memory (ksMachineState \)) (t_hrs_' (globals x))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) hence "cpspace_relation ?ks (underlying_memory (ksMachineState \)) ?ks'" unfolding cpspace_relation_def - apply - + using pte_arr apply (clarsimp simp: rl' cterl cte_C_size tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) - apply (subst cslift_ptr_retyp_memset_same' [where m = "objBitsKO ko", OF guard cover szo ]) - apply (simp add: ko_def objBits_simps archObjSize_def size_of_def) - apply (rule pspace_aligned_to_C[where 'b=pte_C and ko=ko, simplified ko_def objBitsKO_def, simplified archObjSize_def, simplified]) - apply (rule pal) - apply assumption - apply (simp add: ko_def projectKOs objBits_simps archObjSize_def)+ - apply (simp add: ptr_add_to_new_cap_addrs [OF szo]) + apply (simp add: rl'') + apply (simp add: ptr_add_to_new_cap_addrs [OF szo'] ht_rl) apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def cong: if_cong) apply (simp add: rl[where 'a=tcb, unfolded ko_def projectKOs, simplified] @@ -2298,14 +2459,13 @@ proof (intro impI allI) moreover from rf szb al - have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \ {ptr ..+ n * 2^objBitsKO ko} = {}" + have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \ {ptr ..+ 2 ^ ptBits} = {}" apply (clarsimp simp: valid_global_refs'_def Let_def valid_refs'_def ran_def rf_sr_def cstate_relation_def) apply (erule disjoint_subset) apply (simp add:kernel_data_refs_disj) done - moreover ultimately show ?thesis using rf empty kernel_data_refs_disj apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name) @@ -2315,28 +2475,28 @@ proof (intro impI allI) apply (rule conjI) apply (rule h_t_valid_ptr_retyps) apply assumption - apply (simp add:szo ptr_span_def) + apply (simp add:szo) apply (erule disjoint_subset) - apply (simp add: ko_def projectKOs objBits_simps archObjSize_def) + apply (simp add: ptBits_def pageBits_def del: replicate_numeral) apply (simp add:szo ptr_retyps_htd_safe_neg hrs_htd_def - kernel_data_refs_domain_eq_rotate - ko_def projectKOs objBits_simps archObjSize_def Int_ac) + kernel_data_refs_domain_eq_rotate ptBits_def pageBits_def + Int_ac del: replicate_numeral) done qed lemma createObjects_ccorres_pde: defines "ko \ (KOArch (KOPDE (makeObject :: pde)))" shows "\\ x. (\, x) \ rf_sr \ ptr \ 0 - \ n \ 0 \ pspace_aligned' \ \ pspace_distinct' \ - \ pspace_no_overlap' ptr sz \ \ (region_is_bytes ptr (n * 2^objBitsKO ko) x) \ range_cover ptr sz (objBitsKO ko) n + \ pspace_no_overlap' ptr sz \ \ (region_is_bytes ptr (2 ^ pdBits) x) + \ range_cover ptr sz pdBits 1 \ valid_global_refs' s - \ kernel_data_refs \ {ptr..+n * 2 ^ objBitsKO ko} = {} \ - (\\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \)\, + \ kernel_data_refs \ {ptr..+ 2 ^ pdBits} = {} \ + (\\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \)\, x\globals := globals x - \t_hrs_' := hrs_htd_update (ptr_retyps n (Ptr ptr :: pde_C ptr)) + \t_hrs_' := hrs_htd_update (ptr_retyps 1 (Ptr ptr :: (pde_C[4096]) ptr)) (hrs_mem_update - (heap_update_list ptr (replicate (n * 2^objBitsKO ko) 0)) + (heap_update_list ptr (replicate (2 ^ pdBits) 0)) (t_hrs_' (globals x)))\\) \ rf_sr" (is "\\ x. ?P \ x \ (\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr") @@ -2345,19 +2505,17 @@ proof (intro impI allI) let ?thesis = "(\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr" let ?ks = "?ks \" let ?ks' = "?ks' x" - let ?ptr = "Ptr ptr :: pde_C ptr" - + let ?ptr = "Ptr ptr :: (pde_C[4096]) ptr" + assume "?P \ x" - hence rf: "(\, x) \ rf_sr" and al: "is_aligned ptr (objBitsKO ko)" and ptr0: "ptr \ 0" - and cover: "range_cover ptr sz (objBitsKO ko) n" - and sz: "objBitsKO ko \ sz" + hence rf: "(\, x) \ rf_sr" and al: "is_aligned ptr pdBits" and ptr0: "ptr \ 0" + and cover: "range_cover ptr sz pdBits 1" + and sz: "pdBits \ sz" and szb: "sz < word_bits" and pal: "pspace_aligned' \" and pdst: "pspace_distinct' \" and pno: "pspace_no_overlap' ptr sz \" - and empty: "region_is_bytes ptr (n * 2^objBitsKO ko) x" - and rc: "range_cover ptr sz (objBitsKO ko) n" - and n0: "n \ 0" - and kernel_data_refs_disj : "kernel_data_refs \ {ptr..+n * 2 ^ objBitsKO ko} = {}" + and empty: "region_is_bytes ptr (2 ^ pdBits) x" + and kernel_data_refs_disj : "kernel_data_refs \ {ptr..+ 2 ^ pdBits} = {}" by (clarsimp simp:range_cover_def[where 'a=32, folded word_bits_def])+ (* obj specific *) @@ -2402,64 +2560,106 @@ proof (intro impI allI) (* /obj specific *) (* s/obj/obj'/ *) - have szo: "size_of TYPE(pde_C) = 2 ^ objBitsKO ko" by (simp add: size_of_def objBits_simps archObjSize_def ko_def) - have szo': "n * 2 ^ objBitsKO ko = n * size_of TYPE(pde_C)" using sz - apply (subst szo) - apply (simp add: power_add [symmetric]) - done - note rl' = cslift_ptr_retyp_memset_other_inst[OF empty cover szo' szo] + have szo: "size_of TYPE(pde_C[4096]) = 2 ^ pdBits" + by (simp add: size_of_def size_td_array pdBits_def pageBits_def) + have szo': "size_of TYPE(pde_C) = 2 ^ objBitsKO ko" + by (simp add: objBits_simps ko_def archObjSize_def pdBits_def pageBits_def) - (* rest is generic *) - note rl = projectKO_opt_retyp_other [OF _ pal pno] - note cterl = retype_ctes_helper [OF pal pdst pno al sz szb mko cover, simplified] + note rl' = cslift_ptr_retyp_memset_other_inst[where n=1, + simplified, OF empty cover[simplified] szo[symmetric] szo] - have guard: - "\b < n. c_guard (CTypesDefs.ptr_add ?ptr (of_nat b))" - apply (rule retype_guard_helper [where m = 2, OF cover ptr0 szo]) - apply (simp add: ko_def objBits_simps archObjSize_def) - apply (simp add: align_of_def) + have sz_weaken: "objBitsKO ko \ pdBits" + by (simp add: objBits_simps ko_def archObjSize_def pdBits_def pageBits_def) + have cover': "range_cover ptr sz (objBitsKO ko) 4096" + apply (rule range_cover_rel[OF cover sz_weaken]) + apply (simp add: pdBits_def objBits_simps ko_def archObjSize_def pageBits_def) done + from sz sz_weaken have sz': "objBitsKO ko \ sz" by simp + note al' = is_aligned_weaken[OF al sz_weaken] + + have koT: "koTypeOf ko = ArchT PDET" + by (simp add: ko_def) + + (* rest used to be generic, but PD arrays are complicating everything *) + + note rl = projectKO_opt_retyp_other [OF cover' pal pno] + note cterl = retype_ctes_helper [OF pal pdst pno al' sz' szb mko cover'] + + have guard: "c_guard ?ptr" + apply (rule is_aligned_c_guard[where n=pdBits and m=2]) + apply (simp_all add: al ptr0 align_of_def align_td_array) + apply (simp_all add: pdBits_def pageBits_def) + done + + note ptr_retyps.simps[simp del] + + note rl' = cslift_ptr_retyp_memset_other_inst[OF _ cover refl szo, + simplified szo, simplified, OF empty] + + from rf have pderl: "cmap_relation (map_to_pdes (ksPSpace \)) (cslift x) Ptr cpde_relation" + unfolding rf_sr_def cstate_relation_def by (simp add: Let_def cpspace_relation_def) + + guess + apply (rule meta_mp[rotated], rule cslift_ptr_retyp_memset_same_array[OF guard al szo']) + apply (simp add: objBits_simps ko_def archObjSize_def pdBits_def pageBits_def) + apply (rule pspace_aligned_to_C[OF pal pderl]) + apply (simp add: projectKOs ko_def) + apply (simp add: projectKOs ko_def objBits_simps archObjSize_def) + apply simp + done + note rl'' = this + + note rl''' = cslift_ptr_retyp_memset_same'[OF _ cover szo, simplified szo, + simplified, OF guard] + note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] + + have pde_arr: "cpspace_pde_array_relation (ksPSpace \) (t_hrs_' (globals x)) + \ cpspace_pde_array_relation ?ks ?ks'" + apply (erule cmap_relation_array_add_array[OF _ al]) + apply (simp add: foldr_upd_app_if[folded data_map_insert_def]) + apply (rule projectKO_opt_retyp_same, simp add: ko_def projectKOs) + apply (simp add: h_t_valid_clift_Some_iff rl''' dom_def split: split_if) + apply (simp_all add: objBits_simps archObjSize_def pdBits_def + pageBits_def ko_def word_bits_def) + done from rf have cpsp: "cpspace_relation (ksPSpace \) (underlying_memory (ksMachineState \)) (t_hrs_' (globals x))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) - hence cpsp': "cpspace_relation ?ks (underlying_memory (ksMachineState \)) ?ks'" + hence "cpspace_relation ?ks (underlying_memory (ksMachineState \)) ?ks'" unfolding cpspace_relation_def - apply - - apply (clarsimp simp: rl' cte_C_size cterl tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) - apply (subst cslift_ptr_retyp_memset_same' [where m = "objBitsKO ko", OF guard cover szo ]) - apply (simp add: ko_def objBits_simps archObjSize_def size_of_def) - apply (rule pspace_aligned_to_C[where 'b=pde_C and ko=ko, simplified ko_def objBitsKO_def, - simplified archObjSize_def, simplified]) - apply (rule pal) - apply assumption - apply (simp add: ko_def projectKOs objBits_simps archObjSize_def)+ - apply (simp add: ptr_add_to_new_cap_addrs [OF szo]) - apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def + using pde_arr + apply (clarsimp simp: rl' cterl cte_C_size tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) + apply (subst rl'') + apply (simp add: ptr_add_to_new_cap_addrs [OF szo'] ht_rl) + apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def cong: if_cong) - apply (simp add: rl[where 'a=tcb, unfolded ko_def projectKOs, simplified] + apply (simp add: rl[where 'a=tcb, unfolded ko_def projectKOs, simplified] rl[where 'a=endpoint, unfolded ko_def projectKOs, simplified] rl[where 'a=pte, unfolded ko_def projectKOs, simplified] rl[where 'a=asidpool, unfolded ko_def projectKOs, simplified] rl[where 'a=user_data, unfolded ko_def projectKOs, simplified] rl[where 'a=notification, unfolded ko_def projectKOs, simplified] - ko_def projectKOs cover[unfolded ko_def, simplified]) - apply (erule cmap_relation_retype) - apply (insert relrl, auto) + ko_def projectKOs cover[unfolded ko_def, simplified] + ) + apply (erule cmap_relation_retype) + apply (insert relrl, auto) done + moreover + from rf szb al + have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \ {ptr ..+ 2 ^ pdBits} = {}" + apply (clarsimp simp: valid_global_refs'_def Let_def + valid_refs'_def ran_def rf_sr_def cstate_relation_def) + apply (erule disjoint_subset) + apply (simp add:kernel_data_refs_disj) + done + moreover from rf have stored_asids: "(pde_stored_asid \\<^sub>m clift ?ks') = (pde_stored_asid \\<^sub>m cslift x)" unfolding rf_sr_def using cpsp empty apply (clarsimp simp: rl' cterl cte_C_size tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) - apply (subst cslift_ptr_retyp_memset_same' [where m = "objBitsKO ko", OF guard cover szo]) - apply (simp add: ko_def objBits_simps archObjSize_def size_of_def) - apply (rule pspace_aligned_to_C[where 'b=pde_C and ko=ko, simplified ko_def - objBitsKO_def, simplified archObjSize_def, simplified]) - apply (rule pal) - apply (clarsimp simp:cpspace_relation_def) - apply assumption - apply (simp add: ko_def projectKOs objBits_simps archObjSize_def)+ + apply (subst rl'') apply (rule ext) apply (simp add: map_comp_def stored_asid[simplified] split: option.split split_if) apply (simp only: o_def CTypesDefs.ptr_add_def' Abs_fnat_hom_mult) @@ -2468,22 +2668,12 @@ proof (intro impI allI) apply (rule intvl_self, simp) apply clarsimp apply (subst (asm) empty[unfolded region_is_bytes_def]) - apply (simp add: objBits_simps archObjSize_def ko_def) - apply (metis (full_types) Abs_fnat_hom_mult intvlI - mult_strict_right_mono of_nat_numeral zero_less_numeral) + apply (simp add: objBits_simps archObjSize_def ko_def pdBits_def pageBits_def + offs_in_intvl_iff unat_word_ariths unat_of_nat) apply clarsimp apply clarsimp done - moreover - from rf szb al - have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \ {ptr ..+ n * 2^objBitsKO ko} = {}" - apply (clarsimp simp: valid_global_refs'_def cte_wp_at_ctes_of Let_def - valid_refs'_def ran_def rf_sr_def cstate_relation_def) - apply (erule disjoint_subset) - apply (simp add:kernel_data_refs_disj) - done - ultimately show ?thesis using rf empty kernel_data_refs_disj apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name) @@ -2493,12 +2683,15 @@ proof (intro impI allI) apply (rule conjI) apply (rule h_t_valid_ptr_retyps) apply assumption - apply (simp add:szo ptr_span_def) + apply (simp add:szo) apply (erule disjoint_subset) - apply (simp add: ko_def projectKOs objBits_simps archObjSize_def) + apply (simp add: ko_def projectKOs objBits_simps archObjSize_def + pdBits_def pageBits_def del: replicate_numeral) apply (simp add:szo ptr_retyps_htd_safe_neg hrs_htd_def kernel_data_refs_domain_eq_rotate - ko_def projectKOs objBits_simps archObjSize_def Int_ac) + ko_def projectKOs objBits_simps archObjSize_def Int_ac + pdBits_def pageBits_def + del: replicate_numeral) done qed @@ -3187,11 +3380,13 @@ proof - note tcb_C_size[simp del] + from al have cover: "range_cover (ctcb_ptr_to_tcb_ptr p) (objBitsKO kotcb) + (objBitsKO kotcb) (Suc 0)" + by (rule range_cover_full, simp_all add: al) + have "\n<2 ^ (objBitsKO kotcb - objBitsKO ko). c_guard (CTypesDefs.ptr_add ?ptr (of_nat n))" apply (rule retype_guard_helper [where m = 2]) - apply (rule range_cover_rel[OF range_cover_full,rotated -1]) - apply simp - apply (rule al) + apply (rule range_cover_rel[OF cover, rotated]) apply simp apply (simp add: ko_def objBits_simps kotcb_def) apply (rule ptr0) @@ -3215,6 +3410,7 @@ proof - apply (simp add: kotcb_def objBits_simps) done + hence rl': "typ_uinfo_t TYPE(tcb_C) \\<^sub>t typ_uinfo_t TYPE('a :: mem_type) \ typ_uinfo_t TYPE('a :: mem_type) \ typ_uinfo_t TYPE(word8) \ (clift ?hp :: 'a :: mem_type typ_heap) = cslift x" @@ -3329,7 +3525,7 @@ proof - apply (simp add: hrs_mem_def typ_heap_simps packed_heap_update_collapse cong: if_cong) - apply (simp add: heap_update_def) + apply (simp add: heap_update_def) apply (subst heap_list_update_disjoint_same) apply simp apply (erule cte_tcb_disjoint) @@ -3641,12 +3837,15 @@ proof - apply (simp add: size_of_def) done + note ht_rest = clift_eq_h_t_valid_eq[OF cl_rest, simplified] + from rfsr have "cpspace_relation ks (underlying_memory (ksMachineState \)) (t_hrs_' (globals x))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) hence "cpspace_relation ?ks (underlying_memory (ksMachineState \)) (t_hrs_' ?gs)" unfolding cpspace_relation_def apply - - apply (simp add: cl_cte [simplified] cl_tcb [simplified] cl_rest [simplified] tag_disj_via_td_name) + apply (simp add: cl_cte [simplified] cl_tcb [simplified] cl_rest [simplified] tag_disj_via_td_name + ht_rest) apply (simp add: rl kotcb_def projectKOs rl_tcb rl_cte) apply (elim conjE) apply (intro conjI) @@ -4183,6 +4382,7 @@ proof (intro impI allI) note rl = projectKO_opt_retyp_other [OF rc' pal pno,unfolded ko_def] note cterl = retype_ctes_helper[OF pal pdst pno al' range_cover.sz(2)[OF rc'] range_cover.sz(1)[OF rc', folded word_bits_def] mko rc'] + note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have guard: "\ts. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) - and (\_. is_aligned pd pdBits)) + (valid_pde_mappings' and (\s. page_directory_at' (armKSGlobalPD (ksArchState s)) s) + and page_directory_at' pd and (\_. is_aligned pd pdBits)) (UNIV \ {s. newPD_' s = Ptr pd}) [] (copyGlobalMappings pd) (Call copyGlobalMappings_'proc)" apply (rule ccorres_gen_asm) @@ -4260,7 +4460,9 @@ lemma copyGlobalMappings_ccorres: apply csymbr apply (rule ccorres_rel_imp) apply (rule_tac F="\_ s. rv = armKSGlobalPD (ksArchState s) - \ is_aligned rv pdBits \ valid_pde_mappings' s" + \ is_aligned rv pdBits \ valid_pde_mappings' s + \ page_directory_at' pd s + \ page_directory_at' (armKSGlobalPD (ksArchState s)) s" and i="0xF00" in ccorres_mapM_x_while') apply (clarsimp simp del: Collect_const) @@ -4269,20 +4471,28 @@ lemma copyGlobalMappings_ccorres: apply (simp add: storePDE_def del: Collect_const) apply (rule_tac P="\s. ko_at' rva (armKSGlobalPD (ksArchState s) + ((0xF00 + of_nat n) << 2)) s - \ valid_pde_mappings' s" + \ page_directory_at' pd s \ valid_pde_mappings' s + \ page_directory_at' (armKSGlobalPD (ksArchState s)) s" and P'="{s. i_' s = of_nat (3840 + n) \ is_aligned (symbol_table ''armKSGlobalPD'') pdBits}" in setObject_ccorres_helper) apply (rule conseqPre, vcg) apply (clarsimp simp: shiftl_t2n field_simps upto_enum_word rf_sr_armKSGlobalPD - valid_arch_state'_def simp del: upt.simps) apply (rule cmap_relationE1[OF rf_sr_cpde_relation], assumption, erule_tac ko=ko' in ko_at_projectKO_opt) apply (rule cmap_relationE1[OF rf_sr_cpde_relation], assumption, erule_tac ko=rva in ko_at_projectKO_opt) apply (clarsimp simp: typ_heap_simps') + apply (drule(1) page_directory_at_rf_sr)+ + apply clarsimp + apply (subst array_ptr_valid_array_assertionI[where p="Ptr pd" and q="Ptr pd"], + erule h_t_valid_clift; simp) + apply (simp add: unat_def[symmetric] unat_word_ariths unat_of_nat pdBits_def pageBits_def) + apply (subst array_ptr_valid_array_assertionI[where q="Ptr (symbol_table x)" for x], + erule h_t_valid_clift; simp) + apply (simp add: unat_def[symmetric] unat_word_ariths unat_of_nat pdBits_def pageBits_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps) apply (rule conjI) @@ -4291,7 +4501,8 @@ lemma copyGlobalMappings_ccorres: apply (clarsimp simp: cpspace_relation_def typ_heap_simps update_pde_map_tos - update_pde_map_to_pdes) + update_pde_map_to_pdes + carray_map_relation_upd_triv) apply (erule(2) cmap_relation_updI) apply simp apply simp @@ -4334,11 +4545,12 @@ lemma copyGlobalMappings_ccorres: apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule hoare_pre) - apply (wp getObject_valid_pde_mapping' | simp)+ + apply (wp getObject_valid_pde_mapping' | simp + | wps storePDE_arch')+ apply (clarsimp simp: mask_add_aligned) apply (simp add: pdBits_def pageBits_def word_bits_def) apply simp - apply (clarsimp simp: word_sle_def) + apply (clarsimp simp: word_sle_def page_directory_at'_def) done @@ -4777,7 +4989,7 @@ lemma placeNewObject_pte: hs (placeNewObject regionBase (makeObject :: pte) 8) (CALL memzero(Ptr regionBase,0x400);; - global_htd_update (\_. (ptr_retyps 256 (pte_Ptr regionBase))))" + global_htd_update (\_. (ptr_retyps 1 (Ptr regionBase :: (pte_C[256]) ptr))))" apply (rule ccorres_from_vcg_nofail) apply clarsimp apply (rule conseqPre) @@ -4792,7 +5004,7 @@ lemma placeNewObject_pte: apply (frule(1) ghost_assertion_size_logic_no_unat, simp add: o_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def kernel_data_refs_domain_eq_rotate - elim!: ptr_retyps_htd_safe_neg) + elim!: ptr_retyps_htd_safe_neg[where n=1, simplified]) apply (frule range_cover_rel[where sbit' = 2]) apply simp+ apply (frule range_cover.unat_of_nat_shift[where gbits = 2 ]) @@ -4801,13 +5013,13 @@ lemma placeNewObject_pte: apply (subgoal_tac "region_is_bytes regionBase 1024 x") apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) - apply (cut_tac s=\ in createObjects_ccorres_pte [where ptr=regionBase and n="256" and sz=10]) + apply (cut_tac s=\ in createObjects_ccorres_pte [where ptr=regionBase and sz=10]) apply (erule_tac x=\ in allE, erule_tac x=x in allE) apply (clarsimp elim!:is_aligned_weaken simp: objBitsKO_def word_bits_def)+ apply (clarsimp simp: split_def objBitsKO_def archObjSize_def Fun.comp_def rf_sr_def split_def Let_def new_cap_addrs_def field_simps power_add) - apply (simp add:Int_ac) + apply (simp add:Int_ac ptBits_def pageBits_def) apply (clarsimp simp: word_bits_conv range_cover_def archObjSize_def) apply (clarsimp simp: objBitsKO_def range_cover.aligned archObjSize_def) apply (clarsimp simp: no_fail_def) @@ -4827,7 +5039,7 @@ lemma placeNewObject_pde: hs (placeNewObject regionBase (makeObject :: pde) 12) (CALL memzero(Ptr regionBase,0x4000);; - (global_htd_update (\_. (ptr_retyps 4096 (pde_Ptr regionBase)))))" + (global_htd_update (\_. (ptr_retyps 1 (pd_Ptr regionBase)))))" apply (rule ccorres_from_vcg_nofail) apply clarsimp apply (rule conseqPre) @@ -4843,7 +5055,7 @@ lemma placeNewObject_pde: apply (frule(1) ghost_assertion_size_logic_no_unat, simp add: o_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def kernel_data_refs_domain_eq_rotate - elim!: ptr_retyps_htd_safe_neg) + elim!: ptr_retyps_htd_safe_neg[where n=1, simplified]) apply (frule range_cover_rel[where sbit' = 2]) apply simp+ apply (frule range_cover.unat_of_nat_shift[where gbits = 2 ]) @@ -4852,13 +5064,13 @@ lemma placeNewObject_pde: apply (subgoal_tac "region_is_bytes regionBase 16384 x") apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) - apply (cut_tac s=\ in createObjects_ccorres_pde [where ptr=regionBase and n="4096" and sz=14]) + apply (cut_tac s=\ in createObjects_ccorres_pde [where ptr=regionBase and sz=14]) apply (erule_tac x=\ in allE, erule_tac x=x in allE) apply (clarsimp elim!:is_aligned_weaken simp: objBitsKO_def word_bits_def)+ apply (clarsimp simp: split_def objBitsKO_def archObjSize_def Fun.comp_def rf_sr_def split_def Let_def new_cap_addrs_def field_simps power_add) - apply (simp add:Int_ac) + apply (simp add:Int_ac pdBits_def pageBits_def) apply (clarsimp simp: word_bits_conv range_cover_def archObjSize_def) apply (clarsimp simp: objBitsKO_def range_cover.aligned archObjSize_def) apply (clarsimp simp: no_fail_def) @@ -5061,6 +5273,19 @@ lemma gsUserPages_update_ccorres: cong: if_cong) done +lemma createObjects'_page_directory_at_global: + "\ \s. n \ 0 \ range_cover ptr sz (objBitsKO val + gbits) n + \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s + \ page_directory_at' (armKSGlobalPD (ksArchState s)) s \ + createObjects' ptr n val gbits + \ \rv s. page_directory_at' (armKSGlobalPD (ksArchState s)) s \" + apply (simp add: page_directory_at'_def) + apply (rule hoare_pre, wp hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (wps createObjects'_ksArch) + apply (wp createObjects'_typ_at[where sz=sz]) + apply simp + done + lemma Arch_createObject_ccorres: assumes t: "toAPIType newType = None" shows "ccorres (\a b. ccap_relation (ArchObjectCap a) b) ret__struct_cap_C_' @@ -5400,20 +5625,23 @@ proof - Kernel_C.VMKernelOnly_def Kernel_C.VMReadOnly_def) apply (vcg exspec=copyGlobalMappings_modifies) apply (clarsimp simp:placeNewObject_def2) - apply (wp createObjects'_pde_mappings') + apply (wp createObjects'_pde_mappings' createObjects'_page_directory_at_global[where sz=pdBits] + createObjects'_page_directory_at'[where n=0, simplified]) apply clarsimp apply vcg apply (clarsimp simp: invs_pspace_aligned' invs_pspace_distinct' archObjSize_def invs_valid_global' makeObject_pde pdBits_def pageBits_def range_cover.aligned projectKOs APIType_capBits_def object_type_from_H_def objBits_simps) + apply (frule invs_arch_state') apply (frule range_cover.aligned) apply (frule is_aligned_addrFromPPtr_n, simp) apply (intro conjI) - apply fastforce - apply simp+ - apply (clarsimp simp: invs'_def valid_state'_def pageBits_def - valid_arch_state'_def page_directory_at'_def pdBits_def) + apply fastforce + apply simp+ + apply (clarsimp simp: pageBits_def + valid_arch_state'_def page_directory_at'_def pdBits_def) + apply assumption apply (clarsimp simp: is_aligned_no_overflow'[where n=14, simplified] field_simps is_aligned_mask[symmetric] mask_AND_less_0)+ apply (clarsimp elim!: is_aligned_weaken @@ -6278,6 +6506,17 @@ assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::ke apply (simp add: cte_C_size) done +lemma pspace_no_overlap_obj_atD': + "obj_at' P p s \ pspace_no_overlap' ptr bits s + \ \ko. P ko \ is_aligned p (objBitsKO (injectKOS ko)) + \ {p .. p + (2 ^ objBitsKO (injectKOS ko)) - 1} + \ {ptr .. (ptr && ~~ mask bits) + 2 ^ bits - 1} = {}" + apply (clarsimp simp: obj_at'_def) + apply (drule(1) pspace_no_overlapD') + apply (clarsimp simp: projectKOs project_inject) + apply auto + done + lemma typ_bytes_cpspace_relation_clift_adglobs: assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp" and "is_aligned ptr bits" "bits < word_bits" @@ -6294,17 +6533,38 @@ assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::ke apply simp apply fastforce apply (clarsimp simp: liftt_if hrs_htd_update_def split_def split: if_splits) - apply (simp add: h_t_valid_typ_region_bytes ptr_span_def) + apply (simp add: h_t_valid_typ_region_bytes) apply blast done +lemma cmap_array_typ_region_bytes_triv[OF refl]: + "ptrf = (Ptr :: _ \ 'b ptr) + \ carray_map_relation bits' (map_comp f (ksPSpace s)) (h_t_valid htd c_guard) ptrf + \ is_aligned ptr bits + \ pspace_no_overlap' ptr bits s + \ pspace_aligned' s + \ typ_uinfo_t TYPE('b :: c_type) \ typ_uinfo_t TYPE(8 word) + \ size_of TYPE('b) = 2 ^ bits' + \ objBitsT (koType TYPE('a :: pspace_storable)) \ bits + \ objBitsT (koType TYPE('a :: pspace_storable)) \ bits' + \ bits' < word_bits + \ carray_map_relation bits' (map_comp (f :: _ \ 'a option) (ksPSpace s)) + (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf" + apply (frule(7) cmap_array_typ_region_bytes[where ptrf=ptrf]) + apply (subst(asm) restrict_map_subdom, simp_all) + apply (drule(1) pspace_no_overlap_disjoint') + apply (simp add: upto_intvl_eq) + apply (rule order_trans[OF map_comp_subset_dom]) + apply auto + done + lemma ccorres_typ_region_bytes_dummy: "ccorresG rf_sr AnyGamma dc xfdc (invs' and ct_active' and sch_act_simple and pspace_no_overlap' ptr bits and - K (bits < word_bits \ is_aligned ptr bits \ - kernel_data_refs \ {ptr..+2 ^ bits} = {})) + K (bits < word_bits \ is_aligned ptr bits \ 2 \ bits + \ kernel_data_refs \ {ptr..+2 ^ bits} = {})) UNIV hs (return ()) (global_htd_update (\_. (typ_region_bytes ptr bits)))" @@ -6335,6 +6595,9 @@ lemma ccorres_typ_region_bytes_dummy: apply (simp add: cpspace_relation_def htd_safe_typ_region_bytes) apply (simp add: h_t_valid_clift_Some_iff) apply (simp add: hrs_htd_update) + apply (simp add: cmap_array_typ_region_bytes_triv + invs_pspace_aligned' pdBits_def pageBits_def ptBits_def + objBitsT_simps word_bits_def) apply (rule htd_safe_typ_region_bytes, simp) apply blast done @@ -7006,6 +7269,12 @@ lemma range_cover_gsMaxObjectSize: apply simp done +lemma APIType_capBits_min: + "(tp = APIObjectType apiobject_type.Untyped \ 4 \ userSize) + \ 4 \ APIType_capBits tp userSize" + by (simp add: APIType_capBits_def objBits_simps + split: object_type.split ArchTypes_H.apiobject_type.split) + lemma createNewObjects_ccorres: notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex @@ -7313,7 +7582,8 @@ shows "ccorres dc xfdc apply (clarsimp simp: invs_valid_pspace' conj_comms intvl_range_conv createObject_hs_preconds_def range_cover.aligned range_cover_full) apply (frule(1) range_cover_gsMaxObjectSize, fastforce, assumption) - apply (simp add: intvl_range_conv[OF range_cover.aligned range_cover_sz']) + apply (simp add: intvl_range_conv[OF range_cover.aligned range_cover_sz'] + order_trans[OF _ APIType_capBits_min]) apply (intro conjI) apply (simp add: word_bits_def range_cover_def) apply (clarsimp simp:rf_sr_def cstate_relation_def Let_def) diff --git a/proof/crefine/SR_lemmas_C.thy b/proof/crefine/SR_lemmas_C.thy index ed79b691d..a81d8290f 100644 --- a/proof/crefine/SR_lemmas_C.thy +++ b/proof/crefine/SR_lemmas_C.thy @@ -509,7 +509,8 @@ lemma fst_setCTE: (map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s')); (map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s')); (option_map tcb_no_ctes_proj \ map_to_tcbs (ksPSpace s) - = option_map tcb_no_ctes_proj \ map_to_tcbs (ksPSpace s')) \ \ P" + = option_map tcb_no_ctes_proj \ map_to_tcbs (ksPSpace s')); + \T p. typ_at' T p s = typ_at' T p s'\ \ P" shows "P" proof - (* Unpack the existential and bind x, theorems in this. Yuck *) @@ -596,7 +597,12 @@ proof - thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data option) = projectKO_opt (the (ksPSpace s x))" using ko ko' by simp qed fact - + + note sta = setCTE_typ_at'[where P="\x. x = y" for y] + show typ_at: "\T p. typ_at' T p s = typ_at' T p s'" + using use_valid[OF _ sta, OF thms(1), OF refl] + by auto + show "option_map tcb_no_ctes_proj \ map_to_tcbs (ksPSpace s) = option_map tcb_no_ctes_proj \ map_to_tcbs (ksPSpace s')" proof (rule ext) @@ -1998,6 +2004,17 @@ lemma gs_set_assn_Delete_cstate_relation: cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def) done +lemma update_typ_at: + assumes at: "obj_at' P p s" + and tp: "\obj. P obj \ koTypeOf (injectKOS obj) = koTypeOf ko" + shows "typ_at' T p' (s \ksPSpace := ksPSpace s(p \ ko)\) = typ_at' T p' s" + using at + by (auto elim!: obj_atE' simp: typ_at'_def ko_wp_at'_def + dest!: tp[rule_format] + simp: project_inject projectKO_eq split: kernel_object.splits split_if_asm, + simp_all add: objBits_def objBitsT_koTypeOf[symmetric] ps_clear_upd + del: objBitsT_koTypeOf) + end end diff --git a/proof/crefine/StateRelation_C.thy b/proof/crefine/StateRelation_C.thy index 2c4dc67bb..81462b18e 100644 --- a/proof/crefine/StateRelation_C.thy +++ b/proof/crefine/StateRelation_C.thy @@ -48,6 +48,20 @@ definition (addr_fun ` (dom as) = dom cs) \ (\x \ dom as. rel (the (as x)) (the (cs (addr_fun x))))" +definition + carray_map_relation :: "nat \ (word32 \ ('a :: pre_storable)) + \ ('b ptr \ bool) \ (word32 \ 'b ptr) \ bool" +where + "carray_map_relation bits as cs addr_fun \ + (\p. (is_aligned p bits \ (\p'. p' && ~~ mask bits = p \ is_aligned p' (objBits (the (as p'))) + \ p' \ dom as)) \ cs (addr_fun p))" + +definition + cvariable_array_map_relation :: "(word32 \ 'a) \ ('a \ nat) + \ (word32 \ ('c :: c_type) ptr) \ heap_typ_desc \ bool" +where + "cvariable_array_map_relation amap szs ptrfun htd + \ \p v. amap p = Some v \ array_assertion (ptrfun p) (szs v) htd" definition asid_map_pd_to_hwasids :: "(asid \ hw_asid \ obj_ref) \ (obj_ref \ hw_asid set)" @@ -120,11 +134,6 @@ where exclusive_state s = exclusive_state (phantom_machine_state_' s') \ machine_state_rest s = machine_state_rest (phantom_machine_state_' s')" -(* ptr_range uses the wrong set construct for h_t_valid stuff *) -definition - ptr_span :: "'a::mem_type ptr \ word32 set" where - "ptr_span p \ {ptr_val p ..+ size_of TYPE('a)}" - definition "globals_list_id_fudge = id" @@ -513,13 +522,26 @@ abbreviation abbreviation "cpspace_user_data_relation ah bh ch \ cmap_relation (heap_to_page_data ah bh) (clift ch) Ptr cuser_data_relation" +abbreviation + pd_Ptr :: "32 word \ (pde_C[4096]) ptr" where "pd_Ptr == Ptr" + +abbreviation + "cpspace_pde_array_relation ah ch \ carray_map_relation pdBits (map_to_pdes ah) (h_t_valid (hrs_htd ch) c_guard) pd_Ptr" + +abbreviation + pt_Ptr :: "32 word \ (pte_C[256]) ptr" where "pt_Ptr == Ptr" + +abbreviation + "cpspace_pte_array_relation ah ch \ carray_map_relation ptBits (map_to_ptes ah) (h_t_valid (hrs_htd ch) c_guard) pt_Ptr" + definition cpspace_relation :: "(word32 \ Structures_H.kernel_object) \ (word32 \ word8) \ heap_raw_state \ bool" where "cpspace_relation ah bh ch \ cpspace_cte_relation ah ch \ cpspace_tcb_relation ah ch \ cpspace_ep_relation ah ch \ cpspace_ntfn_relation ah ch \ - cpspace_pde_relation ah ch \ cpspace_pte_relation ah ch \ cpspace_asidpool_relation ah ch \ cpspace_user_data_relation ah bh ch" + cpspace_pde_relation ah ch \ cpspace_pte_relation ah ch \ cpspace_asidpool_relation ah ch \ cpspace_user_data_relation ah bh ch \ + cpspace_pde_array_relation ah ch \ cpspace_pte_array_relation ah ch" abbreviation "sched_queue_relation' \ tcb_queue_relation' tcbSchedNext_C tcbSchedPrev_C" @@ -546,6 +568,11 @@ where prio \ ucast minPrio \ prio \ ucast maxPrio) \ aqueues (qdom, prio) = [])" +abbreviation + "cte_array_relation astate cstate + \ cvariable_array_map_relation (gsCNodes astate) (\n. 2 ^ n) + cte_Ptr (hrs_htd (t_hrs_' cstate))" + fun irqstate_to_C :: "irqstate \ word32" where @@ -576,9 +603,6 @@ where ucast (fst adomSched) = dschedule_C.domain_C cdomSched \ (snd adomSched) = dschedule_C.length_C cdomSched" -abbreviation - pd_Ptr :: "32 word \ (pde_C[4096]) ptr" where "pd_Ptr == Ptr" - definition cdom_schedule_relation :: "(8 word \ 32 word) list \ (dschedule_C['b :: finite]) \ bool" where @@ -629,6 +653,7 @@ where (ksSchedulerAction_' cstate) \ carch_state_relation (ksArchState astate) cstate \ cmachine_state_relation (ksMachineState astate) cstate \ + cte_array_relation astate cstate \ apsnd fst (ghost'state_' cstate) = (gsUserPages astate, gsCNodes astate) \ ghost_size_rel (ghost'state_' cstate) (gsMaxObjectSize astate) \ ksWorkUnitsCompleted_' cstate = ksWorkUnitsCompleted astate \ diff --git a/proof/crefine/SyscallArgs_C.thy b/proof/crefine/SyscallArgs_C.thy index e62332c5c..cca2235e0 100644 --- a/proof/crefine/SyscallArgs_C.thy +++ b/proof/crefine/SyscallArgs_C.thy @@ -12,8 +12,7 @@ theory SyscallArgs_C imports TcbQueue_C CSpace_RAB_C - StoreWord_C - DetWP + StoreWord_C DetWP begin declare word_neq_0_conv[simp del] @@ -733,7 +732,7 @@ lemma threadGet_tcbIpcBuffer_ccorres [corres]: apply clarsimp apply (clarsimp simp: return_def typ_heap_simps') apply (clarsimp simp: obj_at'_def ctcb_relation_def) - done + done (* FIXME: move *) lemma ccorres_case_bools: @@ -1143,6 +1142,32 @@ lemma scast_ucast_add_one [simp]: apply clarsimp done +lemma valid_ipc_buffer_ptr_array: + "valid_ipc_buffer_ptr' (ptr_val p) s \ (s, s') \ rf_sr + \ n < 2 ^ (msg_align_bits - 2) + \ n \ 0 + \ array_assertion (p :: word32 ptr) n (hrs_htd (t_hrs_' (globals s')))" + apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches) + apply (drule obj_at_ko_at', clarsimp) + apply (drule rf_sr_heap_relation) + apply (erule cmap_relationE1) + apply (clarsimp simp: heap_to_page_data_def Let_def) + apply (rule conjI, rule exI, erule ko_at_projectKO_opt) + apply (rule refl) + apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp) + apply (erule clift_array_assertion_imp, simp+) + apply (simp add: field_lvalue_def msg_align_bits) + apply (rule_tac x="unat (ptr_val p && mask pageBits >> 2)" in exI, + simp add: word32_shift_by_2 shiftr_shiftl1 + is_aligned_andI1[OF is_aligned_weaken]) + apply (simp add: add.commute word_plus_and_or_coroll2) + apply (cut_tac x="(ptr_val p && mask pageBits ) >> 2" + and n="2 ^ (pageBits - 2) - 2 ^ (msg_align_bits - 2)" in unat_le_helper) + apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask) + apply word_bitwise + apply simp + apply (simp add: msg_align_bits pageBits_def) + done lemma getSyscallArg_ccorres_foo: "ccorres (\a rv. rv = args ! n) ret__unsigned_long_' @@ -1186,7 +1211,8 @@ lemma getSyscallArg_ccorres_foo: apply (rule ccorres_seq_skip [THEN iffD2]) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="\s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s" + apply (rule_tac P="\s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s + \ valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \ n < msgMaxLength" and P'=UNIV in ccorres_from_vcg_throws) apply (simp add: return_def split del: split_if) @@ -1198,6 +1224,10 @@ lemma getSyscallArg_ccorres_foo: apply simp apply (clarsimp simp: mult.commute mult.left_commute ucast_nat_def') apply (clarsimp simp: CTypesDefs.ptr_add_def) + apply (subst valid_ipc_buffer_ptr_array, assumption+) + apply (simp add: unat_def[symmetric] msg_align_bits + msgMaxLength_def unat_arith_simps) + apply simp apply (frule (1) user_word_at_cross_over) apply simp apply (clarsimp simp: mult.commute mult.left_commute ucast_nat_def) @@ -1208,7 +1238,7 @@ lemma getSyscallArg_ccorres_foo: msgLength mi \ msgMaxLength \ scast n_msgRegisters \ i" in hoare_pre(1)) apply (wp getMRs_user_word) - apply clarsimp + apply (clarsimp simp: msgMaxLength_def unat_less_helper) apply simp apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def) diff --git a/proof/crefine/TcbQueue_C.thy b/proof/crefine/TcbQueue_C.thy index 2dd15f6aa..0cf6598ab 100644 --- a/proof/crefine/TcbQueue_C.thy +++ b/proof/crefine/TcbQueue_C.thy @@ -1101,21 +1101,6 @@ proof - done qed -(* FIXME: move to SR_lemmas_C *) -(* FIXME: remove old version *) -lemma update_tcb_map_tos: - fixes P :: "tcb \ bool" - assumes at: "obj_at' P p s" - shows "map_to_eps (ksPSpace s(p \ KOTCB ko)) = map_to_eps (ksPSpace s)" - and "map_to_ntfns (ksPSpace s(p \ KOTCB ko)) = map_to_ntfns (ksPSpace s)" - and "map_to_pdes (ksPSpace s(p \ KOTCB ko)) = map_to_pdes (ksPSpace s)" - and "map_to_ptes (ksPSpace s(p \ KOTCB ko)) = map_to_ptes (ksPSpace s)" - and "map_to_asidpools (ksPSpace s(p \ KOTCB ko)) = map_to_asidpools (ksPSpace s)" - and "map_to_user_data (ksPSpace s(p \ KOTCB ko)) = map_to_user_data (ksPSpace s)" - using at - by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI - simp: projectKOs projectKO_opts_defs split: kernel_object.splits split_if_asm)+ - lemma rf_sr_tcb_update_no_queue: "\ (s, s') \ rf_sr; ko_at' tcb thread s; (cslift t :: tcb_C typ_heap) = (cslift s')(tcb_ptr_to_ctcb_ptr thread \ ctcb); @@ -1130,7 +1115,8 @@ lemma rf_sr_tcb_update_no_queue: \ \ (s\ksPSpace := ksPSpace s(thread \ KOTCB tcb')\, x\globals := globals s'\t_hrs_' := t_hrs_' (globals t)\\) \ rf_sr" unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def - apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes heap_to_page_data_def) + apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes + heap_to_page_data_def) apply (frule (1) cmap_relation_ko_atD) apply (erule obj_atE') apply (clarsimp simp: projectKOs) @@ -1179,7 +1165,8 @@ lemma rf_sr_tcb_update_not_in_queue: \ (s\ksPSpace := ksPSpace s(thread \ KOTCB tcb')\, x\globals := globals s'\t_hrs_' := t_hrs_' (globals t)\\) \ rf_sr" unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def - apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes heap_to_page_data_def) + apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes + heap_to_page_data_def) apply (frule (1) cmap_relation_ko_atD) apply (erule obj_atE') apply (clarsimp simp: projectKOs) diff --git a/proof/crefine/Tcb_C.thy b/proof/crefine/Tcb_C.thy index 5788c0bcb..91b89f818 100644 --- a/proof/crefine/Tcb_C.thy +++ b/proof/crefine/Tcb_C.thy @@ -1568,6 +1568,10 @@ lemma is_aligned_the_x_strengthen: "x \ None \ case_option \ valid_ipc_buffer_ptr' x s \ is_aligned (the x) msg_align_bits" by (clarsimp simp: valid_ipc_buffer_ptr'_def) +lemma valid_ipc_buffer_ptr_the_strengthen: + "x \ None \ case_option \ valid_ipc_buffer_ptr' x s \ valid_ipc_buffer_ptr' (the x) s" + by clarsimp + lemma lookupIPCBuffer_Some_0: "\\\ lookupIPCBuffer w t \\rv s. rv \ Some 0\" apply (simp add: lookupIPCBuffer_def @@ -1580,6 +1584,32 @@ lemma lookupIPCBuffer_Some_0: apply (rule hoare_vcg_prop , simp add:hoare_TrueI) done +lemma storeWordUser_array_ipcBuffer_ccorres: + "ccorres dc xfdc (valid_ipc_buffer_ptr' ptr and valid_pspace' and (\s. off < 2 ^ msg_align_bits)) + (UNIV \ {s. ptr' s = Ptr ptr} \ {s. off = of_int (n' s) * 4} + \ {s. n'' s = Suc (nat (n' s))} \ {s. w' s = w}) hs + (storeWordUser (ptr + off) w) + (Guard C_Guard \hrs_htd \t_hrs \\<^sub>t \(\s. ptr_add (ptr' s) (n' s))\ + (Guard gname \array_assertion \(\s. ptr' s) \(\s. n'' s) (hrs_htd \t_hrs)\ + (Basic (\s. globals_update (t_hrs_'_update + (hrs_mem_update (heap_update (ptr_add (ptr' s) (n' s)) (w' s)))) s))))" + apply (rule ccorres_guard_imp2) + apply (rule ccorres_second_Guard) + apply (rule storeWordUser_ccorres) + apply (clarsimp simp: Collect_const_mem) + apply (subst valid_ipc_buffer_ptr_array, simp+) + defer + apply simp + defer + apply (clarsimp simp: valid_ipc_buffer_ptr'_def msg_align_bits + is_aligned_add[OF is_aligned_weaken] + is_aligned_mult_triv2[where n=2, simplified]) + sorry +find_theorems lookupIPCBuffer valid_ipc_buffer_ptr' +lemma asUser_valid_ipc_buffer_ptr': + "\ valid_ipc_buffer_ptr' p \ asUser t m \ \rv s. valid_ipc_buffer_ptr' p s \" + by (simp add: valid_ipc_buffer_ptr'_def, wp, auto simp: valid_ipc_buffer_ptr'_def) + lemma invokeTCB_ReadRegisters_ccorres: notes min_simps [simp del] @@ -1703,26 +1733,29 @@ shows rule_tac F="\m s. obj_at' (\tcb. map (tcbContext tcb) (genericTake n (State_H.frameRegisters @ State_H.gpRegisters)) = reply) target s - \ is_aligned (the rva) msg_align_bits \ valid_pspace' s" + \ valid_ipc_buffer_ptr' (the rva) s + \ valid_pspace' s" and i="unat n_msgRegisters" in ccorres_mapM_x_while') - apply (clarsimp simp: less_diff_conv) + apply (intro allI impI, elim conjE exE, hypsubst, simp) + apply (simp add: less_diff_conv) apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return, ctac add: getRegister_ccorres_defer[where thread=target]) - apply (rule storeWordUser_ccorres) + apply (rule storeWordUser_array_ipcBuffer_ccorres) apply wp apply (vcg exspec=getRegister_modifies) apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI] word_size) apply (intro conjI[rotated] impI allI) - apply (simp add: n_msgRegisters_def n_frameRegisters_def - word_less_nat_alt) - apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1] - apply (erule sym) - apply (simp add: option_to_ptr_def option_to_0_def + apply (simp add: n_msgRegisters_def n_frameRegisters_def + word_less_nat_alt) + apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1] + apply (erule sym) + apply (simp add: option_to_ptr_def option_to_0_def msg_registers_convs upto_enum_word wordSize_def' - del: upt.simps) + del: upt.simps) + apply (simp add: option_to_ptr_def option_to_0_def) apply (rule frame_gp_registers_convs) apply (simp add: frame_gp_registers_convs less_diff_conv) apply (subst iffD1 [OF unat_add_lem]) @@ -1731,9 +1764,11 @@ shows word_le_nat_alt unat_of_nat) apply (simp add: n_frameRegisters_def n_msgRegisters_def unat_of_nat) - apply (erule aligned_add_aligned) - apply (simp add: word32_shift_by_2 is_aligned_shiftl_self) - apply (simp add: msg_align_bits) + apply (simp add: msg_registers_convs n_msgRegisters_def + msgMaxLength_def n_frameRegisters_def + upto_enum_word_nth msg_align_bits + ) + apply (simp add: unat_word_ariths word_less_nat_alt unat_of_nat) apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets obj_at'_weakenE[OF _ TrueI]) apply (clarsimp simp: asUser_fetch_def simpler_gets_def @@ -1802,35 +1837,38 @@ shows apply (rule_tac F="\m s. obj_at' (\tcb. map (tcbContext tcb) (genericTake n (State_H.frameRegisters @ State_H.gpRegisters)) = reply) target s - \ is_aligned (the rva) msg_align_bits \ valid_pspace' s" + \ valid_ipc_buffer_ptr' (the rva) s \ valid_pspace' s" and i="0" in ccorres_mapM_x_while') apply (clarsimp simp: less_diff_conv drop_zip) apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return, ctac add: getRegister_ccorres_defer[where thread=target]) - apply (rule storeWordUser_ccorres) + apply (rule storeWordUser_array_ipcBuffer_ccorres) apply wp apply (vcg exspec=getRegister_modifies) apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI] word_size) apply (intro conjI[rotated] impI allI) - apply (simp add: n_frameRegisters_def n_msgRegisters_def - length_msgRegisters word_of_nat_less - n_gpRegisters_def) - apply (erule sym) - apply (simp add: option_to_ptr_def option_to_0_def - msg_registers_convs upto_enum_word - n_msgRegisters_def n_frameRegisters_def - n_gpRegisters_def msgMaxLength_def msgLengthBits_def - del: upt.simps upt_rec_numeral) - apply (simp add: min_def split: split_if_asm) + apply (simp add: n_frameRegisters_def n_msgRegisters_def + length_msgRegisters word_of_nat_less + n_gpRegisters_def) + apply (erule sym) + apply (simp add: option_to_ptr_def option_to_0_def + msg_registers_convs upto_enum_word + n_msgRegisters_def n_frameRegisters_def + n_gpRegisters_def msgMaxLength_def msgLengthBits_def + del: upt.simps upt_rec_numeral) + apply (simp add: min_def split: split_if_asm) + apply (simp add: option_to_ptr_def option_to_0_def) apply (rule frame_gp_registers_convs) apply (simp add: frame_gp_registers_convs n_msgRegisters_def n_frameRegisters_def n_gpRegisters_def msgMaxLength_def msgLengthBits_def unat_of_nat) - apply (erule aligned_add_aligned) - apply (simp add: word32_shift_by_2 is_aligned_shiftl_self) - apply (simp add: msg_align_bits) + apply (simp add: msg_registers_convs n_msgRegisters_def + msgMaxLength_def n_frameRegisters_def + upto_enum_word_nth msg_align_bits + ) + apply (simp add: unat_word_ariths word_less_nat_alt unat_of_nat) apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets obj_at'_weakenE[OF _ TrueI]) apply (clarsimp simp: asUser_fetch_def simpler_gets_def @@ -1905,7 +1943,8 @@ shows apply simp apply (rule mapM_x_wp') apply (rule hoare_pre) - apply (wp asUser_obj_at'[where t'=target] static_imp_wp) + apply (wp asUser_obj_at'[where t'=target] static_imp_wp + asUser_valid_ipc_buffer_ptr') apply clarsimp apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem msg_registers_convs n_msgRegisters_def @@ -1914,10 +1953,11 @@ shows word_less_nat_alt unat_of_nat) apply (simp add: min_def split: split_if_asm) apply (wp_once hoare_drop_imps) - apply (wp asUser_obj_at'[where t'=target] static_imp_wp) + apply (wp asUser_obj_at'[where t'=target] static_imp_wp + asUser_valid_ipc_buffer_ptr') apply (vcg exspec=setRegister_modifies) apply simp - apply (strengthen is_aligned_the_x_strengthen) + apply (strengthen valid_ipc_buffer_ptr_the_strengthen) apply simp apply (wp lookupIPCBuffer_Some_0 | wp_once hoare_drop_imps)+ apply (simp add: Collect_const_mem State_H.badgeRegister_def diff --git a/proof/crefine/VSpace_C.thy b/proof/crefine/VSpace_C.thy index 599c06a9e..9ee7bcc6a 100644 --- a/proof/crefine/VSpace_C.thy +++ b/proof/crefine/VSpace_C.thy @@ -162,6 +162,28 @@ lemma rf_sr_asid_map_pd_to_hwasids: by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def) +lemma page_directory_at_carray_map_relation: + "\ page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp \ + \ clift hp (pd_Ptr pd) \ None" + apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) + apply (drule spec, erule iffD1) + apply (clarsimp simp: page_directory_at'_def) + apply (drule_tac x="p' && mask pdBits >> 2" in spec) + apply (clarsimp simp: shiftr_shiftl1) + apply (drule mp) + apply (simp add: shiftr_over_and_dist pdBits_def pageBits_def mask_def + order_le_less_trans[OF word_and_le1]) + apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def + is_aligned_andI1 add.commute word_plus_and_or_coroll2 + dest!: obj_at_ko_at' ko_at_projectKO_opt) + done + +lemma page_directory_at_rf_sr: + "\ page_directory_at' pd s; (s, s') \ rf_sr \ + \ cslift s' (pd_Ptr pd) \ None" + by (clarsimp simp: rf_sr_def cstate_relation_def Let_def + cpspace_relation_def page_directory_at_carray_map_relation) + lemma pd_at_asid_cross_over: "\ pd_at_asid' pd asid s; asid \ mask asid_bits; (s, s') \ rf_sr\ @@ -170,6 +192,7 @@ lemma pd_at_asid_cross_over: \ index ap (unat (asid && 2 ^ asid_low_bits - 1)) = pde_Ptr pd \ cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \ is_aligned pd pdBits + \ array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \ (valid_pde_mappings' s \ pde_get_tag pde = scast pde_pde_invalid)" apply (clarsimp simp: pd_at_asid'_def) apply (subgoal_tac "asid >> asid_low_bits \ 2 ^ asid_high_bits - 1") @@ -192,12 +215,14 @@ lemma pd_at_asid_cross_over: split: asid_pool_C.split_asm) apply (drule spec, drule sym [OF mp]) apply (rule_tac y=asid in word_and_le1) + apply (frule(1) page_directory_at_rf_sr) apply (clarsimp simp: mask_2pm1[symmetric] option_to_ptr_def option_to_0_def page_directory_at'_def typ_at_to_obj_at_arches) apply (drule_tac x="pd_asid_slot" in spec, simp add: pd_asid_slot_def) apply (drule obj_at_ko_at'[where 'a=pde], clarsimp) apply (rule cmap_relationE1 [OF rf_sr_cpde_relation], assumption, erule ko_at_projectKO_opt) + apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) apply (clarsimp simp: valid_pde_mappings'_def) apply (elim allE, drule(1) mp) apply (simp add: valid_pde_mapping'_def valid_pde_mapping_offset'_def @@ -253,6 +278,7 @@ lemma loadHWASID_ccorres: apply (frule(2) pd_at_asid_cross_over) apply (clarsimp simp: asidLowBits_handy_convs word_sless_def word_sle_def) apply (clarsimp simp: typ_heap_simps order_le_less_trans[OF word_and_le1] + array_assertion_shrink_right ptr_add_assertion_def arg_cong[where f="\x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) apply (clarsimp split: option.split) apply (frule_tac x=pd in fun_cong [OF rf_sr_asid_map_pd_to_hwasids]) @@ -333,6 +359,7 @@ lemma storeHWASID_ccorres: carch_state_relation_def pd_at_asid'_def fun_upd_def[symmetric] carch_globals_def order_le_less_trans[OF word_and_le1] + array_assertion_shrink_right arg_cong[where f="\x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) apply (subgoal_tac "ucast hw_asid ucast hw_asid < (256 :: sword32) \ (0 :: sword32) <=s ucast hw_asid") @@ -428,7 +455,8 @@ lemma invalidateASID_ccorres: apply (frule(2) pd_at_asid_cross_over) apply (clarsimp simp: typ_heap_simps) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cpspace_relation_def) + cpspace_relation_def + array_assertion_shrink_right) apply (clarsimp simp: typ_heap_simps cmachine_state_relation_def carch_state_relation_def pd_at_asid'_def carch_globals_def fun_upd_def[symmetric] order_le_less_trans[OF word_and_le1] @@ -717,30 +745,33 @@ lemma generic_frame_cap_ptr_set_capFMappedAddress_spec: apply (clarsimp simp: cte_lift_def) done - lemma lookupPDSlot_spec: - "\s. \ \ {s} + "\s. \ \ \s. array_assertion (pd_' s) (2 ^ pageBits) (hrs_htd (\t_hrs))\ Call lookupPDSlot_'proc \ \ret__ptr_to_struct_pde_C = Ptr (lookupPDSlot (ptr_val (pd_' s)) (vptr_' s)) \" apply vcg apply (clarsimp simp: lookupPDSlot_def) apply (simp add: ArchVSpaceAcc_A.lookup_pd_slot_def) + apply (subst array_assertion_shrink_right, assumption) + apply (rule unat_le_helper, simp) + apply (rule order_less_imp_le, rule vptr_shiftr_le_2p) apply (simp add: Let_def word_sle_def) - apply (case_tac pd) - apply simp + apply (case_tac pd) apply (simp add: word32_shift_by_2) done lemma lookupPTSlot_nofail_spec: - "\s. \ \ {s} + "\s. \ \ \s. array_assertion (pt_' s) (2 ^ (ptBits - 2)) (hrs_htd (\t_hrs))\ Call lookupPTSlot_nofail_'proc \ \ret__ptr_to_struct_pte_C = Ptr (lookupPTSlot_nofail (ptr_val (pt_' s)) (vptr_' s)) \" apply vcg apply (clarsimp simp: lookupPTSlot_nofail_def) apply (simp add: ArchVSpaceAcc_A.lookup_pt_slot_no_fail_def) + apply (subst array_assertion_shrink_right, assumption) + apply (rule order_less_imp_le, rule unat_less_helper, simp) + apply (rule order_le_less_trans, rule word_and_le1, simp add: ptBits_def pageBits_def) apply (simp add: Let_def word_sle_def) apply (case_tac pt) - apply simp apply (simp add: word32_shift_by_2) done @@ -811,8 +842,31 @@ lemma cpde_relation_pde_coarse: apply (simp add: pde_pde_coarse_lift_def) done +lemma page_table_at_carray_map_relation: + "\ page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp \ + \ clift hp (pt_Ptr pt) \ None" + apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) + apply (drule spec, erule iffD1) + apply (clarsimp simp: page_table_at'_def) + apply (drule_tac x="p' && mask ptBits >> 2" in spec) + apply (clarsimp simp: shiftr_shiftl1) + apply (drule mp) + apply (simp add: shiftr_over_and_dist ptBits_def pageBits_def mask_def + order_le_less_trans[OF word_and_le1]) + apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def + is_aligned_andI1 add.commute word_plus_and_or_coroll2 + dest!: obj_at_ko_at' ko_at_projectKO_opt) + done + +lemma page_table_at_rf_sr: + "\ page_table_at' pd s; (s, s') \ rf_sr \ + \ cslift s' (Ptr pd :: (pte_C[256]) ptr) \ None" + by (clarsimp simp: rf_sr_def cstate_relation_def Let_def + cpspace_relation_def page_table_at_carray_map_relation) + lemma lookupPTSlot_ccorres: - "ccorres (lookup_failure_rel \ (\rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf \ + "ccorres (lookup_failure_rel \ (\rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf + (page_directory_at' pd) (UNIV \ \\pd = Ptr pd \ \ \\vptr = vptr \) [] (lookupPTSlot pd vptr) @@ -835,40 +889,30 @@ lemma lookupPTSlot_ccorres: apply (simp add: lookup_fault_missing_capability_lift) apply (simp add: mask_def) apply (rule ccorres_rhs_assoc)+ - apply csymbr - apply csymbr - apply csymbr - apply csymbr - apply (rule ccorres_abstract_cleanup) - apply (rule_tac P="ret__unsigned_long = pdeTable rv" - in ccorres_gen_asm2) - apply simp - apply (simp add: word_sle_def) apply (simp add:liftE_bindE checkPTAt_def) apply (rule ccorres_stateAssert) - apply (rule_tac R=\ and Q' = "UNIV - \ {s. pt_' s = Ptr (ptrFromPAddr ret__unsigned_long)}" in ccorres_symb_exec_r) - apply (rule ccorres_tmp_lift2) - apply ceqv - apply (rule ccorres_Guard_Seq)+ - apply csymbr - apply csymbr - apply csymbr - apply csymbr - apply (rule ccorres_return_CE, simp+)[1] - apply (clarsimp simp: Collect_const_mem shiftl_t2n) - apply simp - apply vcg - apply (rule conseqPre, vcg) - apply clarsimp - apply (clarsimp simp: Collect_const_mem) - apply (frule h_t_valid_clift, simp) - apply (intro conjI impI) - apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def - pde_lift_pde_coarse Let_def) - apply (clarsimp split: Hardware_H.pde.split_asm) - apply (drule cpde_relation_pde_coarse, simp) -done + apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable rv)) + and ko_at' rv (lookup_pd_slot pd vptr) + and K (isPageTablePDE rv)" and P'=UNIV in ccorres_from_vcg_throws) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: returnOk_def return_def Collect_const_mem + lookup_pd_slot_def word_sle_def) + apply (frule(1) page_table_at_rf_sr, clarsimp) + apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps cpde_relation_def Let_def isPageTablePDE_def + pde_pde_coarse_lift_def pde_pde_coarse_lift + split: pde.split_asm) + apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) + apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp) + apply (simp add: word32_shift_by_2) + apply (clarsimp simp: Collect_const_mem h_t_valid_clift) + apply (frule(1) page_directory_at_rf_sr, clarsimp) + apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) + apply (simp add: pageBits_def) + apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def + pde_pde_coarse_lift Let_def isPageTablePDE_def + split: Hardware_H.pde.split_asm) + done lemma cap_case_isPageDirectoryCap: "(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \ fn pd asid @@ -1484,10 +1528,21 @@ lemma ccorres_h_t_valid_armKSGlobalPD: apply (simp add:rf_sr_def cstate_relation_def Let_def) done +lemma array_assertion_abs_tcb_ctes: + "\s s'. (s, s') \ rf_sr \ tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s \ (of_nat n < tcbCNodeEntries) + \ array_assertion (cte_Ptr (ptr_val (tcb s') && 0xFFFFFE00)) n (hrs_htd (t_hrs_' (globals s')))" + (* going to need to assert this too, sigh *) + sorry + +lemmas ccorres_move_array_assertion_tcb_ctes [corres_pre] + = ccorres_move_Guard_Seq [OF array_assertion_abs_tcb_ctes] + ccorres_move_Guard [OF array_assertion_abs_tcb_ctes] + lemma setVMRoot_ccorres: "ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' thread) (UNIV \ {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) [] (setVMRoot thread) (Call setVMRoot_'proc)" apply (cinit lift: tcb_') + apply (rule ccorres_move_array_assertion_tcb_ctes) apply (rule ccorres_move_c_guard_cte) apply (simp add: getThreadVSpaceRoot_def locateSlot_conv) apply (ctac) @@ -1588,7 +1643,7 @@ lemma setVMRoot_ccorres: apply (auto simp: isCap_simps valid_cap'_def mask_def)[1] apply (clarsimp simp: ptr_val_tcb_ptr_mask' size_of_def cte_level_bits_def - tcbVTableSlot_def Kernel_C.tcbVTable_def + tcbVTableSlot_def tcb_cnode_index_defs ccap_rights_relation_def cap_rights_to_H_def to_bool_def true_def allRights_def mask_def[where n="Suc 0"] @@ -1607,7 +1662,6 @@ lemma invs'_invs_no_cicd: "invs' s \ all_invs_but_ct_idle_or_in_cur_domain' s" by (clarsimp simp add: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def newKernelState_def) - lemma setVMRootForFlush_ccorres: "ccorres (\rv rv'. rv' = from_bool rv) ret__unsigned_long_' (invs' and (\s. asid \ mask asid_bits)) @@ -1652,6 +1706,9 @@ lemma setVMRootForFlush_ccorres: mask_def[where n="Suc 0"] true_def to_bool_def allRights_def size_of_def cte_level_bits_def tcbVTableSlot_def Kernel_C.tcbVTable_def invs'_invs_no_cicd) + apply (clarsimp simp: rf_sr_ksCurThread) + apply (subst array_assertion_abs_tcb_ctes, simp add: tcb_cnode_index_defs, + fastforce intro: tcb_at_invs')+ apply (clarsimp simp: rf_sr_ksCurThread ptr_val_tcb_ptr_mask' [OF tcb_at_invs']) apply (frule cte_at_tcb_at_16'[OF tcb_at_invs'], clarsimp simp: cte_wp_at_ctes_of) apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) @@ -2199,6 +2256,108 @@ lemma pte_pte_invalid_new_spec: apply (clarsimp simp: pte_lift_def pte_get_tag_def pte_pte_large_def fupdate_def) done +lemma ccorres_name_pre_C: + "(\s. s \ P' \ ccorres_underlying sr \ r xf arrel axf P {s} hs f g) + \ ccorres_underlying sr \ r xf arrel axf P P' hs f g" + apply (rule ccorres_guard_imp) + apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl) + apply (rule_tac P="rv' \ P'" in ccorres_gen_asm2) + apply assumption + apply simp + apply simp + done + +lemma ccorres_second_Guard: + assumes cc: "ccorres_underlying sr \ r xf arrel axf A C' hs a (Guard F1 S1 c)" + shows "ccorres_underlying sr \ r xf arrel axf A (C' \ S) hs a (Guard F1 S1 (Guard F S c))" + apply (rule ccorres_name_pre_C) + apply (rule ccorres_guard_imp) + apply (rule_tac xf'=id in ccorres_abstract) + apply (rule Guard_ceqv, rule impI, rule refl) + apply (rule_tac x'="{_. rv' \ S}" in Guard_ceqv) + apply (clarsimp simp: Collect_const_mem) + apply (rule ceqv_refl) + apply (rule_tac P="rv' = s" in ccorres_gen_asm2) + apply simp + apply (rule_tac xf'=xfdc in ccorres_abstract) + apply (rule Guard_ceqv, rule impI, rule refl) + apply (rule ceqv_Guard_UNIV[THEN iffD2]) + apply (rule ceqv_refl) + apply (rule cc) + apply simp + apply simp + done + +lemma clift_array_assertion_imp: + "clift hrs (p :: (('a :: wf_type)['b :: finite]) ptr) = Some v + \ htd = hrs_htd hrs + \ n \ 0 + \ \i. p' = ptr_add (ptr_coerce p) (int i) + \ i + n \ CARD('b) + \ array_assertion (p' :: 'a ptr) n htd" + apply clarsimp + apply (drule h_t_valid_clift) + apply (drule array_ptr_valid_array_assertionD) + apply (drule_tac j=i in array_assertion_shrink_left, simp) + apply (erule array_assertion_shrink_right) + apply simp + done + +lemma multiple_add_less_nat: + "a < (c :: nat) \ x dvd a \ x dvd c \ b < x + \ a + b < c" + apply (subgoal_tac "b < c - a") + apply simp + apply (erule order_less_le_trans) + apply (rule dvd_imp_le) + apply simp + apply simp + done + +lemma large_ptSlot_array_constraint: + "is_aligned (ptSlot :: word32) 6 \ n < 16 + \ \i. ptSlot = (ptSlot && ~~ mask ptBits) + of_nat i * 4 \ i + n \ 255" + apply (rule_tac x="unat ((ptSlot && mask ptBits) >> 2)" in exI) + apply (simp add: shiftl_t2n[where n=2, symmetric, THEN trans[rotated], + OF mult.commute, simplified]) + apply (simp add: shiftr_shiftl1) + apply (rule conjI, rule trans, + rule word_plus_and_or_coroll2[symmetric, where w="mask ptBits"]) + apply (simp, rule aligned_neg_mask[THEN sym], rule is_aligned_andI1, + erule is_aligned_weaken, simp) + apply (rule less_Suc_eq_le[THEN iffD1]) + apply (rule_tac x="2 ^ 4" in multiple_add_less_nat, simp_all)[1] + apply (rule unat_less_helper, simp) + apply (rule order_less_le_trans, rule shiftr_less_t2n[where m="ptBits - 2"]) + apply (rule order_le_less_trans, rule word_and_le1, simp add: mask_def ptBits_def pageBits_def) + apply (simp add: ptBits_def pageBits_def) + apply (simp add: is_aligned_def[where n=4, simplified, symmetric]) + apply (rule is_aligned_shiftr, rule is_aligned_andI1, simp) + done + +lemma large_pdSlot_array_constraint: + "is_aligned pd pdBits \ vmsz_aligned vptr ARMSuperSection \ n < 16 + \ \i. lookup_pd_slot pd vptr = pd + of_nat i * 4 \ i + n \ 4095" + apply (rule_tac x="unat (vptr >> 20)" in exI) + apply (rule conjI) + apply (simp add: lookup_pd_slot_def shiftl_t2n) + apply (rule less_Suc_eq_le[THEN iffD1]) + apply (rule_tac x="2 ^ 4" in multiple_add_less_nat, simp_all)[1] + apply (rule unat_less_helper, simp) + apply (rule order_less_le_trans, rule shiftr_less_t2n3[where m=12], simp+) + apply (simp add: is_aligned_def[where n=4, simplified, symmetric] + vmsz_aligned_def is_aligned_shiftr) + done + +lemma findPDForASID_page_directory_at'_simple[wp]: + notes checkPDAt_inv[wp del] + shows "\\\ findPDForASID asiv + \\rv s. page_directory_at' rv s\,-" + apply (simp add:findPDForASID_def) + apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+ + apply auto + done + lemma unmapPage_ccorres: "ccorres dc xfdc (invs' and (\s. 2 ^ pageBitsForSize sz \ gsMaxObjectSize s) and (\_. asid \ mask asid_bits \ vmsz_aligned' vptr sz @@ -2263,6 +2422,7 @@ lemma unmapPage_ccorres: apply csymbr apply csymbr apply (ctac add: lookupPTSlot_ccorres) + apply (rename_tac ptSlot lookupPTSlot_ret) apply (simp add: Collect_False dc_def[symmetric] del: Collect_const) apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) @@ -2282,13 +2442,24 @@ lemma unmapPage_ccorres: apply (ccorres_remove_UNIV_guard) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow_novcg) - apply (rule_tac F="\\" in ccorres_mapM_x_while) + apply (rule_tac P="is_aligned ptSlot 6" in ccorres_gen_asm) + apply (rule_tac F="\_. page_table_at' (ptSlot && ~~ mask ptBits)" + in ccorres_mapM_x_while) apply clarsimp apply (rule ccorres_guard_imp2) apply csymbr + apply (rule ccorres_Guard) + apply (rule ccorres_second_Guard) apply (rule storePTE_Basic_ccorres) apply (simp add: cpte_relation_def Let_def) apply clarsimp + apply (drule(1) page_table_at_rf_sr, clarsimp) + apply (simp add: clift_array_assertion_imp unat_of_nat + upto_enum_step_def large_ptSlot_array_constraint) + apply (subst clift_array_assertion_imp, assumption, + simp_all add: unat_of_nat + upto_enum_step_def)[1] + apply (simp add: large_ptSlot_array_constraint) apply (simp add: upto_enum_step_def upto_enum_word del: upt.simps) @@ -2304,7 +2475,7 @@ lemma unmapPage_ccorres: apply (rule ccorres_move_c_guard_pte, ccorres_remove_UNIV_guard) apply (rule ccorres_move_c_guard_pte, ccorres_remove_UNIV_guard) apply (ctac add: cleanCacheRange_PoU_ccorres[unfolded dc_def]) - apply (rule_tac P="is_aligned rva 6" in hoare_gen_asm) + apply (rule_tac P="is_aligned ptSlot 6" in hoare_gen_asm) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule_tac P="\s. 2 ^ pageBitsForSize sz \ gsMaxObjectSize s" @@ -2335,7 +2506,8 @@ lemma unmapPage_ccorres: apply (rule ccorres_split_throws) apply (rule ccorres_return_void_C') apply vcg - apply (wp lookupPTSlot_inv Arch_R.lookupPTSlot_aligned | simp add: K_def)+ + apply (wp lookupPTSlot_inv Arch_R.lookupPTSlot_aligned + lookupPTSlot_page_table_at' | simp add: K_def)+ apply (vcg exspec=lookupPTSlot_modifies) -- "ARMSection" apply (rule ccorres_Cond_rhs) @@ -2403,15 +2575,21 @@ lemma unmapPage_ccorres: apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) apply (rule_tac P="is_aligned rv pdBits" in ccorres_gen_asm) - apply (rule_tac F="\\" in ccorres_mapM_x_while) + apply (rule_tac F="\_. page_directory_at' rv" in ccorres_mapM_x_while) apply clarsimp apply (rule ccorres_guard_imp2) apply csymbr + apply (rule ccorres_second_Guard) apply (rule storePDE_Basic_ccorres) apply (simp add: cpde_relation_def Let_def pde_lift_pde_invalid) apply clarsimp - apply (simp add: upto_enum_step_def upto_enum_word) + apply (drule(1) page_directory_at_rf_sr, clarsimp) + apply (simp add: unat_def[symmetric] unat_of_nat + upto_enum_step_def upto_enum_word) + apply (subst clift_array_assertion_imp, assumption, simp_all)[1] + apply (rule large_pdSlot_array_constraint, simp_all)[1] + apply (simp add: vmsz_aligned'_def vmsz_aligned_def) apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned field_simps) apply (erule less_kernelBase_valid_pde_offset') diff --git a/spec/cspec/Substitute.thy b/spec/cspec/Substitute.thy index 5ff5c6ddd..62935b8c4 100644 --- a/spec/cspec/Substitute.thy +++ b/spec/cspec/Substitute.thy @@ -44,7 +44,7 @@ fun suspicious_term ctxt s t = if Term.add_var_names t [] = [] then () val debug_trace = ref (Bound 0); fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) = - (term_convert prefix convs tm; (convs, ctxt)) + ((term_convert prefix convs tm; (convs, ctxt)) handle Option => let val cname = unprefix prefix name; @@ -80,7 +80,9 @@ fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) = val abs_tm = list_abs (map (pair "_") lhs_argTs, tm'') in (Termtab.insert (K true) (tm, abs_tm) convs, ctxt) end - end + end) + | convert _ _ _ (tm) _ = raise TERM ("convert: not Const", [tm]) + fun prove_impl_tac ctxt ss = SUBGOAL (fn (t, n) => let @@ -311,6 +313,29 @@ val guard_halt = com_rewrite then (t, [(@{term DontReach}, @{term "{} :: globals myvars set"})]) else (t, [])) +fun acc_ptr_adds (Const (@{const_name h_val}, _) $ m $ (Const (@{const_name ptr_add}, _) $ p $ n)) + = [(p, n, true)] @ maps acc_ptr_adds [m, p, n] + | acc_ptr_adds (Const (@{const_name heap_update}, _) $ (Const (@{const_name ptr_add}, _) $ p $ n)) + = [(p, n, true)] @ maps acc_ptr_adds [p, n] + | acc_ptr_adds (Const (@{const_name ptr_add}, _) $ p $ n) + = [(p, n, false)] @ maps acc_ptr_adds [p, n] + | acc_ptr_adds (f $ x) = maps acc_ptr_adds [f, x] + | acc_ptr_adds (abs as Abs (_, T, t)) = if T = @{typ "globals myvars"} + then acc_ptr_adds (betapply (abs, @{term "s :: globals myvars"})) + else acc_ptr_adds t + | acc_ptr_adds _ = [] + +fun mk_bool true = @{term True} | mk_bool false = @{term False} + +val guard_acc_ptr_adds = com_rewrite + (fn t => (t, acc_ptr_adds t |> map (fn (p, n, strong) => let + val assn = Const (@{const_name ptr_add_assertion}, + fastype_of p --> @{typ "int \ bool \ heap_typ_desc \ bool"}) + $ p $ n $ mk_bool strong + $ @{term "hrs_htd (t_hrs_' (globals (s :: globals myvars)))"} + val gd = HOLogic.mk_Collect ("s", @{typ "globals myvars"}, assn) + in (@{term MemorySafety}, gd) end))) + end *} @@ -325,7 +350,8 @@ SubstituteSpecs.take_all_actions o (strengthen_c_guards ["memset_body", "memcpy_body", "memzero_body"] (Proof_Context.theory_of ctxt) s) o guard_halt - o guard_htd_updates_with_domain) + o guard_htd_updates_with_domain + o guard_acc_ptr_adds) @{term kernel_all_global_addresses.\} (CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the) [@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}] diff --git a/tools/c-parser/CProof.thy b/tools/c-parser/CProof.thy index 42f3eeaf1..1a9db273d 100644 --- a/tools/c-parser/CProof.thy +++ b/tools/c-parser/CProof.thy @@ -13,6 +13,7 @@ imports "umm_heap/SepFrame" "Simpl/Vcg" "umm_heap/StructSupport" + "umm_heap/ArrayAssertion" begin (* name generation is the only thing this theory wants, but that